ares/subject-knowledge/lib/subject-knowledge.hoon

627 lines
13 KiB
Plaintext
Raw Normal View History

=<
:: a memoization for formula analysis, updated/inspected at eval
:: boundaries (2/9)
2022-02-18 02:47:12 +03:00
=| memo=(map * (list [sock (unit sock) (unit @tas)]))
:: A jet dashboard
::
:: The @tas tag is used only for debugging
=| jute=(map * (list [sock [$-(* *) @tas]]))
|%
:: Partial knowledge of a noun
+$ sock ^sock
++ sk .
++ lash
|= [[s=sock f=*] j=$-(* *) n=@tas]
=. jute
?. (~(has by jute) f)
(~(put by jute) f (limo ~[[s [j n]]]))
(~(jab by jute) f |=(js=(list [sock [$-(* *) @tas]]) (weld ~[[s [j n]]] js)))
sk
2022-02-18 02:47:12 +03:00
++ 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)]) (weld (limo ~[[s ~ nam]]) e)))
(~(put by memo) f (limo ~[[s ~ nam]]))
2022-02-18 02:47:12 +03:00
?: (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]]))
:: test whether a sock nests in another sock
:: a=sock nests in b=sock if b has the same information as a, or
:: strictly more information
2022-02-17 01:41:27 +03:00
::
++ mous
|= [a=sock b=sock]
^- ?
?: ?= [%gues ~] a
%.y
?- a
2022-02-18 02:47:12 +03:00
::
[%hint *]
?&
?= [%hint *] b
.= s.a s.b
?~ d.a
?~ d.b
%.y
%.n
?~ d.b
%.n
$(a u.d.a, b u.d.b)
$(a r.a, b r.b)
2022-02-18 02:47:12 +03:00
==
::
[%know *]
?|
?&
?= [%know *] b
=(k.a k.b)
==
?&
?= [%bets * *] b
?= [* *] k.a
$(a [%know -.k.a], b p.b)
$(a [%know +.k.a], b q.b)
==
==
::
[%bets * *]
?|
?&
?= [%know * *] b
$(a p.a, b [%know -.k.b])
$(a q.a, b [%know +.k.b])
==
?&
?= [%bets * *] b
$(a p.a, b p.b)
$(a q.a, b q.b)
==
==
==
2022-02-17 01:41:27 +03:00
:: compute what we know of the result of a formula
::
:: We may reimplement this more efficiently later, but this way we
:: don't have to keep updating our experiments in 2 implementations
++ wash
|= [s=sock f=*]
^- [sock _memo]
2022-02-18 02:47:12 +03:00
=+ (pull s f)
[(cort -<) ->]
:: Check for a jet
++ juke
|= [s=sock f=*]
^- (unit [$-(* *) @tas])
=/ jets
=/ j (~(get by jute) f)
^- (list [sock [$-(* *) @tas]])
?~ j ~ u.j
|-
^- (unit [$-(* *) @tas])
?~ jets
~
?: (mous -<.jets s)
`->.jets
$(jets +.jets)
:: learn a noun at an address
2022-02-17 01:41:27 +03:00
::
:: darn discards hints if it must descend through them
::
:: TODO: we use +knit everywhere, this is just +knit with [%know *], can
:: we get rid of it?
++ darn
|= [s=sock b=@ n=*]
^- sock
2022-02-17 01:41:27 +03:00
?: ?= [%hint *] s
$(s r.s)
?: =(b 1)
[%know n]
?: ?= [%know *] s
:- %know
.* [k.s n] [%10 [b [0 3]] [0 2]]
?- (cap b)
::
%2
?- s
::
[%gues ~]
[%bets p=$(b (mas b), s [%gues ~]) q=[%gues ~]]
::
[%bets p=* q=*]
[%bets p=$(b (mas b), s p.s) q=q.s]
==
::
%3
?- s
::
[%gues ~]
[%bets p=[%gues ~] q=$(b (mas b), s [%gues ~])]
::
[%bets p=* q=*]
[%bets p=p.s q=$(b (mas b), s q.s)]
==
==
:: axis into a sock
2022-02-17 01:41:27 +03:00
::
:: yarn will return a hint record if it is at an axis
:: but will discard them as it descends through them
++ yarn
|= [s=sock b=@]
^- sock
?< =(b 0)
|-
?: =(b 1)
s
2022-02-17 01:41:27 +03:00
?: ?= [%hint *] s
$(s r.s) :: descend through hint records
?- s
::
[%know *]
:- %know
.* k.s [0 b]
::
[%gues ~]
[%gues ~]
::
[%bets p=* q=*]
?- (cap b)
::
%2
$(b (mas b), s p.s)
::
%3
$(b (mas b), s q.s)
2022-02-17 01:41:27 +03:00
::
==
==
2022-02-17 01:41:27 +03:00
:: axis into a sock, retrieving a name from a fast hint
++ narn
|= [s=sock b=@]
^- [sock (unit @tas)]
?< =(b 0)
=| nam=(unit @tas)
|-
^- [sock (unit @tas)]
?: =(b 1)
2022-02-18 02:47:12 +03:00
?. ?= [%hint *] s [s nam]
?. =(s.s %fast) [s nam]
?~ d.s [s nam]
2022-02-17 01:41:27 +03:00
=/ namsock (yarn u.d.s 2)
2022-02-18 02:47:12 +03:00
?. ?= [%know @] namsock [s nam]
2022-02-17 01:41:27 +03:00
[s `k.namsock]
?: ?= [%hint *] s
?. =(s.s %fast) $(s r.s)
?~ d.s $(s r.s)
=/ namsock (yarn u.d.s 2)
?. ?= [%know @] namsock $(s r.s)
=. nam `k.namsock
$(s r.s)
?- s
::
[%know *]
:-
:- %know
.* k.s [%0 b]
nam
::
[%gues ~]
[[%gues ~] nam]
::
[%bets * *]
?- (cap b)
::
%2
$(b (mas b), s p.s)
::
%3
$(b (mas b), s q.s)
==
==
:: make a new sock from 2 socks (and an axis)
++ knit
|= [s=sock b=@ t=sock]
^- sock
?: =(b 1)
t
2022-02-17 01:41:27 +03:00
?: ?= [%hint *] s
[%hint s.s d.s $(s r.s)]
?- s
::
[%know @]
~| %know-atom !!
::
[%know * *]
?- (cap b)
::
%2
=/ r $(s [%know +<.s], b (mas b))
?: ?= [%know k=*] r
[%know +.r +>.s]
[%bets r [%know +.k.s]]
::
%3
=/ r $(s [%know +>.s], b (mas b))
?: ?= [%know k=*] r
[%know +<.s +.r]
[%bets [%know +<.s] r]
==
::
[%bets p=* q=*]
?- (cap b)
::
%2
=/ r $(s p.s, b (mas b))
?: ?= [%know k=*] r
?: ?= [%know k=*] q.s
[%know +.r +.q.s]
[%bets r q.s]
[%bets r q.s]
::
%3
=/ r $(s q.s, b (mas b))
?: ?= [%know k=*] r
?: ?= [%know k=*] p.s
[%know +.p.s +.r]
[%bets p.s r]
[%bets p.s r]
==
::
[%gues ~]
=/ r $(b (mas b))
?: ?= [%gues ~] r
[%gues ~]
?- (cap b)
::
%2
[%bets r [%gues ~]]
::
%3
[%bets [%gues ~] r]
==
==
++ pear
|= [a=sock b=sock]
^- sock
?: ?= [%know *] a
?: ?= [%know *] b
[%know =(a b)]
[%gues ~]
[%gues ~]
:: Description of knowledge at a call site
::
:: Codegen behavior
:: %dyn means we will generate a full eval: check cache or codegen,
:: guard on stored sock
::
:: %mis means we will do fresh inline codegen of a formula with a new
:: label
::
:: %rec and %hit both mean we will generate to jumps to labels
:: They differ because for %rec the analysis must treat the call as
:: unknowable, while for %hit we do not re-analyze the call but return
:: the memoized sock
::
:: %jet corresponds to a jump to a jet
+$ coot
$%
[%dyn =sock] :: we don't know the formula
[%mis =foot] :: we know the formula, it's not memoized
[%rec =sock f=*] :: a recursive call, the memo table has a blackhole for this sock/formula pair
[%hit res=sock] :: a memoized call, the memo table has an entry for this sock/formula pair
[%jet jet=@tas] :: call would be jetted
==
:: Annotated Nock tree with subject knowledge
+$ foot
$:
$%
[%1 b=*]
[%2 b=foot c=foot =coot]
[%3 b=foot]
[%4 b=foot]
[%5 b=foot c=foot]
[%6 b=foot c=(unit foot) d=(unit foot)]
[%7 b=foot c=foot]
[%8 b=foot c=foot]
[%9 b=@ c=foot =coot]
[%10 [b=@ c=foot] d=foot]
[%11 b=@ c=foot]
[%11 [b=@ c=foot] d=foot]
[%12 ref=foot path=foot]
[%cell p=foot q=foot]
[%0 b=@]
==
$= s sock
$= r sock
==
++ cort
|= =coot
^- sock
?- coot
::
[%dyn *]
[%gues ~]
::
[%mis *]
r.foot.coot
::
[%rec *]
[%gues ~]
::
[%hit *]
res.coot
::
[%jet *]
[%gues ~]
==
2022-02-18 02:47:12 +03:00
++ pull
|= [s=sock f=*]
(pull-eval s [%know f] ~)
++ pull-eval
2022-02-17 01:41:27 +03:00
|= [s=sock f=sock nam=(unit @tas)]
^- [coot _memo]
2022-02-17 01:41:27 +03:00
?: ?= [%hint *] f $(f r.f)
?. ?= [%know *] f
[[%dyn s] memo]
=/ jet (juke s k.f)
?. ?= ~ jet
:: found a jet
~& "Jet: {<+.u.jet>}"
[[%jet +.u.jet] memo]
2022-02-18 02:47:12 +03:00
=/ mem=(each _memo [r=(unit sock) n=(unit @tas)]) (entr s k.f nam)
?- mem
::
[%& *]
=. memo +.mem
=^ res memo (pull-inner s k.f)
=. memo (exit s k.f r.res)
[[%mis res] memo]
::
[%| *]
?~ r.p.mem
:: memo blackhole
~& "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=*]
^- [foot _memo]
?+ f ~| "Unrecognized nock {<f>}" ~| %pull-bonk !!
::
[[* *] *]
=^ pfoot memo $(f -.f)
=^ 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]
::
[%1 b=*]
[[[%1 b.f] s=s r=[%know b.f]] memo]
::
[%2 b=* c=*]
=^ bfoot memo $(f b.f)
=^ cfoot memo $(f c.f)
=/ [r=sock nam=(unit @tas)] (narn r.cfoot 1)
=^ coot memo (pull-eval r.bfoot r nam)
[[[%2 bfoot cfoot coot] s (cort coot)] memo]
::
[%3 b=*]
=^ bfoot memo $(f b.f)
=/ br r.bfoot
=/ r
2022-02-17 01:41:27 +03:00
|-
?- br
2022-02-17 01:41:27 +03:00
::
[%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 ~| %pull-nest !!
2022-02-17 01:41:27 +03:00
::
[%hint *]
$(br r.br)
2022-02-18 02:47:12 +03:00
::
[%know %0]
=^ cfoot memo ^$(f c.f)
[[[%6 bfoot `cfoot ~] s r.cfoot] memo]
2022-02-18 02:47:12 +03:00
::
[%know %1]
=^ dfoot memo ^$(f d.f)
[[[%6 bfoot ~ `dfoot] s r.dfoot] memo]
2022-02-18 02:47:12 +03:00
::
[%gues ~]
=^ cfoot memo ^$(f c.f)
=^ dfoot memo ^$(f d.f)
[[[%6 bfoot `cfoot `dfoot] s [%gues ~]] memo]
2022-02-18 02:47:12 +03:00
==
::
[%7 b=* c=*]
=^ bfoot memo $(f b.f)
=^ cfoot memo $(s r.bfoot, f c.f)
[[[%7 bfoot cfoot] s r.cfoot] memo]
::
[%8 b=* c=*]
=^ bfoot memo $(f b.f)
=^ cfoot memo $(s (knit [%bets [%gues ~] s] 2 r.bfoot), f c.f)
[[[%8 bfoot cfoot] s=s r=r.cfoot] memo]
::
[%9 b=@ c=*]
=^ cfoot memo $(f c.f)
=/ [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]
::
[%10 [b=@ c=*] d=*]
=^ cfoot memo $(f c.f)
=^ dfoot memo $(f d.f)
[[[%10 [b.f cfoot] dfoot] s (knit r.dfoot b.f [%gues ~])] 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]
=^ 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)
=^ pathfoot memo $(f path.f)
[[[%12 reffoot pathfoot] s [%gues ~]] memo]
==
++ hord
|= [nam=@tas]
^- (list [s=sock f=*])
=| r=(list [s=sock f=*])
=/ entries ~(tap by memo)
|-
^- (list [s=sock f=*])
?~ entries
r
=/ f p.i.entries
=/ entry q.i.entries
|-
^- (list [s=sock f=*])
?~ entry
^$(entries t.entries)
=? r =(+>.i.entry `nam) (weld (limo ~[[-.i.entry f]]) r)
$(entry t.entry)
2022-02-15 18:24:49 +03:00
:: example nocks for testing
++ nocs
|%
++ dec
!=
!.
=>
=> %ed
|%
++ dec
~/ %dec
|= x=@
2022-02-15 18:24:49 +03:00
~> %data.[x ~]
^- @
=| d=@
|-
^- d=@
?: =(.+(d) x)
d
$(d .+(d))
--
(dec 8)
++ ad
!=
!.
=>
=> %ed
|%
++ dec
~/ %dec
|= x=@
2022-02-15 18:24:49 +03:00
~> %data.[x ~]
^- @
=| d=@
|-
^- d=@
?: =(.+(d) x)
d
$(d .+(d))
++ add
~/ %add
|= [x=@ y=@]
2022-02-15 18:24:49 +03:00
~> %data.[x y ~]
^- @
|-
^- @
?: =(x 0)
y
$(x (dec x), y .+(y))
--
(add 5 8)
--
--
|%
+$ sock
$%
[%know k=*]
2022-02-17 01:41:27 +03:00
[%hint s=@ d=(unit sock) r=sock]
[%bets p=sock q=sock]
[%gues ~]
==
--