mirror of
https://github.com/urbit/ares.git
synced 2024-11-23 00:25:49 +03:00
130 lines
3.0 KiB
Plaintext
130 lines
3.0 KiB
Plaintext
/- *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))
|
|
--
|