urbit/ares
1
1
Fork 0
mirror of https://github.com/urbit/ares.git synced 2024-11-26 09:57:56 +03:00
Code Issues Packages Projects Releases Wiki Activity
30e8a915b2
ares/hoon/codegen/lib/ska.hoon
Edward Amsden 6615cd30e1 [ska] make ska spec work properly
2023-03-13 12:12:51 -05:00

703 lines
16 KiB
Plaintext
Raw Blame History

/- *sock
!:
|%
++ trip
|= toob=$<(%boom boot)
^- (unit *)
?- -.toob
%safe (stub sure.toob)
%risk (stub hope.toob)
==
++ stub
|= =sock
^- (unit *)
?: ?=(%know -.sock)
`know.sock
~
:: Split an axis into a sock into safe and unsafe components
++ punt
|= [axe=@ =sock]
^- [@ @ ^sock]
?: =(0 axe)
[0 0 %toss ~]
=/ saf 1
|-
?: =(axe 1)
[saf 1 sock]
?+ sock [0 0 %toss ~]
[%know * *]
?- (cap axe)
%2 $(axe (mas axe), sock [%know -.know.sock], saf (peg saf 2))
%3 $(axe (mas axe), sock [%know +.know.sock], saf (peg saf 3))
==
::
[%bets *]
?- (cap axe)
%2 $(axe (mas axe), sock hed.sock, saf (peg saf 2))
%3 $(axe (mas axe), sock tal.sock, saf (peg saf 3))
==
::
[%toss ~]
[saf axe %toss ~]
==
:: Get an axis from a sock
++ pull
|= arg=[@ sock]
^- boot
=+ [saf rik ken]=(punt arg)
?: =(0 saf) [%boom ~]
?: =(1 rik) [%safe ken]
[%risk ken]
++ yank
|= [axe=@ =boot]
?- boot
[%safe *] (pull axe sure.boot)
[%risk *] (dare (pull axe hope.boot))
[%boom ~] [%boom ~]
==
:: Test if sock is atom or cell, or unknown
++ fits
|= =sock
^- ^sock
?- sock
::
[%know @]
[%know 1]
::
[%know * *]
[%know 0]
::
[%bets *]
[%know 0]
::
[%dice ~]
[%know 1]
::
[%flip ~]
[%know 1]
::
[%toss ~]
[%flip ~]
==
:: Test if we can know two socks are equal
++ pear
|= [a=sock b=sock]
^- sock
?: ?&(?=([%know *] a) ?=([%know *] b))
?: =(know.a know.b)
[%know 0]
[%know 1]
[%flip ~]
:: Test if we can know two boots are equal
++ bopp
|= [a=boot b=boot]
^- boot
?: ?= [%boom ~] a
[%boom ~]
?: ?= [%boom ~] b
[%boom ~]
?- a
::
[%safe *]
?- b
::
[%safe *]
[%safe (pear sure.a sure.b)]
::
[%risk *]
[%risk (pear sure.a hope.b)]
==
::
[%risk *]
?- b
::
[%safe *]
[%risk (pear hope.a sure.b)]
::
[%risk *]
[%risk (pear hope.a hope.b)]
==
==
:: combine two socks into a sock of a cell
++ knit
|= [a=sock b=sock]
^- sock
?. ?= [%know *] a
[%bets a b]
?. ?= [%know *] b
[%bets a b]
[%know [know.a know.b]]
:: combine two boots into a boot of a cell
++ cobb
|= [hed=boot tal=boot]
^- boot
?: ?= [%boom ~] hed
[%boom ~]
?: ?= [%boom ~] tal
[%boom ~]
?- hed
::
[%safe *]
?- tal
::
[%safe *]
[%safe (knit sure.hed sure.tal)]
::
[%risk *]
[%risk (knit sure.hed hope.tal)]
==
::
[%risk *]
?- tal
::
[%safe *]
[%risk (knit hope.hed sure.tal)]
::
[%risk *]
[%risk (knit hope.hed hope.tal)]
==
==
:: patch a sock
++ darn
|= [axe=@ pat=sock =sock]
^- boot
?: .= 0 axe
[%boom ~]
|-
^- boot
?: =(axe 1)
[%safe pat]
?: ?= [%dice ~] sock
[%boom ~]
?: ?= [%flip ~] sock
[%boom ~]
?: ?= [%know @] sock
[%boom ~]
?- (cap axe)
::
%2
?- sock
::
[%know * *]
(cobb $(axe (mas axe), sock [%know -.know.sock]) [%safe %know +.know.sock])
::
[%bets * *]
(cobb $(axe (mas axe), sock hed.sock) [%safe tal.sock])
::
[%toss ~]
(cobb $(axe (mas axe)) [%risk %toss ~])
==
::
%3
?- sock
::
[%know * *]
(cobb [%safe %know -.know.sock] $(axe (mas axe), sock [%know +.know.sock]))
::
[%bets * *]
(cobb [%safe hed.sock] $(axe (mas axe), sock tal.sock))
::
[%toss ~]
(cobb [%risk %toss ~] $(axe (mas axe)))
==
==
:: Stitch a boot into another boot
++ welt
|= [axe=@ pach=boot wole=boot]
^- boot
?: ?= [%boom ~] pach
[%boom ~]
?: ?= [%boom ~] wole
[%boom ~]
=/ poch
?- pach
::
[%safe *]
sure.pach
::
[%risk *]
hope.pach
==
=/ wool
?- wole
::
[%safe *]
sure.wole
::
[%risk *]
hope.wole
==
?: ?& ?= [%safe *] wole ?= [%safe *] pach ==
(darn axe poch wool)
(dare (darn axe poch wool))
:: Pessimize a boot by making it %risk even if it's %safe
++ dare
|= =boot
?- boot
::
[%boom ~]
[%boom ~]
::
[%risk *]
[%risk hope.boot]
::
[%safe *]
[%risk sure.boot]
==
:: Weaken a %know
++ fray
|= a=*
^- sock
?: ?= @ a
[%dice ~]
[%bets [%know -.a] [%know +.a]]
:: Produce the intersection of two socks
++ mous
|= [a=sock b=sock]
?: ?&(?=([%know *] a) ?=([%know *] b))
?: =(know.a know.b)
a
$(a (fray know.a), b (fray know.b))
?: ?=([%know *] a)
$(a (fray know.a))
?: ?=([%know *] b)
$(b (fray know.b))
?: ?&(?=([%bets *] a) ?=([%bets *] b))
[%bets $(a hed.a, b hed.b) $(a tal.a, b tal.b)]
?: ?&(?=([%dice ~] a) ?|(?=([%dice ~] b) ?=([%flip ~] b)))
[%dice ~]
?: ?&(?=([%dice ~] b) ?=([%flip ~] a))
[%dice ~]
?: ?&(?=([%flip ~] a) ?=([%flip ~] b))
[%flip ~]
[%toss ~]
:: Produce the intersection of two boots
::
:: Note that the intersection of a safe or risk
:: boot and a boom boot is a risk boot, since
:: in a branch between a possibly non-crashing computation
:: and a crashing computation, we might crash and we might not.
::
:: In particular, we have to handle assertions and
:: error cases where it is intended that one branch of a conditional
:: will crash
++ gnaw
|= [a=boot b=boot]
?: ?= [%safe *] a
?: ?= [%safe *] b
[%safe (mous sure.a sure.b)]
?: ?= [%risk *] b
[%risk (mous sure.a hope.b)]
[%risk sure.a]
?: ?= [%risk *] a
?: ?= [%safe *] b
[%risk (mous hope.a sure.b)]
?: ?= [%risk *] b
[%risk (mous hope.a hope.b)]
[%risk hope.a]
?: ?= [%safe *] b
[%risk sure.b]
?: ?= [%risk *] b
[%risk hope.b]
[%boom ~]
:: Produce a boot of whether a given boot is a cell or atom
++ ques
|= non=boot
^- boot
?: ?=([%boom ~] non)
[%boom ~]
?- non
::
[%safe %know @]
[%safe %know 1]
::
[%safe %know * *]
[%safe %know 0]
::
[%safe %bets *]
[%safe %know 0]
::
[%safe %dice ~]
[%safe %know 1]
::
[%safe %flip ~]
[%safe %know 1]
::
[%safe %toss ~]
[%safe %flip ~]
::
[%risk %know @]
[%risk %know 1]
::
[%risk %know * *]
[%risk %know 0]
::
[%risk %bets *]
[%risk %know 0]
::
[%risk %dice ~]
[%risk %know 1]
::
[%risk %flip ~]
[%risk %know 1]
::
[%risk %toss ~]
[%risk %flip ~]
==
++ pile
|= tom=boot
^- boot
?+ tom [%boom ~]
::
[%safe %know @]
[%safe %dice ~]
::
[%safe %dice ~]
[%safe %dice ~]
::
[%safe %flip ~]
[%safe %dice ~]
::
[%safe %toss ~]
[%risk %dice ~]
::
[%risk %know @]
[%risk %dice ~]
::
[%risk %dice ~]
[%risk %dice ~]
::
[%risk %flip ~]
[%risk %dice ~]
::
[%risk %toss ~]
[%risk %dice ~]
==
:: Produce knowledge of the result given knowledge of the subject
++ wash
|= [subj=sock form=*]
^- boot
=| bare=[ward=(map [sock *] boot) dir=@ ind=@]
=. ward.bare (~(put by ward.bare) [subj form] [%risk %toss ~])
|^
=+ swab
~& "direct calls: {<dir>}"
~& "indirect calls: {<ind>}"
-<
++ swab
|-
^- [boot _bare]
?> ?=(^ form)
?+ form [[%boom ~] bare]
::
[[* *] *]
=^ l bare $(form -.form)
=^ r bare $(form +.form)
:_ bare
(cobb l r)
::
[%0 @]
:_ bare
(pull +.form subj)
::
[%1 *]
:_ bare
[%safe %know +.form]
::
[%2 * *]
=^ subn bare $(form +<.form)
?: ?=([%boom ~] subn)
[[%boom ~] bare]
=^ forn bare $(form +>.form)
?: ?=([%boom ~] forn)
[[%boom ~] bare]
?: ?= [%safe %dice ~] forn
[[%boom ~] bare]
?: ?= [%safe %flip ~] forn
[[%boom ~] bare]
?: ?= [%risk %dice ~] forn
[[%boom ~] bare]
?: ?= [%risk %flip ~] forn
[[%boom ~] bare]
?+ forn [[%risk %toss ~] bare(ind .+(ind.bare))]
::
[%safe %know *]
=. dir.bare .+(dir.bare)
?- subn
::
[%safe *]
=/ nubs sure.subn
=/ norm know.sure.forn
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
[r bare(ward (~(put by ward.bare) [nubs norm] r))]
::
[%risk *]
=/ nubs hope.subn
=/ norm know.sure.forn
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
[(dare r) bare(ward (~(put by ward.bare) [nubs norm] (dare r)))] :: XX fix up ward modifications
==
::
[%risk %know *]
=. dir.bare .+(dir.bare)
?- subn
::
[%safe *]
=/ nubs sure.subn
=/ norm know.hope.forn
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
[(dare r) bare(ward (~(put by ward.bare) [nubs norm] (dare r)))]
::
[%risk *]
=/ nubs hope.subn
=/ norm know.hope.forn
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
[(dare r) bare(ward (~(put by ward.bare) [nubs norm] (dare r)))]
==
==
::
[%3 *]
=^ s bare $(form +.form)
:_ bare
(ques s)
::
[%4 *]
=^ s bare $(form +.form)
:_ bare
(pile s)
::
[%5 * *]
=^ l bare $(form +<.form)
=^ r bare $(form +>.form)
:_ bare
(bopp l r)
::
[%6 * * *]
=^ cond bare $(form +<.form)
?+ cond [[%boom ~] bare]
::
[%safe *]
?+ sure.cond [[%boom ~] bare]
::
[%know %0]
$(form +>-.form)
::
[%know %1]
$(form +>+.form)
::
[%flip ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(gnaw t f)
::
[%dice ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(dare (gnaw t f))
::
[%toss ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(dare (gnaw t f))
==
::
[%risk *]
?+ hope.cond [[%boom ~] bare]
::
[%know %0]
=^ t bare $(form +>-.form)
:_ bare
(dare t)
::
[%know %1]
=^ f bare $(form +>+.form)
:_ bare
(dare f)
::
[%flip ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(dare (gnaw t f))
::
[%dice ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(dare (gnaw t f))
::
[%toss ~]
=^ t bare $(form +>-.form)
=^ f bare $(form +>+.form)
:_ bare
(dare (gnaw t f))
==
==
::
[%7 * *]
=^ news bare $(form +<.form)
?+ news [[%boom ~] bare]
::
[%safe *]
$(subj sure.news, form +>.form)
::
[%risk *]
=^ r bare $(subj hope.news, form +>.form)
:_ bare
(dare r)
==
::
[%8 * *]
=^ news bare $(form +<.form)
?+ news [[%boom ~] bare]
::
[%safe *]
$(subj (knit sure.news subj), form +>.form)
::
[%risk *]
=^ r bare $(subj (knit hope.news subj), form +>.form)
:_ bare
(dare r)
==
::
[%9 @ *]
=^ news bare $(form +>.form)
?+ news [[%boom ~] bare]
::
[%safe *]
=/ newf (pull +<.form sure.news)
?+ newf [[%boom ~] bare]
::
[%safe %know *]
=. dir.bare .+(dir.bare)
=/ nubs sure.news
=/ norm know.sure.newf
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
:_ bare(ward (~(put by ward.bare) [nubs norm] r))
r
::
[%risk %know *]
=. dir.bare .+(dir.bare)
=/ nubs sure.news
=/ norm know.hope.newf
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
:_ bare(ward (~(put by ward.bare) [nubs norm] (dare r)))
(dare r)
::
[%safe *]
=. ind.bare .+(ind.bare)
[[%risk %toss ~] bare]
::
[%risk *]
=. ind.bare .+(ind.bare)
[[%risk %toss ~] bare]
==
::
[%risk *]
=/ newf (pull +<.form hope.news)
?+ newf [[%boom ~] bare]
::
[%safe %know *]
=. dir.bare .+(dir.bare)
=/ nubs hope.news
=/ norm know.sure.newf
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
:_ bare(ward (~(put by ward.bare) [nubs norm] (dare r)))
(dare r)
::
[%risk %know *]
=. dir.bare .+(dir.bare)
=/ nubs hope.news
=/ norm know.hope.newf
=/ mem (~(get by ward.bare) [nubs norm])
?. ?=(~ mem) [u.mem bare]
=. ward.bare (~(put by ward.bare) [nubs norm] [%risk %toss ~])
=^ r bare $(subj nubs, form norm)
:_ bare(ward (~(put by ward.bare) [nubs norm] (dare r)))
(dare r)
::
[%safe *]
=. ind.bare .+(ind.bare)
[[%risk %toss ~] bare]
::
[%risk *]
=. ind.bare .+(ind.bare)
[[%risk %toss ~] bare]
==
==
::
[%10 [@ *] *]
=^ p bare $(form +<+.form)
=^ w bare $(form +>.form)
:_ bare
(welt +<-.form p w)
::
[%11 @ *]
$(form +>.form)
::
[%11 [* *] *]
=^ hint bare $(form +<+.form)
?+ hint [[%boom ~] bare]
::
[%safe *]
$(form +>.form)
::
[%risk *]
=^ r bare $(form +<.form)
:_ bare
(dare r)
==
::
[%12 *]
[[%risk %toss ~] bare]
==
--
++ cuff
|= =sock
=/ axe 1
|-
^- (list @)
?- sock
::
[%know *]
(limo [axe ~])
::
[%bets *]
(weld $(axe (add axe axe), sock hed.sock) $(axe (add (add axe axe) 1), sock tal.sock))
::
[%dice ~]
(limo [axe ~])
::
[%flip ~]
(limo [axe ~])
::
[%toss ~]
(limo [axe ~])
==
--
Reference in New Issue View Git Blame Copy Permalink