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

infinite loops, somewhere

Browse Source
This commit is contained in:
Edward Amsden 2022-02-17 17:47:12 -06:00
parent 65b5e829e0
commit 92f7604a87
No known key found for this signature in database
GPG Key ID: 548EDF608CA956F6
1 changed files with 200 additions and 149 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

349
subject-knowledge/lib/subject-knowledge.hoon
View File

@ -1,7 +1,7 @@
=< =<
:: a memoization for formula analysis, updated/inspected at eval :: a memoization for formula analysis, updated/inspected at eval
:: boundaries (2/9) :: boundaries (2/9)
=| memo=(map [sock *] [(unit sock) (unit @tas)]) =| memo=(map * (list [sock (unit sock) (unit @tas)]))
:: A jet dashboard :: A jet dashboard
:: ::
:: The @tas tag is used only for debugging :: The @tas tag is used only for debugging
@ -9,22 +9,61 @@
|% |%
:: Partial knowledge of a noun :: Partial knowledge of a noun
+$ sock ^sock +$ sock ^sock
++ entr
|= [s=sock f=* nam=(unit @tas)]
^- (each _memo [r=(unit sock) n=(unit @tas)])
=/ entry
=/ e (~(get by memo) f) ?~ e ~ u.e
|-
^- (each _memo [(unit sock) (unit @tas)])
?~ entry
:- %&
?: (~(has by memo) f)
(~(jab by memo) f |=(e=(list [sock (unit sock) (unit @tas)]) [[s ~ nam] e]))
(~(put by memo) f ~[[s ~ nam]])
?: (mous -<.entry s)
[%| ->.entry]
$(entry +.entry)
++ exit
|= [s=sock f=* r=sock]
^- _memo
~| "Should not exit where there is no entry"
%:
~(jab by memo)
f
|= e=(list [sock (unit sock) (unit @tas)])
|-
^- (list [sock (unit sock) (unit @tas)])
?< ?= %~ e
?: =(-<.e s)
[[s `r ->+.e] +.e]
[-.e $(e +.e)]
==
++ bord *(map * (list [sock [$-(* *) @tas]])) ++ bord *(map * (list [sock [$-(* *) @tas]]))
:: test whether a sock nests in another sock :: test whether a sock nests in another sock
:: a=sock nests in b=sock if b has the same information as a, or :: a=sock nests in b=sock if b has the same information as a, or
:: strictly more information :: strictly more information
:: ::
:: mous ignores hints for matching
++ mous ++ mous
|= [a=sock b=sock] |= [a=sock b=sock]
^- ? ^- ?
?: ?= [%gues ~] a ?: ?= [%gues ~] a
%.y %.y
?: ?= [%hint *] a
$(a r.a)
?: ?= [%hint *] b
$(b r.b)
?- a ?- a
::
[%hint *]
?&
?= [%hint *] b
.= s.a s.b
?~ d.a
?~ d.b
%.y
%.n
?~ d.b
%.n
$(u.d.a u.d.b)
$(r.a r.b)
==
:: ::
[%know *] [%know *]
?| ?|
@ -61,7 +100,8 @@
++ wash ++ wash
|= [s=sock f=*] |= [s=sock f=*]
^- [sock _memo] ^- [sock _memo]
[r.- +]:(pull s f) =+ (pull s f)
[(cort -<) ->]
:: Check for a jet :: Check for a jet
++ juke ++ juke
|= [s=sock f=*] |= [s=sock f=*]
@ -157,11 +197,11 @@
|- |-
^- [sock (unit @tas)] ^- [sock (unit @tas)]
?: =(b 1) ?: =(b 1)
?. ?= [%hint *] s [s ~] ?. ?= [%hint *] s [s nam]
?. =(s.s %fast) [s ~] ?. =(s.s %fast) [s nam]
?~ d.s [s ~] ?~ d.s [s nam]
=/ namsock (yarn u.d.s 2) =/ namsock (yarn u.d.s 2)
?. ?= [%know @] namsock [s ~] ?. ?= [%know @] namsock [s nam]
[s `k.namsock] [s `k.namsock]
?: ?= [%hint *] s ?: ?= [%hint *] s
?. =(s.s %fast) $(s r.s) ?. =(s.s %fast) $(s r.s)
@ -327,6 +367,9 @@
[%jet *] [%jet *]
[%gues ~] [%gues ~]
== ==
++ pull
|= [s=sock f=*]
(pull-eval s [%know f] ~)
++ pull-eval ++ pull-eval
|= [s=sock f=sock nam=(unit @tas)] |= [s=sock f=sock nam=(unit @tas)]
^- [coot _memo] ^- [coot _memo]
@ -339,160 +382,168 @@
:: found a jet :: found a jet
~& "Jet: {<+.u.jet>}" ~& "Jet: {<+.u.jet>}"
[[%jet +.u.jet] memo] [[%jet +.u.jet] memo]
=/ mem (~(get by memo) [s k.f]) =/ mem=(each _memo [r=(unit sock) n=(unit @tas)]) (entr s k.f nam)
?~ mem ?- mem
:: memo miss ::
=. memo (~(put by memo) [s k.f] [~ nam]) :: blackhole for recursive eval [%& *]
=^ res memo (pull s k.f) :: ~& "Miss sock: {<s>}"
~& "Miss: sock {<s>} formula {<k.f>}" :: ~& "Miss formula: {<k.f>}"
=. memo (~(jab by memo) [s k.f] |=([(unit sock) nm=(unit @tas)] [`r.res nm])) :: ~& "Miss name: {<nam>}"
[[%mis res] memo] :: fill in result =. memo +.mem
?~ -.u.mem =^ res memo (pull-inner s k.f)
:: memo blackhole =. memo (exit s k.f r.res)
~& "Recur: sock {<[s]>} formula {<k.f>}" [[%mis res] memo]
[[%rec s k.f] memo] ::
:: memo hit [%| *]
~& "Hit: sock {<[s]>} formula {<k.f>} result {<u.u.mem>}" ?~ r.p.mem
[[%hit u.-.u.mem] memo] :: memo blackhole
++ pull ~& "Recur: sock {<[s]>} formula {<k.f>}"
[[%rec s k.f] memo]
:: memo hit
~& "Hit: sock {<[s]>} formula {<k.f>} result {<u.r.p.mem>} named {<n.p.mem>}"
[[%hit u.r.p.mem] memo]
==
++ pull-inner
|= [s=sock f=*] |= [s=sock f=*]
^- [foot _memo] ^- [foot _memo]
~| "Formula {(scow %q (mug f))}" ~& "Formula {<f>}"
?+ f ~| "Unrecognized nock {<f>}" ~| %pull-bonk !! =/ r
:: ?+ f ~| "Unrecognized nock {<f>}" ~| %pull-bonk !!
[[* *] *] ::
=^ pfoot memo $(f -.f) [[* *] *]
=^ qfoot memo $(f +.f) =^ pfoot memo $(f -.f)
[[[%cell pfoot qfoot] s=s r=(knit [%bets r.pfoot [%gues ~]] 3 r.qfoot)] memo] =^ qfoot memo $(f +.f)
:: [[[%cell pfoot qfoot] s=s r=(knit [%bets r.pfoot [%gues ~]] 3 r.qfoot)] memo]
[%0 b=@] ::
[[[%0 b.f] s=s r=(yarn s b.f)] memo] [%0 b=@]
:: [[[%0 b.f] s=s r=(yarn s b.f)] memo]
[%1 b=*] ::
[[[%1 b.f] s=s r=[%know b.f]] memo] [%1 b=*]
:: [[[%1 b.f] s=s r=[%know b.f]] memo]
[%2 b=* c=*] ::
=^ bfoot memo $(f b.f) [%2 b=* c=*]
=^ cfoot memo $(f c.f) =^ bfoot memo $(f b.f)
=/ [r=sock nam=(unit @tas)] (narn r.cfoot 1) =^ cfoot memo $(f c.f)
=^ coot memo (pull-eval r.bfoot r nam) =/ [r=sock nam=(unit @tas)] (narn r.cfoot 1)
[[[%2 bfoot cfoot coot] s (cort coot)] memo] =^ coot memo (pull-eval r.bfoot r nam)
:: [[[%2 bfoot cfoot coot] s (cort coot)] memo]
[%3 b=*] ::
=^ bfoot memo $(f b.f) [%3 b=*]
=/ br r.bfoot =^ bfoot memo $(f b.f)
=/ r =/ br r.bfoot
=/ r
|-
?- br
::
[%hint *]
$(br r.br)
::
[%know @]
[%know 1]
::
[%know * *]
[%know 0]
::
[%bets * *]
[%know 0]
::
[%gues ~]
[%gues ~]
==
[[[%3 bfoot] s r] memo]
::
[%4 b=*]
=^ bfoot memo $(f b.f)
[[[%4 bfoot] s [%gues ~]] memo]
::
[%5 b=* c=*]
=^ bfoot memo $(f b.f)
=^ cfoot memo $(f c.f)
=/ br r.bfoot
=/ cr r.cfoot
=/ r
|-
?: ?= [%hint *] br
$(br r.br)
?: ?= [%hint *] cr
$(cr r.cr)
?: ?= [%know *] r.bfoot
?: ?= [%know *] r.cfoot
[%know =(k.r.bfoot k.r.cfoot)]
[%gues ~]
[%gues ~]
[[[%5 bfoot cfoot] s r] memo]
::
[%6 b=* c=* d=*]
=^ bfoot memo $(f b.f)
=/ br r.bfoot
|- |-
?- br ?+ br ~| %pull-nest !!
:: ::
[%hint *] [%hint *]
$(br r.br) $(br r.br)
:: ::
[%know @] [%know %0]
[%know 1] =^ cfoot memo ^$(f c.f)
[[[%6 bfoot `cfoot ~] s r.cfoot] memo]
:: ::
[%know * *] [%know %1]
[%know 0] =^ dfoot memo ^$(f d.f)
:: [[[%6 bfoot ~ `dfoot] s r.dfoot] memo]
[%bets * *]
[%know 0]
:: ::
[%gues ~] [%gues ~]
[%gues ~] =^ cfoot memo ^$(f c.f)
=^ dfoot memo ^$(f d.f)
[[[%6 bfoot `cfoot `dfoot] s [%gues ~]] memo]
== ==
[[[%3 bfoot] s r] memo]
::
[%4 b=*]
=^ bfoot memo $(f b.f)
[[[%4 bfoot] s [%gues ~]] memo]
::
[%5 b=* c=*]
=^ bfoot memo $(f b.f)
=^ cfoot memo $(f c.f)
=/ br r.bfoot
=/ cr r.cfoot
=/ r
|-
?: ?= [%hint *] br
$(br r.br)
?: ?= [%hint *] cr
$(cr r.cr)
?: ?= [%know *] r.bfoot
?: ?= [%know *] r.cfoot
[%know =(k.r.bfoot k.r.cfoot)]
[%gues ~]
[%gues ~]
[[[%5 bfoot cfoot] s r] memo]
::
[%6 b=* c=* d=*]
=^ bfoot memo $(f b.f)
=/ br r.bfoot
|-
?+ br ~| %pull-nest !!
:: ::
[%hint *] [%7 b=* c=*]
$(br r.br) =^ bfoot memo $(f b.f)
=^ cfoot memo $(s r.bfoot, f c.f)
[[[%7 bfoot cfoot] s r.cfoot] memo]
:: ::
[%know %0] [%8 b=* c=*]
=^ cfoot memo ^$(f c.f) =^ bfoot memo $(f b.f)
[[[%6 bfoot `cfoot ~] s r.cfoot] memo] =^ cfoot memo $(s (knit [%bets [%gues ~] s] 2 r.bfoot), f c.f)
[[[%8 bfoot cfoot] s=s r=r.cfoot] memo]
:: ::
[%know %1] [%9 b=@ c=*]
=^ dfoot memo ^$(f d/f) =^ cfoot memo $(f c.f)
[[[%6 bfoot ~ `dfoot] s r.dfoot] memo] =/ [r=sock nam=(unit @tas)] (narn r.cfoot b.f)
=^ coot memo (pull-eval r.cfoot r nam)
[[[%9 b.f cfoot coot] s (cort coot)] memo]
:: ::
[%gues ~] [%10 [b=@ c=*] d=*]
=^ cfoot memo ^$(f c.f) =^ cfoot memo $(f c.f)
=^ dfoot memo ^$(f d.f) =^ dfoot memo $(f d.f)
[[[%6 bfoot `cfoot `dfoot] s [%gues ~]] memo] [[[%10 [b.f cfoot] dfoot] s (knit r.dfoot b.f [%gues ~])] memo]
== ::
:: [%11 b=@ c=*]
[%7 b=* c=*] =^ cfoot memo $(f c.f)
=^ bfoot memo $(f b.f) [[[%11 b.f cfoot] s r=[%hint b.f ~ r.cfoot]] memo]
=^ cfoot memo $(s r.bfoot, f c.f) ::
[[[%7 bfoot cfoot] s r.cfoot] memo] [%11 [b=@ c=*] d=*]
:: =^ cfoot memo $(f c.f)
[%8 b=* c=*] :: implement the %data hint
=^ bfoot memo $(f b.f) :: delete the axes which are looked up in the hint from the subject
=^ cfoot memo $(s (knit [%bets [%gues ~] s] 2 r.bfoot), f c.f) :: knowledge for the hinted computation
[[[%8 bfoot cfoot] s=s r=r.cfoot] memo] ?: =(b.f %data)
:: =/ c c.f
[%9 b=@ c=*] |-
=^ cfoot memo $(f c.f) ?: ?= [[%0 @] *] c
=/ [r=sock nam=(unit @tas)] (narn r.cfoot b.f) =. s (knit s ->.c [%gues ~])
=^ coot memo (pull-eval r.cfoot r nam) $(c +.c)
[[[%9 b.f cfoot coot] s (cort coot)] memo] =^ dfoot memo ^$(f d.f)
:: [[[%11 [b.f cfoot] dfoot] s [%hint b.f `r.cfoot r.dfoot]] memo]
[%10 [b=@ c=*] d=*] =^ dfoot memo $(f d.f)
=^ cfoot memo $(f c.f)
=^ dfoot memo $(f d.f)
[[[%10 [b.f cfoot] dfoot] s (knit r.dfoot b.f r.cfoot)] memo]
::
[%11 b=@ c=*]
=^ cfoot memo $(f c.f)
[[[%11 b.f cfoot] s r=[%hint b.f ~ r.cfoot]] memo]
::
[%11 [b=@ c=*] d=*]
=^ cfoot memo $(f c.f)
:: implement the %data hint
:: delete the axes which are looked up in the hint from the subject
:: knowledge for the hinted computation
?: =(b.f %data)
=/ c c.f
|-
?: ?= [[%0 @] *] c
=. s (knit s ->.c [%gues ~])
$(c +.c)
=^ dfoot memo ^$(f d.f)
[[[%11 [b.f cfoot] dfoot] s [%hint b.f `r.cfoot r.dfoot]] memo] [[[%11 [b.f cfoot] dfoot] s [%hint b.f `r.cfoot r.dfoot]] memo]
=^ dfoot memo $(f d.f) ::
[[[%11 [b.f cfoot] dfoot] s [%hint b.f `r.cfoot r.dfoot]] memo] [%12 ref=* path=*]
:: =^ reffoot memo $(f ref.f)
[%12 ref=* path=*] =^ pathfoot memo $(f path.f)
=^ reffoot memo $(f ref.f) [[[%12 reffoot pathfoot] s [%gues ~]] memo]
=^ pathfoot memo $(f path.f) ==
[[[%12 reffoot pathfoot] s [%gues ~]] memo] ~& "Result {<r>}" r
==
:: example nocks for testing :: example nocks for testing
++ nocs ++ nocs
|% |%