Merge branch 'philip/core-gol' (#1928)

* philip/core-gol:
  hoon: extend gol check through cores

Signed-off-by: Jared Tobin <jared@tlon.io>
This commit is contained in:
Jared Tobin 2019-11-09 18:36:32 +08:00
commit a480e3aafd
No known key found for this signature in database
GPG Key ID: 0E4647D58F8A69E4
2 changed files with 127 additions and 9 deletions

View File

@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:ccb3dc7661a01ab606806bc2d2bf8dfca349ad37ac49432937336431f20b5880
size 8935337
oid sha256:9e6a332c3f22b3448284437ab597a2f0a76649a2c380a558f16eb788769e25c0
size 8958901

View File

@ -10013,13 +10013,13 @@
++ hemp
:: generate formula from foot
::
|= [hud/poly gen/hoon]
|= [hud/poly gol/type gen/hoon]
^- nock
~+
=+ %hemp-141
?- hud
$dry q:(mint %noun gen)
$wet q:(mint(vet |) %noun gen)
$dry q:(mint gol gen)
$wet q:(mint(vet |) gol gen)
==
::
++ laze
@ -10043,7 +10043,7 @@
^- (unit noun)
%+ bind (~(get by tal) axe)
|= gen/hoon
%. [hud gen]
%. [hud %noun gen]
hemp(sut (core sut [nym hud %gold] sut [[%lazy 1 ..^$] ~] dom))
::
%- ~(gas by *(map @ud hoon))
@ -10167,8 +10167,11 @@
++ mine
:: mint all chapters and feet in a core
::
|= [mel/vair nym/(unit term) hud/poly dom/(map term tome)]
|= [gol/type mel/vair nym/(unit term) hud/poly dom/(map term tome)]
^- (pair type nock)
|^
=/ log (chapters-check (core-check gol))
=/ dog (get-tomes log)
=- :_ [%1 dez]
(core sut [nym hud mel] sut [[%full ~] dez] dom)
^= dez
@ -10178,10 +10181,12 @@
~
=/ dov/?(~ ^)
=/ dab/(map term hoon) q.q.n.dom
=/ dag (arms-check dab (get-arms dog p.n.dom))
|- ^- ?(~ ^)
?: ?=(~ dab)
~
=+ vad=(hemp hud q.n.dab)
=/ gog (get-arm-type log dag p.n.dab)
=+ vad=(hemp hud gog q.n.dab)
?- dab
{* ~ ~} vad
{* ~ *} [vad $(dab r.dab)]
@ -10195,6 +10200,119 @@
{* * *} [dov $(dom l.dom) $(dom r.dom)]
==
::
:: all the below arms are used for gol checking and should have no
:: effect other than giving more specific errors
::
:: all the possible types we could be expecting.
::
+$ gol-type
$~ %noun
$@ %noun
$% [%cell p=type q=type]
[%core p=type q=coil]
[%fork p=(set gol-type)]
==
:: check that we're looking for a core
::
++ core-check
|= log=type
|- ^- gol-type
?+ log $(log repo(sut log))
%noun (nice log &)
%void (nice %noun |)
[%atom *] (nice %noun |)
[%cell *] (nice log (nest(sut p.log) & %noun))
[%core *] (nice log(r.p.q %gold) &)
[%fork *]
=/ tys ~(tap in p.log)
:- %fork
|- ^- (set gol-type)
?~ tys
~
=/ a ^$(log i.tys)
=/ b $(tys t.tys)
(~(put in b) a)
==
:: check we have the expected number of chapters
::
++ chapters-check
|= log=gol-type
|- ^- gol-type
?- log
%noun (nice log &)
[%cell *] (nice log &)
[%core *] ~_ leaf+"core-number-of-chapters"
(nice log =(~(wyt by dom) ~(wyt by q.r.q.log)))
[%fork *]
=/ tys ~(tap in p.log)
|- ^- gol-type
?~ tys
log
=/ a ^$(log i.tys)
=/ b $(tys t.tys)
log
==
:: get map of tomes if exists
::
++ get-tomes
|= log=gol-type
^- (unit (map term tome))
?- log
%noun ~
[%cell *] ~
[%fork *] ~ :: maybe could be more aggressive
[%core *] `q.r.q.log
==
:: get arms in tome
::
++ get-arms
|= [dog=(unit (map term tome)) nam=term]
^- (unit (map term hoon))
%+ bind dog
|= a/(map term tome)
~_ leaf+"unexpcted-chapter.{(trip nam)}"
q:(~(got by a) nam)
:: check we have the expected number of arms
::
++ arms-check
|= [dab=(map term hoon) dag=(unit (map term hoon))]
?~ dag
dag
=/ a
=/ exp ~(wyt by u.dag)
=/ hav ~(wyt by dab)
~_ =/ expt (scow %ud exp)
=/ havt (scow %ud hav)
leaf+"core-number-of-arms.exp={expt}.hav={havt}"
~_ =/ missing ~(tap in (~(dif in ~(key by u.dag)) ~(key by dab)))
leaf+"missing.{<missing>}"
~_ =/ extra ~(tap in (~(dif in ~(key by dab)) ~(key by u.dag)))
leaf+"extra.{<extra>}"
~_ =/ have ~(tap in ~(key by dab))
leaf+"have.{<have>}"
(nice dag =(exp hav))
a
:: get expected type of this arm
::
++ get-arm-type
|= [log=gol-type dag=(unit (map term hoon)) nam=term]
^- type
%- fall :_ %noun
%+ bind dag
|= a=(map term hoon)
=/ gen=hoon
~_ leaf+"unexpected-arm.{(trip nam)}"
(~(got by a) nam)
(play(sut log) gen)
::
++ nice
|* [typ=* gud=?]
?: gud
typ
~_ leaf+"core-nice"
!!
--
::
++ mint
~/ %mint
|= {gol/type gen/hoon}
@ -10342,7 +10460,7 @@
|= {mel/vair nym/(unit term) hud/poly ruf/hoon dom/(map term tome)}
^- {p/type q/nock}
=+ dan=^$(gen ruf, gol %noun)
=+ pul=(mine mel nym hud dom)
=+ pul=(mine gol mel nym hud dom)
[(nice p.pul) (cons q.pul q.dan)]
--
::