urbit/ares
1
1
Fork 0
mirror of https://github.com/urbit/ares.git synced 2024-11-22 15:08:54 +03:00
Code Issues Packages Projects Releases Wiki Activity

[ska] prototypes for initialization

Browse Source
This commit is contained in:
Edward Amsden 2023-03-08 15:43:26 -06:00
parent f4bbc255f0
commit f86ba2fb31
2 changed files with 433 additions and 187 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

491
hoon/codegen/lib/ska.hoon
View File

@ -1,5 +1,19 @@
/- *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]
@ -244,11 +258,11 @@
?: ?&(?=([%know *] a) ?=([%know *] b))
?: =(know.a know.b)
a
$(a (fray a), b (fray b))
$(a (fray know.a), b (fray know.b))
?: ?=([%know *] a)
$(a (fray a))
$(a (fray know.a))
?: ?=([%know *] b)
$(b (fray 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)))
@ -364,209 +378,312 @@
++ 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)
?: ?=([%boom ~] subn)
[%boom ~]
=/ forn $(form +>.form)
?: ?=([%boom ~] forn)
[%boom ~]
?: ?= [%safe %dice ~] forn
[%boom ~]
?: ?= [%safe %flip ~] forn
[%boom ~]
?: ?= [%risk %dice ~] forn
[%boom ~]
?: ?= [%risk %flip ~] forn
[%boom ~]
?+ forn [%risk %toss ~]
=| ward=(map [sock *] boot)
=. ward (~(put by ward) [subj form] [%risk %toss ~])
|^
-:swab
++ swab
|-
^- [boot _ward]
?> ?=(^ form)
?+ form [[%boom ~] ward]
::
[%safe %know *]
?- subn
::
[%safe *]
$(subj sure.subn, form know.sure.forn)
::
[%risk *]
(dare $(subj hope.subn, form know.sure.forn))
==
[[* *] *]
=^ l ward $(form -.form)
=^ r ward $(form +.form)
:_ ward
(cobb l r)
::
[%risk %know *]
?- subn
::
[%safe *]
(dare $(subj sure.subn, form know.hope.forn))
::
[%risk *]
(dare $(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 ~]
[%0 @]
:_ ward
(pull +.form subj)
::
[%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)))
::
[%toss ~]
(dare (gnaw $(form +>-.form) $(form +>+.form)))
==
[%1 *]
:_ ward
[%safe %know +.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)))
::
[%toss ~]
(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 (knit sure.news subj), form +>.form)
::
[%risk *]
(dare $(subj (knit hope.news subj), form +>.form))
==
::
[%9 @ *]
=/ news $(form +>.form)
?+ news [%boom ~]
::
[%safe *]
=/ newf (pull +<.form sure.news)
?+ newf [%boom ~]
[%2 * *]
=^ subn ward $(form +<.form)
?: ?=([%boom ~] subn)
[[%boom ~] ward]
=^ forn ward $(form +>.form)
?: ?=([%boom ~] forn)
[[%boom ~] ward]
?: ?= [%safe %dice ~] forn
[[%boom ~] ward]
?: ?= [%safe %flip ~] forn
[[%boom ~] ward]
?: ?= [%risk %dice ~] forn
[[%boom ~] ward]
?: ?= [%risk %flip ~] forn
[[%boom ~] ward]
?+ forn [[%risk %toss ~] ward]
::
[%safe %know *]
$(subj sure.news, form know.sure.newf)
?- subn
::
[%safe *]
=/ nubs sure.subn
=/ norm know.sure.forn
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
[r (~(put by ward) [nubs norm] r)]
::
[%risk *]
=/ nubs hope.subn
=/ norm know.sure.forn
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
[(dare r) (~(put by ward) [nubs norm] (dare r))]
==
::
[%risk %know *]
(dare $(subj sure.news, form know.hope.newf))
::
[%safe *]
[%risk %toss ~]
::
[%risk *]
[%risk %toss ~]
?- subn
::
[%safe *]
=/ nubs sure.subn
=/ norm know.hope.forn
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
[(dare r) (~(put by ward) [nubs norm] (dare r))]
::
[%risk *]
=/ nubs hope.subn
=/ norm know.hope.forn
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
[(dare r) (~(put by ward) [nubs norm] (dare r))]
==
==
::
[%risk *]
=/ newf (pull +<.form hope.news)
?+ newf [%boom ~]
::
[%safe %know *]
(dare $(subj hope.news, form know.sure.newf))
::
[%risk %know *]
(dare $(subj hope.news, form know.hope.newf))
[%3 *]
=^ s ward $(form +.form)
:_ ward
(ques s)
::
[%4 *]
=^ s ward $(form +.form)
:_ ward
(pile s)
::
[%5 * *]
=^ l ward $(form +<.form)
=^ r ward $(form +>.form)
:_ ward
(bopp l r)
::
[%6 * * *]
=^ cond ward $(form +<.form)
?+ cond [[%boom ~] ward]
::
[%safe *]
[%risk %toss ~]
?+ sure.cond [[%boom ~] ward]
::
[%know %0]
$(form +>-.form)
::
[%know %1]
$(form +>+.form)
::
[%flip ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(gnaw t f)
::
[%dice ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(dare (gnaw t f))
::
[%toss ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(dare (gnaw t f))
==
::
[%risk *]
[%risk %toss ~]
?+ hope.cond [[%boom ~] ward]
::
[%know %0]
=^ t ward $(form +>-.form)
:_ ward
(dare t)
::
[%know %1]
=^ f ward $(form +>+.form)
:_ ward
(dare f)
::
[%flip ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(dare (gnaw t f))
::
[%dice ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(dare (gnaw t f))
::
[%toss ~]
=^ t ward $(form +>-.form)
=^ f ward $(form +>+.form)
:_ ward
(dare (gnaw t f))
==
==
==
::
[%10 [@ *] *]
(welt +<-.form $(form +<+.form) $(form +>.form))
::
[%11 @ *]
$(form +>.form)
::
[%11 [* *] *]
=/ hint $(form +<+.form)
?+ hint [%boom ~]
::
[%safe *]
[%7 * *]
=^ news ward $(form +<.form)
?+ news [[%boom ~] ward]
::
[%safe *]
$(subj sure.news, form +>.form)
::
[%risk *]
=^ r ward $(subj hope.news, form +>.form)
:_ ward
(dare r)
==
::
[%8 * *]
=^ news ward $(form +<.form)
?+ news [[%boom ~] ward]
::
[%safe *]
$(subj (knit sure.news subj), form +>.form)
::
[%risk *]
=^ r ward $(subj (knit hope.news subj), form +>.form)
:_ ward
(dare r)
==
::
[%9 @ *]
=^ news ward $(form +>.form)
?+ news [[%boom ~] ward]
::
[%safe *]
=/ newf (pull +<.form sure.news)
?+ newf [[%boom ~] ward]
::
[%safe %know *]
=/ nubs sure.news
=/ norm know.sure.newf
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
:_ (~(put by ward) [nubs norm] r)
r
::
[%risk %know *]
=/ nubs sure.news
=/ norm know.hope.newf
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
:_ (~(put by ward) [nubs norm] (dare r))
(dare r)
::
[%safe *]
[[%risk %toss ~] ward]
::
[%risk *]
[[%risk %toss ~] ward]
==
::
[%risk *]
=/ newf (pull +<.form hope.news)
?+ newf [[%boom ~] ward]
::
[%safe %know *]
=/ nubs hope.news
=/ norm know.sure.newf
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
:_ (~(put by ward) [nubs norm] (dare r))
(dare r)
::
[%risk %know *]
=/ nubs hope.news
=/ norm know.hope.newf
=/ mem (~(get by ward) [nubs norm])
?. ?=(~ mem) [u.mem ward]
=. ward (~(put by ward) [nubs norm] [%risk %toss ~])
=^ r ward $(subj nubs, form norm)
:_ (~(put by ward) [nubs norm] (dare r))
(dare r)
::
[%safe *]
[[%risk %toss ~] ward]
::
[%risk *]
[[%risk %toss ~] ward]
==
==
::
[%10 [@ *] *]
=^ p ward $(form +<+.form)
=^ w ward $(form +>.form)
:_ ward
(welt +<-.form p w)
::
[%11 @ *]
$(form +>.form)
::
[%risk *]
(dare $(form +>.form))
[%11 [* *] *]
=^ hint ward $(form +<+.form)
?+ hint [[%boom ~] ward]
::
[%safe *]
$(form +>.form)
::
[%risk *]
=^ r ward $(form +<.form)
:_ ward
(dare r)
==
::
[%12 *]
[[%risk %toss ~] ward]
==
--
++ cuff
|= =sock
=/ axe 1
|-
^- (list @)
?- sock
::
[%12 *]
[%risk %toss ~]
[%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 ~])
==
++ 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 ~])
==
--

129
hoon/codegen/lib/sky.hoon Normal file
View File

@ -0,0 +1,129 @@
/- *sock
/+ ska
|%
:: mask axes in a noun to make a sock
++ dope
|= [mask=(list @) non=noun]
^- boot
=/ sack=boot [%safe %know non]
|-
^- boot
?~ mask sack
$(sack (welt:ska i.mask [%safe %toss ~] sack), mask t.mask)
:: turn a hoon type into a boot
++ wove
|= kine=type
^- boot
?@ kine
?- kine
%noun [%risk %toss ~]
%void [%boom ~]
==
?- -.kine
%atom
?~ q.kine
[%risk %dice ~]
[%risk %know u.q.kine]
::
%cell
(cobb:ska $(kine p.kine) $(kine q.kine))
::
%core
%+ cobb:ska
(spry p.r.q.kine) :: compiled battery
$(kine p.kine) :: current payload
::
%face
$(kine q.kine)
::
%fork
=/ tins ~(tap in p.kine)
?~ tins [%risk %toss ~]
=/ hypo $(kine i.tins)
=/ tons t.tins
|-
^- boot
?~ tons hypo
$(hypo (gnaw:ska ^$(kine i.tons) hypo))
::
%hint
$(kine q.kine)
::
%hold
$(kine p.kine)
==
:: turn a seminoun into a sock
++ spry
|= seminoun
^- boot
?- -.mask
%half
?> ?=(^ data)
(cobb:ska $(mask left.mask, data -.data) $(mask rite.mask, data +.data))
::
%full
?~ blocks.mask
[%risk %know data]
[%risk %toss ~]
::
%lazy
[%risk %toss ~]
==
:: for a stateful core, figure out what we can assume across all state
:: transitions
::
:: step is a list of arm axes and result axes which are expected to produce gates
:: the gates will be simul-slammed with %toss
:: then the result axis will be intersected with the stateful core
:: knowledge
::
:: fixed point termination argument: we can only know the same or less
:: than what we knew last time (intersection cannot add knowledge)
:: if we know the same, we stop now. We can only subtract finitely many
:: axes of knowledge from the tree before we know [%boom ~] or
:: [%risk %gues ~] at which point we will learn the same thing twice
:: and terminate
++ arid
|= [muck=boot step=(list [@ @])]
^- boot
=/ yuck muck
=/ stop step
?: ?=(%boom -.muck)
[%boom ~]
|-
^- boot
?~ stop
?: =(yuck muck)
yuck
^$(muck yuck)
=/ erm (yank:ska -.i.stop muck)
?: ?=(%boom -.erm)
$(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
=/ arm (trip:ska erm)
?~ arm
$(stop t.stop, yuck (gnaw:ska [%risk %toss ~] yuck))
=/ cor
?- -.muck
%safe sure.muck
%risk hope.muck
==
=/ mat (wash:ska cor u.arm)
?: ?=(%boom -.mat)
$(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
=/ ear (yank:ska 2 mat)
?: ?=(%boom -.ear)
$(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
=/ gar (trip:ska ear)
?~ gar
$(stop t.stop, yuck (gnaw:ska [%risk %toss ~] yuck))
=/ mar (welt:ska 6 [%risk %toss ~] mat)
?: ?=(%boom -.mar)
$(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
=/ gor
?- -.mar
%safe sure.mar
%risk hope.mar
==
=/ beg (wash:ska gor u.gar)
$(stop t.stop, yuck (gnaw:ska (yank:ska +.i.stop beg) yuck))
--