ilyakooo0/urbit
1
0
Fork 0
mirror of https://github.com/ilyakooo0/urbit.git synced 2024-12-01 03:23:09 +03:00
Code Issues Packages Projects Releases Wiki Activity

hoon: extend gol check through cores

Browse Source 
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.
This commit is contained in:
Philip Monk 2019-11-08 12:53:03 -08:00 committed by Jared Tobin
parent d557ea87dc
commit e43036d748
No known key found for this signature in database
GPG Key ID: 0E4647D58F8A69E4
2 changed files with 127 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
bin/solid.pill
View File

@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
oid sha256:63c31ab63feda55e69a5759411bcc3d4b762a158ab0e416dd2265f7661734032
size 8933534
oid sha256:b9199f3c40f1f96ec926d6823f59eeb1d8d174a7d6d5f167898872dc20054ddb
size 8970828

132
pkg/arvo/sys/hoon.hoon
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)]
--
::