diff --git a/docs/spec/ska/lib/degen.hoon b/docs/spec/ska/lib/degen.hoon index 30adcdb..fe80301 100644 --- a/docs/spec/ska/lib/degen.hoon +++ b/docs/spec/ska/lib/degen.hoon @@ -1,405 +1,416 @@ -:: TODO: generate labels and jumps everywhere and stick them in the code -:: table immediately, then linearize -/- *gene -/- *sock /+ ska -=| prog=tinn -=| buff=linn -=| bust=(list linn) +/- *sock +/- *gene |% -++ this . -++ inst - |= =dinn - ^- _this - this(buff [dinn buff]) -++ sift - ^- _this - (inst [%mov 2 5]) -++ suft - ^- _this - (inst [%mov 11 5]) -++ gene - |= bloc=labl - ^- [boot _this] - =/ puff (~(get by prog) bloc) - ?. ?=(~ puff) - [says.u.puff this] - =. prog (~(put by prog) bloc [~ [%risk %gues ~]]) :: prevent recursive functions from infinite looping the compiler - =. bust [buff bust] - =. buff ~ - =+ faxe=1 - =+ fate=for.bloc - =+ ject=sub.bloc - =| heir=cost - =| vale=dast +++ plot + =| ski=farm + |= ent=barn + ^- [boot farm] + =/ ext (~(get by ski) ent) + ?. ?=(~ ext) [says.u.ext ski] + =; [res sku] [says.res sku(yard (~(put by yard.sku) ent res), wood [ent wood.sku]] + =. ski ski(yard (~(put by yard.ski) ent [[%zer 0 %.n] [%risk %toss ~]])) :: blackhole, guard recursion + |- + ^- [[does=nomm says=boot:ska] farm] =< - =^ moot this - |- - ^- [boot _this] - ?. (hast vale) - ~| 'vale must not be 5 or a subaxis of 5' !! - ?+ fate bomb - [[* *] *] - ?: ?= [%bab *] heir - bomb - =/ tier [%dab (bear 3)] - =^ shed this $(faxe (peg faxe 2), fate -.fate, heir tier, vale 4) :: we can't clobber subject - =. this sift - =^ stal this $(faxe (peg faxe 3), fate +.fate, heir [%dab here], vale (peg vale 3)) - =. this (inst [%mov 10 (peg vale 2)]) - =. this suft - =. this tale - :_ this - (cobb:ska shed stal) - :: - [%0 @] - ?: =(0 +.fate) - bomb - =. this (inst [%mov (peg 3 +.fate) vale]) - =. this bale - :_ this - (pull:ska +.fate ject) - :: - [%1 *] - =. this (inst [%imm +.fate vale]) - ?: ?= [%bab *] heir - ?: =(0 +.fate) - =. this (inst [%hop troo.heir]) - =. this tale - :_ this - [%safe %know +.fate] - ?: =(1 +.fate) - =. this (inst [%hop fals.heir]) - =. this tale - :_ this - [%safe %know +.fate] - bomb - =. this tale - :_ this - [%safe %know +.fate] - :: - [%2 * *] - =/ shis this - =/ tier [%dab (bear 7)] - =. this hide - =^ norm this $(faxe (peg faxe 6), fate +<.fate, heir tier, vale 4) - ?: ?= [%boom ~] norm - bomb - =? this ?=([%safe %know *] norm) =.(this shis hide) - =^ news this $(faxe (peg faxe 7), fate +>.fate, heir [%dab here], vale 3) - ?: ?= [%boom ~] news - bomb - =/ sewn - ?- news - [%safe *] sure.news - [%risk *] hope.news - == - ?: ?=([$?(%safe %risk) %know *] norm) - =/ sabl - ?- norm - [%safe *] [sewn know.sure.norm] - [%risk *] [sewn know.hope.norm] - == - =^ toot this ^$(bloc sabl) - ?: ?=([%ret ~] heir) - ?. =(vale 4) - ~| 'Value destination for tail call should always be 4' !! - =. this (inst [%jmp sabl]) - :_ this - ?: ?& ?=([%safe *] news) ?=([%safe *] norm) == - toot - (dare:ska toot) - =. this (inst [%cal sabl]) - =. this show - =. this (inst [%mov 4 vale]) - =. this bran - :_ this - ?: ?& ?=([%safe *] news) ?=([%safe *] norm) == - toot - (dare:ska toot) - ?: ?=([%ret ~] heir) - ?. =(vale 4) - ~| 'Value destination for tail call should always be 4' !! - =. this (inst [%lnt ~]) - :_ this - [%risk %gues ~] - =. this (inst [%lnk ~]) - =. this show - =. this (inst [%mov 4 vale]) - =. this bran - :_ this - [%risk %gues ~] - :: - [%3 *] - :: TODO: statically jump to a branch if we know atom or cell - =^ spec this $(faxe (peg 3 faxe), fate +.fate, heir [%dab here], vale 4) - =. this (inst [%clq will wont]) - =. this does - =. this dont - :_ this - (ques:ska spec) - :: - [%4 *] - =^ mota this $(faxe (peg 3 faxe), fate +.fate, heir [%dab here]) :: leave vale the same - =. this (inst [%inc vale]) - =. this bale - :_ this - (pile:ska mota) - :: - [%5 * *] - :: TODO: statically jump to a branch if we know equal or - :: disequal - =/ tier (bear 7) - =^ left this $(faxe (peg 6 faxe), fate +<.fate, heir [%dab tier], vale 4) - =. this sift - =^ rite this $(faxe (peg 7 faxe), fate +>.fate, heir [%dab here], vale 9) - =. this (inst [%mov 10 8]) - =. this suft - =. this (inst [%eqq will wont]) - =. this does - =. this dont - :_ this - (bopp:ska left rite) - :: - [%6 * * *] - =/ troo (bear 14) - =/ fals (bear 15) - =/ shis this - =^ cond this $(faxe (peg 6 faxe), fate +<.fate, heir [%bab troo fals], vale 4) - ?: ?= [%safe %know *] cond - ?: =(0 know.sure.cond) - =. this shis - $(faxe (peg 14 faxe), fate +>-.fate) :: pass on heir and vale - ?: =(1 know.sure.cond) - =. this shis - $(faxe (peg 15 faxe), fate +>+.fate) :: pass on heir and vale - bomb - ?: ?= [%risk %know *] cond - ?: =(0 know.hope.cond) - =. this (inst [%her troo]) - =^ trus this $(faxe (peg 14 faxe), fate +>-.fate) :: pass on heir and vale - :_ this - (dare:ska trus) - ?: =(1 know.hope.cond) - =. this (inst [%her fals]) - =^ lies this $(faxe (peg 15 faxe), fate +>+.fate) - :_ this - (dare:ska lies) - bomb - ?: ?= [%safe %bets *] cond - bomb - ?: ?= [%risk %bets *] cond - bomb - =. this (inst [%her troo]) - =^ trus this $(faxe (peg 14 faxe), fate +>-.fate) :: pass on heir and vale - =. this (inst [%her fals]) - =^ lies this $(faxe (peg 15 faxe), fate +>+.fate) :: pass on heir and vale - :_ this - ?: ?= [%safe %flip ~] cond - (gnaw:ska trus lies) - (dare:ska (gnaw:ska trus lies)) - :: - [%7 * *] - =. this hide - =^ news this $(faxe (peg 6 faxe), fate +<.fate, heir [%dab (bear 7)], vale 3) :: put result in subject - ?: ?= [%boom ~] news - bomb - =/ sewn - ?- news - [%safe *] sure.news - [%risk *] hope.news - == - ?: ?= [%ret ~] heir - =^ soot this $(faxe (peg 7 faxe), fate +>.fate, ject sewn) - :_ this - ?: ?= [%safe *] news - soot - (dare:ska soot) - :: this is what we must do for now to make sure the subject is - :: cleaned up in a test expression. - :: TODO: some way to inject the cleanup code at the start of - :: the branches so we can still branch directly - =^ soot this $(faxe (peg 7 faxe), fate +>.fate, heir [%dab here], vale 4, ject sewn) - =. this show - =. this (inst [%mov 4 vale]) - =. this bran - :_ this - ?: ?= [%safe *] news - soot - (dare:ska soot) - :: - [%8 * *] - =^ news this $(faxe (peg 6 faxe), fate +<.fate, heir [%dab (bear 7)], vale 8) :: store in head of result - ?: ?= [%boom ~] news - bomb - =/ sewn - ?- news - [%safe *] sure.news - [%risk *] hope.news - == - =/ newp (knit:ska sewn ject) - =. this (inst [%mov 3 9]) :: copy subject to tail of result - =. this (inst [%mov 4 3]) :: copy cell back to subject - ?: ?= [%ret ~] heir - =^ hoot this $(faxe (peg 7 faxe), fate +>.fate, ject newp) - :_ this - ?: ?= [%safe *] news - hoot - (dare:ska hoot) - =^ hoot this $(faxe (peg 7 faxe), fate +>.fate, ject newp, heir [%dab here], vale 4) - =. this (inst [%mov 7 3]) :: put the subject back - =. this (inst [%mov 4 vale]) :: put the result in the right place - :_ this - ?: ?= [%safe *] news - hoot - (dare:ska hoot) + ?+ for.ent bomb + [[* *] *] + =^ [doth sath] ski $(for.ent -.for.ent) + ?: ?=([%boom ~] sath) bomb + =^ [toes tays] ski $(for.ent +.for.ent) + ?: ?=([%boom ~] tays) bomb + :_ ski + :_ (cobb:ska sath tays) + [%par doth sath] + :: + [%0 @] + :: we can decompose the axis into two axes, a safe axis which can + :: be implemented unchecked, and an unsafe axis which must be + :: checked. We then compose these two axes into safe %zer and + :: unsafe %zer composed by %sev + =/ [saf rik ken] (punt:ska +.for.ent sub.ent) + ?: =(0 saf) bomb + ?: =(1 rik) [[%zer saf %.y] [%safe ken]] + ?: =(1 saf) [[%zer rik %.n] [%risk ken]] + :_ ski + :_ [%risk ken] + [%sev [%zer saf %.y] [%zer rik %.n]] + :: + [%1 *] + :_ ski + :_ [%safe %know +.for.ent] + [%one +.for.ent] + :: + [%2 * *] + =^ [dost sass] ski $(for.ent +<.for.ent) + ?: ?=([%boom ~] sass) bomb + =^ [doff faff] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] faff) bomb + =/ skun + ?- sass + [%safe *] sure.sass + [%risk *] hope.sass + == + ?: ?=([%safe %know *] faff) + =^ ret ski ^$(ent [skun know.sure.faff]) + :_ ski + :_ ?: ?=([%safe *] sass) ret (dare:ska ret) + [%two dost doff skun (some know.sure.faff) %.y] + ?: ?=([%risk %know *] faff) + =^ ret ski ^$(ent [skun know.hope.faff]) + :_ ski + :_ (dare:ska ret) + [%two dost doff skun (some know.hope.faff) %.n] + :_ ski + :_ [%risk %toss ~] + [%two dost doff skun ~ %.n] + :: + [%3 *] + =^ [deft koob] ski $(for.ent +.for.ent) + ?: ?=([%boom ~] koob) bomb + :_ ski + :_ (ques:ska koob) + [%thr deft] + :: + [%4 *] + =^ [dink sink] ski $(for.ent +.for.ent) + ?: ?=([%boom ~] sink) bomb + =/ rink + ?- sink + [%safe *] sure.sink + [%risk *] hope.sink + == + :_ ski + :_ (pile:ska sink) + [%fou dink ?|(?=([%dice ~] rink) ?=([%flip ~] rink) ?=([%know @] rink))] + :: + [%5 * *] + =^ [dome foam] ski $(for.ent +<.for.ent) + ?: ?=([%boom ~] foam) bomb + =^ [doot foot] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] foot) bomb + :_ ski + :_ (bopp:ska foam foot) + [%fiv dome doot] + :: + [%6 * * *] + =^ [dawn sond] ski $(for.ent +<.for.ent) + ?: ?=([%safe %know %0] sond) $(for.ent +>-.for.ent) + ?: ?=([%safe %know %1] sond) $(for.ent +>+.for.ent) + ?: ?=([%safe %know *] sond) bomb + ?: ?=([%safe %bets *] sond) bomb + ?: ?=([%safe %flip ~] sond) + =^ [drew slew] ski $(for.ent +>-.for.ent) + =^ [darn song] ski $(for.ent +>+.for.ent) + :_ ski + :_ (gnaw:ska slew song) + [%six dawn slew song] + ?: ?=([%risk %know %0] sond) + =^ [drew slew] ski $(for.ent +>-.for.ent) + :_ ski + :_ (dare:ska slew) + [%sev [dawn drew] [%zer 3 %.y]] + ?: ?=([%risk %know %1] sond) + =^ [darn song] ski $(for.ent +>+.for.ent) + :_ ski + :_ (dare:ska song) + [%sev [dawn darn] [%zer 3 %.y]] + ?: ?=([%risk %know *] sond) bomb + ?: ?=([%risk %bets *] sond) bomb + =^ [drew slew] ski $(for.ent +>-.for.ent) + =^ [darn song] ski $(for.ent +>+.for.ent) + :_ ski + :_ (dare:ska (gnaw:ska slew song)) + [%six dawn drew darn] + :: + [%7 * *] + =^ [deck keck] ski $(for.ent +<.for.ent) + ?: ?=([%boom ~] keck) bomb + =/ news + ?- keck + [%safe *] sure.keck + [%risk *] hope.keck + == + =^ [dest zest] ski $(sub.ent news, for.ent +>.for.ent) + ?: ?=([%boom ~] zest) bomb + :_ ski + :_ ?: ?=([%safe *] keck) zest (dare:ska zest) + [%sev deck dest] + :: + [%8 * *] + =^ [pink pest] ski $(for.ent +<.for.ent) + ?: ?=([%boom ~] pest) bomb + =/ nest + ?- pest + [%safe *] sure.pest + [%risk *] hope.pest + == + =^ [dest zest] ski $(sub.ent (knit nest sub.ent), for.ent +>.for.ent) + ?: ?=([%boom ~] zest) bomb + :_ ski + :_ ?: ?=([%safe *] pest) zest) (dare:ska zest) + [%eig pink dest] :: [%9 @ *] - =. this hide - =^ bore this $(faxe (peg 7 faxe), fate +>.fate, heir [%dab (bear 6)], vale 3) - ?: ?= [%boom ~] bore - bomb - =/ sore - ?- bore - [%safe *] sure.bore - [%risk *] hope.bore + =^ [lore sore] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] sore) bomb + =/ news + ?- sore + [%safe *] sure.sore + [%risk *] hope.sore == - =/ norm (pull:ska +<.fate sore) - ?: ?= [%boom ~] norm - bomb - =? this ?!(?=([%safe %know *] norm)) (inst [%mov (peg 3 +<.fate) 4]) :: look up axis - ?: ?=([$?(%safe %risk) %know *] norm) - =/ sabl - ?- norm - [%safe %know *] [sore know.sure.norm] - [%risk %know *] [sore know.hope.norm] - == - =^ noot this ^$(bloc sabl) - ?: ?= [%ret ~] heir - =. this (inst [%jmp sabl]) - :_ this - ?: ?&(?=([%safe *] bore) ?=([%safe *] norm)) - noot - (dare:ska noot) - =. this (inst [%cal sabl]) - =. this show - =. this (inst [%mov 4 vale]) - =. this bran - :_ this - ?: ?&(?=([%safe *] bore) ?=([%safe *] norm)) - noot - (dare:ska noot) - ?: ?= [%ret ~] heir - =. this (inst [%lnt ~]) - :_ this - [%risk %gues ~] - =. this (inst [%lnk ~]) - =. this show - =. this (inst [%mov 4 vale]) - =. this bran - :_ this - [%risk %gues ~] - :: - [%10 [@ *] *] - =^ soot this $(faxe (peg 13 faxe), fate +<+.fate, heir [%dab (bear 7)], vale 4) - =. this sift - =^ toot this $(faxe (peg 7 faxe), fate +>.fate, heir [%dab here]) :: write tree to destination - =. this (inst [%mov 10 (peg vale +<-.fate)]) :: write patch to axis under destination - =. this suft - :_ this - (welt:ska +<-.fate soot toot) - :: - [%11 @ *] - $(faxe (peg 7 faxe), fate +>.fate) - :: - [%11 [@ *] *] - =^ hoot this $(faxe (peg 13 faxe), fate +<+.fate, heir [%dab (bear 7)], vale 4) - ?: ?= [%boom ~] hoot - bomb - =^ root this $(faxe (peg 7 faxe), fate +>.fate) - :_ this - ?: ?= [%safe *] hoot - root - (dare:ska root) - :: - [%12 * *] - =^ root this $(faxe (peg 6 faxe), fate +<.fate, heir [%dab (bear 7)], vale 8) - ?: ?= [%boom ~] root - bomb - =^ soot this $(faxe (peg 7 faxe), fate +>.fate, heir [%dab here], vale 9) - ?: ?= [%boom ~] soot - bomb - =. this (inst [%spy ~]) - =. this (inst [%mov 4 vale]) - :_ this - [%risk %gues ~] - == - :_ this(prog (~(put by prog) bloc [(flop buff) moot]), buff -.bust, bust +.bust) - moot + =/ fork (pull:ska +<.for.ent news) + ?: ?=([%safe %know *] fork) + =^ ret ski ^$(ent [news know.sure.fork]) + :_ ski + :_ ?: ?=([%safe *] sass) ret (dare:ska ret) + [%nin +<.for.ent lore news (some know.sure.fork) %.y] + ?: ?=([%risk %know *] fork) + =^ ret ski ^$(ent [news know.hope.fork]) + :_ ski + :_ (dare:ska ret) + [%nin +<.for.ent lore news (some know.hope.fork) %.n] + :_ ski + :_ [%risk %toss ~] + [%nin +<.for.ent lore news ~ ?=([%safe *] fork)] + :: + [%10 [@ *] *] + =^ [neat seat] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] seat) bomb + =^ [pace spat] ski $(for.ent +<+.for.ent) + ?: ?=([%boom ~] spat) bomb + =/ teak + ?- seat + [%safe *] sure.seat + [%risk *] hope.seat + == + =/ [saf rik ken] (punt +<-.for.ent teak) + ?: =(0 saf) bomb + ?: =(1 rik) + :_ [(welt +<-.for.ent spat seat) ski] + :_ [%ten [+<-.for.ent pace] neat %.y] + :_ [(welt +<-.for.ent spat seat) ski] + :_ [%sev [neat pace] %ten [saf %ten [rik %zer 3 %.n] [%zer (peg 2 saf) %.y] %.y] [%zer 2 %.y] %.y] + :: + [%11 @ *] + =^ [real seal] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] seal) bomb + :_ [seal ski] + :_ [%els +<.for.ent real] + :: + [%11 [@ *] *] + =^ [fake sake] ski $(for.ent +<+.for.ent) + ?: ?=([%boom ~] sake) bomb + =^ [real seal] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] seal) bomb + :_ ski + ?: ?=([%safe *] sake) + [[%eld [+<-.for.ent fake] real %.y] seal] + [[%eld [+<-.for.ent fake] real %.n] seal] + :: + [%12 * *] + =^ [fear sear] ski $(for.ent +<.for.ent) + ?: ?=([%boom ~] sear) bomb + =^ [pack sack] ski $(for.ent +>.for.ent) + ?: ?=([%boom ~] sack) bomb + :_ [[%risk %toss ~] ski] + [%twe fear pack] + == |% - ++ bomb - ^- [boot _this] - =. this (inst [%bom ~]) - :_ this - [%boom ~] - ++ bear - |= weir=@ - ^- dabl - [sub.bloc for.bloc (peg faxe weir) 0] - ++ here - ^- dabl - [sub.bloc for.bloc faxe 1] - ++ will - ^- dabl - [sub.bloc for.bloc faxe 2] - ++ wont - ^- dabl - [sub.bloc for.bloc faxe 3] - :: hide away a subject for later (clobbers 4) - ++ hide - =. this (inst [%mov 5 11]) - (inst [%mov 3 10]) :: subject is now in 10 - :: put back a subject that was hidden away (does not clobber 4) - ++ show - =. this (inst [%mov 10 3]) :: put back the subject - suft :: put the result where it will get shifted back into result space - ++ bran - ?: ?= [%bab *] heir - (inst [%brn troo.heir fals.heir]) - this - ++ tale - ?: ?= [%ret ~] heir - ?. =(4 vale) - ~| 'Value destination for tail call should always be 4' !! - (inst [%don ~]) - this - ++ bale - =. this bran - tale - ++ does - =. this (inst [%her will]) - =. this (inst [%imm 0 vale]) - ?- heir - [%dab *] (inst [%hop wher.heir]) - [%bab *] (inst [%hop troo.heir]) - [%ret ~] (inst [%don ~]) - == - ++ dont - =. this (inst [%her wont]) - =. this (inst [%imm 1 vale]) - ?- heir - [%dab *] (inst [%hop wher.heir]) - [%bab *] (inst [%hop fals.heir]) - [%ret ~] (inst [%don ~]) - == + ++ bomb [[%zer 0 %.n] [%boom ~] ski] -- -:: assert correctness of a dast: must not be 5 or a subaxis of 5 -++ hast - |= wast=dast - ^- ? - ?. (lth wast 5) - ?. =(wast 5) - $(wast (rsh [0 1] wast)) - %.n - %.y +++ till + =| burg=town + |= =farm + ^- town + =/ work (flop (skip wood.farm ~(has in ~(key by burg)))) + =< burg + |- + ^- _this + ?: =(~ work) this + =^ next work work + =+ ~| %next-miss (~(got by yard.farm) next) + :: now we have the nock-- in does + =/ dock [lamb=lamb.burg lake=*lake] + =| flow=line + =/ axle=@ 1 + =/ fawn=does + =+ + =< + |- + ^- [[hat=sans her=berm] dock] + ?- fawn + [%par * *] + =^ [one two her] dock twin + =^ [bat bit] dock $(fawn +>.fawn, axle (peg axle 3), flow [%dab her two]) + =^ [hat hit] dock $(fawn +<.fawn, axle (peg axle 2), flow [%dab bit one]) + (copy hat bat hit) + :: + [%zer *] + ?- flow + [%moat *] + =/ slow (take +<.fawn what.flow +>.fawn) + ?~ slow + =^ hole dock bomb + :_ dock + [[%disc ~] hole] + :_ dock + [u.slow wher.flow] + :: + [%one *] + (bang +.fawn) + :: + [%two *] + ~| %todo !! + :: + == + |% + ++ bang + |= non=* + ^- [[hat=plow her=berm] _dock] + ?- flow + [%pond ~] + =^ ret dock wean + =^ her dock (mend %rime ~[[%imm +.fawn ret]] [%don ret]) + :_ dock + [[%disc ~] her] + :: + [%rift *] + ?: =(0 +.fawn) [[[%disc ~] troo.flow] dock] + ?: =(1 +.fawn) [[[%disc ~] fals.flow] dock] + =^ hole dock bomb :: XX maybe we should assert that SKA should have caught this? + :_ dock + [[%disc ~] hole] + :: + [%moat *] + =/ what what.flow + =/ mitt + |- + ^- (unit (list bran)) + ?- what + [%disc ~] + (some ~) + :: + [%tine @] + (some ~[[%imm non +.what]]) + :: + [%fork *] + ?@ non + ?: safe.what + ~| %safe-axis-atom !! + ~ + (clap $(what left.what, non -.non) $(what rite.what, non +.non) weld) + == + ?~ mitt + =^ hole dock bomb + :_ dock + [[%disc ~] hole] + =^ rock dock (mend %toil u.mitt [%hop wher.flow]) + :_ dock + [[%disc ~] rock] + == + ++ take :: axis + |= [sax=@ tow=plow row=?] :: axis, destination, safety + ^- plow :: nullary case = crash + ?: =(0 sax) ~ + %- some + |- + ?: =(1 sax) tow + ?- (cap sax) + %2 [%fork $(sax (mas sax)) [%disc ~] row] + %3 [%fork [%disc ~] $(sax (mas sax)) row] + == + ++ milk :: local label + |= gen=@ + ^- berm + [sub.does for.does axle gen] + ++ wean :: fresh ssa + ^- [@ _dock] + [lamb.dock dock(lamb .+(lamb.dock))] + ++ copy :: replicate values to two destinations + |= [hat=plow bat=plow her=berm] + ^- [[hat=plow her=berm] _dock] + =^ [tog moot] dock + |- + ^- [[tog=plow moot=(list tins)] _dock] + ?: ?=([%disc ~] hat) [[bat ~] dock] + ?: ?=([%disc ~] bat) [[hat ~] dock] + ?- hat + [%tine @] + ?- bat + [%tine @] + ?: =(+.hat +.bat) + [[hat ~] dock] + [[hat ~[[%mov +.hat +.bat]]] dock] + :: + [%fork *] + =^ one dock wean + =^ two dock wean + =^ [hog hoot] dock $(hat [%tine one], bat hed.bat) + =^ [log loot] dock $(hat [%tine two], bat tal.bat) + [[[%fork hog log safe.bat] [[%con one two +.hat] (weld hoot loot)]] dock] + == + :: + [%fork *] + ?- bat + [%tine @] + =^ one dock wean + =^ two dock wean + =^ [hog hoot] dock $(hat hed.hat, bat [%ssa one]) + =^ [log loot] dock $(hat tal.hat, bat [%ssa two]) + [[[%fork hog log safe.hat] [[%con one two +.bat] (weld hoot loot)]] dock] + :: + [%fork *] + =^ [hog hoot] dock $(hat hed.hat, bat hed.bat) + =^ [log loot] dock $(hat tal.hat, bat tal.bat) + [[%fork hog log ?&(safe.hat safe.bat)] (weld hoot loot)] dock] + == + == + =/ blab (milk %copy) + :_ dock(pond (~(put by pond) blab [moot %hop her])) + [tog blab] + ++ twin :: split sans from flow + ^- [[plow plow berm] _dock] + ?- flow + [%rift *] + =^ hole dock bomb + :_ dock + [[%disc ~] [%disc ~] hole] + :: + [%pond ~] + =^ one dock wean + =^ two dock wean + =^ ret dock wean + =^ her dock (mend %taco ~[[%con one two ret]] [%don ret]) + :_ dock + [[%tine one] [%tine two] her] + :: + [%moat *] + ?- what.flow + [%fork *] + :_ dock + [left.what.flow rite.what.flow wher.flow] + :: + [%disc ~] + :_ dock + [[%disc ~] [%disc ~] wher.flow] + [%tine @] + :_ dock + =^ one dock wean + =^ two dock wean + =^ her dock (mend %cons ~[[%con one two +.what.flow]] [%hop wher.flow]) + :_ dock + [[%tine one] [%tine two] her] + == + == + ++ mend + |= [gen=@ =lock] + ^- [berm _dock] + =/ curb (milk gen) + :- curb + dock(pond (~(put by pond.dock) berm lock)) + ++ bomb + ^- [berm _dock] + (mend %boom ~ [%bom ~]) + -- -- diff --git a/docs/spec/ska/lib/run.hoon b/docs/spec/ska/lib/run.hoon index b380852..6cbe8f9 100644 --- a/docs/spec/ska/lib/run.hoon +++ b/docs/spec/ska/lib/run.hoon @@ -3,7 +3,7 @@ |% ++ real |= [ject=* form=*] - =/ labl [[%gues ~] form] + =/ labl [[%toss ~] form] =/ prog prog:+:(gene:degen labl) (play ject prog labl) ++ play @@ -49,15 +49,15 @@ :: [%lnt ~] =/ dorm (gett 4) - =. prog prog:+:(gene:degen(prog prog) [[%gues ~] dorm]) - =/ entu (~(get by prog) [[%gues ~] dorm]) + =. prog prog:+:(gene:degen(prog prog) [[%toss ~] dorm]) + =/ entu (~(get by prog) [[%toss ~] dorm]) ?~ entu ~| 'No entry for given labl' !! $:this(inst does.u.entu) :: [%lnk ~] =/ dorm (gett 4) - =. prog prog:+:(gene:degen(prog prog) [[%gues ~] dorm]) + =. prog prog:+:(gene:degen(prog prog) [[%toss ~] dorm]) =/ entu (~(get by prog) entr) ?~ entu ~| 'No entry for given labl' !! diff --git a/docs/spec/ska/lib/ska.hoon b/docs/spec/ska/lib/ska.hoon index 3c13ad1..f5c39c4 100644 --- a/docs/spec/ska/lib/ska.hoon +++ b/docs/spec/ska/lib/ska.hoon @@ -1,46 +1,45 @@ /- *sock |% -:: Get an axis from a sock -++ pull +:: Split an axis into a sock into safe and unsafe components +++ punt |= [axe=@ =sock] - ^- boot - ?: .= axe 0 - [%boom ~] + ^- [@ @ sock] + ?: =(0 axe) + [0 0 %toss ~] + =/ saf 1 |- - ?: =(axe 1) - [%safe sock] - ?- sock - :: - [%know @] - [%boom ~] - :: + ?: =(axe 1) + [saf 1 sock] + ?+ sock [0 0 %toss ~] [%know * *] ?- (cap axe) - :: - %2 - $(axe (mas axe), sock [%know -.know.sock]) - %3 - $(axe (mas axe), sock [%know +.know.sock]) + %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 * *] + [%bets *] ?- (cap axe) - :: - %2 - $(axe (mas axe), sock hed.sock) - :: - %3 - $(axe (mas axe), sock tal.sock) + %2 $(axe (mas axe), sock hed.sock, saf (peg saf 2)) + %3 $(axe (mas axe), sock tal.sock, saf (peg saf 3)) == :: - [%dice ~] - [%boom ~] - :: - [%flip ~] - [%boom ~] - :: - [%gues ~] - [%risk %gues ~] + [%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 @@ -63,7 +62,7 @@ [%flip ~] [%know 1] :: - [%gues ~] + [%toss ~] [%flip ~] == :: Test if we can know two socks are equal @@ -171,8 +170,8 @@ [%bets * *] (cobb $(axe (mas axe), sock hed.sock) [%safe tal.sock]) :: - [%gues ~] - (cobb $(axe (mas axe)) [%risk %gues ~]) + [%toss ~] + (cobb $(axe (mas axe)) [%risk %toss ~]) == :: %3 @@ -184,8 +183,8 @@ [%bets * *] (cobb [%safe hed.sock] $(axe (mas axe), sock tal.sock)) :: - [%gues ~] - (cobb [%risk %gues ~] $(axe (mas axe))) + [%toss ~] + (cobb [%risk %toss ~] $(axe (mas axe))) == == :: Stitch a boot into another boot @@ -258,7 +257,7 @@ [%dice ~] ?: ?&(?=([%flip ~] a) ?=([%flip ~] b)) [%flip ~] - [%gues ~] + [%toss ~] :: Produce the intersection of two boots :: :: Note that the intersection of a safe or risk @@ -311,7 +310,7 @@ [%safe %flip ~] [%safe %know 1] :: - [%safe %gues ~] + [%safe %toss ~] [%safe %flip ~] :: [%risk %know @] @@ -329,7 +328,7 @@ [%risk %flip ~] [%risk %know 1] :: - [%risk %gues ~] + [%risk %toss ~] [%risk %flip ~] == ++ pile @@ -346,7 +345,7 @@ [%safe %flip ~] [%safe %dice ~] :: - [%safe %gues ~] + [%safe %toss ~] [%risk %dice ~] :: [%risk %know @] @@ -358,7 +357,7 @@ [%risk %flip ~] [%risk %dice ~] :: - [%risk %gues ~] + [%risk %toss ~] [%risk %dice ~] == :: Produce knowledge of the result given knowledge of the subject @@ -392,7 +391,7 @@ [%boom ~] ?: ?= [%risk %flip ~] forn [%boom ~] - ?+ forn [%risk %gues ~] + ?+ forn [%risk %toss ~] :: [%safe %know *] ?- subn @@ -443,7 +442,7 @@ [%dice ~] (dare (gnaw $(form +>-.form) $(form +>+.form))) :: - [%gues ~] + [%toss ~] (dare (gnaw $(form +>-.form) $(form +>+.form))) == :: @@ -462,7 +461,7 @@ [%dice ~] (dare (gnaw $(form +>-.form) $(form +>+.form))) :: - [%gues ~] + [%toss ~] (dare (gnaw $(form +>-.form) $(form +>+.form))) == == @@ -504,10 +503,10 @@ (dare $(subj sure.news, form know.hope.newf)) :: [%safe *] - [%risk %gues ~] + [%risk %toss ~] :: [%risk *] - [%risk %gues ~] + [%risk %toss ~] == :: [%risk *] @@ -521,10 +520,10 @@ (dare $(subj hope.news, form know.hope.newf)) :: [%safe *] - [%risk %gues ~] + [%risk %toss ~] :: [%risk *] - [%risk %gues ~] + [%risk %toss ~] == == :: @@ -546,7 +545,7 @@ == :: [%12 *] - [%risk %gues ~] + [%risk %toss ~] == ++ cuff |= =sock @@ -567,7 +566,7 @@ [%flip ~] (limo [axe ~]) :: - [%gues ~] + [%toss ~] (limo [axe ~]) == -- diff --git a/docs/spec/ska/sur/gene.hoon b/docs/spec/ska/sur/gene.hoon index aee75fc..e17f5db 100644 --- a/docs/spec/ska/sur/gene.hoon +++ b/docs/spec/ska/sur/gene.hoon @@ -1,35 +1,71 @@ /- *sock |% -+$ labl [sub=sock for=*] -+$ dabl [sub=sock for=* ax=@ gen=@] -+$ cost :: control destination (jump dest) - $% [%dab wher=dabl] :: go here unconditionally - [%bab troo=dabl fals=dabl] :: branch on result - [%ret ~] :: tail position ++| %ska ++$ barn [sub=sock for=*] ++$ nomm :: SKA-analyzed nock + $% [%par nomm nomm] + [%zer @ ?] :: safety-tagged lookup + [%one *] + [%two nomm nomm sock (unit *) ?] :: subject knowledge and known formula, safety-tag on metaformula + [%thr nomm] + [%fou nomm ?] :: safety-tagged increment + [%fiv nomm nomm] + [%six nomm nomm nomm] + [%sev nomm nomm] + [%eig nomm nomm] + [%nin @ nomm sock (unit *) ?] :: subject knowledge and known formula + [%ten [@ nomm] nomm ?] :: safety-tagged edit + [%els @ nomm] + [%eld [@ nomm] nomm ?] :: safety-tagged hint formula + [%twe nomm nomm] == -+$ dast $~(4 @) :: data destination (value dest) -+$ dinn - $% [%imm * @] :: Write a noun to an axis - [%mov @ @] :: Copy an axis to another axis - :: If destination nests under source, fill - :: dangling axes with 0 - [%clq dabl dabl] :: Branch left if axis 4 is a cell, right otherwise - [%inc @] :: Increment the atom at the axis and write it back to the axis - [%eqq dabl dabl] :: Branch left if axes 8 and 9 are structurally equal, right otherwise - [%brn dabl dabl] :: Branch left if axis 4 is atom 0, right if atom 1, crash otherwise - [%hop dabl] :: Go to dabl unconditionally (local direct jump) - [%her dabl] :: Label explicitly in code, as branch or jump target - [%lnk ~] :: Push a frame with a return pointer, eval the code at the axis 4 - :: Places result at axis 4 - [%cal labl] :: Push a frame with a return pointer, call the code at labl - :: Places result at axis 4 - [%lnt ~] :: Eval the code at axis 4 in tail position - [%jmp labl] :: Jump to the code at the label in tail position - [%spy ~] :: Scry with the ref/path pair at axis 4, write back to axis 4 - [%don ~] :: Finish the procedure, returning the value at axis 4 - [%bom ~] :: Crash ++$ farm [yard=(map barn [does=nomm says=boot]) wood=(list barn)] ++| %lin ++$ berm [sub=sock for=* ax=@ gen=@] :: local label ++$ plow :: noun<->ssa map + $% [%fork left=plow rite=plow safe=?] :: cons of two mappings + [%tine @] :: use this SSA value at this axis + [%disc ~] :: no uses here or below == -+$ linn (list dinn) -+$ tine [does=linn says=boot] -+$ tinn (map labl tine) ++$ line :: destination + $% [%moat wher=berm what=plow] :: place result in SSA values specified by what, go wher + [%rift troo=berm fals=berm] :: branch on result + [%pond ~] :: tail position, return result in a register + == ++$ bran :: instructions in a block + $% [%imm * @] :: Write a noun to an SSA value + [%mov @ @] :: Copy an SSA value + [%inc @ @] :: Define second SSA register as increment of first + [%con @ @ @] :: Construct a cell, first SSA head, second SSA tail, third SSA result + [%hed @ @] :: Take the head of first SSA and place in second. + :: Crash if first SSA not a cell + [%hud @ @] :: Take the head of the first SSA, known to be a cell + [%tal @ @] :: Take tail head of first SSA and place in second. + :: Crash if first SSA not a cell + [%tul @ @] :: Take the tail of the first SSA, known to be a cell + == ++$ germ :: instructions ending a block + $% [%clq @ berm berm] :: Branch left if the SSA value is a cell, right otherwise + [%eqq @ @ berm berm] :: Branch left if SSA registers are equal, right otherwise + [%brn @ berm berm] :: Branch left if SSA register is 0, right if 1 + [%hop berm] :: Go to berm unconditionally (local direct jump) + [%lnk @ @ @ berm] :: Call formula in first SSA register with subject in second, + :: result in third, return to berm + [%cal barn (list @) @ berm] :: Call arm given by barn, subject in first SSA register, + :: result in second, return to berm + [%lnt @ @] :: Jump to formula in first SSA register with subject in second + [%jmp barn (list @)] :: Jump to the code at the label in tail position, + :: with the subject in the SSA register + [%spy @ @ @ berm] :: Scry with the ref/path pair in the first 2 SSA registers + :: define the third as the result + [%hnt @ berm] :: Treat the result in the SSA register as a hint and continue to the given label + + [%don @] :: Finish the procedure, returning the value at axis 4 + [%bom ~] :: Crash + == ++$ lock [body=(list bran) bend=germ] :: basic block: instructions + a terminator or branch ++$ lake (map (unit berm) lock) :: labeled basic blocks ++$ rice [goes=lake uses=(list @)] :: labeled basic blocks and entry point arguments as subject axes ++$ sack [does=rice says=boot] :: code table entry: basic blocks + SKA result for an arm ++$ town [land=(map barn sack) lamb=@] :: code table -- diff --git a/docs/spec/ska/sur/sock.hoon b/docs/spec/ska/sur/sock.hoon index 6c3a14f..756d140 100644 --- a/docs/spec/ska/sur/sock.hoon +++ b/docs/spec/ska/sur/sock.hoon @@ -4,11 +4,11 @@ [%bets hed=sock tal=sock] :: This noun is a cell, with partial knowledge of its head and tail [%dice ~] :: This noun is an atom [%flip ~] :: This noun is an atom, specifically 0 or 1 - [%gues ~] :: We know nothing about this noun + [%toss ~] :: We know nothing about this noun == +$ boot - $% [%safe sure=sock] :: The Nock that produces this noun will not crash + $% [%boom ~] :: The Nock will crash [%risk hope=sock] :: The Nock that produces this noun might crash - [%boom ~] :: The Nock will crash + [%safe sure=sock] :: The Nock that produces this noun will not crash == --