@@ -874,7 +874,7 @@
874874 %'~[' %'|=(' %'$-(' :: openers
875875 %'%/' %'/' :: paths
876876 %'+' %'`' %'=' :: pair, unit, face
877− %'*' %'?' :: noun, loobean mold
877+ %'*' %'?' %'_' :: noun, loobean, type hole
878878 %'++' %'+$' %'|=' %'|$' :: runes
879879 %'^-' %'~&' %'?-' %'!!' :: runes
880880 %'/-' %'/%' %'/=' :: imports
@@ -1016,6 +1016,7 @@
10161016 [%const at=span =lit] :: ~ %add %.y
10171017 [%ref at=span names=(list term)] :: state item.todo
10181018 [%tvar at=span name=@t] :: M
1019+ [%hole at=span ~] :: _
10191020 [%path at=span segs=(list pseg)] :: / /todos /todo/[id=@ud]
10201021 [%apply at=span ref=(list term) args=(list shape)] :: (list @t)
10211022 [%cell at=span fields=(list field)] :: [text=@t done=?]
@@ -1024,9 +1025,9 @@
10241025 [%generic at=span vars=(list @t) body=shape] :: +$ name |$ [M] …
10251026 ==
10261027::
1027−:: +pseg: a path mold's segment, a knot or [name=aura]
1028+:: +pseg: a path mold's segment, a knot, [name=aura], or [name=_]
10281029::
1029−+$ pseg $%([%knot p=@ta] [%typed at=span name=term aura=@ta])
1030++$ pseg $%([%knot p=@ta] [%typed at=span name=term aura=@ta] [%inferred at=span name=term hole-at=span])
10301031::
10311032+| %api
10321033::
@@ -1295,6 +1296,7 @@
12951296 (emit 1 %'=')
12961297 ?: =('`' a) (emit 1 %'`')
12971298 ?: =('*' a) (emit 1 %'*')
1299+ ?: =('_' a) (emit 1 %'_')
12981300 ?: =('~' a)
12991301 ?: =('[' b) (emit 2 %'~[')
13001302 ?: =('&' b) (emit 2 %'~&')
@@ -1670,14 +1672,14 @@
16701672:: What may begin each place the parser reads (section 3, Errors):
16711673:: an expression a-z 0-9 " ( [ ~ % / ` | ^ ? !
16721674:: an operand a-z 0-9 " ( [ ~ % / ` | !
1673−:: a mold a-z A-Z @ * ! ? ~ % / ( [ $
1675+:: a mold a-z A-Z @ * ! ? ~ % / ( [ $ _
16741676:: a pattern a-z 0-9 " ~ % * [
16751677:: and what may go tight after an operand: . ( + = after a name, a
16761678:: closer ) ] }, or the : of a comment
16771679::
16781680++ expr-mask 0x57ff.ffff.4800.0000.83ff.8126.0000.0000
16791681++ operand-mask 0x57ff.ffff.0800.0000.03ff.8126.0000.0000
1680−++ mold-mask 0x47ff.fffe.0fff.ffff.8000.8532.0000.0000
1682+++ mold-mask 0x47ff.fffe.8fff.ffff.8000.8532.0000.0000
16811683++ bar-mask 0x1000.0000.0000.0000.0000.0000.0000.0000
16821684++ pattern-mask 0x47ff.fffe.0800.0000.03ff.0424.0000.0000
16831685++ after-mask 0x2000.0000.2000.0000.2400.4b00.0000.0000
@@ -2107,6 +2109,7 @@
21072109 ?- -.s
21082110 %knot (weld "/" (trip p.s))
21092111 %typed "/[{(trip name.s)}=@{(trip aura.s)}]"
2112+ %inferred "/[{(trip name.s)}=_]"
21102113 ==
21112114::
21122115++ show-tvars
@@ -2318,6 +2321,7 @@
23182321 %const (nod "const" at.s (show-lit lit.s) ~)
23192322 %ref (nod "ref" at.s (show-names names.s) ~)
23202323 %tvar (nod "tvar" at.s (trip name.s) ~)
2324+ %hole (nod "hole" at.s "" ~)
23212325 %path (nod "path" at.s (show-psegs segs.s) ~)
23222326 %apply (nod "apply" at.s (show-names ref.s) (turn args.s sexp-shape))
23232327 %cell (nod "cell" at.s "" (turn fields.s sexp-field))
@@ -3842,6 +3846,7 @@
38423846 %'*' [%& [%noun at.t ~] t.ts]
38433847 %'!!' [%& [%void at.t ~] t.ts]
38443848 %'?' [%& [%flag at.t ~] t.ts]
3849+ %'_' [%& [%hole at.t ~] t.ts]
38453850 [%name *] [%& [%ref at.t ~[p.lex.t]] t.ts]
38463851 [%wing *] [%& [%ref at.t p.lex.t] t.ts]
38473852 [%tvar *] [%& [%tvar at.t p.lex.t] t.ts]
@@ -4058,7 +4063,7 @@
40584063 ?: &(?=(^ nex) tight.i.nex) (bad nex "a path segment")
40594064 (bad-space i.after nex "a path segment")
40604065 ::
4061− :: +read-pseg: a path mold's segment, a knot or [name=aura] with no
4066+ :: +read-pseg: a path mold's knot, [name=aura], or [name=_] with no
40624067 :: spaces, and where it ends
40634068 ::
40644069 ++ read-pseg
@@ -4075,13 +4080,16 @@
40754080 ?: |(?=(~ r2) !tight.i.r2) (bad-space i.r1 r2 "`=`")
40764081 ?. ?=([[* * %'='] *] r2) (bad-in r2 "`=`" tis-mask)
40774082 =/ r3=(list token) t.r2
4078− ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura")
4079− ?. ?=([[* * [%aura *]] *] r3) (bad-in r3 "an aura" pat-mask)
4083+ ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura or type hole")
4084+ ?. ?=([[* * ?([%aura *] %'_')] *] r3) (bad-in r3 "an aura or type hole" (con pat-mask (bex 95)))
40804085 =/ r4=(list token) t.r3
40814086 ?: |(?=(~ r4) !tight.i.r4) (bad-space i.r3 r4 "`]`")
40824087 ?. ?=([[* * %']'] *] r4) (bad-in r4 "`]`" ser-mask)
40834088 =/ at=span [beg.at.op end.at.i.r4]
4084− [%& [[%typed at p.lex.i.r1 p.lex.i.r3] end.at.i.r4] t.r4]
4089+ =/ seg=pseg
4090+ ?: ?=(%'_' lex.i.r3) [%inferred at p.lex.i.r1 at.i.r3]
4091+ [%typed at p.lex.i.r1 p.lex.i.r3]
4092+ [%& [seg end.at.i.r4] t.r4]
40854093 --
40864094::
40874095+| %span-check
@@ -4465,6 +4473,7 @@
44654473 %const [%const at.s ~[%lit] %one ~]
44664474 %ref [%ref at.s ~[%name %wing] %one ~]
44674475 %tvar [%tvar at.s ~[%tvar] %one ~]
4476+ %hole [%hole at.s ~[%'_'] %one ~]
44684477 %apply [%apply at.s ~[%'('] %shut (turn args.s outline-shape)]
44694478 %cell [%cell at.s ~[%'['] %shut (turn fields.s outline-sample)]
44704479 ::
@@ -4473,8 +4482,11 @@
44734482 %+ murn segs.s
44744483 |= g=pseg
44754484 ^- (unit outline)
4476− ?. ?=(%typed -.g) ~
4477− `[%typed at.g ~[%'['] %shut ~]
4485+ ?- -.g
4486+ %knot ~
4487+ %typed `[%typed at.g ~[%'['] %shut ~]
4488+ %inferred `[%typed at.g ~[%'['] %shut ~[[%hole hole-at.g ~[%'_'] %one ~]]]
4489+ ==
44784490 [%path at.s ~[%'/'] %run ks]
44794491 ::
44804492 %union
@@ -4534,6 +4546,8 @@
45344546 [%path [1 9] [1 9] [1 21]]
45354547 [%face [1 7] [1 7] [1 21]]
45364548 ==
4549+ :: an inferred path aura's hole spanning its = as well
4550+ ['+$ x /a/[id=_]' ~[[%hole [1 13] [1 12] [1 14]]]]
45374551 :: an import's path cut short
45384552 ['/= c /ui/c' ~[[%jibb [1 1] [1 1] [1 11]]]]
45394553 :: brackets that close with the deeper lines, cut at their line's
@@ -4600,6 +4614,20 @@
46004614:: from their display name. Generic cases must be disjoint for all arguments.
46014615:: Unnamed union printing is informational; it is not Jibb syntax.
46024616::
4617+:: `proj` is a reserved, type-directed operation, not an ordinary gate.
4618+:: The supported fragment selects uniquely faced fields from a known record
4619+:: in source order (reordering is a doc question). It records the original
4620+:: call, source and target types, and source axes with its definition;
4621+:: A single selected field keeps its face and uses one source axis.
4622+:: Checked module interfaces retain that evidence and their source, including
4623+:: the private prelude dependency. A later lowerer must replace the call by
4624+:: an inline gate applied to the operand once; no lowering is implemented yet.
4625+:: Ordinary fits never insert a projection. Unknown or variable-origin record
4626+:: spines, implicit narrowing inside selected fields, and projections in
4627+:: recursive groups remain unsupported. Directional fits bound faced-spine
4628+:: proofs to fewer than 1,024 cells; the projection planner has a separate
4629+:: 4,096-step bound. These are inference limits, not language limits.
4630+::
46034631+$ itype
46044632 $~ [%var 0]
46054633 $% [%var id=@ud]
@@ -4608,10 +4636,12 @@
46084636 [%atom aura=@ta]
46094637 [%any-atom ~]
46104638 [%flag ~]
4639+ [%noun ~]
46114640 [%tag id=@ud literal=lit constructor=?]
46124641 [%const literal=lit]
46134642 [%collection name=term args=(list itype)]
46144643 [%recursive module=term name=term label=(unit @t)]
4644+ [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
46154645 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46164646 [%face name=term body=itype]
46174647 [%fn sample=itype product=itype]
@@ -4661,10 +4691,12 @@
46614691 %atom |
46624692 %any-atom |
46634693 %flag |
4694+ %noun |
46644695 %tag =(n id.t)
46654696 %const |
46664697 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
46674698 %recursive |
4699+ %jrec |
46684700 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
46694701 %face $(t body.t)
46704702 %fn |($(t sample.t) $(t product.t))
@@ -4683,6 +4715,8 @@
46834715 =. a (itype-walk a sub)
46844716 =. b (itype-walk b sub)
46854717 ?: =(a b) `sub
4718+ ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4719+ ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
46864720 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
46874721 ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
46884722 ?: &(?=(%union -.a) ?=(%union -.b))
@@ -4757,10 +4791,12 @@
47574791 %atom |
47584792 %any-atom &
47594793 %flag |
4794+ %noun |
47604795 %tag |
47614796 %const |
47624797 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
47634798 %recursive |
4799+ %jrec |
47644800 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
47654801 %face $(t body.t)
47664802 %fn |($(t sample.t) $(t product.t))
@@ -4827,10 +4863,12 @@
48274863 %atom &
48284864 %any-atom &
48294865 %flag &
4866+ %noun |
48304867 %tag &
48314868 %const &
48324869 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
48334870 %recursive |
4871+ %jrec |
48344872 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
48354873 %face $(typ body.typ)
48364874 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4916,6 +4954,8 @@
49164954 %cell &
49174955 %union &
49184956 %recursive &
4957+ %jrec &
4958+ %noun &
49194959 %collection &
49204960 %face $(t body.t)
49214961 %fn |($(t sample.t) $(t product.t))
@@ -4987,6 +5027,7 @@
49875027 ^- ?
49885028 ?- -.t
49895029 %recursive &
5030+ %jrec &
49905031 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
49915032 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
49925033 %face $(t body.t)
@@ -5000,6 +5041,7 @@
50005041 ^- ?
50015042 ?- -.t
50025043 %recursive ?=(~ label.t)
5044+ %jrec ?=(~ label.t)
50035045 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
50045046 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
50055047 %face $(t body.t)
@@ -5050,11 +5092,39 @@
50505092++ itype-fit
50515093 |= [actual=itype expected=itype sub=isub next=@ud]
50525094 ^- ifit
5095+ (itype-fit-inner actual expected sub next | |)
5096+++ itype-fit-inner
5097+ |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5098+ ^- ifit
5099+ ?: &(!skip-width ?=(%cell -.actual) ?=(%cell -.expected) |((width-spine-exhausted actual 1.024) (width-spine-exhausted expected 1.024)))
5100+ [%unknown ~]
5101+ =/ known=(unit [source=iwfields target=iwfields])
5102+ ?: skip-width ~
5103+ (width-known-shape actual expected sub)
5104+ =/ too-wide=? ?~(known | (gth (lent order.source.u.known) (lent order.target.u.known)))
5105+ ?: too-wide [%unknown ~]
5106+ =/ spine-checked=? |(spine-proof ?=(^ known))
50535107 =/ uncertain=?
50545108 |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5109+ =/ actual-open=?
5110+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
50555111 =. actual (itype-walk actual sub)
50565112 =. expected (itype-walk expected sub)
50575113 ?: =(actual expected) [%ok sub next]
5114+ :: Any value can be used where a noun is expected. An unresolved
5115+ :: bare tag is fixed as a constant; a constructor still needs a gate.
5116+ ?: ?=(%noun -.expected)
5117+ ?: ?=(%tag -.actual)
5118+ ?: constructor.actual [%unknown ~]
5119+ [%ok [[id.actual expected] sub] next]
5120+ [%ok sub next]
5121+ :: An arbitrary noun is not known to fit a narrower type.
5122+ ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5123+ ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5124+ ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5125+ ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
5126+ ?:(&(=(at.actual at.expected) =(name.actual name.expected) =(head.actual head.expected) =(aura.actual aura.expected) =(tail.actual tail.expected)) [%ok sub next] [%bad ~])
5127+ ?: &(|(?=(%jrec -.actual) ?=(%jrec -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
50585128 ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
50595129 ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
50605130 ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
@@ -5066,6 +5136,19 @@
50665136 =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
50675137 ?^ unified [%ok u.unified next]
50685138 [%unknown ~]
5139+ :: A known union can instantiate an unconstrained sample directly;
5140+ :: preserve unknown results for variable-bound union origins.
5141+ ?: &(!actual-open ?=(%union -.actual) ?=(%var -.expected))
5142+ ?~ origin.actual [%unknown ~]
5143+ =/ normalized=itype (itype-normalize actual sub)
5144+ ?: |((itype-has-tag normalized) (itype-has-recursive normalized) (itype-has-any-atom actual sub)) [%unknown ~]
5145+ =/ unified=(unit isub) (itype-unify actual expected sub)
5146+ ?~ unified [%unknown ~]
5147+ [%ok u.unified next]
5148+ :: A concrete union value in a tuple may acquire the expected field's
5149+ :: face. A variable-bound union still needs face propagation support.
5150+ ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5151+ $(expected body.expected)
50695152 ?: ?=(%union -.actual) [%unknown ~]
50705153 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
50715154 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -5084,6 +5167,10 @@
50845167 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
50855168 ?. ?=(%ok -.trial) trial
50865169 [%ok [[id.actual expected] sub.trial] next.trial]
5170+ :: Zero may be the empty list. A nested cell fit lacks the context
5171+ :: needed to resolve it here, so do not report a definite mismatch.
5172+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5173+ [%unknown ~]
50875174 ?: ?=(%const -.expected)
50885175 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
50895176 ?: ?=(%atom -.expected)
@@ -5101,6 +5188,8 @@
51015188 [%ok u.u next]
51025189 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
51035190 ?: ?=(%face -.expected) $(expected body.expected)
5191+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5192+ [%unknown ~]
51045193 ?: ?=(%const -.expected)
51055194 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
51065195 ?: ?=(%atom -.expected)
@@ -5130,9 +5219,9 @@
51305219 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
51315220 [%bad ~]
51325221 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5133− =/ first=ifit $(actual hed.actual, expected hed.expected)
5222+ =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
51345223 ?. ?=(%ok -.first) first
5135− $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
5224+ $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
51365225 :: A field may add a face to an occurrence of the very same type
51375226 :: variable. Binding that variable to a face around itself would fail
51385227 :: the occurs check, but its underlying type has already matched.
@@ -5154,9 +5243,9 @@
51545243 [%ok u.unified next]
51555244 ?: &(?=(%face -.actual) ?=(%face -.expected))
51565245 ?. =(name.actual name.expected) [%bad ~]
5157− $(actual body.actual, expected body.expected)
5158− ?: ?=(%face -.actual) $(actual body.actual)
5159− ?: ?=(%face -.expected) $(expected body.expected)
5246+ $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
5247+ ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
5248+ ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
51605249 ?: (itype-face-asym actual expected sub) [%unknown ~]
51615250 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
51625251 [%unknown ~]
@@ -5232,7 +5321,10 @@
52325321+$ ischeme [typ=itype vars=(list @ud)]
52335322+$ ienv (list [name=term scheme=ischeme])
52345323+$ imold-types (list [name=term template=ischeme])
5235−+$ ifile [values=ienv molds=imold-types at=path]
5324++$ iderived [name=term agent=term mark=term]
5325++$ iwidth-definition [name=term original=expr typ=itype sub=isub projections=(list iwprojection)]
5326++$ iwidth-dependency [at=path source=(unit @t) definitions=(list iwidth-definition)]
5327++$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t)]
52365328+$ ijimports (list [face=term interface=ifile])
52375329+$ icap [name=@t id=@ud at=span]
52385330+$ icaps (list icap)
@@ -5242,7 +5334,100 @@
52425334:: This core has no Ford dependencies; unrecognized payloads fail closed.
52435335+$ iexternals (list [module=term name=term result=*])
52445336+$ imark-externals (list [mark=term result=*])
5245−+$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile)]
5337+:: Hole obligations survive discarded expressions until their owning
5338+:: definition has inferred; their source spans support unresolved reports.
5339++$ ihole [id=@ud at=span]
5340+:: Recursive-mold unfolding spends fuel in the threaded inference state.
5341+:: Retries can restart from an earlier state, so this bounds an attempt,
5342+:: not all parsing or module-checking work.
5343+:: Experimental: only closed, uniquely faced records have known axes.
5344++$ iwfield [name=term axis=@ud typ=itype]
5345++$ iwfields [order=(list iwfield) index=(map term iwfield)]
5346++$ iwstep [name=term axis=@ud]
5347++$ iwidth-result [steps=(list iwstep) sub=isub next=@ud]
5348++$ iwprojection [at=span original=expr source=itype target=itype steps=(list iwstep)]
5349+++ width-scan
5350+ |= [typ=itype sub=isub axis=@ud fuel=@ud]
5351+ ^- (unit iwfields)
5352+ =/ order=(list iwfield) ~
5353+ =/ index=(map term iwfield) *(map term iwfield)
5354+ |-
5355+ ?: =(0 fuel) ~
5356+ ?: |(?=(%var -.typ) ?=(%avar -.typ) ?=(%nvar -.typ)) ~
5357+ ?: ?=(%face -.typ)
5358+ =/ entry=iwfield [name.typ axis body.typ]
5359+ ?: ?=(^ (~(get by index) name.entry)) ~
5360+ `[(flop [entry order]) (~(put by index) name.entry entry)]
5361+ ?. ?=(%cell -.typ) ~
5362+ =/ head=itype hed.typ
5363+ ?: |(?=(%var -.head) ?=(%avar -.head) ?=(%nvar -.head)) ~
5364+ ?. ?=(%face -.head) ~
5365+ =/ entry=iwfield [name.head (mul 2 axis) body.head]
5366+ ?: ?=(^ (~(get by index) name.entry)) ~
5367+ $(typ tal.typ, axis +((mul 2 axis)), fuel (dec fuel), order [entry order], index (~(put by index) name.entry entry))
5368+++ width-in-order
5369+ |= [source=(list iwfield) target=(list iwfield)]
5370+ ^- ?
5371+ ?~ target &
5372+ ?~ source |
5373+ ?: =(name.i.source name.i.target) $(source t.source, target t.target)
5374+ $(source t.source)
5375+++ width-fit-fields
5376+ |= [source=(map term iwfield) target=(list iwfield) sub=isub next=@ud]
5377+ ^- (unit iwidth-result)
5378+ ?~ target `[~ sub next]
5379+ =/ found=(unit iwfield) (~(get by source) name.i.target)
5380+ ?~ found ~
5381+ =/ fit=ifit (itype-fit typ.u.found typ.i.target sub next)
5382+ ?. ?=(%ok -.fit) ~
5383+ =/ rest=(unit iwidth-result) $(target t.target, sub sub.fit, next next.fit)
5384+ ?~ rest ~
5385+ `[[[name.i.target axis.u.found] steps.u.rest] sub.u.rest next.u.rest]
5386+++ width-spine-exhausted
5387+ |= [t=itype fuel=@ud]
5388+ ^- ?
5389+ ?: =(0 fuel) &
5390+ ?. ?=(%cell -.t) |
5391+ ?. ?=(%face -.hed.t) |
5392+ $(t tal.t, fuel (dec fuel))
5393+++ width-known-shape
5394+ |= [actual=itype expected=itype sub=isub]
5395+ ^- (unit [source=iwfields target=iwfields])
5396+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5397+ =/ source=(unit iwfields) (width-scan actual sub 1 1.024)
5398+ =/ target=(unit iwfields) (width-scan expected sub 1 1.024)
5399+ ?~ source ~
5400+ ?~ target ~
5401+ `[u.source u.target]
5402+::
5403+++ width-shape
5404+ |= [actual=itype expected=itype sub=isub]
5405+ ^- (unit [source=iwfields target=iwfields])
5406+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5407+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5408+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5409+ ?~ source ~
5410+ ?~ target ~
5411+ ?. (gth (lent order.u.source) (lent order.u.target)) ~
5412+ `[u.source u.target]
5413+++ width-proj-shape
5414+ |= [actual=itype expected=itype sub=isub]
5415+ ^- (unit [source=iwfields target=iwfields])
5416+ ?. &(|(?=(%cell -.actual) ?=(%face -.actual)) |(?=(%cell -.expected) ?=(%face -.expected))) ~
5417+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5418+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5419+ ?~ source ~
5420+ ?~ target ~
5421+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
5422+ `[u.source u.target]
5423+::
5424+++ width-project
5425+ |= [shape=[source=iwfields target=iwfields] sub=isub next=@ud]
5426+ ^- (unit iwidth-result)
5427+ ?. (width-in-order order.source.shape order.target.shape) ~
5428+ (width-fit-fields index.source.shape order.target.shape sub next)
5429+::
5430++$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile) holes=(list ihole) jrec-fuel=@ud projections=(list iwprojection)]
52465431+$ idiag [msg=tape sites=(list [at=span note=tape])]
52475432+$ iresult (each [typ=itype state=istate] idiag)
52485433+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5278,6 +5463,8 @@
52785463:: generalize an aura from its sample, which requires constraint analysis
52795464:: beyond this fragment; leave those cases unresolved.
52805465::
5466+:: This helper only controls decimal defaulting in visible types. A noun
5467+:: may contain gates and is not proof of a gate-free value.
52815468++ itype-has-gate
52825469 |= t=itype
52835470 ^- ?
@@ -5285,6 +5472,7 @@
52855472 %fn &
52865473 %cell |($(t hed.t) $(t tal.t))
52875474 %recursive |
5475+ %jrec |
52885476 %collection (lien args.t |=(c=itype (itype-has-gate c)))
52895477 %face $(t body.t)
52905478 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5296,6 +5484,7 @@
52965484 %atom |
52975485 %any-atom |
52985486 %flag |
5487+ %noun |
52995488 ==
53005489::
53015490++ default-decimals
@@ -5310,6 +5499,90 @@
53105499 * t
53115500 ==
53125501::
5502+:: A hole is solved only by a fully determined type or a written
5503+:: in-scope type variable. Ordinary fresh variables are not evidence.
5504+:: Compare representatives after substitution, since unification can
5505+:: orient a written capital toward the hole rather than the reverse.
5506+++ hole-variable-id
5507+ |= t=itype
5508+ ^- (unit @ud)
5509+ ?- -.t
5510+ %var `id.t
5511+ %avar `id.t
5512+ %nvar `id.t
5513+ %tag `id.t
5514+ * ~
5515+ ==
5516+++ hole-same-variable
5517+ |= [a=itype b=itype]
5518+ ^- ?
5519+ =/ x=(unit @ud) (hole-variable-id a)
5520+ ?~ x |
5521+ =/ y=(unit @ud) (hole-variable-id b)
5522+ ?~ y |
5523+ =(u.x u.y)
5524+++ hole-known
5525+ |= [t=itype state=istate]
5526+ ^- ?
5527+ =. t (itype-walk t sub.state)
5528+ ?- -.t
5529+ ?(%var %avar %nvar)
5530+ ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
5531+ (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
5532+ %tag |
5533+ %any-atom &
5534+ %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5535+ %collection (levy args.t |=(c=itype (hole-known c state)))
5536+ %face $(t body.t)
5537+ %fn &($(t sample.t) $(t product.t))
5538+ %cell &($(t hed.t) $(t tal.t))
5539+ * &
5540+ ==
5541+++ default-hole-numbers
5542+ |= [all=(list ihole) prior=(list ihole) state=istate env=ienv permit=?]
5543+ ^- istate
5544+ :: Do not default a named capital or a variable captured from env.
5545+ ?. permit state
5546+ ?: =(all prior) state
5547+ ?~ all state
5548+ =/ t=itype (itype-walk [%var id.i.all] sub.state)
5549+ =/ free=(list @ud) (free-env-vars env sub.state)
5550+ =? state &(?=(%nvar -.t) !(hole-known t state) !(lien free |=(id=@ud =(id id.t))))
5551+ state(sub [[id.t [%atom %ud]] sub.state])
5552+ $(all t.all)
5553+::
5554+:: Only obligations created inside this definition belong to it.
5555+++ holes-created
5556+ |= [all=(list ihole) prior=(list ihole)]
5557+ ^- (list ihole)
5558+ ?: =(all prior) ~
5559+ ?~ all ~
5560+ [i.all $(all t.all)]
5561+++ hole-uncertain
5562+ |= [t=itype state=istate]
5563+ ^- ?
5564+ =. t (itype-walk t sub.state)
5565+ ?- -.t
5566+ ?(%tag %nvar %avar) !(hole-known t state)
5567+ %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5568+ %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5569+ %face $(t body.t)
5570+ %fn |($(t sample.t) $(t product.t))
5571+ %cell |($(t hed.t) $(t tal.t))
5572+ * |
5573+ ==
5574+::
5575+++ unresolved-hole
5576+ |= [all=(list ihole) prior=(list ihole) state=istate]
5577+ ^- (unit idiag)
5578+ =/ work=(list ihole) (flop (holes-created all prior))
5579+ |-
5580+ ?~ work ~
5581+ ?: (hole-known [%var id.i.work] state) $(work t.work)
5582+ ?: (hole-uncertain [%var id.i.work] state)
5583+ `["type hole needs unsupported inference" ~[[at.i.work "type hole"]]]
5584+ `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
5585+::
53135586++ itype-vars
53145587 |= t=itype
53155588 ^- (list @ud)
@@ -5320,10 +5593,12 @@
53205593 %atom ~
53215594 %any-atom ~
53225595 %flag ~
5596+ %noun ~
53235597 %tag ~
53245598 %const ~
53255599 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
53265600 %recursive ~
5601+ %jrec ~
53275602 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
53285603 %face $(t body.t)
53295604 %fn (weld $(t sample.t) $(t product.t))
@@ -5358,10 +5633,12 @@
53585633 %atom t
53595634 %any-atom t
53605635 %flag t
5636+ %noun t
53615637 %tag t
53625638 %const t
53635639 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
53645640 %recursive t
5641+ %jrec t
53655642 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
53665643 %face [%face name.t $(t body.t)]
53675644 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5381,10 +5658,12 @@
53815658 %atom |
53825659 %any-atom |
53835660 %flag |
5661+ %noun |
53845662 %tag |
53855663 %const |
53865664 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
53875665 %recursive |
5666+ %jrec |
53885667 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
53895668 %face $(t body.t)
53905669 %fn |($(t sample.t) $(t product.t))
@@ -5487,6 +5766,11 @@
54875766 ?. ?=([%ref @ @] node) ~
54885767 ?. &(=(module +<.node) =(name +>.node)) ~
54895768 `[[%unknown ~] &]
5769+ %apply
5770+ ?. ?=([%apply %list [* ~]] node) ~
5771+ =/ item $(node -.+>.node)
5772+ ?~ item ~
5773+ `[[%or ~[[%atom `0] [%cell pat.u.item [%unknown ~]]]] has.u.item]
54905774 %face
54915775 ?. ?=([%face @ *] node) ~
54925776 ?. (jibb-face-name +<.node) ~
@@ -5541,6 +5825,10 @@
55415825 %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
55425826 %fork (imported-faces-valid-list +.node)
55435827 %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
5828+ %named
5829+ ?. ?=([%named @ @ *] node) |
5830+ =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
5831+ (imported-faces-valid body.n)
55445832 ==
55455833::
55465834++ imported-faces-valid-list
@@ -5572,7 +5860,19 @@
55725860 ^- (unit itype)
55735861 ?@ node ~
55745862 ?+ -.node ~
5863+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
55755864 %atom
5865+ :: A Hoon loobean singleton is one of the two Jibb loobeans.
5866+ ?: ?=([%atom %f [~ @]] node)
5867+ =/ value=@ +>+.node
5868+ ?. |(=(value 0) =(value 1)) ~
5869+ =/ printed=@t ?:(=(value 0) '%.y' '%.n')
5870+ `[%const [%loobean %f value printed]]
5871+ :: Hoon's null singleton is the same noun as Jibb's `~` mold.
5872+ :: Other non-term singleton atoms remain unsupported here.
5873+ ?: ?=([%atom %n [~ @]] node)
5874+ ?. =(0 +>+.node) ~
5875+ `[%const [%null %n 0 '~']]
55765876 ?: ?=([%atom %tas [~ @]] node)
55775877 =/ value=@ +>+.node
55785878 ?. |(=(value 0) (jibb-face-name value)) ~
@@ -5582,6 +5882,15 @@
55825882 =/ aura=@ta (@ta +<.node)
55835883 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
55845884 `[%atom aura]
5885+ %named
5886+ ?. ?=([%named @ @ *] node) ~
5887+ =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
5888+ ?. &((jibb-face-name module.n) (jibb-face-name name.n)) ~
5889+ ?. ?=([%fork *] body.n) ~
5890+ =/ proof=(unit irec-pattern) (rec-pattern body.n (@tas module.n) (@tas name.n))
5891+ ?~ proof ~
5892+ ?. has.u.proof ~
5893+ `[%recursive (@tas module.n) (@tas name.n) `(crip "{(trip name.n)}.{(trip module.n)}")]
55855894 %apply
55865895 ?. ?=([%apply @ *] node) ~
55875896 =/ name=term (@tas +<.node)
@@ -5595,10 +5904,15 @@
55955904 ?. =(arity (lent u.args)) ~
55965905 `[%collection name u.args]
55975906 %fork
5598− =/ cases=(unit (list itype)) (import-to-itypes +.node)
5907+ :: Hoon's ordinary ? mold is the fork of its two %f singletons.
5908+ =/ raw=* +.node
5909+ ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
5910+ `[%flag ~]
5911+ =/ cases=(unit (list itype)) (import-to-itypes raw)
55995912 ?~ cases ~
56005913 ?~ u.cases ~
56015914 ?~ t.u.cases ~
5915+ ?: (import-has-loobean-singleton u.cases) ~
56025916 ?. (import-cases-disjoint u.cases) ~
56035917 `[%union u.cases ~ ~ ~]
56045918 %face
@@ -5617,6 +5931,20 @@
56175931 `[%cell u.left u.right]
56185932 ==
56195933::
5934+++ import-direct-loobean
5935+ |= t=itype
5936+ ^- ?
5937+ ?: ?=(%face -.t) $(t body.t)
5938+ ?: ?=(%union -.t) (import-has-loobean-singleton cases.t)
5939+ ?=([%const [%loobean *]] t)
5940+::
5941+++ import-has-loobean-singleton
5942+ |= cases=(list itype)
5943+ ^- ?
5944+ ?~ cases |
5945+ ?: (import-direct-loobean i.cases) &
5946+ $(cases t.cases)
5947+::
56205948++ import-to-itypes
56215949 |= nodes=*
56225950 ^- (unit (list itype))
@@ -5631,7 +5959,9 @@
56315959 |= typ=itype
56325960 ^- upat
56335961 ?- -.typ
5962+ %noun [%all ~]
56345963 %atom [%atom ~]
5964+ %flag [%or ~[[%atom `0] [%atom `1]]]
56355965 %const [%atom `val.literal.typ]
56365966 %face $(typ body.typ)
56375967 %cell [%cell $(typ hed.typ) $(typ tal.typ)]
@@ -5726,25 +6056,55 @@
57266056 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
57276057 $(molds t.molds)
57286058::
5729−:: Only names exported by this directly imported module are visible through
5730−:: its face. Other origins retain identity but print as unnamed unions.
6059+:: A public non-generic alias names exactly its origin and arguments.
6060+:: Reusing only an origin could print a different generic instantiation.
6061+++ prelude-union-alias
6062+ |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
6063+ ^- (unit term)
6064+ ?^ args ~
6065+ ?~ molds ~
6066+ =/ template=ischeme template.i.molds
6067+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
6068+ ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
6069+ $(molds t.molds)
6070+::
6071+:: Names exported by the directly imported module are visible through its
6072+:: face; a matching prelude alias is also visible without a qualifier.
6073+::
6074+++ jrec-alias
6075+ |= [origin=path name=term molds=imold-types]
6076+ ^- (unit term)
6077+ ?~ molds ~
6078+ =/ template=ischeme template.i.molds
6079+ ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6080+ $(molds t.molds)
57316081::
57326082++ itype-in-import
5733− |= [t=itype iface=ifile face=term]
6083+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
57346084 ^- itype
57356085 ?- -.t
57366086 %union
57376087 =/ label=(unit @t)
57386088 ?~ origin.t ~
57396089 ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
6090+ =/ public=(unit term)
6091+ ?~ prelude ~
6092+ (prelude-union-alias u.origin.t args.t molds.u.prelude)
6093+ ?^ public `u.public
57406094 =/ alias=(unit term) ~
57416095 =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
57426096 =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
57436097 ?~ alias ~
57446098 `(crip "{(trip u.alias)}.{(trip face)}")
5745− [%union (turn cases.t |=(c=itype (itype-in-import c iface face))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face)))]
6099+ [%union (turn cases.t |=(c=itype (itype-in-import c iface face prelude))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
57466100 %recursive [%recursive module.t name.t ~]
5747− %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face)))]
6101+ %jrec
6102+ =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6103+ ?^ public t(label `u.public)
6104+ =/ alias=(unit term) (jrec-alias at.t name.t molds.iface)
6105+ ?~ alias t(label ~)
6106+ t(label `(crip "{(trip u.alias)}.{(trip face)}"))
6107+ %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
57486108 %face [%face name.t $(t body.t)]
57496109 %fn [%fn $(t sample.t) $(t product.t)]
57506110 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5817,9 +6177,46 @@
58176177 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
58186178 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
58196179::
6180+:: Recognize a unique top-level source mold with exactly a null case and a
6181+:: faced atom-headed cell whose faced tail names that same mold. Its Jibb
6182+:: path and name provide nominal identity. Other recursive shapes fail closed;
6183+:: construction and matching expose the proven shape one layer at a time.
6184+++ simple-source-recursive
6185+ |= [name=term sh=shape state=istate]
6186+ ^- (unit itype)
6187+ ?. (lien top-molds.state |=(n=term =(n name))) ~
6188+ =/ original=(unit shape) (find-simple-mold name molds.state)
6189+ ?~ original ~
6190+ ?. =(u.original sh) ~
6191+ ?. ?=(%union -.sh) ~
6192+ =/ cs=(list shape) cases.sh
6193+ ?~ cs ~
6194+ ?~ t.cs ~
6195+ ?^ t.t.cs ~
6196+ ?. ?=(%const -.i.cs) ~
6197+ ?. =(%null form.lit.i.cs) ~
6198+ ?. ?=(%cell -.i.t.cs) ~
6199+ =/ fs=(list field) fields.i.t.cs
6200+ ?~ fs ~
6201+ ?~ t.fs ~
6202+ ?^ t.t.fs ~
6203+ ?. ?=(%face -.i.fs) ~
6204+ ?. ?=(%aura -.shape.i.fs) ~
6205+ ?. !=(0 aura.shape.i.fs) ~
6206+ ?. ?=(%face -.i.t.fs) ~
6207+ ?. !=(name.i.fs name.i.t.fs) ~
6208+ =/ tail=shape shape.i.t.fs
6209+ ?. ?=(%ref -.tail) ~
6210+ ?. =(names.tail ~[name]) ~
6211+ `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6212+::
58206213++ infer-mold-template
58216214 |= [sh=shape state=istate]
58226215 ^- (unit [template=ischeme state=istate])
6216+ =/ direct=(unit itype)
6217+ ?. ?=([@ ~] active.state) ~
6218+ (simple-source-recursive i.active.state sh state)
6219+ ?^ direct `[[u.direct ~] state]
58236220 ?: ?=(%generic -.sh)
58246221 ?~ vars.sh ~
58256222 ?. (distinct-params vars.sh) ~
@@ -5827,17 +6224,19 @@
58276224 =/ out=(unit [typ=itype state=istate])
58286225 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
58296226 ?~ out ~
6227+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
58306228 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
58316229 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
58326230 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
58336231 =/ used=(list @ud) (itype-vars typ.u.out)
58346232 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5835− `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state)]
6233+ `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
58366234 =/ out=(unit [typ=itype state=istate])
58376235 (infer-simple-shape sh state(params ~, in-mold &))
58386236 ?~ out ~
6237+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
58396238 ?: ?=(^ (itype-vars typ.u.out)) ~
5840− `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
6239+ `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
58416240::
58426241:: A direct imported reference may carry definite reader evidence. Only
58436242:: uniquely supplied, declared inputs are used; unsupported data stay generic.
@@ -5940,10 +6339,12 @@
59406339 |= [sh=shape state=istate]
59416340 ^- (unit [typ=itype state=istate])
59426341 ?- -.sh
6342+ %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
59436343 %aura
59446344 ?: =(0 aura.sh) `[[%any-atom ~] state]
59456345 `[[%atom aura.sh] state]
59466346 %flag `[[%flag ~] state]
6347+ %noun `[[%noun ~] state]
59476348 %const
59486349 ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
59496350 `[[%const lit.sh] state]
@@ -5970,7 +6371,7 @@
59706371 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
59716372 ?~ found ~
59726373 ?^ vars.u.found ~
5973− `[(itype-in-import typ.u.found u.iface i.t.names.sh) state]
6374+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
59746375 =/ found=(unit itype)
59756376 (find-imported-mold i.t.names.sh n externals.state surs.state)
59766377 ?~ found ~
@@ -5989,10 +6390,13 @@
59896390 ?~ prelude-entry ~
59906391 ?^ vars.u.prelude-entry ~
59916392 `[typ.u.prelude-entry state]
6393+ =/ direct=(unit itype) (simple-source-recursive n u.found state)
6394+ ?^ direct `[u.direct state]
59926395 =/ out=(unit [typ=itype state=istate])
59936396 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
59946397 ?~ out ~
5995− `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state)]
6398+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
6399+ `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state, holes holes.state)]
59966400 %apply
59976401 ?~ ref.sh ~
59986402 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -6007,7 +6411,7 @@
60076411 ?~ vars.u.template ~
60086412 =/ applied=(unit itype) (template-apply u.template types.u.args)
60096413 ?~ applied ~
6010− `[(itype-in-import u.applied u.iface i.t.ref.sh) state.u.args]
6414+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
60116415 ?: (lien active.state.u.args |=(x=term =(x n))) ~
60126416 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
60136417 ?~ found
@@ -6026,11 +6430,12 @@
60266430 =/ out=(unit [typ=itype state=istate])
60276431 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
60286432 ?~ out ~
6433+ ?^ (unresolved-hole holes.state.u.out holes.state.u.args state.u.out) ~
60296434 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
60306435 ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
60316436 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
60326437 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6033− `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
6438+ `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args, holes holes.state.u.args)]
60346439 %tvar
60356440 =/ param=(unit itype) (iparam-lookup name.sh params.state)
60366441 ?^ param `[u.param state]
@@ -6070,12 +6475,12 @@
60706475 ^- isample-result
60716476 ?- -.s
60726477 %bind
6073− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6478+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
60746479 [%| "sample shadows a name"]
60756480 =/ t=itype [%var next.state]
60766481 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
60776482 %face
6078− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6483+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
60796484 [%| "sample shadows a name"]
60806485 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
60816486 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -6113,8 +6518,8 @@
61136518 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
61146519::
61156520:: Local definitions generalize only variables outside their enclosing
6116−:: environment and explicit-capital scope. Single self-recursive gates
6117−:: use a monomorphic placeholder; mutually recursive groups stay unsupported.
6521+:: environment and explicit-capital scope. Recursive gate groups use
6522+:: monomorphic placeholders while their bodies are checked.
61186523::
61196524+$ ilocal-result (each [env=ienv state=istate] idiag)
61206525++ free-env-vars
@@ -6143,6 +6548,7 @@
61436548 |-
61446549 ?~ ds &
61456550 ?: ?=(%mold -.i.ds) $(ds t.ds)
6551+ ?: =(name.i.ds %proj) |
61466552 ?. (unique-value-name name.i.ds names) |
61476553 ?: ?=(^ (ienv-lookup name.i.ds env)) |
61486554 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -6166,6 +6572,7 @@
61666572 |-
61676573 ?~ locals &
61686574 =/ n=term name.i.locals
6575+ ?: =(n %proj) |
61696576 ?. (unique-value-name n names) |
61706577 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
61716578 ?: (lien marks.state |=(m=term =(n m))) |
@@ -6330,7 +6737,13 @@
63306737 |-
63316738 ?~ ds
63326739 ?~ remaining [%& env state]
6333− ?. progressed [%| ["local definitions need unsupported inference" ~]]
6740+ ?. progressed
6741+ =/ pending=(list def) (flop remaining)
6742+ =/ groups=icomponents (graph-components pending (global-value-names pending))
6743+ =/ grouped=(unit [rest=(list def) env=ienv state=istate])
6744+ (try-local-group pending groups env state)
6745+ ?~ grouped [%| ["local definitions need unsupported inference" ~]]
6746+ $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
63346747 $(ds (flop remaining), remaining ~, progressed |)
63356748 =/ d=def i.ds
63366749 ?> ?=(%value -.d)
@@ -6339,6 +6752,9 @@
63396752 =/ retried=? ?=(%| -.inferred)
63406753 =? inferred retried (infer-recursive-gate d env local-state)
63416754 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6755+ =. state.p.inferred (default-hole-numbers holes.state.p.inferred holes.state state.p.inferred env !(itype-has-gate (itype-normalize typ.p.inferred sub.state.p.inferred)))
6756+ =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
6757+ ?^ hole [%| u.hole]
63426758 =/ merged=(unit [first=icap second=icap])
63436759 (merged-capitals caps.state.p.inferred sub.state.p.inferred)
63446760 ?^ merged
@@ -6354,7 +6770,28 @@
63546770 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
63556771 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
63566772 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6357− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
6773+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
6774+::
6775+:: Try complete cyclic local groups after individual definitions stall.
6776+:: Components with non-gates or unresolved constraints stay unavailable.
6777+::
6778+++ try-local-group
6779+ |= [ds=(list def) groups=icomponents env=ienv state=istate]
6780+ ^- (unit [rest=(list def) env=ienv state=istate])
6781+ ?~ groups ~
6782+ =/ names=(list term) i.groups
6783+ ?. (gth (lent names) 1) $(groups t.groups)
6784+ =/ members=(list def)
6785+ (skim ds |=(d=def &(?=(%value -.d) (lien names |=(n=term =(n name.d))))))
6786+ ?. =((lent members) (lent names)) $(groups t.groups)
6787+ =/ result=ilocal-result (infer-gate-group members env state)
6788+ ?: ?=(%| -.result) $(groups t.groups)
6789+ =/ rest=(list def)
6790+ (skim ds |=(d=def !(lien names |=(n=term =(n name.d)))))
6791+ =/ more=(unit [rest=(list def) env=ienv state=istate])
6792+ $(ds rest, groups t.groups, env env.p.result, state state.p.result)
6793+ ?^ more more
6794+ `[rest env.p.result state.p.result]
63586795::
63596796:: Read only fields of a known record. Unresolved field constraints and
63606797:: ambiguous repeated faces are outside this fragment. Imported record
@@ -6377,17 +6814,29 @@
63776814 ^- iresult
63786815 =/ reverse=(list term) (flop names)
63796816 ?~ reverse [%| ["empty wing" ~]]
6380− =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6381− ?~ scheme [%| ["field access is not supported by partial inference" ~]]
6382− =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
6817+ =/ iface=(unit ifile) (find-jibb-interface i.reverse jimports.state)
63836818 =/ fields=(list term) t.reverse
6819+ ?~ fields [%| ["field access is not supported by partial inference" ~]]
6820+ =/ scheme=(unit ischeme)
6821+ ?~ iface
6822+ (ienv-lookup i.reverse env)
6823+ (ienv-lookup i.fields values.u.iface)
6824+ ?~ scheme
6825+ ?^ iface [%| ["module member is not available to partial inference" ~]]
6826+ [%| ["field access is not supported by partial inference" ~]]
6827+ =/ inst=[typ=itype state=istate]
6828+ ?~ iface (instantiate-scheme u.scheme state)
6829+ =/ imported=ischeme u.scheme
6830+ =. typ.imported (itype-in-import typ.imported u.iface i.reverse prelude.state)
6831+ (instantiate-scheme imported state)
6832+ =/ remaining=(list term) ?~(iface fields t.fields)
63846833 =/ typ=itype typ.inst
63856834 |-
6386− ?~ fields [%& typ state.inst]
6387− =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
6835+ ?~ remaining [%& typ state.inst]
6836+ =/ found=(list itype) (record-fields-named i.remaining typ sub.state.inst)
63886837 ?~ found [%| ["field is not available to partial inference" ~]]
63896838 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6390− $(fields t.fields, typ i.found)
6839+ $(remaining t.remaining, typ i.found)
63916840::
63926841:: Propagate a known union or list through supported loobean, unit and list
63936842:: branches. Empty bodies and groups are transparent; bodies with definitions
@@ -6426,6 +6875,9 @@
64266875 [%| ["branch does not cover both loobeans" ~]]
64276876 =/ subject=iresult (infer-fragment subject.e env state)
64286877 ?: ?=(%| -.subject) subject
6878+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
6879+ ?: ?=(%union -.subject-type)
6880+ [%| ["contextual union-pattern branch is not supported by partial inference" ~]]
64296881 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
64306882 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
64316883 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6439,10 +6891,17 @@
64396891 ?: ?=(%unknown -.fit)
64406892 ?: &(?=(%collection -.expected) =(%list name.expected))
64416893 [%| ["branch list constraint is not supported by partial inference" ~]]
6894+ ?: ?=(%flag -.expected) [%| ["branch loobean constraint is not supported by partial inference" ~]]
64426895 [%| ["branch union constraint is not supported by partial inference" ~]]
64436896 ?: ?=(%bad -.fit)
6897+ =/ missing=(unit idiag) (missing-union-tag e expected sub.state.p.value context)
6898+ ?^ missing [%| u.missing]
6899+ =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
6900+ ?^ nested [%| u.nested]
64446901 ?: &(?=(%collection -.expected) =(%list name.expected))
64456902 [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
6903+ ?: ?=(%flag -.expected)
6904+ [%| ["branch arm does not fit its expected loobean" ~[[context "expected loobean"] [(span-of e) "branch arm"]]]]
64466905 [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
64476906 [%& expected state.p.value(sub sub.fit, next next.fit)]
64486907::
@@ -6507,23 +6966,37 @@
65076966 [%| ["list tail does not fit its expected type" ~[[context (site-type-note "expected list" target sub.state.p.tail)] [(span-of val.i.t.items.e) (site-type-note "list tail" typ.p.tail sub.state.p.tail)]]]]
65086967 [%& target state.p.tail(sub sub.fit, next next.fit)]
65096968::
6969+++ infer-open-list-items
6970+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6971+ ^- iresult
6972+ ?~ items [%& expected state]
6973+ =/ target=itype (itype-walk expected sub.state)
6974+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6975+ ?: ?=(%| -.value) value
6976+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6977+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6978+ ?: ?=(%bad -.fit)
6979+ ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
6980+ [%| ["list item widening is not supported by partial inference" ~]]
6981+ [%| ["list items do not have compatible types" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
6982+ ?: (itype-has-tag (itype-normalize expected sub.fit))
6983+ [%| ["list item needs context in partial inference" ~]]
6984+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
6985+::
65106986++ infer-list-items
65116987 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
65126988 ^- iresult
65136989 ?~ items [%& expected state]
65146990 =/ target=itype (itype-walk expected sub.state)
6515− =/ value=iresult
6516− ?: &(?=(%union -.target) (context-union-branch i.items))
6517− (infer-union-context i.items target env state context)
6518− ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch i.items))
6519− (infer-union-context i.items target env state context)
6520− ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression i.items))
6521− (infer-list-context i.items target env state context)
6522− (infer-fragment i.items env state)
6991+ =/ value=iresult (infer-call-context-arg i.items target env state context)
65236992 ?: ?=(%| -.value) value
65246993 =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
65256994 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
65266995 ?: ?=(%bad -.fit)
6996+ =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
6997+ ?^ missing [%| u.missing]
6998+ =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
6999+ ?^ nested [%| u.nested]
65277000 [%| ["list item does not fit its expected type" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
65287001 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
65297002::
@@ -6616,7 +7089,7 @@
66167089 [%| ["list branch pattern is not supported by partial inference" ~]]
66177090 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
66187091 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6619− ?: |(=(head.u.binder tail.u.binder) ?=(^ (ienv-lookup head.u.binder env)) ?=(^ (ienv-lookup tail.u.binder env)) (lien globals.state |=(n=term |(=(n head.u.binder) =(n tail.u.binder)))))
7092+ ?: |(=(head.u.binder %proj) =(tail.u.binder %proj) =(head.u.binder tail.u.binder) ?=(^ (ienv-lookup head.u.binder env)) ?=(^ (ienv-lookup tail.u.binder env)) (lien globals.state |=(n=term |(=(n head.u.binder) =(n tail.u.binder)))))
66207093 [%| ["pattern binder shadows a name" ~]]
66217094 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
66227095 =/ left=iresult
@@ -6653,7 +7126,7 @@
66537126 [%| ["unit branch pattern is not supported by partial inference" ~]]
66547127 =/ binder=(unit term) ?:(first-empty second-name first-name)
66557128 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
6656− ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
7129+ ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
66577130 [%| ["pattern binder shadows a name" ~]]
66587131 =/ payload=(unit itype) (unit-union-payload typ)
66597132 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -6695,10 +7168,553 @@
66957168 [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
66967169 [%| ["interpolation type needs unsupported inference" ~]]
66977170::
7171+:: Whole-case coverage for a known union. When a pattern may cover only
7172+:: part of a case, finite loobean refinements are tried below; other
7173+:: partial coverage stays unsupported until the general pattern matrix.
7174++$ imatch ?(%full %none %unknown)
7175+++ union-pattern-items
7176+ |= [ps=(list pattern) t=itype]
7177+ ^- imatch
7178+ ?~ ps %unknown
7179+ ?~ t.ps (union-pattern i.ps t)
7180+ =. t ?:(?=(%face -.t) body.t t)
7181+ ?. ?=(%cell -.t)
7182+ ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
7183+ %unknown
7184+ =/ a=imatch (union-pattern i.ps hed.t)
7185+ =/ b=imatch $(ps t.ps, t tal.t)
7186+ ?: |(=(%none a) =(%none b)) %none
7187+ ?:(&(=(%full a) =(%full b)) %full %unknown)
7188+::
7189+++ union-pattern
7190+ |= [p=pattern t=itype]
7191+ ^- imatch
7192+ =. t ?:(?=(%face -.t) body.t t)
7193+ ?- -.p
7194+ %any %full
7195+ %bind %full
7196+ %lit
7197+ ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
7198+ ?: ?=(%cell -.t) %none
7199+ ?: ?=(%flag -.t)
7200+ ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
7201+ %unknown
7202+ %str ?:(?=(%cell -.t) %none %unknown)
7203+ %cell (union-pattern-items items.p t)
7204+ ==
7205+::
7206+++ union-pattern-has-bind
7207+ |= p=pattern
7208+ ^- ?
7209+ ?: ?=(%bind -.p) &
7210+ ?. ?=(%cell -.p) |
7211+ (lien items.p union-pattern-has-bind)
7212+::
7213+++ union-pattern-bind-items
7214+ |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
7215+ ^- (unit ienv)
7216+ ?~ ps ~
7217+ ?~ t.ps (union-pattern-bind i.ps t env globals)
7218+ =. t ?:(?=(%face -.t) body.t t)
7219+ ?. ?=(%cell -.t) ~
7220+ =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
7221+ ?~ first ~
7222+ $(ps t.ps, t tal.t, env u.first)
7223+::
7224+++ union-pattern-bind
7225+ |= [p=pattern t=itype env=ienv globals=(list term)]
7226+ ^- (unit ienv)
7227+ =. t ?:(?=(%face -.t) body.t t)
7228+ ?: ?=(%bind -.p)
7229+ ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
7230+ `[[name.p [t ~]] env]
7231+ ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
7232+ `env
7233+::
7234+:: Split loobean fields into finite refinements for partial patterns.
7235+:: Keep original cases for binder types and preserve whole-case matching
7236+:: before trying refinements. Cap products at 64; unknown, empty or opaque
7237+:: shapes stay unsupported rather than implying complete pattern checking.
7238++$ ifinite [origin=@ud base=itype part=itype]
7239+++ finite-product
7240+ |= [hs=(list itype) ts=(list itype) out=(list itype)]
7241+ ^- (list itype)
7242+ ?~ hs out
7243+ =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
7244+ $(hs t.hs, out (weld rows out))
7245+::
7246+++ finite-type
7247+ |= t=itype
7248+ ^- (unit (list itype))
7249+ ?- -.t
7250+ %flag
7251+ `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
7252+ %face
7253+ =/ body=(unit (list itype)) $(t body.t)
7254+ ?~ body ~
7255+ `(turn u.body |=(x=itype [%face name.t x]))
7256+ %cell
7257+ =/ hed=(unit (list itype)) $(t hed.t)
7258+ ?~ hed ~
7259+ =/ tal=(unit (list itype)) $(t tal.t)
7260+ ?~ tal ~
7261+ ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
7262+ `(finite-product u.hed u.tal ~)
7263+ * `~[t]
7264+ ==
7265+::
7266+++ finite-cases
7267+ |= [xs=(list itype) out=(list ifinite) origin=@ud]
7268+ ^- (unit (list ifinite))
7269+ ?~ xs `out
7270+ =/ parts=(unit (list itype)) (finite-type i.xs)
7271+ ?~ parts ~
7272+ ?: (gth (add (lent out) (lent u.parts)) 64) ~
7273+ =/ rows=(list ifinite) (turn u.parts |=(t=itype [origin i.xs t]))
7274+ $(xs t.xs, out (weld out rows), origin +(origin))
7275+::
7276+++ infer-known-union-whole
7277+ |= [e=expr env=ienv subject=iresult]
7278+ ^- (unit iresult)
7279+ ?> ?=(%branch -.e)
7280+ ?: ?=(%| -.subject) `subject
7281+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7282+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7283+ =/ cases=(list itype) cases.typ
7284+ =/ remaining=(list itype) cases
7285+ =/ arms=(list arm) arms.e
7286+ =/ st=istate state.p.subject
7287+ =/ answer=(unit itype) ~
7288+ |-
7289+ ?~ arms
7290+ ?^ remaining
7291+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7292+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7293+ `[%& u.answer st]
7294+ =/ a=arm i.arms
7295+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7296+ ~
7297+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
7298+ ?~ matching
7299+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
7300+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7301+ `[%| ["union pattern is not supported by partial inference" ~]]
7302+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
7303+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7304+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7305+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
7306+ =/ body=iresult (infer-fragment val.a u.bound st)
7307+ ?: ?=(%| -.body) `body
7308+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7309+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7310+ ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
7311+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
7312+::
7313+++ infer-known-union-context-whole
7314+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
7315+ ^- (unit iresult)
7316+ ?> ?=(%branch -.e)
7317+ ?: ?=(%| -.subject) `subject
7318+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7319+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7320+ =/ cases=(list itype) cases.typ
7321+ =/ remaining=(list itype) cases
7322+ =/ arms=(list arm) arms.e
7323+ =/ st=istate state.p.subject
7324+ =/ answer=(unit itype) ~
7325+ |-
7326+ ?~ arms
7327+ ?^ remaining
7328+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7329+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7330+ `[%& expected st]
7331+ =/ a=arm i.arms
7332+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7333+ ~
7334+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
7335+ ?~ matching
7336+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
7337+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7338+ `[%| ["union pattern is not supported by partial inference" ~]]
7339+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
7340+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7341+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7342+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
7343+ =/ body=iresult (infer-call-context-arg val.a expected u.bound st context)
7344+ ?: ?=(%| -.body) `body
7345+ =/ fit=ifit (itype-fit typ.p.body expected sub.state.p.body next.state.p.body)
7346+ ?: ?=(%unknown -.fit) `[%| ["union branch result constraint is not supported by partial inference" ~]]
7347+ ?: ?=(%bad -.fit)
7348+ =/ missing=(unit idiag) (missing-union-tag val.a expected sub.state.p.body context)
7349+ ?^ missing `[%| u.missing]
7350+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body expected sub.state.p.body next.state.p.body context)
7351+ ?^ nested `[%| u.nested]
7352+ `[%| ["union branch arm does not fit its expected type" ~[[context "expected type"] [(span-of val.a) "branch arm"]]]]
7353+ ?: (itype-has-tag (itype-normalize expected sub.fit))
7354+ `[%| ["union branch result needs context in partial inference" ~]]
7355+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body(sub sub.fit, next next.fit), answer `expected)
7356+::
7357+++ infer-known-union-finite
7358+ |= [e=expr env=ienv subject=iresult expected=(unit [typ=itype context=span])]
7359+ ^- iresult
7360+ ?> ?=(%branch -.e)
7361+ ?: ?=(%| -.subject) subject
7362+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7363+ ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7364+ =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7365+ ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7366+ =/ cases=(list ifinite) u.expanded
7367+ =/ remaining=(list ifinite) cases
7368+ =/ arms=(list arm) arms.e
7369+ =/ st=istate state.p.subject
7370+ =/ answer=(unit itype) ~
7371+ |-
7372+ ?~ arms
7373+ ?^ remaining
7374+ [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
7375+ ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
7376+ ?~ expected [%& u.answer st]
7377+ [%& typ.u.expected st]
7378+ =/ a=arm i.arms
7379+ ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
7380+ [%| ["partial union pattern is not supported by partial inference" ~]]
7381+ =/ matching=(list ifinite) (skim remaining |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7382+ ?~ matching
7383+ ?: (lien cases |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7384+ [%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7385+ [%| ["union pattern is not supported by partial inference" ~]]
7386+ ?: &((union-pattern-has-bind pat.a) (lien t.matching |=(c=ifinite !=(origin.c origin.i.matching))))
7387+ [%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7388+ =/ bound=(unit ienv) (union-pattern-bind pat.a base.i.matching env globals.st)
7389+ ?~ bound [%| ["pattern binder shadows a name" ~]]
7390+ =/ body=iresult
7391+ ?~ expected (infer-fragment val.a u.bound st)
7392+ (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7393+ ?: ?=(%| -.body) body
7394+ ?^ expected
7395+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7396+ ?: ?=(%unknown -.fit) [%| ["union branch result constraint is not supported by partial inference" ~]]
7397+ ?: ?=(%bad -.fit)
7398+ =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7399+ ?^ missing [%| u.missing]
7400+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body typ.u.expected sub.state.p.body next.state.p.body context.u.expected)
7401+ ?^ nested [%| u.nested]
7402+ [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7403+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7404+ [%| ["union branch result needs context in partial inference" ~]]
7405+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body(sub sub.fit, next next.fit), answer `typ.u.expected)
7406+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7407+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7408+ ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
7409+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
7410+::
7411+:: Prove a one-arm record pattern covers a known, non-union subject.
7412+:: Variable or partial matches stay unsupported; binding uses the same
7413+:: scope and original payload types as the existing union matcher.
7414+++ single-structured-pattern
7415+ |= e=expr
7416+ ^- ?
7417+ ?. ?=(%branch -.e) |
7418+ ?~ arms.e |
7419+ ?^ t.arms.e |
7420+ =/ p=pattern pat.i.arms.e
7421+ ?. ?=(%cell -.p) |
7422+ !(levy items.p |=(x=pattern ?=(%bind -.x)))
7423+::
7424+++ infer-single-case-branch
7425+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7426+ ^- iresult
7427+ ?> (single-structured-pattern e)
7428+ ?> ?=(%branch -.e)
7429+ ?> ?=(^ arms.e)
7430+ =/ a=arm i.arms.e
7431+ =/ subject=iresult (infer-fragment subject.e env state)
7432+ ?: ?=(%| -.subject) subject
7433+ =/ st=istate state.p.subject
7434+ =/ typ=itype (itype-normalize typ.p.subject sub.st)
7435+ ?: ?=(%union -.typ) [%| ["single-case pattern needs unsupported inference" ~]]
7436+ ?. =(%full (union-pattern pat.a typ))
7437+ [%| ["single-case pattern needs unsupported inference" ~]]
7438+ =/ bound=(unit ienv) (union-pattern-bind pat.a typ env globals.st)
7439+ ?~ bound [%| ["pattern binder shadows a name" ~]]
7440+ ?~ expected (infer-fragment val.a u.bound st)
7441+ =/ body=iresult (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7442+ ?: ?=(%| -.body) body
7443+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7444+ ?: ?=(%unknown -.fit) [%| ["single-case branch result constraint is not supported by partial inference" ~]]
7445+ ?: ?=(%bad -.fit)
7446+ =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7447+ ?^ missing [%| u.missing]
7448+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body typ.u.expected sub.state.p.body next.state.p.body context.u.expected)
7449+ ?^ nested [%| u.nested]
7450+ [%| ["single-case branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7451+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7452+ [%| ["single-case branch result needs context in partial inference" ~]]
7453+ [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
7454+::
7455+:: This view is used only by pattern analysis, never exported or bound as
7456+:: the subject. Only null plus a two-binder/wildcard cell is supported; its
7457+:: tail keeps the original recursive type. Other patterns fail closed.
7458+++ jrec-match-view
7459+ |= [e=expr subject=iresult]
7460+ ^- iresult
7461+ ?: ?=(%| -.subject) subject
7462+ ?. ?=(%branch -.e) subject
7463+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7464+ ?. ?=(%jrec -.typ) subject
7465+ ?~ arms.e subject
7466+ ?~ t.arms.e subject
7467+ ?^ t.t.arms.e subject
7468+ =/ x=pattern pat.i.arms.e
7469+ =/ y=pattern pat.i.t.arms.e
7470+ =/ empty=? &(?=(%lit -.x) =(%null form.lit.x))
7471+ =/ full=pattern ?:(empty y x)
7472+ ?. |(empty &(?=(%lit -.y) =(%null form.lit.y))) subject
7473+ ?. ?=(%cell -.full) subject
7474+ ?~ items.full subject
7475+ ?~ t.items.full subject
7476+ ?^ t.t.items.full subject
7477+ ?. |(?=(%bind -.i.items.full) ?=(%any -.i.items.full)) subject
7478+ ?. |(?=(%bind -.i.t.items.full) ?=(%any -.i.t.items.full)) subject
7479+ ?: =(0 jrec-fuel.state.p.subject)
7480+ [%| ["recursive mold unfolding needs unsupported inference" ~]]
7481+ =/ nil=itype [%const [%null %n 0 '~']]
7482+ =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
7483+ [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
7484+::
7485+++ infer-known-union-branch-subject
7486+ |= [e=expr env=ienv subject=iresult]
7487+ ^- iresult
7488+ =. subject (jrec-match-view e subject)
7489+ =/ whole=(unit iresult) (infer-known-union-whole e env subject)
7490+ ?~ whole (infer-known-union-finite e env subject ~)
7491+ u.whole
7492+::
7493+++ infer-known-union-branch
7494+ |= [e=expr env=ienv state=istate]
7495+ ^- iresult
7496+ ?> ?=(%branch -.e)
7497+ (infer-known-union-branch-subject e env (infer-fragment subject.e env state))
7498+::
7499+++ infer-known-union-context-subject
7500+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
7501+ ^- iresult
7502+ =. subject (jrec-match-view e subject)
7503+ =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
7504+ ?~ whole (infer-known-union-finite e env subject `[expected context])
7505+ u.whole
7506+::
7507+:: Limit speculative subject inference to wings and shallow calls;
7508+:: grouping is peeled linearly and cannot introduce a nested branch.
7509+++ simple-union-subject-arg
7510+ |= e=expr
7511+ ^- ?
7512+ ?- -.e
7513+ %wing &
7514+ %lit &
7515+ %str !(lien pieces.e |=(p=piece ?=(%expr -.p)))
7516+ * |
7517+ ==
7518+::
7519+++ safe-union-subject
7520+ |= e=expr
7521+ ^- ?
7522+ ?: ?=(%group -.e) $(e inner.e)
7523+ ?: ?=(%wing -.e) &
7524+ ?. ?=(%call -.e) |
7525+ ?. ?=(%wing -.head.e) |
7526+ (levy args.e simple-union-subject-arg)
7527+::
7528+++ duplicate-loobean-arms
7529+ |= e=expr
7530+ ^- ?
7531+ ?. ?=(%branch -.e) |
7532+ ?~ arms.e |
7533+ ?~ t.arms.e |
7534+ ?^ t.t.arms.e |
7535+ =/ x=pattern pat.i.arms.e
7536+ =/ y=pattern pat.i.t.arms.e
7537+ ?. &(?=(%lit -.x) ?=(%lit -.y)) |
7538+ ?. &(=(%loobean form.lit.x) =(%loobean form.lit.y)) |
7539+ =(val.lit.x val.lit.y)
7540+::
7541+++ union-subject-call
7542+ |= e=expr
7543+ ^- ?
7544+ ?: ?=(%group -.e) $(e inner.e)
7545+ ?=(%call -.e)
7546+::
7547+++ known-union-subject
7548+ |= [e=expr env=ienv state=istate]
7549+ ^- (unit iresult)
7550+ ?. (safe-union-subject e) ~
7551+ =/ subject=iresult (infer-fragment e env state)
7552+ ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
7553+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7554+ ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
7555+ `subject
7556+::
7557+::
7558+:: Infer changes only against a fully known record spine. Retain the
7559+:: target type; unknown spines and repeated edits remain unsupported.
7560+++ change-spine-known
7561+ |= [t=itype sub=isub]
7562+ ^- ?
7563+ =. t (itype-walk t sub)
7564+ ?: ?=(%face -.t) &
7565+ ?. ?=(%cell -.t) |
7566+ =/ first=itype (itype-walk hed.t sub)
7567+ ?. ?=(%face -.first) |
7568+ $(t tal.t)
7569+::
7570+++ infer-change-edits
7571+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
7572+ ^- iresult
7573+ ?~ edits [%& target state]
7574+ =/ entry=edit i.edits
7575+ ?: (lien seen |=(name=term =(name name.entry)))
7576+ [%| ["repeated change fields are not supported by partial inference" ~]]
7577+ ?. (change-spine-known target sub.state)
7578+ [%| ["change target needs a known record in partial inference" ~]]
7579+ =/ found=(list itype) (record-fields-named name.entry target sub.state)
7580+ ?~ found
7581+ [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
7582+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
7583+ =/ expected=itype i.found
7584+ =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
7585+ ?: ?=(%| -.value) value
7586+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
7587+ ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
7588+ ?: ?=(%bad -.fit)
7589+ [%| ["change field and replacement do not unify" ~[[at.entry (site-type-note "expected replacement" expected sub.state.p.value)] [(span-of val.entry) (site-type-note "replacement" typ.p.value sub.state.p.value)]]]]
7590+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
7591+::
7592+:: Backtick constructs the canonical prelude unit, after checking its
7593+:: prepared template has the standard null and [~ u=A] cases.
7594+++ standard-unit-template
7595+ |= [template=ischeme at=path]
7596+ ^- ?
7597+ ?. =(at /lib/jibb/prelude/jibb) |
7598+ ?~ vars.template |
7599+ ?^ t.vars.template |
7600+ =/ v=@ud i.vars.template
7601+ =/ nil=itype [%const [%null %n 0 '~']]
7602+ =/ expected=itype
7603+ [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
7604+ =(typ.template expected)
7605+::
7606+:: A named missing-case diagnostic needs more than a failed fit: a case
7607+:: with that tag but the wrong payload is not a missing case. Unknown
7608+:: shapes and atom types that accept terms keep the proof conservative.
7609++$ itag-presence ?(%yes %no %maybe)
7610+++ tag-presence-cases
7611+ |= [cases=(list itype) value=@ sub=isub]
7612+ ^- itag-presence
7613+ ?~ cases %no
7614+ =/ first=itag-presence (tag-presence i.cases value sub)
7615+ ?: =(%yes first) %yes
7616+ =/ rest=itag-presence $(cases t.cases)
7617+ ?: =(%yes rest) %yes
7618+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7619+ %no
7620+::
7621+++ tag-presence
7622+ |= [t=itype value=@ sub=isub]
7623+ ^- itag-presence
7624+ =. t (itype-walk t sub)
7625+ ?- -.t
7626+ %const ?:(=(value val.literal.t) %yes %no)
7627+ %flag ?:(|(=(value 0) =(value 1)) %yes %no)
7628+ %atom ?:(|(=(%tas aura.t) =(%ta aura.t)) %maybe %no)
7629+ %face $(t body.t)
7630+ %cell
7631+ =/ first=itag-presence $(t hed.t)
7632+ ?: =(%yes first) %yes
7633+ =/ rest=itag-presence $(t tal.t)
7634+ ?: =(%yes rest) %yes
7635+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7636+ %no
7637+ %union (tag-presence-cases cases.t value sub)
7638+ * %maybe
7639+ ==
7640+::
7641+++ missing-union-tag
7642+ |= [e=expr expected=itype sub=isub context=span]
7643+ ^- (unit idiag)
7644+ ?. ?=(%lit -.e) ~
7645+ ?. =(%term form.lit.e) ~
7646+ =. expected (itype-walk expected sub)
7647+ |-
7648+ ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
7649+ ?. ?=(%union -.expected) ~
7650+ ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
7651+ =/ label=tape
7652+ ?~ label.expected "union {(show-itype expected sub)}"
7653+ (show-itype expected sub)
7654+ `["{label} has no case `{(trip txt.lit.e)}`" ~[[context "expected union"] [(span-of e) "tag"]]]
7655+::
7656+:: Locate a missing tag inside a syntactic tuple only by replaying the
7657+:: directional fit in source order. Uncertain or earlier failures stop
7658+:: the walk, preserving the generic diagnostic rather than guessing.
7659+++ nested-missing-tag
7660+ |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7661+ ^- (unit idiag)
7662+ =/ original=[left=itype right=itype] [actual expected]
7663+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7664+ =/ fit=ifit (itype-fit actual expected sub next)
7665+ ?. ?=(%bad -.fit) ~
7666+ =. actual (itype-walk actual sub)
7667+ =. expected (itype-walk expected sub)
7668+ ?: &(?=(%face -.actual) ?=(%face -.expected))
7669+ ?. =(name.actual name.expected) ~
7670+ $(actual body.actual, expected body.expected)
7671+ ?: ?=(%face -.actual) $(actual body.actual)
7672+ ?: ?=(%face -.expected) $(expected body.expected)
7673+ =/ direct=(unit idiag) (missing-union-tag e expected sub context)
7674+ ?^ direct direct
7675+ ?. ?=(%tuple -.e) ~
7676+ (nested-missing-items items.e actual expected sub next context)
7677+::
7678+++ nested-missing-items
7679+ |= [items=(list item) actual=itype expected=itype sub=isub next=@ud context=span]
7680+ ^- (unit idiag)
7681+ ?~ items ~
7682+ ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
7683+ =/ original=[left=itype right=itype] [actual expected]
7684+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7685+ =. actual (itype-walk actual sub)
7686+ =. expected (itype-walk expected sub)
7687+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7688+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7689+ ?: ?=(%bad -.first)
7690+ (nested-missing-tag val.i.items hed.actual hed.expected sub next context)
7691+ ?. ?=(%ok -.first) ~
7692+ $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7693+::
7694+:: A term-headed pair is the same noun as a two-item cell. Preserve the
7695+:: whole pair span for the synthetic head and the value's own span for
7696+:: the payload; unresolved term constraints follow ordinary cell inference.
7697+++ pair-as-cell
7698+ |= e=expr
7699+ ^- expr
7700+ ?> ?=(%pair -.e)
7701+ =/ head=expr [%lit at.e [%term %tas tag.e (crip ['%' (trip tag.e)])]]
7702+ [%tuple at.e ~[[at.e ~ head] [(span-of val.e) ~ val.e]]]
7703+::
7704+:: A segment costs one shared step; dynamic segments are not handled yet.
7705+++ qath-static-fuel
7706+ |= [segs=(list qseg) fuel=@ud]
7707+ ^- (unit @ud)
7708+ ?~ segs `fuel
7709+ ?: =(0 fuel) ~
7710+ ?. ?=(%knot -.i.segs) ~
7711+ $(segs t.segs, fuel (dec fuel))
7712+::
66987713++ infer-fragment
66997714 |= [e=expr env=ienv state=istate]
67007715 ^- iresult
67017716 ?- -.e
7717+ %pair $(e (pair-as-cell e))
67027718 %lit
67037719 ?- form.lit.e
67047720 %number ?: =(%ud aura.lit.e)
@@ -6712,7 +7728,45 @@
67127728 %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
67137729 %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
67147730 ==
7731+ %unit
7732+ ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
7733+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7734+ ?~ standard [%| ["unit construction needs the standard prelude in partial inference" ~]]
7735+ ?. (standard-unit-template u.standard at.u.prelude.state)
7736+ [%| ["unit construction needs the standard prelude in partial inference" ~]]
7737+ =/ value=iresult $(e val.e)
7738+ ?: ?=(%| -.value) value
7739+ =/ result=(unit itype) (template-apply u.standard ~[typ.p.value])
7740+ ?~ result [%| ["unit construction is not supported by partial inference" ~]]
7741+ [%& u.result state.p.value]
7742+ %list
7743+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
7744+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7745+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7746+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
7747+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
7748+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
7749+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7750+ =/ element=itype [%var next.state]
7751+ =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
7752+ ?: ?=(%| -.result) result
7753+ [%& [%collection %list ~[element]] state.p.result]
67157754 %str (infer-string-pieces pieces.e env state)
7755+ %qath
7756+ ?~ prelude.state [%| ["application path needs the standard prelude in partial inference" ~]]
7757+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7758+ [%| ["application path needs the standard prelude in partial inference" ~]]
7759+ =/ standard=(unit ischeme) (find-jibb-mold %qath u.prelude.state)
7760+ ?~ standard [%| ["application path needs the standard prelude in partial inference" ~]]
7761+ ?. ?=(~ vars.u.standard) [%| ["application path mold needs unsupported inference" ~]]
7762+ =/ typ=itype typ.u.standard
7763+ ?. ?=(%jrec -.typ) [%| ["application path mold needs unsupported inference" ~]]
7764+ ?. &(=(at.typ /lib/jibb/internal/jibb) =(%qath name.typ) =(%i head.typ) =(%ta aura.typ) =(%t tail.typ))
7765+ [%| ["application path mold needs unsupported inference" ~]]
7766+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
7767+ =/ remain=(unit @ud) (qath-static-fuel segs.e (dec jrec-fuel.state))
7768+ ?~ remain [%| ["application path segments need unsupported inference" ~]]
7769+ [%& typ state(jrec-fuel u.remain)]
67167770 %wing
67177771 ?~ names.e [%| ["empty wing" ~]]
67187772 ?^ t.names.e
@@ -6721,7 +7775,7 @@
67217775 ?~ iface (infer-field-wing names.e env state)
67227776 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
67237777 ?~ member [%| ["module member is not available to partial inference" ~]]
6724− =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e)
7778+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
67257779 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
67267780 [%& typ.instance state.instance]
67277781 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
@@ -6734,6 +7788,11 @@
67347788 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
67357789 [%& typ.instance state.instance]
67367790 %group $(e inner.e)
7791+ %change
7792+ ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
7793+ =/ target=iresult $(e [%wing at.e target.e])
7794+ ?: ?=(%| -.target) target
7795+ (infer-change-edits edits.e typ.p.target env state.p.target ~)
67377796 %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
67387797 %trace
67397798 =/ traced=iresult $(e val.e)
@@ -6750,6 +7809,9 @@
67507809 [%| ["local molds shadow a name" ~]]
67517810 =/ local-state=istate
67527811 state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
7812+ =/ mold-hole=(unit span) (simple-local-mold-hole defs.e)
7813+ ?^ mold-hole
7814+ [%| ["type hole needs a determined type" ~[[u.mold-hole "unresolved type hole"]]]]
67537815 ?. (local-molds-supported local-molds local-state)
67547816 [%| ["local molds need unsupported inference" ~]]
67557817 =/ values=(list def) (local-value-defs defs.e)
@@ -6760,20 +7822,30 @@
67607822 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
67617823 %branch
67627824 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
6763− ?~ t.arms.e (infer-cell-branch e env state)
6764− ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
7825+ ?~ t.arms.e
7826+ ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
7827+ (infer-cell-branch e env state ~)
7828+ ?^ t.t.arms.e (infer-known-union-branch e env state)
7829+ =/ known=(unit iresult) (known-union-subject subject.e env state)
7830+ ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
7831+ ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
7832+ (infer-known-union-branch-subject e env u.known)
67657833 =/ x=arm i.arms.e
67667834 =/ y=arm i.t.arms.e
67677835 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
67687836 (infer-unit-branch e env state ~)
6769− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
6770− ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
7837+ ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7838+ ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
67717839 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6772− [%| ["branch pattern is not supported by partial inference" ~]]
7840+ (infer-known-union-branch e env state)
7841+ ?: &(?=(^ known) ?=(%& -.u.known)) (infer-known-union-branch-subject e env u.known)
67737842 ?: =(val.lit.pat.x val.lit.pat.y)
67747843 [%| ["branch does not cover both loobeans" ~]]
67757844 =/ subject=iresult $(e subject.e)
67767845 ?: ?=(%| -.subject) subject
7846+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
7847+ ?: ?=(%union -.subject-type)
7848+ [%| ["union-pattern branch subject is not supported by partial inference" ~]]
67777849 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
67787850 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
67797851 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6805,17 +7877,18 @@
68057877 ?^ diag [%| u.diag]
68067878 [%| ["cast mold is not supported by partial inference" ~]]
68077879 =/ value=iresult
6808− ?: &(?=(%union -.typ.u.target) (context-union-branch val.e))
6809− (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6810− ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-union-branch val.e))
6811− (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6812− ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-list-expression val.e))
6813− (infer-list-context val.e typ.u.target env state.u.target at.shape.e)
6814− $(e val.e, state state.u.target)
7880+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
68157881 ?: ?=(%| -.value) value
7882+ =/ shape=(unit [source=iwfields target=iwfields])
7883+ (width-shape typ.p.value typ.u.target sub.state.p.value)
7884+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
68167885 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
68177886 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
68187887 ?: ?=(%bad -.fit)
7888+ =/ missing=(unit idiag) (missing-union-tag val.e typ.u.target sub.state.p.value at.shape.e)
7889+ ?^ missing [%| u.missing]
7890+ =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value at.shape.e)
7891+ ?^ nested [%| u.nested]
68197892 [%| ["cast mold and expression type do not unify" ~[[at.shape.e (site-type-note "cast mold" typ.u.target sub.state.p.value)] [(span-of val.e) (site-type-note "expression" typ.p.value sub.state.p.value)]]]]
68207893 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
68217894 [%& merged state.p.value(sub sub.fit, next next.fit)]
@@ -6840,43 +7913,9 @@
68407913 [%& [%fn typ.p.sam typ.p.body] state.p.body]
68417914 %call
68427915 ?~ args.e [%| ["call has no argument" ~]]
6843− =/ head=iresult $(e head.e)
6844− ?: ?=(%| -.head) head
6845− =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
6846− =/ arg=iresult
6847− ?^ t.args.e
6848− ?: ?=(%fn -.head-type)
6849− (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
6850− (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
6851− ?: &(?=(%fn -.head-type) ?=(%union -.sample.head-type) (context-union-branch i.args.e))
6852− (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6853− ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-union-branch i.args.e))
6854− (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6855− ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-list-expression i.args.e))
6856− (infer-list-context i.args.e sample.head-type env state.p.head (span-of head.e))
6857− $(e i.args.e, state state.p.head)
6858− ?: ?=(%| -.arg) arg
6859− =/ st=istate state.p.arg
6860− =/ ht=itype (itype-walk typ.p.head sub.st)
6861− ?: ?=(%fn -.ht)
6862− =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
6863− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
6864− ?: ?=(%bad -.fit)
6865− =/ bad=(unit [at=span typ=itype])
6866− ?~(t.args.e ~ (call-error-site args.e typ.p.arg sample.ht sub.st next.st))
6867− =/ whole-args=span
6868− ?~(t.args.e (span-of i.args.e) [beg:(span-of i.args.e) end:(span-of (rear args.e))])
6869− =/ arg-at=span ?~(bad whole-args at.u.bad)
6870− =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
6871− [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]
6872− ?: &((itype-has-face typ.p.arg sub.fit) (itype-face-asym typ.p.arg sample.ht sub.fit) (itype-output-may-be-cell product.ht sub.fit))
6873− [%| ["call result face propagation is not supported by partial inference" ~]]
6874− [%& product.ht st(sub sub.fit, next next.fit)]
6875− =/ result=itype [%var next.st]
6876− =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
6877− ?~ uni
6878− [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
6879− [%& result st(next +(next.st), sub u.uni)]
7916+ ?: (explicit-proj-call e env state)
7917+ [%| ["proj needs an expected record type" ~]]
7918+ (infer-call-with-head e env state (infer-fragment head.e env state))
68807919 * [%| ["expression is not supported by partial inference" ~]]
68817920 ==
68827921::
@@ -6884,6 +7923,72 @@
68847923:: failed. If an intermediate fit is uncertain, retain the whole argument
68857924:: span rather than assigning blame to a particular argument.
68867925::
7926+:: Check a call using the head already inferred in this state. Keeping
7927+:: this shared avoids evaluating or instantiating a contextual head twice.
7928+++ width-has-projections
7929+ |= ps=(list iwprojection)
7930+ ^- ?
7931+ ?~ ps |
7932+ &
7933+::
7934++$ iwidth-elaboration [original=expr typ=itype sub=isub projections=(list iwprojection)]
7935+++ infer-width-elaboration
7936+ |= [e=expr env=ienv state=istate]
7937+ ^- (each iwidth-elaboration idiag)
7938+ =/ out=iresult (infer-fragment e env state)
7939+ ?: ?=(%| -.out) [%| p.out]
7940+ [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
7941+::
7942+++ infer-call-with-head
7943+ |= [e=expr env=ienv state=istate head=iresult]
7944+ ^- iresult
7945+ ?> ?=(%call -.e)
7946+ ?~ args.e [%| ["call has no argument" ~]]
7947+ ?: ?=(%| -.head) head
7948+ =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
7949+ =/ arg=iresult
7950+ ?^ t.args.e
7951+ ?: ?=(%fn -.head-type)
7952+ (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
7953+ (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
7954+ ?: ?=(%fn -.head-type)
7955+ (infer-call-context-arg i.args.e sample.head-type env state.p.head (span-of head.e))
7956+ (infer-fragment i.args.e env state.p.head)
7957+ ?: ?=(%| -.arg) arg
7958+ =/ st=istate state.p.arg
7959+ =/ ht=itype (itype-walk typ.p.head sub.st)
7960+ ?: ?=(%fn -.ht)
7961+ =/ shape=(unit [source=iwfields target=iwfields])
7962+ ?^ t.args.e ~
7963+ (width-shape typ.p.arg sample.ht sub.st)
7964+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
7965+ =/ fit=ifit
7966+ ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
7967+ (itype-fit typ.p.arg sample.ht sub.st next.st)
7968+ ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
7969+ ?: ?=(%bad -.fit)
7970+ ?~ t.args.e
7971+ =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
7972+ ?^ missing [%| u.missing]
7973+ =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
7974+ ?^ nested [%| u.nested]
7975+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7976+ =/ bad=(unit [at=span typ=itype])
7977+ (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
7978+ =/ whole-args=span
7979+ [beg:(span-of i.args.e) end:(span-of (rear args.e))]
7980+ =/ arg-at=span ?~(bad whole-args at.u.bad)
7981+ =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7982+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]
7983+ ?: &((itype-has-face typ.p.arg sub.fit) (itype-face-asym typ.p.arg sample.ht sub.fit) (itype-output-may-be-cell product.ht sub.fit))
7984+ [%| ["call result face propagation is not supported by partial inference" ~]]
7985+ [%& product.ht st(sub sub.fit, next next.fit)]
7986+ =/ result=itype [%var next.st]
7987+ =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
7988+ ?~ uni
7989+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7990+ [%& result st(next +(next.st), sub u.uni)]
7991+::
68877992++ call-error-site
68887993 |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
68897994 ^- (unit [at=span typ=itype])
@@ -6904,34 +8009,249 @@
69048009 ?: ?=(%unknown -.first) ~
69058010 $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
69068011::
6907−:: Context can help each argument while the final fit still checks the
6908−:: complete right-nested sample, including any faces on its positions.
8012+:: Context can help a call argument or cast value while the final fit
8013+:: checks the complete right-nested type, including any written faces.
8014+::
8015+:: Context can resolve the payload of a canonical prelude unit, but an
8016+:: unrelated union with a similar noun shape is not the same mold.
8017+++ infer-unit-context
8018+ |= [e=expr expected=itype env=ienv state=istate context=span]
8019+ ^- iresult
8020+ ?> ?=(%unit -.e)
8021+ ?> ?=(%union -.expected)
8022+ ?~ prelude.state (infer-fragment e env state)
8023+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
8024+ ?~ standard (infer-fragment e env state)
8025+ ?. (standard-unit-template u.standard at.u.prelude.state) (infer-fragment e env state)
8026+ ?. =(origin.expected `[at.u.prelude.state %unit]) (infer-fragment e env state)
8027+ ?~ args.expected (infer-fragment e env state)
8028+ ?^ t.args.expected (infer-fragment e env state)
8029+ =/ payload=itype i.args.expected
8030+ =/ canonical=(unit itype) (template-apply u.standard ~[payload])
8031+ ?~ canonical (infer-fragment e env state)
8032+ ?> ?=(%union -.u.canonical)
8033+ ?. =((itype-normalize expected(label ~) sub.state) (itype-normalize u.canonical(label ~) sub.state))
8034+ (infer-fragment e env state)
8035+ =/ value=iresult (infer-call-context-arg val.e payload env state context)
8036+ ?: ?=(%| -.value) value
8037+ =/ fit=ifit (itype-fit typ.p.value payload sub.state.p.value next.state.p.value)
8038+ ?: ?=(%unknown -.fit) [%| ["unit payload constraint is not supported by partial inference" ~]]
8039+ ?: ?=(%bad -.fit)
8040+ =/ missing=(unit idiag) (missing-union-tag val.e payload sub.state.p.value context)
8041+ ?^ missing [%| u.missing]
8042+ =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
8043+ ?^ nested [%| u.nested]
8044+ [%| ["unit payload does not fit its expected type" ~[[context (site-type-note "expected unit payload" payload sub.state.p.value)] [(span-of val.e) (site-type-note "payload" typ.p.value sub.state.p.value)]]]]
8045+ [%& expected state.p.value(sub sub.fit, next next.fit)]
8046+::
8047+:: A known gate whose result is still an inference variable can receive
8048+:: an enclosing target before its argument is inferred. Other products
8049+:: and unresolved calls use the existing directional path unchanged.
8050+++ infer-contextual-call
8051+ |= [e=expr expected=itype env=ienv state=istate]
8052+ ^- iresult
8053+ ?> ?=(%call -.e)
8054+ ?~ args.e [%| ["call has no argument" ~]]
8055+ =/ head=iresult (infer-fragment head.e env state)
8056+ ?: ?=(%| -.head) head
8057+ =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
8058+ ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
8059+ =/ result=itype (itype-walk product.ht sub.state.p.head)
8060+ ?. ?=(%var -.result) (infer-call-with-head e env state head)
8061+ ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected) (itype-has-tag (itype-normalize expected sub.state.p.head)))
8062+ (infer-call-with-head e env state head)
8063+ =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
8064+ ?~ sub (infer-call-with-head e env state head)
8065+ (infer-call-with-head e env state [%& typ.p.head state.p.head(sub u.sub)])
8066+::
8067+:: An eligible fully faced literal receives context by name, in source order.
8068+++ width-literal-fields
8069+ |= [items=(list item) axis=@ud fuel=@ud]
8070+ ^- (unit iwfields)
8071+ =/ order=(list iwfield) ~
8072+ =/ index=(map term iwfield) *(map term iwfield)
8073+ |-
8074+ ?~ items ~
8075+ ?: =(0 fuel) ~
8076+ ?~ face.i.items ~
8077+ =/ at-axis=@ud ?~(t.items axis (mul 2 axis))
8078+ =/ entry=iwfield [u.face.i.items at-axis [%noun ~]]
8079+ ?: ?=(^ (~(get by index) name.entry)) ~
8080+ =. index (~(put by index) name.entry entry)
8081+ =. order [entry order]
8082+ ?~ t.items `[(flop order) index]
8083+ $(items t.items, axis +((mul 2 axis)), fuel (dec fuel))
8084+++ width-infer-items
8085+ |= [items=(list item) expected=(map term iwfield) env=ienv state=istate context=span]
8086+ ^- iresult
8087+ ?~ items [%| ["empty record is not supported" ~]]
8088+ ?~ face.i.items [%| ["record face needs unsupported inference" ~]]
8089+ =/ field=(unit iwfield) (~(get by expected) u.face.i.items)
8090+ =/ head=iresult
8091+ ?~ field (infer-fragment val.i.items env state)
8092+ (infer-call-context-arg val.i.items typ.u.field env state context)
8093+ ?: ?=(%| -.head) head
8094+ =/ typ=itype [%face u.face.i.items typ.p.head]
8095+ ?~ t.items [%& typ state.p.head]
8096+ =/ tail=iresult $(items t.items, state state.p.head)
8097+ ?: ?=(%| -.tail) tail
8098+ [%& [%cell typ typ.p.tail] state.p.tail]
8099+++ width-infer-literal
8100+ |= [e=expr expected=itype env=ienv state=istate context=span]
8101+ ^- (unit iresult)
8102+ ?. ?=(%tuple -.e) ~
8103+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) ~
8104+ =/ source=(unit iwfields) (width-literal-fields items.e 1 4.096)
8105+ =/ target=(unit iwfields) (width-scan expected sub.state 1 4.096)
8106+ ?~ source ~
8107+ ?~ target ~
8108+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
8109+ ?. (width-in-order order.u.source order.u.target)
8110+ `(infer-simple-items items.e env state)
8111+ `(width-infer-items items.e index.u.target env state context)
8112+::
8113+:: Recognize only the reserved unqualified, one-argument operation.
8114+++ explicit-proj-call
8115+ |= [e=expr env=ienv state=istate]
8116+ ^- ?
8117+ ?. ?=(%call -.e) |
8118+ ?. ?=([* ~] args.e) |
8119+ ?. ?=(%wing -.head.e) |
8120+ ?. =(names.head.e ~[%proj]) |
8121+ ?: ?=(^ (ienv-lookup %proj env)) |
8122+ ?: (lien globals.state |=(n=term =(n %proj))) |
8123+ ?~ prelude.state &
8124+ ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
8125+++ infer-proj-source
8126+ |= [e=expr expected=itype env=ienv state=istate context=span]
8127+ ^- iresult
8128+ ?: ?=(%group -.e) $(e inner.e)
8129+ =/ literal=(unit iresult) (width-infer-literal e expected env state context)
8130+ ?^ literal u.literal
8131+ (infer-fragment e env state)
8132+++ infer-proj-context
8133+ |= [e=expr expected=itype env=ienv state=istate context=span]
8134+ ^- iresult
8135+ ?> ?=(%call -.e)
8136+ ?~ args.e [%| ["proj needs one record" ~]]
8137+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) [%| ["proj needs an expected record type" ~]]
8138+ =/ value=iresult (infer-proj-source i.args.e expected env state context)
8139+ ?: ?=(%| -.value) value
8140+ =/ shape=(unit [source=iwfields target=iwfields])
8141+ (width-proj-shape typ.p.value expected sub.state.p.value)
8142+ ?~ shape [%| ["proj needs a known record containing its expected fields" ~]]
8143+ =/ project=(unit iwidth-result) (width-project u.shape sub.state.p.value next.state.p.value)
8144+ ?~ project [%| ["proj constraint needs unsupported inference" ~]]
8145+ =/ st=istate state.p.value(sub sub.u.project, next next.u.project)
8146+ [%& expected st(projections [[at.e e typ.p.value expected steps.u.project] projections.st])]
69098147::
69108148++ infer-call-context-arg
69118149 |= [e=expr expected=itype env=ienv state=istate context=span]
69128150 ^- iresult
8151+ ?: ?=(%pair -.e) $(e (pair-as-cell e))
8152+ ?: ?=(%group -.e) $(e inner.e)
8153+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8154+ ?: ?=(%trace -.e)
8155+ =/ traced=iresult (infer-fragment val.e env state)
8156+ ?: ?=(%| -.traced) traced
8157+ $(e then.e, state state.p.traced)
69138158 =/ target=itype (itype-walk expected sub.state)
69148159 |-
69158160 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8161+ ?: (explicit-proj-call e env state)
8162+ (infer-proj-context e expected env state context)
8163+ :: Only the source-proven one-layer cell is exposed. Each recursive
8164+ :: descent consumes one written tuple; named values use ordinary fit.
8165+ ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
8166+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8167+ [%& target state(jrec-fuel (dec jrec-fuel.state))]
8168+ ?: &(?=(%jrec -.target) ?=(%tuple -.e))
8169+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8170+ =. state state(jrec-fuel (dec jrec-fuel.state))
8171+ =/ shape=itype
8172+ [%cell [%face head.target [%atom aura.target]] [%face tail.target target]]
8173+ =/ value=iresult (infer-call-context-items items.e shape env state context)
8174+ ?: ?=(%| -.value) value
8175+ =/ fit=ifit (itype-fit typ.p.value shape sub.state.p.value next.state.p.value)
8176+ ?: ?=(%unknown -.fit) [%| ["recursive mold cell constraint needs unsupported inference" ~]]
8177+ ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
8178+ [%& target state.p.value(sub sub.fit, next next.fit)]
8179+ ?: ?=(%call -.e) (infer-contextual-call e target env state)
8180+ ?: (single-structured-pattern e)
8181+ (infer-single-case-branch e env state `[target context])
8182+ ?: (cell-binder-pattern e)
8183+ (infer-cell-branch e env state `[target context])
8184+ :: In a loobean-singleton context retain the written loobean noun;
8185+ :: the usual final fit decides whether that value is permitted.
8186+ =/ singleton=(unit itype)
8187+ ?. ?=(%lit -.e) ~
8188+ ?. =(%loobean form.lit.e) ~
8189+ ?. ?=(%const -.target) ~
8190+ ?. =(%loobean form.literal.target) ~
8191+ `[%const lit.e]
8192+ ?^ singleton [%& u.singleton state]
8193+ =/ known=(unit iresult)
8194+ ?: ?=(%branch -.e) (known-union-subject subject.e env state)
8195+ ~
8196+ ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
8197+ ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
8198+ (infer-known-union-context-subject e target env u.known context)
8199+ ?: &(?=(%union -.target) ?=(%unit -.e))
8200+ (infer-unit-context e target env state context)
8201+ ?: &(?=(%flag -.target) (context-union-branch e))
8202+ (infer-union-context e target env state context)
69168203 ?: &(?=(%union -.target) (context-union-branch e))
69178204 (infer-union-context e target env state context)
69188205 ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
69198206 (infer-union-context e target env state context)
69208207 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
69218208 (infer-list-context e target env state context)
8209+ ?: &(?=(%cell -.target) ?=(%tuple -.e))
8210+ (infer-call-context-items items.e target env state context)
69228211 (infer-fragment e env state)
69238212::
8213+:: Preserve each written face; the final complete sample fit checks faces.
8214+:: A tuple or positional field face belongs to the enclosing sample,
8215+:: not to the expression at that position. A second face, if present,
8216+:: is part of the value's own expected type.
8217+++ projection-field-target
8218+ |= expected=itype
8219+ ^- itype
8220+ ?:(?=(%face -.expected) body.expected expected)
8221+::
8222+++ infer-call-context-items
8223+ |= [items=(list item) expected=itype env=ienv state=istate context=span]
8224+ ^- iresult
8225+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
8226+ ?~ t.items
8227+ =/ last=iresult (infer-call-context-arg val.i.items (projection-field-target expected) env state context)
8228+ ?: ?=(%| -.last) last
8229+ =/ typ=itype typ.p.last
8230+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8231+ [%& typ state.p.last]
8232+ =/ target=itype (itype-walk expected sub.state)
8233+ |-
8234+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8235+ ?. ?=(%cell -.target) (infer-simple-items items env state)
8236+ =/ head=iresult (infer-call-context-arg val.i.items (projection-field-target hed.target) env state context)
8237+ ?: ?=(%| -.head) head
8238+ =/ typ=itype typ.p.head
8239+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8240+ =/ tail=iresult (infer-call-context-items t.items tal.target env state.p.head context)
8241+ ?: ?=(%| -.tail) tail
8242+ [%& [%cell typ typ.p.tail] state.p.tail]
8243+::
69248244++ infer-call-context-args
69258245 |= [args=(list expr) expected=itype env=ienv state=istate context=span]
69268246 ^- iresult
69278247 ?~ args [%| ["call has no argument" ~]]
6928− ?~ t.args (infer-call-context-arg i.args expected env state context)
8248+ ?~ t.args (infer-call-context-arg i.args (projection-field-target expected) env state context)
69298249 =/ target=itype (itype-walk expected sub.state)
69308250 |-
69318251 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
69328252 ?. ?=(%cell -.target)
69338253 (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
6934− =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
8254+ =/ head=iresult (infer-call-context-arg i.args (projection-field-target hed.target) env state context)
69358255 ?: ?=(%| -.head) head
69368256 =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
69378257 ?: ?=(%| -.tail) tail
@@ -6952,11 +8272,55 @@
69528272 ?: ?=(%| -.tail) tail
69538273 [%& [%cell ht typ.p.tail] state.p.tail]
69548274::
6955−:: A single two-binder cell pattern covers every value of a cell type.
6956−:: No other pattern matrix is implemented here.
8275+:: A single all-binder cell pattern covers a known cell spine; the final
8276+:: binder captures the remaining noun. Other pattern matrices stay partial.
8277+::
8278+:: Validate binders before reading the subject, preserving shadow-error
8279+:: precedence. The last binder receives the entire remaining tail.
8280+++ cell-pattern-names
8281+ |= [pats=(list pattern) env=ienv globals=(list term) seen=(list term)]
8282+ ^- (each (list term) @t)
8283+ ?~ pats [%& ~]
8284+ ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
8285+ =/ name=term name.i.pats
8286+ ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
8287+ [%| 'pattern shadows a name']
8288+ =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
8289+ ?: ?=(%| -.rest) rest
8290+ [%& [name p.rest]]
8291+::
8292+++ cell-pattern-types
8293+ |= [names=(list term) env=ienv next=@ud]
8294+ ^- [typ=itype env=ienv next=@ud]
8295+ ?~ names !!
8296+ =/ head=itype [%var next]
8297+ =/ scope=ienv [[i.names [head ~]] env]
8298+ ?~ t.names [head scope +(next)]
8299+ =/ tail=[typ=itype env=ienv next=@ud] $(names t.names, env scope, next +(next))
8300+ [[%cell head typ.tail] env.tail next.tail]
8301+::
8302+:: At every position that must be a cell, opaque or sum types may still
8303+:: contain cells. Do not report a definite mismatch without unfolding them.
8304+++ cell-pattern-spine-unknown
8305+ |= [typ=itype names=(list term) sub=isub]
8306+ ^- ?
8307+ ?~ names |
8308+ ?~ t.names |
8309+ =. typ (itype-walk typ sub)
8310+ ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8311+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
8312+::
8313+++ cell-binder-pattern
8314+ |= e=expr
8315+ ^- ?
8316+ ?. ?=(%branch -.e) |
8317+ ?~ arms.e |
8318+ ?^ t.arms.e |
8319+ ?. ?=(%cell -.pat.i.arms.e) |
8320+ !(single-structured-pattern e)
69578321::
69588322++ infer-cell-branch
6959− |= [e=expr env=ienv state=istate]
8323+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
69608324 ^- iresult
69618325 ?> ?=(%branch -.e)
69628326 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -6965,25 +8329,31 @@
69658329 =/ pats=(list pattern) items.pat.arm
69668330 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
69678331 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6968− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6969− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6970− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6971− =/ one=term name.i.pats
6972− =/ two=term name.i.t.pats
6973− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
6974− [%| ["pattern shadows a name" ~]]
8332+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
8333+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
69758334 =/ subject=iresult (infer-fragment subject.e env state)
69768335 ?: ?=(%| -.subject) subject
69778336 =/ st=istate state.p.subject
6978− ?: (itype-has-recursive (itype-normalize typ.p.subject sub.st))
8337+ =/ subject-type=itype (itype-normalize typ.p.subject sub.st)
8338+ ?: (itype-has-recursive subject-type)
69798339 [%| ["recursive pattern is not supported by partial inference" ~]]
69808340 ?: (itype-has-face typ.p.subject sub.st)
69818341 [%| ["record patterns are not supported by partial inference" ~]]
6982− =/ head=itype [%var next.st]
6983− =/ tail=itype [%var +(next.st)]
6984− =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
8342+ ?: (cell-pattern-spine-unknown subject-type p.names sub.st)
8343+ [%| ["cell pattern subject is not supported by partial inference" ~]]
8344+ =/ binders=[typ=itype env=ienv next=@ud] (cell-pattern-types p.names env next.st)
8345+ =/ sub=(unit isub) (itype-unify typ.p.subject typ.binders sub.st)
69858346 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
6986− (infer-fragment val.arm [[one [head ~]] [two [tail ~]] env] st(next (add 2 next.st), sub u.sub))
8347+ =. st st(next next.binders, sub u.sub)
8348+ ?~ expected (infer-fragment val.arm env.binders st)
8349+ =/ body=iresult (infer-call-context-arg val.arm typ.u.expected env.binders st context.u.expected)
8350+ ?: ?=(%| -.body) body
8351+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
8352+ ?: ?=(%unknown -.fit) [%| ["cell branch result constraint is not supported by partial inference" ~]]
8353+ ?: ?=(%bad -.fit) [%| ["cell branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.arm) "branch arm"]]]]
8354+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8355+ [%| ["cell branch result needs context in partial inference" ~]]
8356+ [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
69878357::
69888358++ show-itype
69898359 |= [t=itype sub=isub]
@@ -7002,6 +8372,7 @@
70028372 %atom "@{(trip aura.t)}"
70038373 %any-atom "@"
70048374 %flag "?"
8375+ %noun "*"
70058376 %tag (trip txt.literal.t)
70068377 %const (trip txt.literal.t)
70078378 %union
@@ -7009,6 +8380,7 @@
70098380 ?~ args.t (trip u.label.t)
70108381 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
70118382 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8383+ %jrec ?~(label.t "recursive mold" (trip u.label.t))
70128384 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
70138385 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
70148386 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -7049,10 +8421,12 @@
70498421 %atom |
70508422 %any-atom |
70518423 %flag |
8424+ %noun |
70528425 %tag |
70538426 %const |
70548427 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
70558428 %recursive |
8429+ %jrec |
70568430 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
70578431 %face $(typ body.typ)
70588432 %fn |($(typ sample.typ) $(typ product.typ))
@@ -7157,10 +8531,12 @@
71578531 %atom |
71588532 %any-atom |
71598533 %flag |
8534+ %noun |
71608535 %tag |
71618536 %const |
71628537 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
71638538 %recursive |
8539+ %jrec |
71648540 %collection (lien args.t |=(c=itype (has-atom-var n c)))
71658541 %face $(t body.t)
71668542 %fn |($(t sample.t) $(t product.t))
@@ -7208,9 +8584,9 @@
72088584::
72098585:: Build the supported part of the value environment in dependency order.
72108586:: Each pass adds successful definitions. Forward references become
7211−:: available on a later pass; mutually recursive groups and unsupported
7212−:: syntax do not enter the environment. Generalized definitions are closed, so a
7213−:: use instantiates its variables afresh.
8587+:: available on a later pass; unsupported syntax does not enter the
8588+:: environment. Generalized definitions are closed, so a use instantiates
8589+:: its variables afresh.
72148590::
72158591++ global-value-names
72168592 |= ds=(list def)
@@ -7337,36 +8713,508 @@
73378713 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
73388714 [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
73398715::
7340−++ add-supported-defs
7341− |= [ds=(list def) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]
8716+++ dependency-root
8717+ |= names=(list term)
8718+ ^- (list term)
8719+ ?~ names ~
8720+ ~[(rear names)]
8721+::
8722+++ dependency-exprs
8723+ |= xs=(list expr)
8724+ ^- (list term)
8725+ ?~ xs ~
8726+ =/ first=(list term) (dependency-expr i.xs)
8727+ (weld first $(xs t.xs))
8728+::
8729+++ dependency-pieces
8730+ |= xs=(list piece)
8731+ ^- (list term)
8732+ ?~ xs ~
8733+ =/ first=(list term)
8734+ ?- -.i.xs
8735+ %expr (dependency-expr p.i.xs)
8736+ %text ~
8737+ ==
8738+ (weld first $(xs t.xs))
8739+::
8740+++ dependency-qsegs
8741+ |= xs=(list qseg)
8742+ ^- (list term)
8743+ ?~ xs ~
8744+ =/ first=(list term)
8745+ ?- -.i.xs
8746+ %expr (dependency-expr p.i.xs)
8747+ %knot ~
8748+ ==
8749+ (weld first $(xs t.xs))
8750+::
8751+++ dependency-items
8752+ |= xs=(list item)
8753+ ^- (list term)
8754+ ?~ xs ~
8755+ =/ first=(list term) (dependency-expr val.i.xs)
8756+ (weld first $(xs t.xs))
8757+::
8758+++ dependency-edits
8759+ |= xs=(list edit)
8760+ ^- (list term)
8761+ ?~ xs ~
8762+ =/ first=(list term) (dependency-expr val.i.xs)
8763+ (weld first $(xs t.xs))
8764+::
8765+++ dependency-arms
8766+ |= xs=(list arm)
8767+ ^- (list term)
8768+ ?~ xs ~
8769+ =/ first=(list term) (dependency-expr val.i.xs)
8770+ (weld first $(xs t.xs))
8771+::
8772+++ dependency-defs
8773+ |= xs=(list def)
8774+ ^- (list term)
8775+ ?~ xs ~
8776+ =/ first=(list term)
8777+ ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
8778+ ~
8779+ (weld first $(xs t.xs))
8780+::
8781+++ dependency-expr
8782+ |= e=expr
8783+ ^- (list term)
8784+ ?- -.e
8785+ %str (dependency-pieces pieces.e)
8786+ %qath (dependency-qsegs segs.e)
8787+ %wing (dependency-root names.e)
8788+ %change
8789+ =/ first=(list term) (dependency-root target.e)
8790+ =/ last=(list term) (dependency-edits edits.e)
8791+ (weld first last)
8792+ %pair (dependency-expr val.e)
8793+ %unit (dependency-expr val.e)
8794+ %group (dependency-expr inner.e)
8795+ %list (dependency-exprs items.e)
8796+ %tuple (dependency-items items.e)
8797+ %gate (dependency-expr body.e)
8798+ %gate-wide (dependency-expr body.e)
8799+ %call
8800+ =/ first=(list term) (dependency-expr head.e)
8801+ =/ last=(list term) (dependency-exprs args.e)
8802+ (weld first last)
8803+ %cast (dependency-expr val.e)
8804+ %trace
8805+ =/ first=(list term) (dependency-expr val.e)
8806+ =/ last=(list term) (dependency-expr then.e)
8807+ (weld first last)
8808+ %branch
8809+ =/ first=(list term) (dependency-expr subject.e)
8810+ =/ last=(list term) (dependency-arms arms.e)
8811+ (weld first last)
8812+ %body
8813+ =/ first=(list term) (dependency-defs defs.e)
8814+ =/ last=(list term) (dependency-expr final.e)
8815+ (weld first last)
8816+ * ~
8817+ ==
8818+::
8819+:: Infer a cyclic component with one monomorphic seed per gate. All members
8820+:: must succeed before any scheme is available; pending constraints and
8821+:: unresolved branch joins remain partial.
8822++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
8823++$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
8824+++ seed-gate-group
8825+ |= [ds=(list def) env=ienv state=istate]
8826+ ^- igate-seeds
8827+ ?~ ds [%& [~ state]]
8828+ =/ d=def i.ds
8829+ ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
8830+ =/ gate=expr val.d
8831+ ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
8832+ [%| ["recursive group contains a non-gate" ~]]
8833+ =/ initial=istate (reserve-def-caps gate state)
8834+ =/ sam=isample-result
8835+ ?- -.gate
8836+ %gate (infer-sample sample.gate env initial)
8837+ %gate-wide (infer-sample sample.gate env initial)
8838+ * !!
8839+ ==
8840+ ?: ?=(%| -.sam) [%| [p.sam ~]]
8841+ =/ body=expr
8842+ ?- -.gate
8843+ %gate body.gate
8844+ %gate-wide body.gate
8845+ * !!
8846+ ==
8847+ =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
8848+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
8849+ =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
8850+ =/ rest=igate-seeds $(ds t.ds, state after)
8851+ ?: ?=(%| -.rest) rest
8852+ [%& [[entry entries.p.rest] state.p.rest]]
8853+::
8854+++ group-seed-env
8855+ |= [entries=(list igate-entry) env=ienv]
73428856 ^- ienv
7343− ?~ ds env
8857+ ?~ entries env
8858+ [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
8859+::
8860+++ infer-gate-group-bodies
8861+ |= [entries=(list igate-entry) seeds=ienv state=istate]
8862+ ^- igate-seeds
8863+ ?~ entries [%& [~ state]]
8864+ =/ entry=igate-entry i.entries
8865+ ?> ?=(%fn -.typ.entry)
8866+ =/ scope=ienv (weld seeds env.entry)
8867+ =/ out=iresult (infer-fragment body.entry scope state(caps caps.entry))
8868+ ?: ?=(%| -.out) out
8869+ =/ uni=(unit isub) (itype-unify product.typ.entry typ.p.out sub.state.p.out)
8870+ ?~ uni [%| ["recursive group constraint is not supported by partial inference" ~]]
8871+ =. caps.entry caps.state.p.out
8872+ =/ after=istate state.p.out(sub u.uni, caps caps.state)
8873+ =/ rest=igate-seeds $(entries t.entries, state after)
8874+ ?: ?=(%| -.rest) rest
8875+ [%& [[entry entries.p.rest] state.p.rest]]
8876+::
8877+++ group-schemes
8878+ |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
8879+ ^- (each ienv idiag)
8880+ ?~ entries [%& ~]
8881+ =/ entry=igate-entry i.entries
8882+ =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
8883+ ?^ merged
8884+ [%| ["distinct type variables must not be forced equal" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
8885+ ?: (constrained-capitals caps.entry sub.state)
8886+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
8887+ =/ typ=itype (itype-normalize typ.entry sub.state)
8888+ ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
8889+ [%| ["recursive group needs unsupported inference" ~]]
8890+ =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
8891+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8892+ =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
8893+ ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
8894+ =/ rest=(each ienv idiag) $(entries t.entries)
8895+ ?: ?=(%| -.rest) rest
8896+ [%& [[name.entry [typ vars]] p.rest]]
8897+::
8898+++ infer-gate-group
8899+ |= [ds=(list def) env=ienv state=istate]
8900+ ^- ilocal-result
8901+ =/ names=(list term) (global-value-names ds)
8902+ ?. (levy names |=(n=term (unique-value-name n names)))
8903+ [%| ["recursive group contains duplicate names" ~]]
8904+ ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
8905+ [%| ["recursive group shadows a name" ~]]
8906+ =/ scoped=istate state(globals (weld names globals.state))
8907+ =/ seeded=igate-seeds (seed-gate-group ds env scoped)
8908+ ?: ?=(%| -.seeded) seeded
8909+ =/ seeds=ienv (group-seed-env entries.p.seeded ~)
8910+ =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
8911+ ?: ?=(%| -.body) body
8912+ :: Per-member ownership through mutual recursion is not implemented.
8913+ ?: !=(projections.state.p.body projections.state)
8914+ [%| ["record projection in recursive groups needs unsupported inference" ~]]
8915+ ?: !=(holes.state.p.body holes.state)
8916+ [%| ["holes in recursive groups need unsupported inference" ~]]
8917+ ?: (pending-tags tags.state.p.body sub.state.p.body)
8918+ [%| ["recursive group has unresolved literal constraints" ~]]
8919+ =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
8920+ ?: ?=(%| -.schemes) schemes
8921+ [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
8922+::
8923+++ width-finalize
8924+ |= [ps=(list iwprojection) sub=isub visible=(list @ud)]
8925+ ^- (unit (list iwprojection))
8926+ ?~ ps `~
8927+ ?: (lien t.ps |=(p=iwprojection =(at.p at.i.ps))) ~
8928+ =/ src=itype (default-decimals (itype-normalize source.i.ps sub))
8929+ =/ dst=itype (default-decimals (itype-normalize target.i.ps sub))
8930+ ?: |((itype-has-nvar src) (itype-has-nvar dst) (itype-has-tag src) (itype-has-tag dst)) ~
8931+ =/ vars=(list @ud) (weld (itype-vars src) (itype-vars dst))
8932+ ?. (levy vars |=(n=@ud (lien visible |=(v=@ud =(n v))))) ~
8933+ =/ rest=(unit (list iwprojection)) $(ps t.ps)
8934+ ?~ rest ~
8935+ =/ entry=iwprojection i.ps
8936+ =. entry entry(source src, target dst)
8937+ `[entry u.rest]
8938+::
8939+++ add-supported-defs
8940+ |= [ds=(list def) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition)]
8941+ ^- [env=ienv artifacts=(list iwidth-definition)]
8942+ ?~ ds [env artifacts]
73448943 =/ d=def i.ds
73458944 ?: ?=(%mold -.d) $(ds t.ds)
73468945 ?. (unique-value-name name.d globals) $(ds t.ds)
73478946 ?^ (ienv-lookup name.d env) $(ds t.ds)
73488947 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7349− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8948+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
73508949 =. initial (reserve-def-caps val.d initial)
73518950 =/ result=iresult (infer-fragment val.d env initial)
73528951 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
73538952 ?: ?=(%| -.result) $(ds t.ds)
8953+ =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
8954+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
73548955 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
73558956 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
73568957 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
73578958 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
73588959 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
73598960 ?: (gth (lent vars) 26) $(ds t.ds)
8961+ =/ finalized=(unit (list iwprojection))
8962+ (width-finalize projections.state.p.result sub.state.p.result vars)
8963+ ?~ finalized $(ds t.ds)
8964+ =? artifacts ?=(^ u.finalized)
8965+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
73608966 $(ds t.ds, env [[name.d [typ vars]] env])
73618967::
8968++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
8969++$ iadj (map term (list term))
8970++$ ivisited (map term ?)
8971++$ iwork (list [name=term done=?])
8972++$ iwresult [seen=ivisited order=(list term)]
8973++$ icresult [seen=ivisited component=(list term)]
8974++$ icomponents (list (list term))
8975+++ graph-nameset
8976+ |= [names=(list term) seen=ivisited]
8977+ ^- ivisited
8978+ ?~ names seen
8979+ $(names t.names, seen (~(put by seen) i.names &))
8980+::
8981+++ graph-edges
8982+ |= [name=term graph=iadj]
8983+ ^- (list term)
8984+ =/ found=(unit (list term)) (~(get by graph) name)
8985+ ?~ found ~
8986+ u.found
8987+::
8988+++ graph-make-forward
8989+ |= [ds=(list def) names=ivisited graph=iadj]
8990+ ^- iadj
8991+ ?~ ds graph
8992+ ?. ?=(%value -.i.ds) $(ds t.ds)
8993+ =/ deps=(list term) (dependency-expr val.i.ds)
8994+ =. deps (skim deps |=(n=term ?=(^ (~(get by names) n))))
8995+ $(ds t.ds, graph (~(put by graph) name.i.ds deps))
8996+::
8997+++ graph-add-reverse
8998+ |= [name=term edges=(list term) reverse=iadj]
8999+ ^- iadj
9000+ ?~ edges reverse
9001+ =/ prior=(list term) (graph-edges i.edges reverse)
9002+ $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
9003+::
9004+++ graph-reverse
9005+ |= [names=(list term) graph=iadj reverse=iadj]
9006+ ^- iadj
9007+ ?~ names reverse
9008+ =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
9009+ $(names t.names)
9010+::
9011+++ graph-order
9012+ |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
9013+ ^- iwresult
9014+ ?~ todo [seen order]
9015+ =/ event=[name=term done=?] i.todo
9016+ ?: done.event $(todo t.todo, order [name.event order])
9017+ ?: ?=(^ (~(get by seen) name.event)) $(todo t.todo)
9018+ =. seen (~(put by seen) name.event &)
9019+ =/ children=iwork (turn (graph-edges name.event graph) |=(n=term [n |]))
9020+ $(todo (weld children [[name.event &] t.todo]))
9021+::
9022+++ graph-collect
9023+ |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
9024+ ^- icresult
9025+ ?~ todo [seen component]
9026+ ?: ?=(^ (~(get by seen) i.todo)) $(todo t.todo)
9027+ =. seen (~(put by seen) i.todo &)
9028+ $(todo (weld (graph-edges i.todo graph) t.todo), component [i.todo component])
9029+::
9030+++ graph-collect-all
9031+ |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
9032+ ^- icomponents
9033+ ?~ order comps
9034+ ?: ?=(^ (~(get by seen) i.order)) $(order t.order)
9035+ =/ found=icresult (graph-collect ~[i.order] seen ~ graph)
9036+ $(order t.order, seen seen.found, comps [component.found comps])
9037+::
9038+:: Two depth-first passes find components before group inference. Maps
9039+:: preserve the graph identity; duplicate global names fail closed.
9040+++ graph-components
9041+ |= [ds=(list def) names=(list term)]
9042+ ^- icomponents
9043+ =/ nameset=ivisited ~
9044+ =/ pending=(list term) names
9045+ |-
9046+ ?^ pending
9047+ ?: ?=(^ (~(get by nameset) i.pending)) ~
9048+ $(pending t.pending, nameset (~(put by nameset) i.pending &))
9049+ =/ graph=iadj (graph-make-forward ds nameset ~)
9050+ =/ reverse=iadj (graph-reverse names graph ~)
9051+ =/ order=iwresult (graph-order (turn names |=(n=term [n |])) ~ ~ graph)
9052+ (graph-collect-all order.order ~ reverse ~)
9053+::
9054+++ graph-cycle
9055+ |= [component=(list term) graph=iadj]
9056+ ^- ?
9057+ ?~ component |
9058+ ?^ t.component &
9059+ (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
9060+::
9061+++ add-groups
9062+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
9063+ ^- iresolved
9064+ ?~ components [env grouped artifacts]
9065+ =/ component=(list term) i.components
9066+ ?. (graph-cycle component graph) $(components t.components)
9067+ ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
9068+ =/ members=(list def)
9069+ %+ skim ds
9070+ |= d=def
9071+ &(?=(%value -.d) (lien component |=(n=term =(n name.d))))
9072+ ?. =((lent members) (lent component)) $(components t.components)
9073+ ?. (levy component |=(n=term (unique-value-name n globals.state))) $(components t.components)
9074+ =/ result=ilocal-result (infer-gate-group members env state)
9075+ ?: ?=(%| -.result) $(components t.components)
9076+ $(components t.components, env env.p.result, grouped (weld component grouped))
9077+::
9078+++ resolve-groups
9079+ |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]
9080+ ^- iresolved
9081+ =/ env=ienv ~
9082+ =/ grouped=(list term) ~
9083+ =/ artifacts=(list iwidth-definition) ~
9084+ =/ names=(list term) (global-value-names ds)
9085+ =/ nameset=ivisited (graph-nameset names ~)
9086+ =/ graph=iadj (graph-make-forward ds nameset ~)
9087+ =/ components=icomponents (graph-components ds names)
9088+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9089+ |-
9090+ =/ next=[env=ienv artifacts=(list iwidth-definition)]
9091+ (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)
9092+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
9093+ =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
9094+ ?: =(env env.out) out
9095+ $(env env.out, grouped grouped.out, artifacts artifacts.out)
9096+::
73629097++ resolve-supported-defs
73639098 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]
73649099 ^- ienv
7365− =/ env=ienv ~
9100+ env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
9101+::
9102+:: A diagnostic-only proof for a narrow syntactic value cycle. Every
9103+:: edge is an unqualified wing in a supported expression, and samples
9104+:: may not shadow global bindings. Unknown forms yield no conclusion.
9105++$ icyclesite [name=term at=span]
9106++$ icycle [name=term first=span next=span]
9107+++ cycle-sites-list
9108+ |= [xs=(list expr) globals=(list term) locals=(list term)]
9109+ ^- (unit (list icyclesite))
9110+ ?~ xs `~
9111+ =/ first=(unit (list icyclesite)) (cycle-sites i.xs globals locals)
9112+ ?~ first ~
9113+ =/ tail=(unit (list icyclesite)) $(xs t.xs)
9114+ ?~ tail ~
9115+ `(weld u.first u.tail)
9116+::
9117+++ cycle-sample-name
9118+ |= [sam=sample globals=(list term) locals=(list term)]
9119+ ^- (unit (unit term))
9120+ ?- -.sam
9121+ %bind
9122+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9123+ ``name.sam
9124+ %face
9125+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9126+ ``name.sam
9127+ %bare `~
9128+ * ~
9129+ ==
9130+::
9131+++ cycle-sites
9132+ |= [e=expr globals=(list term) locals=(list term)]
9133+ ^- (unit (list icyclesite))
9134+ ?- -.e
9135+ %wing
9136+ ?. ?=([@ ~] names.e) ~
9137+ `~[[i.names.e at.e]]
9138+ %lit `~
9139+ %str
9140+ ?: (lien pieces.e |=(p=piece ?=(%expr -.p))) ~
9141+ `~
9142+ %group $(e inner.e)
9143+ %body ?~(defs.e $(e final.e) ~)
9144+ %cast $(e val.e)
9145+ %gate
9146+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9147+ ?~ binder ~
9148+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9149+ $(e body.e, locals nested)
9150+ %gate-wide
9151+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9152+ ?~ binder ~
9153+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9154+ $(e body.e, locals nested)
9155+ %call
9156+ =/ first=(unit (list icyclesite)) $(e head.e)
9157+ ?~ first ~
9158+ =/ tail=(unit (list icyclesite)) (cycle-sites-list args.e globals locals)
9159+ ?~ tail ~
9160+ `(weld u.first u.tail)
9161+ * ~
9162+ ==
9163+::
9164+++ cycle-definitely-atom
9165+ |= e=expr
9166+ ^- ?
9167+ ?: ?=(%group -.e) $(e inner.e)
9168+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9169+ ?. ?=(%cast -.e) |
9170+ |(?=(%aura -.shape.e) ?=(%flag -.shape.e))
9171+::
9172+++ cycle-proof-group
9173+ |= [members=(list def) globals=(list term)]
9174+ ^- ?
9175+ ?~ members &
9176+ ?. ?=(%value -.i.members) |
9177+ ?. (unique-value-name name.i.members globals) |
9178+ ?. ?=(^ (cycle-sites val.i.members globals ~)) |
9179+ $(members t.members)
9180+::
9181+++ cycle-find-site
9182+ |= [sites=(list icyclesite) component=(list term)]
9183+ ^- (unit span)
9184+ ?~ sites ~
9185+ ?: (lien component |=(n=term =(n name.i.sites))) `at.i.sites
9186+ $(sites t.sites)
9187+::
9188+++ cycle-group-errors
9189+ |= [members=(list def) component=(list term) globals=(list term)]
9190+ ^- (list icycle)
9191+ ?~ members ~
9192+ =/ d=def i.members
9193+ ?> ?=(%value -.d)
9194+ =/ tail=(list icycle) $(members t.members)
9195+ ?. (cycle-definitely-atom val.d) tail
9196+ =/ sites=(unit (list icyclesite)) (cycle-sites val.d globals ~)
9197+ ?~ sites tail
9198+ =/ found=(unit span) (cycle-find-site u.sites component)
9199+ ?~ found tail
9200+ [[name.d at.d u.found] tail]
9201+::
9202+++ definite-value-cycles
9203+ |= [ds=(list def) globals=(list term)]
9204+ ^- (list icycle)
9205+ =/ names=(list term) (global-value-names ds)
9206+ =/ graph=iadj (graph-make-forward ds (graph-nameset names ~) ~)
9207+ =/ components=icomponents (graph-components ds names)
9208+ =/ out=(list icycle) ~
73669209 |-
7367− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
7368− ?: =(next env) env
7369− $(env next)
9210+ ?~ components out
9211+ =/ component=(list term) i.components
9212+ ?. (graph-cycle component graph) $(components t.components)
9213+ =/ members=(list def)
9214+ (skim ds |=(d=def &(?=(%value -.d) (lien component |=(n=term =(n name.d))))))
9215+ ?. =((lent members) (lent component)) $(components t.components)
9216+ ?. (cycle-proof-group members globals) $(components t.components)
9217+ $(components t.components, out (weld (cycle-group-errors members component globals) out))
73709218::
73719219+| %union-analysis
73729220::
@@ -7503,11 +9351,142 @@
75039351 [at.first at.second (union-relate a (project-union-mold second molds ~))]
75049352 (weld pairs $(cases t.cases))
75059353::
9354+:: A closed structural mold supplies no equation to determine a hole.
9355+:: Applications, references, unbound capitals and unions are unproved.
9356+++ simple-mold-hole
9357+ |= sh=shape
9358+ ^- (unit (unit span))
9359+ ?: ?=(%generic -.sh)
9360+ ?~ vars.sh ~
9361+ ?. (distinct-params vars.sh) ~
9362+ (simple-mold-hole-in body.sh vars.sh)
9363+ (simple-mold-hole-in sh ~)
9364+++ simple-mold-hole-in
9365+ |= [sh=shape vars=(list @t)]
9366+ ^- (unit (unit span))
9367+ ?- -.sh
9368+ %hole ``at.sh
9369+ ?(%aura %noun %void %flag %const) `~
9370+ %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
9371+ %cell (simple-mold-field-holes fields.sh vars)
9372+ %fn
9373+ =/ a=(unit (unit span)) $(sh sample.sh)
9374+ ?~ a ~
9375+ =/ b=(unit (unit span)) $(sh product.sh)
9376+ ?~ b ~
9377+ `?~(u.a u.b u.a)
9378+ %generic ~
9379+ * ~
9380+ ==
9381+++ simple-mold-field-holes
9382+ |= [fields=(list field) vars=(list @t)]
9383+ ^- (unit (unit span))
9384+ ?~ fields `~
9385+ =/ f=field i.fields
9386+ =/ first=(unit (unit span))
9387+ ?- -.f
9388+ %face (simple-mold-hole-in shape.f vars)
9389+ %bare (simple-mold-hole-in shape.f vars)
9390+ %pun ~
9391+ ==
9392+ ?~ first ~
9393+ =/ rest=(unit (unit span)) $(fields t.fields)
9394+ ?~ rest ~
9395+ `?~(u.first u.rest u.first)
9396+++ simple-local-mold-hole
9397+ |= defs=(list def)
9398+ ^- (unit span)
9399+ ?~ defs ~
9400+ ?. ?=(%mold -.i.defs) $(defs t.defs)
9401+ =/ found=(unit (unit span)) (simple-mold-hole shape.i.defs)
9402+ ?~ found $(defs t.defs)
9403+ ?^ u.found u.found
9404+ $(defs t.defs)
9405+::
9406+:: A partial prelude may omit unsupported declarations, but may not
9407+:: publish an interface while a named mold's hole remains unchecked.
9408+++ shape-has-hole
9409+ |= sh=shape
9410+ ^- ?
9411+ ?- -.sh
9412+ %hole &
9413+ %path (lien segs.sh |=(s=pseg ?=(%inferred -.s)))
9414+ %apply (lien args.sh shape-has-hole)
9415+ %union (lien cases.sh shape-has-hole)
9416+ %cell (lien fields.sh field-has-hole)
9417+ %fn |($(sh sample.sh) $(sh product.sh))
9418+ %generic $(sh body.sh)
9419+ * |
9420+ ==
9421+++ field-has-hole
9422+ |= f=field
9423+ ^- ?
9424+ ?- -.f
9425+ %face (shape-has-hole shape.f)
9426+ %bare (shape-has-hole shape.f)
9427+ %pun |
9428+ ==
9429+++ named-mold-has-hole
9430+ |= ds=(list def)
9431+ ^- ?
9432+ ?~ ds |
9433+ ?: &(?=(%mold -.i.ds) (shape-has-hole shape.i.ds)) &
9434+ $(ds t.ds)
9435+::
9436+++ sample-has-hole
9437+ |= sam=sample
9438+ ^- ?
9439+ ?- -.sam
9440+ %face (shape-has-hole shape.sam)
9441+ %bare (shape-has-hole shape.sam)
9442+ %cell (lien items.sam sample-has-hole)
9443+ * |
9444+ ==
9445+++ def-has-hole
9446+ |= d=def
9447+ ^- ?
9448+ ?- -.d
9449+ %mold (shape-has-hole shape.d)
9450+ %value (expr-has-hole val.d)
9451+ ==
9452+++ expr-has-hole
9453+ |= e=expr
9454+ ^- ?
9455+ ?- -.e
9456+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9457+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9458+ %change (lien edits.e |=(p=edit (expr-has-hole val.p)))
9459+ %pair $(e val.e)
9460+ %unit $(e val.e)
9461+ %group $(e inner.e)
9462+ %list (lien items.e expr-has-hole)
9463+ %tuple (lien items.e |=(i=item (expr-has-hole val.i)))
9464+ ?(%gate %gate-wide) |((sample-has-hole sample.e) $(e body.e))
9465+ %cast |((shape-has-hole shape.e) $(e val.e))
9466+ %call |($(e head.e) (lien args.e expr-has-hole))
9467+ %trace |($(e val.e) $(e then.e))
9468+ %branch |($(e subject.e) (lien arms.e |=(a=arm (expr-has-hole val.a))))
9469+ %body |((lien defs.e def-has-hole) $(e final.e))
9470+ * |
9471+ ==
9472+++ hole-values-present
9473+ |= [ds=(list def) env=ienv]
9474+ ^- ?
9475+ ?~ ds &
9476+ ?. ?=(%value -.i.ds) $(ds t.ds)
9477+ ?: (expr-has-hole val.i.ds)
9478+ ?. ?=(^ (ienv-lookup name.i.ds env)) |
9479+ $(ds t.ds)
9480+ $(ds t.ds)
75069481++ show-partial-mold
75079482 |= [file=path src=@t d=def molds=imolds]
75089483 ^- @t
75099484 ?> ?=(%mold -.d)
75109485 =/ sh=shape shape.d
9486+ =/ hole=(unit (unit span)) (simple-mold-hole sh)
9487+ ?: &(?=(^ hole) ?=(^ u.hole))
9488+ =/ text=@t (show-error src [file line.beg.u.u.hole col.beg.u.u.hole "unresolved type hole"])
9489+ (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])
75119490 =? sh ?=(%generic -.sh) body.sh
75129491 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
75139492 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -7534,6 +9513,21 @@
75349513 (show-error src [file line.beg.at.site col.beg.at.site note.site])
75359514 (of-wain:format [summary excerpts])
75369515::
9516+:: Both written field sites are shown in the source that declares them.
9517+++ show-duplicate-fields
9518+ |= [file=path src=@t diagnostic=idiag]
9519+ ^- @t
9520+ =/ excerpts=(list @t)
9521+ %+ turn sites.diagnostic
9522+ |= site=[at=span note=tape]
9523+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
9524+ (of-wain:format [(crip msg.diagnostic) excerpts])
9525+::
9526+++ duplicate-fields-report
9527+ |= [file=path src=@t diagnostic=idiag]
9528+ ^- @t
9529+ (of-wain:format ~['partial inference; module not checked' (show-duplicate-fields file src diagnostic)])
9530+::
75379531:: +golden-types: a partial report; it does not claim the module checks
75389532::
75399533++ golden-types
@@ -7563,6 +9557,180 @@
75639557+$ jfile-result (each [iface=ifile cache=jcache] @t)
75649558+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
75659559::
9560+:: Written record fields each have their own lexical record scope.
9561++$ written-fields (map term span)
9562+++ duplicate-written-field
9563+ |= [name=term at=span seen=written-fields]
9564+ ^- (unit idiag)
9565+ =/ prior=(unit span) (~(get by seen) name)
9566+ ?~ prior ~
9567+ `["record field `{(trip name)}` is repeated" ~[[u.prior "first field"] [at "repeated field"]]]
9568+++ duplicate-shapes
9569+ |= xs=(list shape)
9570+ ^- (unit idiag)
9571+ ?~ xs ~
9572+ =/ first (duplicate-shape i.xs)
9573+ ?^ first first
9574+ $(xs t.xs)
9575+++ duplicate-fields
9576+ |= [fields=(list field) seen=written-fields]
9577+ ^- (unit idiag)
9578+ ?~ fields ~
9579+ =/ f=field i.fields
9580+ =/ n=(unit term)
9581+ ?- -.f
9582+ %face `name.f
9583+ %pun `name.f
9584+ %bare ~
9585+ ==
9586+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.f seen))
9587+ ?^ dup dup
9588+ =/ inner=(unit idiag)
9589+ ?- -.f
9590+ %face (duplicate-shape shape.f)
9591+ %pun ~
9592+ %bare (duplicate-shape shape.f)
9593+ ==
9594+ ?^ inner inner
9595+ $(fields t.fields, seen ?~(n seen (~(put by seen) u.n at.f)))
9596+++ duplicate-shape
9597+ |= s=shape
9598+ ^- (unit idiag)
9599+ ?- -.s
9600+ %cell (duplicate-fields fields.s ~)
9601+ %apply (duplicate-shapes args.s)
9602+ %union (duplicate-shapes cases.s)
9603+ %fn
9604+ =/ left (duplicate-shape sample.s)
9605+ ?^ left left
9606+ (duplicate-shape product.s)
9607+ %generic (duplicate-shape body.s)
9608+ * ~
9609+ ==
9610+++ duplicate-samples
9611+ |= [items=(list sample) seen=written-fields]
9612+ ^- (unit idiag)
9613+ ?~ items ~
9614+ =/ a=sample i.items
9615+ =/ n=(unit term)
9616+ ?- -.a
9617+ %bind `name.a
9618+ %face `name.a
9619+ %pun `name.a
9620+ * ~
9621+ ==
9622+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.a seen))
9623+ ?^ dup dup
9624+ =/ inner (duplicate-sample a)
9625+ ?^ inner inner
9626+ $(items t.items, seen ?~(n seen (~(put by seen) u.n at.a)))
9627+++ duplicate-sample
9628+ |= s=sample
9629+ ^- (unit idiag)
9630+ ?- -.s
9631+ %cell (duplicate-samples items.s ~)
9632+ %face (duplicate-shape shape.s)
9633+ %bare (duplicate-shape shape.s)
9634+ * ~
9635+ ==
9636+++ duplicate-exprs
9637+ |= xs=(list expr)
9638+ ^- (unit idiag)
9639+ ?~ xs ~
9640+ =/ first (duplicate-expr i.xs)
9641+ ?^ first first
9642+ $(xs t.xs)
9643+++ duplicate-items
9644+ |= [items=(list item) seen=written-fields]
9645+ ^- (unit idiag)
9646+ ?~ items ~
9647+ =/ a=item i.items
9648+ =/ dup=(unit idiag) ?~(face.a ~ (duplicate-written-field u.face.a at.a seen))
9649+ ?^ dup dup
9650+ =/ inner (duplicate-expr val.a)
9651+ ?^ inner inner
9652+ $(items t.items, seen ?~(face.a seen (~(put by seen) u.face.a at.a)))
9653+++ duplicate-pieces
9654+ |= pieces=(list piece)
9655+ ^- (unit idiag)
9656+ ?~ pieces ~
9657+ =/ first=(unit idiag) ?:(?=(%expr -.i.pieces) (duplicate-expr p.i.pieces) ~)
9658+ ?^ first first
9659+ $(pieces t.pieces)
9660+++ duplicate-qsegs
9661+ |= segs=(list qseg)
9662+ ^- (unit idiag)
9663+ ?~ segs ~
9664+ =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
9665+ ?^ first first
9666+ $(segs t.segs)
9667+++ duplicate-edits
9668+ |= edits=(list edit)
9669+ ^- (unit idiag)
9670+ ?~ edits ~
9671+ =/ first (duplicate-expr val.i.edits)
9672+ ?^ first first
9673+ $(edits t.edits)
9674+++ duplicate-arms
9675+ |= arms=(list arm)
9676+ ^- (unit idiag)
9677+ ?~ arms ~
9678+ =/ first (duplicate-expr val.i.arms)
9679+ ?^ first first
9680+ $(arms t.arms)
9681+++ duplicate-defs
9682+ |= defs=(list def)
9683+ ^- (unit idiag)
9684+ ?~ defs ~
9685+ =/ first=(unit idiag)
9686+ ?- -.i.defs
9687+ %mold (duplicate-shape shape.i.defs)
9688+ %value (duplicate-expr val.i.defs)
9689+ ==
9690+ ?^ first first
9691+ $(defs t.defs)
9692+++ duplicate-expr
9693+ |= e=expr
9694+ ^- (unit idiag)
9695+ ?- -.e
9696+ %str (duplicate-pieces pieces.e)
9697+ %qath (duplicate-qsegs segs.e)
9698+ %change (duplicate-edits edits.e)
9699+ %pair (duplicate-expr val.e)
9700+ %unit (duplicate-expr val.e)
9701+ %group (duplicate-expr inner.e)
9702+ %list (duplicate-exprs items.e)
9703+ %tuple (duplicate-items items.e ~)
9704+ %gate-wide
9705+ =/ first (duplicate-sample sample.e)
9706+ ?^ first first
9707+ (duplicate-expr body.e)
9708+ %gate
9709+ =/ first (duplicate-sample sample.e)
9710+ ?^ first first
9711+ (duplicate-expr body.e)
9712+ %cast
9713+ =/ first (duplicate-shape shape.e)
9714+ ?^ first first
9715+ (duplicate-expr val.e)
9716+ %call
9717+ =/ first (duplicate-expr head.e)
9718+ ?^ first first
9719+ (duplicate-exprs args.e)
9720+ %trace
9721+ =/ first (duplicate-expr val.e)
9722+ ?^ first first
9723+ (duplicate-expr then.e)
9724+ %branch
9725+ =/ first (duplicate-expr subject.e)
9726+ ?^ first first
9727+ (duplicate-arms arms.e)
9728+ %body
9729+ =/ first (duplicate-defs defs.e)
9730+ ?^ first first
9731+ (duplicate-expr final.e)
9732+ * ~
9733+ ==
75669734++ import-binding-names
75679735 |= imports=(list import)
75689736 ^- (list term)
@@ -7575,6 +9743,60 @@
75759743 ==
75769744 [n $(imports t.imports)]
75779745::
9746+++ reserved-proj-sample
9747+ |= sam=sample
9748+ ^- ?
9749+ ?- -.sam
9750+ %bind =(name.sam %proj)
9751+ %face =(name.sam %proj)
9752+ %pun =(name.sam %proj)
9753+ %cell (lien items.sam reserved-proj-sample)
9754+ * |
9755+ ==
9756+++ reserved-proj-pattern
9757+ |= p=pattern
9758+ ^- ?
9759+ ?- -.p
9760+ %bind =(name.p %proj)
9761+ %cell (lien items.p reserved-proj-pattern)
9762+ * |
9763+ ==
9764+++ reserved-proj-def
9765+ |= d=def
9766+ ^- ?
9767+ ?: =(name.d %proj) &
9768+ ?: ?=(%value -.d) (reserved-proj-expr val.d)
9769+ |
9770+++ reserved-proj-expr
9771+ |= e=expr
9772+ ^- ?
9773+ ?- -.e
9774+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
9775+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
9776+ %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
9777+ %pair $(e val.e)
9778+ %unit $(e val.e)
9779+ %group $(e inner.e)
9780+ %list (lien items.e reserved-proj-expr)
9781+ %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
9782+ ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
9783+ %cast $(e val.e)
9784+ %call |($(e head.e) (lien args.e reserved-proj-expr))
9785+ %trace |($(e val.e) $(e then.e))
9786+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
9787+ %body |((lien defs.e reserved-proj-def) $(e final.e))
9788+ * |
9789+ ==
9790+::
9791+++ module-has-reserved-proj
9792+ |= mod=module
9793+ ^- ?
9794+ =/ imported=(list term) (import-binding-names imports.mod)
9795+ =/ vals=(list term) (global-value-names defs.mod)
9796+ =/ molds=imolds (collect-simple-molds defs.mod)
9797+ =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9798+ |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
9799+::
75789800++ module-scope-valid
75799801 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
75809802 ^- ?
@@ -7582,6 +9804,7 @@
75829804 =/ vals=(list term) (global-value-names defs.mod)
75839805 =/ molds=imolds (collect-simple-molds defs.mod)
75849806 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9807+ ?: (module-has-reserved-proj mod) |
75859808 ?. %+ levy imported
75869809 |= n=term
75879810 &((unique-value-name n imported) !(lien vals |=(v=term =(n v))) !(lien mold-names |=(m=term =(n m))) !(lien prelude-values |=(v=term =(n v))) !(lien prelude-molds |=(m=term =(n m))))
@@ -7589,6 +9812,22 @@
75899812 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
75909813 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
75919814::
9815+:: In an API file or before main's kind is known, a lone `+$ poke`
9816+:: may be a declaration rather than a mold that shadows the prelude. Do not call
9817+:: that one collision definite, and do not hide unrelated scope errors.
9818+++ pending-declared-poke
9819+ |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
9820+ ^- ?
9821+ ?. (lien prelude-molds |=(n=term =(%poke n))) |
9822+ ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
9823+ =/ pokes=(list def)
9824+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
9825+ ?~ pokes |
9826+ ?^ t.pokes |
9827+ =/ remaining=(list def)
9828+ (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
9829+ (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
9830+::
75929831++ module-mold-types
75939832 |= [molds=imolds state=istate]
75949833 ^- (each imold-types @t)
@@ -7604,9 +9843,9 @@
76049843::
76059844:: Prepare a provisional interface from the trusted vendored source.
76069845:: Every declared name remains reserved, but only molds and values this
7607−:: fragment can infer are usable. Unsupported bodies are not validated,
7608−:: and imports into the prelude are not supported yet. The fixed origin
7609−:: gives its named unions the same identity in every importing module.
9846+:: fragment can infer are usable. Unsupported bodies are not validated.
9847+:: An optional internal source supplies the prelude's one supported import;
9848+:: clients cannot import that path directly. Named unions retain their origin.
76109849::
76119850:: Recognize only the complete standard prelude list shape. Its recursive
76129851:: tail uses the same parameter and the unqualified list name. The reader
@@ -7646,6 +9885,14 @@
76469885 ?. ?=(%tvar -.i.args.tail) |
76479886 =(var name.i.args.tail)
76489887::
9888+++ prelude-label
9889+ |= [typ=itype name=term]
9890+ ^- itype
9891+ ?: ?=(%jrec -.typ) typ(label `name)
9892+ ?. ?=(%union -.typ) typ
9893+ ?^ args.typ typ
9894+ typ(label `name)
9895+::
76499896++ partial-prelude-molds
76509897 |= [molds=imolds state=istate]
76519898 ^- imold-types
@@ -7658,22 +9905,72 @@
76589905 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
76599906 ?~ out $(molds t.molds)
76609907 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
9908+ =. typ.template.u.out (prelude-label typ.template.u.out name.m)
76619909 [[name.m template.u.out] $(molds t.molds)]
76629910::
7663−++ partial-prelude-interface
9911+:: A compiler-owned interface available only to the dedicated
9912+:: internal-prelude preparation path, never the ordinary module resolver.
9913+++ private-primitive-interface
9914+ ^- ifile
9915+ =/ a=itype [%avar 0]
9916+ =/ pair=itype [%cell a a]
9917+ =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
9918+ [~[[%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~]
9919+::
9920+++ infer-private-internal
76649921 |= src=@t
76659922 ^- (unit ifile)
9923+ =/ at=path /lib/jibb/internal/jibb
9924+ =/ parsed (parse at src)
9925+ ?: ?=(%| -.parsed) ~
9926+ =/ mod=module p.parsed
9927+ ?^ (duplicate-defs defs.mod) ~
9928+ ?~ imports.mod
9929+ =/ built=jfile-result (infer-jibb-file at src ~ ~ ~ ~[at] ~ ~ ~ ~)
9930+ ?: ?=(%| -.built) ~
9931+ `iface.p.built
9932+ ?. ?=([[%jibb *] ~] imports.mod) ~
9933+ ?. =(path.i.imports.mod /lib/jibb/primitives) ~
9934+ ?. (module-scope-valid mod ~ ~) ~
9935+ =/ vals=(list term) (global-value-names defs.mod)
9936+ ?: (lien vals |=(n=term =(n %main))) ~
9937+ =/ molds=imolds (collect-simple-molds defs.mod)
9938+ =/ globals=(list term) (weld (import-binding-names imports.mod) vals)
9939+ =/ js=ijimports ~[[face.i.imports.mod private-primitive-interface]]
9940+ =/ reserved=(list term) ~[face.i.imports.mod]
9941+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9942+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~]
9943+ =/ mts=(each imold-types @t) (module-mold-types molds state)
9944+ ?: ?=(%| -.mts) ~
9945+ =/ resolution=iresolved (resolve-groups defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
9946+ =/ env=ienv env.resolution
9947+ ?. (module-values-complete defs.mod env) ~
9948+ `[env p.mts at ~ artifacts.resolution ~ `src]
9949+::
9950+++ partial-prelude-interface-with-internal
9951+ |= [src=@t internal-source=(unit @t)]
9952+ ^- (unit ifile)
76669953 ?: =(0 src) ~
76679954 =/ at=path /lib/jibb/prelude/jibb
76689955 =/ parsed (parse at src)
76699956 ?: ?=(%| -.parsed) ~
7670− ?^ imports.p.parsed ~
9957+ ?: (named-mold-has-hole defs.p.parsed) ~
9958+ ?^ (duplicate-defs defs.p.parsed) ~
9959+ =/ private=(unit ijimports)
9960+ ?~ imports.p.parsed `~
9961+ ?. ?=([[%jibb *] ~] imports.p.parsed) ~
9962+ ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
9963+ ?~ internal-source ~
9964+ =/ built=(unit ifile) (infer-private-internal u.internal-source)
9965+ ?~ built ~
9966+ `~[[face.i.imports.p.parsed u.built]]
9967+ ?~ private ~
76719968 ?~ defs.p.parsed ~
76729969 ?. (module-scope-valid p.parsed ~ ~) ~
76739970 =/ ds=(list def) defs.p.parsed
76749971 =/ molds=imolds (collect-simple-molds ds)
76759972 =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7676− =/ globals=(list term) (global-value-names ds)
9973+ =/ globals=(list term) (weld (import-binding-names imports.p.parsed) (global-value-names ds))
76779974 :: Remove raw list before inferring any template, so an altered list
76789975 :: cannot leak through an alias. Its name remains reserved either way.
76799976 =/ declared=? (lien names |=(name=term =(%list name)))
@@ -7681,11 +9978,38 @@
76819978 =? env-molds declared
76829979 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
76839980 =/ reserved=(list term) ?:(declared ~[%list] ~)
7684− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ ~ reserved ~ ~ ~ | at names ~]
7685− =/ mt=imold-types (partial-prelude-molds molds state)
7686− =/ partial=ifile [~ mt at]
7687− =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ ~ reserved at `partial)
7688− `[env mt at]
9981+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~]
9982+ :: Other prelude molds may use list only after its source has passed
9983+ :: the standard-list check. The raw declaration remains removed.
9984+ =/ declared-list=(unit shape) (find-simple-mold %list molds)
9985+ =/ mold-prelude=(unit ifile)
9986+ ?~ declared-list ~
9987+ ?. (standard-prelude-list u.declared-list) ~
9988+ `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~]
9989+ =/ mt=imold-types (partial-prelude-molds molds state(prelude mold-prelude))
9990+ =/ partial=ifile [~ mt at ~ ~ ~ ~]
9991+ :: An explicitly qualified re-export must resolve. Other unsupported
9992+ :: prelude declarations remain reserved but absent from the interface.
9993+ =/ required=imolds
9994+ %+ skim molds
9995+ |= m=[name=term body=shape]
9996+ =/ sh=shape body.m
9997+ ?. ?=(%ref -.sh) |
9998+ ?~ names.sh |
9999+ ?=(^ t.names.sh)
10000+ ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
10001+ =/ resolution=iresolved (resolve-groups ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
10002+ =/ env=ienv env.resolution
10003+ ?. (hole-values-present ds env) ~
10004+ =/ deps=(list iwidth-dependency)
10005+ ?~ u.private ~
10006+ ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
10007+ `[env mt at ~ artifacts.resolution deps `src]
10008+::
10009+++ partial-prelude-interface
10010+ |= src=@t
10011+ ^- (unit ifile)
10012+ (partial-prelude-interface-with-internal src ~)
768910013::
769010014+$ iprelude [iface=ifile values=(list term) molds=(list term)]
769110015::
@@ -7700,6 +10024,17 @@
770010024 =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
770110025 `[u.iface vals ms]
770210026::
10027+++ prepare-prelude-with-internal
10028+ |= [src=@t internal-source=@t]
10029+ ^- (unit iprelude)
10030+ =/ iface=(unit ifile) (partial-prelude-interface-with-internal src `internal-source)
10031+ ?~ iface ~
10032+ =/ parsed (parse /lib/jibb/prelude/jibb src)
10033+ ?: ?=(%| -.parsed) ~
10034+ =/ vals=(list term) (global-value-names defs.p.parsed)
10035+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
10036+ `[u.iface vals ms]
10037+::
770310038++ module-values-complete
770410039 |= [ds=(list def) env=ienv]
770510040 ^- ?
@@ -7726,6 +10061,10 @@
772610061 ?~ imports [%& [~ cache]]
772710062 ?. ?=(%jibb -.i.imports) $(imports t.imports)
772810063 =/ at=path (weld path.i.imports `path`~[%jibb])
10064+ ?: =(at /lib/jibb/internal/jibb)
10065+ [%| 'the prelude internal module is private']
10066+ ?: =(at /lib/jibb/primitives/jibb)
10067+ [%| 'the prelude primitive interface is private']
772910068 ?: (lien active |=(p=path =(p at)))
773010069 [%| (crip "import cycle at {(spud at)}")]
773110070 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -7740,14 +10079,287 @@
774010079 ?: ?=(%| -.rest) rest
774110080 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
774210081::
10082+:: Provisional declaration extraction only; this does not derive asks,
10083+:: validate imported types, or claim that an API module has checked.
10084++$ iapi-path [at=span name=term segments=(list pseg) full=term diffs=(list term) scry=(unit (list pseg))]
10085+++ api-path-mark
10086+ |= [sh=shape marks=(list term)]
10087+ ^- (unit term)
10088+ ?. ?=(%ref -.sh) ~
10089+ ?. ?=([@ ~] names.sh) ~
10090+ ?. (unique-value-name i.names.sh marks) ~
10091+ `i.names.sh
10092+::
10093+++ api-path-diffs
10094+ |= [shapes=(list shape) marks=(list term) used=(list term)]
10095+ ^- (unit (list term))
10096+ ?~ shapes `~
10097+ =/ n=(unit term) (api-path-mark i.shapes marks)
10098+ ?~ n ~
10099+ ?: (lien used |=(x=term =(x u.n))) ~
10100+ =/ rest=(unit (list term)) $(shapes t.shapes, used [u.n used])
10101+ ?~ rest ~
10102+ `[u.n u.rest]
10103+::
10104+++ api-path-payload
10105+ |= [sh=shape marks=(list term)]
10106+ ^- (unit [full=term diffs=(list term)])
10107+ =/ direct=(unit term) (api-path-mark sh marks)
10108+ ?^ direct `[u.direct ~]
10109+ ?. ?=(%apply -.sh) ~
10110+ ?. =(~[%facts] ref.sh) ~
10111+ ?~ args.sh ~
10112+ ?~ t.args.sh ~
10113+ =/ full=(unit term) (api-path-mark i.args.sh marks)
10114+ ?~ full ~
10115+ =/ diffs=(unit (list term)) (api-path-diffs t.args.sh marks ~[u.full])
10116+ ?~ diffs ~
10117+ `[u.full u.diffs]
10118+::
10119++$ iapi-parameter [name=term aura=@ta at=span]
10120+++ api-path-parameters
10121+ |= [segments=(list pseg) seen=(list term)]
10122+ ^- (unit (list iapi-parameter))
10123+ ?~ segments `~
10124+ ?: ?=(%knot -.i.segments) $(segments t.segments)
10125+ =/ seg=pseg i.segments
10126+ ?. ?=(%typed -.seg) ~
10127+ ?: =(0 aura.seg) ~
10128+ ?: (lien seen |=(n=term =(n name.seg))) ~
10129+ =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
10130+ ?~ rest ~
10131+ `[[name.seg aura.seg at.seg] u.rest]
10132+::
10133+++ api-scry-parameters-compatible
10134+ |= [scry=(list iapi-parameter) watch=(list iapi-parameter)]
10135+ ^- ?
10136+ ?~ scry &
10137+ ?. (lien watch |=(p=iapi-parameter &(=(name.p name.i.scry) =(aura.p aura.i.scry)))) |
10138+ $(scry t.scry)
10139+::
10140+++ api-path-one
10141+ |= [sh=shape marks=(list term)]
10142+ ^- (unit iapi-path)
10143+ ?. ?=(%cell -.sh) ~
10144+ =/ fs=(list field) fields.sh
10145+ ?~ fs ~
10146+ ?~ t.fs ~
10147+ ?~ t.t.fs ~
10148+ ?: (gth (lent fs) 4) ~
10149+ ?. ?=(%bare -.i.fs) ~
10150+ =/ tag=shape shape.i.fs
10151+ ?. ?=(%const -.tag) ~
10152+ ?. =(%term form.lit.tag) ~
10153+ =/ name=term val.lit.tag
10154+ ?. (jibb-face-name name) ~
10155+ ?. ?=(%bare -.i.t.fs) ~
10156+ =/ path-shape=shape shape.i.t.fs
10157+ ?. ?=(%path -.path-shape) ~
10158+ ?. ?=(%bare -.i.t.t.fs) ~
10159+ =/ payload=(unit [full=term diffs=(list term)]) (api-path-payload shape.i.t.t.fs marks)
10160+ ?~ payload ~
10161+ =/ scry=(unit (unit (list pseg)))
10162+ ?~ t.t.t.fs `~
10163+ =/ entry=field i.t.t.t.fs
10164+ ?. ?=(%face -.entry) ~
10165+ ?. =(%scry name.entry) ~
10166+ ?. ?=(%path -.shape.entry) ~
10167+ ``segs.shape.entry
10168+ ?~ scry ~
10169+ =/ params=(unit (list iapi-parameter)) (api-path-parameters segs.path-shape ~)
10170+ ?~ params ~
10171+ ?^ u.scry
10172+ =/ scry-params=(unit (list iapi-parameter)) (api-path-parameters u.u.scry ~)
10173+ ?~ scry-params ~
10174+ ?. (api-scry-parameters-compatible u.scry-params u.params) ~
10175+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
10176+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
10177+::
10178+++ api-path-many
10179+ |= [shapes=(list shape) marks=(list term) seen=(list term)]
10180+ ^- (unit (list iapi-path))
10181+ ?~ shapes `~
10182+ =/ one=(unit iapi-path) (api-path-one i.shapes marks)
10183+ ?~ one ~
10184+ ?: (lien seen |=(n=term =(n name.u.one))) ~
10185+ =/ rest=(unit (list iapi-path)) $(shapes t.shapes, seen [name.u.one seen])
10186+ ?~ rest ~
10187+ `[u.one u.rest]
10188+::
10189+++ api-path-declaration
10190+ |= [sh=shape marks=(list term)]
10191+ ^- (unit (list iapi-path))
10192+ ?: ?=(%union -.sh) (api-path-many cases.sh marks ~)
10193+ (api-path-many ~[sh] marks ~)
10194+::
10195+:: Derived gates share the value namespace. /% marks name molds; /- and
10196+:: /= also introduce faces that cannot be shadowed by a derived value.
10197+++ api-import-faces
10198+ |= imports=(list import)
10199+ ^- (list term)
10200+ ?~ imports ~
10201+ ?- -.i.imports
10202+ %mark $(imports t.imports)
10203+ %sur [name.i.imports $(imports t.imports)]
10204+ %jibb [face.i.imports $(imports t.imports)]
10205+ ==
10206+::
10207+++ api-derived-names-valid
10208+ |= [paths=(list iapi-path) poke-names=(list term) mod=module prelude-values=(list term)]
10209+ ^- ?
10210+ =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
10211+ =/ derived=(list term) (weld path-names poke-names)
10212+ ?: (lien derived |=(n=term =(n %proj))) |
10213+ =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
10214+ (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
10215+::
10216+:: Analysis only. Successful external entries must be unchanged results
10217+:: produced for the declared marks; no request interface is produced.
10218++$ iapi-mark-type [name=term typ=itype]
10219++$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
10220+++ api-diff-types
10221+ |= [names=(list term) externals=imark-externals declared=(list term)]
10222+ ^- (unit (list iapi-mark-type))
10223+ ?~ names `~
10224+ =/ typ=(unit itype) (find-imported-mark i.names externals declared)
10225+ ?~ typ ~
10226+ =/ tail=(unit (list iapi-mark-type)) $(names t.names)
10227+ ?~ tail ~
10228+ `[[i.names u.typ] u.tail]
10229+::
10230+++ api-path-types
10231+ |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
10232+ ^- (unit (list iapi-path-typed))
10233+ ?~ paths `~
10234+ =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
10235+ ?~ full ~
10236+ =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
10237+ ?~ diffs ~
10238+ =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
10239+ ?~ tail ~
10240+ `[[i.paths u.full u.diffs] u.tail]
10241+::
10242+++ api-poke-mark-names
10243+ |= [pokes=(list def) declared=(list term)]
10244+ ^- (unit (list term))
10245+ ?~ pokes `~
10246+ ?^ t.pokes ~
10247+ =/ d=def i.pokes
10248+ ?. ?=(%mold -.d) ~
10249+ =/ sh=shape shape.d
10250+ ?: ?=(%union -.sh) (api-path-diffs cases.sh declared ~)
10251+ =/ name=(unit term) (api-path-mark sh declared)
10252+ ?~ name ~
10253+ `~[u.name]
10254+::
10255+++ api-path-analysis
10256+ |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
10257+ ^- (unit (list iapi-path-typed))
10258+ ?: (lien defs.mod def-has-hole) ~
10259+ ?^ (duplicate-defs defs.mod) ~
10260+ =/ ds=(list def) defs.mod
10261+ =/ declarations=(list def)
10262+ (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
10263+ ?. ?=([* ~] declarations) ~
10264+ =/ pokes=(list def)
10265+ (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
10266+ ?: (gth (lent pokes) 1) ~
10267+ =/ ordinary=(list def)
10268+ (skim ds |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
10269+ ?. (module-scope-valid mod(defs ordinary) prelude-values prelude-molds) ~
10270+ =/ declared=(list term) (collect-mark-imports imports.mod)
10271+ =/ poke-names=(unit (list term)) (api-poke-mark-names pokes declared)
10272+ ?~ poke-names ~
10273+ =/ decl=def i.declarations
10274+ ?> ?=(%mold -.decl)
10275+ =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
10276+ ?~ paths ~
10277+ ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
10278+ (api-path-types u.paths externals declared)
10279+::
10280+:: Source/graph entry for path analysis only. The returned paths retain
10281+:: reader-derived mark types and import resolution has checked reachable
10282+:: Jibb dependencies. This is not an API interface or a module check.
10283+++ api-path-analysis-source
10284+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
10285+ ^- (each (list iapi-path-typed) @t)
10286+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
10287+ =/ parsed (parse file src)
10288+ ?: ?=(%| -.parsed) [%| 'API path source does not parse']
10289+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10290+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
10291+ ?~ prepared [%| 'API path analysis needs the prepared prelude']
10292+ =/ prelude=(unit ifile) `iface.u.prepared
10293+ =/ deps=jimports-result
10294+ (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
10295+ ?: ?=(%| -.deps) [%| p.deps]
10296+ =/ paths=(unit (list iapi-path-typed))
10297+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
10298+ ?~ paths [%| 'API path declaration needs unsupported analysis']
10299+ [%& u.paths]
10300+::
10301+++ api-mark-exports
10302+ |= [marks=(list term) all=(list term) externals=imark-externals]
10303+ ^- imold-types
10304+ ?~ marks ~
10305+ =/ t=(unit itype) (find-imported-mark i.marks externals all)
10306+ ?~ t $(marks t.marks)
10307+ [[i.marks [u.t ~]] $(marks t.marks)]
10308+::
10309+:: Experimental direct poke-only API. Unsupported API declarations fail
10310+:: as a whole; supplied mark reader results retain their existing boundary.
10311+++ api-poke-interface
10312+ |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
10313+ ^- (unit ifile)
10314+ ?: (lien defs.mod def-has-hole) ~
10315+ ?. ?=([%ui %api @ %jibb ~] at) ~
10316+ ?^ (duplicate-defs defs.mod) ~
10317+ ?~ prelude ~
10318+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
10319+ =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
10320+ ?~ poke ~
10321+ ?. ?=(%union -.typ.u.poke) ~
10322+ ?^ vars.u.poke ~
10323+ =/ compatible=?
10324+ %+ lien cases.typ.u.poke
10325+ |= c=itype
10326+ ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
10327+ ?. compatible ~
10328+ ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
10329+ ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
10330+ =/ marks=(list term) (collect-mark-imports imports.mod)
10331+ ?. ?=([@ ~] marks) ~
10332+ =/ ds=(list def) defs.mod
10333+ ?. ?=([[%mold *] ~] ds) ~
10334+ ?. =(%poke name.i.ds) ~
10335+ =/ sh=shape shape.i.ds
10336+ ?. ?=([%ref *] sh) ~
10337+ ?. ?=([@ ~] names.sh) ~
10338+ =/ n=term i.names.sh
10339+ ?. (unique-value-name n marks) ~
10340+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
10341+ =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
10342+ ?~ mark ~
10343+ =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
10344+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~]
10345+::
774310346++ infer-jibb-file
774410347 |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
774510348 ^- jfile-result
7746− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
774710349 =/ parsed (parse at src)
774810350 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
774910351 =/ mod=module p.parsed
7750− ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
10352+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
10353+ ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
10354+ ?: ?=([%ui %api *] at)
10355+ =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
10356+ ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
10357+ =/ checked=ifile u.iface(source `src)
10358+ [%& [checked [[at checked] cache]]]
10359+ ?. (module-scope-valid mod prelude-values prelude-molds)
10360+ ?: (pending-declared-poke at mod prelude-values prelude-molds)
10361+ [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
10362+ [%| (crip "module has conflicting names: {(spud at)}")]
775110363 =/ vals=(list term) (global-value-names defs.mod)
775210364 ?: (lien vals |=(n=term =(n %main)))
775310365 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
@@ -7759,13 +10371,15 @@
775910371 =/ marks=(list term) (collect-mark-imports imports.mod)
776010372 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
776110373 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7762− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
10374+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
776310375 =/ mts=(each imold-types @t) (module-mold-types molds state)
776410376 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
7765− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
10377+ =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
10378+ =/ env=ienv env.resolution
776610379 ?. (module-values-complete defs.mod env)
776710380 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
7768− [%& [[env p.mts at] [[at [env p.mts at]] cache.p.js]]]
10381+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src]
10382+ [%& [iface [[at iface] cache.p.js]]]
776910383::
777010384:: +golden-types-with-modules fails closed for imports without prelude
777110385:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -7776,6 +10390,8 @@
777610390 ^- @t
777710391 =/ parsed (parse file src)
777810392 ?: ?=(%| -.parsed) (show-error src p.parsed)
10393+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10394+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
777910395 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
778010396 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
778110397 (golden-types-with-marks file src externals mark-externals)
@@ -7790,6 +10406,8 @@
779010406 ^- @t
779110407 =/ parsed (parse file src)
779210408 ?: ?=(%| -.parsed) (show-error src p.parsed)
10409+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10410+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
779310411 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
779410412 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
779510413 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
@@ -7797,16 +10415,26 @@
779710415 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
779810416 (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
779910417::
10418+++ golden-types-with-prelude-and-internal
10419+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t internal-source=@t]
10420+ ^- @t
10421+ =/ prepared=(unit iprelude) (prepare-prelude-with-internal prelude-source internal-source)
10422+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
10423+::
780010424++ golden-types-with-prepared-prelude
780110425 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
780210426 ^- @t
780310427 =/ parsed (parse file src)
780410428 ?: ?=(%| -.parsed) (show-error src p.parsed)
10429+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10430+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
780510431 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
780610432 =/ prelude-values=(list term) values.u.prepared
780710433 =/ prelude-molds=(list term) molds.u.prepared
780810434 =/ iface=(unit ifile) `iface.u.prepared
780910435 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
10436+ ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
10437+ 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
781010438 'partial inference; module not checked\0amodule has conflicting names'
781110439 =/ js=jimports-result
781210440 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
@@ -7847,12 +10475,18 @@
784710475 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
784810476 =/ parsed (parse file src)
784910477 ?: ?=(%| -.parsed) (show-error src p.parsed)
10478+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10479+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
10480+ ?: (module-has-reserved-proj p.parsed)
10481+ 'module has reserved proj name'
785010482 =/ ds=(list def) defs.p.parsed
785110483 =/ molds=imolds (collect-simple-molds ds)
785210484 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
785310485 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
785410486 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
7855− =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
10487+ =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
10488+ =/ cycles=(list icycle) (definite-value-cycles ds globals)
10489+ =/ env=ienv env.resolution
785610490 =/ lines=(list @t) ~
785710491 |-
785810492 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -7861,8 +10495,18 @@
786110495 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
786210496 ?. (unique-value-name name.d globals)
786310497 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
10498+ =/ cycle=(list icycle) (skim cycles |=(c=icycle =(name.c name.d)))
10499+ ?^ cycle
10500+ =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
10501+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
10502+ ?: (lien grouped.resolution |=(n=term =(n name.d)))
10503+ =/ found=(unit ischeme) (ienv-lookup name.d env)
10504+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
10505+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
10506+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
10507+ $(ds t.ds, lines [line lines])
786410508 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7865− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
10509+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~]
786610510 =. initial (reserve-def-caps val.d initial)
786710511 =/ result=iresult
786810512 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -7870,6 +10514,10 @@
787010514 (infer-fragment val.d env initial)
787110515 ?: ?=(%| -.result)
787210516 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
10517+ =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10518+ =/ hole=(unit idiag) (unresolved-hole holes.state.p.result holes.initial state.p.result)
10519+ ?^ hole
10520+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d u.hole) lines])
787310521 =/ merged=(unit [first=icap second=icap])
787410522 (merged-capitals caps.state.p.result sub.state.p.result)
787510523 ?^ merged
@@ -7892,6 +10540,8 @@
789210540 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
789310541 ?: (gth (lent vars) 26)
789410542 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
10543+ ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
10544+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
789510545 =/ printable=itype (canonical-itype typ vars)
789610546 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
789710547 $(ds t.ds, lines [line lines])