From e43036d748e097d39b5e69d20bf62739a7c9fc59 Mon Sep 17 00:00:00 2001 From: Philip Monk Date: Fri, 8 Nov 2019 12:53:03 -0800 Subject: [PATCH] hoon: extend gol check through cores This extends `gol` "backward-inference" typechecking to thread through cores. Recall that `gol` is used exclusively for receiving more specific error messages; these changes should have no effect on programs which already compile successfully. Before, this would type-fail on the second `|%`. ``` !: ^+ ^? |% ++ foo *@ud -- |% ++ foo ?: =(1 1) 2 %foo -- ``` With these changes, it gives a mint-nice at `%foo`. It will also give you explicit errors if you have the wrong number/names of arms, including which arms it expects. This is becoming much more important with static gall, since it's the first time we've used core subtyping so extensively and in userspace. --- bin/solid.pill | 4 +- pkg/arvo/sys/hoon.hoon | 132 ++++++++++++++++++++++++++++++++++++++--- 2 files changed, 127 insertions(+), 9 deletions(-) diff --git a/bin/solid.pill b/bin/solid.pill index f0bd23e6d..d9c3c21d6 100644 --- a/bin/solid.pill +++ b/bin/solid.pill @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:63c31ab63feda55e69a5759411bcc3d4b762a158ab0e416dd2265f7661734032 -size 8933534 +oid sha256:b9199f3c40f1f96ec926d6823f59eeb1d8d174a7d6d5f167898872dc20054ddb +size 8970828 diff --git a/pkg/arvo/sys/hoon.hoon b/pkg/arvo/sys/hoon.hoon index 4b11fe2fb..d9e44e504 100644 --- a/pkg/arvo/sys/hoon.hoon +++ b/pkg/arvo/sys/hoon.hoon @@ -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)] @@ -10194,6 +10199,119 @@ {* * ~} [dov $(dom l.dom)] {* * *} [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.{}" + ~_ =/ extra ~(tap in (~(dif in ~(key by dab)) ~(key by u.dag))) + leaf+"extra.{}" + ~_ =/ have ~(tap in ~(key by dab)) + leaf+"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 @@ -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)] -- ::