@@ -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 ~]
@@ -5226,22 +5315,119 @@
52265315 problems
52275316::
52285317:: The expression inference below is deliberately a fragment: bindings,
5229−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5318+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
52305319:: result for unsupported syntax is a diagnostic, never a checked module.
52315320::
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])
5237−+$ icaps (list [name=@t id=@ud])
5329++$ icap [name=@t id=@ud at=span]
5330++$ icaps (list icap)
52385331+$ iparams (list [name=@t typ=itype])
52395332+$ imolds (list [name=term body=shape])
52405333:: A caller supplies the exact noun returned by +read-mold:jibb-import.
52415334:: This core has no Ford dependencies; unrecognized payloads fail closed.
52425335+$ iexternals (list [module=term name=term result=*])
52435336+$ imark-externals (list [mark=term result=*])
5244−+$ 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)]
52455431+$ idiag [msg=tape sites=(list [at=span note=tape])]
52465432+$ iresult (each [typ=itype state=istate] idiag)
52475433+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5277,6 +5463,8 @@
52775463:: generalize an aura from its sample, which requires constraint analysis
52785464:: beyond this fragment; leave those cases unresolved.
52795465::
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.
52805468++ itype-has-gate
52815469 |= t=itype
52825470 ^- ?
@@ -5284,6 +5472,7 @@
52845472 %fn &
52855473 %cell |($(t hed.t) $(t tal.t))
52865474 %recursive |
5475+ %jrec |
52875476 %collection (lien args.t |=(c=itype (itype-has-gate c)))
52885477 %face $(t body.t)
52895478 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5295,6 +5484,7 @@
52955484 %atom |
52965485 %any-atom |
52975486 %flag |
5487+ %noun |
52985488 ==
52995489::
53005490++ default-decimals
@@ -5309,6 +5499,90 @@
53095499 * t
53105500 ==
53115501::
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+::
53125586++ itype-vars
53135587 |= t=itype
53145588 ^- (list @ud)
@@ -5319,10 +5593,12 @@
53195593 %atom ~
53205594 %any-atom ~
53215595 %flag ~
5596+ %noun ~
53225597 %tag ~
53235598 %const ~
53245599 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
53255600 %recursive ~
5601+ %jrec ~
53265602 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
53275603 %face $(t body.t)
53285604 %fn (weld $(t sample.t) $(t product.t))
@@ -5357,10 +5633,12 @@
53575633 %atom t
53585634 %any-atom t
53595635 %flag t
5636+ %noun t
53605637 %tag t
53615638 %const t
53625639 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
53635640 %recursive t
5641+ %jrec t
53645642 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
53655643 %face [%face name.t $(t body.t)]
53665644 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5380,10 +5658,12 @@
53805658 %atom |
53815659 %any-atom |
53825660 %flag |
5661+ %noun |
53835662 %tag |
53845663 %const |
53855664 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
53865665 %recursive |
5666+ %jrec |
53875667 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
53885668 %face $(t body.t)
53895669 %fn |($(t sample.t) $(t product.t))
@@ -5486,6 +5766,11 @@
54865766 ?. ?=([%ref @ @] node) ~
54875767 ?. &(=(module +<.node) =(name +>.node)) ~
54885768 `[[%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]
54895774 %face
54905775 ?. ?=([%face @ *] node) ~
54915776 ?. (jibb-face-name +<.node) ~
@@ -5524,12 +5809,70 @@
55245809 $(pats t.pats)
55255810::
55265811::
5812+::
5813+:: Repeated faces along an imported record spine fail closed. Hoon's type
5814+:: graph can erase unfaced nested-cell boundaries, so that alone does not
5815+:: prove the original source repeated a name within one record. A faced
5816+:: body and each union alternative have separate scopes. Check recursive
5817+:: roots before making them opaque; unused molds are never inspected.
5818+::
5819+++ imported-faces-valid
5820+ |= node=*
5821+ ^- ?
5822+ ?@ node &
5823+ ?+ -.node &
5824+ %face ?:(?=([%face @ *] node) $(node +>.node) |)
5825+ %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
5826+ %fork (imported-faces-valid-list +.node)
5827+ %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)
5832+ ==
5833+::
5834+++ imported-faces-valid-list
5835+ |= nodes=*
5836+ ^- ?
5837+ ?@ nodes =(nodes 0)
5838+ ?. (imported-faces-valid -.nodes) |
5839+ $(nodes +.nodes)
5840+::
5841+++ imported-record-faces-valid
5842+ |= [node=* names=(list @)]
5843+ ^- ?
5844+ ?: ?=([%cell * *] node)
5845+ =/ head=* +<.node
5846+ =/ rest=* +>.node
5847+ ?: ?=([%face @ *] head)
5848+ ?: (lien names |=(n=@ =(n +<.head))) |
5849+ ?. (imported-faces-valid +>.head) |
5850+ $(node rest, names [+<.head names])
5851+ ?. (imported-faces-valid head) |
5852+ $(node rest)
5853+ ?: ?=([%face @ *] node)
5854+ ?: (lien names |=(n=@ =(n +<.node))) |
5855+ (imported-faces-valid +>.node)
5856+ (imported-faces-valid node)
5857+::
55275858++ import-to-itype
55285859 |= node=*
55295860 ^- (unit itype)
55305861 ?@ node ~
55315862 ?+ -.node ~
5863+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
55325864 %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 '~']]
55335876 ?: ?=([%atom %tas [~ @]] node)
55345877 =/ value=@ +>+.node
55355878 ?. |(=(value 0) (jibb-face-name value)) ~
@@ -5539,6 +5882,15 @@
55395882 =/ aura=@ta (@ta +<.node)
55405883 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
55415884 `[%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)}")]
55425894 %apply
55435895 ?. ?=([%apply @ *] node) ~
55445896 =/ name=term (@tas +<.node)
@@ -5552,10 +5904,15 @@
55525904 ?. =(arity (lent u.args)) ~
55535905 `[%collection name u.args]
55545906 %fork
5555− =/ 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)
55565912 ?~ cases ~
55575913 ?~ u.cases ~
55585914 ?~ t.u.cases ~
5915+ ?: (import-has-loobean-singleton u.cases) ~
55595916 ?. (import-cases-disjoint u.cases) ~
55605917 `[%union u.cases ~ ~ ~]
55615918 %face
@@ -5574,6 +5931,20 @@
55745931 `[%cell u.left u.right]
55755932 ==
55765933::
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+::
55775948++ import-to-itypes
55785949 |= nodes=*
55795950 ^- (unit (list itype))
@@ -5588,7 +5959,9 @@
55885959 |= typ=itype
55895960 ^- upat
55905961 ?- -.typ
5962+ %noun [%all ~]
55915963 %atom [%atom ~]
5964+ %flag [%or ~[[%atom `0] [%atom `1]]]
55925965 %const [%atom `val.literal.typ]
55935966 %face $(typ body.typ)
55945967 %cell [%cell $(typ hed.typ) $(typ tal.typ)]
@@ -5616,6 +5989,7 @@
56165989 ?@ result ~
56175990 ?. ?=(%& -.result) ~
56185991 =/ node=* +.result
5992+ ?. (imported-faces-valid node) ~
56195993 ?@ node (import-to-itype node)
56205994 ?: ?=(%ref -.node) (import-to-itype node)
56215995 =/ pattern=(unit irec-pattern) (rec-pattern node module name)
@@ -5651,6 +6025,7 @@
56516025 =/ result=* result.i.found
56526026 ?@ result ~
56536027 ?. ?=(%& -.result) ~
6028+ ?. (imported-faces-valid +.result) ~
56546029 (import-to-itype +.result)
56556030::
56566031++ find-jibb-interface
@@ -5681,25 +6056,55 @@
56816056 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
56826057 $(molds t.molds)
56836058::
5684−:: Only names exported by this directly imported module are visible through
5685−:: 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)
56866081::
56876082++ itype-in-import
5688− |= [t=itype iface=ifile face=term]
6083+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
56896084 ^- itype
56906085 ?- -.t
56916086 %union
56926087 =/ label=(unit @t)
56936088 ?~ origin.t ~
56946089 ?: =(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
56956094 =/ alias=(unit term) ~
56966095 =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
56976096 =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
56986097 ?~ alias ~
56996098 `(crip "{(trip u.alias)}.{(trip face)}")
5700− [%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)))]
57016100 %recursive [%recursive module.t name.t ~]
5702− %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)))]
57036108 %face [%face name.t $(t body.t)]
57046109 %fn [%fn $(t sample.t) $(t product.t)]
57056110 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5772,9 +6177,46 @@
57726177 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
57736178 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
57746179::
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+::
57756213++ infer-mold-template
57766214 |= [sh=shape state=istate]
57776215 ^- (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]
57786220 ?: ?=(%generic -.sh)
57796221 ?~ vars.sh ~
57806222 ?. (distinct-params vars.sh) ~
@@ -5782,26 +6224,127 @@
57826224 =/ out=(unit [typ=itype state=istate])
57836225 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
57846226 ?~ out ~
6227+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
57856228 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
57866229 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
57876230 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
57886231 =/ used=(list @ud) (itype-vars typ.u.out)
57896232 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5790− `[[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)]
57916234 =/ out=(unit [typ=itype state=istate])
57926235 (infer-simple-shape sh state(params ~, in-mold &))
57936236 ?~ out ~
6237+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
57946238 ?: ?=(^ (itype-vars typ.u.out)) ~
5795− `[[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)]
6240+::
6241+:: A direct imported reference may carry definite reader evidence. Only
6242+:: uniquely supplied, declared inputs are used; unsupported data stay generic.
6243+++ direct-import-invalid
6244+ |= [sh=shape state=istate]
6245+ ^- (unit idiag)
6246+ ?. ?=(%ref -.sh) ~
6247+ ?~ names.sh ~
6248+ =/ n=term i.names.sh
6249+ =/ raw=*
6250+ ?~ t.names.sh
6251+ ?. (unique-value-name n marks.state) ~
6252+ ?: (lien surs.state |=(x=term =(x n))) ~
6253+ ?: ?=(^ (find-jibb-interface n jimports.state)) ~
6254+ ?: (lien globals.state |=(x=term =(x n))) ~
6255+ ?: (lien reserved-molds.state |=(x=term =(x n))) ~
6256+ ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) ~
6257+ =/ found=imark-externals (skim mark-externals.state |=(e=[mark=term result=*] =(mark.e n)))
6258+ ?~ found ~
6259+ ?^ t.found ~
6260+ result.i.found
6261+ ?^ t.t.names.sh ~
6262+ =/ mod=term i.t.names.sh
6263+ ?: ?=(^ (find-jibb-interface mod jimports.state)) ~
6264+ ?. (unique-value-name mod surs.state) ~
6265+ ?: (lien marks.state |=(x=term =(x mod))) ~
6266+ ?: (lien globals.state |=(x=term =(x mod))) ~
6267+ ?: (lien reserved-molds.state |=(x=term =(x mod))) ~
6268+ ?: (lien molds.state |=(m=[name=term body=shape] =(mod name.m))) ~
6269+ =/ found=iexternals (skim externals.state |=(e=[module=term name=term result=*] &(=(module.e mod) =(name.e n))))
6270+ ?~ found ~
6271+ ?^ t.found ~
6272+ result.i.found
6273+ ?. ?=([%invalid ?(%aura %core) @] raw) ~
6274+ `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
6275+::
6276+:: Replay only the shape branches whose evaluation order we can prove.
6277+:: Successful prefixes must be checked before descending to a failure.
6278+++ nested-import-invalid
6279+ |= [sh=shape state=istate]
6280+ ^- (unit idiag)
6281+ ?: ?=(^ (infer-simple-shape sh state)) ~
6282+ ?- -.sh
6283+ %ref
6284+ =/ direct=(unit idiag) (direct-import-invalid sh state)
6285+ ?^ direct direct
6286+ ?~ names.sh ~
6287+ ?^ t.names.sh ~
6288+ =/ n=term i.names.sh
6289+ ?: (lien marks.state |=(x=term =(x n))) ~
6290+ ?: (lien active.state |=(x=term =(x n))) ~
6291+ =/ found=(unit shape) (find-simple-mold n molds.state)
6292+ ?~ found ~
6293+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
6294+ %fn
6295+ =/ first=(unit [typ=itype state=istate]) (infer-simple-shape sample.sh state)
6296+ ?~ first $(sh sample.sh)
6297+ $(sh product.sh, state state.u.first)
6298+ %cell (nested-field-invalid fields.sh state)
6299+ * ~
6300+ ==
6301+::
6302+++ nested-field-invalid
6303+ |= [fields=(list field) state=istate]
6304+ ^- (unit idiag)
6305+ ?~ fields ~
6306+ =/ sh=shape
6307+ ?- -.i.fields
6308+ %bare shape.i.fields
6309+ %face shape.i.fields
6310+ %pun [%ref at.i.fields ~[name.i.fields]]
6311+ ==
6312+ =/ out=(unit [typ=itype state=istate]) (infer-simple-shape sh state)
6313+ ?~ out (nested-import-invalid sh state)
6314+ $(fields t.fields, state state.u.out)
6315+::
6316+++ sample-import-invalid
6317+ |= [s=sample env=ienv state=istate]
6318+ ^- (unit idiag)
6319+ =/ result=isample-result (infer-sample s env state)
6320+ ?: ?=(%& -.result) ~
6321+ ?. =(p.result "sample mold is not supported by partial inference") ~
6322+ ?- s
6323+ [%face *] (nested-import-invalid shape.s state)
6324+ [%bare *] (nested-import-invalid shape.s state)
6325+ [%pun *] (nested-import-invalid [%ref at.s ~[name.s]] state)
6326+ [%cell *] (nested-samples-invalid items.s env state)
6327+ * ~
6328+ ==
6329+::
6330+++ nested-samples-invalid
6331+ |= [items=(list sample) env=ienv state=istate]
6332+ ^- (unit idiag)
6333+ ?~ items ~
6334+ =/ head=isample-result (infer-sample i.items env state)
6335+ ?: ?=(%| -.head) (sample-import-invalid i.items env state)
6336+ $(items t.items, env env.p.head, state state.p.head)
57966337::
57976338++ infer-simple-shape
57986339 |= [sh=shape state=istate]
57996340 ^- (unit [typ=itype state=istate])
58006341 ?- -.sh
6342+ %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
58016343 %aura
58026344 ?: =(0 aura.sh) `[[%any-atom ~] state]
58036345 `[[%atom aura.sh] state]
58046346 %flag `[[%flag ~] state]
6347+ %noun `[[%noun ~] state]
58056348 %const
58066349 ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
58076350 `[[%const lit.sh] state]
@@ -5828,7 +6371,7 @@
58286371 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
58296372 ?~ found ~
58306373 ?^ vars.u.found ~
5831− `[(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]
58326375 =/ found=(unit itype)
58336376 (find-imported-mold i.t.names.sh n externals.state surs.state)
58346377 ?~ found ~
@@ -5847,10 +6390,13 @@
58476390 ?~ prelude-entry ~
58486391 ?^ vars.u.prelude-entry ~
58496392 `[typ.u.prelude-entry state]
6393+ =/ direct=(unit itype) (simple-source-recursive n u.found state)
6394+ ?^ direct `[u.direct state]
58506395 =/ out=(unit [typ=itype state=istate])
58516396 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
58526397 ?~ out ~
5853− `[(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)]
58546400 %apply
58556401 ?~ ref.sh ~
58566402 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -5865,7 +6411,7 @@
58656411 ?~ vars.u.template ~
58666412 =/ applied=(unit itype) (template-apply u.template types.u.args)
58676413 ?~ applied ~
5868− `[(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]
58696415 ?: (lien active.state.u.args |=(x=term =(x n))) ~
58706416 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
58716417 ?~ found
@@ -5884,18 +6430,19 @@
58846430 =/ out=(unit [typ=itype state=istate])
58856431 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
58866432 ?~ out ~
6433+ ?^ (unresolved-hole holes.state.u.out holes.state.u.args state.u.out) ~
58876434 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
58886435 ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
58896436 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
58906437 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
5891− `[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)]
58926439 %tvar
58936440 =/ param=(unit itype) (iparam-lookup name.sh params.state)
58946441 ?^ param `[u.param state]
58956442 ?: in-mold.state ~
58966443 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
58976444 ?^ n `[[%var u.n] state]
5898− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state] caps.state])]
6445+ `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
58996446 * ~
59006447 ==
59016448::
@@ -5928,12 +6475,12 @@
59286475 ^- isample-result
59296476 ?- -.s
59306477 %bind
5931− ?: |(?=(^ (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))))
59326479 [%| "sample shadows a name"]
59336480 =/ t=itype [%var next.state]
59346481 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
59356482 %face
5936− ?: |(?=(^ (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))))
59376484 [%| "sample shadows a name"]
59386485 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
59396486 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -5971,8 +6518,8 @@
59716518 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
59726519::
59736520:: Local definitions generalize only variables outside their enclosing
5974−:: environment and explicit-capital scope. Unresolved groups stay
5975−:: unsupported: this fragment does not infer recursive definitions.
6521+:: environment and explicit-capital scope. Recursive gate groups use
6522+:: monomorphic placeholders while their bodies are checked.
59766523::
59776524+$ ilocal-result (each [env=ienv state=istate] idiag)
59786525++ free-env-vars
@@ -6001,6 +6548,7 @@
60016548 |-
60026549 ?~ ds &
60036550 ?: ?=(%mold -.i.ds) $(ds t.ds)
6551+ ?: =(name.i.ds %proj) |
60046552 ?. (unique-value-name name.i.ds names) |
60056553 ?: ?=(^ (ienv-lookup name.i.ds env)) |
60066554 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -6024,6 +6572,7 @@
60246572 |-
60256573 ?~ locals &
60266574 =/ n=term name.i.locals
6575+ ?: =(n %proj) |
60276576 ?. (unique-value-name n names) |
60286577 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
60296578 ?: (lien marks.state |=(m=term =(n m))) |
@@ -6041,6 +6590,145 @@
60416590 ?~ inferred |
60426591 $(locals t.locals)
60436592::
6593+:: Gather written capitals belonging to one ++. Nested local definitions
6594+:: establish their own scopes; inline gates remain in the enclosing scope.
6595++$ icap-site [name=@t at=span]
6596+++ scope-shape
6597+ |= s=shape
6598+ ^- (list icap-site)
6599+ ?- -.s
6600+ %tvar ~[[name.s at.s]]
6601+ %apply (zing (turn args.s scope-shape))
6602+ %cell (zing (turn fields.s scope-field))
6603+ %union (zing (turn cases.s scope-shape))
6604+ %fn (weld (scope-shape sample.s) (scope-shape product.s))
6605+ %generic
6606+ =/ inside=(list icap-site) (scope-shape body.s)
6607+ (skim inside |=(site=icap-site !(lien vars.s |=(v=@t =(v name.site)))))
6608+ * ~
6609+ ==
6610+::
6611+++ scope-field
6612+ |= f=field
6613+ ^- (list icap-site)
6614+ ?- -.f
6615+ %face (scope-shape shape.f)
6616+ %bare (scope-shape shape.f)
6617+ %pun ~
6618+ ==
6619+::
6620+++ scope-sample
6621+ |= s=sample
6622+ ^- (list icap-site)
6623+ ?- -.s
6624+ %face (scope-shape shape.s)
6625+ %bare (scope-shape shape.s)
6626+ %cell (zing (turn items.s scope-sample))
6627+ * ~
6628+ ==
6629+::
6630+++ scope-pieces
6631+ |= ps=(list piece)
6632+ ^- (list icap-site)
6633+ ?~ ps ~
6634+ =/ first=(list icap-site)
6635+ ?- -.i.ps
6636+ %expr (scope-expr p.i.ps)
6637+ %text ~
6638+ ==
6639+ (weld first $(ps t.ps))
6640+::
6641+++ scope-qsegs
6642+ |= ps=(list qseg)
6643+ ^- (list icap-site)
6644+ ?~ ps ~
6645+ =/ first=(list icap-site)
6646+ ?- -.i.ps
6647+ %expr (scope-expr p.i.ps)
6648+ %knot ~
6649+ ==
6650+ (weld first $(ps t.ps))
6651+::
6652+++ scope-edits
6653+ |= xs=(list edit)
6654+ ^- (list icap-site)
6655+ ?~ xs ~
6656+ =/ first=(list icap-site) (scope-expr val.i.xs)
6657+ (weld first $(xs t.xs))
6658+::
6659+++ scope-items
6660+ |= xs=(list item)
6661+ ^- (list icap-site)
6662+ ?~ xs ~
6663+ =/ first=(list icap-site) (scope-expr val.i.xs)
6664+ (weld first $(xs t.xs))
6665+::
6666+++ scope-arms
6667+ |= xs=(list arm)
6668+ ^- (list icap-site)
6669+ ?~ xs ~
6670+ =/ first=(list icap-site) (scope-expr val.i.xs)
6671+ (weld first $(xs t.xs))
6672+::
6673+++ scope-exprs
6674+ |= xs=(list expr)
6675+ ^- (list icap-site)
6676+ ?~ xs ~
6677+ =/ first=(list icap-site) (scope-expr i.xs)
6678+ (weld first $(xs t.xs))
6679+::
6680+++ scope-expr
6681+ |= e=expr
6682+ ^- (list icap-site)
6683+ ?- -.e
6684+ %str (scope-pieces pieces.e)
6685+ %qath (scope-qsegs segs.e)
6686+ %change (scope-edits edits.e)
6687+ %pair (scope-expr val.e)
6688+ %unit (scope-expr val.e)
6689+ %group (scope-expr inner.e)
6690+ %list (scope-exprs items.e)
6691+ %tuple (scope-items items.e)
6692+ %gate
6693+ =/ first=(list icap-site) (scope-sample sample.e)
6694+ =/ last=(list icap-site) (scope-expr body.e)
6695+ (weld first last)
6696+ %gate-wide
6697+ =/ first=(list icap-site) (scope-sample sample.e)
6698+ =/ last=(list icap-site) (scope-expr body.e)
6699+ (weld first last)
6700+ %call
6701+ =/ first=(list icap-site) (scope-expr head.e)
6702+ =/ last=(list icap-site) (scope-exprs args.e)
6703+ (weld first last)
6704+ %cast
6705+ =/ first=(list icap-site) (scope-shape shape.e)
6706+ =/ last=(list icap-site) (scope-expr val.e)
6707+ (weld first last)
6708+ %trace
6709+ =/ first=(list icap-site) (scope-expr val.e)
6710+ =/ last=(list icap-site) (scope-expr then.e)
6711+ (weld first last)
6712+ %branch
6713+ =/ first=(list icap-site) (scope-expr subject.e)
6714+ =/ last=(list icap-site) (scope-arms arms.e)
6715+ (weld first last)
6716+ %body (scope-expr final.e)
6717+ * ~
6718+ ==
6719+::
6720+++ reserve-cap-sites
6721+ |= [sites=(list icap-site) state=istate]
6722+ ^- istate
6723+ ?~ sites state
6724+ ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
6725+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
6726+::
6727+++ reserve-def-caps
6728+ |= [e=expr state=istate]
6729+ ^- istate
6730+ (reserve-cap-sites (scope-expr e) state)
6731+::
60446732++ infer-local-defs
60456733 |= [ds=(list def) env=ienv state=istate]
60466734 ^- ilocal-result
@@ -6049,26 +6737,65 @@
60496737 |-
60506738 ?~ ds
60516739 ?~ remaining [%& env state]
6052− ?. 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 |)
60536747 $(ds (flop remaining), remaining ~, progressed |)
60546748 =/ d=def i.ds
60556749 ?> ?=(%value -.d)
6056− =/ inferred=iresult (infer-fragment val.d env state)
6750+ =/ local-state=istate (reserve-def-caps val.d state)
6751+ =/ inferred=iresult (infer-fragment val.d env local-state)
6752+ =/ retried=? ?=(%| -.inferred)
6753+ =? inferred retried (infer-recursive-gate d env local-state)
60576754 ?: ?=(%| -.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]
6758+ =/ merged=(unit [first=icap second=icap])
6759+ (merged-capitals caps.state.p.inferred sub.state.p.inferred)
6760+ ?^ merged
6761+ [%| ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
6762+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred)
6763+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
60586764 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
60596765 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
60606766 $(ds t.ds, remaining [d remaining])
60616767 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
60626768 $(ds t.ds, remaining [d remaining])
60636769 =/ free=(list @ud)
6064− (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state.p.inferred sub.state.p.inferred))
6770+ (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
60656771 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
60666772 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6067− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred, 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]
60686795::
60696796:: Read only fields of a known record. Unresolved field constraints and
6070−:: ambiguous repeated faces are outside this fragment (doc question:
6071−:: whether duplicate imported Hoon faces are valid or select a field).
6797+:: ambiguous repeated faces are outside this fragment. Imported record
6798+:: spines with repeated names are unavailable when used.
60726799::
60736800++ record-fields-named
60746801 |= [name=term t=itype sub=isub]
@@ -6087,21 +6814,33 @@
60876814 ^- iresult
60886815 =/ reverse=(list term) (flop names)
60896816 ?~ reverse [%| ["empty wing" ~]]
6090− =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6091− ?~ scheme [%| ["field access is not supported by partial inference" ~]]
6092− =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
6817+ =/ iface=(unit ifile) (find-jibb-interface i.reverse jimports.state)
60936818 =/ 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)
60946833 =/ typ=itype typ.inst
60956834 |-
6096− ?~ fields [%& typ state.inst]
6097− =/ 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)
60986837 ?~ found [%| ["field is not available to partial inference" ~]]
60996838 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6100− $(fields t.fields, typ i.found)
6839+ $(remaining t.remaining, typ i.found)
61016840::
6102−:: Propagate a known union through supported loobean and unit branches. Empty bodies
6103−:: and groups are transparent; bodies with definitions keep their normal
6104−:: scoping and wait for general bidirectional inference.
6841+:: Propagate a known union or list through supported loobean, unit and list
6842+:: branches. Empty bodies and groups are transparent; bodies with definitions
6843+:: keep their normal scoping and wait for general bidirectional inference.
61056844::
61066845++ context-union-branch
61076846 |= e=expr
@@ -6118,6 +6857,8 @@
61186857 ^- iresult
61196858 ?: ?=(%group -.e) $(e inner.e)
61206859 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6860+ ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
6861+ (infer-list-context e expected env state context)
61216862 ?: ?=(%branch -.e)
61226863 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
61236864 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
@@ -6134,6 +6875,9 @@
61346875 [%| ["branch does not cover both loobeans" ~]]
61356876 =/ subject=iresult (infer-fragment subject.e env state)
61366877 ?: ?=(%| -.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" ~]]
61376881 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
61386882 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
61396883 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6145,20 +6889,33 @@
61456889 ?: ?=(%| -.value) value
61466890 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
61476891 ?: ?=(%unknown -.fit)
6892+ ?: &(?=(%collection -.expected) =(%list name.expected))
6893+ [%| ["branch list constraint is not supported by partial inference" ~]]
6894+ ?: ?=(%flag -.expected) [%| ["branch loobean constraint is not supported by partial inference" ~]]
61486895 [%| ["branch union constraint is not supported by partial inference" ~]]
61496896 ?: ?=(%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]
6901+ ?: &(?=(%collection -.expected) =(%list name.expected))
6902+ [%| ["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"]]]]
61506905 [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
61516906 [%& expected state.p.value(sub sub.fit, next next.fit)]
61526907::
6153−:: A list literal needs a known list target and the validated prelude list.
6154−:: Its items receive that target one by one; pending constraints elsewhere
6155−:: stay in the threaded state. Other list syntax remains unsupported.
6908+:: A list expression needs a known list target and the validated prelude list.
6909+:: Literal items and unfaced two-item cons cells receive that target one by
6910+:: one; pending constraints elsewhere stay in the threaded state.
61566911::
6157−++ context-list-literal
6912+++ context-list-expression
61586913 |= e=expr
61596914 ^- ?
61606915 ?- -.e
61616916 %list &
6917+ %tuple &
6918+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
61626919 %group $(e inner.e)
61636920 %body ?~(defs.e $(e final.e) |)
61646921 * |
@@ -6169,7 +6926,6 @@
61696926 ^- iresult
61706927 ?: ?=(%group -.e) $(e inner.e)
61716928 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6172− ?> ?=(%list -.e)
61736929 ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
61746930 ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
61756931 [%| ["list literal needs the standard prelude in partial inference" ~]]
@@ -6182,25 +6938,65 @@
61826938 ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
61836939 ?~ args.target [%| ["list context is not supported by partial inference" ~]]
61846940 ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
6185− =/ result=iresult (infer-list-items items.e i.args.target env state context)
6186− ?: ?=(%| -.result) result
6187− [%& target state.p.result]
6941+ ?: ?=(%lit -.e)
6942+ ?. |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6943+ [%| ["list expression is not supported by partial inference" ~]]
6944+ [%& target state]
6945+ ?: ?=(%list -.e)
6946+ =/ result=iresult (infer-list-items items.e i.args.target env state context)
6947+ ?: ?=(%| -.result) result
6948+ [%& target state.p.result]
6949+ ?. ?=(%tuple -.e) [%| ["list expression is not supported by partial inference" ~]]
6950+ ?~ items.e [%| ["cons shape is not supported by partial inference" ~]]
6951+ ?~ t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6952+ ?^ t.t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6953+ ?^ face.i.items.e [%| ["faced cons is not supported by partial inference" ~]]
6954+ ?^ face.i.t.items.e [%| ["faced cons is not supported by partial inference" ~]]
6955+ =/ head=iresult (infer-list-items ~[val.i.items.e] i.args.target env state context)
6956+ ?: ?=(%| -.head) head
6957+ =/ target=itype (itype-walk target sub.state.p.head)
6958+ =/ tail=iresult
6959+ ?: (context-list-expression val.i.t.items.e)
6960+ (infer-list-context val.i.t.items.e target env state.p.head context)
6961+ (infer-fragment val.i.t.items.e env state.p.head)
6962+ ?: ?=(%| -.tail) tail
6963+ =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
6964+ ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
6965+ ?: ?=(%bad -.fit)
6966+ [%| ["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)]]]]
6967+ [%& target state.p.tail(sub sub.fit, next next.fit)]
6968+::
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))
61886985::
61896986++ infer-list-items
61906987 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
61916988 ^- iresult
61926989 ?~ items [%& expected state]
61936990 =/ target=itype (itype-walk expected sub.state)
6194− =/ value=iresult
6195− ?: &(?=(%union -.target) (context-union-branch i.items))
6196− (infer-union-context i.items target env state context)
6197− ?: &(?=(%collection -.target) =(%list name.target) (context-list-literal i.items))
6198− (infer-list-context i.items target env state context)
6199− (infer-fragment i.items env state)
6991+ =/ value=iresult (infer-call-context-arg i.items target env state context)
62006992 ?: ?=(%| -.value) value
62016993 =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
62026994 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
62036995 ?: ?=(%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]
62047000 [%| ["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)]]]]
62057001 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
62067002::
@@ -6293,7 +7089,7 @@
62937089 [%| ["list branch pattern is not supported by partial inference" ~]]
62947090 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
62957091 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6296− ?: |(=(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)))))
62977093 [%| ["pattern binder shadows a name" ~]]
62987094 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
62997095 =/ left=iresult
@@ -6330,7 +7126,7 @@
63307126 [%| ["unit branch pattern is not supported by partial inference" ~]]
63317127 =/ binder=(unit term) ?:(first-empty second-name first-name)
63327128 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
6333− ?: |(?=(^ (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))))
63347130 [%| ["pattern binder shadows a name" ~]]
63357131 =/ payload=(unit itype) (unit-union-payload typ)
63367132 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -6348,10 +7144,577 @@
63487144 ?~ joined [%| ["unit branch results need unsupported inference" ~]]
63497145 [%& typ.p.left state.p.right(sub u.joined)]
63507146::
7147+:: Infer pieces in order, retaining their substitutions and pending tags.
7148+:: A bare decimal literal has no outside type constraint, so it takes its
7149+:: normal @ud default here. Other open numeric and aura variables wait for
7150+:: deferred constraints, which this fragment does not implement yet.
7151+++ infer-string-pieces
7152+ |= [ps=(list piece) env=ienv state=istate]
7153+ ^- iresult
7154+ ?~ ps [%& [%atom %t] state]
7155+ ?: ?=(%text -.i.ps) $(ps t.ps)
7156+ =/ item=iresult (infer-fragment p.i.ps env state)
7157+ ?: ?=(%| -.item) item
7158+ =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
7159+ ?: |(?=(%atom -.t) ?=(%any-atom -.t))
7160+ $(ps t.ps, state state.p.item)
7161+ ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
7162+ $(ps t.ps, state state.p.item)
7163+ ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
7164+ $(ps t.ps, state state.p.item)
7165+ ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
7166+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
7167+ ?: ?=(%cell -.t)
7168+ [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
7169+ [%| ["interpolation type needs unsupported inference" ~]]
7170+::
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+::
63517713++ infer-fragment
63527714 |= [e=expr env=ienv state=istate]
63537715 ^- iresult
63547716 ?- -.e
7717+ %pair $(e (pair-as-cell e))
63557718 %lit
63567719 ?- form.lit.e
63577720 %number ?: =(%ud aura.lit.e)
@@ -6365,10 +7728,45 @@
63657728 %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
63667729 %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
63677730 ==
6368− %str
6369− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
6370− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
6371− [%& [%atom %t] state]
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]
7754+ %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)]
63727770 %wing
63737771 ?~ names.e [%| ["empty wing" ~]]
63747772 ?^ t.names.e
@@ -6377,7 +7775,7 @@
63777775 ?~ iface (infer-field-wing names.e env state)
63787776 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
63797777 ?~ member [%| ["module member is not available to partial inference" ~]]
6380− =. 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)
63817779 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
63827780 [%& typ.instance state.instance]
63837781 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
@@ -6390,6 +7788,11 @@
63907788 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
63917789 [%& typ.instance state.instance]
63927790 %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 ~)
63937796 %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
63947797 %trace
63957798 =/ traced=iresult $(e val.e)
@@ -6406,6 +7809,9 @@
64067809 [%| ["local molds shadow a name" ~]]
64077810 =/ local-state=istate
64087811 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"]]]]
64097815 ?. (local-molds-supported local-molds local-state)
64107816 [%| ["local molds need unsupported inference" ~]]
64117817 =/ values=(list def) (local-value-defs defs.e)
@@ -6416,20 +7822,30 @@
64167822 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
64177823 %branch
64187824 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
6419− ?~ t.arms.e (infer-cell-branch e env state)
6420− ?^ 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)
64217833 =/ x=arm i.arms.e
64227834 =/ y=arm i.t.arms.e
64237835 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
64247836 (infer-unit-branch e env state ~)
6425− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
6426− ?. ?=(%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)
64277839 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6428− [%| ["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)
64297842 ?: =(val.lit.pat.x val.lit.pat.y)
64307843 [%| ["branch does not cover both loobeans" ~]]
64317844 =/ subject=iresult $(e subject.e)
64327845 ?: ?=(%| -.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" ~]]
64337849 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
64347850 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
64357851 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6456,69 +7872,396 @@
64567872 [%& typ.p.left state.p.right(sub u.joined)]
64577873 %cast
64587874 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
6459− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
7875+ ?~ target
7876+ =/ diag=(unit idiag) (nested-import-invalid shape.e state)
7877+ ?^ diag [%| u.diag]
7878+ [%| ["cast mold is not supported by partial inference" ~]]
64607879 =/ value=iresult
6461− ?: &(?=(%union -.typ.u.target) (context-union-branch val.e))
6462− (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6463− ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-list-literal val.e))
6464− (infer-list-context val.e typ.u.target env state.u.target at.shape.e)
6465− $(e val.e, state state.u.target)
7880+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
64667881 ?: ?=(%| -.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" ~]]
64677885 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
64687886 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
64697887 ?: ?=(%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]
64707892 [%| ["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)]]]]
64717893 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
64727894 [%& merged state.p.value(sub sub.fit, next next.fit)]
64737895 %crash [%& [%var next.state] state(next +(next.state))]
64747896 %gate
64757897 =/ sam=isample-result (infer-sample sample.e env state)
6476− ?: ?=(%| -.sam) [%| [p.sam ~]]
7898+ ?: ?=(%| -.sam)
7899+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7900+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7901+ [%| [p.sam ~]]
64777902 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
64787903 ?: ?=(%| -.body) body
64797904 [%& [%fn typ.p.sam typ.p.body] state.p.body]
64807905 %gate-wide
64817906 =/ sam=isample-result (infer-sample sample.e env state)
6482− ?: ?=(%| -.sam) [%| [p.sam ~]]
7907+ ?: ?=(%| -.sam)
7908+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7909+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7910+ [%| [p.sam ~]]
64837911 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
64847912 ?: ?=(%| -.body) body
64857913 [%& [%fn typ.p.sam typ.p.body] state.p.body]
64867914 %call
64877915 ?~ args.e [%| ["call has no argument" ~]]
6488− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
6489− =/ head=iresult $(e head.e)
6490− ?: ?=(%| -.head) head
6491− =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
6492− =/ arg=iresult
6493− ?: &(?=(%fn -.head-type) ?=(%union -.sample.head-type) (context-union-branch i.args.e))
6494− (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6495− ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-list-literal i.args.e))
6496− (infer-list-context i.args.e sample.head-type env state.p.head (span-of head.e))
6497− $(e i.args.e, state state.p.head)
6498− ?: ?=(%| -.arg) arg
6499− =/ st=istate state.p.arg
6500− =/ ht=itype (itype-walk typ.p.head sub.st)
6501− ?: ?=(%fn -.ht)
6502− =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
6503− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
6504− ?: ?=(%bad -.fit)
6505− [%| ["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)]]]]
6506− ?: &((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))
6507− [%| ["call result face propagation is not supported by partial inference" ~]]
6508− [%& product.ht st(sub sub.fit, next next.fit)]
6509− =/ result=itype [%var next.st]
6510− =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
6511− ?~ uni
6512− [%| ["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)]]]]
6513− [%& 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))
65147919 * [%| ["expression is not supported by partial inference" ~]]
65157920 ==
65167921::
6517−:: Tuple and record expressions preserve their explicitly written faces.
7922+:: Locate a definite failing argument after the complete sample fit has
7923+:: failed. If an intermediate fit is uncertain, retain the whole argument
7924+:: span rather than assigning blame to a particular argument.
65187925::
6519−++ infer-simple-items
6520− |= [items=(list item) env=ienv state=istate]
6521− ^- iresult
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+::
7992+++ call-error-site
7993+ |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
7994+ ^- (unit [at=span typ=itype])
7995+ ?~ args ~
7996+ =/ original=[left=itype right=itype] [actual expected]
7997+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7998+ =. actual (itype-walk actual sub)
7999+ =. expected (itype-walk expected sub)
8000+ ?: &(?=(%face -.expected) !?=(%face -.actual))
8001+ $(expected body.expected)
8002+ ?~ t.args
8003+ =/ fit=ifit (itype-fit actual expected sub next)
8004+ ?. ?=(%bad -.fit) ~
8005+ `[(span-of i.args) (itype-normalize actual sub)]
8006+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8007+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
8008+ ?: ?=(%bad -.first) `[(span-of i.args) (itype-normalize hed.actual sub)]
8009+ ?: ?=(%unknown -.first) ~
8010+ $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
8011+::
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])]
8147+::
8148+++ infer-call-context-arg
8149+ |= [e=expr expected=itype env=ienv state=istate context=span]
8150+ ^- 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)
8158+ =/ target=itype (itype-walk expected sub.state)
8159+ |-
8160+ ?: ?=(%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)
8203+ ?: &(?=(%union -.target) (context-union-branch e))
8204+ (infer-union-context e target env state context)
8205+ ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
8206+ (infer-union-context e target env state context)
8207+ ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
8208+ (infer-list-context e target env state context)
8209+ ?: &(?=(%cell -.target) ?=(%tuple -.e))
8210+ (infer-call-context-items items.e target env state context)
8211+ (infer-fragment e env state)
8212+::
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+::
8244+++ infer-call-context-args
8245+ |= [args=(list expr) expected=itype env=ienv state=istate context=span]
8246+ ^- iresult
8247+ ?~ args [%| ["call has no argument" ~]]
8248+ ?~ t.args (infer-call-context-arg i.args (projection-field-target expected) env state context)
8249+ =/ target=itype (itype-walk expected sub.state)
8250+ |-
8251+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8252+ ?. ?=(%cell -.target)
8253+ (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
8254+ =/ head=iresult (infer-call-context-arg i.args (projection-field-target hed.target) env state context)
8255+ ?: ?=(%| -.head) head
8256+ =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
8257+ ?: ?=(%| -.tail) tail
8258+ [%& [%cell typ.p.head typ.p.tail] state.p.tail]
8259+::
8260+:: Tuple and record expressions preserve their explicitly written faces.
8261+::
8262+++ infer-simple-items
8263+ |= [items=(list item) env=ienv state=istate]
8264+ ^- iresult
65228265 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
65238266 =/ head=iresult (infer-fragment val.i.items env state)
65248267 ?: ?=(%| -.head) head
@@ -6529,11 +8272,55 @@
65298272 ?: ?=(%| -.tail) tail
65308273 [%& [%cell ht typ.p.tail] state.p.tail]
65318274::
6532−:: A single two-binder cell pattern covers every value of a cell type.
6533−:: 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)
65348321::
65358322++ infer-cell-branch
6536− |= [e=expr env=ienv state=istate]
8323+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
65378324 ^- iresult
65388325 ?> ?=(%branch -.e)
65398326 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -6542,25 +8329,31 @@
65428329 =/ pats=(list pattern) items.pat.arm
65438330 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
65448331 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6545− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6546− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6547− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6548− =/ one=term name.i.pats
6549− =/ two=term name.i.t.pats
6550− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
6551− [%| ["pattern shadows a name" ~]]
8332+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
8333+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
65528334 =/ subject=iresult (infer-fragment subject.e env state)
65538335 ?: ?=(%| -.subject) subject
65548336 =/ st=istate state.p.subject
6555− ?: (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)
65568339 [%| ["recursive pattern is not supported by partial inference" ~]]
65578340 ?: (itype-has-face typ.p.subject sub.st)
65588341 [%| ["record patterns are not supported by partial inference" ~]]
6559− =/ head=itype [%var next.st]
6560− =/ tail=itype [%var +(next.st)]
6561− =/ 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)
65628346 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
6563− (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)]
65648357::
65658358++ show-itype
65668359 |= [t=itype sub=isub]
@@ -6579,6 +8372,7 @@
65798372 %atom "@{(trip aura.t)}"
65808373 %any-atom "@"
65818374 %flag "?"
8375+ %noun "*"
65828376 %tag (trip txt.literal.t)
65838377 %const (trip txt.literal.t)
65848378 %union
@@ -6586,6 +8380,7 @@
65868380 ?~ args.t (trip u.label.t)
65878381 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
65888382 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8383+ %jrec ?~(label.t "recursive mold" (trip u.label.t))
65898384 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
65908385 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
65918386 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -6626,10 +8421,12 @@
66268421 %atom |
66278422 %any-atom |
66288423 %flag |
8424+ %noun |
66298425 %tag |
66308426 %const |
66318427 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
66328428 %recursive |
8429+ %jrec |
66338430 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
66348431 %face $(typ body.typ)
66358432 %fn |($(typ sample.typ) $(typ product.typ))
@@ -6650,8 +8447,8 @@
66508447:: A capital in a written mold is generalized with its enclosing ++.
66518448:: Atom constraints may remain generic; until full rigidity checking
66528449:: is implemented, do not report a type if one became more specific.
6653−:: Whether distinct written capitals may become equal is a doc question;
6654−:: the partial checker leaves such inference unsupported for now.
8450+:: Distinct written capitals cannot be forced equal; use the same
8451+:: capital where a type must be shared (Decisions 2026-10-30).
66558452::
66568453++ cap-id-in
66578454 |= [n=@ud caps=icaps sub=isub]
@@ -6667,6 +8464,35 @@
66678464 ?: =(n u.ident) &
66688465 $(caps t.caps)
66698466::
8467+++ cap-with-id
8468+ |= [n=@ud caps=icaps sub=isub]
8469+ ^- (unit icap)
8470+ ?~ caps ~
8471+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8472+ =/ ident=(unit @ud)
8473+ ?+ -.resolved ~
8474+ %var `id.resolved
8475+ %avar `id.resolved
8476+ ==
8477+ ?~ ident $(caps t.caps)
8478+ ?: =(n u.ident) `i.caps
8479+ $(caps t.caps)
8480+::
8481+++ merged-capitals
8482+ |= [caps=icaps sub=isub]
8483+ ^- (unit [first=icap second=icap])
8484+ ?~ caps ~
8485+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8486+ =/ ident=(unit @ud)
8487+ ?+ -.resolved ~
8488+ %var `id.resolved
8489+ %avar `id.resolved
8490+ ==
8491+ ?~ ident $(caps t.caps)
8492+ =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
8493+ ?^ found `[u.found i.caps]
8494+ $(caps t.caps)
8495+::
66708496++ constrained-capitals
66718497 |= [caps=icaps sub=isub]
66728498 ^- ?
@@ -6705,10 +8531,12 @@
67058531 %atom |
67068532 %any-atom |
67078533 %flag |
8534+ %noun |
67088535 %tag |
67098536 %const |
67108537 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
67118538 %recursive |
8539+ %jrec |
67128540 %collection (lien args.t |=(c=itype (has-atom-var n c)))
67138541 %face $(t body.t)
67148542 %fn |($(t sample.t) $(t product.t))
@@ -6756,9 +8584,9 @@
67568584::
67578585:: Build the supported part of the value environment in dependency order.
67588586:: Each pass adds successful definitions. Forward references become
6759−:: available on a later pass; recursive groups and unsupported syntax do
6760−:: not enter the environment. Generalized definitions are closed, so a
6761−:: 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.
67628590::
67638591++ global-value-names
67648592 |= ds=(list def)
@@ -6776,33 +8604,617 @@
67768604 ?~ t.hits &
67778605 |
67788606::
6779−++ add-supported-defs
6780− |= [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)]
8607+:: A top-level gate may refer to itself through one monomorphic placeholder.
8608+:: Its declared sample is inferred first and preserves its field faces.
8609+:: Unify the completed body with that placeholder before generalization;
8610+:: reporting repeats the same check instead of instantiating the gate's
8611+:: generalized interface inside its own body. Mutual groups stay unsupported.
8612+::
8613+++ direct-self-call
8614+ |= [e=expr name=term]
8615+ ^- ?
8616+ ?: ?=(%group -.e) $(e inner.e)
8617+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8618+ ?. ?=(%call -.e) |
8619+ ?. ?=(%wing -.head.e) |
8620+ =(names.head.e ~[name])
8621+::
8622+++ branch-base-arm
8623+ |= [e=expr name=term]
8624+ ^- (unit expr)
8625+ ?: ?=(%group -.e) $(e inner.e)
8626+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8627+ ?. ?=(%branch -.e) ~
8628+ ?~ arms.e ~
8629+ ?~ t.arms.e ~
8630+ ?^ t.t.arms.e ~
8631+ =/ x=arm i.arms.e
8632+ =/ y=arm i.t.arms.e
8633+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) ~
8634+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) ~
8635+ ?: =(val.lit.pat.x val.lit.pat.y) ~
8636+ =/ first=? (direct-self-call val.x name)
8637+ =/ second=? (direct-self-call val.y name)
8638+ ?: =(first second) ~
8639+ `?:(first val.y val.x)
8640+::
8641+:: Infer the base arm independently, with the self binding removed. Only
8642+:: a closed type whose constraints resolved can seed the recursive result.
8643+:: The regular body inference then checks both arms with shared state.
8644+::
8645+++ recursive-branch-seed
8646+ |= [d=def env=ienv state=istate]
8647+ ^- (unit itype)
8648+ ?. ?=(%value -.d) ~
8649+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) ~
8650+ =/ gate=expr val.d
8651+ =/ body=expr
8652+ ?- -.gate
8653+ %gate body.gate
8654+ %gate-wide body.gate
8655+ * !!
8656+ ==
8657+ =/ base=(unit expr) (branch-base-arm body name.d)
8658+ ?~ base ~
8659+ =/ outer=ienv (skim env |=(entry=[name=term scheme=ischeme] !=(name.entry name.d)))
8660+ =/ sam=isample-result
8661+ ?- -.gate
8662+ %gate (infer-sample sample.gate outer state)
8663+ %gate-wide (infer-sample sample.gate outer state)
8664+ * !!
8665+ ==
8666+ ?: ?=(%| -.sam) ~
8667+ =/ inferred=iresult (infer-fragment u.base env.p.sam state.p.sam)
8668+ ?: ?=(%| -.inferred) ~
8669+ ?: (pending-tags tags.state.p.inferred sub.state.p.inferred) ~
8670+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred) ~
8671+ =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
8672+ ?: ?=(^ (itype-vars typ)) ~
8673+ ?: (itype-has-tag typ) ~
8674+ `typ
8675+::
8676+++ infer-recursive-gate
8677+ |= [d=def env=ienv state=istate]
8678+ ^- iresult
8679+ ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
8680+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
8681+ [%| ["recursive definition is not a gate" ~]]
8682+ =/ result=(unit itype) (recursive-branch-seed d env state)
8683+ =/ gate=expr val.d
8684+ =/ sam=isample-result
8685+ ?- -.gate
8686+ %gate (infer-sample sample.gate env state)
8687+ %gate-wide (infer-sample sample.gate env state)
8688+ * !!
8689+ ==
8690+ ?: ?=(%| -.sam)
8691+ =/ diag=(unit idiag)
8692+ ?- -.gate
8693+ %gate (sample-import-invalid sample.gate env state)
8694+ %gate-wide (sample-import-invalid sample.gate env state)
8695+ * ~
8696+ ==
8697+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
8698+ [%| [p.sam ~]]
8699+ =/ id=@ud next.state.p.sam
8700+ =/ product=itype ?~(result [%var id] u.result)
8701+ =/ st=istate state.p.sam(next +(id))
8702+ =/ seed=itype [%fn typ.p.sam product]
8703+ =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
8704+ =/ body=expr
8705+ ?- -.gate
8706+ %gate body.gate
8707+ %gate-wide body.gate
8708+ * !!
8709+ ==
8710+ =/ out=iresult (infer-fragment body seeded st)
8711+ ?: ?=(%| -.out) out
8712+ =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
8713+ ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
8714+ [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
8715+::
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]
67818856 ^- ienv
6782− ?~ 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]
67838943 =/ d=def i.ds
67848944 ?: ?=(%mold -.d) $(ds t.ds)
67858945 ?. (unique-value-name name.d globals) $(ds t.ds)
67868946 ?^ (ienv-lookup name.d env) $(ds t.ds)
67878947 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6788− =/ result=iresult (infer-fragment val.d env [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 ~]
8949+ =. initial (reserve-def-caps val.d initial)
8950+ =/ result=iresult (infer-fragment val.d env initial)
8951+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
67898952 ?: ?=(%| -.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)
67908955 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
67918956 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
67928957 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
67938958 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
67948959 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
67958960 ?: (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]
67968966 $(ds t.ds, env [[name.d [typ vars]] env])
67978967::
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+::
67989097++ resolve-supported-defs
67999098 |= [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)]
68009099 ^- ienv
6801− =/ 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) ~
68029209 |-
6803− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
6804− ?: =(next env) env
6805− $(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))
68069218::
68079219+| %union-analysis
68089220::
@@ -6939,11 +9351,142 @@
69399351 [at.first at.second (union-relate a (project-union-mold second molds ~))]
69409352 (weld pairs $(cases t.cases))
69419353::
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)
69429481++ show-partial-mold
69439482 |= [file=path src=@t d=def molds=imolds]
69449483 ^- @t
69459484 ?> ?=(%mold -.d)
69469485 =/ 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])
69479490 =? sh ?=(%generic -.sh) body.sh
69489491 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
69499492 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -6970,6 +9513,21 @@
69709513 (show-error src [file line.beg.at.site col.beg.at.site note.site])
69719514 (of-wain:format [summary excerpts])
69729515::
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+::
69739531:: +golden-types: a partial report; it does not claim the module checks
69749532::
69759533++ golden-types
@@ -6999,6 +9557,180 @@
69999557+$ jfile-result (each [iface=ifile cache=jcache] @t)
70009558+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
70019559::
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+ ==
70029734++ import-binding-names
70039735 |= imports=(list import)
70049736 ^- (list term)
@@ -7011,6 +9743,60 @@
70119743 ==
70129744 [n $(imports t.imports)]
70139745::
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+::
70149800++ module-scope-valid
70159801 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
70169802 ^- ?
@@ -7018,6 +9804,7 @@
70189804 =/ vals=(list term) (global-value-names defs.mod)
70199805 =/ molds=imolds (collect-simple-molds defs.mod)
70209806 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9807+ ?: (module-has-reserved-proj mod) |
70219808 ?. %+ levy imported
70229809 |= n=term
70239810 &((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))))
@@ -7025,6 +9812,22 @@
70259812 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
70269813 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
70279814::
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+::
70289831++ module-mold-types
70299832 |= [molds=imolds state=istate]
70309833 ^- (each imold-types @t)
@@ -7040,9 +9843,9 @@
70409843::
70419844:: Prepare a provisional interface from the trusted vendored source.
70429845:: Every declared name remains reserved, but only molds and values this
7043−:: fragment can infer are usable. Unsupported bodies are not validated,
7044−:: and imports into the prelude are not supported yet. The fixed origin
7045−:: 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.
70469849::
70479850:: Recognize only the complete standard prelude list shape. Its recursive
70489851:: tail uses the same parameter and the unqualified list name. The reader
@@ -7082,6 +9885,14 @@
70829885 ?. ?=(%tvar -.i.args.tail) |
70839886 =(var name.i.args.tail)
70849887::
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+::
70859896++ partial-prelude-molds
70869897 |= [molds=imolds state=istate]
70879898 ^- imold-types
@@ -7094,26 +9905,111 @@
70949905 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
70959906 ?~ out $(molds t.molds)
70969907 =. 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)
70979909 [[name.m template.u.out] $(molds t.molds)]
70989910::
7099−++ 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
71009921 |= src=@t
71019922 ^- (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)
71029953 ?: =(0 src) ~
71039954 =/ at=path /lib/jibb/prelude/jibb
71049955 =/ parsed (parse at src)
71059956 ?: ?=(%| -.parsed) ~
7106− ?^ 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 ~
71079968 ?~ defs.p.parsed ~
71089969 ?. (module-scope-valid p.parsed ~ ~) ~
71099970 =/ ds=(list def) defs.p.parsed
71109971 =/ molds=imolds (collect-simple-molds ds)
71119972 =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7112− =/ globals=(list term) (global-value-names ds)
7113− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ ~ ~ ~ ~ ~ | at names ~]
7114− =/ mt=imold-types (partial-prelude-molds molds state)
7115− =/ env=ienv (resolve-supported-defs ds molds globals ~ ~ ~ ~ ~ ~ at ~)
7116− `[env mt at]
9973+ =/ globals=(list term) (weld (import-binding-names imports.p.parsed) (global-value-names ds))
9974+ :: Remove raw list before inferring any template, so an altered list
9975+ :: cannot leak through an alias. Its name remains reserved either way.
9976+ =/ declared=? (lien names |=(name=term =(%list name)))
9977+ =/ env-molds=imolds molds
9978+ =? env-molds declared
9979+ (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
9980+ =/ reserved=(list term) ?:(declared ~[%list] ~)
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 ~)
711710013::
711810014+$ iprelude [iface=ifile values=(list term) molds=(list term)]
711910015::
@@ -7128,6 +10024,17 @@
712810024 =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
712910025 `[u.iface vals ms]
713010026::
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+::
713110038++ module-values-complete
713210039 |= [ds=(list def) env=ienv]
713310040 ^- ?
@@ -7154,6 +10061,10 @@
715410061 ?~ imports [%& [~ cache]]
715510062 ?. ?=(%jibb -.i.imports) $(imports t.imports)
715610063 =/ 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']
715710068 ?: (lien active |=(p=path =(p at)))
715810069 [%| (crip "import cycle at {(spud at)}")]
715910070 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -7168,14 +10079,287 @@
716810079 ?: ?=(%| -.rest) rest
716910080 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
717010081::
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+::
717110346++ infer-jibb-file
717210347 |= [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)]
717310348 ^- jfile-result
7174− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
717510349 =/ parsed (parse at src)
717610350 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
717710351 =/ mod=module p.parsed
7178− ?. (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)}")]
717910363 =/ vals=(list term) (global-value-names defs.mod)
718010364 ?: (lien vals |=(n=term =(n %main)))
718110365 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
@@ -7187,13 +10371,15 @@
718710371 =/ marks=(list term) (collect-mark-imports imports.mod)
718810372 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
718910373 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7190− =/ 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 ~]
719110375 =/ mts=(each imold-types @t) (module-mold-types molds state)
719210376 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
7193− =/ 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
719410379 ?. (module-values-complete defs.mod env)
719510380 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
7196− [%& [[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]]]
719710383::
719810384:: +golden-types-with-modules fails closed for imports without prelude
719910385:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -7204,6 +10390,8 @@
720410390 ^- @t
720510391 =/ parsed (parse file src)
720610392 ?: ?=(%| -.parsed) (show-error src p.parsed)
10393+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10394+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
720710395 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
720810396 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
720910397 (golden-types-with-marks file src externals mark-externals)
@@ -7218,6 +10406,8 @@
721810406 ^- @t
721910407 =/ parsed (parse file src)
722010408 ?: ?=(%| -.parsed) (show-error src p.parsed)
10409+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10410+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
722110411 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
722210412 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
722310413 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
@@ -7225,16 +10415,26 @@
722510415 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
722610416 (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
722710417::
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+::
722810424++ golden-types-with-prepared-prelude
722910425 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
723010426 ^- @t
723110427 =/ parsed (parse file src)
723210428 ?: ?=(%| -.parsed) (show-error src p.parsed)
10429+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10430+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
723310431 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
723410432 =/ prelude-values=(list term) values.u.prepared
723510433 =/ prelude-molds=(list term) molds.u.prepared
723610434 =/ iface=(unit ifile) `iface.u.prepared
723710435 ?. (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'
723810438 'partial inference; module not checked\0amodule has conflicting names'
723910439 =/ js=jimports-result
724010440 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
@@ -7247,6 +10447,23 @@
724710447:: entries, as [mark result] with the result from +read-mark:jibb-import.
724810448:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
724910449::
10450+:: Callers pass unchanged structured reader results; graph validation
10451+:: remains in the existing bridge, and failures stay available lazily.
10452+++ reader-result-for-checker
10453+ |= result=*
10454+ ^- *
10455+ ?: ?=([%ok *] result) [%& +.result]
10456+ result
10457+::
10458+++ golden-types-with-reader-diagnostics
10459+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
10460+ ^- @t
10461+ =/ ex=iexternals
10462+ (turn externals |=(e=[module=term name=term result=*] [module.e name.e (reader-result-for-checker result.e)]))
10463+ =/ mx=imark-externals
10464+ (turn mark-externals |=(e=[mark=term result=*] [mark.e (reader-result-for-checker result.e)]))
10465+ (golden-types-with-marks file src ex mx)
10466+::
725010467++ golden-types-with-marks
725110468 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
725210469 ^- @t
@@ -7258,12 +10475,18 @@
725810475 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
725910476 =/ parsed (parse file src)
726010477 ?: ?=(%| -.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'
726110482 =/ ds=(list def) defs.p.parsed
726210483 =/ molds=imolds (collect-simple-molds ds)
726310484 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
726410485 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
726510486 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
7266− =/ 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
726710490 =/ lines=(list @t) ~
726810491 |-
726910492 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -7272,10 +10495,35 @@
727210495 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
727310496 ?. (unique-value-name name.d globals)
727410497 $(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])
727510508 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7276− =/ result=iresult (infer-fragment val.d env [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 ~]
10510+ =. initial (reserve-def-caps val.d initial)
10511+ =/ result=iresult
10512+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
10513+ (infer-recursive-gate d env initial)
10514+ (infer-fragment val.d env initial)
727710515 ?: ?=(%| -.result)
727810516 $(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])
10521+ =/ merged=(unit [first=icap second=icap])
10522+ (merged-capitals caps.state.p.result sub.state.p.result)
10523+ ?^ merged
10524+ =/ diag=idiag
10525+ ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]
10526+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
727910527 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
728010528 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
728110529 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
@@ -7292,6 +10540,8 @@
729210540 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
729310541 ?: (gth (lent vars) 26)
729410542 $(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])
729510545 =/ printable=itype (canonical-itype typ vars)
729610546 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
729710547 $(ds t.ds, lines [line lines])