@@ -874,7 +874,7 @@
874 %'~[' %'|=(' %'$-(' :: openers
874 %'~[' %'|=(' %'$-(' :: openers
875 %'%/' %'/' :: paths
875 %'%/' %'/' :: paths
876 %'+' %'`' %'=' :: pair, unit, face
876 %'+' %'`' %'=' :: pair, unit, face
877− %'*' %'?' :: noun, loobean mold
877+ %'*' %'?' %'_' :: noun, loobean, type hole
878 %'++' %'+$' %'|=' %'|$' :: runes
878 %'++' %'+$' %'|=' %'|$' :: runes
879 %'^-' %'~&' %'?-' %'!!' :: runes
879 %'^-' %'~&' %'?-' %'!!' :: runes
880 %'/-' %'/%' %'/=' :: imports
880 %'/-' %'/%' %'/=' :: imports
@@ -1016,6 +1016,7 @@
1016 [%const at=span =lit] :: ~ %add %.y
1016 [%const at=span =lit] :: ~ %add %.y
1017 [%ref at=span names=(list term)] :: state item.todo
1017 [%ref at=span names=(list term)] :: state item.todo
1018 [%tvar at=span name=@t] :: M
1018 [%tvar at=span name=@t] :: M
1019+ [%hole at=span ~] :: _
1019 [%path at=span segs=(list pseg)] :: / /todos /todo/[id=@ud]
1020 [%path at=span segs=(list pseg)] :: / /todos /todo/[id=@ud]
1020 [%apply at=span ref=(list term) args=(list shape)] :: (list @t)
1021 [%apply at=span ref=(list term) args=(list shape)] :: (list @t)
1021 [%cell at=span fields=(list field)] :: [text=@t done=?]
1022 [%cell at=span fields=(list field)] :: [text=@t done=?]
@@ -1024,9 +1025,9 @@
1024 [%generic at=span vars=(list @t) body=shape] :: +$ name |$ [M] …
1025 [%generic at=span vars=(list @t) body=shape] :: +$ name |$ [M] …
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=_]
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])
@@ -1295,6 +1296,7 @@
1295 (emit 1 %'=')
1296 (emit 1 %'=')
1296 ?: =('`' a) (emit 1 %'`')
1297 ?: =('`' a) (emit 1 %'`')
1297 ?: =('*' a) (emit 1 %'*')
1298 ?: =('*' a) (emit 1 %'*')
1299+ ?: =('_' a) (emit 1 %'_')
1298 ?: =('~' a)
1300 ?: =('~' a)
1299 ?: =('[' b) (emit 2 %'~[')
1301 ?: =('[' b) (emit 2 %'~[')
1300 ?: =('&' b) (emit 2 %'~&')
1302 ?: =('&' b) (emit 2 %'~&')
@@ -1670,14 +1672,14 @@
1670:: What may begin each place the parser reads (section 3, Errors):
1672:: What may begin each place the parser reads (section 3, Errors):
1671:: an expression a-z 0-9 " ( [ ~ % / ` | ^ ? !
1673:: an expression a-z 0-9 " ( [ ~ % / ` | ^ ? !
1672:: an operand a-z 0-9 " ( [ ~ % / ` | !
1674:: an operand a-z 0-9 " ( [ ~ % / ` | !
1673−:: a mold a-z A-Z @ * ! ? ~ % / ( [ $
1675+:: a mold a-z A-Z @ * ! ? ~ % / ( [ $ _
1674:: a pattern a-z 0-9 " ~ % * [
1676:: a pattern a-z 0-9 " ~ % * [
1675:: and what may go tight after an operand: . ( + = after a name, a
1677:: and what may go tight after an operand: . ( + = after a name, a
1676:: closer ) ] }, or the : of a comment
1678:: closer ) ] }, or the : of a comment
1678++ expr-mask 0x57ff.ffff.4800.0000.83ff.8126.0000.0000
1680++ expr-mask 0x57ff.ffff.4800.0000.83ff.8126.0000.0000
1679++ operand-mask 0x57ff.ffff.0800.0000.03ff.8126.0000.0000
1681++ 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
1681++ bar-mask 0x1000.0000.0000.0000.0000.0000.0000.0000
1683++ bar-mask 0x1000.0000.0000.0000.0000.0000.0000.0000
1682++ pattern-mask 0x47ff.fffe.0800.0000.03ff.0424.0000.0000
1684++ pattern-mask 0x47ff.fffe.0800.0000.03ff.0424.0000.0000
1683++ after-mask 0x2000.0000.2000.0000.2400.4b00.0000.0000
1685++ after-mask 0x2000.0000.2000.0000.2400.4b00.0000.0000
@@ -2107,6 +2109,7 @@
2108 %knot (weld "/" (trip p.s))
2110 %knot (weld "/" (trip p.s))
2109 %typed "/[{(trip name.s)}=@{(trip aura.s)}]"
2111 %typed "/[{(trip name.s)}=@{(trip aura.s)}]"
2112+ %inferred "/[{(trip name.s)}=_]"
2112++ show-tvars
2115++ show-tvars
@@ -2318,6 +2321,7 @@
2318 %const (nod "const" at.s (show-lit lit.s) ~)
2321 %const (nod "const" at.s (show-lit lit.s) ~)
2319 %ref (nod "ref" at.s (show-names names.s) ~)
2322 %ref (nod "ref" at.s (show-names names.s) ~)
2320 %tvar (nod "tvar" at.s (trip name.s) ~)
2323 %tvar (nod "tvar" at.s (trip name.s) ~)
2324+ %hole (nod "hole" at.s "" ~)
2321 %path (nod "path" at.s (show-psegs segs.s) ~)
2325 %path (nod "path" at.s (show-psegs segs.s) ~)
2322 %apply (nod "apply" at.s (show-names ref.s) (turn args.s sexp-shape))
2326 %apply (nod "apply" at.s (show-names ref.s) (turn args.s sexp-shape))
2323 %cell (nod "cell" at.s "" (turn fields.s sexp-field))
2327 %cell (nod "cell" at.s "" (turn fields.s sexp-field))
@@ -3842,6 +3846,7 @@
3842 %'*' [%& [%noun at.t ~] t.ts]
3846 %'*' [%& [%noun at.t ~] t.ts]
3843 %'!!' [%& [%void at.t ~] t.ts]
3847 %'!!' [%& [%void at.t ~] t.ts]
3844 %'?' [%& [%flag at.t ~] t.ts]
3848 %'?' [%& [%flag at.t ~] t.ts]
3849+ %'_' [%& [%hole at.t ~] t.ts]
3845 [%name *] [%& [%ref at.t ~[p.lex.t]] t.ts]
3850 [%name *] [%& [%ref at.t ~[p.lex.t]] t.ts]
3846 [%wing *] [%& [%ref at.t p.lex.t] t.ts]
3851 [%wing *] [%& [%ref at.t p.lex.t] t.ts]
3847 [%tvar *] [%& [%tvar at.t p.lex.t] t.ts]
3852 [%tvar *] [%& [%tvar at.t p.lex.t] t.ts]
@@ -4058,7 +4063,7 @@
4058 ?: &(?=(^ nex) tight.i.nex) (bad nex "a path segment")
4063 ?: &(?=(^ nex) tight.i.nex) (bad nex "a path segment")
4059 (bad-space i.after nex "a path segment")
4064 (bad-space i.after nex "a path segment")
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
4062 :: spaces, and where it ends
4067 :: spaces, and where it ends
4064 ++ read-pseg
4069 ++ read-pseg
@@ -4075,13 +4080,16 @@
4075 ?: |(?=(~ r2) !tight.i.r2) (bad-space i.r1 r2 "`=`")
4080 ?: |(?=(~ r2) !tight.i.r2) (bad-space i.r1 r2 "`=`")
4076 ?. ?=([[* * %'='] *] r2) (bad-in r2 "`=`" tis-mask)
4081 ?. ?=([[* * %'='] *] r2) (bad-in r2 "`=`" tis-mask)
4077 =/ r3=(list token) t.r2
4082 =/ r3=(list token) t.r2
4078− ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura")
4083+ ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura or type hole")
4079− ?. ?=([[* * [%aura *]] *] r3) (bad-in r3 "an aura" pat-mask)
4084+ ?. ?=([[* * ?([%aura *] %'_')] *] r3) (bad-in r3 "an aura or type hole" (con pat-mask (bex 95)))
4080 =/ r4=(list token) t.r3
4085 =/ r4=(list token) t.r3
4081 ?: |(?=(~ r4) !tight.i.r4) (bad-space i.r3 r4 "`]`")
4086 ?: |(?=(~ r4) !tight.i.r4) (bad-space i.r3 r4 "`]`")
4082 ?. ?=([[* * %']'] *] r4) (bad-in r4 "`]`" ser-mask)
4087 ?. ?=([[* * %']'] *] r4) (bad-in r4 "`]`" ser-mask)
4083 =/ at=span [beg.at.op end.at.i.r4]
4088 =/ at=span [beg.at.op end.at.i.r4]
4090+ ?: ?=(%'_' lex.i.r3) [%inferred at p.lex.i.r1 at.i.r3]
4084− [%& [[%typed at p.lex.i.r1 p.lex.i.r3] end.at.i.r4] t.r4]
4091+ [%typed at p.lex.i.r1 p.lex.i.r3]
4092+ [%& [seg end.at.i.r4] t.r4]
4087+| %span-check
4095+| %span-check
@@ -4465,6 +4473,7 @@
4465 %const [%const at.s ~[%lit] %one ~]
4473 %const [%const at.s ~[%lit] %one ~]
4466 %ref [%ref at.s ~[%name %wing] %one ~]
4474 %ref [%ref at.s ~[%name %wing] %one ~]
4467 %tvar [%tvar at.s ~[%tvar] %one ~]
4475 %tvar [%tvar at.s ~[%tvar] %one ~]
4476+ %hole [%hole at.s ~[%'_'] %one ~]
4468 %apply [%apply at.s ~[%'('] %shut (turn args.s outline-shape)]
4477 %apply [%apply at.s ~[%'('] %shut (turn args.s outline-shape)]
4469 %cell [%cell at.s ~[%'['] %shut (turn fields.s outline-sample)]
4478 %cell [%cell at.s ~[%'['] %shut (turn fields.s outline-sample)]
@@ -4473,8 +4482,11 @@
4473 %+ murn segs.s
4482 %+ murn segs.s
4474 |= g=pseg
4483 |= g=pseg
4475 ^- (unit outline)
4484 ^- (unit outline)
4476− ?. ?=(%typed -.g) ~
4487+ %typed `[%typed at.g ~[%'['] %shut ~]
4477− `[%typed at.g ~[%'['] %shut ~]
4488+ %inferred `[%typed at.g ~[%'['] %shut ~[[%hole hole-at.g ~[%'_'] %one ~]]]
4478 [%path at.s ~[%'/'] %run ks]
4490 [%path at.s ~[%'/'] %run ks]
@@ -4534,6 +4546,8 @@
4534 [%path [1 9] [1 9] [1 21]]
4546 [%path [1 9] [1 9] [1 21]]
4535 [%face [1 7] [1 7] [1 21]]
4547 [%face [1 7] [1 7] [1 21]]
4549+ :: an inferred path aura's hole spanning its = as well
4550+ ['+$ x /a/[id=_]' ~[[%hole [1 13] [1 12] [1 14]]]]
4537 :: an import's path cut short
4551 :: an import's path cut short
4538 ['/= c /ui/c' ~[[%jibb [1 1] [1 1] [1 11]]]]
4552 ['/= c /ui/c' ~[[%jibb [1 1] [1 1] [1 11]]]]
4539 :: brackets that close with the deeper lines, cut at their line's
4553 :: brackets that close with the deeper lines, cut at their line's
@@ -4595,8 +4609,24 @@
4595:: their defaulting and inferred generalization are implemented.
4609:: their defaulting and inferred generalization are implemented.
4596:: Bare @ is a separate unrestricted atom type. A directional fit check
4610:: Bare @ is a separate unrestricted atom type. A directional fit check
4597:: permits concrete atoms to widen to it, never the reverse. A fit that
4611:: permits concrete atoms to widen to it, never the reverse. A fit that
4598−:: needs a not-yet-implemented constraint remains unsupported. Only
4612+:: needs a not-yet-implemented constraint remains unsupported. Named unions
4599−:: unfaced cells are represented here.
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.
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.
4602 $~ [%var 0]
4632 $~ [%var 0]
@@ -4606,15 +4636,20 @@
4606 [%atom aura=@ta]
4636 [%atom aura=@ta]
4607 [%any-atom ~]
4637 [%any-atom ~]
4608 [%flag ~]
4638 [%flag ~]
4609 [%tag id=@ud literal=lit constructor=?]
4640 [%tag id=@ud literal=lit constructor=?]
4610 [%const literal=lit]
4641 [%const literal=lit]
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]
4611− [%union cases=(list itype)]
4645+ [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4612 [%face name=term body=itype]
4646 [%face name=term body=itype]
4613 [%fn sample=itype product=itype]
4647 [%fn sample=itype product=itype]
4614 [%cell hed=itype tal=itype]
4648 [%cell hed=itype tal=itype]
4616+$ ibinding [id=@ud val=itype]
4650+$ ibinding [id=@ud val=itype]
4617+$ isub (list ibinding)
4651+$ isub (list ibinding)
4652++$ ipending [id=@ud literal=lit]
4619++ itype-lookup
4654++ itype-lookup
4620 |= [n=@ud sub=isub]
4655 |= [n=@ud sub=isub]
@@ -4656,9 +4691,13 @@
4657 %any-atom |
4692 %any-atom |
4659 %tag =(n id.t)
4695 %tag =(n id.t)
4660 %const |
4696 %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))))
4700+ %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4662 %face $(t body.t)
4701 %face $(t body.t)
4663 %fn |($(t sample.t) $(t product.t))
4702 %fn |($(t sample.t) $(t product.t))
4664 %cell |($(t hed.t) $(t tal.t))
4703 %cell |($(t hed.t) $(t tal.t))
@@ -4676,6 +4715,18 @@
4676 =. a (itype-walk a sub)
4715 =. a (itype-walk a sub)
4677 =. b (itype-walk b sub)
4716 =. b (itype-walk b sub)
4678 ?: =(a b) `sub
4717 ?: =(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 ~)
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)
4679 ?: ?=(%var -.a)
4730 ?: ?=(%var -.a)
4680 ?: (itype-occurs id.a b sub) ~
4731 ?: (itype-occurs id.a b sub) ~
4681 `[[id.a b] sub]
4732 `[[id.a b] sub]
@@ -4714,6 +4765,15 @@
4714 $(a tal.a, b tal.b, sub u.first)
4765 $(a tal.a, b tal.b, sub u.first)
4769+ |= [as=(list itype) bs=(list itype) sub=isub]
4771+ ?~ as ?~(bs `sub ~)
4773+ =/ next=(unit isub) (itype-unify i.as i.bs sub)
4775+ $(as t.as, bs t.bs, sub u.next)
4717:: +itype-fit: one-way widening from an actual type to an expected type
4777:: +itype-fit: one-way widening from an actual type to an expected type
4719:: An unknown variable used where @ is expected gains a fresh atom
4779:: An unknown variable used where @ is expected gains a fresh atom
@@ -4731,9 +4791,13 @@
4732 %any-atom &
4792 %any-atom &
4735 %const |
4796 %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))))
4800+ %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4737 %face $(t body.t)
4801 %face $(t body.t)
4738 %fn |($(t sample.t) $(t product.t))
4802 %fn |($(t sample.t) $(t product.t))
4739 %cell |($(t hed.t) $(t tal.t))
4803 %cell |($(t hed.t) $(t tal.t))
@@ -4757,6 +4821,14 @@
4757:: Related auras in a structural unification need a common-type rule;
4821:: Related auras in a structural unification need a common-type rule;
4758:: until that rule is implemented, report an unknown rather than error.
4822:: until that rule is implemented, report an unknown rather than error.
4824+++ itype-family-related-collection-args
4825+ |= [as=(list itype) bs=(list itype) sub=isub]
4829+ ?: (itype-family-related i.as i.bs sub) &
4830+ $(as t.as, bs t.bs)
4760++ itype-family-related
4832++ itype-family-related
4761 |= [a=itype b=itype sub=isub]
4833 |= [a=itype b=itype sub=isub]
@@ -4765,6 +4837,9 @@
4765 ?: &(?=(%atom -.a) ?=(%atom -.b))
4837 ?: &(?=(%atom -.a) ?=(%atom -.b))
4766 ?. !=(aura.a aura.b) |
4838 ?. !=(aura.a aura.b) |
4767 |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4839 |((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)
4768 ?: &(?=(%face -.a) ?=(%face -.b))
4843 ?: &(?=(%face -.a) ?=(%face -.b))
4769 ?. =(name.a name.b) |
4844 ?. =(name.a name.b) |
4770 $(a body.a, b body.b)
4845 $(a body.a, b body.b)
@@ -4788,9 +4863,13 @@
4789 %any-atom &
4864 %any-atom &
4792 %const &
4868 %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))))
4872+ %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4794 %face $(typ body.typ)
4873 %face $(typ body.typ)
4795 %fn |($(typ sample.typ) $(typ product.typ))
4874 %fn |($(typ sample.typ) $(typ product.typ))
4796 %cell |($(typ hed.typ) $(typ tal.typ))
4875 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -4818,17 +4897,29 @@
4819 =. t (itype-walk t sub)
4898 =. t (itype-walk t sub)
4900+ %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4822 %cell |($(t hed.t) $(t tal.t))
4902 %cell |($(t hed.t) $(t tal.t))
4823 %fn |($(t sample.t) $(t product.t))
4903 %fn |($(t sample.t) $(t product.t))
4907+++ itype-face-asym-collection-args
4908+ |= [as=(list itype) bs=(list itype) sub=isub]
4912+ ?: (itype-face-asym i.as i.bs sub) &
4913+ $(as t.as, bs t.bs)
4827++ itype-face-asym
4915++ itype-face-asym
4828 |= [a=itype b=itype sub=isub]
4916 |= [a=itype b=itype sub=isub]
4830 =. a (itype-walk a sub)
4918 =. a (itype-walk a sub)
4831 =. b (itype-walk b sub)
4919 =. 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)
4832 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4923 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4833 ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4924 ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4834 ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
4925 ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
@@ -4862,16 +4953,27 @@
4864 %union &
4955 %union &
4865 %face $(t body.t)
4960 %face $(t body.t)
4866 %fn |($(t sample.t) $(t product.t))
4961 %fn |($(t sample.t) $(t product.t))
4870++ pending-tags
4965++ pending-tags
4871− |= [tags=(list @ud) sub=isub]
4966+ |= [tags=(list ipending) sub=isub]
4969+ ?~ (itype-lookup id.i.tags sub) &
4973+ |= [tags=(list ipending) sub=isub]
4873 ?~ tags |
4975 ?~ tags |
4874− ?~ (itype-lookup i.tags sub) &
4976+ ?: &(?=(%null form.literal.i.tags) ?=(~ (itype-lookup id.i.tags sub))) &
4875 $(tags t.tags)
4977 $(tags t.tags)
4877:: Tags remain constrained until a mold selects a case or permitted atom
4979:: Tags remain constrained until a mold selects a case or permitted atom
@@ -4882,10 +4984,11 @@
4987+ %collection (lien args.t |=(c=itype (itype-has-tag c)))
4885 %face $(t body.t)
4988 %face $(t body.t)
4886 %fn |($(t sample.t) $(t product.t))
4989 %fn |($(t sample.t) $(t product.t))
4887 %cell |($(t hed.t) $(t tal.t))
4990 %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))))
@@ -4894,12 +4997,59 @@
4896 %union &
4999 %union &
5000+ %collection (lien args.t |=(c=itype (itype-has-union c)))
4897 %face $(t body.t)
5001 %face $(t body.t)
4898 %fn |($(t sample.t) $(t product.t))
5002 %fn |($(t sample.t) $(t product.t))
4899 %cell |($(t hed.t) $(t tal.t))
5003 %cell |($(t hed.t) $(t tal.t))
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.
5011+++ itype-has-hidden-generic
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)))
5020+ %fn |($(t sample.t) $(t product.t))
5021+ %cell |($(t hed.t) $(t tal.t))
5025+++ itype-has-recursive
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)))
5034+ %cell |($(t hed.t) $(t tal.t))
5035+ %fn |($(t sample.t) $(t product.t))
5039+++ itype-has-hidden-recursive
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)))
5048+ %cell |($(t hed.t) $(t tal.t))
5049+ %fn |($(t sample.t) $(t product.t))
4903++ itype-fit-cases
5053++ itype-fit-cases
4904 |= [actual=itype cases=(list itype) sub=isub next=@ud]
5054 |= [actual=itype cases=(list itype) sub=isub next=@ud]
@@ -4933,6 +5083,7 @@
4933 ?. ?=(%cell -.c) $(cases t.cases)
5083 ?. ?=(%cell -.c) $(cases t.cases)
4934 =/ head=itype (itype-walk hed.c sub)
5084 =/ head=itype (itype-walk hed.c sub)
4935 ?. ?=(%const -.head) $(cases t.cases)
5085 ?. ?=(%const -.head) $(cases t.cases)
5086+ ?. =(%term form.literal.head) $(cases t.cases)
4936 ?. =(val.literal.head val.tag) $(cases t.cases)
5087 ?. =(val.literal.head val.tag) $(cases t.cases)
4937 ?^ found [%unknown ~]
5088 ?^ found [%unknown ~]
4938 =/ trial=ifit (itype-fit sample tal.c sub next)
5089 =/ trial=ifit (itype-fit sample tal.c sub next)
@@ -4941,12 +5092,63 @@
4941++ itype-fit
5092++ itype-fit
4942 |= [actual=itype expected=itype sub=isub next=@ud]
5093 |= [actual=itype expected=itype sub=isub next=@ud]
5095+ (itype-fit-inner actual expected sub next | |)
5097+ |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5099+ ?: &(!skip-width ?=(%cell -.actual) ?=(%cell -.expected) |((width-spine-exhausted actual 1.024) (width-spine-exhausted expected 1.024)))
5101+ =/ known=(unit [source=iwfields target=iwfields])
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))
4944 =/ uncertain=?
5107 =/ uncertain=?
4945 |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5108 |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5110+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
4946 =. actual (itype-walk actual sub)
5111 =. actual (itype-walk actual sub)
4947 =. expected (itype-walk expected sub)
5112 =. expected (itype-walk expected sub)
4948 ?: =(actual expected) [%ok sub next]
5113 ?: =(actual expected) [%ok sub next]
5114+ :: Any value can be used where a noun is expected. An unresolved
5115+ :: bare tag is fixed as a constant; a constructor still needs a gate.
5116+ ?: ?=(%noun -.expected)
5117+ ?: ?=(%tag -.actual)
5118+ ?: constructor.actual [%unknown ~]
5119+ [%ok [[id.actual expected] sub] next]
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 ~]
4949− ?: &(?=(%union -.actual) ?=(%union -.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]
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)
4950 ?: ?=(%union -.actual) [%unknown ~]
5152 ?: ?=(%union -.actual) [%unknown ~]
4951 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
5153 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
4952 ?: &(?=(%union -.expected) !?=(%var -.actual))
5154 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -4965,6 +5167,10 @@
4965 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
5167 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
4966 ?. ?=(%ok -.trial) trial
5168 ?. ?=(%ok -.trial) trial
4967 [%ok [[id.actual expected] sub.trial] next.trial]
5169 [%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))
4968 ?: ?=(%const -.expected)
5174 ?: ?=(%const -.expected)
4969 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
5175 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
4970 ?: ?=(%atom -.expected)
5176 ?: ?=(%atom -.expected)
@@ -4982,6 +5188,8 @@
4982 [%ok u.u next]
5188 [%ok u.u next]
4983 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5189 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
4984 ?: ?=(%face -.expected) $(expected body.expected)
5190 ?: ?=(%face -.expected) $(expected body.expected)
5191+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
4985 ?: ?=(%const -.expected)
5193 ?: ?=(%const -.expected)
4986 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
5194 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
4987 ?: ?=(%atom -.expected)
5195 ?: ?=(%atom -.expected)
@@ -5011,27 +5219,40 @@
5011 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
5219 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
5012 [%bad ~]
5220 [%bad ~]
5013 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5221 ?: &(?=(%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 |)
5015 ?. ?=(%ok -.first) first
5223 ?. ?=(%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)))
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 ~]
5017 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
5234 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
5018 [%unknown ~]
5235 [%unknown ~]
5019 ?: |(?=(%var -.actual) ?=(%var -.expected))
5236 ?: |(?=(%var -.actual) ?=(%var -.expected))
5020 =/ unified=(unit isub) (itype-unify actual expected sub)
5237 =/ unified=(unit isub) (itype-unify actual expected sub)
5021 ?~ unified
5238 ?~ unified
5239+ ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5240+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
5022 ?: (itype-family-related actual expected sub) [%unknown ~]
5241 ?: (itype-family-related actual expected sub) [%unknown ~]
5023 [%bad ~]
5242 [%bad ~]
5024 [%ok u.unified next]
5243 [%ok u.unified next]
5025 ?: &(?=(%face -.actual) ?=(%face -.expected))
5244 ?: &(?=(%face -.actual) ?=(%face -.expected))
5026 ?. =(name.actual name.expected) [%bad ~]
5245 ?. =(name.actual name.expected) [%bad ~]
5027− $(actual body.actual, expected body.expected)
5246+ $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
5028− ?: ?=(%face -.actual) $(actual body.actual)
5247+ ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
5029− ?: ?=(%face -.expected) $(expected body.expected)
5248+ ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
5030 ?: (itype-face-asym actual expected sub) [%unknown ~]
5249 ?: (itype-face-asym actual expected sub) [%unknown ~]
5031 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
5250 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
5032 [%unknown ~]
5251 [%unknown ~]
5033 =/ unified=(unit isub) (itype-unify actual expected sub)
5252 =/ unified=(unit isub) (itype-unify actual expected sub)
5034 ?~ unified
5253 ?~ 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 ~]
5035 ?: (itype-family-related actual expected sub) [%unknown ~]
5256 ?: (itype-family-related actual expected sub) [%unknown ~]
5036 [%bad ~]
5257 [%bad ~]
5037 [%ok u.unified next]
5258 [%ok u.unified next]
@@ -5060,25 +5281,153 @@
5060 ["a shared type variable should reject incompatible arguments" problems]
5281 ["a shared type variable should reject incompatible arguments" problems]
5061 =? problems ?=(~ (itype-unify same fine ~))
5282 =? problems ?=(~ (itype-unify same fine ~))
5062 ["a shared type variable should accept equal arguments" problems]
5283 ["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]
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]
5063 problems
5315 problems
5065:: The expression inference below is deliberately a fragment: bindings,
5317:: 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
5067:: result for unsupported syntax is a diagnostic, never a checked module.
5319:: result for unsupported syntax is a diagnostic, never a checked module.
5069+$ ischeme [typ=itype vars=(list @ud)]
5321+$ ischeme [typ=itype vars=(list @ud)]
5070+$ ienv (list [name=term scheme=ischeme])
5322+$ ienv (list [name=term scheme=ischeme])
5071+$ imold-types (list [name=term template=ischeme])
5323+$ 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)]
5073+$ ijimports (list [face=term interface=ifile])
5328+$ 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)
5075+$ iparams (list [name=@t typ=itype])
5331+$ iparams (list [name=@t typ=itype])
5076+$ imolds (list [name=term body=shape])
5332+$ imolds (list [name=term body=shape])
5077:: A caller supplies the exact noun returned by +read-mold:jibb-import.
5333:: A caller supplies the exact noun returned by +read-mold:jibb-import.
5078:: This core has no Ford dependencies; unrecognized payloads fail closed.
5334:: This core has no Ford dependencies; unrecognized payloads fail closed.
5079+$ iexternals (list [module=term name=term result=*])
5335+$ iexternals (list [module=term name=term result=*])
5080+$ imark-externals (list [mark=term result=*])
5336+$ imark-externals (list [mark=term result=*])
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)]
5350+ |= [typ=itype sub=isub axis=@ud fuel=@ud]
5352+ =/ order=(list iwfield) ~
5353+ =/ index=(map term iwfield) *(map term iwfield)
5356+ ?: |(?=(%var -.typ) ?=(%avar -.typ) ?=(%nvar -.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))
5369+ |= [source=(list iwfield) target=(list iwfield)]
5373+ ?: =(name.i.source name.i.target) $(source t.source, target t.target)
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)
5381+ =/ fit=ifit (itype-fit typ.u.found typ.i.target sub next)
5383+ =/ rest=(unit iwidth-result) $(target t.target, sub sub.fit, next next.fit)
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]
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)
5401+ `[u.source u.target]
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)
5411+ ?. (gth (lent order.u.source) (lent order.u.target)) ~
5412+ `[u.source u.target]
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)
5421+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
5422+ `[u.source u.target]
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)
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=?]
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)]
5082+$ idiag [msg=tape sites=(list [at=span note=tape])]
5431+$ idiag [msg=tape sites=(list [at=span note=tape])]
5083+$ iresult (each [typ=itype state=istate] idiag)
5432+$ iresult (each [typ=itype state=istate] idiag)
5084+$ isample-result (each [typ=itype env=ienv state=istate] tape)
5433+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5098,8 +5447,9 @@
5098 |= [t=itype sub=isub]
5447 |= [t=itype sub=isub]
5099 ^- itype
5448 ^- itype
5100 =. t (itype-walk t sub)
5449 =. t (itype-walk t sub)
5450+ ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5101 ?: ?=(%union -.t)
5451 ?: ?=(%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)))]
5103 ?: ?=(%face -.t)
5453 ?: ?=(%face -.t)
5104 [%face name.t $(t body.t)]
5454 [%face name.t $(t body.t)]
5105 ?: ?=(%fn -.t)
5455 ?: ?=(%fn -.t)
@@ -5113,12 +5463,17 @@
5113:: generalize an aura from its sample, which requires constraint analysis
5463:: generalize an aura from its sample, which requires constraint analysis
5114:: beyond this fragment; leave those cases unresolved.
5464:: beyond this fragment; leave those cases unresolved.
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.
5116++ itype-has-gate
5468++ itype-has-gate
5117 |= t=itype
5469 |= t=itype
5121 %cell |($(t hed.t) $(t tal.t))
5473 %cell |($(t hed.t) $(t tal.t))
5476+ %collection (lien args.t |=(c=itype (itype-has-gate c)))
5122 %face $(t body.t)
5477 %face $(t body.t)
5123 %union (lien cases.t |=(c=itype (itype-has-gate c)))
5478 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5129,6 +5484,7 @@
5130 %any-atom |
5485 %any-atom |
5134++ default-decimals
5490++ default-decimals
@@ -5137,11 +5493,96 @@
5137 ?: (itype-has-gate t) t
5493 ?: (itype-has-gate t) t
5139 %nvar [%atom %ud]
5495 %nvar [%atom %ud]
5496+ %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5140 %face [%face name.t $(t body.t)]
5497 %face [%face name.t $(t body.t)]
5141 %cell [%cell $(t hed.t) $(t tal.t)]
5498 %cell [%cell $(t hed.t) $(t tal.t)]
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.
5516+++ hole-same-variable
5517+ |= [a=itype b=itype]
5519+ =/ x=(unit @ud) (hole-variable-id a)
5521+ =/ y=(unit @ud) (hole-variable-id b)
5525+ |= [t=itype state=istate]
5527+ =. t (itype-walk t sub.state)
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))))
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)))
5537+ %fn &($(t sample.t) $(t product.t))
5538+ %cell &($(t hed.t) $(t tal.t))
5541+++ default-hole-numbers
5542+ |= [all=(list ihole) prior=(list ihole) state=istate env=ienv permit=?]
5544+ :: Do not default a named capital or a variable captured from env.
5546+ ?: =(all prior) 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])
5554+:: Only obligations created inside this definition belong to it.
5556+ |= [all=(list ihole) prior=(list ihole)]
5560+ [i.all $(all t.all)]
5562+ |= [t=itype state=istate]
5564+ =. t (itype-walk t sub.state)
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)))
5570+ %fn |($(t sample.t) $(t product.t))
5571+ %cell |($(t hed.t) $(t tal.t))
5576+ |= [all=(list ihole) prior=(list ihole) state=istate]
5578+ =/ work=(list ihole) (flop (holes-created all prior))
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"]]]
5145++ itype-vars
5586++ itype-vars
5146 |= t=itype
5587 |= t=itype
5147 ^- (list @ud)
5588 ^- (list @ud)
@@ -5152,9 +5593,13 @@
5153 %any-atom ~
5594 %any-atom ~
5156 %const ~
5598 %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))))
5602+ %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5158 %face $(t body.t)
5603 %face $(t body.t)
5159 %fn (weld $(t sample.t) $(t product.t))
5604 %fn (weld $(t sample.t) $(t product.t))
5160 %cell (weld $(t hed.t) $(t tal.t))
5605 %cell (weld $(t hed.t) $(t tal.t))
@@ -5188,9 +5633,13 @@
5189 %any-atom t
5634 %any-atom t
5192 %const t
5638 %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)))]
5642+ %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5194 %face [%face name.t $(t body.t)]
5643 %face [%face name.t $(t body.t)]
5195 %fn [%fn $(t sample.t) $(t product.t)]
5644 %fn [%fn $(t sample.t) $(t product.t)]
5196 %cell [%cell $(t hed.t) $(t tal.t)]
5645 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5209,9 +5658,13 @@
5210 %any-atom |
5659 %any-atom |
5213 %const |
5663 %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))))
5667+ %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5215 %face $(t body.t)
5668 %face $(t body.t)
5216 %fn |($(t sample.t) $(t product.t))
5669 %fn |($(t sample.t) $(t product.t))
5217 %cell |($(t hed.t) $(t tal.t))
5670 %cell |($(t hed.t) $(t tal.t))
@@ -5273,9 +5726,12 @@
5273 $(ds t.ds)
5726 $(ds t.ds)
5276−:: The importer owns its algebra. Fixed atoms, cells and Jibb-named faces
5729+:: The caller supplies unchanged results from the source-aware importer.
5277−:: are decoded recursively. Singletons, unions, collections, recursive
5730+:: That boundary is trusted for source provenance: a fork alone cannot
5278−:: references and invalid face names remain unsupported, never widened.
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.
5280++ jibb-face-name
5736++ jibb-face-name
5281 |= name=@
5737 |= name=@
@@ -5285,16 +5741,180 @@
5285 ?. (is-lower i.chars) |
5741 ?. (is-lower i.chars) |
5286 (levy t.chars |=(c=@tD (in c name-mask)))
5742 (levy t.chars |=(c=@tD (in c name-mask)))
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=?]
5749+ |= [node=* module=term name=term]
5750+ ^- (unit irec-pattern)
5754+ ?: ?=([%atom %n [~ @]] node)
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)) ~
5766+ ?. ?=([%ref @ @] node) ~
5767+ ?. &(=(module +<.node) =(name +>.node)) ~
5770+ ?. ?=([%apply %list [* ~]] node) ~
5771+ =/ item $(node -.+>.node)
5773+ `[[%or ~[[%atom `0] [%cell pat.u.item [%unknown ~]]]] has.u.item]
5775+ ?. ?=([%face @ *] node) ~
5776+ ?. (jibb-face-name +<.node) ~
5779+ ?. ?=([%cell * *] node) ~
5780+ =/ left $(node +<.node)
5782+ =/ right $(node +>.node)
5784+ `[[%cell pat.u.left pat.u.right] |(has.u.left has.u.right)]
5786+ =/ cases (rec-patterns +.node module name)
5789+ ?~ t.pats.u.cases ~
5790+ ?. (rec-patterns-disjoint pats.u.cases) ~
5791+ `[[%or pats.u.cases] has.u.cases]
5795+ |= [nodes=* module=term name=term]
5796+ ^- (unit [pats=(list upat) has=?])
5797+ ?@ nodes ?:(=(nodes 0) `[~ |] ~)
5798+ =/ first (rec-pattern -.nodes module name)
5800+ =/ rest $(nodes +.nodes)
5802+ `[[pat.u.first pats.u.rest] |(has.u.first has.u.rest)]
5804+++ rec-patterns-disjoint
5805+ |= pats=(list upat)
5808+ ?. (levy t.pats |=(p=upat =(%disjoint (union-relate i.pats p)))) |
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.
5819+++ imported-faces-valid
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) |)
5829+ ?. ?=([%named @ @ *] node) |
5830+ =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
5831+ (imported-faces-valid body.n)
5834+++ imported-faces-valid-list
5837+ ?@ nodes =(nodes 0)
5838+ ?. (imported-faces-valid -.nodes) |
5841+++ imported-record-faces-valid
5842+ |= [node=* names=(list @)]
5844+ ?: ?=([%cell * *] 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) |
5853+ ?: ?=([%face @ *] node)
5854+ ?: (lien names |=(n=@ =(n +<.node))) |
5855+ (imported-faces-valid +>.node)
5856+ (imported-faces-valid node)
5288++ import-to-itype
5858++ import-to-itype
5289 |= node=*
5859 |= node=*
5290 ^- (unit itype)
5860 ^- (unit itype)
5291 ?@ node ~
5861 ?@ node ~
5292 ?+ -.node ~
5862 ?+ -.node ~
5863+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
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)
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]]
5294 ?. ?=([%atom @ ~] node) ~
5881 ?. ?=([%atom @ ~] node) ~
5295 =/ aura=@ta (@ta +<.node)
5882 =/ aura=@ta (@ta +<.node)
5296 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5883 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5297 `[%atom aura]
5884 `[%atom aura]
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))
5893+ `[%recursive (@tas module.n) (@tas name.n) `(crip "{(trip name.n)}.{(trip module.n)}")]
5895+ ?. ?=([%apply @ *] node) ~
5896+ =/ name=term (@tas +<.node)
5898+ ?: |(=(%list name) =(%unit name) =(%set name) =(%qeu name)) 1
5899+ ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
5902+ =/ args=(unit (list itype)) (import-to-itypes +>.node)
5904+ ?. =(arity (lent u.args)) ~
5905+ `[%collection name u.args]
5907+ :: Hoon's ordinary ? mold is the fork of its two %f singletons.
5909+ ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
5911+ =/ cases=(unit (list itype)) (import-to-itypes raw)
5915+ ?: (import-has-loobean-singleton u.cases) ~
5916+ ?. (import-cases-disjoint u.cases) ~
5917+ `[%union u.cases ~ ~ ~]
5299 ?. ?=([%face @ *] node) ~
5919 ?. ?=([%face @ *] node) ~
5300 =/ name=@ +<.node
5920 =/ name=@ +<.node
@@ -5311,6 +5931,52 @@
5311 `[%cell u.left u.right]
5931 `[%cell u.left u.right]
5934+++ import-direct-loobean
5937+ ?: ?=(%face -.t) $(t body.t)
5938+ ?: ?=(%union -.t) (import-has-loobean-singleton cases.t)
5939+ ?=([%const [%loobean *]] t)
5941+++ import-has-loobean-singleton
5942+ |= cases=(list itype)
5945+ ?: (import-direct-loobean i.cases) &
5950+ ^- (unit (list itype))
5951+ ?@ nodes ?:(=(nodes 0) `~ ~)
5952+ =/ first (import-to-itype -.nodes)
5954+ =/ rest $(nodes +.nodes)
5958+++ import-type-pattern
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)))]
5972+++ import-cases-disjoint
5973+ |= cases=(list itype)
5976+ =/ first=upat (import-type-pattern i.cases)
5977+ ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
5314++ find-imported-mold
5980++ find-imported-mold
5315 |= [module=term name=term externals=iexternals surs=(list term)]
5981 |= [module=term name=term externals=iexternals surs=(list term)]
5316 ^- (unit itype)
5982 ^- (unit itype)
@@ -5322,7 +5988,15 @@
5322 =/ result=* result.i.found
5988 =/ result=* result.i.found
5323 ?@ result ~
5989 ?@ result ~
5324 ?. ?=(%& -.result) ~
5990 ?. ?=(%& -.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)}")]
5327++ collect-sur-imports
6001++ collect-sur-imports
5328 |= imports=(list import)
6002 |= imports=(list import)
@@ -5351,6 +6025,7 @@
5351 =/ result=* result.i.found
6025 =/ result=* result.i.found
5352 ?@ result ~
6026 ?@ result ~
5353 ?. ?=(%& -.result) ~
6027 ?. ?=(%& -.result) ~
6028+ ?. (imported-faces-valid +.result) ~
5354 (import-to-itype +.result)
6029 (import-to-itype +.result)
5356++ find-jibb-interface
6031++ find-jibb-interface
@@ -5369,9 +6044,88 @@
5369 ?: =(name name.i.ms) `template.i.ms
6044 ?: =(name name.i.ms) `template.i.ms
5370 $(ms t.ms)
6045 $(ms t.ms)
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.
6050+++ imported-union-alias
6051+ |= [origin=[at=path name=term] molds=imold-types]
6054+ =/ template=ischeme template.i.molds
6055+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
6056+ ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
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]
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))
6071+:: Names exported by the directly imported module are visible through its
6072+:: face; a matching prelude alias is also visible without a qualifier.
6075+ |= [origin=path name=term molds=imold-types]
6078+ =/ template=ischeme template.i.molds
6079+ ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6083+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6089+ ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
6090+ =/ public=(unit term)
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)
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 ~]
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)]
6114+++ label-direct-union
6115+ |= [typ=itype body=shape name=term state=istate]
6117+ ?. ?=(%union -.typ) typ
6118+ =/ direct=? ?=(%union -.body)
6119+ =? direct ?=(%generic -.body) ?=(%union -.body.body)
6121+ ?. (lien top-molds.state |=(n=term =(n name))) typ
6122+ [%union cases.typ `[at.state name] `name args.typ]
5372:: Generic mold parameters are lexical and distinct from the enclosing
6124:: Generic mold parameters are lexical and distinct from the enclosing
5373:: value's capital variables. Arguments are substituted only once, so
6125:: value's capital variables. Arguments are substituted only once, so
5374:: an argument's variable ID cannot be captured by a template ID.
6126:: 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.
5376++ iparam-lookup
6130++ iparam-lookup
5377 |= [name=@t params=iparams]
6131 |= [name=@t params=iparams]
@@ -5423,9 +6177,46 @@
5423 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
6177 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
5424 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
6178 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
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]
6187+ ?. (lien top-molds.state |=(n=term =(n name))) ~
6188+ =/ original=(unit shape) (find-simple-mold name molds.state)
6190+ ?. =(u.original sh) ~
6191+ ?. ?=(%union -.sh) ~
6192+ =/ cs=(list shape) cases.sh
6196+ ?. ?=(%const -.i.cs) ~
6197+ ?. =(%null form.lit.i.cs) ~
6198+ ?. ?=(%cell -.i.t.cs) ~
6199+ =/ fs=(list field) fields.i.t.cs
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]
5426++ infer-mold-template
6213++ infer-mold-template
5427 |= [sh=shape state=istate]
6214 |= [sh=shape state=istate]
5428 ^- (unit [template=ischeme state=istate])
6215 ^- (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]
5429 ?: ?=(%generic -.sh)
6220 ?: ?=(%generic -.sh)
5430 ?~ vars.sh ~
6221 ?~ vars.sh ~
5431 ?. (distinct-params vars.sh) ~
6222 ?. (distinct-params vars.sh) ~
@@ -5433,33 +6224,136 @@
5433 =/ out=(unit [typ=itype state=istate])
6224 =/ out=(unit [typ=itype state=istate])
5434 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
6225 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
5435 ?~ out ~
6226 ?~ 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])))
5436 =/ used=(list @ud) (itype-vars typ.u.out)
6231 =/ used=(list @ud) (itype-vars typ.u.out)
5437 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
6232 ?. (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)]
5439 =/ out=(unit [typ=itype state=istate])
6234 =/ out=(unit [typ=itype state=istate])
5440 (infer-simple-shape sh state(params ~, in-mold &))
6235 (infer-simple-shape sh state(params ~, in-mold &))
5441 ?~ out ~
6236 ?~ out ~
6237+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
5442 ?: ?=(^ (itype-vars typ.u.out)) ~
6238 ?: ?=(^ (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)]
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]
6248+ =/ n=term i.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)))
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))))
6273+ ?. ?=([%invalid ?(%aura %core) @] raw) ~
6274+ `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
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]
6281+ ?: ?=(^ (infer-simple-shape sh state)) ~
6284+ =/ direct=(unit idiag) (direct-import-invalid sh state)
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)
6293+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
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)
6302+++ nested-field-invalid
6303+ |= [fields=(list field) state=istate]
6308+ %bare shape.i.fields
6309+ %face shape.i.fields
6310+ %pun [%ref at.i.fields ~[name.i.fields]]
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)
6316+++ sample-import-invalid
6317+ |= [s=sample env=ienv state=istate]
6319+ =/ result=isample-result (infer-sample s env state)
6320+ ?: ?=(%& -.result) ~
6321+ ?. =(p.result "sample mold is not supported by partial inference") ~
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)
6330+++ nested-samples-invalid
6331+ |= [items=(list sample) env=ienv state=istate]
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)
5445++ infer-simple-shape
6338++ infer-simple-shape
5446 |= [sh=shape state=istate]
6339 |= [sh=shape state=istate]
5447 ^- (unit [typ=itype state=istate])
6340 ^- (unit [typ=itype state=istate])
6342+ %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
5450 ?: =(0 aura.sh) `[[%any-atom ~] state]
6344 ?: =(0 aura.sh) `[[%any-atom ~] state]
5451 `[[%atom aura.sh] state]
6345 `[[%atom aura.sh] state]
5452 %flag `[[%flag ~] state]
6346 %flag `[[%flag ~] state]
6347+ %noun `[[%noun ~] state]
5454− ?. =(%term form.lit.sh) ~
6349+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
5455 `[[%const lit.sh] state]
6350 `[[%const lit.sh] state]
5457 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6352 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
5458 ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
6353 ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
5459 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
6354 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
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]
5463 %cell (infer-simple-fields fields.sh state)
6357 %cell (infer-simple-fields fields.sh state)
5465 =/ arg=(unit [typ=itype state=istate]) $(sh sample.sh)
6359 =/ arg=(unit [typ=itype state=istate]) $(sh sample.sh)
@@ -5477,7 +6371,7 @@
5477 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
6371 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
5478 ?~ found ~
6372 ?~ found ~
5479 ?^ vars.u.found ~
6373 ?^ vars.u.found ~
5480− `[typ.u.found state]
6374+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
5481 =/ found=(unit itype)
6375 =/ found=(unit itype)
5482 (find-imported-mold i.t.names.sh n externals.state surs.state)
6376 (find-imported-mold i.t.names.sh n externals.state surs.state)
5483 ?~ found ~
6377 ?~ found ~
@@ -5489,11 +6383,20 @@
5489 `[u.imported state]
6383 `[u.imported state]
5490 ?: (lien active.state |=(x=term =(x n))) ~
6384 ?: (lien active.state |=(x=term =(x n))) ~
5491 =/ found=(unit shape) (find-simple-mold n molds.state)
6385 =/ 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))) ~
6389+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state)
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]
5493 =/ out=(unit [typ=itype state=istate])
6395 =/ out=(unit [typ=itype state=istate])
5494 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
6396 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
5495 ?~ out ~
6397 ?~ out ~
6398+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
5496− `[typ.u.out state.u.out(active active.state, in-mold in-mold.state, params params.state)]
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)]
5498 ?~ ref.sh ~
6401 ?~ ref.sh ~
5499 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
6402 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -5508,10 +6411,18 @@
5508 ?~ vars.u.template ~
6411 ?~ vars.u.template ~
5509 =/ applied=(unit itype) (template-apply u.template types.u.args)
6412 =/ applied=(unit itype) (template-apply u.template types.u.args)
5510 ?~ applied ~
6413 ?~ 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]
5512 ?: (lien active.state.u.args |=(x=term =(x n))) ~
6415 ?: (lien active.state.u.args |=(x=term =(x n))) ~
5513 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
6416 =/ 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)
6422+ ?~ vars.u.prelude-entry ~
6423+ =/ applied=(unit itype) (template-apply u.prelude-entry types.u.args)
6425+ `[u.applied state.u.args]
5515 ?. ?=(%generic -.u.found) ~
6426 ?. ?=(%generic -.u.found) ~
5516 ?. (distinct-params vars.u.found) ~
6427 ?. (distinct-params vars.u.found) ~
5517 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6428 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
@@ -5519,14 +6430,19 @@
5519 =/ out=(unit [typ=itype state=istate])
6430 =/ out=(unit [typ=itype state=istate])
5520 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
6431 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
5521 ?~ out ~
6432 ?~ out ~
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)
5522− `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
6438+ `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args, holes holes.state.u.args)]
5524 =/ param=(unit itype) (iparam-lookup name.sh params.state)
6440 =/ param=(unit itype) (iparam-lookup name.sh params.state)
5525 ?^ param `[u.param state]
6441 ?^ param `[u.param state]
5526 ?: in-mold.state ~
6442 ?: in-mold.state ~
5527 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
6443 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
5528 ?^ n `[[%var u.n] state]
6444 ?^ 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])]
@@ -5559,12 +6475,12 @@
5559 ^- isample-result
6475 ^- isample-result
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))))
5563 [%| "sample shadows a name"]
6479 [%| "sample shadows a name"]
5564 =/ t=itype [%var next.state]
6480 =/ t=itype [%var next.state]
5565 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
6481 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
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))))
5568 [%| "sample shadows a name"]
6484 [%| "sample shadows a name"]
5569 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
6485 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
5570 ?~ t [%| "sample mold is not supported by partial inference"]
6486 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -5602,8 +6518,8 @@
5602 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
6518 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
5604:: Local definitions generalize only variables outside their enclosing
6520:: Local definitions generalize only variables outside their enclosing
5605−:: environment and explicit-capital scope. Unresolved groups stay
6521+:: environment and explicit-capital scope. Recursive gate groups use
5606−:: unsupported: this fragment does not infer recursive definitions.
6522+:: monomorphic placeholders while their bodies are checked.
5608+$ ilocal-result (each [env=ienv state=istate] idiag)
6524+$ ilocal-result (each [env=ienv state=istate] idiag)
5609++ free-env-vars
6525++ free-env-vars
@@ -5632,6 +6548,7 @@
5634 ?: ?=(%mold -.i.ds) $(ds t.ds)
6550 ?: ?=(%mold -.i.ds) $(ds t.ds)
6551+ ?: =(name.i.ds %proj) |
5635 ?. (unique-value-name name.i.ds names) |
6552 ?. (unique-value-name name.i.ds names) |
5636 ?: ?=(^ (ienv-lookup name.i.ds env)) |
6553 ?: ?=(^ (ienv-lookup name.i.ds env)) |
5637 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
6554 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -5655,6 +6572,7 @@
5656 ?~ locals &
6573 ?~ locals &
5657 =/ n=term name.i.locals
6574 =/ n=term name.i.locals
5658 ?. (unique-value-name n names) |
6576 ?. (unique-value-name n names) |
5659 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
6577 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
5660 ?: (lien marks.state |=(m=term =(n m))) |
6578 ?: (lien marks.state |=(m=term =(n m))) |
@@ -5672,6 +6590,145 @@
5672 ?~ inferred |
6590 ?~ inferred |
5673 $(locals t.locals)
6591 $(locals t.locals)
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]
6598+ ^- (list icap-site)
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))
6606+ =/ inside=(list icap-site) (scope-shape body.s)
6607+ (skim inside |=(site=icap-site !(lien vars.s |=(v=@t =(v name.site)))))
6613+ ^- (list icap-site)
6615+ %face (scope-shape shape.f)
6616+ %bare (scope-shape shape.f)
6622+ ^- (list icap-site)
6624+ %face (scope-shape shape.s)
6625+ %bare (scope-shape shape.s)
6626+ %cell (zing (turn items.s scope-sample))
6632+ ^- (list icap-site)
6634+ =/ first=(list icap-site)
6636+ %expr (scope-expr p.i.ps)
6639+ (weld first $(ps t.ps))
6643+ ^- (list icap-site)
6645+ =/ first=(list icap-site)
6647+ %expr (scope-expr p.i.ps)
6650+ (weld first $(ps t.ps))
6654+ ^- (list icap-site)
6656+ =/ first=(list icap-site) (scope-expr val.i.xs)
6657+ (weld first $(xs t.xs))
6661+ ^- (list icap-site)
6663+ =/ first=(list icap-site) (scope-expr val.i.xs)
6664+ (weld first $(xs t.xs))
6668+ ^- (list icap-site)
6670+ =/ first=(list icap-site) (scope-expr val.i.xs)
6671+ (weld first $(xs t.xs))
6675+ ^- (list icap-site)
6677+ =/ first=(list icap-site) (scope-expr i.xs)
6678+ (weld first $(xs t.xs))
6682+ ^- (list icap-site)
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)
6693+ =/ first=(list icap-site) (scope-sample sample.e)
6694+ =/ last=(list icap-site) (scope-expr body.e)
6697+ =/ first=(list icap-site) (scope-sample sample.e)
6698+ =/ last=(list icap-site) (scope-expr body.e)
6701+ =/ first=(list icap-site) (scope-expr head.e)
6702+ =/ last=(list icap-site) (scope-exprs args.e)
6705+ =/ first=(list icap-site) (scope-shape shape.e)
6706+ =/ last=(list icap-site) (scope-expr val.e)
6709+ =/ first=(list icap-site) (scope-expr val.e)
6710+ =/ last=(list icap-site) (scope-expr then.e)
6713+ =/ first=(list icap-site) (scope-expr subject.e)
6714+ =/ last=(list icap-site) (scope-arms arms.e)
6716+ %body (scope-expr final.e)
6720+++ reserve-cap-sites
6721+ |= [sites=(list icap-site) state=istate]
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]))
6728+ |= [e=expr state=istate]
6730+ (reserve-cap-sites (scope-expr e) state)
5675++ infer-local-defs
6732++ infer-local-defs
5676 |= [ds=(list def) env=ienv state=istate]
6733 |= [ds=(list def) env=ienv state=istate]
5677 ^- ilocal-result
6734 ^- ilocal-result
@@ -5680,26 +6737,65 @@
5682 ?~ remaining [%& env state]
6739 ?~ remaining [%& env state]
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)
5683− ?. progressed [%| ["local definitions need unsupported inference" ~]]
6745+ ?~ grouped [%| ["local definitions need unsupported inference" ~]]
6746+ $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
5684 $(ds (flop remaining), remaining ~, progressed |)
6747 $(ds (flop remaining), remaining ~, progressed |)
5685 =/ d=def i.ds
6748 =/ d=def i.ds
5686 ?> ?=(%value -.d)
6749 ?> ?=(%value -.d)
6750+ =/ local-state=istate (reserve-def-caps val.d state)
5687− =/ inferred=iresult (infer-fragment val.d env state)
6751+ =/ inferred=iresult (infer-fragment val.d env local-state)
6752+ =/ retried=? ?=(%| -.inferred)
6753+ =? inferred retried (infer-recursive-gate d env local-state)
5688 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6754 ?: ?=(%| -.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)
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" ~]]
5689 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
6764 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
5690 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
6765 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
5691 $(ds t.ds, remaining [d remaining])
6766 $(ds t.ds, remaining [d remaining])
5692 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
6767 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
5693 $(ds t.ds, remaining [d remaining])
6768 $(ds t.ds, remaining [d remaining])
5694 =/ free=(list @ud)
6769 =/ 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))
5696 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
6771 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
5697 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6772 =. 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 &)
6775+:: Try complete cyclic local groups after individual definitions stall.
6776+:: Components with non-gates or unresolved constraints stay unavailable.
6779+ |= [ds=(list def) groups=icomponents env=ienv state=istate]
6780+ ^- (unit [rest=(list def) env=ienv state=istate])
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)
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)
6794+ `[rest env.p.result state.p.result]
5700:: Read only fields of a known record. Unresolved field constraints and
6796:: Read only fields of a known record. Unresolved field constraints and
5701−:: ambiguous repeated faces are outside this fragment (doc question:
6797+:: ambiguous repeated faces are outside this fragment. Imported record
5702−:: whether duplicate imported Hoon faces are valid or select a field).
6798+:: spines with repeated names are unavailable when used.
5704++ record-fields-named
6800++ record-fields-named
5705 |= [name=term t=itype sub=isub]
6801 |= [name=term t=itype sub=isub]
@@ -5718,92 +6814,1038 @@
5718 ^- iresult
6814 ^- iresult
5719 =/ reverse=(list term) (flop names)
6815 =/ reverse=(list term) (flop names)
5720 ?~ reverse [%| ["empty wing" ~]]
6816 ?~ reverse [%| ["empty wing" ~]]
5721− =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6817+ =/ iface=(unit ifile) (find-jibb-interface i.reverse jimports.state)
5722− ?~ scheme [%| ["field access is not supported by partial inference" ~]]
5723− =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
5724 =/ fields=(list term) t.reverse
6818 =/ fields=(list term) t.reverse
6819+ ?~ fields [%| ["field access is not supported by partial inference" ~]]
6820+ =/ scheme=(unit ischeme)
6822+ (ienv-lookup i.reverse env)
6823+ (ienv-lookup i.fields values.u.iface)
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)
5725 =/ typ=itype typ.inst
6833 =/ typ=itype typ.inst
5727− ?~ fields [%& typ state.inst]
6835+ ?~ remaining [%& typ state.inst]
5728− =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
6836+ =/ found=(list itype) (record-fields-named i.remaining typ sub.state.inst)
5729 ?~ found [%| ["field is not available to partial inference" ~]]
6837 ?~ found [%| ["field is not available to partial inference" ~]]
5730 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6838 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
5731− $(fields t.fields, typ i.found)
6839+ $(remaining t.remaining, typ i.found)
5733−++ infer-fragment
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.
6845+++ context-union-branch
6850+ %group $(e inner.e)
6851+ %body ?~(defs.e $(e final.e) |)
6855+++ infer-union-context
5734− |= [e=expr env=ienv state=istate]
6856+ |= [e=expr expected=itype env=ienv state=istate context=span]
5735 ^- iresult
6857 ^- 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)
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" ~]]
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" ~]]
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)]
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.
6912+++ context-list-expression
5738− ?- form.lit.e
6917+ %tuple &
5739− %number ?: =(%ud aura.lit.e)
6918+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.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" ~]]
5751− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
5752− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
5753− [%& [%atom %t] state]
5755− ?~ names.e [%| ["empty wing" ~]]
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]
5768 %group $(e inner.e)
6919 %group $(e inner.e)
5769− %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [next.state tags.state])]
6920+ %body ?~(defs.e $(e final.e) |)
5771− =/ traced=iresult $(e val.e)
6922+ ==
5772− ?: ?=(%| -.traced) traced
6923+::
5773− $(e then.e, state state.p.traced)
6924+++ infer-list-context
5774− %tuple (infer-simple-items items.e env state)
6925+ |= [e=expr expected=itype env=ienv state=istate context=span]
5775− %body
6926+ ^- iresult
5776− ?~ defs.e $(e final.e)
6927+ ?: ?=(%group -.e) $(e inner.e)
5777− =/ local-names=(list term) (global-value-names defs.e)
6928+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
5778− ?. (local-names-valid defs.e env state)
6929+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
5779− [%| ["local definitions shadow a name" ~]]
6930+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
5780− =/ local-molds=imolds (collect-simple-molds defs.e)
6931+ [%| ["list literal needs the standard prelude in partial inference" ~]]
5781− ?. (local-mold-names-valid local-molds state)
6932+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
5782− [%| ["local molds shadow a name" ~]]
6933+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
5783− =/ local-state=istate
6934+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
5784− state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
6935+ [%| ["list literal needs the standard prelude in partial inference" ~]]
5785− ?. (local-molds-supported local-molds local-state)
6936+ =/ target=itype (itype-walk expected sub.state)
5786− [%| ["local molds need unsupported inference" ~]]
6937+ ?. ?=(%collection -.target) [%| ["list context is not supported by partial inference" ~]]
5787− =/ values=(list def) (local-value-defs defs.e)
6938+ ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
5788− =/ locals=ilocal-result (infer-local-defs values env local-state)
6939+ ?~ args.target [%| ["list context is not supported by partial inference" ~]]
5789− ?: ?=(%| -.locals) locals
6940+ ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
5790− =/ result=iresult $(e final.e, env env.p.locals, state state.p.locals)
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" ~]]
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)
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" ~]]
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)]
6969+++ infer-open-list-items
6970+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
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" ~]]
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))
6987+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
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" ~]]
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))
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.
7007+++ unit-empty-pattern
7011+ =(%null form.lit.p)
7013+++ unit-payload-pattern
7020+ ?. (unit-empty-pattern i.items.p) ~
7021+ ?. ?=(%bind -.i.t.items.p) ~
7027+ ?. ?=(%const -.t) |
7030+++ unit-payload-case
7034+ ?. (unit-empty-case hed.t) ~
7035+ =/ payload=itype tal.t
7036+ =? payload ?=(%face -.payload) body.payload
7039+++ unit-union-payload
7042+ ?. ?=(%union -.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)
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.
7054+++ list-payload-pattern
7056+ ^- (unit [head=term tail=term])
7061+ ?. ?=(%bind -.i.items.p) ~
7062+ ?. ?=(%bind -.i.t.items.p) ~
7063+ `[name.i.items.p name.i.t.items.p]
7065+++ infer-list-branch
7066+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span]) typ=itype]
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" ~]]
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]
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
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)]
7108+++ infer-unit-branch
7109+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
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)
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]
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
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)]
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]
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"]]]]
7168+ [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
7169+ [%| ["interpolation type needs unsupported inference" ~]]
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]
7179+ ?~ t.ps (union-pattern i.ps t)
7180+ =. t ?:(?=(%face -.t) body.t t)
7182+ ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
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)
7190+ |= [p=pattern t=itype]
7192+ =. t ?:(?=(%face -.t) body.t t)
7197+ ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
7198+ ?: ?=(%cell -.t) %none
7200+ ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
7202+ %str ?:(?=(%cell -.t) %none %unknown)
7203+ %cell (union-pattern-items items.p t)
7206+++ union-pattern-has-bind
7211+ (lien items.p union-pattern-has-bind)
7213+++ union-pattern-bind-items
7214+ |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
7217+ ?~ t.ps (union-pattern-bind i.ps t env globals)
7218+ =. t ?:(?=(%face -.t) body.t t)
7220+ =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
7222+ $(ps t.ps, t tal.t, env u.first)
7224+++ union-pattern-bind
7225+ |= [p=pattern t=itype env=ienv globals=(list term)]
7227+ =. t ?:(?=(%face -.t) body.t t)
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)
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]
7240+ |= [hs=(list itype) ts=(list itype) out=(list itype)]
7243+ =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
7244+ $(hs t.hs, out (weld rows out))
7248+ ^- (unit (list itype))
7251+ `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
7253+ =/ body=(unit (list itype)) $(t body.t)
7255+ `(turn u.body |=(x=itype [%face name.t x]))
7257+ =/ hed=(unit (list itype)) $(t hed.t)
7259+ =/ tal=(unit (list itype)) $(t tal.t)
7261+ ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
7262+ `(finite-product u.hed u.tal ~)
7267+ |= [xs=(list itype) out=(list ifinite) origin=@ud]
7268+ ^- (unit (list ifinite))
7270+ =/ parts=(unit (list itype)) (finite-type i.xs)
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))
7276+++ infer-known-union-whole
7277+ |= [e=expr env=ienv subject=iresult]
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) ~
7291+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7292+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7295+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7297+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
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)
7313+++ infer-known-union-context-whole
7314+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
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) ~
7328+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7329+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7332+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7334+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
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" ~]]
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)
7357+++ infer-known-union-finite
7358+ |= [e=expr env=ienv subject=iresult expected=(unit [typ=itype context=span])]
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) ~
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]
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))))
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" ~]]
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
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" ~]]
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)
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
7417+ ?. ?=(%branch -.e) |
7420+ =/ p=pattern pat.i.arms.e
7422+ !(levy items.p |=(x=pattern ?=(%bind -.x)))
7424+++ infer-single-case-branch
7425+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7427+ ?> (single-structured-pattern 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" ~]]
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)]
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.
7459+ |= [e=expr subject=iresult]
7461+ ?: ?=(%| -.subject) subject
7462+ ?. ?=(%branch -.e) subject
7463+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7464+ ?. ?=(%jrec -.typ) 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))]
7485+++ infer-known-union-branch-subject
7486+ |= [e=expr env=ienv subject=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 ~)
7493+++ infer-known-union-branch
7494+ |= [e=expr env=ienv state=istate]
7497+ (infer-known-union-branch-subject e env (infer-fragment subject.e env state))
7499+++ infer-known-union-context-subject
7500+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
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])
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
7515+ %str !(lien pieces.e |=(p=piece ?=(%expr -.p)))
7519+++ safe-union-subject
7522+ ?: ?=(%group -.e) $(e inner.e)
7525+ ?. ?=(%wing -.head.e) |
7526+ (levy args.e simple-union-subject-arg)
7528+++ duplicate-loobean-arms
7531+ ?. ?=(%branch -.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)
7541+++ union-subject-call
7544+ ?: ?=(%group -.e) $(e inner.e)
7547+++ known-union-subject
7548+ |= [e=expr env=ienv state=istate]
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)) ~
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]
7563+ =. t (itype-walk t sub)
7566+ =/ first=itype (itype-walk hed.t sub)
7567+ ?. ?=(%face -.first) |
7570+++ infer-change-edits
7571+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
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)
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" ~]]
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])
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]
7597+ ?. =(at /lib/jibb/prelude/jibb) |
7599+ ?^ t.vars.template |
7600+ =/ v=@ud i.vars.template
7601+ =/ nil=itype [%const [%null %n 0 '~']]
7603+ [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
7604+ =(typ.template expected)
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]
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
7622+ |= [t=itype value=@ sub=isub]
7624+ =. t (itype-walk t sub)
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)
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
7637+ %union (tag-presence-cases cases.t value sub)
7641+++ missing-union-tag
7642+ |= [e=expr expected=itype sub=isub context=span]
7645+ ?. =(%term form.lit.e) ~
7646+ =. expected (itype-walk expected sub)
7648+ ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
7649+ ?. ?=(%union -.expected) ~
7650+ ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
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"]]]
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]
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)
7675+ ?. ?=(%tuple -.e) ~
7676+ (nested-missing-items items.e actual expected sub next context)
7678+++ nested-missing-items
7679+ |= [items=(list item) actual=itype expected=itype sub=isub next=@ud context=span]
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)
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.
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]]]
7704+:: A segment costs one shared step; dynamic segments are not handled yet.
7706+ |= [segs=(list qseg) fuel=@ud]
7710+ ?. ?=(%knot -.i.segs) ~
7711+ $(segs t.segs, fuel (dec fuel))
7714+ |= [e=expr env=ienv state=istate]
7717+ %pair $(e (pair-as-cell 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])]
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]
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)
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)]
7771+ ?~ names.e [%| ["empty wing" ~]]
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)
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)
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])]
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)
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)
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)
5791 ?: ?=(%| -.result) result
7821 ?: ?=(%| -.result) result
5792 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
7822 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
5794 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
7824 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
7826+ ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
5795− ?~ t.arms.e (infer-cell-branch e env state)
7827+ (infer-cell-branch e env state ~)
5796− ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
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)
5797 =/ x=arm i.arms.e
7833 =/ x=arm i.arms.e
5798 =/ y=arm i.t.arms.e
7834 =/ y=arm i.t.arms.e
5799− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
7835+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
5800− ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
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)
5801 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
7839 ?. &(=(%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)
5803 ?: =(val.lit.pat.x val.lit.pat.y)
7842 ?: =(val.lit.pat.x val.lit.pat.y)
5804 [%| ["branch does not cover both loobeans" ~]]
7843 [%| ["branch does not cover both loobeans" ~]]
5805 =/ subject=iresult $(e subject.e)
7844 =/ subject=iresult $(e subject.e)
5806 ?: ?=(%| -.subject) subject
7845 ?: ?=(%| -.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" ~]]
5807 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
7849 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
5808 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
7850 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
5809 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
7851 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -5816,6 +7858,8 @@
5816 [%| ["branch widening is not supported by partial inference" ~]]
7858 [%| ["branch widening is not supported by partial inference" ~]]
5817 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
7859 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
5818 ?~ joined
7860 ?~ joined
7861+ ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
7862+ [%| ["recursive branch matching is not supported by partial inference" ~]]
5819 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
7863 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
5820 [%| ["branch tag or union context is not supported by partial inference" ~]]
7864 [%| ["branch tag or union context is not supported by partial inference" ~]]
5821 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
7865 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
@@ -5828,53 +7872,391 @@
5828 [%& typ.p.left state.p.right(sub u.joined)]
7872 [%& typ.p.left state.p.right(sub u.joined)]
5830 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
7874 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
7876+ =/ diag=(unit idiag) (nested-import-invalid shape.e state)
7877+ ?^ diag [%| u.diag]
5831− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
7878+ [%| ["cast mold is not supported by partial inference" ~]]
5832− =/ value=iresult $(e val.e, state state.u.target)
7879+ =/ value=iresult
7880+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
5833 ?: ?=(%| -.value) value
7881 ?: ?=(%| -.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" ~]]
5834 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
7885 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
5835 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
7886 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
5836 ?: ?=(%bad -.fit)
7887 ?: ?=(%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]
5837 [%| ["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)]]]]
7892 [%| ["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)]]]]
5838 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
7893 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
5839 [%& merged state.p.value(sub sub.fit, next next.fit)]
7894 [%& merged state.p.value(sub sub.fit, next next.fit)]
5840 %crash [%& [%var next.state] state(next +(next.state))]
7895 %crash [%& [%var next.state] state(next +(next.state))]
5842 =/ sam=isample-result (infer-sample sample.e env state)
7897 =/ sam=isample-result (infer-sample sample.e env state)
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]
5843− ?: ?=(%| -.sam) [%| [p.sam ~]]
7901+ [%| [p.sam ~]]
5844 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
7902 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
5845 ?: ?=(%| -.body) body
7903 ?: ?=(%| -.body) body
5846 [%& [%fn typ.p.sam typ.p.body] state.p.body]
7904 [%& [%fn typ.p.sam typ.p.body] state.p.body]
5847 %gate-wide
7905 %gate-wide
5848 =/ sam=isample-result (infer-sample sample.e env state)
7906 =/ sam=isample-result (infer-sample sample.e env state)
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]
5849− ?: ?=(%| -.sam) [%| [p.sam ~]]
7910+ [%| [p.sam ~]]
5850 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
7911 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
5851 ?: ?=(%| -.body) body
7912 ?: ?=(%| -.body) body
5852 [%& [%fn typ.p.sam typ.p.body] state.p.body]
7913 [%& [%fn typ.p.sam typ.p.body] state.p.body]
5854 ?~ args.e [%| ["call has no argument" ~]]
7915 ?~ args.e [%| ["call has no argument" ~]]
5855− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
7916+ ?: (explicit-proj-call e env state)
5856− =/ head=iresult $(e head.e)
7917+ [%| ["proj needs an expected record type" ~]]
5857− ?: ?=(%| -.head) head
7918+ (infer-call-with-head e env state (infer-fragment head.e env state))
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)
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" ~]]
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)
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)]
5875 * [%| ["expression is not supported by partial inference" ~]]
7919 * [%| ["expression is not supported by partial inference" ~]]
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.
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)
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)]]
7942+++ infer-call-with-head
7943+ |= [e=expr env=ienv state=istate head=iresult]
7946+ ?~ args.e [%| ["call has no argument" ~]]
7947+ ?: ?=(%| -.head) head
7948+ =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
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)
7961+ =/ shape=(unit [source=iwfields target=iwfields])
7963+ (width-shape typ.p.arg sample.ht sub.st)
7964+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
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" ~]]
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)
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)
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)]
7993+ |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
7994+ ^- (unit [at=span typ=itype])
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)
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)
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.
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]
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" ~]]
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)]
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]
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)])
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]
8071+ =/ order=(list iwfield) ~
8072+ =/ index=(map term iwfield) *(map term iwfield)
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]
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)
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]
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)
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)
8113+:: Recognize only the reserved unqualified, one-argument operation.
8114+++ explicit-proj-call
8115+ |= [e=expr env=ienv state=istate]
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))) |
8124+ ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
8125+++ infer-proj-source
8126+ |= [e=expr expected=itype env=ienv state=istate context=span]
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]
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])]
8148+++ infer-call-context-arg
8149+ |= [e=expr expected=itype env=ienv state=istate context=span]
8151+ ?: ?=(%pair -.e) $(e (pair-as-cell e))
8152+ ?: ?=(%group -.e) $(e inner.e)
8153+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.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)
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))
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)
8188+ ?. =(%loobean form.lit.e) ~
8189+ ?. ?=(%const -.target) ~
8190+ ?. =(%loobean form.literal.target) ~
8192+ ?^ singleton [%& u.singleton state]
8193+ =/ known=(unit iresult)
8194+ ?: ?=(%branch -.e) (known-union-subject subject.e env state)
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)
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
8220+ ?:(?=(%face -.expected) body.expected expected)
8222+++ infer-call-context-items
8223+ |= [items=(list item) expected=itype env=ienv state=istate context=span]
8225+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
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)
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]
8244+++ infer-call-context-args
8245+ |= [args=(list expr) expected=itype env=ienv state=istate context=span]
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)
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]
5878:: Tuple and record expressions preserve their explicitly written faces.
8260:: Tuple and record expressions preserve their explicitly written faces.
5880++ infer-simple-items
8262++ infer-simple-items
@@ -5890,11 +8272,55 @@
5890 ?: ?=(%| -.tail) tail
8272 ?: ?=(%| -.tail) tail
5891 [%& [%cell ht typ.p.tail] state.p.tail]
8273 [%& [%cell ht typ.p.tail] state.p.tail]
5893−:: A single two-binder cell pattern covers every value of a cell type.
8275+:: A single all-binder cell pattern covers a known cell spine; the final
5894−:: No other pattern matrix is implemented here.
8276+:: binder captures the remaining noun. Other pattern matrices stay partial.
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)
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
8292+++ cell-pattern-types
8293+ |= [names=(list term) env=ienv next=@ud]
8294+ ^- [typ=itype env=ienv next=@ud]
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]
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]
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))
8313+++ cell-binder-pattern
8316+ ?. ?=(%branch -.e) |
8319+ ?. ?=(%cell -.pat.i.arms.e) |
8320+ !(single-structured-pattern e)
5896++ infer-cell-branch
8322++ infer-cell-branch
5897− |= [e=expr env=ienv state=istate]
8323+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
5898 ^- iresult
8324 ^- iresult
5899 ?> ?=(%branch -.e)
8325 ?> ?=(%branch -.e)
5900 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
8326 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -5903,23 +8329,31 @@
5903 =/ pats=(list pattern) items.pat.arm
8329 =/ pats=(list pattern) items.pat.arm
5904 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
8330 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
5905 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
8331 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
5906− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
8332+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
5907− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
8333+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
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" ~]]
5913 =/ subject=iresult (infer-fragment subject.e env state)
8334 =/ subject=iresult (infer-fragment subject.e env state)
5914 ?: ?=(%| -.subject) subject
8335 ?: ?=(%| -.subject) subject
5915 =/ st=istate state.p.subject
8336 =/ 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" ~]]
5916 ?: (itype-has-face typ.p.subject sub.st)
8340 ?: (itype-has-face typ.p.subject sub.st)
5917 [%| ["record patterns are not supported by partial inference" ~]]
8341 [%| ["record patterns are not supported by partial inference" ~]]
5918− =/ head=itype [%var next.st]
8342+ ?: (cell-pattern-spine-unknown subject-type p.names sub.st)
5919− =/ tail=itype [%var +(next.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)
5920− =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
8345+ =/ sub=(unit isub) (itype-unify typ.p.subject typ.binders sub.st)
5921 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
8346 ?~ 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)]
5924++ show-itype
8358++ show-itype
5925 |= [t=itype sub=isub]
8359 |= [t=itype sub=isub]
@@ -5938,11 +8372,18 @@
5938 %atom "@{(trip aura.t)}"
8372 %atom "@{(trip aura.t)}"
5939 %any-atom "@"
8373 %any-atom "@"
5940 %flag "?"
8374 %flag "?"
5941 %tag (trip txt.literal.t)
8376 %tag (trip txt.literal.t)
5942 %const (trip txt.literal.t)
8377 %const (trip txt.literal.t)
5943− %union "<union>"
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)})"
5944− %face "[{(trip name.t)}={$(t body.t)}]"
8385+ %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
5945− %fn "$-({$(t sample.t)} {$(t product.t)})"
8386+ %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
5946 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
8387 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
@@ -5950,9 +8391,23 @@
5950 |= [t=itype sub=isub]
8391 |= [t=itype sub=isub]
5952 =. t (itype-walk t sub)
8393 =. 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)
8397+++ show-itype-context
8398+ |= [t=itype sub=isub]
8400+ =. t (itype-walk t sub)
8401+ ?: &(?=(%union -.t) ?=(~ label.t)) "({(show-itype t sub)})"
5954 (show-itype t sub)
8402 (show-itype t sub)
8405+ |= [cases=(list itype) sub=isub]
8408+ ?~ t.cases (show-itype-context i.cases sub)
8409+ "{(show-itype-context i.cases sub)} {$(cases t.cases)}"
5956:: Include the type at a conflicting site where it can be printed.
8411:: Include the type at a conflicting site where it can be printed.
5957:: A lone unresolved variable or decimal variable keeps the neutral label.
8412:: A lone unresolved variable or decimal variable keeps the neutral label.
@@ -5966,9 +8421,13 @@
5967 %any-atom |
8422 %any-atom |
5970 %const |
8426 %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))))
8430+ %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
5972 %face $(typ body.typ)
8431 %face $(typ body.typ)
5973 %fn |($(typ sample.typ) $(typ product.typ))
8432 %fn |($(typ sample.typ) $(typ product.typ))
5974 %cell |($(typ hed.typ) $(typ tal.typ))
8433 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -5979,6 +8438,7 @@
5980 =/ normalized=itype (itype-normalize typ sub)
8439 =/ normalized=itype (itype-normalize typ sub)
5981 ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
8440 ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
8441+ ?: (itype-has-hidden-recursive normalized) label
5982 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
8442 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
5983 ?: (gth (lent vars) 26) label
8443 ?: (gth (lent vars) 26) label
5984 =/ printable=itype (canonical-itype normalized vars)
8444 =/ printable=itype (canonical-itype normalized vars)
@@ -5987,13 +8447,64 @@
5987:: A capital in a written mold is generalized with its enclosing ++.
8447:: A capital in a written mold is generalized with its enclosing ++.
5988:: Atom constraints may remain generic; until full rigidity checking
8448:: Atom constraints may remain generic; until full rigidity checking
5989:: is implemented, do not report a type if one became more specific.
8449:: 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).
8454+ |= [n=@ud caps=icaps sub=isub]
8457+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8458+ =/ ident=(unit @ud)
8463+ ?~ ident $(caps t.caps)
8468+ |= [n=@ud caps=icaps sub=isub]
8471+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8472+ =/ ident=(unit @ud)
8477+ ?~ ident $(caps t.caps)
8478+ ?: =(n u.ident) `i.caps
8482+ |= [caps=icaps sub=isub]
8483+ ^- (unit [first=icap second=icap])
8485+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8486+ =/ ident=(unit @ud)
8491+ ?~ ident $(caps t.caps)
8492+ =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
8493+ ?^ found `[u.found i.caps]
5991++ constrained-capitals
8496++ constrained-capitals
5992 |= [caps=icaps sub=isub]
8497 |= [caps=icaps sub=isub]
5994 ?~ caps |
8499 ?~ caps |
5995 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8500 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8501+ =/ ident=(unit @ud)
5996− ?. |(?=(%var -.resolved) ?=(%avar -.resolved)) &
8503+ %var `id.resolved
8507+ ?: (cap-id-in u.ident t.caps sub) &
5997 $(caps t.caps)
8508 $(caps t.caps)
5999:: An atom variable may be generalized when an explicit capital, sample
8510:: An atom variable may be generalized when an explicit capital, sample
@@ -6020,9 +8531,13 @@
6021 %any-atom |
8532 %any-atom |
6024 %const |
8536 %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))))
8540+ %collection (lien args.t |=(c=itype (has-atom-var n c)))
6026 %face $(t body.t)
8541 %face $(t body.t)
6027 %fn |($(t sample.t) $(t product.t))
8542 %fn |($(t sample.t) $(t product.t))
6028 %cell |($(t hed.t) $(t tal.t))
8543 %cell |($(t hed.t) $(t tal.t))
@@ -6069,9 +8584,9 @@
6070:: Build the supported part of the value environment in dependency order.
8585:: Build the supported part of the value environment in dependency order.
6071:: Each pass adds successful definitions. Forward references become
8586:: Each pass adds successful definitions. Forward references become
6072−:: available on a later pass; recursive groups and unsupported syntax do
8587+:: available on a later pass; unsupported syntax does not enter the
6073−:: not enter the environment. Generalized definitions are closed, so a
8588+:: environment. Generalized definitions are closed, so a use instantiates
6074−:: use instantiates its variables afresh.
8589+:: its variables afresh.
6076++ global-value-names
8591++ global-value-names
6077 |= ds=(list def)
8592 |= ds=(list def)
@@ -6089,32 +8604,617 @@
6089 ?~ t.hits &
8604 ?~ t.hits &
6092−++ add-supported-defs
8607+:: A top-level gate may refer to itself through one monomorphic placeholder.
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)]
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.
8614+ |= [e=expr name=term]
8616+ ?: ?=(%group -.e) $(e inner.e)
8617+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8619+ ?. ?=(%wing -.head.e) |
8620+ =(names.head.e ~[name])
8623+ |= [e=expr name=term]
8625+ ?: ?=(%group -.e) $(e inner.e)
8626+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8627+ ?. ?=(%branch -.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)
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.
8645+++ recursive-branch-seed
8646+ |= [d=def env=ienv state=istate]
8648+ ?. ?=(%value -.d) ~
8649+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) ~
8654+ %gate-wide body.gate
8657+ =/ base=(unit expr) (branch-base-arm body name.d)
8659+ =/ outer=ienv (skim env |=(entry=[name=term scheme=ischeme] !=(name.entry name.d)))
8660+ =/ sam=isample-result
8662+ %gate (infer-sample sample.gate outer state)
8663+ %gate-wide (infer-sample sample.gate outer state)
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) ~
8676+++ infer-recursive-gate
8677+ |= [d=def env=ienv state=istate]
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)
8684+ =/ sam=isample-result
8686+ %gate (infer-sample sample.gate env state)
8687+ %gate-wide (infer-sample sample.gate env state)
8691+ =/ diag=(unit idiag)
8693+ %gate (sample-import-invalid sample.gate env state)
8694+ %gate-wide (sample-import-invalid sample.gate env state)
8697+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
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]
8707+ %gate-wide body.gate
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)]
8717+ |= names=(list term)
8726+ =/ first=(list term) (dependency-expr i.xs)
8727+ (weld first $(xs t.xs))
8729+++ dependency-pieces
8733+ =/ first=(list term)
8735+ %expr (dependency-expr p.i.xs)
8738+ (weld first $(xs t.xs))
8744+ =/ first=(list term)
8746+ %expr (dependency-expr p.i.xs)
8749+ (weld first $(xs t.xs))
8755+ =/ first=(list term) (dependency-expr val.i.xs)
8756+ (weld first $(xs t.xs))
8762+ =/ first=(list term) (dependency-expr val.i.xs)
8763+ (weld first $(xs t.xs))
8769+ =/ first=(list term) (dependency-expr val.i.xs)
8770+ (weld first $(xs t.xs))
8776+ =/ first=(list term)
8777+ ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
8779+ (weld first $(xs t.xs))
8785+ %str (dependency-pieces pieces.e)
8786+ %qath (dependency-qsegs segs.e)
8787+ %wing (dependency-root names.e)
8789+ =/ first=(list term) (dependency-root target.e)
8790+ =/ last=(list term) (dependency-edits edits.e)
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)
8800+ =/ first=(list term) (dependency-expr head.e)
8801+ =/ last=(list term) (dependency-exprs args.e)
8803+ %cast (dependency-expr val.e)
8805+ =/ first=(list term) (dependency-expr val.e)
8806+ =/ last=(list term) (dependency-expr then.e)
8809+ =/ first=(list term) (dependency-expr subject.e)
8810+ =/ last=(list term) (dependency-arms arms.e)
8813+ =/ first=(list term) (dependency-defs defs.e)
8814+ =/ last=(list term) (dependency-expr final.e)
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)
8825+ |= [ds=(list def) env=ienv state=istate]
8827+ ?~ ds [%& [~ state]]
8829+ ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
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
8836+ %gate (infer-sample sample.gate env initial)
8837+ %gate-wide (infer-sample sample.gate env initial)
8840+ ?: ?=(%| -.sam) [%| [p.sam ~]]
8844+ %gate-wide body.gate
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]]
8855+ |= [entries=(list igate-entry) env=ienv]
6095− ?~ ds env
8857+ ?~ entries env
8858+ [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
8860+++ infer-gate-group-bodies
8861+ |= [entries=(list igate-entry) seeds=ienv state=istate]
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]]
8878+ |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
8879+ ^- (each ienv idiag)
8881+ =/ entry=igate-entry i.entries
8882+ =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
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]]
8899+ |= [ds=(list def) env=ienv state=istate]
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)]]
8924+ |= [ps=(list iwprojection) sub=isub visible=(list @ud)]
8925+ ^- (unit (list iwprojection))
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)
8935+ =/ entry=iwprojection i.ps
8936+ =. entry entry(source src, target dst)
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]
6096 =/ d=def i.ds
8943 =/ d=def i.ds
6097 ?: ?=(%mold -.d) $(ds t.ds)
8944 ?: ?=(%mold -.d) $(ds t.ds)
6098 ?. (unique-value-name name.d globals) $(ds t.ds)
8945 ?. (unique-value-name name.d globals) $(ds t.ds)
6099 ?^ (ienv-lookup name.d env) $(ds t.ds)
8946 ?^ (ienv-lookup name.d env) $(ds t.ds)
8947+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6100− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ |])
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)
6101 ?: ?=(%| -.result) $(ds t.ds)
8952 ?: ?=(%| -.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)
6102 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
8955 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
6103 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
8956 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
6104 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
8957 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
6105 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
8958 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
6106 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8959 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
6107 ?: (gth (lent vars) 26) $(ds t.ds)
8960 ?: (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]
6108 $(ds t.ds, env [[name.d [typ vars]] env])
8966 $(ds t.ds, env [[name.d [typ vars]] env])
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))
8976+ |= [names=(list term) seen=ivisited]
8979+ $(names t.names, seen (~(put by seen) i.names &))
8982+ |= [name=term graph=iadj]
8984+ =/ found=(unit (list term)) (~(get by graph) name)
8988+++ graph-make-forward
8989+ |= [ds=(list def) names=ivisited graph=iadj]
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))
8997+++ graph-add-reverse
8998+ |= [name=term edges=(list term) reverse=iadj]
9001+ =/ prior=(list term) (graph-edges i.edges reverse)
9002+ $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
9005+ |= [names=(list term) graph=iadj reverse=iadj]
9008+ =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
9012+ |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
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]))
9023+ |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
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])
9030+++ graph-collect-all
9031+ |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
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])
9038+:: Two depth-first passes find components before group inference. Maps
9039+:: preserve the graph identity; duplicate global names fail closed.
9041+ |= [ds=(list def) names=(list term)]
9043+ =/ nameset=ivisited ~
9044+ =/ pending=(list term) names
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 ~)
9055+ |= [component=(list term) graph=iadj]
9059+ (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
9062+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
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)
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))
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)]
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))
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)
6110++ resolve-supported-defs
9097++ 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)]
6113− =/ env=ienv ~
9100+ env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
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]
9108+ |= [xs=(list expr) globals=(list term) locals=(list term)]
9109+ ^- (unit (list icyclesite))
9111+ =/ first=(unit (list icyclesite)) (cycle-sites i.xs globals locals)
9113+ =/ tail=(unit (list icyclesite)) $(xs t.xs)
9115+ `(weld u.first u.tail)
9117+++ cycle-sample-name
9118+ |= [sam=sample globals=(list term) locals=(list term)]
9119+ ^- (unit (unit term))
9122+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9125+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9132+ |= [e=expr globals=(list term) locals=(list term)]
9133+ ^- (unit (list icyclesite))
9136+ ?. ?=([@ ~] names.e) ~
9137+ `~[[i.names.e at.e]]
9140+ ?: (lien pieces.e |=(p=piece ?=(%expr -.p))) ~
9142+ %group $(e inner.e)
9143+ %body ?~(defs.e $(e final.e) ~)
9146+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9148+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9149+ $(e body.e, locals nested)
9151+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9153+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9154+ $(e body.e, locals nested)
9156+ =/ first=(unit (list icyclesite)) $(e head.e)
9158+ =/ tail=(unit (list icyclesite)) (cycle-sites-list args.e globals locals)
9160+ `(weld u.first u.tail)
9164+++ cycle-definitely-atom
9167+ ?: ?=(%group -.e) $(e inner.e)
9168+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9170+ |(?=(%aura -.shape.e) ?=(%flag -.shape.e))
9172+++ cycle-proof-group
9173+ |= [members=(list def) globals=(list term)]
9176+ ?. ?=(%value -.i.members) |
9177+ ?. (unique-value-name name.i.members globals) |
9178+ ?. ?=(^ (cycle-sites val.i.members globals ~)) |
9179+ $(members t.members)
9182+ |= [sites=(list icyclesite) component=(list term)]
9185+ ?: (lien component |=(n=term =(n name.i.sites))) `at.i.sites
9188+++ cycle-group-errors
9189+ |= [members=(list def) component=(list term) globals=(list term)]
9194+ =/ tail=(list icycle) $(members t.members)
9195+ ?. (cycle-definitely-atom val.d) tail
9196+ =/ sites=(unit (list icyclesite)) (cycle-sites val.d globals ~)
9198+ =/ found=(unit span) (cycle-find-site u.sites component)
9200+ [[name.d at.d u.found] tail]
9202+++ definite-value-cycles
9203+ |= [ds=(list def) globals=(list term)]
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) ~
6115− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds)
9210+ ?~ components out
6116− ?: =(next env) env
9211+ =/ component=(list term) i.components
6117− $(env next)
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))
6119+| %union-analysis
9219+| %union-analysis
@@ -6251,11 +9351,142 @@
6251 [at.first at.second (union-relate a (project-union-mold second molds ~))]
9351 [at.first at.second (union-relate a (project-union-mold second molds ~))]
6252 (weld pairs $(cases t.cases))
9352 (weld pairs $(cases t.cases))
9354+:: A closed structural mold supplies no equation to determine a hole.
9355+:: Applications, references, unbound capitals and unions are unproved.
9358+ ^- (unit (unit span))
9359+ ?: ?=(%generic -.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))
9369+ ?(%aura %noun %void %flag %const) `~
9370+ %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
9371+ %cell (simple-mold-field-holes fields.sh vars)
9373+ =/ a=(unit (unit span)) $(sh sample.sh)
9375+ =/ b=(unit (unit span)) $(sh product.sh)
9381+++ simple-mold-field-holes
9382+ |= [fields=(list field) vars=(list @t)]
9383+ ^- (unit (unit span))
9385+ =/ f=field i.fields
9386+ =/ first=(unit (unit span))
9388+ %face (simple-mold-hole-in shape.f vars)
9389+ %bare (simple-mold-hole-in shape.f vars)
9393+ =/ rest=(unit (unit span)) $(fields t.fields)
9395+ `?~(u.first u.rest u.first)
9396+++ simple-local-mold-hole
9400+ ?. ?=(%mold -.i.defs) $(defs t.defs)
9401+ =/ found=(unit (unit span)) (simple-mold-hole shape.i.defs)
9402+ ?~ found $(defs t.defs)
9406+:: A partial prelude may omit unsupported declarations, but may not
9407+:: publish an interface while a named mold's hole remains unchecked.
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)
9425+ %face (shape-has-hole shape.f)
9426+ %bare (shape-has-hole shape.f)
9429+++ named-mold-has-hole
9433+ ?: &(?=(%mold -.i.ds) (shape-has-hole shape.i.ds)) &
9440+ %face (shape-has-hole shape.sam)
9441+ %bare (shape-has-hole shape.sam)
9442+ %cell (lien items.sam sample-has-hole)
9449+ %mold (shape-has-hole shape.d)
9450+ %value (expr-has-hole val.d)
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)))
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))
9472+++ hole-values-present
9473+ |= [ds=(list def) env=ienv]
9476+ ?. ?=(%value -.i.ds) $(ds t.ds)
9477+ ?: (expr-has-hole val.i.ds)
9478+ ?. ?=(^ (ienv-lookup name.i.ds env)) |
6254++ show-partial-mold
9481++ show-partial-mold
6255 |= [file=path src=@t d=def molds=imolds]
9482 |= [file=path src=@t d=def molds=imolds]
6257 ?> ?=(%mold -.d)
9484 ?> ?=(%mold -.d)
6258 =/ sh=shape shape.d
9485 =/ 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])
6259 =? sh ?=(%generic -.sh) body.sh
9490 =? sh ?=(%generic -.sh) body.sh
6260 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
9491 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
6261 =/ pairs=(list upair) (union-pairs cases.sh molds)
9492 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -6282,6 +9513,21 @@
6282 (show-error src [file line.beg.at.site col.beg.at.site note.site])
9513 (show-error src [file line.beg.at.site col.beg.at.site note.site])
6283 (of-wain:format [summary excerpts])
9514 (of-wain:format [summary excerpts])
9516+:: Both written field sites are shown in the source that declares them.
9517+++ show-duplicate-fields
9518+ |= [file=path src=@t diagnostic=idiag]
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])
9526+++ duplicate-fields-report
9527+ |= [file=path src=@t diagnostic=idiag]
9529+ (of-wain:format ~['partial inference; module not checked' (show-duplicate-fields file src diagnostic)])
6285:: +golden-types: a partial report; it does not claim the module checks
9531:: +golden-types: a partial report; it does not claim the module checks
6287++ golden-types
9533++ golden-types
@@ -6311,6 +9557,180 @@
6311+$ jfile-result (each [iface=ifile cache=jcache] @t)
9557+$ jfile-result (each [iface=ifile cache=jcache] @t)
6312+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
9558+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
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]
9565+ =/ prior=(unit span) (~(get by seen) name)
9567+ `["record field `{(trip name)}` is repeated" ~[[u.prior "first field"] [at "repeated field"]]]
9572+ =/ first (duplicate-shape i.xs)
9576+ |= [fields=(list field) seen=written-fields]
9579+ =/ f=field i.fields
9586+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.f seen))
9588+ =/ inner=(unit idiag)
9590+ %face (duplicate-shape shape.f)
9592+ %bare (duplicate-shape shape.f)
9595+ $(fields t.fields, seen ?~(n seen (~(put by seen) u.n at.f)))
9600+ %cell (duplicate-fields fields.s ~)
9601+ %apply (duplicate-shapes args.s)
9602+ %union (duplicate-shapes cases.s)
9604+ =/ left (duplicate-shape sample.s)
9606+ (duplicate-shape product.s)
9607+ %generic (duplicate-shape body.s)
9610+++ duplicate-samples
9611+ |= [items=(list sample) seen=written-fields]
9614+ =/ a=sample i.items
9622+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.a seen))
9624+ =/ inner (duplicate-sample a)
9626+ $(items t.items, seen ?~(n seen (~(put by seen) u.n at.a)))
9631+ %cell (duplicate-samples items.s ~)
9632+ %face (duplicate-shape shape.s)
9633+ %bare (duplicate-shape shape.s)
9640+ =/ first (duplicate-expr i.xs)
9644+ |= [items=(list item) seen=written-fields]
9648+ =/ dup=(unit idiag) ?~(face.a ~ (duplicate-written-field u.face.a at.a seen))
9650+ =/ inner (duplicate-expr val.a)
9652+ $(items t.items, seen ?~(face.a seen (~(put by seen) u.face.a at.a)))
9654+ |= pieces=(list piece)
9657+ =/ first=(unit idiag) ?:(?=(%expr -.i.pieces) (duplicate-expr p.i.pieces) ~)
9661+ |= segs=(list qseg)
9664+ =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
9668+ |= edits=(list edit)
9671+ =/ first (duplicate-expr val.i.edits)
9678+ =/ first (duplicate-expr val.i.arms)
9685+ =/ first=(unit idiag)
9687+ %mold (duplicate-shape shape.i.defs)
9688+ %value (duplicate-expr val.i.defs)
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 ~)
9705+ =/ first (duplicate-sample sample.e)
9707+ (duplicate-expr body.e)
9709+ =/ first (duplicate-sample sample.e)
9711+ (duplicate-expr body.e)
9713+ =/ first (duplicate-shape shape.e)
9715+ (duplicate-expr val.e)
9717+ =/ first (duplicate-expr head.e)
9719+ (duplicate-exprs args.e)
9721+ =/ first (duplicate-expr val.e)
9723+ (duplicate-expr then.e)
9725+ =/ first (duplicate-expr subject.e)
9727+ (duplicate-arms arms.e)
9729+ =/ first (duplicate-defs defs.e)
9731+ (duplicate-expr final.e)
6314++ import-binding-names
9734++ import-binding-names
6315 |= imports=(list import)
9735 |= imports=(list import)
6316 ^- (list term)
9736 ^- (list term)
@@ -6323,6 +9743,60 @@
6324 [n $(imports t.imports)]
9744 [n $(imports t.imports)]
9746+++ reserved-proj-sample
9750+ %bind =(name.sam %proj)
9751+ %face =(name.sam %proj)
9752+ %pun =(name.sam %proj)
9753+ %cell (lien items.sam reserved-proj-sample)
9756+++ reserved-proj-pattern
9760+ %bind =(name.p %proj)
9761+ %cell (lien items.p reserved-proj-pattern)
9764+++ reserved-proj-def
9767+ ?: =(name.d %proj) &
9768+ ?: ?=(%value -.d) (reserved-proj-expr val.d)
9770+++ reserved-proj-expr
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)))
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))
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))
9791+++ module-has-reserved-proj
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))
6326++ module-scope-valid
9800++ module-scope-valid
6327 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
9801 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -6330,6 +9804,7 @@
6330 =/ vals=(list term) (global-value-names defs.mod)
9804 =/ vals=(list term) (global-value-names defs.mod)
6331 =/ molds=imolds (collect-simple-molds defs.mod)
9805 =/ molds=imolds (collect-simple-molds defs.mod)
6332 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9806 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9807+ ?: (module-has-reserved-proj mod) |
6333 ?. %+ levy imported
9808 ?. %+ levy imported
6334 |= n=term
9809 |= n=term
6335 &((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))))
9810 &((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 @@
6337 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
9812 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
6338 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
9813 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
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)]
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))))
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)
6340++ module-mold-types
9831++ module-mold-types
6341 |= [molds=imolds state=istate]
9832 |= [molds=imolds state=istate]
6342 ^- (each imold-types @t)
9833 ^- (each imold-types @t)
@@ -6345,10 +9836,205 @@
6345 =/ t=(unit [template=ischeme state=istate])
9836 =/ t=(unit [template=ischeme state=istate])
6346 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
9837 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
6347 ?~ t [%| 'module mold needs unsupported inference']
9838 ?~ t [%| 'module mold needs unsupported inference']
9839+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
6348 =/ rest=(each imold-types @t) $(molds t.molds)
9840 =/ rest=(each imold-types @t) $(molds t.molds)
6349 ?: ?=(%| -.rest) rest
9841 ?: ?=(%| -.rest) rest
6350 [%& [[name.m template.u.t] p.rest]]
9842 [%& [[name.m template.u.t] p.rest]]
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.
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.
9855+++ standard-prelude-list
9858+ ?. ?=(%generic -.sh) |
9861+ =/ var=@t i.vars.sh
9862+ ?. ?=(%union -.body.sh) |
9863+ =/ cs=(list shape) cases.body.sh
9867+ ?. ?=(%const -.i.cs) |
9868+ ?. =(%null form.lit.i.cs) |
9869+ ?. ?=(%cell -.i.t.cs) |
9870+ =/ fs=(list field) fields.i.t.cs
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) |
9885+ ?. ?=(%tvar -.i.args.tail) |
9886+ =(var name.i.args.tail)
9889+ |= [typ=itype name=term]
9891+ ?: ?=(%jrec -.typ) typ(label `name)
9892+ ?. ?=(%union -.typ) typ
9896+++ partial-prelude-molds
9897+ |= [molds=imolds state=istate]
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)]
9911+:: A compiler-owned interface available only to the dedicated
9912+:: internal-prelude preparation path, never the ordinary module resolver.
9913+++ private-primitive-interface
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 ~ ~ ~ ~]
9920+++ infer-private-internal
9923+ =/ at=path /lib/jibb/internal/jibb
9924+ =/ parsed (parse at src)
9925+ ?: ?=(%| -.parsed) ~
9926+ =/ mod=module p.parsed
9927+ ?^ (duplicate-defs defs.mod) ~
9929+ =/ built=jfile-result (infer-jibb-file at src ~ ~ ~ ~[at] ~ ~ ~ ~)
9930+ ?: ?=(%| -.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)
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]
9950+++ partial-prelude-interface-with-internal
9951+ |= [src=@t internal-source=(unit @t)]
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)
9966+ `~[[face.i.imports.p.parsed u.built]]
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)
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.
9995+ |= m=[name=term body=shape]
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)
10006+ ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
10007+ `[env mt at ~ artifacts.resolution deps `src]
10009+++ partial-prelude-interface
10012+ (partial-prelude-interface-with-internal src ~)
10014++$ iprelude [iface=ifile values=(list term) molds=(list term)]
10018+ ^- (unit iprelude)
10019+ =/ iface=(unit ifile) (partial-prelude-interface src)
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]
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)
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]
6352++ module-values-complete
10038++ module-values-complete
6353 |= [ds=(list def) env=ienv]
10039 |= [ds=(list def) env=ienv]
@@ -6370,11 +10056,15 @@
6370 $(cache t.cache)
10056 $(cache t.cache)
6372++ resolve-jibb-imports
10058++ 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)]
6374 ^- jimports-result
10060 ^- jimports-result
6375 ?~ imports [%& [~ cache]]
10061 ?~ imports [%& [~ cache]]
6376 ?. ?=(%jibb -.i.imports) $(imports t.imports)
10062 ?. ?=(%jibb -.i.imports) $(imports t.imports)
6377 =/ at=path (weld path.i.imports `path`~[%jibb])
10063 =/ 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']
6378 ?: (lien active |=(p=path =(p at)))
10068 ?: (lien active |=(p=path =(p at)))
6379 [%| (crip "import cycle at {(spud at)}")]
10069 [%| (crip "import cycle at {(spud at)}")]
6380 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
10070 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -6383,37 +10073,313 @@
6383 =/ cached=(unit ifile) (find-jibb-cache at cache)
10073 =/ cached=(unit ifile) (find-jibb-cache at cache)
6384 =/ iface=jfile-result
10074 =/ iface=jfile-result
6385 ?^ cached [%& [u.cached cache]]
10075 ?^ 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)
6387 ?: ?=(%| -.iface) [%| p.iface]
10077 ?: ?=(%| -.iface) [%| p.iface]
6388 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
10078 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
6389 ?: ?=(%| -.rest) rest
10079 ?: ?=(%| -.rest) rest
6390 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
10080 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
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))]
10086+ |= [sh=shape marks=(list term)]
10088+ ?. ?=(%ref -.sh) ~
10089+ ?. ?=([@ ~] names.sh) ~
10090+ ?. (unique-value-name i.names.sh marks) ~
10094+ |= [shapes=(list shape) marks=(list term) used=(list term)]
10095+ ^- (unit (list term))
10097+ =/ n=(unit term) (api-path-mark i.shapes marks)
10099+ ?: (lien used |=(x=term =(x u.n))) ~
10100+ =/ rest=(unit (list term)) $(shapes t.shapes, used [u.n used])
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) ~
10113+ =/ full=(unit term) (api-path-mark i.args.sh marks)
10115+ =/ diffs=(unit (list term)) (api-path-diffs t.args.sh marks ~[u.full])
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))
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])
10131+ `[[name.seg aura.seg at.seg] u.rest]
10133+++ api-scry-parameters-compatible
10134+ |= [scry=(list iapi-parameter) watch=(list iapi-parameter)]
10137+ ?. (lien watch |=(p=iapi-parameter &(=(name.p name.i.scry) =(aura.p aura.i.scry)))) |
10141+ |= [sh=shape marks=(list term)]
10142+ ^- (unit iapi-path)
10143+ ?. ?=(%cell -.sh) ~
10144+ =/ fs=(list field) fields.sh
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)
10161+ =/ scry=(unit (unit (list pseg)))
10163+ =/ entry=field i.t.t.t.fs
10164+ ?. ?=(%face -.entry) ~
10165+ ?. =(%scry name.entry) ~
10166+ ?. ?=(%path -.shape.entry) ~
10167+ ``segs.shape.entry
10169+ =/ params=(unit (list iapi-parameter)) (api-path-parameters segs.path-shape ~)
10172+ =/ scry-params=(unit (list iapi-parameter)) (api-path-parameters u.u.scry ~)
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]
10179+ |= [shapes=(list shape) marks=(list term) seen=(list term)]
10180+ ^- (unit (list iapi-path))
10182+ =/ one=(unit iapi-path) (api-path-one i.shapes marks)
10184+ ?: (lien seen |=(n=term =(n name.u.one))) ~
10185+ =/ rest=(unit (list iapi-path)) $(shapes t.shapes, seen [name.u.one seen])
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 ~)
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)
10202+ %mark $(imports t.imports)
10203+ %sur [name.i.imports $(imports t.imports)]
10204+ %jibb [face.i.imports $(imports t.imports)]
10207+++ api-derived-names-valid
10208+ |= [paths=(list iapi-path) poke-names=(list term) mod=module prelude-values=(list term)]
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))))))
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)]
10221+ |= [names=(list term) externals=imark-externals declared=(list term)]
10222+ ^- (unit (list iapi-mark-type))
10224+ =/ typ=(unit itype) (find-imported-mark i.names externals declared)
10226+ =/ tail=(unit (list iapi-mark-type)) $(names t.names)
10228+ `[[i.names u.typ] u.tail]
10231+ |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
10232+ ^- (unit (list iapi-path-typed))
10234+ =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
10236+ =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
10238+ =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
10240+ `[[i.paths u.full u.diffs] u.tail]
10242+++ api-poke-mark-names
10243+ |= [pokes=(list def) declared=(list term)]
10244+ ^- (unit (list term))
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)
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)
10273+ =/ decl=def i.declarations
10274+ ?> ?=(%mold -.decl)
10275+ =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
10277+ ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
10278+ (api-path-types u.paths externals declared)
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']
10301+++ api-mark-exports
10302+ |= [marks=(list term) all=(list term) externals=imark-externals]
10305+ =/ t=(unit itype) (find-imported-mark i.marks externals all)
10306+ ?~ t $(marks t.marks)
10307+ [[i.marks [u.t ~]] $(marks t.marks)]
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)]
10314+ ?: (lien defs.mod def-has-hole) ~
10315+ ?. ?=([%ui %api @ %jibb ~] at) ~
10316+ ?^ (duplicate-defs defs.mod) ~
10318+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
10319+ =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
10321+ ?. ?=(%union -.typ.u.poke) ~
10324+ %+ lien cases.typ.u.poke
10326+ ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
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)
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]] ~ ~ ~]
6392++ infer-jibb-file
10346++ 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)]
6394 ^- jfile-result
10348 ^- jfile-result
6395− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
6396 =/ parsed (parse at src)
10349 =/ parsed (parse at src)
6397 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
10350 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
6398 =/ mod=module p.parsed
10351 =/ mod=module p.parsed
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]]]
6399− ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
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)}")]
6400 =/ vals=(list term) (global-value-names defs.mod)
10363 =/ vals=(list term) (global-value-names defs.mod)
6401 ?: (lien vals |=(n=term =(n %main)))
10364 ?: (lien vals |=(n=term =(n %main)))
6402 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
10365 [%| (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)
6404 ?: ?=(%| -.js) [%| p.js]
10367 ?: ?=(%| -.js) [%| p.js]
6405 =/ molds=imolds (collect-simple-molds defs.mod)
10368 =/ molds=imolds (collect-simple-molds defs.mod)
6406 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
10369 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
6407 =/ surs=(list term) (collect-sur-imports imports.mod)
10370 =/ surs=(list term) (collect-sur-imports imports.mod)
6408 =/ marks=(list term) (collect-mark-imports imports.mod)
10371 =/ marks=(list term) (collect-mark-imports imports.mod)
6409 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
10372 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
10373+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6410− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ |]
10374+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
6411 =/ mts=(each imold-types @t) (module-mold-types molds state)
10375 =/ mts=(each imold-types @t) (module-mold-types molds state)
6412 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
10376 ?: ?=(%| -.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
6414 ?. (module-values-complete defs.mod env)
10379 ?. (module-values-complete defs.mod env)
6415 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
10380 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
10381+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src]
6416− [%& [[env p.mts] [[at [env p.mts]] cache.p.js]]]
10382+ [%& [iface [[at iface] cache.p.js]]]
6418:: +golden-types-with-modules fails closed for imports without prelude
10384:: +golden-types-with-modules fails closed for imports without prelude
6419:: scope. +golden-types-with-prelude resolves supported library graphs;
10385:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -6424,54 +10390,103 @@
6425 =/ parsed (parse file src)
10391 =/ parsed (parse file src)
6426 ?: ?=(%| -.parsed) (show-error src p.parsed)
10392 ?: ?=(%| -.parsed) (show-error src p.parsed)
10393+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10394+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
6427 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
10395 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
6428 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
10396 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
6429 (golden-types-with-marks file src externals mark-externals)
10397 (golden-types-with-marks file src externals mark-externals)
6431−:: The caller supplies the actual prelude source. Its current names are
10399+:: The caller supplies the actual prelude source. Its declared names are
6432−:: reserved, but its incomplete inventory and types are not checked here.
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.
6434++ golden-types-with-prelude
10404++ golden-types-with-prelude
6435 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
10405 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
6437 =/ parsed (parse file src)
10407 =/ parsed (parse file src)
6438 ?: ?=(%| -.parsed) (show-error src p.parsed)
10408 ?: ?=(%| -.parsed) (show-error src p.parsed)
10409+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10410+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
6439 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
10411 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
6440 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
10412 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
6441 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
10413 ?: ?=(%| -.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)
10414+ =/ prepared=(unit iprelude) (prepare-prelude prelude-source)
6443− =/ prelude-molds=(list term)
10415+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
6444− (turn (collect-simple-molds defs.p.prelude) |=(m=[name=term body=shape] name.m))
10416+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
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]
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)
10424+++ golden-types-with-prepared-prelude
10425+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
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
6445 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
10435 ?. (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'
6446 'partial inference; module not checked\0amodule has conflicting names'
10438 'partial inference; module not checked\0amodule has conflicting names'
6447 =/ js=jimports-result
10439 =/ 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)
6449 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
10441 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
6450 =/ scope-values=(list term)
10442 =/ scope-values=(list term)
6451 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
10443 (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)
6454:: +golden-types-with-marks: supply declared mark types separately from /sur
10446:: +golden-types-with-marks: supply declared mark types separately from /sur
6455:: entries, as [mark result] with the result from +read-mark:jibb-import.
10447:: entries, as [mark result] with the result from +read-mark:jibb-import.
6456:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
10448:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
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
10455+ ?: ?=([%ok *] result) [%& +.result]
10458+++ golden-types-with-reader-diagnostics
10459+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
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)
6458++ golden-types-with-marks
10467++ golden-types-with-marks
6459 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
10468 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
6461− (golden-types-in-context file src externals mark-externals ~ ~ ~)
10470+ (golden-types-in-context file src externals mark-externals ~ ~ ~ ~)
6463++ golden-types-in-context
10472++ 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)]
6466 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
10475 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
6467 =/ parsed (parse file src)
10476 =/ parsed (parse file src)
6468 ?: ?=(%| -.parsed) (show-error src p.parsed)
10477 ?: ?=(%| -.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'
6469 =/ ds=(list def) defs.p.parsed
10482 =/ ds=(list def) defs.p.parsed
6470 =/ molds=imolds (collect-simple-molds ds)
10483 =/ molds=imolds (collect-simple-molds ds)
6471 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
10484 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
6472 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
10485 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
6473 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
10486 =/ 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
6475 =/ lines=(list @t) ~
10490 =/ lines=(list @t) ~
6477 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
10492 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -6480,21 +10495,53 @@
6480 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
10495 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
6481 ?. (unique-value-name name.d globals)
10496 ?. (unique-value-name name.d globals)
6482 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
10497 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
10498+ =/ cycle=(list icycle) (skim cycles |=(c=icycle =(name.c name.d)))
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))
6483− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ |])
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)
10512+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
10513+ (infer-recursive-gate d env initial)
10514+ (infer-fragment val.d env initial)
6484 ?: ?=(%| -.result)
10515 ?: ?=(%| -.result)
6485 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
10516 $(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)
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)
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])
6486 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
10527 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
6487 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
10528 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
6488 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10529 =/ 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])
6489 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
10532 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
6490 $(ds t.ds, lines [(crip "++ {(trip name.d)}: tag needs context in partial inference") lines])
10533 $(ds t.ds, lines [(crip "++ {(trip name.d)}: tag needs context in partial inference") lines])
6491− ?: (itype-has-union typ)
10534+ ?: (itype-has-hidden-recursive typ)
6492− $(ds t.ds, lines [(crip "++ {(trip name.d)}: union type printing is not supported by partial inference") lines])
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])
6493 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
10538 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
6494 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
10539 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
6495 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10540 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
6496 ?: (gth (lent vars) 26)
10541 ?: (gth (lent vars) 26)
6497 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
10542 $(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])
6498 =/ printable=itype (canonical-itype typ vars)
10545 =/ printable=itype (canonical-itype typ vars)
6499 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
10546 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
6500 $(ds t.ds, lines [line lines])
10547 $(ds t.ds, lines [line lines])