diff --git a/docs/spec/ska/lib/gen.hoon b/docs/spec/ska/lib/gen.hoon new file mode 100644 index 0000000..c8749f6 --- /dev/null +++ b/docs/spec/ska/lib/gen.hoon @@ -0,0 +1,773 @@ +/- *sock +/- *gene +/+ ska +=| prog=tabl +=| buff=lock +=| bust=(list [buff=lock]) +=| gab=gabl +=* this . +=< +|% +:: Write an instruction to the program buffer +++ inst + |= [=lick] + ^- _this + this(buff [lick buff]) +++ gibl + ^- [gabl _this] + [gab this(gab .+(gab))] +:: Finish writing a procedure +++ done + |= says=boot + ^- [boot _this] + :- says + this(prog (~(put by prog) bloc [(flop buff) says]), buff ~)] +:: Procrastinate on the current procedure, start +:: writing the one with a new label +++ proc + ^- _this + this(bust [buff bust], buff ~) +:: Done procrastinating, work on the procedure we +:: were doing +++ crop + ^- _this + ?< ?~ bust + this(buff buff.i.bust, bust t.bust) +:: Generate code for a formula +:: +:: TODO: add crash instruction %bom, generate whenever +:: returning [%boom ~] +++ gene + |= blos=labl + =| mod=mode + =/ bloc blos + |^ + ^- [boot _this] + ?- mod + :: + %save + ?+ for.bloc boom + :: + [[* *] *] + =. this (inst [%puh 1]) + =^ hed this $(for.bloc -.for.bloc) + =. this (inst [%put 0]) + =^ tal this $(for.bloc +.for.bloc) + =. this (inst [%cel 0]) + =. this (inst [%pop ~]) + [(cobb:ska hed tal) this] + :: + [%0 @] + ?: .= +.for.bloc 0 + bomb + =. (inst [%axe +.for.bloc]) + [(pull:ska +.for.bloc sub.bloc) this] + :: + [%1 *] + =. (inst [%con +.for.bloc]) + [[%safe %know +.for.bloc] this] + :: + [%2 * *] + =. this (inst [%puh 3]) + =. this (inst [%sav 1]) + =^ news this $(for.bloc +<.for.bloc, mod %step) + ?: ?= [%boom ~] news + boom + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + risk.news + == + =/ shis this + =. this (inst [%put 2]) + =. this (inst [%reo 1]) + =^ newf this $(for.bloc +>.for.bloc, mod %step) + =. this (inst [%reo 2]) + ?: ?= [%boom ~] newf + bomb + ?: ?= [%safe %know *] newf + =. this shis + =. this (inst [%sub ~]) + =/ nabl [nows know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nows know.hope.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + [(dare res) this] + =. this (inst [%lnk ~]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + [[%risk %gues ~] this] + :: + [%3 *] + =^ non this $(for.bloc +.for.bloc) + =. this (inst [%clq ~]) + [(ques:ska non) this] + :: + [%4 *] + =^ num this $(for.bloc +.for.bloc) + =. this (inst [%inc ~]) + [(pile:ska num) this] + :: + [%5 * *] + =. this (inst [%puh 1]) + =^ nox this $(for.bloc +<.for.bloc) + =. this (inst [%put 0]) + =^ noy this $(for.bloc +>.for.bloc) + =. this (inst [%eqq 0]) + =. this (inst [%pop ~]) + [(bopp nox noy) this] + :: + [%6 * * *] + =/ shis this + =^ tes this $(for.bloc +<.for.bloc) + ?: ?= [%boom ~] tes + boom + ?: ?= [%safe %know 0] tes + =. this shis + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%safe %know 1] tes + =. this shis + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?= [%risk %know 0] tes + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%risk %know 1] tes + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?| ?= [%safe %know *] tes + ?= [%safe %bets *] tes + ?= [%risk %know *] tes + ?= [%risk %bets *] tes + == + boom + =^ gib this gibl + =^ geb this gibl + =. this (inst [%br1 gib]) + =^ roo this $(for.bloc +>-.for.bloc) + =. this (inst [%bru geb]) + =. this (inst [%brh gib]) + =^ ral this $(for.bloc +>+.for.bloc) + =. this (inst [%brh geb]) + ?: ?= [%safe %flip ~] tes + [(gnaw roo ral) this] + [(dare (gnaw roo ral)) this] + :: + [%7 * *] + =. this (inst [%puh 1]) + =. this (inst [%sav 0]) + =^ news this $(for.bloc +<.for.bloc, mod %step) + ?: ?= [%boom ~] news + boom + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + hope.news + == + =. this (inst [%sub ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc nows, mod %step) + =. this (inst [%reo 0]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + :: + [%8 * *] + =. this (inst [%puh 1]) + =. this (inst [%sav 0]) + =^ newh this $(for.bloc +<.for.bloc, mod %step) + ?: ?= [%boom ~] newh + boom + =/ nowh + ?- newh + :: + [%safe *] + sure.newh + :: + [%risk *] + hope.newh + == + =. this (inst [%ext ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc (knit nows sub.bloc), mod %step) + =. this (inst [%reo 0]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] newh + [res this] + [(dare res) this] + :: + [%9 @ *] + =. this (inst [%puh 2]) + =. this (inst [%sav 1]) + =^ newc this $(for.bloc +>.for.bloc, mod %step) + ?: ?= newc [%boom ~] + boom + =/ nowc + ?- newc + :: + [%safe *] + sure.newc + :: + [%risk *] + hope.newc + == + =. this (inst [%sub ~]) + =/ newf (pull +<.for.bloc nowc) + ?: ?= [%boom ~] newf + boom + =/ shis this + =. this (inst [%axe +<.for.bloc]) + ?: ?= [%safe %know *] newf + =. this shis + =/ nabl [nowc know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] newc + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nowc know.hope.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + [(dare res) this] + =. this (inst [%lnk ~]) + =. this (inst [%reo 1]) + =. this (inst [%pop ~]) + [[%risk %gues ~] this] + :: + [%10 [@ *] *] + =. this (inst [%puh 2]) + =. this (inst [%sav 0]) + =^ wole this $(for.bloc +>.for.bloc, mod %step) + ?: ?= [%boom ~] wole + boom + =. this (inst [%put 1]) + =. this (inst [%reo 0]) + =^ pach this $(for.bloc +<+.for.bloc, mod %step) + ?: ?= [%boom ~] pach + boom + =. this (inst [%reo 1]) + =. this (inst [%edt +<-.for.bloc]) + =. this (inst [%reo 0]) + =. this (inst [%pop ~]) + [(welt axe pach wole) this] + :: + [%11 @ *] + $(for.bloc +>.for.bloc) + :: + [%11 [* *] *] + =/ shis this + =^ hnt this $(for.bloc +<+.for.bloc) + ?: ?= [%safe *] hnt + =. this shis + $(for.bloc +>.for.bloc) + $(for.bloc +>.for.bloc) + :: + [%12 * *] + =. this (inst [%puh 1]) + =^ ref this $(for.bloc +<.for.bloc) + ?: ?= [%boom ~] ref + boom + =. this (inst [%put 0]) + =^ pat this $(for.bloc +< + ?: ?= [%boom ~] pat + boom + =. this (inst [%cel 0]) + =. this (inst [%spy ~]) + [[%risk %gues ~] this] + == + :: + %step + ?+ for.bloc boom + :: + [[* *] *] + =. this (inst [%puh 1]) + =^ hed this $(for.bloc -.for.bloc, mod %save) + =. this (inst [%put 0]) + =^ tal this $(for.bloc +.for.bloc) + =. this (inst [%cel 0]) + =. this (inst [%pop ~]) + [(cobb:ska hed tal) this] + :: + [%0 @] + =. (inst [%axe +.for.bloc]) + [(pull:ska +.for.bloc sub.bloc) this] + :: + [%1 *] + =. (inst [%con +.for.bloc]) + [[%safe %know +.for.bloc] this] + :: + [%2 * *] + =. this (inst [%puh 2]) + =^ news this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] news + bomb + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + hope.news + == + =/ shis this + =. this (inst [%put 1]) + =^ newf this $(for.bloc +>.for.bloc) + =. this (inst [%reo 1]) + ?: ?= [%boom ~] newf + bomb + ?: ?= [%safe %know *] newf + =. this shis + =. this (inst [%sub ~]) + =/ nabl [nows know.sure.newf) + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nows know.hope.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%pop ~]) + [(dare res) this] + =. this (inst [%lnk ~]) + =. this (inst [%pop ~]) + [[%risk %gues ~] this] + :: + [%3 *] + =^ non this $(for.bloc +.for.bloc) + =. this (inst [%clq ~]) + [(ques:ska non) this] + :: + [%4 *] + =^ num this $(for.bloc +.for.bloc) + =. this (inst [%inc ~] + [(pile:ska num) this] + :: + [%5 * *] + =. this (inst [%puh 1]) + =^ nox this $(for.bloc +<.for.bloc, mod %save) + =. this (inst [%put 0]) + =^ noy this $(for.bloc +>.for.bloc) + =. this (inst [%eqq 0]) + =. this (inst [%pop ~]) + [(bopp nox noy) this] + :: + [%6 * * *] + =/ shis this + =^ tes this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] tes + boom + ?: ?= [%safe %know 0] tes + =. this shis + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%safe %know 1] tes + =. this shis + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?= [%risk %know 0] tes + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%risk %know 1] tes + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?| ?= [%safe %know *] tes + ?= [%safe %bets *] tes + ?= [%risk %know *] tes + ?= [%risk %bets *] tes + == + boom + =^ gib this gibl + =^ geb this gibl + =. this (inst [%br1 gib]) + =^ roo this $(for.bloc +>-.for.bloc) + =. this (inst [%bru geb]) + =. this (inst [%brh gib]) + =^ ral this $(for.bloc +>+.for.bloc) + =. this (inst [%brh geb]) + ?: ?= [%safe %flip ~] tes + [(gnaw roo ral) this] + [(dare (gnaw roo ral)) this] + :: + [%7 * *] + =^ news this $(for.bloc +<.for.bloc) + ?: ?= [%boom ~] news + boom + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + hope.news + == + =. this (inst [%sub ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc nows) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + :: + [%8 * *] + =^ newh this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] newh + boom + =/ nowh + ?- newh + :: + [%safe *] + sure.newh + :: + [%risk *] + hope.newh + == + =. this (inst [%ext ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc (knit nows sub.bloc)) + ?: ?= [%safe *] newh + [res this] + [(dare res) this] + :: + [%9 @ *] + =. this (inst [%puh 1]) + =^ newc this $(for.bloc +>.for.bloc) + ?: ?= [%boom ~] newc + boom + =/ nowc + ?- newc + :: + [%safe *] + sure.newc + :: + [%risk *] + hope.newc + == + =. this (inst [%sub ~]) + =/ newf (pull +<.for.bloc nowc) + ?: ?= [%boom ~] newf + boom + =/ shis this + =. this (inst [%axe +<.for.bloc]) + ?: ?= [%safe %know *] newf + =. this shis + =/ nabl [nowc know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%pop ~]) + ?: ?= [%safe *] newc + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nowc know.hope.newf] + =^ res this (fics nabl) + =. this (inst [%cal nabl]) + =. this (inst [%pop ~]) + [(dare res) this] + =. this (inst [%lnk ~]) + =. this (inst [%pop ~]) + [[%risk %gues ~] this] + :: + [%10 [@ *] *] + =. this (inst [%puh 1]) + =^ wole this $(for.bloc +>.for.bloc, mod %save) + ?: ?= [%boom ~] wole + boom + =. this (inst [%put 0]) + =^ pach this $(for.bloc +<+.for.bloc) + ?: ?= [%boom ~] pach + boom + =. this (inst [%reo 0]) + =. this (inst [%edt +<-.for.bloc]) + =. this (inst [%pop ~]) + [(welt axe pach wole) this] + :: + [%11 @ *] + $(for.bloc +>.for.bloc) + :: + [%11 [* *] *] + =/ shis this + =^ hnt this $(for.bloc +<+.for.bloc, mod %save) + ?: ?= [%safe *] hnt + =. this shis + $(for.bloc +>.for.bloc) + $(for.bloc +>.for.bloc) + :: + [%12 * *] + =. this (inst [%puh 1]) + =^ ref this $(for.bloc +<.for.bloc, mod %save) + =. this (inst [%put 0]) + =^ pat this $(for.bloc +>.for.bloc) + =. this (inst [%cel 0]) + =. this (inst [%pop ~]) + =. this (inst [%spy ~]) + [[%risk %gues ~] this] + == + :: + %butt + ?+ for.bloc boom + :: + [[* *] *] + =. this (inst [%puh 1]) + =^ hed this $(for.bloc -.for.bloc, mod %save) + =. this (inst [%put 0]) + =^ tal this $(for.bloc +.for.bloc, mod %step) + =. this (inst [%cel 0]) + =. this (inst [%pop ~]) + [(cobb:ska hed tal) this] + :: + [%0 @] + =. (inst [%axe +.for.bloc]) + [(pull:ska +.for.bloc sub.bloc) this] + :: + [%1 *] + =. (inst [%con +.for.bloc]) + [[%safe %know +.for.bloc] %this] + :: + [%2 * *] + =^ news this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] news + bomb + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + hope.news + == + =/ shis this + =. this (inst [%puh 1]) + =. this (inst [%put 0]) + =^ newf this $(for.bloc +>.for.bloc, mod %step) + =. this (inst [%cel 0]) + =. this (inst [%pop ~]) + =. this (inst [%noc ~]) + ?: ?= [%boom ~] newf + bomb + ?: ?= [%safe %know *] newf + =. this shis + =. this (inst [%sub ~]) + =/ nabl [nows know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%jmp nabl]) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nows know.hope.newf] + =^ res this (fics nabl) + =. this (inst [%jmp nabl]) + [(dare res) this] + =. this (inst [%lnt ~]) + [[%risk %gues ~] this] + :: + [%3 *] + =^ non this $(for.bloc +.for.bloc, mod %step) + =. this (inst [%clq ~]) + [(ques:ska non) this] + :: + [%4 *] + =^ num this $(for.bloc +.for.bloc, mod %step) + =. this (inst [%inc ~]) + [(pile:ska num) this] + :: + [%5 * *] + =. this (inst [%puh 1]) + =^ nox this $(for.bloc +<.for.bloc, mod %save) + =. this (inst [%put 0]) + =^ noy this $(for.bloc +>.for.bloc, mod %step) + =. this (inst [%eqq 0]) + =. this (inst [%pop ~]) + [(bopp nox noy) this] + :: + [%6 * * *] + =/ shis this + =^ tes this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] tes + bomb + ?: ?= [%safe %know 0] tes + =. this shis + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%safe %know 1] tes + =. this shis + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?= [%risk %know 0] tes + =^ res this $(for.bloc +>-.for.bloc) + [res this] + ?: ?= [%risk %know 1] tes + =^ res this $(for.bloc +>+.for.bloc) + [res this] + ?: ?| ?= [%safe %know *] tes + ?= [%safe %bets *] tes + ?= [%risk %know *] tes + ?= [%risk %bets *] tes + == + bomb + =^ gib this gibl + =. this (inst [%br1 gib]) + =^ roo this $(for.bloc +>-.for.bloc) + =. this (inst [%brh gib]) + =^ ral this $(for.bloc +>+.for.bloc) + ?: ?= [%safe %flip ~] tes + [(gnaw roo ral) this] + [(dare (gnaw roo ral)) this] + :: + [%7 * *] + =^ news this $(for.bloc +<.for.bloc, mod %step) + ?: ?= [%boom ~] news + boom + =/ nows + ?- news + :: + [%safe *] + sure.news + :: + [%risk *] + hope.news + == + =. this (inst [%sub ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc nows) + ?: ?= [%safe *] news + [res this] + [(dare res) this] + :: + [%8 * *] + =^ newh this $(for.bloc +<.for.bloc, mod %save) + ?: ?= [%boom ~] newh + boom + =/ nowh + ?- newh + :: + [%safe *] + sure.newh + :: + [%risk *] + hope.newh + == + =. this (inst [%ext ~]) + =^ res $(for.bloc +>.for.bloc, sub.bloc (knit nows sub.bloc)) + ?: ?= [%safe *] newh + [res this] + [(dare res) this] + :: + [%9 @ *] + =^ newc this $(for.bloc +>.for.bloc, mod %step) + ?: ?= [%boom ~] newc + bomb + =/ nowc + ?- newc + :: + [%safe *] + sure.newc + :: + [%risk *] + hope.newc + == + =. this (inst [%sub ~]) + =. newf (pull +<.for.bloc nowc) + ?: ?= [%boom ~] newf + bomb + =/ shis this + =. this (inst [%axe +<.for.bloc]) + ?: ?= [%safe %know *] newf + =. this shis + =/ nabl [nowc know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%jmp nabl]) + ?: ?= [%safe *] newc + [res this] + [(dare res) this] + ?: ?= [%risk %know *] newf + =/ nabl [nowc know.sure.newf] + =^ res this (fics nabl) + =. this (inst [%jmp nabl]) + [(dare res) this] + =. this (inst [%lnt ~]) + [[%risk %gues ~] this] + :: + [%10 [@ *] *] + =. this (inst [%puh 1]) + =^ wole this $(for.bloc +>.for.bloc, mod %save) + ?: ?= [%boom ~] wole + bomb + =. this (inst [%put 0]) + =^ pach this $(for.bloc +<+.for.bloc, mod %step) + ?: ?= [%boom ~] pach + bomb + =. this (inst [%reo 0]) + =. this (inst [%edt +<-.for.bloc]) + =. this (inst [%pop ~]) + [(welt axe pach wole) this] + :: + [%11 @ *] + $(for.bloc +>.for.bloc) + :: + [%11 [* *] *] + =/ shis this + =^ hnt this $(for.bloc +<+.for.bloc, mod %save) + ?: ?= [%safe *] hnt + =. this shis + $(for.bloc +>.for.bloc) + $(for.bloc +>.for.bloc) + :: + [%12 * *] + =. this (inst [%puh 1]) + :: TODO: finish 12 butt + + == + :: + %tail + ~| 'TODO: implement tail mode' !! + == + ++ done + |= says=boot + ^- [boot _this] + :- says + ?: ?= says [%boom ~] + this(prog (~(put by prog) blos [~[[%bom ~]] says]), buff ~) + this(prog (~(put by prog) blos [(flop buff) says]), buff ~) + ++ fics + |= cabl=labl + ^- [boot _this] + =/ vet (~(get by prog) cabl) + ?~ vet + =. this proc + =^ res this (^$ cabl) + =. this crop + [res this] + u.vet + ++ boom + ?: ?= mod %tail + (done [%boom ~]) + :- [%boom ~] + this(buff ~[[%bom ~]]) + -- +-- diff --git a/docs/spec/ska/lib/ska.hoon b/docs/spec/ska/lib/ska.hoon new file mode 100644 index 0000000..af3ea97 --- /dev/null +++ b/docs/spec/ska/lib/ska.hoon @@ -0,0 +1,566 @@ +/- *sock +|% +:: Get an axis from a sock +++ pull + |= [axe=@ =sock] + ^- boot + ?: .= axe 0 + [%boom ~] + |- + ?: (= axe 1) + [%safe sock] + ?- sock + :: + [%know @] + [%boom ~] + :: + [%know * *] + ?- (cap axe) + :: + %2 + $(axe (mas axe), sock [%know -.know.sock]) + %3 + $(axe (mas axe), sock [%know +.know.sock]) + == + :: + [%bets * *] + ?- (cap axe) + :: + %2 + $(axe (mas axe), sock hed.sock) + :: + %3 + $(axe (mas axe), sock tal.sock) + == + :: + [%dice ~] + [%boom ~] + :: + [%flip ~] + [%boom ~] + :: + [%gues ~] + [%risk %gues ~] + == +:: 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] + :: + [%gues ~] + [%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 ~] a + [%boom ~] + ?: ?= [%boom ~] b + [%boom ~] + ?- a + :: + [%safe *] + ?- b + :: + [%safe *] + [%safe (knit sure.a sure.b)] + :: + [%risk *] + [%risk (knit sure.a hope.b)] + == + :: + [%risk *] + ?- b + :: + [%safe *] + [%risk (knit hope.a sure.b)] + :: + [%risk *] + [%risk (knit hope.a hope.b)] + == + == +:: 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]) + :: + [%gues ~] + (cobb $(axe (mas axe)) [%risk %gues ~]) + == + :: + %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)) + :: + [%gues ~] + (cobb [%risk %gues ~] $(axe (mas axe))) + == + == +:: Stitch a boot into another boot +++ welt + |= [axe=@ pach=boot wole=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 a), b (fray b)) + ?: ?= [%know *] a + $(a (fray a)) + ?: ?= [%know *] b + $(b (fray 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 ~] + [%gues ~] +:: 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 + ?- 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 %gues ~] + [%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 %gues ~] + [%risk %flip ~] + == +++ pile + |= tom=boot + ^- boot + ?+ tom [%boom ~] + :: + [%safe %know @] + [%safe %dice ~] + :: + [%safe %dice ~] + [%safe %dice ~] + :: + [%safe %flip ~] + [%safe %dice ~] + :: + [%safe %gues ~] + [%risk %dice ~] + :: + [%risk %know @] + [%risk %dice ~] + :: + [%risk %dice ~] + [%risk %dice ~] + :: + [%risk %flip ~] + [%risk %dice ~] + :: + [%risk %gues ~] + [%risk %dice ~] + == +:: Produce knowledge of the result given knowledge of the subject +++ wash + |= [subj=sock form=*] + ^- boot + =+ ward=(map [sock *] boot) + ?+ form [%boom ~] + :: + [[* *] *] + (cobb $(form -.form) $(form +.form)) + :: + [%0 @] + (pull +.form subj) + :: + [%1 *] + [%safe %know +.form] + :: + [%2 * *] + =/ subn $(form +<.form) + =/ forn $(form +>.form) + ?: ?= [%safe %dice ~] forn + [%boom ~] + ?: ?= [%safe %flip ~] forn + [%boom ~] + ?: ?= [%risk %dice ~] forn + [%boom ~] + ?: ?= [%risk %flip ~] forn + [%boom ~] + ?+ forn [%risk %gues ~] + :: + [%safe %know *] + ?- subn + :: + [%safe *] + $(subj sure.subn, form know.sure.forn) + :: + [%risk *] + (risk $(subj risk.subn, form know.sure.forn)) + == + :: + [%risk %know *] + ?- subn + :: + [%safe *] + (risk $(subj sure.subn, form know.hope.forn)) + :: + [%risk *] + (risk $(subj hope.subn, form know.hope.forn)) + == + == + :: + [%3 *] + (ques $(form +.form)) + :: + [%4 *] + (pile $(form +.form)) + :: + [%5 * *] + (bopp $(form +<.form) $(form +>.form)) + :: + [%6 * * *] + =/ cond $(form +<.form) + ?+ cond [%boom ~] + :: + [%safe *] + ?+ sure.cond [%boom ~] + :: + [%know 0] + $(form +>-.form) + :: + [%know 1] + $(form +>+.form) + :: + [%flip ~] + (gnaw $(form +>-.form) $(form +>+.form)) + :: + [%dice ~] + (dare (gnaw $(form +>-.form) $(form +>+.form))) + :: + [%gues ~] + (dare (gnaw $(form +>-.form) $(form +>+.form))) + == + :: + [%risk *] + ?+ hope.cond [%boom ~] + :: + [%know 0] + (dare $(form +>-.form)) + :: + [%know 1] + (dare $(form +>+.form)) + :: + [%flip ~] + (dare (gnaw $(form +>-.form) $(form +>+.form))) + :: + [%dice ~] + (dare (gnaw $(form +>-.form) $(form +>+.form))) + :: + [%gues ~] + (dare (gnaw $(form +>-.form) $(form +>+.form))) + == + == + :: + [%7 * *] + =/ news $(form +<.form) + ?+ news [%boom ~] + :: + [%safe *] + $(subj sure.news, form +>.form) + :: + [%risk *] + (dare $(subj hope.news, form +>.form)) + == + :: + [%8 * *] + =/ news $(form +<.form) + ?+ news [%boom ~] + :: + [%safe *] + $(subj [sure.news subj], form +>.form) + :: + [%risk *] + $(dare $(subj [hope.news subj], form +>.form)) + == + :: + [%9 @ *] + =/ news $(form +>.form) + ?+ news [%boom ~] + :: + [%safe *] + =/ newf (axe +<.form news) + ?+ newf [%boom ~] + :: + [%safe %know *] + $(subj sure.news, form know.sure.newf) + :: + [%risk %know *) + (dare $(subj sure.news, form know.hope.newf)) + :: + [%safe *] + [%risk %gues ~] + :: + [%risk *] + [%risk %gues ~] + == + :: + [%risk *] + =/ newf (axe +<.form news) + ?+ newf [%boom ~] + :: + [%safe %know *] + (dare $(subj hope.news, form know.sure.newf)) + :: + [%risk %know *] + (dare %(subj hope.news, form know.hope.newf)) + :: + [%safe *] + [%risk %gues ~] + :: + [%risk *] + [%risk %gues ~] + == + == + :: + [%10 [@ *] *] + (welt $(form +>.form) $(form ->.form)) + :: + [%11 @ *] + $(form +>.form) + :: + [%11 [* *] *] + =/ hint $(form +<+.form) + ?+ hint [%boom ~] + :: + [%safe *] + $(form +>.form) + :: + [%risk *] + (dare $(form +>.form)) + == + :: + [%12 *] + [%risk %gues ~] + == + ++ 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 ~]) + :: + [%gues ~] + (limo [axe ~]) + == +-- diff --git a/docs/spec/ska/sur/gene.hoon b/docs/spec/ska/sur/gene.hoon new file mode 100644 index 0000000..a2dac36 --- /dev/null +++ b/docs/spec/ska/sur/gene.hoon @@ -0,0 +1,43 @@ +/- *sock +|% ++$ mode + $? %save :: Must not clobber subject, non-tail + %step :: May clobber subject, non-tail + %butt :: Tail, but do not write to table when done + %tail :: Tail, write to table when done + == ++$ labl [sub=sock for=*] ++$ gabl @ ++$ lick + $% [%con *] :: constant + [%axe @] :: axis + [%cel @] :: Cell [slot result] + [%clq ~] :: Test if result is cell + [%inc ~] :: Increment result + [%eqq @] :: Test if slot is equal to result + [%br1 gabl] :: Jump to generated label if result is 1 + [%bru gabl] :: Jump to generated label unconditionally + [%brh gabl] :: Generated label + [%sub ~] :: Set subject to result + [%ext ~] :: Cons result onto subject + [%dxt ~] :: Set subject to tail of subject (restore after ext) + [%noc ~] :: Split cell in result register to subject and result + [%lnk ~] :: Call code, save PC in slot 0 + [%cal labl] :: Call label, save PC in slot 0 + [%lnt ~] :: Tail-call code + [%jmp labl] :: Jump to label + [%edt @] :: Edit result into axis in subject + [%spy ~] :: Slam peek gate + [%puh @] :: Push frame with given number of slots + [%pop ~] :: Pop frame + [%put @] :: Save result register to slot + [%get @] :: Restore result register from slot + [%sav @] :: Save subject register to slot + [%reo @] :: Restore subject register from slot + [%don ~] :: Return from procedure + [%bom ~] :: Crash + == ++$ lock (list lick) ++$ link [does=lock says=boot] ++$ tabl (map labl link) +-- diff --git a/docs/spec/ska/sur/sock.hoon b/docs/spec/ska/sur/sock.hoon new file mode 100644 index 0000000..f90c2b0 --- /dev/null +++ b/docs/spec/ska/sur/sock.hoon @@ -0,0 +1,16 @@ +|% ++$ sock + $% [%know know=*] + [%bets hed=sock tal=sock] + [%dice ~] + [%flip ~] + [%gues ~] + == ++$ stok + $: sock * ++$ boot + $? [%safe sure=sock] + [%risk hope=sock] + [%boom ~] + == +--