@@ -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
@@ -4595,8 +4609,24 @@
45954609:: their defaulting and inferred generalization are implemented.
45964610:: Bare @ is a separate unrestricted atom type. A directional fit check
45974611:: permits concrete atoms to widen to it, never the reverse. A fit that
4598−:: needs a not-yet-implemented constraint remains unsupported. Only
4599−:: unfaced cells are represented here.
4612+:: needs a not-yet-implemented constraint remains unsupported. Named unions
4613+:: retain origin and ordered arguments, including phantom arguments, apart
4614+:: from their display name. Generic cases must be disjoint for all arguments.
4615+:: Unnamed union printing is informational; it is not Jibb syntax.
4616+::
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.
46004630::
46014631+$ itype
46024632 $~ [%var 0]
@@ -4606,15 +4636,20 @@
46064636 [%atom aura=@ta]
46074637 [%any-atom ~]
46084638 [%flag ~]
4639+ [%noun ~]
46094640 [%tag id=@ud literal=lit constructor=?]
46104641 [%const literal=lit]
4611− [%union cases=(list itype)]
4642+ [%collection name=term args=(list itype)]
4643+ [%recursive module=term name=term label=(unit @t)]
4644+ [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
4645+ [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46124646 [%face name=term body=itype]
46134647 [%fn sample=itype product=itype]
46144648 [%cell hed=itype tal=itype]
46154649 ==
46164650+$ ibinding [id=@ud val=itype]
46174651+$ isub (list ibinding)
4652++$ ipending [id=@ud literal=lit]
46184653::
46194654++ itype-lookup
46204655 |= [n=@ud sub=isub]
@@ -4656,9 +4691,13 @@
46564691 %atom |
46574692 %any-atom |
46584693 %flag |
4694+ %noun |
46594695 %tag =(n id.t)
46604696 %const |
4661− %union (lien cases.t |=(c=itype (itype-occurs n c sub)))
4697+ %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4698+ %recursive |
4699+ %jrec |
4700+ %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
46624701 %face $(t body.t)
46634702 %fn |($(t sample.t) $(t product.t))
46644703 %cell |($(t hed.t) $(t tal.t))
@@ -4676,6 +4715,18 @@
46764715 =. a (itype-walk a sub)
46774716 =. b (itype-walk b sub)
46784717 ?: =(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 ~)
4720+ ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4721+ ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
4722+ ?: &(?=(%union -.a) ?=(%union -.b))
4723+ ?. =(origin.a origin.b) ~
4724+ ?: &(?=(~ args.a) ?=(~ args.b)) ?:(=(cases.a cases.b) `sub ~)
4725+ ?~ origin.a ~
4726+ (itype-unify-args args.a args.b sub)
4727+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4728+ ?. =(name.a name.b) ~
4729+ (itype-unify-args args.a args.b sub)
46794730 ?: ?=(%var -.a)
46804731 ?: (itype-occurs id.a b sub) ~
46814732 `[[id.a b] sub]
@@ -4714,6 +4765,15 @@
47144765 $(a tal.a, b tal.b, sub u.first)
47154766 ~
47164767::
4768+++ itype-unify-args
4769+ |= [as=(list itype) bs=(list itype) sub=isub]
4770+ ^- (unit isub)
4771+ ?~ as ?~(bs `sub ~)
4772+ ?~ bs ~
4773+ =/ next=(unit isub) (itype-unify i.as i.bs sub)
4774+ ?~ next ~
4775+ $(as t.as, bs t.bs, sub u.next)
4776+::
47174777:: +itype-fit: one-way widening from an actual type to an expected type
47184778::
47194779:: An unknown variable used where @ is expected gains a fresh atom
@@ -4731,9 +4791,13 @@
47314791 %atom |
47324792 %any-atom &
47334793 %flag |
4794+ %noun |
47344795 %tag |
47354796 %const |
4736− %union (lien cases.t |=(c=itype (itype-has-any-atom c sub)))
4797+ %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4798+ %recursive |
4799+ %jrec |
4800+ %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
47374801 %face $(t body.t)
47384802 %fn |($(t sample.t) $(t product.t))
47394803 %cell |($(t hed.t) $(t tal.t))
@@ -4757,6 +4821,14 @@
47574821:: Related auras in a structural unification need a common-type rule;
47584822:: until that rule is implemented, report an unknown rather than error.
47594823::
4824+++ itype-family-related-collection-args
4825+ |= [as=(list itype) bs=(list itype) sub=isub]
4826+ ^- ?
4827+ ?~ as |
4828+ ?~ bs |
4829+ ?: (itype-family-related i.as i.bs sub) &
4830+ $(as t.as, bs t.bs)
4831+::
47604832++ itype-family-related
47614833 |= [a=itype b=itype sub=isub]
47624834 ^- ?
@@ -4765,6 +4837,9 @@
47654837 ?: &(?=(%atom -.a) ?=(%atom -.b))
47664838 ?. !=(aura.a aura.b) |
47674839 |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4840+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4841+ ?. =(name.a name.b) |
4842+ (itype-family-related-collection-args args.a args.b sub)
47684843 ?: &(?=(%face -.a) ?=(%face -.b))
47694844 ?. =(name.a name.b) |
47704845 $(a body.a, b body.b)
@@ -4788,9 +4863,13 @@
47884863 %atom &
47894864 %any-atom &
47904865 %flag &
4866+ %noun |
47914867 %tag &
47924868 %const &
4793− %union (lien cases.typ |=(c=itype (itype-has-fixed-atom c)))
4869+ %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4870+ %recursive |
4871+ %jrec |
4872+ %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
47944873 %face $(typ body.typ)
47954874 %fn |($(typ sample.typ) $(typ product.typ))
47964875 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -4818,17 +4897,29 @@
48184897 ^- ?
48194898 =. t (itype-walk t sub)
48204899 ?- -.t
4900+ %collection (lien args.t |=(c=itype (itype-has-face c sub)))
48214901 %face &
48224902 %cell |($(t hed.t) $(t tal.t))
48234903 %fn |($(t sample.t) $(t product.t))
48244904 * |
48254905 ==
48264906::
4907+++ itype-face-asym-collection-args
4908+ |= [as=(list itype) bs=(list itype) sub=isub]
4909+ ^- ?
4910+ ?~ as |
4911+ ?~ bs |
4912+ ?: (itype-face-asym i.as i.bs sub) &
4913+ $(as t.as, bs t.bs)
4914+::
48274915++ itype-face-asym
48284916 |= [a=itype b=itype sub=isub]
48294917 ^- ?
48304918 =. a (itype-walk a sub)
48314919 =. b (itype-walk b sub)
4920+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4921+ ?. =(name.a name.b) |
4922+ (itype-face-asym-collection-args args.a args.b sub)
48324923 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
48334924 ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
48344925 ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
@@ -4862,16 +4953,27 @@
48624953 %var &
48634954 %cell &
48644955 %union &
4956+ %recursive &
4957+ %jrec &
4958+ %noun &
4959+ %collection &
48654960 %face $(t body.t)
48664961 %fn |($(t sample.t) $(t product.t))
48674962 * |
48684963 ==
48694964::
48704965++ pending-tags
4871− |= [tags=(list @ud) sub=isub]
4966+ |= [tags=(list ipending) sub=isub]
4967+ ^- ?
4968+ ?~ tags |
4969+ ?~ (itype-lookup id.i.tags sub) &
4970+ $(tags t.tags)
4971+::
4972+++ pending-null
4973+ |= [tags=(list ipending) sub=isub]
48724974 ^- ?
48734975 ?~ tags |
4874− ?~ (itype-lookup i.tags sub) &
4976+ ?: &(?=(%null form.literal.i.tags) ?=(~ (itype-lookup id.i.tags sub))) &
48754977 $(tags t.tags)
48764978::
48774979:: Tags remain constrained until a mold selects a case or permitted atom
@@ -4882,10 +4984,11 @@
48824984 ^- ?
48834985 ?- -.t
48844986 %tag &
4987+ %collection (lien args.t |=(c=itype (itype-has-tag c)))
48854988 %face $(t body.t)
48864989 %fn |($(t sample.t) $(t product.t))
48874990 %cell |($(t hed.t) $(t tal.t))
4888− %union (lien cases.t |=(c=itype (itype-has-tag c)))
4991+ %union |((lien cases.t |=(c=itype (itype-has-tag c))) (lien args.t |=(c=itype (itype-has-tag c))))
48894992 * |
48904993 ==
48914994::
@@ -4894,12 +4997,59 @@
48944997 ^- ?
48954998 ?- -.t
48964999 %union &
5000+ %collection (lien args.t |=(c=itype (itype-has-union c)))
48975001 %face $(t body.t)
48985002 %fn |($(t sample.t) $(t product.t))
48995003 %cell |($(t hed.t) $(t tal.t))
49005004 * |
49015005 ==
49025006::
5007+:: Until a visible generic alias can be selected, expanding a named
5008+:: generic union would hide phantom arguments and its origin. This is a
5009+:: limitation of partial inference, not the unnamed-union print notation.
5010+::
5011+++ itype-has-hidden-generic
5012+ |= t=itype
5013+ ^- ?
5014+ ?- -.t
5015+ %union
5016+ ?: &(?=(~ label.t) ?=(^ args.t)) &
5017+ (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
5018+ %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
5019+ %face $(t body.t)
5020+ %fn |($(t sample.t) $(t product.t))
5021+ %cell |($(t hed.t) $(t tal.t))
5022+ * |
5023+ ==
5024+::
5025+++ itype-has-recursive
5026+ |= t=itype
5027+ ^- ?
5028+ ?- -.t
5029+ %recursive &
5030+ %jrec &
5031+ %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5032+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5033+ %face $(t body.t)
5034+ %cell |($(t hed.t) $(t tal.t))
5035+ %fn |($(t sample.t) $(t product.t))
5036+ * |
5037+ ==
5038+::
5039+++ itype-has-hidden-recursive
5040+ |= t=itype
5041+ ^- ?
5042+ ?- -.t
5043+ %recursive ?=(~ label.t)
5044+ %jrec ?=(~ label.t)
5045+ %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5046+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5047+ %face $(t body.t)
5048+ %cell |($(t hed.t) $(t tal.t))
5049+ %fn |($(t sample.t) $(t product.t))
5050+ * |
5051+ ==
5052+::
49035053++ itype-fit-cases
49045054 |= [actual=itype cases=(list itype) sub=isub next=@ud]
49055055 ^- ifit
@@ -4933,6 +5083,7 @@
49335083 ?. ?=(%cell -.c) $(cases t.cases)
49345084 =/ head=itype (itype-walk hed.c sub)
49355085 ?. ?=(%const -.head) $(cases t.cases)
5086+ ?. =(%term form.literal.head) $(cases t.cases)
49365087 ?. =(val.literal.head val.tag) $(cases t.cases)
49375088 ?^ found [%unknown ~]
49385089 =/ trial=ifit (itype-fit sample tal.c sub next)
@@ -4941,12 +5092,63 @@
49415092++ itype-fit
49425093 |= [actual=itype expected=itype sub=isub next=@ud]
49435094 ^- 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))
49445107 =/ uncertain=?
49455108 |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5109+ =/ actual-open=?
5110+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
49465111 =. actual (itype-walk actual sub)
49475112 =. expected (itype-walk expected sub)
49485113 ?: =(actual expected) [%ok sub next]
4949− ?: &(?=(%union -.actual) ?=(%union -.expected)) [%unknown ~]
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 ~]
5128+ ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
5129+ ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
5130+ ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
5131+ ?: &(?=(%union -.actual) ?=(%union -.expected))
5132+ ?. =(origin.actual origin.expected) [%unknown ~]
5133+ ?: &(?=(~ args.actual) ?=(~ args.expected))
5134+ ?:(=(cases.actual cases.expected) [%ok sub next] [%unknown ~])
5135+ ?~ origin.actual [%unknown ~]
5136+ =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
5137+ ?^ unified [%ok u.unified next]
5138+ [%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)
49505152 ?: ?=(%union -.actual) [%unknown ~]
49515153 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
49525154 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -4965,6 +5167,10 @@
49655167 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
49665168 ?. ?=(%ok -.trial) trial
49675169 [%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 ~]
49685174 ?: ?=(%const -.expected)
49695175 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
49705176 ?: ?=(%atom -.expected)
@@ -4982,6 +5188,8 @@
49825188 [%ok u.u next]
49835189 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
49845190 ?: ?=(%face -.expected) $(expected body.expected)
5191+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5192+ [%unknown ~]
49855193 ?: ?=(%const -.expected)
49865194 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
49875195 ?: ?=(%atom -.expected)
@@ -5011,27 +5219,40 @@
50115219 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
50125220 [%bad ~]
50135221 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5014− =/ first=ifit $(actual hed.actual, expected hed.expected)
5222+ =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
50155223 ?. ?=(%ok -.first) first
5016− $(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)
5225+ :: A field may add a face to an occurrence of the very same type
5226+ :: variable. Binding that variable to a face around itself would fail
5227+ :: the occurs check, but its underlying type has already matched.
5228+ ?: &(?=(%var -.actual) ?=(%face -.expected) =(actual (itype-walk body.expected sub)))
5229+ [%ok sub next]
5230+ :: Differing variables and faces need propagation that is not yet
5231+ :: represented. Binding one to the face can create a false mismatch.
5232+ ?: &(?=(%var -.actual) ?=(%face -.expected)) [%unknown ~]
5233+ ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
50175234 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
50185235 [%unknown ~]
50195236 ?: |(?=(%var -.actual) ?=(%var -.expected))
50205237 =/ unified=(unit isub) (itype-unify actual expected sub)
50215238 ?~ unified
5239+ ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5240+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
50225241 ?: (itype-family-related actual expected sub) [%unknown ~]
50235242 [%bad ~]
50245243 [%ok u.unified next]
50255244 ?: &(?=(%face -.actual) ?=(%face -.expected))
50265245 ?. =(name.actual name.expected) [%bad ~]
5027− $(actual body.actual, expected body.expected)
5028− ?: ?=(%face -.actual) $(actual body.actual)
5029− ?: ?=(%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 |)
50305249 ?: (itype-face-asym actual expected sub) [%unknown ~]
50315250 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
50325251 [%unknown ~]
50335252 =/ unified=(unit isub) (itype-unify actual expected sub)
50345253 ?~ unified
5254+ ?: |((itype-has-union (itype-normalize actual sub)) (itype-has-union (itype-normalize expected sub))) [%unknown ~]
5255+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
50355256 ?: (itype-family-related actual expected sub) [%unknown ~]
50365257 [%bad ~]
50375258 [%ok u.unified next]
@@ -5060,25 +5281,153 @@
50605281 ["a shared type variable should reject incompatible arguments" problems]
50615282 =? problems ?=(~ (itype-unify same fine ~))
50625283 ["a shared type variable should accept equal arguments" problems]
5284+ =/ list-a=itype [%collection %list ~[a]]
5285+ =/ list-t=itype [%collection %list ~[txt]]
5286+ =/ list-n=itype [%collection %list ~[num]]
5287+ =? problems ?=(^ (itype-unify a list-a ~))
5288+ ["occurs check should look through collection arguments" problems]
5289+ =? problems !=((itype-vars list-a) ~[0])
5290+ ["generalization should see collection argument variables" problems]
5291+ =? problems !=((itype-rename list-a ~[[0 num]]) list-n)
5292+ ["instantiation should rename collection argument variables" problems]
5293+ =? problems ?=(^ (itype-unify list-t list-n ~))
5294+ ["collection arguments with different auras should conflict" problems]
5295+ =? problems ?=(^ (itype-unify list-t [%collection %unit ~[txt]] ~))
5296+ ["different collection names should conflict" problems]
5297+ =? problems !(itype-family-related list-t [%collection %list ~[[%atom 'tD']]] ~)
5298+ ["collection arguments should preserve aura-family uncertainty" problems]
5299+ =? problems !(itype-face-asym [%collection %list ~[[%face %x txt]]] list-t ~)
5300+ ["collection arguments should preserve face uncertainty" problems]
5301+ =/ recursive=itype [%recursive %fixture %chain `'chain.fixture']
5302+ =/ same-recursive=itype [%recursive %fixture %chain ~]
5303+ =/ other-recursive=itype [%recursive %other %chain `'chain.other']
5304+ =? problems ?=(~ (itype-unify recursive same-recursive ~))
5305+ ["recursive identity should not depend on its visible name" problems]
5306+ =? problems ?=(^ (itype-unify recursive other-recursive ~))
5307+ ["recursive identity should include the source module" problems]
5308+ =/ recursive-fit=ifit (itype-fit recursive txt ~ 0)
5309+ =? problems !?=(%unknown -.recursive-fit)
5310+ ["opaque recursive types should not be unfolded by a fit" problems]
5311+ =/ nested-fit=ifit
5312+ (itype-fit [%collection %list ~[a]] list-t ~[[0 recursive]] 1)
5313+ =? problems !?=(%unknown -.nested-fit)
5314+ ["recursive types behind substitutions should remain uncertain" problems]
50635315 problems
50645316::
50655317:: The expression inference below is deliberately a fragment: bindings,
5066−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5318+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
50675319:: result for unsupported syntax is a diagnostic, never a checked module.
50685320::
50695321+$ ischeme [typ=itype vars=(list @ud)]
50705322+$ ienv (list [name=term scheme=ischeme])
50715323+$ imold-types (list [name=term template=ischeme])
5072−+$ ifile [values=ienv molds=imold-types]
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)]
50735328+$ ijimports (list [face=term interface=ifile])
5074−+$ icaps (list [name=@t id=@ud])
5329++$ icap [name=@t id=@ud at=span]
5330++$ icaps (list icap)
50755331+$ iparams (list [name=@t typ=itype])
50765332+$ imolds (list [name=term body=shape])
50775333:: A caller supplies the exact noun returned by +read-mold:jibb-import.
50785334:: This core has no Ford dependencies; unrecognized payloads fail closed.
50795335+$ iexternals (list [module=term name=term result=*])
50805336+$ imark-externals (list [mark=term result=*])
5081−+$ 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 @ud) in-mold=?]
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)]
50825431+$ idiag [msg=tape sites=(list [at=span note=tape])]
50835432+$ iresult (each [typ=itype state=istate] idiag)
50845433+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5098,8 +5447,9 @@
50985447 |= [t=itype sub=isub]
50995448 ^- itype
51005449 =. t (itype-walk t sub)
5450+ ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
51015451 ?: ?=(%union -.t)
5102− [%union (turn cases.t |=(c=itype (itype-normalize c sub)))]
5452+ [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
51035453 ?: ?=(%face -.t)
51045454 [%face name.t $(t body.t)]
51055455 ?: ?=(%fn -.t)
@@ -5113,12 +5463,17 @@
51135463:: generalize an aura from its sample, which requires constraint analysis
51145464:: beyond this fragment; leave those cases unresolved.
51155465::
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.
51165468++ itype-has-gate
51175469 |= t=itype
51185470 ^- ?
51195471 ?- -.t
51205472 %fn &
51215473 %cell |($(t hed.t) $(t tal.t))
5474+ %recursive |
5475+ %jrec |
5476+ %collection (lien args.t |=(c=itype (itype-has-gate c)))
51225477 %face $(t body.t)
51235478 %union (lien cases.t |=(c=itype (itype-has-gate c)))
51245479 %tag |
@@ -5129,6 +5484,7 @@
51295484 %atom |
51305485 %any-atom |
51315486 %flag |
5487+ %noun |
51325488 ==
51335489::
51345490++ default-decimals
@@ -5137,11 +5493,96 @@
51375493 ?: (itype-has-gate t) t
51385494 ?- -.t
51395495 %nvar [%atom %ud]
5496+ %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
51405497 %face [%face name.t $(t body.t)]
51415498 %cell [%cell $(t hed.t) $(t tal.t)]
51425499 * t
51435500 ==
51445501::
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+::
51455586++ itype-vars
51465587 |= t=itype
51475588 ^- (list @ud)
@@ -5152,9 +5593,13 @@
51525593 %atom ~
51535594 %any-atom ~
51545595 %flag ~
5596+ %noun ~
51555597 %tag ~
51565598 %const ~
5157− %union (zing (turn cases.t |=(c=itype (itype-vars c))))
5599+ %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5600+ %recursive ~
5601+ %jrec ~
5602+ %collection (zing (turn args.t |=(c=itype (itype-vars c))))
51585603 %face $(t body.t)
51595604 %fn (weld $(t sample.t) $(t product.t))
51605605 %cell (weld $(t hed.t) $(t tal.t))
@@ -5188,9 +5633,13 @@
51885633 %atom t
51895634 %any-atom t
51905635 %flag t
5636+ %noun t
51915637 %tag t
51925638 %const t
5193− %union [%union (turn cases.t |=(c=itype (itype-rename c ren)))]
5639+ %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5640+ %recursive t
5641+ %jrec t
5642+ %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
51945643 %face [%face name.t $(t body.t)]
51955644 %fn [%fn $(t sample.t) $(t product.t)]
51965645 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5209,9 +5658,13 @@
52095658 %atom |
52105659 %any-atom |
52115660 %flag |
5661+ %noun |
52125662 %tag |
52135663 %const |
5214− %union (lien cases.t |=(c=itype (itype-var-is-atom n c)))
5664+ %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5665+ %recursive |
5666+ %jrec |
5667+ %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
52155668 %face $(t body.t)
52165669 %fn |($(t sample.t) $(t product.t))
52175670 %cell |($(t hed.t) $(t tal.t))
@@ -5273,9 +5726,12 @@
52735726 $(ds t.ds)
52745727::
52755728::
5276−:: The importer owns its algebra. Fixed atoms, cells and Jibb-named faces
5277−:: are decoded recursively. Singletons, unions, collections, recursive
5278−:: references and invalid face names remain unsupported, never widened.
5729+:: The caller supplies unchanged results from the source-aware importer.
5730+:: That boundary is trusted for source provenance: a fork alone cannot
5731+:: reveal cases Hoon collapsed before it was constructed. Validate the
5732+:: supplied graph independently, including pairwise disjointness. Fixed
5733+:: atoms, term singletons, cells, faces and proven forks are decoded;
5734+:: unsupported singletons, collections and recursive references fail.
52795735::
52805736++ jibb-face-name
52815737 |= name=@
@@ -5285,16 +5741,180 @@
52855741 ?. (is-lower i.chars) |
52865742 (levy t.chars |=(c=@tD (in c name-mask)))
52875743::
5744+:: A source-aware reader result is trusted for origin. Validate every
5745+:: supplied branch and keep the recursive mold opaque: unfolding its
5746+:: root while naming only its tail would change its type identity.
5747++$ irec-pattern [pat=upat has=?]
5748+++ rec-pattern
5749+ |= [node=* module=term name=term]
5750+ ^- (unit irec-pattern)
5751+ ?@ node ~
5752+ ?+ -.node ~
5753+ %atom
5754+ ?: ?=([%atom %n [~ @]] node)
5755+ ?. =(0 +>+.node) ~
5756+ `[[%atom `0] |]
5757+ ?: ?=([%atom %tas [~ @]] node)
5758+ =/ value=@ +>+.node
5759+ ?. |(=(value 0) (jibb-face-name value)) ~
5760+ `[[%atom `value] |]
5761+ ?. ?=([%atom @ ~] node) ~
5762+ =/ aura=@ta (@ta +<.node)
5763+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5764+ `[[%atom ~] |]
5765+ %ref
5766+ ?. ?=([%ref @ @] node) ~
5767+ ?. &(=(module +<.node) =(name +>.node)) ~
5768+ `[[%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]
5774+ %face
5775+ ?. ?=([%face @ *] node) ~
5776+ ?. (jibb-face-name +<.node) ~
5777+ $(node +>.node)
5778+ %cell
5779+ ?. ?=([%cell * *] node) ~
5780+ =/ left $(node +<.node)
5781+ ?~ left ~
5782+ =/ right $(node +>.node)
5783+ ?~ right ~
5784+ `[[%cell pat.u.left pat.u.right] |(has.u.left has.u.right)]
5785+ %fork
5786+ =/ cases (rec-patterns +.node module name)
5787+ ?~ cases ~
5788+ ?~ pats.u.cases ~
5789+ ?~ t.pats.u.cases ~
5790+ ?. (rec-patterns-disjoint pats.u.cases) ~
5791+ `[[%or pats.u.cases] has.u.cases]
5792+ ==
5793+::
5794+++ rec-patterns
5795+ |= [nodes=* module=term name=term]
5796+ ^- (unit [pats=(list upat) has=?])
5797+ ?@ nodes ?:(=(nodes 0) `[~ |] ~)
5798+ =/ first (rec-pattern -.nodes module name)
5799+ ?~ first ~
5800+ =/ rest $(nodes +.nodes)
5801+ ?~ rest ~
5802+ `[[pat.u.first pats.u.rest] |(has.u.first has.u.rest)]
5803+::
5804+++ rec-patterns-disjoint
5805+ |= pats=(list upat)
5806+ ^- ?
5807+ ?~ pats &
5808+ ?. (levy t.pats |=(p=upat =(%disjoint (union-relate i.pats p)))) |
5809+ $(pats t.pats)
5810+::
5811+::
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+::
52885858++ import-to-itype
52895859 |= node=*
52905860 ^- (unit itype)
52915861 ?@ node ~
52925862 ?+ -.node ~
5863+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
52935864 %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 '~']]
5876+ ?: ?=([%atom %tas [~ @]] node)
5877+ =/ value=@ +>+.node
5878+ ?. |(=(value 0) (jibb-face-name value)) ~
5879+ =/ printed=@t ?:(=(value 0) '%$' (cat 3 '%' value))
5880+ `[%const [%term %tas value printed]]
52945881 ?. ?=([%atom @ ~] node) ~
52955882 =/ aura=@ta (@ta +<.node)
52965883 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
52975884 `[%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)}")]
5894+ %apply
5895+ ?. ?=([%apply @ *] node) ~
5896+ =/ name=term (@tas +<.node)
5897+ =/ arity=@ud
5898+ ?: |(=(%list name) =(%unit name) =(%set name) =(%qeu name)) 1
5899+ ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
5900+ 0
5901+ ?: =(arity 0) ~
5902+ =/ args=(unit (list itype)) (import-to-itypes +>.node)
5903+ ?~ args ~
5904+ ?. =(arity (lent u.args)) ~
5905+ `[%collection name u.args]
5906+ %fork
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)
5912+ ?~ cases ~
5913+ ?~ u.cases ~
5914+ ?~ t.u.cases ~
5915+ ?: (import-has-loobean-singleton u.cases) ~
5916+ ?. (import-cases-disjoint u.cases) ~
5917+ `[%union u.cases ~ ~ ~]
52985918 %face
52995919 ?. ?=([%face @ *] node) ~
53005920 =/ name=@ +<.node
@@ -5311,6 +5931,52 @@
53115931 `[%cell u.left u.right]
53125932 ==
53135933::
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+::
5948+++ import-to-itypes
5949+ |= nodes=*
5950+ ^- (unit (list itype))
5951+ ?@ nodes ?:(=(nodes 0) `~ ~)
5952+ =/ first (import-to-itype -.nodes)
5953+ ?~ first ~
5954+ =/ rest $(nodes +.nodes)
5955+ ?~ rest ~
5956+ `[u.first u.rest]
5957+::
5958+++ import-type-pattern
5959+ |= typ=itype
5960+ ^- upat
5961+ ?- -.typ
5962+ %noun [%all ~]
5963+ %atom [%atom ~]
5964+ %flag [%or ~[[%atom `0] [%atom `1]]]
5965+ %const [%atom `val.literal.typ]
5966+ %face $(typ body.typ)
5967+ %cell [%cell $(typ hed.typ) $(typ tal.typ)]
5968+ %union [%or (turn cases.typ |=(t=itype (import-type-pattern t)))]
5969+ * [%unknown ~]
5970+ ==
5971+::
5972+++ import-cases-disjoint
5973+ |= cases=(list itype)
5974+ ^- ?
5975+ ?~ cases &
5976+ =/ first=upat (import-type-pattern i.cases)
5977+ ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
5978+ $(cases t.cases)
5979+::
53145980++ find-imported-mold
53155981 |= [module=term name=term externals=iexternals surs=(list term)]
53165982 ^- (unit itype)
@@ -5322,7 +5988,15 @@
53225988 =/ result=* result.i.found
53235989 ?@ result ~
53245990 ?. ?=(%& -.result) ~
5325− (import-to-itype +.result)
5991+ =/ node=* +.result
5992+ ?. (imported-faces-valid node) ~
5993+ ?@ node (import-to-itype node)
5994+ ?: ?=(%ref -.node) (import-to-itype node)
5995+ =/ pattern=(unit irec-pattern) (rec-pattern node module name)
5996+ ?~ pattern (import-to-itype node)
5997+ ?. has.u.pattern (import-to-itype node)
5998+ `[%recursive module name `(crip "{(trip name)}.{(trip module)}")]
5999+
53266000::
53276001++ collect-sur-imports
53286002 |= imports=(list import)
@@ -5351,6 +6025,7 @@
53516025 =/ result=* result.i.found
53526026 ?@ result ~
53536027 ?. ?=(%& -.result) ~
6028+ ?. (imported-faces-valid +.result) ~
53546029 (import-to-itype +.result)
53556030::
53566031++ find-jibb-interface
@@ -5369,9 +6044,88 @@
53696044 ?: =(name name.i.ms) `template.i.ms
53706045 $(ms t.ms)
53716046::
6047+:: An exported alias may name a union from another module. Only a
6048+:: nongeneric alias of the same origin is usable through this import face.
6049+::
6050+++ imported-union-alias
6051+ |= [origin=[at=path name=term] molds=imold-types]
6052+ ^- (unit term)
6053+ ?~ molds ~
6054+ =/ template=ischeme template.i.molds
6055+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
6056+ ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
6057+ $(molds t.molds)
6058+::
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)
6081+::
6082+++ itype-in-import
6083+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6084+ ^- itype
6085+ ?- -.t
6086+ %union
6087+ =/ label=(unit @t)
6088+ ?~ origin.t ~
6089+ ?: =(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
6094+ =/ alias=(unit term) ~
6095+ =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
6096+ =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
6097+ ?~ alias ~
6098+ `(crip "{(trip u.alias)}.{(trip 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)))]
6100+ %recursive [%recursive module.t name.t ~]
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)))]
6108+ %face [%face name.t $(t body.t)]
6109+ %fn [%fn $(t sample.t) $(t product.t)]
6110+ %cell [%cell $(t hed.t) $(t tal.t)]
6111+ * t
6112+ ==
6113+::
6114+++ label-direct-union
6115+ |= [typ=itype body=shape name=term state=istate]
6116+ ^- itype
6117+ ?. ?=(%union -.typ) typ
6118+ =/ direct=? ?=(%union -.body)
6119+ =? direct ?=(%generic -.body) ?=(%union -.body.body)
6120+ ?. direct typ
6121+ ?. (lien top-molds.state |=(n=term =(n name))) typ
6122+ [%union cases.typ `[at.state name] `name args.typ]
6123+::
53726124:: Generic mold parameters are lexical and distinct from the enclosing
53736125:: value's capital variables. Arguments are substituted only once, so
53746126:: an argument's variable ID cannot be captured by a template ID.
6127+:: A generic alias of a named union keeps the underlying union's origin
6128+:: and substituted argument order; an originless union stays unsupported.
53756129::
53766130++ iparam-lookup
53776131 |= [name=@t params=iparams]
@@ -5423,9 +6177,46 @@
54236177 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
54246178 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
54256179::
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+::
54266213++ infer-mold-template
54276214 |= [sh=shape state=istate]
54286215 ^- (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]
54296220 ?: ?=(%generic -.sh)
54306221 ?~ vars.sh ~
54316222 ?. (distinct-params vars.sh) ~
@@ -5433,33 +6224,136 @@
54336224 =/ out=(unit [typ=itype state=istate])
54346225 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
54356226 ?~ out ~
6227+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
6228+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
6229+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
6230+ typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
54366231 =/ used=(list @ud) (itype-vars typ.u.out)
54376232 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5438− `[[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)]
54396234 =/ out=(unit [typ=itype state=istate])
54406235 (infer-simple-shape sh state(params ~, in-mold &))
54416236 ?~ out ~
6237+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
54426238 ?: ?=(^ (itype-vars typ.u.out)) ~
5443− `[[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)
54446337::
54456338++ infer-simple-shape
54466339 |= [sh=shape state=istate]
54476340 ^- (unit [typ=itype state=istate])
54486341 ?- -.sh
6342+ %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
54496343 %aura
54506344 ?: =(0 aura.sh) `[[%any-atom ~] state]
54516345 `[[%atom aura.sh] state]
54526346 %flag `[[%flag ~] state]
6347+ %noun `[[%noun ~] state]
54536348 %const
5454− ?. =(%term form.lit.sh) ~
6349+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
54556350 `[[%const lit.sh] state]
54566351 %union
54576352 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
54586353 ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
54596354 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
54606355 ?~ cs ~
5461− ?: (lien types.u.cs |=(t=itype ?=(^ (itype-vars t)))) ~
5462− `[[%union types.u.cs] state.u.cs]
6356+ `[[%union types.u.cs ~ ~ ~] state.u.cs]
54636357 %cell (infer-simple-fields fields.sh state)
54646358 %fn
54656359 =/ arg=(unit [typ=itype state=istate]) $(sh sample.sh)
@@ -5477,7 +6371,7 @@
54776371 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
54786372 ?~ found ~
54796373 ?^ vars.u.found ~
5480− `[typ.u.found state]
6374+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
54816375 =/ found=(unit itype)
54826376 (find-imported-mold i.t.names.sh n externals.state surs.state)
54836377 ?~ found ~
@@ -5489,11 +6383,20 @@
54896383 `[u.imported state]
54906384 ?: (lien active.state |=(x=term =(x n))) ~
54916385 =/ found=(unit shape) (find-simple-mold n molds.state)
5492− ?~ found ~
6386+ ?~ found
6387+ ?: (lien molds.state |=(m=[name=term body=shape] =(name.m n))) ~
6388+ ?~ prelude.state ~
6389+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state)
6390+ ?~ prelude-entry ~
6391+ ?^ vars.u.prelude-entry ~
6392+ `[typ.u.prelude-entry state]
6393+ =/ direct=(unit itype) (simple-source-recursive n u.found state)
6394+ ?^ direct `[u.direct state]
54936395 =/ out=(unit [typ=itype state=istate])
54946396 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
54956397 ?~ out ~
5496− `[typ.u.out 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)]
54976400 %apply
54986401 ?~ ref.sh ~
54996402 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -5508,10 +6411,18 @@
55086411 ?~ vars.u.template ~
55096412 =/ applied=(unit itype) (template-apply u.template types.u.args)
55106413 ?~ applied ~
5511− `[u.applied state.u.args]
6414+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
55126415 ?: (lien active.state.u.args |=(x=term =(x n))) ~
55136416 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
5514− ?~ found ~
6417+ ?~ found
6418+ ?: (lien molds.state.u.args |=(m=[name=term body=shape] =(name.m n))) ~
6419+ ?~ prelude.state.u.args ~
6420+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state.u.args)
6421+ ?~ prelude-entry ~
6422+ ?~ vars.u.prelude-entry ~
6423+ =/ applied=(unit itype) (template-apply u.prelude-entry types.u.args)
6424+ ?~ applied ~
6425+ `[u.applied state.u.args]
55156426 ?. ?=(%generic -.u.found) ~
55166427 ?. (distinct-params vars.u.found) ~
55176428 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
@@ -5519,14 +6430,19 @@
55196430 =/ out=(unit [typ=itype state=istate])
55206431 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
55216432 ?~ out ~
5522− `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
6433+ ?^ (unresolved-hole holes.state.u.out holes.state.u.args state.u.out) ~
6434+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
6435+ ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
6436+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
6437+ (label-direct-union typ.u.out(args types.u.args) u.found n 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)]
55236439 %tvar
55246440 =/ param=(unit itype) (iparam-lookup name.sh params.state)
55256441 ?^ param `[u.param state]
55266442 ?: in-mold.state ~
55276443 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
55286444 ?^ n `[[%var u.n] state]
5529− `[[%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])]
55306446 * ~
55316447 ==
55326448::
@@ -5559,12 +6475,12 @@
55596475 ^- isample-result
55606476 ?- -.s
55616477 %bind
5562− ?: |(?=(^ (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))))
55636479 [%| "sample shadows a name"]
55646480 =/ t=itype [%var next.state]
55656481 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
55666482 %face
5567− ?: |(?=(^ (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))))
55686484 [%| "sample shadows a name"]
55696485 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
55706486 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -5602,8 +6518,8 @@
56026518 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
56036519::
56046520:: Local definitions generalize only variables outside their enclosing
5605−:: environment and explicit-capital scope. Unresolved groups stay
5606−:: 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.
56076523::
56086524+$ ilocal-result (each [env=ienv state=istate] idiag)
56096525++ free-env-vars
@@ -5632,6 +6548,7 @@
56326548 |-
56336549 ?~ ds &
56346550 ?: ?=(%mold -.i.ds) $(ds t.ds)
6551+ ?: =(name.i.ds %proj) |
56356552 ?. (unique-value-name name.i.ds names) |
56366553 ?: ?=(^ (ienv-lookup name.i.ds env)) |
56376554 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -5655,6 +6572,7 @@
56556572 |-
56566573 ?~ locals &
56576574 =/ n=term name.i.locals
6575+ ?: =(n %proj) |
56586576 ?. (unique-value-name n names) |
56596577 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
56606578 ?: (lien marks.state |=(m=term =(n m))) |
@@ -5672,6 +6590,145 @@
56726590 ?~ inferred |
56736591 $(locals t.locals)
56746592::
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+::
56756732++ infer-local-defs
56766733 |= [ds=(list def) env=ienv state=istate]
56776734 ^- ilocal-result
@@ -5680,26 +6737,65 @@
56806737 |-
56816738 ?~ ds
56826739 ?~ remaining [%& env state]
5683− ?. 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 |)
56846747 $(ds (flop remaining), remaining ~, progressed |)
56856748 =/ d=def i.ds
56866749 ?> ?=(%value -.d)
5687− =/ 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)
56886754 ?: ?=(%| -.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" ~]]
56896764 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
56906765 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
56916766 $(ds t.ds, remaining [d remaining])
56926767 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
56936768 $(ds t.ds, remaining [d remaining])
56946769 =/ free=(list @ud)
5695− (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))
56966771 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
56976772 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
5698− $(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]
56996795::
57006796:: Read only fields of a known record. Unresolved field constraints and
5701−:: ambiguous repeated faces are outside this fragment (doc question:
5702−:: 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.
57036799::
57046800++ record-fields-named
57056801 |= [name=term t=itype sub=isub]
@@ -5718,92 +6814,1038 @@
57186814 ^- iresult
57196815 =/ reverse=(list term) (flop names)
57206816 ?~ reverse [%| ["empty wing" ~]]
5721− =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
5722− ?~ scheme [%| ["field access is not supported by partial inference" ~]]
5723− =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
6817+ =/ iface=(unit ifile) (find-jibb-interface i.reverse jimports.state)
57246818 =/ 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)
57256833 =/ typ=itype typ.inst
57266834 |-
5727− ?~ fields [%& typ state.inst]
5728− =/ 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)
57296837 ?~ found [%| ["field is not available to partial inference" ~]]
57306838 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
5731− $(fields t.fields, typ i.found)
6839+ $(remaining t.remaining, typ i.found)
57326840::
5733−++ infer-fragment
5734− |= [e=expr env=ienv state=istate]
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.
6844+::
6845+++ context-union-branch
6846+ |= e=expr
6847+ ^- ?
6848+ ?- -.e
6849+ %branch &
6850+ %group $(e inner.e)
6851+ %body ?~(defs.e $(e final.e) |)
6852+ * |
6853+ ==
6854+::
6855+++ infer-union-context
6856+ |= [e=expr expected=itype env=ienv state=istate context=span]
57356857 ^- iresult
6858+ ?: ?=(%group -.e) $(e inner.e)
6859+ ?: &(?=(%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)
6862+ ?: ?=(%branch -.e)
6863+ ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
6864+ ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
6865+ ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
6866+ =/ x=arm i.arms.e
6867+ =/ y=arm i.t.arms.e
6868+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
6869+ (infer-unit-branch e env state `[expected context])
6870+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y))
6871+ [%| ["branch pattern is not supported by partial inference" ~]]
6872+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6873+ [%| ["branch pattern is not supported by partial inference" ~]]
6874+ ?: =(val.lit.pat.x val.lit.pat.y)
6875+ [%| ["branch does not cover both loobeans" ~]]
6876+ =/ subject=iresult (infer-fragment subject.e env state)
6877+ ?: ?=(%| -.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" ~]]
6881+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
6882+ ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
6883+ =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
6884+ ?: ?=(%| -.left) left
6885+ =/ right=iresult $(e val.y, state state.p.left)
6886+ ?: ?=(%| -.right) right
6887+ [%& expected state.p.right]
6888+ =/ value=iresult (infer-fragment e env state)
6889+ ?: ?=(%| -.value) value
6890+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
6891+ ?: ?=(%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" ~]]
6895+ [%| ["branch union constraint is not supported by partial inference" ~]]
6896+ ?: ?=(%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"]]]]
6905+ [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
6906+ [%& expected state.p.value(sub sub.fit, next next.fit)]
6907+::
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.
6911+::
6912+++ context-list-expression
6913+ |= e=expr
6914+ ^- ?
57366915 ?- -.e
5737− %lit
5738− ?- form.lit.e
5739− %number ?: =(%ud aura.lit.e)
5740− [%& [%nvar next.state] state(next +(next.state))]
5741− [%& [%atom aura.lit.e] state]
5742− %ship [%& [%atom %p] state]
5743− %date [%& [%atom %da] state]
5744− %duration [%& [%atom %dr] state]
5745− %knot [%& [%atom %ta] state]
5746− %loobean [%& [%flag ~] state]
5747− %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [next.state tags.state])]
5748− * [%| ["literal needs contextual inference" ~]]
5749− ==
5750− %str
5751− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
5752− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
5753− [%& [%atom %t] state]
5754− %wing
5755− ?~ names.e [%| ["empty wing" ~]]
5756− ?^ t.names.e
5757− ?^ t.t.names.e (infer-field-wing names.e env state)
5758− =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
5759− ?~ iface (infer-field-wing names.e env state)
5760− =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
5761− ?~ member [%| ["module member is not available to partial inference" ~]]
5762− =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
5763− [%& typ.instance state.instance]
5764− =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
5765− ?~ scheme [%| ["name is not available to partial inference" ~]]
5766− =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
5767− [%& typ.instance state.instance]
6916+ %list &
6917+ %tuple &
6918+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
57686919 %group $(e inner.e)
5769− %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [next.state tags.state])]
5770− %trace
5771− =/ traced=iresult $(e val.e)
5772− ?: ?=(%| -.traced) traced
5773− $(e then.e, state state.p.traced)
5774− %tuple (infer-simple-items items.e env state)
5775− %body
5776− ?~ defs.e $(e final.e)
5777− =/ local-names=(list term) (global-value-names defs.e)
5778− ?. (local-names-valid defs.e env state)
5779− [%| ["local definitions shadow a name" ~]]
5780− =/ local-molds=imolds (collect-simple-molds defs.e)
5781− ?. (local-mold-names-valid local-molds state)
5782− [%| ["local molds shadow a name" ~]]
5783− =/ local-state=istate
5784− state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
5785− ?. (local-molds-supported local-molds local-state)
5786− [%| ["local molds need unsupported inference" ~]]
5787− =/ values=(list def) (local-value-defs defs.e)
5788− =/ locals=ilocal-result (infer-local-defs values env local-state)
5789− ?: ?=(%| -.locals) locals
5790− =/ result=iresult $(e final.e, env env.p.locals, state state.p.locals)
6920+ %body ?~(defs.e $(e final.e) |)
6921+ * |
6922+ ==
6923+::
6924+++ infer-list-context
6925+ |= [e=expr expected=itype env=ienv state=istate context=span]
6926+ ^- iresult
6927+ ?: ?=(%group -.e) $(e inner.e)
6928+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6929+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
6930+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
6931+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6932+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
6933+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
6934+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
6935+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6936+ =/ target=itype (itype-walk expected sub.state)
6937+ ?. ?=(%collection -.target) [%| ["list context is not supported by partial inference" ~]]
6938+ ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
6939+ ?~ args.target [%| ["list context is not supported by partial inference" ~]]
6940+ ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
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))
6985+::
6986+++ infer-list-items
6987+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6988+ ^- iresult
6989+ ?~ items [%& expected state]
6990+ =/ target=itype (itype-walk expected sub.state)
6991+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6992+ ?: ?=(%| -.value) value
6993+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6994+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6995+ ?: ?=(%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]
7000+ [%| ["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)]]]]
7001+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
7002+::
7003+:: The supported unit pattern covers exactly an atom zero and a cell
7004+:: headed by zero, with a single binder for its payload. Unresolved
7005+:: subjects and all other pattern matrices stay outside this fragment.
7006+::
7007+++ unit-empty-pattern
7008+ |= p=pattern
7009+ ^- ?
7010+ ?. ?=(%lit -.p) |
7011+ =(%null form.lit.p)
7012+::
7013+++ unit-payload-pattern
7014+ |= p=pattern
7015+ ^- (unit term)
7016+ ?. ?=(%cell -.p) ~
7017+ ?~ items.p ~
7018+ ?~ t.items.p ~
7019+ ?^ t.t.items.p ~
7020+ ?. (unit-empty-pattern i.items.p) ~
7021+ ?. ?=(%bind -.i.t.items.p) ~
7022+ `name.i.t.items.p
7023+::
7024+++ unit-empty-case
7025+ |= t=itype
7026+ ^- ?
7027+ ?. ?=(%const -.t) |
7028+ =(0 val.literal.t)
7029+::
7030+++ unit-payload-case
7031+ |= t=itype
7032+ ^- (unit itype)
7033+ ?. ?=(%cell -.t) ~
7034+ ?. (unit-empty-case hed.t) ~
7035+ =/ payload=itype tal.t
7036+ =? payload ?=(%face -.payload) body.payload
7037+ `payload
7038+::
7039+++ unit-union-payload
7040+ |= t=itype
7041+ ^- (unit itype)
7042+ ?. ?=(%union -.t) ~
7043+ ?~ cases.t ~
7044+ ?~ t.cases.t ~
7045+ ?^ t.t.cases.t ~
7046+ ?: (unit-empty-case i.cases.t) (unit-payload-case i.t.cases.t)
7047+ ?: (unit-empty-case i.t.cases.t) (unit-payload-case i.cases.t)
7048+ ~
7049+::
7050+:: List matching currently covers exactly null and a cell of two binders.
7051+:: The head has the element type and the tail has the whole list type.
7052+:: Other patterns and lists whose element mold is empty remain unsupported.
7053+::
7054+++ list-payload-pattern
7055+ |= p=pattern
7056+ ^- (unit [head=term tail=term])
7057+ ?. ?=(%cell -.p) ~
7058+ ?~ items.p ~
7059+ ?~ t.items.p ~
7060+ ?^ t.t.items.p ~
7061+ ?. ?=(%bind -.i.items.p) ~
7062+ ?. ?=(%bind -.i.t.items.p) ~
7063+ `[name.i.items.p name.i.t.items.p]
7064+::
7065+++ infer-list-branch
7066+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span]) typ=itype]
7067+ ^- iresult
7068+ ?> ?=(%branch -.e)
7069+ ?> ?=(%collection -.typ)
7070+ ?. =(%list name.typ) [%| ["list pattern is not supported by partial inference" ~]]
7071+ ?~ prelude.state [%| ["list pattern needs the standard prelude in partial inference" ~]]
7072+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7073+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
7074+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
7075+ ?~ standard [%| ["list pattern needs the standard prelude in partial inference" ~]]
7076+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
7077+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
7078+ ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
7079+ ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
7080+ ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
7081+ ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
7082+ ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
7083+ =/ x=arm i.arms.e
7084+ =/ y=arm i.t.arms.e
7085+ =/ first-empty=? (unit-empty-pattern pat.x)
7086+ =/ first-name=(unit [head=term tail=term]) (list-payload-pattern pat.x)
7087+ =/ second-name=(unit [head=term tail=term]) (list-payload-pattern pat.y)
7088+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
7089+ [%| ["list branch pattern is not supported by partial inference" ~]]
7090+ =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
7091+ ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
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)))))
7093+ [%| ["pattern binder shadows a name" ~]]
7094+ =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
7095+ =/ left=iresult
7096+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state)
7097+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state context.u.expected)
7098+ ?: ?=(%| -.left) left
7099+ =/ right=iresult
7100+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
7101+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
7102+ ?: ?=(%| -.right) right
7103+ ?^ expected [%& typ.u.expected state.p.right]
7104+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
7105+ ?~ joined [%| ["list branch results need unsupported inference" ~]]
7106+ [%& typ.p.left state.p.right(sub u.joined)]
7107+::
7108+++ infer-unit-branch
7109+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7110+ ^- iresult
7111+ ?> ?=(%branch -.e)
7112+ ?~ arms.e [%| ["unit branch is not supported by partial inference" ~]]
7113+ ?~ t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
7114+ ?^ t.t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
7115+ =/ subject=iresult (infer-fragment subject.e env state)
7116+ ?: ?=(%| -.subject) subject
7117+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7118+ ?: &(?=(%collection -.typ) =(%list name.typ))
7119+ (infer-list-branch e env state.p.subject expected typ)
7120+ =/ x=arm i.arms.e
7121+ =/ y=arm i.t.arms.e
7122+ =/ first-empty=? (unit-empty-pattern pat.x)
7123+ =/ first-name=(unit term) (unit-payload-pattern pat.x)
7124+ =/ second-name=(unit term) (unit-payload-pattern pat.y)
7125+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
7126+ [%| ["unit branch pattern is not supported by partial inference" ~]]
7127+ =/ binder=(unit term) ?:(first-empty second-name first-name)
7128+ ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
7129+ ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
7130+ [%| ["pattern binder shadows a name" ~]]
7131+ =/ payload=(unit itype) (unit-union-payload typ)
7132+ ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
7133+ =/ extended=ienv [[u.binder [u.payload ~]] env]
7134+ =/ left=iresult
7135+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
7136+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state.p.subject context.u.expected)
7137+ ?: ?=(%| -.left) left
7138+ =/ right=iresult
7139+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
7140+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
7141+ ?: ?=(%| -.right) right
7142+ ?^ expected [%& typ.u.expected state.p.right]
7143+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
7144+ ?~ joined [%| ["unit branch results need unsupported inference" ~]]
7145+ [%& typ.p.left state.p.right(sub u.joined)]
7146+::
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+::
7713+++ infer-fragment
7714+ |= [e=expr env=ienv state=istate]
7715+ ^- iresult
7716+ ?- -.e
7717+ %pair $(e (pair-as-cell e))
7718+ %lit
7719+ ?- form.lit.e
7720+ %number ?: =(%ud aura.lit.e)
7721+ [%& [%nvar next.state] state(next +(next.state))]
7722+ [%& [%atom aura.lit.e] state]
7723+ %ship [%& [%atom %p] state]
7724+ %date [%& [%atom %da] state]
7725+ %duration [%& [%atom %dr] state]
7726+ %knot [%& [%atom %ta] state]
7727+ %loobean [%& [%flag ~] state]
7728+ %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
7729+ %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
7730+ ==
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)]
7770+ %wing
7771+ ?~ names.e [%| ["empty wing" ~]]
7772+ ?^ t.names.e
7773+ ?^ t.t.names.e (infer-field-wing names.e env state)
7774+ =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
7775+ ?~ iface (infer-field-wing names.e env state)
7776+ =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
7777+ ?~ member [%| ["module member is not available to partial inference" ~]]
7778+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
7779+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
7780+ [%& typ.instance state.instance]
7781+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
7782+ ?~ scheme
7783+ ?~ prelude.state [%| ["name is not available to partial inference" ~]]
7784+ =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
7785+ ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
7786+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.prelude-entry state)
7787+ [%& typ.inst state.inst]
7788+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
7789+ [%& typ.instance state.instance]
7790+ %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 ~)
7796+ %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
7797+ %trace
7798+ =/ traced=iresult $(e val.e)
7799+ ?: ?=(%| -.traced) traced
7800+ $(e then.e, state state.p.traced)
7801+ %tuple (infer-simple-items items.e env state)
7802+ %body
7803+ ?~ defs.e $(e final.e)
7804+ =/ local-names=(list term) (global-value-names defs.e)
7805+ ?. (local-names-valid defs.e env state)
7806+ [%| ["local definitions shadow a name" ~]]
7807+ =/ local-molds=imolds (collect-simple-molds defs.e)
7808+ ?. (local-mold-names-valid local-molds state)
7809+ [%| ["local molds shadow a name" ~]]
7810+ =/ local-state=istate
7811+ 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"]]]]
7815+ ?. (local-molds-supported local-molds local-state)
7816+ [%| ["local molds need unsupported inference" ~]]
7817+ =/ values=(list def) (local-value-defs defs.e)
7818+ =/ locals=ilocal-result (infer-local-defs values env local-state)
7819+ ?: ?=(%| -.locals) locals
7820+ =/ result=iresult $(e final.e, env env.p.locals, state state.p.locals)
57917821 ?: ?=(%| -.result) result
57927822 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
57937823 %branch
57947824 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
5795− ?~ t.arms.e (infer-cell-branch e env state)
5796− ?^ 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)
57977833 =/ x=arm i.arms.e
57987834 =/ y=arm i.t.arms.e
5799− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
5800− ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
7835+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
7836+ (infer-unit-branch e env state ~)
7837+ ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7838+ ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
58017839 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
5802− [%| ["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)
58037842 ?: =(val.lit.pat.x val.lit.pat.y)
58047843 [%| ["branch does not cover both loobeans" ~]]
58057844 =/ subject=iresult $(e subject.e)
58067845 ?: ?=(%| -.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" ~]]
58077849 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
58087850 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
58097851 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -5816,6 +7858,8 @@
58167858 [%| ["branch widening is not supported by partial inference" ~]]
58177859 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
58187860 ?~ joined
7861+ ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
7862+ [%| ["recursive branch matching is not supported by partial inference" ~]]
58197863 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
58207864 [%| ["branch tag or union context is not supported by partial inference" ~]]
58217865 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
@@ -5828,53 +7872,391 @@
58287872 [%& typ.p.left state.p.right(sub u.joined)]
58297873 %cast
58307874 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
5831− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
5832− =/ value=iresult $(e val.e, state state.u.target)
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" ~]]
7879+ =/ value=iresult
7880+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
58337881 ?: ?=(%| -.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" ~]]
58347885 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
58357886 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
58367887 ?: ?=(%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]
58377892 [%| ["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)]]]]
58387893 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
58397894 [%& merged state.p.value(sub sub.fit, next next.fit)]
58407895 %crash [%& [%var next.state] state(next +(next.state))]
58417896 %gate
58427897 =/ sam=isample-result (infer-sample sample.e env state)
5843− ?: ?=(%| -.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 ~]]
58447902 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
58457903 ?: ?=(%| -.body) body
58467904 [%& [%fn typ.p.sam typ.p.body] state.p.body]
58477905 %gate-wide
58487906 =/ sam=isample-result (infer-sample sample.e env state)
5849− ?: ?=(%| -.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 ~]]
58507911 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
58517912 ?: ?=(%| -.body) body
58527913 [%& [%fn typ.p.sam typ.p.body] state.p.body]
58537914 %call
58547915 ?~ args.e [%| ["call has no argument" ~]]
5855− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
5856− =/ head=iresult $(e head.e)
5857− ?: ?=(%| -.head) head
5858− =/ arg=iresult $(e i.args.e, state state.p.head)
5859− ?: ?=(%| -.arg) arg
5860− =/ st=istate state.p.arg
5861− =/ ht=itype (itype-walk typ.p.head sub.st)
5862− ?: ?=(%fn -.ht)
5863− =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
5864− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
5865− ?: ?=(%bad -.fit)
5866− [%| ["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)]]]]
5867− ?: &((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))
5868− [%| ["call result face propagation is not supported by partial inference" ~]]
5869− [%& product.ht st(sub sub.fit, next next.fit)]
5870− =/ result=itype [%var next.st]
5871− =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
5872− ?~ uni
5873− [%| ["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)]]]]
5874− [%& 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))
58757919 * [%| ["expression is not supported by partial inference" ~]]
58767920 ==
58777921::
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.
7925+::
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+::
58788260:: Tuple and record expressions preserve their explicitly written faces.
58798261::
58808262++ infer-simple-items
@@ -5890,11 +8272,55 @@
58908272 ?: ?=(%| -.tail) tail
58918273 [%& [%cell ht typ.p.tail] state.p.tail]
58928274::
5893−:: A single two-binder cell pattern covers every value of a cell type.
5894−:: 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)
58958321::
58968322++ infer-cell-branch
5897− |= [e=expr env=ienv state=istate]
8323+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
58988324 ^- iresult
58998325 ?> ?=(%branch -.e)
59008326 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -5903,23 +8329,31 @@
59038329 =/ pats=(list pattern) items.pat.arm
59048330 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
59058331 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
5906− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
5907− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
5908− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
5909− =/ one=term name.i.pats
5910− =/ two=term name.i.t.pats
5911− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
5912− [%| ["pattern shadows a name" ~]]
8332+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
8333+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
59138334 =/ subject=iresult (infer-fragment subject.e env state)
59148335 ?: ?=(%| -.subject) subject
59158336 =/ st=istate state.p.subject
8337+ =/ subject-type=itype (itype-normalize typ.p.subject sub.st)
8338+ ?: (itype-has-recursive subject-type)
8339+ [%| ["recursive pattern is not supported by partial inference" ~]]
59168340 ?: (itype-has-face typ.p.subject sub.st)
59178341 [%| ["record patterns are not supported by partial inference" ~]]
5918− =/ head=itype [%var next.st]
5919− =/ tail=itype [%var +(next.st)]
5920− =/ 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)
59218346 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
5922− (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)]
59238357::
59248358++ show-itype
59258359 |= [t=itype sub=isub]
@@ -5938,11 +8372,18 @@
59388372 %atom "@{(trip aura.t)}"
59398373 %any-atom "@"
59408374 %flag "?"
8375+ %noun "*"
59418376 %tag (trip txt.literal.t)
59428377 %const (trip txt.literal.t)
5943− %union "<union>"
5944− %face "[{(trip name.t)}={$(t body.t)}]"
5945− %fn "$-({$(t sample.t)} {$(t product.t)})"
8378+ %union
8379+ ?~ label.t (show-itype-cases cases.t sub)
8380+ ?~ args.t (trip u.label.t)
8381+ "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
8382+ %recursive ?~(label.t "recursive mold" (trip u.label.t))
8383+ %jrec ?~(label.t "recursive mold" (trip u.label.t))
8384+ %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
8385+ %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
8386+ %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
59468387 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
59478388 ==
59488389::
@@ -5950,9 +8391,23 @@
59508391 |= [t=itype sub=isub]
59518392 ^- tape
59528393 =. t (itype-walk t sub)
5953− ?: ?=(%face -.t) "{(trip name.t)}={(show-itype body.t sub)}"
8394+ ?: ?=(%face -.t) "{(trip name.t)}={(show-itype-context body.t sub)}"
8395+ (show-itype-context t sub)
8396+::
8397+++ show-itype-context
8398+ |= [t=itype sub=isub]
8399+ ^- tape
8400+ =. t (itype-walk t sub)
8401+ ?: &(?=(%union -.t) ?=(~ label.t)) "({(show-itype t sub)})"
59548402 (show-itype t sub)
59558403::
8404+++ show-itype-cases
8405+ |= [cases=(list itype) sub=isub]
8406+ ^- tape
8407+ ?~ cases ""
8408+ ?~ t.cases (show-itype-context i.cases sub)
8409+ "{(show-itype-context i.cases sub)} {$(cases t.cases)}"
8410+::
59568411:: Include the type at a conflicting site where it can be printed.
59578412:: A lone unresolved variable or decimal variable keeps the neutral label.
59588413::
@@ -5966,9 +8421,13 @@
59668421 %atom |
59678422 %any-atom |
59688423 %flag |
8424+ %noun |
59698425 %tag |
59708426 %const |
5971− %union (lien cases.typ |=(c=itype (itype-has-nvar c)))
8427+ %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
8428+ %recursive |
8429+ %jrec |
8430+ %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
59728431 %face $(typ body.typ)
59738432 %fn |($(typ sample.typ) $(typ product.typ))
59748433 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -5979,6 +8438,7 @@
59798438 ^- tape
59808439 =/ normalized=itype (itype-normalize typ sub)
59818440 ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
8441+ ?: (itype-has-hidden-recursive normalized) label
59828442 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
59838443 ?: (gth (lent vars) 26) label
59848444 =/ printable=itype (canonical-itype normalized vars)
@@ -5987,13 +8447,64 @@
59878447:: A capital in a written mold is generalized with its enclosing ++.
59888448:: Atom constraints may remain generic; until full rigidity checking
59898449:: is implemented, do not report a type if one became more specific.
8450+:: Distinct written capitals cannot be forced equal; use the same
8451+:: capital where a type must be shared (Decisions 2026-10-30).
8452+::
8453+++ cap-id-in
8454+ |= [n=@ud caps=icaps sub=isub]
8455+ ^- ?
8456+ ?~ caps |
8457+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8458+ =/ ident=(unit @ud)
8459+ ?+ -.resolved ~
8460+ %var `id.resolved
8461+ %avar `id.resolved
8462+ ==
8463+ ?~ ident $(caps t.caps)
8464+ ?: =(n u.ident) &
8465+ $(caps t.caps)
8466+::
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)
59908495::
59918496++ constrained-capitals
59928497 |= [caps=icaps sub=isub]
59938498 ^- ?
59948499 ?~ caps |
59958500 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
5996− ?. |(?=(%var -.resolved) ?=(%avar -.resolved)) &
8501+ =/ ident=(unit @ud)
8502+ ?+ -.resolved ~
8503+ %var `id.resolved
8504+ %avar `id.resolved
8505+ ==
8506+ ?~ ident &
8507+ ?: (cap-id-in u.ident t.caps sub) &
59978508 $(caps t.caps)
59988509::
59998510:: An atom variable may be generalized when an explicit capital, sample
@@ -6020,9 +8531,13 @@
60208531 %atom |
60218532 %any-atom |
60228533 %flag |
8534+ %noun |
60238535 %tag |
60248536 %const |
6025− %union (lien cases.t |=(c=itype (has-atom-var n c)))
8537+ %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
8538+ %recursive |
8539+ %jrec |
8540+ %collection (lien args.t |=(c=itype (has-atom-var n c)))
60268541 %face $(t body.t)
60278542 %fn |($(t sample.t) $(t product.t))
60288543 %cell |($(t hed.t) $(t tal.t))
@@ -6069,9 +8584,9 @@
60698584::
60708585:: Build the supported part of the value environment in dependency order.
60718586:: Each pass adds successful definitions. Forward references become
6072−:: available on a later pass; recursive groups and unsupported syntax do
6073−:: not enter the environment. Generalized definitions are closed, so a
6074−:: 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.
60758590::
60768591++ global-value-names
60778592 |= ds=(list def)
@@ -6089,32 +8604,617 @@
60898604 ?~ t.hits &
60908605 |
60918606::
6092−++ add-supported-defs
6093− |= [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)]
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]
60948856 ^- ienv
6095− ?~ 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]
60968943 =/ d=def i.ds
60978944 ?: ?=(%mold -.d) $(ds t.ds)
60988945 ?. (unique-value-name name.d globals) $(ds t.ds)
60998946 ?^ (ienv-lookup name.d env) $(ds t.ds)
6100− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ |])
8947+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
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)
61018952 ?: ?=(%| -.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)
61028955 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
61038956 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
61048957 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
61058958 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
61068959 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
61078960 ?: (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]
61088966 $(ds t.ds, env [[name.d [typ vars]] env])
61098967::
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+::
61109097++ resolve-supported-defs
6111− |= [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)]
9098+ |= [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)]
61129099 ^- ienv
6113− =/ 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) ~
61149209 |-
6115− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds)
6116− ?: =(next env) env
6117− $(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))
61189218::
61199219+| %union-analysis
61209220::
@@ -6251,11 +9351,142 @@
62519351 [at.first at.second (union-relate a (project-union-mold second molds ~))]
62529352 (weld pairs $(cases t.cases))
62539353::
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)
62549481++ show-partial-mold
62559482 |= [file=path src=@t d=def molds=imolds]
62569483 ^- @t
62579484 ?> ?=(%mold -.d)
62589485 =/ 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])
62599490 =? sh ?=(%generic -.sh) body.sh
62609491 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
62619492 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -6282,6 +9513,21 @@
62829513 (show-error src [file line.beg.at.site col.beg.at.site note.site])
62839514 (of-wain:format [summary excerpts])
62849515::
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+::
62859531:: +golden-types: a partial report; it does not claim the module checks
62869532::
62879533++ golden-types
@@ -6311,6 +9557,180 @@
63119557+$ jfile-result (each [iface=ifile cache=jcache] @t)
63129558+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
63139559::
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+ ==
63149734++ import-binding-names
63159735 |= imports=(list import)
63169736 ^- (list term)
@@ -6323,6 +9743,60 @@
63239743 ==
63249744 [n $(imports t.imports)]
63259745::
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+::
63269800++ module-scope-valid
63279801 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
63289802 ^- ?
@@ -6330,6 +9804,7 @@
63309804 =/ vals=(list term) (global-value-names defs.mod)
63319805 =/ molds=imolds (collect-simple-molds defs.mod)
63329806 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9807+ ?: (module-has-reserved-proj mod) |
63339808 ?. %+ levy imported
63349809 |= n=term
63359810 &((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))))
@@ -6337,6 +9812,22 @@
63379812 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
63389813 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
63399814::
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+::
63409831++ module-mold-types
63419832 |= [molds=imolds state=istate]
63429833 ^- (each imold-types @t)
@@ -6345,10 +9836,205 @@
63459836 =/ t=(unit [template=ischeme state=istate])
63469837 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
63479838 ?~ t [%| 'module mold needs unsupported inference']
9839+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
63489840 =/ rest=(each imold-types @t) $(molds t.molds)
63499841 ?: ?=(%| -.rest) rest
63509842 [%& [[name.m template.u.t] p.rest]]
63519843::
9844+:: Prepare a provisional interface from the trusted vendored source.
9845+:: Every declared name remains reserved, but only molds and values this
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.
9849+::
9850+:: Recognize only the complete standard prelude list shape. Its recursive
9851+:: tail uses the same parameter and the unqualified list name. The reader
9852+:: verifies Hoon's list provenance before producing the same collection type.
9853+:: The prelude source and reader output are trusted caller inputs.
9854+::
9855+++ standard-prelude-list
9856+ |= sh=shape
9857+ ^- ?
9858+ ?. ?=(%generic -.sh) |
9859+ ?~ vars.sh |
9860+ ?^ t.vars.sh |
9861+ =/ var=@t i.vars.sh
9862+ ?. ?=(%union -.body.sh) |
9863+ =/ cs=(list shape) cases.body.sh
9864+ ?~ cs |
9865+ ?~ t.cs |
9866+ ?^ t.t.cs |
9867+ ?. ?=(%const -.i.cs) |
9868+ ?. =(%null form.lit.i.cs) |
9869+ ?. ?=(%cell -.i.t.cs) |
9870+ =/ fs=(list field) fields.i.t.cs
9871+ ?~ fs |
9872+ ?~ t.fs |
9873+ ?^ t.t.fs |
9874+ ?. ?=(%face -.i.fs) |
9875+ ?. =(%i name.i.fs) |
9876+ ?. ?=(%tvar -.shape.i.fs) |
9877+ ?. =(var name.shape.i.fs) |
9878+ ?. ?=(%face -.i.t.fs) |
9879+ ?. =(%t name.i.t.fs) |
9880+ =/ tail=shape shape.i.t.fs
9881+ ?. ?=(%apply -.tail) |
9882+ ?. =(~[%list] ref.tail) |
9883+ ?~ args.tail |
9884+ ?^ t.args.tail |
9885+ ?. ?=(%tvar -.i.args.tail) |
9886+ =(var name.i.args.tail)
9887+::
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+::
9896+++ partial-prelude-molds
9897+ |= [molds=imolds state=istate]
9898+ ^- imold-types
9899+ ?~ molds ~
9900+ =/ m=[name=term body=shape] i.molds
9901+ ?: &(=(at.state /lib/jibb/prelude/jibb) =(%list name.m))
9902+ ?. (standard-prelude-list body.m) $(molds t.molds)
9903+ [[%list [[%collection %list ~[[%var 0]]] ~[0]]] $(molds t.molds)]
9904+ =/ out=(unit [template=ischeme state=istate])
9905+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
9906+ ?~ out $(molds t.molds)
9907+ =. 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)
9909+ [[name.m template.u.out] $(molds t.molds)]
9910+::
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
9921+ |= src=@t
9922+ ^- (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)
9953+ ?: =(0 src) ~
9954+ =/ at=path /lib/jibb/prelude/jibb
9955+ =/ parsed (parse at src)
9956+ ?: ?=(%| -.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 ~
9968+ ?~ defs.p.parsed ~
9969+ ?. (module-scope-valid p.parsed ~ ~) ~
9970+ =/ ds=(list def) defs.p.parsed
9971+ =/ molds=imolds (collect-simple-molds ds)
9972+ =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
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 ~)
10013+::
10014++$ iprelude [iface=ifile values=(list term) molds=(list term)]
10015+::
10016+++ prepare-prelude
10017+ |= src=@t
10018+ ^- (unit iprelude)
10019+ =/ iface=(unit ifile) (partial-prelude-interface src)
10020+ ?~ iface ~
10021+ =/ parsed (parse /lib/jibb/prelude/jibb src)
10022+ ?: ?=(%| -.parsed) ~
10023+ =/ vals=(list term) (global-value-names defs.p.parsed)
10024+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
10025+ `[u.iface vals ms]
10026+::
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+::
635210038++ module-values-complete
635310039 |= [ds=(list def) env=ienv]
635410040 ^- ?
@@ -6370,11 +10056,15 @@
637010056 $(cache t.cache)
637110057::
637210058++ resolve-jibb-imports
6373− |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache]
10059+ |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache prelude=(unit ifile)]
637410060 ^- jimports-result
637510061 ?~ imports [%& [~ cache]]
637610062 ?. ?=(%jibb -.i.imports) $(imports t.imports)
637710063 =/ 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']
637810068 ?: (lien active |=(p=path =(p at)))
637910069 [%| (crip "import cycle at {(spud at)}")]
638010070 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -6383,37 +10073,313 @@
638310073 =/ cached=(unit ifile) (find-jibb-cache at cache)
638410074 =/ iface=jfile-result
638510075 ?^ cached [%& [u.cached cache]]
6386− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache)
10076+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
638710077 ?: ?=(%| -.iface) [%| p.iface]
638810078 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
638910079 ?: ?=(%| -.rest) rest
639010080 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
639110081::
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+::
639210346++ infer-jibb-file
6393− |= [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]
10347+ |= [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)]
639410348 ^- jfile-result
6395− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
639610349 =/ parsed (parse at src)
639710350 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
639810351 =/ mod=module p.parsed
6399− ?. (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)}")]
640010363 =/ vals=(list term) (global-value-names defs.mod)
640110364 ?: (lien vals |=(n=term =(n %main)))
640210365 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
6403− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache)
10366+ =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
640410367 ?: ?=(%| -.js) [%| p.js]
640510368 =/ molds=imolds (collect-simple-molds defs.mod)
640610369 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
640710370 =/ surs=(list term) (collect-sur-imports imports.mod)
640810371 =/ marks=(list term) (collect-mark-imports imports.mod)
640910372 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
6410− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ |]
10373+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10374+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
641110375 =/ mts=(each imold-types @t) (module-mold-types molds state)
641210376 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
6413− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved)
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
641410379 ?. (module-values-complete defs.mod env)
641510380 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
6416− [%& [[env p.mts] [[at [env p.mts]] cache.p.js]]]
10381+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src]
10382+ [%& [iface [[at iface] cache.p.js]]]
641710383::
641810384:: +golden-types-with-modules fails closed for imports without prelude
641910385:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -6424,54 +10390,103 @@
642410390 ^- @t
642510391 =/ parsed (parse file src)
642610392 ?: ?=(%| -.parsed) (show-error src p.parsed)
10393+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10394+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
642710395 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
642810396 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
642910397 (golden-types-with-marks file src externals mark-externals)
643010398::
6431−:: The caller supplies the actual prelude source. Its current names are
6432−:: reserved, but its incomplete inventory and types are not checked here.
10399+:: The caller supplies the actual prelude source. Its declared names are
10400+:: reserved, and supported inferred types are made available. The inventory
10401+:: and the checker are incomplete, so this never claims a checked module.
10402+:: Hosts may prepare the same trusted source once and reuse its interface.
643310403::
643410404++ golden-types-with-prelude
643510405 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
643610406 ^- @t
643710407 =/ parsed (parse file src)
643810408 ?: ?=(%| -.parsed) (show-error src p.parsed)
10409+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10410+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
643910411 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
644010412 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
644110413 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
6442− =/ prelude-values=(list term) (global-value-names defs.p.prelude)
6443− =/ prelude-molds=(list term)
6444− (turn (collect-simple-molds defs.p.prelude) |=(m=[name=term body=shape] name.m))
10414+ =/ prepared=(unit iprelude) (prepare-prelude prelude-source)
10415+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
10416+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
10417+::
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+::
10424+++ golden-types-with-prepared-prelude
10425+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
10426+ ^- @t
10427+ =/ parsed (parse file src)
10428+ ?: ?=(%| -.parsed) (show-error src p.parsed)
10429+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10430+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
10431+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
10432+ =/ prelude-values=(list term) values.u.prepared
10433+ =/ prelude-molds=(list term) molds.u.prepared
10434+ =/ iface=(unit ifile) `iface.u.prepared
644510435 ?. (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'
644610438 'partial inference; module not checked\0amodule has conflicting names'
644710439 =/ js=jimports-result
6448− (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~)
10440+ (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
644910441 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
645010442 =/ scope-values=(list term)
645110443 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
6452− (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds)
10444+ (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
645310445::
645410446:: +golden-types-with-marks: supply declared mark types separately from /sur
645510447:: entries, as [mark result] with the result from +read-mark:jibb-import.
645610448:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
645710449::
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+::
645810467++ golden-types-with-marks
645910468 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
646010469 ^- @t
6461− (golden-types-in-context file src externals mark-externals ~ ~ ~)
10470+ (golden-types-in-context file src externals mark-externals ~ ~ ~ ~)
646210471::
646310472++ golden-types-in-context
6464− |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term)]
10473+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
646510474 ^- @t
646610475 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
646710476 =/ parsed (parse file src)
646810477 ?: ?=(%| -.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'
646910482 =/ ds=(list def) defs.p.parsed
647010483 =/ molds=imolds (collect-simple-molds ds)
647110484 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
647210485 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
647310486 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
6474− =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds)
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
647510490 =/ lines=(list @t) ~
647610491 |-
647710492 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -6480,21 +10495,53 @@
648010495 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
648110496 ?. (unique-value-name name.d globals)
648210497 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
6483− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ |])
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])
10508+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
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)
648410515 ?: ?=(%| -.result)
648510516 $(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])
648610527 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
648710528 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
648810529 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10530+ ?: (pending-null tags.state.p.result sub.state.p.result)
10531+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: `~` needs context in partial inference") lines])
648910532 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
649010533 $(ds t.ds, lines [(crip "++ {(trip name.d)}: tag needs context in partial inference") lines])
6491− ?: (itype-has-union typ)
6492− $(ds t.ds, lines [(crip "++ {(trip name.d)}: union type printing is not supported by partial inference") lines])
10534+ ?: (itype-has-hidden-recursive typ)
10535+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
10536+ ?: (itype-has-hidden-generic typ)
10537+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
649310538 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
649410539 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
649510540 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
649610541 ?: (gth (lent vars) 26)
649710542 $(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])
649810545 =/ printable=itype (canonical-itype typ vars)
649910546 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
650010547 $(ds t.ds, lines [line lines])