@@ -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
@@ -4600,11 +4614,53 @@
4600:: from their display name. Generic cases must be disjoint for all arguments.
4614:: from their display name. Generic cases must be disjoint for all arguments.
4601:: Unnamed union printing is informational; it is not Jibb syntax.
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, nested projected 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.
4631+:: Supported API imports derive request-gate types atomically for multiple
4632+:: paths, including one typed segment or one diff fold per case. Their checked
4633+:: ordinary definitions, mark molds and supported poke constructor are also
4634+:: exported. A selected /sur mold is checked through its trusted reader result;
4635+:: unused cores and other bindings are not independently validated. APIs
4636+:: with /= imports, separate scry paths, multiple parameters or diffs, or a
4637+:: parameter together with a fold remain unsupported. The unchanged todo API
4638+:: fits this fragment, including named closed fold gates.
4640+:: Each case's source-derived schema and canonical API identity travel in a
4641+:: dependency closure bound to the exact supplied bundle, prelude, scope and
4642+:: trusted reader results. Unknown cached entries are rebuilt. Request-bearing
4643+:: closures are limited to 256 source paths and requests. This is type
4644+:: inference only: no request lowering, runtime schema validator or proof that
4645+:: an arbitrary ask value is watchable is supplied.
4647+:: A closed gate sample may omit one outer face from a known input slot when
4648+:: its product is identical. Distinct written names, nested value faces,
4649+:: ambiguous cell tails and raw-variable-origin fits retain their prior rules.
4651+:: In one synthetic eval of a 48-module deep and 48-module wide request-free
4652+:: graph, baseline versus certificate inference took 21.53 s versus 23.10 s
4653+:: elapsed (21.10 s versus 22.34 s CPU), including startup. The deep cache's
4654+:: jam grew from 2,402 to 4,209 bytes (+1,807 bytes). These single-run figures
4655+:: are not production memory or performance benchmarks.
4604 $~ [%var 0]
4658 $~ [%var 0]
4605 $% [%var id=@ud]
4659 $% [%var id=@ud]
4606 [%avar id=@ud]
4660 [%avar id=@ud]
4607 [%nvar id=@ud]
4662 [%nvar id=@ud]
4608 [%atom aura=@ta]
4664 [%atom aura=@ta]
4609 [%any-atom ~]
4665 [%any-atom ~]
4610 [%flag ~]
4666 [%flag ~]
@@ -4613,6 +4669,7 @@
4613 [%const literal=lit]
4669 [%const literal=lit]
4614 [%collection name=term args=(list itype)]
4670 [%collection name=term args=(list itype)]
4615 [%recursive module=term name=term label=(unit @t)]
4671 [%recursive module=term name=term label=(unit @t)]
4672+ [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
4616 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4673 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4617 [%face name=term body=itype]
4674 [%face name=term body=itype]
4618 [%fn sample=itype product=itype]
4675 [%fn sample=itype product=itype]
@@ -4636,18 +4693,32 @@
4637 =/ found=(unit itype) (itype-lookup id.t sub)
4694 =/ found=(unit itype) (itype-lookup id.t sub)
4638 ?~ found t
4695 ?~ found t
4696+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4639 $(t u.found)
4697 $(t u.found)
4641 =/ found=(unit itype) (itype-lookup id.t sub)
4699 =/ found=(unit itype) (itype-lookup id.t sub)
4642 ?~ found t
4700 ?~ found t
4701+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4704+ =/ found=(unit itype) (itype-lookup id.t sub)
4706+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4643 $(t u.found)
4707 $(t u.found)
4645 =/ found=(unit itype) (itype-lookup id.t sub)
4709 =/ found=(unit itype) (itype-lookup id.t sub)
4646 ?~ found t
4710 ?~ found t
4711+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4714+ =/ found=(unit itype) (itype-lookup id.t sub)
4716+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4647 $(t u.found)
4717 $(t u.found)
4649 =/ found=(unit itype) (itype-lookup id.t sub)
4719 =/ found=(unit itype) (itype-lookup id.t sub)
4650 ?~ found t
4720 ?~ found t
4721+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4651 $(t u.found)
4722 $(t u.found)
@@ -4658,7 +4729,9 @@
4659 %var =(n id.t)
4730 %var =(n id.t)
4660 %avar =(n id.t)
4731 %avar =(n id.t)
4661 %nvar =(n id.t)
4733 %nvar =(n id.t)
4663 %any-atom |
4736 %any-atom |
@@ -4667,6 +4740,7 @@
4667 %const |
4740 %const |
4668 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4741 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4669 %recursive |
4742 %recursive |
4670 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4744 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4671 %face $(t body.t)
4745 %face $(t body.t)
4672 %fn |($(t sample.t) $(t product.t))
4746 %fn |($(t sample.t) $(t product.t))
@@ -4685,6 +4759,8 @@
4685 =. a (itype-walk a sub)
4759 =. a (itype-walk a sub)
4686 =. b (itype-walk b sub)
4760 =. b (itype-walk b sub)
4687 ?: =(a b) `sub
4761 ?: =(a b) `sub
4762+ ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4763+ ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
4688 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4764 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4689 ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
4765 ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
4690 ?: &(?=(%union -.a) ?=(%union -.b))
4766 ?: &(?=(%union -.a) ?=(%union -.b))
@@ -4701,6 +4777,32 @@
4701 ?: ?=(%var -.b)
4777 ?: ?=(%var -.b)
4702 ?: (itype-occurs id.b a sub) ~
4778 ?: (itype-occurs id.b a sub) ~
4703 `[[id.b a] sub]
4779 `[[id.b a] sub]
4780+ :: Arithmetic's aura variable excludes loobeans; decimal literals
4781+ :: remain defaultable until a later constraint makes them concrete.
4782+ ?: &(?=(%nvar -.a) ?=(%rvar -.b))
4783+ `[[id.b [%rnvar id.a]] [id.a [%rnvar id.a]] sub]
4784+ ?: &(?=(%rvar -.a) ?=(%nvar -.b))
4785+ `[[id.a [%rnvar id.b]] [id.b [%rnvar id.b]] sub]
4786+ ?: &(?=(%rnvar -.a) ?=(%rvar -.b)) `[[id.b a] sub]
4787+ ?: &(?=(%rvar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4788+ ?: &(?=(%rnvar -.a) ?=(%nvar -.b)) `[[id.b a] sub]
4789+ ?: &(?=(%nvar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4790+ ?: &(?=(%rnvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4791+ ?: &(?=(%avar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4793+ ?. |(?=(%rnvar -.b) ?=(%atom -.b)) ~
4798+ ?: &(?=(%avar -.a) ?=(%rvar -.b)) `[[id.a b] sub]
4799+ ?: &(?=(%rvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4801+ ?. |(?=(%rvar -.b) ?=(%atom -.b)) ~
4704 :: The narrower decimal constraint survives a match with an atom
4806 :: The narrower decimal constraint survives a match with an atom
4705 :: variable; decimal syntax alone does not make it a loobean.
4807 :: variable; decimal syntax alone does not make it a loobean.
4706 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4808 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
@@ -4755,7 +4857,9 @@
4760 %any-atom &
4864 %any-atom &
@@ -4764,6 +4868,7 @@
4764 %const |
4868 %const |
4765 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4869 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4766 %recursive |
4870 %recursive |
4767 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4872 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4768 %face $(t body.t)
4873 %face $(t body.t)
4769 %fn |($(t sample.t) $(t product.t))
4874 %fn |($(t sample.t) $(t product.t))
@@ -4826,7 +4931,9 @@
4826 ?- -.typ
4931 ?- -.typ
4831 %any-atom &
4938 %any-atom &
@@ -4835,6 +4942,7 @@
4835 %const &
4942 %const &
4836 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4943 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4837 %recursive |
4944 %recursive |
4838 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4946 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4839 %face $(typ body.typ)
4947 %face $(typ body.typ)
4840 %fn |($(typ sample.typ) $(typ product.typ))
4948 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4870,6 +4978,42 @@
4981+:: Closed function samples may omit a slot face, but a known name must
4982+:: match another known name. Keep nested value faces and require exact
4983+:: invariant compatibility; a faced tail against a cell is ambiguous.
4984+++ itype-closed-slot-match
4985+ |= [a=itype b=itype]
4987+ ?: &(?=(%face -.a) ?=(%face -.b))
4988+ ?. =(name.a name.b) |
4989+ ?=(^ (itype-unify body.a body.b ~))
4990+ ?: ?=(%face -.a) ?=(^ (itype-unify body.a b ~))
4991+ ?: ?=(%face -.b) ?=(^ (itype-unify a body.b ~))
4992+ ?=(^ (itype-unify a b ~))
4993+++ itype-closed-sample-match
4994+ |= [a=itype b=itype fuel=@ud]
4997+ ?. &(?=(%cell -.a) ?=(%cell -.b)) |
4998+ ?. (itype-closed-slot-match hed.a hed.b) |
5001+ ?: &(?=(%cell -.x) ?=(%cell -.y))
5002+ ?=(^ (itype-unify x y ~))
5003+ ?: |(&(?=(%face -.x) ?=(%cell -.y)) &(?=(%cell -.x) ?=(%face -.y))) |
5004+ (itype-closed-slot-match x y)
5005+++ itype-closed-gates-match
5006+ |= [a=itype b=itype]
5008+ ?. &(?=(%fn -.a) ?=(%fn -.b)) |
5009+ ?. &(?=(%cell -.sample.a) ?=(%cell -.sample.b)) |
5010+ ?. =(product.a product.b) |
5011+ ?^ (itype-vars a) |
5012+ ?^ (itype-vars b) |
5013+ ?: |((itype-has-tag a) (itype-has-tag b)) |
5014+ ?. (itype-closed-sample-match sample.a sample.b 1.024) |
5015+ ?=(^ (itype-unify product.a product.b ~))
4873++ itype-face-asym-collection-args
5017++ itype-face-asym-collection-args
4874 |= [as=(list itype) bs=(list itype) sub=isub]
5018 |= [as=(list itype) bs=(list itype) sub=isub]
@@ -4887,8 +5031,8 @@
4887 ?. =(name.a name.b) |
5031 ?. =(name.a name.b) |
4888 (itype-face-asym-collection-args args.a args.b sub)
5032 (itype-face-asym-collection-args args.a args.b sub)
4889 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
5033 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4890− ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
5034+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%rvar -.b) |(?=(%nvar -.b) ?=(%rnvar -.b)))
4891− ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
5035+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%rvar -.a) |(?=(%nvar -.a) ?=(%rnvar -.a)))
4892 ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
5036 ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4893 ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
5037 ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
@@ -4911,6 +5055,30 @@
4911 [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
5055 [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
4912 expected
5056 expected
5058+:: Positional call arguments do not write the sample's enclosing field
5059+:: labels. Ignore one raw sample-slot face per written argument while
5060+:: checking value faces as usual. An unknown or variable-bound cell spine
5061+:: cannot justify this distinction, so keep the existing conservative guard.
5062+++ itype-positional-slot-face-asym
5063+ |= [actual=itype expected=itype sub=isub]
5065+ ?: &(?=(%fn -.actual) ?=(%fn -.expected) (itype-closed-gates-match actual expected)) |
5066+ (itype-face-asym actual expected sub)
5068+++ itype-positional-face-asym
5069+ |= [args=(list expr) actual=itype expected=itype sub=isub]
5073+ =/ slot=itype expected
5074+ =? slot ?=(%face -.slot) body.slot
5075+ (itype-positional-slot-face-asym actual slot sub)
5076+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) &
5077+ =/ slot=itype hed.expected
5078+ =? slot ?=(%face -.slot) body.slot
5079+ ?: (itype-positional-slot-face-asym hed.actual slot sub) &
5080+ $(args t.args, actual tal.actual, expected tal.expected)
4914++ itype-output-may-be-cell
5082++ itype-output-may-be-cell
4915 |= [t=itype sub=isub]
5083 |= [t=itype sub=isub]
@@ -4920,6 +5088,7 @@
4921 %union &
5089 %union &
4922 %recursive &
5090 %recursive &
4924 %collection &
5093 %collection &
4925 %face $(t body.t)
5094 %face $(t body.t)
@@ -4992,6 +5161,7 @@
4994 %recursive &
5163 %recursive &
4995 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5165 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
4996 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5166 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
4997 %face $(t body.t)
5167 %face $(t body.t)
@@ -5005,6 +5175,7 @@
5007 %recursive ?=(~ label.t)
5177 %recursive ?=(~ label.t)
5178+ %jrec ?=(~ label.t)
5008 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5179 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5009 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5180 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5010 %face $(t body.t)
5181 %face $(t body.t)
@@ -5032,36 +5203,77 @@
5032 $(cases t.cases, good `trial)
5203 $(cases t.cases, good `trial)
5035−:: A constructor needs a case with its tag at the head and a payload
5206+:: A constructor needs a case whose head has the same literal noun as its
5036−:: compatible with the expected gate sample. Other case forms do not
5207+:: tag. An unresolved or opaque case may reveal one later, so it cannot
5037−:: identify a constructor.
5208+:: prove a mismatch or a unique match. A broad atom mold is not a case.
5039++ itype-fit-ctor-cases
5210++ itype-fit-ctor-cases
5040 |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
5211 |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
5042 =/ found=(unit ifit) ~
5213 =/ found=(unit ifit) ~
5217+ ?: pending [%unknown ~]
5044− ?~ cases ?~(found [%bad ~] u.found)
5218+ ?~ found [%bad ~]
5220+ =/ raw=itype i.cases
5222+ $(cases t.cases, pending &)
5045− =/ c=itype (itype-walk i.cases sub)
5223+ =/ c=itype (itype-walk raw sub)
5224+ ?: ?=(?(%var %tag %recursive %jrec %union %face) -.c)
5225+ $(cases t.cases, pending &)
5046 ?. ?=(%cell -.c) $(cases t.cases)
5226 ?. ?=(%cell -.c) $(cases t.cases)
5047− =/ head=itype (itype-walk hed.c sub)
5227+ =/ raw-head=itype hed.c
5228+ ?: ?=(%var -.raw-head)
5229+ $(cases t.cases, pending &)
5230+ =/ head=itype (itype-walk raw-head sub)
5231+ :: A single faced, explicitly atom-only head cannot be the tag case.
5232+ :: Do not follow variables or peel nested faces for this negative proof.
5233+ ?: ?=(%face -.head)
5234+ ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5236+ $(cases t.cases, pending &)
5237+ ?: ?=(?(%var %tag %recursive %jrec %union) -.head)
5238+ $(cases t.cases, pending &)
5048 ?. ?=(%const -.head) $(cases t.cases)
5239 ?. ?=(%const -.head) $(cases t.cases)
5049− ?. =(%term form.literal.head) $(cases t.cases)
5050 ?. =(val.literal.head val.tag) $(cases t.cases)
5240 ?. =(val.literal.head val.tag) $(cases t.cases)
5051− ?^ found [%unknown ~]
5241+ :: Equal heads can have disjoint payloads. Test each from the original
5242+ :: substitution; a unique success is usable only with no unknown rival.
5052 =/ trial=ifit (itype-fit sample tal.c sub next)
5243 =/ trial=ifit (itype-fit sample tal.c sub next)
5245+ %bad $(cases t.cases)
5246+ %unknown $(cases t.cases, pending &)
5248+ ?^ found [%unknown ~]
5053− $(cases t.cases, found `trial)
5249+ $(cases t.cases, found `trial)
5055++ itype-fit
5252++ itype-fit
5056 |= [actual=itype expected=itype sub=isub next=@ud]
5253 |= [actual=itype expected=itype sub=isub next=@ud]
5255+ (itype-fit-inner actual expected sub next | |)
5257+ |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5259+ ?: &(!skip-width ?=(%cell -.actual) ?=(%cell -.expected) |((width-spine-exhausted actual 1.024) (width-spine-exhausted expected 1.024)))
5261+ =/ known=(unit [source=iwfields target=iwfields])
5263+ (width-known-shape actual expected sub)
5264+ =/ too-wide=? ?~(known | (gth (lent order.source.u.known) (lent order.target.u.known)))
5265+ ?: too-wide [%unknown ~]
5266+ =/ spine-checked=? |(spine-proof ?=(^ known))
5058 =/ uncertain=?
5267 =/ uncertain=?
5059− |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5268+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)))
5060 =/ actual-open=?
5269 =/ actual-open=?
5061− |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
5270+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))
5062 =. actual (itype-walk actual sub)
5271 =. actual (itype-walk actual sub)
5063 =. expected (itype-walk expected sub)
5272 =. expected (itype-walk expected sub)
5064 ?: =(actual expected) [%ok sub next]
5273 ?: =(actual expected) [%ok sub next]
5274+ :: The relation of the source loobean mold to explicit @f is not yet
5275+ :: established. Keep it unsupported rather than asserting a mismatch.
5276+ ?: &(?=(%flag -.actual) ?=(%atom -.expected) =(%f aura.expected)) [%unknown ~]
5065 :: Any value can be used where a noun is expected. An unresolved
5277 :: Any value can be used where a noun is expected. An unresolved
5066 :: bare tag is fixed as a constant; a constructor still needs a gate.
5278 :: bare tag is fixed as a constant; a constructor still needs a gate.
5067 ?: ?=(%noun -.expected)
5279 ?: ?=(%noun -.expected)
@@ -5071,6 +5283,11 @@
5071 [%ok sub next]
5283 [%ok sub next]
5072 :: An arbitrary noun is not known to fit a narrower type.
5284 :: An arbitrary noun is not known to fit a narrower type.
5073 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5285 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5286+ ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5287+ ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5288+ ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
5289+ ?:(&(=(at.actual at.expected) =(name.actual name.expected) =(head.actual head.expected) =(aura.actual aura.expected) =(tail.actual tail.expected)) [%ok sub next] [%bad ~])
5290+ ?: &(|(?=(%jrec -.actual) ?=(%jrec -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
5074 ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
5291 ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
5075 ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
5292 ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
5076 ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
5293 ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
@@ -5096,7 +5313,7 @@
5096 ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5313 ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5097 $(expected body.expected)
5314 $(expected body.expected)
5098 ?: ?=(%union -.actual) [%unknown ~]
5315 ?: ?=(%union -.actual) [%unknown ~]
5099− ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
5316+ ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))) [%unknown ~]
5100 ?: &(?=(%union -.expected) !?=(%var -.actual))
5317 ?: &(?=(%union -.expected) !?=(%var -.actual))
5101 (itype-fit-cases actual cases.expected sub next)
5318 (itype-fit-cases actual cases.expected sub next)
5102 ?: ?=(%tag -.actual)
5319 ?: ?=(%tag -.actual)
@@ -5104,7 +5321,7 @@
5104 =/ u=(unit isub) (itype-unify actual expected sub)
5321 =/ u=(unit isub) (itype-unify actual expected sub)
5105 ?~ u [%bad ~]
5322 ?~ u [%bad ~]
5106 [%ok u.u next]
5323 [%ok u.u next]
5107− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5324+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5108 ?: ?=(%face -.expected) $(expected body.expected)
5325 ?: ?=(%face -.expected) $(expected body.expected)
5109 ?: constructor.actual
5326 ?: constructor.actual
5110 ?. ?=(%fn -.expected) [%bad ~]
5327 ?. ?=(%fn -.expected) [%bad ~]
@@ -5132,13 +5349,17 @@
5132 =/ u=(unit isub) (itype-unify actual expected sub)
5349 =/ u=(unit isub) (itype-unify actual expected sub)
5133 ?~ u [%bad ~]
5350 ?~ u [%bad ~]
5134 [%ok u.u next]
5351 [%ok u.u next]
5135− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5352+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5136 ?: ?=(%face -.expected) $(expected body.expected)
5353 ?: ?=(%face -.expected) $(expected body.expected)
5137 ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5354 ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5138 [%unknown ~]
5355 [%unknown ~]
5139 ?: ?=(%const -.expected)
5356 ?: ?=(%const -.expected)
5140 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
5357 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
5141 ?: ?=(%atom -.expected)
5358 ?: ?=(%atom -.expected)
5359+ :: A loobean singleton must not silently widen into another aura.
5360+ ?: =(%loobean form.literal.actual)
5361+ ?: =(%f aura.expected) [%unknown ~]
5142 ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
5363 ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
5143 [%bad ~]
5364 [%bad ~]
5144 ?: ?=(%flag -.expected)
5365 ?: ?=(%flag -.expected)
@@ -5146,8 +5367,14 @@
5146 ?: ?=(%any-atom -.expected) [%ok sub next]
5367 ?: ?=(%any-atom -.expected) [%ok sub next]
5147 [%bad ~]
5368 [%bad ~]
5148 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5369 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5370+ :: A known face labels the same noun. Peel it before applying the
5371+ :: directional unrestricted-atom rule, preserving raw-variable guards.
5372+ ?: &(!uncertain ?=(%any-atom -.actual) ?=(%face -.expected))
5373+ $(expected body.expected, skip-width |, spine-proof |)
5374+ ?: &(!uncertain ?=(%any-atom -.expected) ?=(%face -.actual))
5375+ $(actual body.actual, skip-width |, spine-proof |)
5149 ?: ?=(%any-atom -.expected)
5376 ?: ?=(%any-atom -.expected)
5150− ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
5377+ ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%flag -.actual)) [%ok sub next]
5151 ?: ?=(%var -.actual)
5378 ?: ?=(%var -.actual)
5152 =/ unified=(unit isub) (itype-unify actual [%avar next] sub)
5379 =/ unified=(unit isub) (itype-unify actual [%avar next] sub)
5153 ?~ unified [%bad ~]
5380 ?~ unified [%bad ~]
@@ -5158,16 +5385,16 @@
5158 =/ unified=(unit isub) (itype-unify actual expected sub)
5385 =/ unified=(unit isub) (itype-unify actual expected sub)
5159 ?~ unified [%bad ~]
5386 ?~ unified [%bad ~]
5160 [%ok u.unified next]
5387 [%ok u.unified next]
5161− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5388+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
5162 [%bad ~]
5389 [%bad ~]
5163 ?: &(?=(%atom -.actual) ?=(%atom -.expected))
5390 ?: &(?=(%atom -.actual) ?=(%atom -.expected))
5164 ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
5391 ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
5165 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
5392 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
5166 [%bad ~]
5393 [%bad ~]
5167 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5394 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5168− =/ first=ifit $(actual hed.actual, expected hed.expected)
5395+ =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
5169 ?. ?=(%ok -.first) first
5396 ?. ?=(%ok -.first) first
5170− $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
5397+ $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
5171 :: A field may add a face to an occurrence of the very same type
5398 :: A field may add a face to an occurrence of the very same type
5172 :: variable. Binding that variable to a face around itself would fail
5399 :: variable. Binding that variable to a face around itself would fail
5173 :: the occurs check, but its underlying type has already matched.
5400 :: the occurs check, but its underlying type has already matched.
@@ -5189,9 +5416,10 @@
5189 [%ok u.unified next]
5416 [%ok u.unified next]
5190 ?: &(?=(%face -.actual) ?=(%face -.expected))
5417 ?: &(?=(%face -.actual) ?=(%face -.expected))
5191 ?. =(name.actual name.expected) [%bad ~]
5418 ?. =(name.actual name.expected) [%bad ~]
5192− $(actual body.actual, expected body.expected)
5419+ $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
5193− ?: ?=(%face -.actual) $(actual body.actual)
5420+ ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
5194− ?: ?=(%face -.expected) $(expected body.expected)
5421+ ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
5422+ ?: &(!uncertain (itype-closed-gates-match actual expected)) [%ok sub next]
5195 ?: (itype-face-asym actual expected sub) [%unknown ~]
5423 ?: (itype-face-asym actual expected sub) [%unknown ~]
5196 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
5424 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
5197 [%unknown ~]
5425 [%unknown ~]
@@ -5268,7 +5496,17 @@
5268+$ ienv (list [name=term scheme=ischeme])
5496+$ ienv (list [name=term scheme=ischeme])
5269+$ imold-types (list [name=term template=ischeme])
5497+$ imold-types (list [name=term template=ischeme])
5270+$ iderived [name=term agent=term mark=term]
5498+$ iderived [name=term agent=term mark=term]
5499++$ iwidth-definition [name=term original=expr typ=itype sub=isub projections=(list iwprojection)]
5500++$ iwidth-dependency [at=path source=(unit @t) definitions=(list iwidth-definition)]
5501+:: Nonrecursive request evidence is compiler-owned metadata, not a property
5502+:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
5503++$ irequest-evidence
5504+ [api-at=path name=term path=iapi-path-typed api-source=@t public-source=@t internal-source=@t prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5505+:: A unit distinguishes a verified empty closure from a detached legacy file.
5506+:: The opaque prelude is an exact trusted input, not a recursive interface mold.
5508+ [paths=(set path) requests=(list irequest-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5271−+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived)]
5509++$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t) graph=(unit irequest-graph)]
5272+$ ijimports (list [face=term interface=ifile])
5510+$ ijimports (list [face=term interface=ifile])
5273+$ icap [name=@t id=@ud at=span]
5511+$ icap [name=@t id=@ud at=span]
5274+$ icaps (list icap)
5512+$ icaps (list icap)
@@ -5278,7 +5516,165 @@
5278:: This core has no Ford dependencies; unrecognized payloads fail closed.
5516:: This core has no Ford dependencies; unrecognized payloads fail closed.
5279+$ iexternals (list [module=term name=term result=*])
5517+$ iexternals (list [module=term name=term result=*])
5280+$ imark-externals (list [mark=term result=*])
5518+$ imark-externals (list [mark=term result=*])
5519+:: Hole obligations survive discarded expressions until their owning
5520+:: definition has inferred; their source spans support unresolved reports.
5521++$ ihole [id=@ud at=span]
5522+:: Recursive-mold unfolding spends fuel in the threaded inference state.
5523+:: Retries can restart from an earlier state, so this bounds an attempt,
5524+:: not all parsing or module-checking work.
5525+:: Experimental: only closed, uniquely faced records have known axes.
5526++$ iwfield [name=term axis=@ud typ=itype]
5527++$ iwfields [order=(list iwfield) index=(map term iwfield)]
5528++$ iwstep [name=term axis=@ud]
5529++$ iwidth-result [steps=(list iwstep) sub=isub next=@ud]
5530++$ iwprojection [at=span original=expr source=itype target=itype steps=(list iwstep)]
5532+ |= [typ=itype sub=isub axis=@ud fuel=@ud]
5534+ =/ order=(list iwfield) ~
5535+ =/ index=(map term iwfield) *(map term iwfield)
5538+ ?: |(?=(%var -.typ) ?=(%avar -.typ) ?=(%rvar -.typ) ?=(%nvar -.typ) ?=(%rnvar -.typ)) ~
5540+ =/ entry=iwfield [name.typ axis body.typ]
5541+ ?: ?=(^ (~(get by index) name.entry)) ~
5542+ `[(flop [entry order]) (~(put by index) name.entry entry)]
5543+ ?. ?=(%cell -.typ) ~
5544+ =/ head=itype hed.typ
5545+ ?: |(?=(%var -.head) ?=(%avar -.head) ?=(%rvar -.head) ?=(%nvar -.head) ?=(%rnvar -.head)) ~
5546+ ?. ?=(%face -.head) ~
5547+ =/ entry=iwfield [name.head (mul 2 axis) body.head]
5548+ ?: ?=(^ (~(get by index) name.entry)) ~
5549+ $(typ tal.typ, axis +((mul 2 axis)), fuel (dec fuel), order [entry order], index (~(put by index) name.entry entry))
5551+ |= [source=(list iwfield) target=(list iwfield)]
5555+ ?: =(name.i.source name.i.target) $(source t.source, target t.target)
5558+ |= [source=(map term iwfield) target=(list iwfield) sub=isub next=@ud]
5559+ ^- (unit iwidth-result)
5560+ ?~ target `[~ sub next]
5561+ =/ found=(unit iwfield) (~(get by source) name.i.target)
5563+ =/ fit=ifit (itype-fit typ.u.found typ.i.target sub next)
5565+ =/ rest=(unit iwidth-result) $(target t.target, sub sub.fit, next next.fit)
5567+ `[[[name.i.target axis.u.found] steps.u.rest] sub.u.rest next.u.rest]
5568+++ width-spine-exhausted
5569+ |= [t=itype fuel=@ud]
5573+ ?. ?=(%face -.hed.t) |
5574+ $(t tal.t, fuel (dec fuel))
5575+++ width-known-shape
5576+ |= [actual=itype expected=itype sub=isub]
5577+ ^- (unit [source=iwfields target=iwfields])
5578+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5579+ =/ source=(unit iwfields) (width-scan actual sub 1 1.024)
5580+ =/ target=(unit iwfields) (width-scan expected sub 1 1.024)
5583+ `[u.source u.target]
5586+ |= [actual=itype expected=itype sub=isub]
5587+ ^- (unit [source=iwfields target=iwfields])
5588+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5589+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5590+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5593+ ?. (gth (lent order.u.source) (lent order.u.target)) ~
5594+ `[u.source u.target]
5596+ |= [actual=itype expected=itype sub=isub]
5597+ ^- (unit [source=iwfields target=iwfields])
5598+ ?. &(|(?=(%cell -.actual) ?=(%face -.actual)) |(?=(%cell -.expected) ?=(%face -.expected))) ~
5599+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5600+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5603+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
5604+ `[u.source u.target]
5607+ |= [shape=[source=iwfields target=iwfields] sub=isub next=@ud]
5608+ ^- (unit iwidth-result)
5609+ ?. (width-in-order order.source.shape order.target.shape) ~
5610+ (width-fit-fields index.source.shape order.target.shape sub next)
5612+:: Provisional, globally budgeted gate-free proof. %no includes a
5613+:: gate-bearing witness; an uninhabited sibling could invalidate it.
5614+:: Input types must be resolved and normalized under valid substitutions,
5615+:: from trusted source-backed interfaces and reader results. Collection
5616+:: list/unit names rely on their existing identity invariant; this arm
5617+:: does not validate fabricated internal types.
5619+ $% [%field name=term]
5625++$ igate-free [verdict=?(%yes %no %unknown) inhabited=? left=@ud path=(unit (list igf-segment))]
5627+ |= [types=(list itype) fuel=@ud path=(list igf-segment) index=@ud]
5629+ ?~ types [%yes | fuel ~]
5630+ ?: =(0 fuel) [%unknown | 0 ~]
5631+ =/ first=igate-free (gate-free-type i.types fuel [[%case index] path])
5632+ ?: =(%no verdict.first) first
5633+ =/ rest=igate-free $(types t.types, fuel left.first, index +(index))
5634+ ?: =(%no verdict.rest) rest
5635+ =/ inhabited=? |(inhabited.first inhabited.rest)
5636+ ?: |(=(%unknown verdict.first) =(%unknown verdict.rest)) [%unknown inhabited left.rest ~]
5637+ [%yes inhabited left.rest ~]
5639+ |= [typ=itype fuel=@ud path=(list igf-segment)]
5641+ ?: =(0 fuel) [%unknown | 0 ~]
5644+ %fn [%no & fuel `(flop path)]
5645+ %atom [%yes & fuel ~]
5646+ %any-atom [%yes & fuel ~]
5647+ %flag [%yes & fuel ~]
5648+ %const [%yes & fuel ~]
5649+ %face $(typ body.typ, path [[%field name.typ] path])
5651+ =/ head=igate-free $(typ hed.typ, path [[%head ~] path])
5652+ =/ tail=igate-free $(typ tal.typ, fuel left.head, path [[%tail ~] path])
5653+ =/ inhabited=? &(inhabited.head inhabited.tail)
5654+ ?: &(=(%no verdict.head) inhabited.tail) head(left left.tail)
5655+ ?: &(=(%no verdict.tail) inhabited.head) tail
5656+ ?: |(!=(%yes verdict.head) !=(%yes verdict.tail)) [%unknown inhabited left.tail ~]
5657+ [%yes inhabited left.tail ~]
5659+ ?. |(=(%list name.typ) =(%unit name.typ)) [%unknown | fuel ~]
5660+ ?. ?=([* ~] args.typ) [%unknown | fuel ~]
5661+ =/ item=igate-free $(typ i.args.typ, path [[%item ~] path])
5664+ ?~ cases.typ [%unknown | fuel ~]
5665+ (gate-free-types cases.typ fuel path 0)
5666+ %noun [%unknown & fuel ~]
5667+ %var [%unknown | fuel ~]
5668+ %avar [%yes & fuel ~]
5669+ %rvar [%yes & fuel ~]
5670+ %nvar [%yes & fuel ~]
5671+ %rnvar [%yes & fuel ~]
5672+ %tag [%unknown | fuel ~]
5673+ %recursive [%unknown | fuel ~]
5674+ %jrec [%yes & fuel ~]
5281−+$ 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)]
5677++$ 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)]
5282+$ idiag [msg=tape sites=(list [at=span note=tape])]
5678+$ idiag [msg=tape sites=(list [at=span note=tape])]
5283+$ iresult (each [typ=itype state=istate] idiag)
5679+$ iresult (each [typ=itype state=istate] idiag)
5284+$ isample-result (each [typ=itype env=ienv state=istate] tape)
5680+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5323,6 +5719,7 @@
5324 %cell |($(t hed.t) $(t tal.t))
5720 %cell |($(t hed.t) $(t tal.t))
5325 %recursive |
5721 %recursive |
5326 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5723 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5327 %face $(t body.t)
5724 %face $(t body.t)
5328 %union (lien cases.t |=(c=itype (itype-has-gate c)))
5725 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5330,7 +5727,9 @@
5330 %const |
5727 %const |
5335 %any-atom |
5734 %any-atom |
@@ -5343,19 +5742,120 @@
5343 ?: (itype-has-gate t) t
5742 ?: (itype-has-gate t) t
5345 %nvar [%atom %ud]
5744 %nvar [%atom %ud]
5346 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5746 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5347 %face [%face name.t $(t body.t)]
5747 %face [%face name.t $(t body.t)]
5348 %cell [%cell $(t hed.t) $(t tal.t)]
5748 %cell [%cell $(t hed.t) $(t tal.t)]
5752+:: A hole is solved only by a fully determined type or a written
5753+:: in-scope type variable. Ordinary fresh variables are not evidence.
5754+:: Compare representatives after substitution, since unification can
5755+:: orient a written capital toward the hole rather than the reverse.
5768+++ hole-same-variable
5769+ |= [a=itype b=itype]
5771+ =/ x=(unit @ud) (hole-variable-id a)
5773+ =/ y=(unit @ud) (hole-variable-id b)
5777+ |= [t=itype state=istate]
5779+ =. t (itype-walk t sub.state)
5781+ ?(%var %avar %rvar %nvar %rnvar)
5782+ ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
5783+ (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
5786+ %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5787+ %collection (levy args.t |=(c=itype (hole-known c state)))
5789+ %fn &($(t sample.t) $(t product.t))
5790+ %cell &($(t hed.t) $(t tal.t))
5793+++ promote-restricted-numbers
5794+ |= [state=istate env=ienv]
5796+ =/ ids=(list @ud) (turn caps.state |=(c=icap id.c))
5797+ =/ free=(list @ud) (free-env-vars env sub.state)
5800+ =/ t=itype (itype-walk [%var i.ids] sub.state)
5801+ ?: &(?=(%rnvar -.t) !(lien free |=(n=@ud =(n +.t))))
5802+ $(ids t.ids, state state(sub [[+.t [%rvar +.t]] sub.state]))
5805+++ default-hole-numbers
5806+ |= [all=(list ihole) prior=(list ihole) state=istate env=ienv permit=?]
5808+ :: Do not default a named capital or a variable captured from env.
5810+ ?: =(all prior) state
5812+ =/ t=itype (itype-walk [%var id.i.all] sub.state)
5813+ =/ free=(list @ud) (free-env-vars env sub.state)
5814+ =? state &(?=(?(%nvar %rnvar) -.t) !(hole-known t state) !(lien free |=(id=@ud =(id id.t))))
5815+ state(sub [[id.t [%atom %ud]] sub.state])
5818+:: Only obligations created inside this definition belong to it.
5820+ |= [all=(list ihole) prior=(list ihole)]
5824+ [i.all $(all t.all)]
5826+ |= [t=itype state=istate]
5828+ =. t (itype-walk t sub.state)
5830+ ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
5831+ %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5832+ %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5834+ %fn |($(t sample.t) $(t product.t))
5835+ %cell |($(t hed.t) $(t tal.t))
5840+ |= [all=(list ihole) prior=(list ihole) state=istate]
5842+ =/ work=(list ihole) (flop (holes-created all prior))
5845+ ?: (hole-known [%var id.i.work] state) $(work t.work)
5846+ ?: (hole-uncertain [%var id.i.work] state)
5847+ `["type hole needs unsupported inference" ~[[at.i.work "type hole"]]]
5848+ `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
5352++ itype-vars
5850++ itype-vars
5353 |= t=itype
5851 |= t=itype
5354 ^- (list @ud)
5852 ^- (list @ud)
5356 %var ~[id.t]
5854 %var ~[id.t]
5357 %avar ~[id.t]
5855 %avar ~[id.t]
5358 %nvar ~[id.t]
5857 %nvar ~[id.t]
5360 %any-atom ~
5860 %any-atom ~
@@ -5364,6 +5864,7 @@
5364 %const ~
5864 %const ~
5365 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5865 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5366 %recursive ~
5866 %recursive ~
5367 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5868 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5368 %face $(t body.t)
5869 %face $(t body.t)
5369 %fn (weld $(t sample.t) $(t product.t))
5870 %fn (weld $(t sample.t) $(t product.t))
@@ -5391,10 +5892,18 @@
5391 =/ found=(unit itype) (itype-lookup id.t ren)
5892 =/ found=(unit itype) (itype-lookup id.t ren)
5392 ?~ found t
5893 ?~ found t
5896+ =/ found=(unit itype) (itype-lookup id.t ren)
5395 =/ found=(unit itype) (itype-lookup id.t ren)
5900 =/ found=(unit itype) (itype-lookup id.t ren)
5396 ?~ found t
5901 ?~ found t
5904+ =/ found=(unit itype) (itype-lookup id.t ren)
5399 %any-atom t
5908 %any-atom t
@@ -5403,6 +5912,7 @@
5403 %const t
5912 %const t
5404 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5913 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5405 %recursive t
5914 %recursive t
5406 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5916 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5407 %face [%face name.t $(t body.t)]
5917 %face [%face name.t $(t body.t)]
5408 %fn [%fn $(t sample.t) $(t product.t)]
5918 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5418,7 +5928,9 @@
5420 %avar =(n id.t)
5930 %avar =(n id.t)
5421 %nvar =(n id.t)
5932 %nvar =(n id.t)
5423 %any-atom |
5935 %any-atom |
@@ -5427,11 +5939,35 @@
5427 %const |
5939 %const |
5428 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5940 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5429 %recursive |
5941 %recursive |
5430 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5943 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5431 %face $(t body.t)
5944 %face $(t body.t)
5432 %fn |($(t sample.t) $(t product.t))
5945 %fn |($(t sample.t) $(t product.t))
5433 %cell |($(t hed.t) $(t tal.t))
5946 %cell |($(t hed.t) $(t tal.t))
5948+++ itype-var-is-restricted
5963+ %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
5966+ %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
5968+ %fn |($(t sample.t) $(t product.t))
5969+ %cell |($(t hed.t) $(t tal.t))
5436:: Canonical numbering makes printed variables independent of the order
5972:: Canonical numbering makes printed variables independent of the order
5437:: the unifier happened to allocate intermediates.
5973:: the unifier happened to allocate intermediates.
@@ -5443,7 +5979,7 @@
5443 =/ n=@ud 0
5979 =/ n=@ud 0
5445 ?~ vars (itype-rename t ren)
5981 ?~ vars (itype-rename t ren)
5446− =/ replacement=itype ?:((itype-var-is-atom i.vars t) [%avar n] [%var n])
5982+ =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] [%var n]))
5447 $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
5983 $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
5449++ instantiate-scheme
5985++ instantiate-scheme
@@ -5454,11 +5990,11 @@
5455 ?~ vars [(itype-rename typ.scheme ren) state]
5991 ?~ vars [(itype-rename typ.scheme ren) state]
5456 =/ replacement=itype
5992 =/ replacement=itype
5457− ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] [%var next.state])
5993+ ?:((itype-var-is-restricted i.vars typ.scheme) [%rvar next.state] ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] [%var next.state]))
5458 :: A generalized atom variable is a valid origin for re-generalizing
5994 :: A generalized atom variable is a valid origin for re-generalizing
5459 :: an alias, just as a sample binder is.
5995 :: an alias, just as a sample binder is.
5460 =/ st=istate state(next +(next.state))
5996 =/ st=istate state(next +(next.state))
5461− =? binders.st ?=(%avar -.replacement) [next.state binders.state]
5997+ =? binders.st |(?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
5462 $(vars t.vars, ren [[i.vars replacement] ren], state st)
5998 $(vars t.vars, ren [[i.vars replacement] ren], state st)
5464++ icap-lookup
6000++ icap-lookup
@@ -5588,6 +6124,10 @@
5588 %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
6124 %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
5589 %fork (imported-faces-valid-list +.node)
6125 %fork (imported-faces-valid-list +.node)
5590 %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
6126 %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
6128+ ?. ?=([%named @ @ *] node) |
6129+ =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
6130+ (imported-faces-valid body.n)
5593++ imported-faces-valid-list
6133++ imported-faces-valid-list
@@ -5641,6 +6181,15 @@
5641 =/ aura=@ta (@ta +<.node)
6181 =/ aura=@ta (@ta +<.node)
5642 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
6182 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5643 `[%atom aura]
6183 `[%atom aura]
6185+ ?. ?=([%named @ @ *] node) ~
6186+ =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
6187+ ?. &((jibb-face-name module.n) (jibb-face-name name.n)) ~
6188+ ?. ?=([%fork *] body.n) ~
6189+ =/ proof=(unit irec-pattern) (rec-pattern body.n (@tas module.n) (@tas name.n))
6192+ `[%recursive (@tas module.n) (@tas name.n) `(crip "{(trip name.n)}.{(trip module.n)}")]
5645 ?. ?=([%apply @ *] node) ~
6194 ?. ?=([%apply @ *] node) ~
5646 =/ name=term (@tas +<.node)
6195 =/ name=term (@tas +<.node)
@@ -5806,21 +6355,44 @@
5806 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
6355 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
5807 $(molds t.molds)
6356 $(molds t.molds)
5809−:: A public non-generic alias names exactly its origin and arguments.
6358+:: A prelude union alias is a display name, not a new union identity. An
5810−:: Reusing only an origin could print a different generic instantiation.
6359+:: identity-generic alias can carry the origin's arguments only when the
6360+:: origin, arity and ordered parameters match. Swapped, repeated, fixed
6361+:: or phantom parameters cannot be printed that way and remain unsupported
6362+:: when their only available name is private. A nongeneric alias of a
6363+:: generic instantiation cannot be printed with the origin's arguments.
6364+++ identity-union-parameters
6365+ |= [vars=(list @ud) args=(list itype)]
6369+ ?. =([%var i.vars] i.args) |
6370+ $(vars t.vars, args t.args)
5811++ prelude-union-alias
6371++ prelude-union-alias
5812 |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
6372 |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
5813 ^- (unit term)
6373 ^- (unit term)
5815 ?~ molds ~
6374 ?~ molds ~
5816 =/ template=ischeme template.i.molds
6375 =/ template=ischeme template.i.molds
5817− ?: &(?=(~ vars.template) ?=(%union -.typ.template))
6376+ ?. ?=(%union -.typ.template) $(molds t.molds)
6377+ ?. =(`origin origin.typ.template) $(molds t.molds)
6379+ ?^ args $(molds t.molds)
5818− ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
6380+ ?:(=(args args.typ.template) `name.i.molds $(molds t.molds))
6381+ ?: &((identity-union-parameters vars.template args.typ.template) =((lent vars.template) (lent args)))
5819 $(molds t.molds)
6383 $(molds t.molds)
5821:: Names exported by the directly imported module are visible through its
6385:: Names exported by the directly imported module are visible through its
5822:: face; a matching prelude alias is also visible without a qualifier.
6386:: face; a matching prelude alias is also visible without a qualifier.
6389+ |= [origin=path name=term molds=imold-types]
6392+ =/ template=ischeme template.i.molds
6393+ ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
5824++ itype-in-import
6396++ itype-in-import
5825 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6397 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
5826 ^- itype
6398 ^- itype
@@ -5840,6 +6412,12 @@
5840 `(crip "{(trip u.alias)}.{(trip face)}")
6412 `(crip "{(trip u.alias)}.{(trip face)}")
5841 [%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)))]
6413 [%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)))]
5842 %recursive [%recursive module.t name.t ~]
6414 %recursive [%recursive module.t name.t ~]
6416+ =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6417+ ?^ public t(label `u.public)
6418+ =/ alias=(unit term) (jrec-alias at.t name.t molds.iface)
6419+ ?~ alias t(label ~)
6420+ t(label `(crip "{(trip u.alias)}.{(trip face)}"))
5843 %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
6421 %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
5844 %face [%face name.t $(t body.t)]
6422 %face [%face name.t $(t body.t)]
5845 %fn [%fn $(t sample.t) $(t product.t)]
6423 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5913,9 +6491,46 @@
5913 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
6491 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
5914 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
6492 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
6494+:: Recognize a unique top-level source mold with exactly a null case and a
6495+:: faced atom-headed cell whose faced tail names that same mold. Its Jibb
6496+:: path and name provide nominal identity. Other recursive shapes fail closed;
6497+:: construction and matching expose the proven shape one layer at a time.
6498+++ simple-source-recursive
6499+ |= [name=term sh=shape state=istate]
6501+ ?. (lien top-molds.state |=(n=term =(n name))) ~
6502+ =/ original=(unit shape) (find-simple-mold name molds.state)
6504+ ?. =(u.original sh) ~
6505+ ?. ?=(%union -.sh) ~
6506+ =/ cs=(list shape) cases.sh
6510+ ?. ?=(%const -.i.cs) ~
6511+ ?. =(%null form.lit.i.cs) ~
6512+ ?. ?=(%cell -.i.t.cs) ~
6513+ =/ fs=(list field) fields.i.t.cs
6517+ ?. ?=(%face -.i.fs) ~
6518+ ?. ?=(%aura -.shape.i.fs) ~
6519+ ?. !=(0 aura.shape.i.fs) ~
6520+ ?. ?=(%face -.i.t.fs) ~
6521+ ?. !=(name.i.fs name.i.t.fs) ~
6522+ =/ tail=shape shape.i.t.fs
6523+ ?. ?=(%ref -.tail) ~
6524+ ?. =(names.tail ~[name]) ~
6525+ `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
5916++ infer-mold-template
6527++ infer-mold-template
5917 |= [sh=shape state=istate]
6528 |= [sh=shape state=istate]
5918 ^- (unit [template=ischeme state=istate])
6529 ^- (unit [template=ischeme state=istate])
6530+ =/ direct=(unit itype)
6531+ ?. ?=([@ ~] active.state) ~
6532+ (simple-source-recursive i.active.state sh state)
6533+ ?^ direct `[[u.direct ~] state]
5919 ?: ?=(%generic -.sh)
6534 ?: ?=(%generic -.sh)
5920 ?~ vars.sh ~
6535 ?~ vars.sh ~
5921 ?. (distinct-params vars.sh) ~
6536 ?. (distinct-params vars.sh) ~
@@ -5923,17 +6538,19 @@
5923 =/ out=(unit [typ=itype state=istate])
6538 =/ out=(unit [typ=itype state=istate])
5924 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
6539 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
5925 ?~ out ~
6540 ?~ out ~
6541+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
5926 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
6542 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
5927 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
6543 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
5928 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
6544 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
5929 =/ used=(list @ud) (itype-vars typ.u.out)
6545 =/ used=(list @ud) (itype-vars typ.u.out)
5930 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
6546 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5931− `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state)]
6547+ `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
5932 =/ out=(unit [typ=itype state=istate])
6548 =/ out=(unit [typ=itype state=istate])
5933 (infer-simple-shape sh state(params ~, in-mold &))
6549 (infer-simple-shape sh state(params ~, in-mold &))
5934 ?~ out ~
6550 ?~ out ~
6551+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
5935 ?: ?=(^ (itype-vars typ.u.out)) ~
6552 ?: ?=(^ (itype-vars typ.u.out)) ~
5936− `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
6553+ `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
5938:: A direct imported reference may carry definite reader evidence. Only
6555:: A direct imported reference may carry definite reader evidence. Only
5939:: uniquely supplied, declared inputs are used; unsupported data stay generic.
6556:: uniquely supplied, declared inputs are used; unsupported data stay generic.
@@ -6036,13 +6653,15 @@
6036 |= [sh=shape state=istate]
6653 |= [sh=shape state=istate]
6037 ^- (unit [typ=itype state=istate])
6654 ^- (unit [typ=itype state=istate])
6656+ %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
6040 ?: =(0 aura.sh) `[[%any-atom ~] state]
6658 ?: =(0 aura.sh) `[[%any-atom ~] state]
6041 `[[%atom aura.sh] state]
6659 `[[%atom aura.sh] state]
6042 %flag `[[%flag ~] state]
6660 %flag `[[%flag ~] state]
6043 %noun `[[%noun ~] state]
6661 %noun `[[%noun ~] state]
6045− ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
6663+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh) =(%loobean form.lit.sh)) ~
6664+ ?: &(=(%loobean form.lit.sh) !|(=(0 val.lit.sh) =(1 val.lit.sh))) ~
6046 `[[%const lit.sh] state]
6665 `[[%const lit.sh] state]
6048 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6667 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
@@ -6086,10 +6705,13 @@
6086 ?~ prelude-entry ~
6705 ?~ prelude-entry ~
6087 ?^ vars.u.prelude-entry ~
6706 ?^ vars.u.prelude-entry ~
6088 `[typ.u.prelude-entry state]
6707 `[typ.u.prelude-entry state]
6708+ =/ direct=(unit itype) (simple-source-recursive n u.found state)
6709+ ?^ direct `[u.direct state]
6089 =/ out=(unit [typ=itype state=istate])
6710 =/ out=(unit [typ=itype state=istate])
6090 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
6711 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
6091 ?~ out ~
6712 ?~ out ~
6713+ ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
6092− `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state)]
6714+ `[(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)]
6094 ?~ ref.sh ~
6716 ?~ ref.sh ~
6095 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
6717 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -6123,11 +6745,12 @@
6123 =/ out=(unit [typ=itype state=istate])
6745 =/ out=(unit [typ=itype state=istate])
6124 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
6746 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
6125 ?~ out ~
6747 ?~ out ~
6748+ ?^ (unresolved-hole holes.state.u.out holes.state.u.args state.u.out) ~
6126 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
6749 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
6127 ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
6750 ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
6128 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
6751 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
6129 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6752 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6130− `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
6753+ `[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)]
6132 =/ param=(unit itype) (iparam-lookup name.sh params.state)
6755 =/ param=(unit itype) (iparam-lookup name.sh params.state)
6133 ?^ param `[u.param state]
6756 ?^ param `[u.param state]
@@ -6167,12 +6790,12 @@
6167 ^- isample-result
6790 ^- isample-result
6170− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6793+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6171 [%| "sample shadows a name"]
6794 [%| "sample shadows a name"]
6172 =/ t=itype [%var next.state]
6795 =/ t=itype [%var next.state]
6173 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
6796 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
6175− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6798+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6176 [%| "sample shadows a name"]
6799 [%| "sample shadows a name"]
6177 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
6800 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
6178 ?~ t [%| "sample mold is not supported by partial inference"]
6801 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -6240,6 +6863,7 @@
6242 ?: ?=(%mold -.i.ds) $(ds t.ds)
6865 ?: ?=(%mold -.i.ds) $(ds t.ds)
6866+ ?: =(name.i.ds %proj) |
6243 ?. (unique-value-name name.i.ds names) |
6867 ?. (unique-value-name name.i.ds names) |
6244 ?: ?=(^ (ienv-lookup name.i.ds env)) |
6868 ?: ?=(^ (ienv-lookup name.i.ds env)) |
6245 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
6869 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -6263,6 +6887,7 @@
6264 ?~ locals &
6888 ?~ locals &
6265 =/ n=term name.i.locals
6889 =/ n=term name.i.locals
6266 ?. (unique-value-name n names) |
6891 ?. (unique-value-name n names) |
6267 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
6892 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
6268 ?: (lien marks.state |=(m=term =(n m))) |
6893 ?: (lien marks.state |=(m=term =(n m))) |
@@ -6442,6 +7067,10 @@
6442 =/ retried=? ?=(%| -.inferred)
7067 =/ retried=? ?=(%| -.inferred)
6443 =? inferred retried (infer-recursive-gate d env local-state)
7068 =? inferred retried (infer-recursive-gate d env local-state)
6444 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7069 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7070+ =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7071+ =. 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)))
7072+ =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
7073+ ?^ hole [%| u.hole]
6445 =/ merged=(unit [first=icap second=icap])
7074 =/ merged=(unit [first=icap second=icap])
6446 (merged-capitals caps.state.p.inferred sub.state.p.inferred)
7075 (merged-capitals caps.state.p.inferred sub.state.p.inferred)
6447 ?^ merged
7076 ?^ merged
@@ -6457,7 +7086,7 @@
6457 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7086 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
6458 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7087 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
6459 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7088 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6460− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
7089+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
6462:: Try complete cyclic local groups after individual definitions stall.
7091:: Try complete cyclic local groups after individual definitions stall.
6463:: Components with non-gates or unresolved constraints stay unavailable.
7092:: Components with non-gates or unresolved constraints stay unavailable.
@@ -6776,7 +7405,7 @@
6776 [%| ["list branch pattern is not supported by partial inference" ~]]
7405 [%| ["list branch pattern is not supported by partial inference" ~]]
6777 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
7406 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
6778 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
7407 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6779− ?: |(=(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)))))
7408+ ?: |(=(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)))))
6780 [%| ["pattern binder shadows a name" ~]]
7409 [%| ["pattern binder shadows a name" ~]]
6781 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
7410 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
6782 =/ left=iresult
7411 =/ left=iresult
@@ -6813,7 +7442,7 @@
6813 [%| ["unit branch pattern is not supported by partial inference" ~]]
7442 [%| ["unit branch pattern is not supported by partial inference" ~]]
6814 =/ binder=(unit term) ?:(first-empty second-name first-name)
7443 =/ binder=(unit term) ?:(first-empty second-name first-name)
6815 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
7444 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
6816− ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
7445+ ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
6817 [%| ["pattern binder shadows a name" ~]]
7446 [%| ["pattern binder shadows a name" ~]]
6818 =/ payload=(unit itype) (unit-union-payload typ)
7447 =/ payload=(unit itype) (unit-union-payload typ)
6819 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
7448 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -6845,12 +7474,14 @@
6845 =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
7474 =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
6846 ?: |(?=(%atom -.t) ?=(%any-atom -.t))
7475 ?: |(?=(%atom -.t) ?=(%any-atom -.t))
6847 $(ps t.ps, state state.p.item)
7476 $(ps t.ps, state state.p.item)
6848− ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
7477+ ?: &(|(?=(%nvar -.t) ?=(%rnvar -.t)) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
6849 $(ps t.ps, state state.p.item)
7478 $(ps t.ps, state state.p.item)
6850 ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
7479 ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
6851 $(ps t.ps, state state.p.item)
7480 $(ps t.ps, state state.p.item)
6852 ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
7481 ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
6853 [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
7482 [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
7483+ ?: &(?=(%rvar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
7484+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
6854 ?: ?=(%cell -.t)
7485 ?: ?=(%cell -.t)
6855 [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
7486 [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
6856 [%| ["interpolation type needs unsupported inference" ~]]
7487 [%| ["interpolation type needs unsupported inference" ~]]
@@ -6913,7 +7544,7 @@
6913 ^- (unit ienv)
7544 ^- (unit ienv)
6914 =. t ?:(?=(%face -.t) body.t t)
7545 =. t ?:(?=(%face -.t) body.t t)
6915 ?: ?=(%bind -.p)
7546 ?: ?=(%bind -.p)
6916− ?: |(?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
7547+ ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
6917 `[[name.p [t ~]] env]
7548 `[[name.p [t ~]] env]
6918 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
7549 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
@@ -6961,10 +7592,9 @@
6961 $(xs t.xs, out (weld out rows), origin +(origin))
7592 $(xs t.xs, out (weld out rows), origin +(origin))
6963++ infer-known-union-whole
7594++ infer-known-union-whole
6964− |= [e=expr env=ienv state=istate]
7595+ |= [e=expr env=ienv subject=iresult]
6965 ^- (unit iresult)
7596 ^- (unit iresult)
6966 ?> ?=(%branch -.e)
7597 ?> ?=(%branch -.e)
6967− =/ subject=iresult (infer-fragment subject.e env state)
6968 ?: ?=(%| -.subject) `subject
7598 ?: ?=(%| -.subject) `subject
6969 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7599 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6970 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7600 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
@@ -6999,10 +7629,9 @@
6999 $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
7629 $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
7001++ infer-known-union-context-whole
7631++ infer-known-union-context-whole
7002− |= [e=expr expected=itype env=ienv state=istate context=span]
7632+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
7003 ^- (unit iresult)
7633 ^- (unit iresult)
7004 ?> ?=(%branch -.e)
7634 ?> ?=(%branch -.e)
7005− =/ subject=iresult (infer-fragment subject.e env state)
7006 ?: ?=(%| -.subject) `subject
7635 ?: ?=(%| -.subject) `subject
7007 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7636 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7008 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7637 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
@@ -7044,10 +7673,9 @@
7044 $(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)
7673 $(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)
7046++ infer-known-union-finite
7675++ infer-known-union-finite
7047− |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7676+ |= [e=expr env=ienv subject=iresult expected=(unit [typ=itype context=span])]
7048 ^- iresult
7677 ^- iresult
7049 ?> ?=(%branch -.e)
7678 ?> ?=(%branch -.e)
7050− =/ subject=iresult (infer-fragment subject.e env state)
7051 ?: ?=(%| -.subject) subject
7679 ?: ?=(%| -.subject) subject
7052 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7680 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7053 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7681 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
@@ -7142,29 +7770,108 @@
7142 [%| ["single-case branch result needs context in partial inference" ~]]
7770 [%| ["single-case branch result needs context in partial inference" ~]]
7143 [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
7771 [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
7773+:: This view is used only by pattern analysis, never exported or bound as
7774+:: the subject. Only null plus a two-binder/wildcard cell is supported; its
7775+:: tail keeps the original recursive type. Other patterns fail closed.
7777+ |= [e=expr subject=iresult]
7779+ ?: ?=(%| -.subject) subject
7780+ ?. ?=(%branch -.e) subject
7781+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7782+ ?. ?=(%jrec -.typ) subject
7784+ ?~ t.arms.e subject
7785+ ?^ t.t.arms.e subject
7786+ =/ x=pattern pat.i.arms.e
7787+ =/ y=pattern pat.i.t.arms.e
7788+ =/ empty=? &(?=(%lit -.x) =(%null form.lit.x))
7789+ =/ full=pattern ?:(empty y x)
7790+ ?. |(empty &(?=(%lit -.y) =(%null form.lit.y))) subject
7791+ ?. ?=(%cell -.full) subject
7792+ ?~ items.full subject
7793+ ?~ t.items.full subject
7794+ ?^ t.t.items.full subject
7795+ ?. |(?=(%bind -.i.items.full) ?=(%any -.i.items.full)) subject
7796+ ?. |(?=(%bind -.i.t.items.full) ?=(%any -.i.t.items.full)) subject
7797+ ?: =(0 jrec-fuel.state.p.subject)
7798+ [%| ["recursive mold unfolding needs unsupported inference" ~]]
7799+ =/ nil=itype [%const [%null %n 0 '~']]
7800+ =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
7801+ [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
7803+++ infer-known-union-branch-subject
7804+ |= [e=expr env=ienv subject=iresult]
7806+ =. subject (jrec-match-view e subject)
7807+ =/ whole=(unit iresult) (infer-known-union-whole e env subject)
7808+ ?~ whole (infer-known-union-finite e env subject ~)
7145++ infer-known-union-branch
7811++ infer-known-union-branch
7146 |= [e=expr env=ienv state=istate]
7812 |= [e=expr env=ienv state=istate]
7147 ^- iresult
7813 ^- iresult
7148− =/ whole=(unit iresult) (infer-known-union-whole e env state)
7814+ ?> ?=(%branch -.e)
7149− ?~ whole (infer-known-union-finite e env state ~)
7815+ (infer-known-union-branch-subject e env (infer-fragment subject.e env state))
7152−++ infer-known-union-context
7817+++ infer-known-union-context-subject
7153− |= [e=expr expected=itype env=ienv state=istate context=span]
7818+ |= [e=expr expected=itype env=ienv subject=iresult context=span]
7154 ^- iresult
7819 ^- iresult
7820+ =. subject (jrec-match-view e subject)
7155− =/ whole=(unit iresult) (infer-known-union-context-whole e expected env state context)
7821+ =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
7156− ?~ whole (infer-known-union-finite e env state `[expected context])
7822+ ?~ whole (infer-known-union-finite e env subject `[expected context])
7825+:: Limit speculative subject inference to wings and shallow calls;
7826+:: grouping is peeled linearly and cannot introduce a nested branch.
7827+++ simple-union-subject-arg
7833+ %str !(lien pieces.e |=(p=piece ?=(%expr -.p)))
7837+++ safe-union-subject
7840+ ?: ?=(%group -.e) $(e inner.e)
7843+ ?. ?=(%wing -.head.e) |
7844+ (levy args.e simple-union-subject-arg)
7846+++ duplicate-loobean-arms
7849+ ?. ?=(%branch -.e) |
7853+ =/ x=pattern pat.i.arms.e
7854+ =/ y=pattern pat.i.t.arms.e
7855+ ?. &(?=(%lit -.x) ?=(%lit -.y)) |
7856+ ?. &(=(%loobean form.lit.x) =(%loobean form.lit.y)) |
7857+ =(val.lit.x val.lit.y)
7859+++ union-subject-call
7862+ ?: ?=(%group -.e) $(e inner.e)
7159++ known-union-subject
7865++ known-union-subject
7160 |= [e=expr env=ienv state=istate]
7866 |= [e=expr env=ienv state=istate]
7161− ^- (unit itype)
7867+ ^- (unit iresult)
7162− ?. ?=(%wing -.e) ~
7868+ ?. (safe-union-subject e) ~
7163 =/ subject=iresult (infer-fragment e env state)
7869 =/ subject=iresult (infer-fragment e env state)
7164− ?: ?=(%| -.subject) ~
7870+ ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
7165 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7871 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7166− ?. ?=(%union -.typ) ~
7872+ ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
7169:: Infer changes only against a fully known record spine. Retain the
7876:: Infer changes only against a fully known record spine. Retain the
7170:: target type; unknown spines and repeated edits remain unsupported.
7877:: target type; unknown spines and repeated edits remain unsupported.
@@ -7271,7 +7978,7 @@
7271 |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7978 |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7272 ^- (unit idiag)
7979 ^- (unit idiag)
7273 =/ original=[left=itype right=itype] [actual expected]
7980 =/ original=[left=itype right=itype] [actual expected]
7274− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7981+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%rvar -.left.original) |(?=(%nvar -.left.original) ?=(%rnvar -.left.original)) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%rvar -.right.original) |(?=(%nvar -.right.original) ?=(%rnvar -.right.original))) ~
7275 =/ fit=ifit (itype-fit actual expected sub next)
7982 =/ fit=ifit (itype-fit actual expected sub next)
7276 ?. ?=(%bad -.fit) ~
7983 ?. ?=(%bad -.fit) ~
7277 =. actual (itype-walk actual sub)
7984 =. actual (itype-walk actual sub)
@@ -7292,7 +7999,7 @@
7292 ?~ items ~
7999 ?~ items ~
7293 ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
8000 ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
7294 =/ original=[left=itype right=itype] [actual expected]
8001 =/ original=[left=itype right=itype] [actual expected]
7295− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
8002+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%rvar -.left.original) |(?=(%nvar -.left.original) ?=(%rnvar -.left.original)) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%rvar -.right.original) |(?=(%nvar -.right.original) ?=(%rnvar -.right.original))) ~
7296 =. actual (itype-walk actual sub)
8003 =. actual (itype-walk actual sub)
7297 =. expected (itype-walk expected sub)
8004 =. expected (itype-walk expected sub)
7298 ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8005 ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
@@ -7312,6 +8019,15 @@
7312 =/ head=expr [%lit at.e [%term %tas tag.e (crip ['%' (trip tag.e)])]]
8019 =/ head=expr [%lit at.e [%term %tas tag.e (crip ['%' (trip tag.e)])]]
7313 [%tuple at.e ~[[at.e ~ head] [(span-of val.e) ~ val.e]]]
8020 [%tuple at.e ~[[at.e ~ head] [(span-of val.e) ~ val.e]]]
8022+:: A segment costs one shared step; dynamic segments are not handled yet.
8024+ |= [segs=(list qseg) fuel=@ud]
8028+ ?. ?=(%knot -.i.segs) ~
8029+ $(segs t.segs, fuel (dec fuel))
7315++ infer-fragment
8031++ infer-fragment
7316 |= [e=expr env=ienv state=istate]
8032 |= [e=expr env=ienv state=istate]
7317 ^- iresult
8033 ^- iresult
@@ -7354,6 +8070,21 @@
7354 ?: ?=(%| -.result) result
8070 ?: ?=(%| -.result) result
7355 [%& [%collection %list ~[element]] state.p.result]
8071 [%& [%collection %list ~[element]] state.p.result]
7356 %str (infer-string-pieces pieces.e env state)
8072 %str (infer-string-pieces pieces.e env state)
8074+ ?~ prelude.state [%| ["application path needs the standard prelude in partial inference" ~]]
8075+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
8076+ [%| ["application path needs the standard prelude in partial inference" ~]]
8077+ =/ standard=(unit ischeme) (find-jibb-mold %qath u.prelude.state)
8078+ ?~ standard [%| ["application path needs the standard prelude in partial inference" ~]]
8079+ ?. ?=(~ vars.u.standard) [%| ["application path mold needs unsupported inference" ~]]
8080+ =/ typ=itype typ.u.standard
8081+ ?. ?=(%jrec -.typ) [%| ["application path mold needs unsupported inference" ~]]
8082+ ?. &(=(at.typ /lib/jibb/internal/jibb) =(%qath name.typ) =(%i head.typ) =(%ta aura.typ) =(%t tail.typ))
8083+ [%| ["application path mold needs unsupported inference" ~]]
8084+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8085+ =/ remain=(unit @ud) (qath-static-fuel segs.e (dec jrec-fuel.state))
8086+ ?~ remain [%| ["application path segments need unsupported inference" ~]]
8087+ [%& typ state(jrec-fuel u.remain)]
7358 ?~ names.e [%| ["empty wing" ~]]
8089 ?~ names.e [%| ["empty wing" ~]]
7359 ?^ t.names.e
8090 ?^ t.names.e
@@ -7396,6 +8127,9 @@
7396 [%| ["local molds shadow a name" ~]]
8127 [%| ["local molds shadow a name" ~]]
7397 =/ local-state=istate
8128 =/ local-state=istate
7398 state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
8129 state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
8130+ =/ mold-hole=(unit span) (simple-local-mold-hole defs.e)
8132+ [%| ["type hole needs a determined type" ~[[u.mold-hole "unresolved type hole"]]]]
7399 ?. (local-molds-supported local-molds local-state)
8133 ?. (local-molds-supported local-molds local-state)
7400 [%| ["local molds need unsupported inference" ~]]
8134 [%| ["local molds need unsupported inference" ~]]
7401 =/ values=(list def) (local-value-defs defs.e)
8135 =/ values=(list def) (local-value-defs defs.e)
@@ -7410,9 +8144,10 @@
7410 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
8144 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
7411 (infer-cell-branch e env state ~)
8145 (infer-cell-branch e env state ~)
7412 ?^ t.t.arms.e (infer-known-union-branch e env state)
8146 ?^ t.t.arms.e (infer-known-union-branch e env state)
7413− =/ known=(unit itype) (known-union-subject subject.e env state)
8147+ =/ known=(unit iresult) (known-union-subject subject.e env state)
8148+ ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
7414− ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
8149+ ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
7415− (infer-known-union-branch e env state)
8150+ (infer-known-union-branch-subject e env u.known)
7416 =/ x=arm i.arms.e
8151 =/ x=arm i.arms.e
7417 =/ y=arm i.t.arms.e
8152 =/ y=arm i.t.arms.e
7418 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
8153 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
@@ -7421,7 +8156,7 @@
7421 ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
8156 ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
7422 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
8157 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
7423 (infer-known-union-branch e env state)
8158 (infer-known-union-branch e env state)
7424− ?^ known (infer-known-union-branch e env state)
8159+ ?: &(?=(^ known) ?=(%& -.u.known)) (infer-known-union-branch-subject e env u.known)
7425 ?: =(val.lit.pat.x val.lit.pat.y)
8160 ?: =(val.lit.pat.x val.lit.pat.y)
7426 [%| ["branch does not cover both loobeans" ~]]
8161 [%| ["branch does not cover both loobeans" ~]]
7427 =/ subject=iresult $(e subject.e)
8162 =/ subject=iresult $(e subject.e)
@@ -7462,6 +8197,9 @@
7462 =/ value=iresult
8197 =/ value=iresult
7463 (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
8198 (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
7464 ?: ?=(%| -.value) value
8199 ?: ?=(%| -.value) value
8200+ =/ shape=(unit [source=iwfields target=iwfields])
8201+ (width-shape typ.p.value typ.u.target sub.state.p.value)
8202+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
7465 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
8203 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
7466 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
8204 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
7467 ?: ?=(%bad -.fit)
8205 ?: ?=(%bad -.fit)
@@ -7493,6 +8231,8 @@
7493 [%& [%fn typ.p.sam typ.p.body] state.p.body]
8231 [%& [%fn typ.p.sam typ.p.body] state.p.body]
7495 ?~ args.e [%| ["call has no argument" ~]]
8233 ?~ args.e [%| ["call has no argument" ~]]
8234+ ?: (explicit-proj-call e env state)
8235+ [%| ["proj needs an expected record type" ~]]
7496 (infer-call-with-head e env state (infer-fragment head.e env state))
8236 (infer-call-with-head e env state (infer-fragment head.e env state))
7497 * [%| ["expression is not supported by partial inference" ~]]
8237 * [%| ["expression is not supported by partial inference" ~]]
@@ -7503,6 +8243,20 @@
7504:: Check a call using the head already inferred in this state. Keeping
8244:: Check a call using the head already inferred in this state. Keeping
7505:: this shared avoids evaluating or instantiating a contextual head twice.
8245:: this shared avoids evaluating or instantiating a contextual head twice.
8246+++ width-has-projections
8247+ |= ps=(list iwprojection)
8252++$ iwidth-elaboration [original=expr typ=itype sub=isub projections=(list iwprojection)]
8253+++ infer-width-elaboration
8254+ |= [e=expr env=ienv state=istate]
8255+ ^- (each iwidth-elaboration idiag)
8256+ =/ out=iresult (infer-fragment e env state)
8257+ ?: ?=(%| -.out) [%| p.out]
8258+ [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
7506++ infer-call-with-head
8260++ infer-call-with-head
7507 |= [e=expr env=ienv state=istate head=iresult]
8261 |= [e=expr env=ienv state=istate head=iresult]
7508 ^- iresult
8262 ^- iresult
@@ -7522,7 +8276,13 @@
7522 =/ st=istate state.p.arg
8276 =/ st=istate state.p.arg
7523 =/ ht=itype (itype-walk typ.p.head sub.st)
8277 =/ ht=itype (itype-walk typ.p.head sub.st)
7524 ?: ?=(%fn -.ht)
8278 ?: ?=(%fn -.ht)
8279+ =/ shape=(unit [source=iwfields target=iwfields])
8281+ (width-shape typ.p.arg sample.ht sub.st)
8282+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
8284+ ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
7525− =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
8285+ (itype-fit typ.p.arg sample.ht sub.st next.st)
7526 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
8286 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
7527 ?: ?=(%bad -.fit)
8287 ?: ?=(%bad -.fit)
7528 ?~ t.args.e
8288 ?~ t.args.e
@@ -7538,7 +8298,10 @@
7538 =/ arg-at=span ?~(bad whole-args at.u.bad)
8298 =/ arg-at=span ?~(bad whole-args at.u.bad)
7539 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
8299 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7540 [%| ["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)]]]]
8300 [%| ["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)]]]]
8302+ ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
8303+ (itype-face-asym typ.p.arg sample.ht sub.fit)
7541− ?: &((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))
8304+ ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
7542 [%| ["call result face propagation is not supported by partial inference" ~]]
8305 [%| ["call result face propagation is not supported by partial inference" ~]]
7543 [%& product.ht st(sub sub.fit, next next.fit)]
8306 [%& product.ht st(sub sub.fit, next next.fit)]
7544 =/ result=itype [%var next.st]
8307 =/ result=itype [%var next.st]
@@ -7552,7 +8315,7 @@
7552 ^- (unit [at=span typ=itype])
8315 ^- (unit [at=span typ=itype])
7553 ?~ args ~
8316 ?~ args ~
7554 =/ original=[left=itype right=itype] [actual expected]
8317 =/ original=[left=itype right=itype] [actual expected]
7555− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
8318+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%rvar -.left.original) |(?=(%nvar -.left.original) ?=(%rnvar -.left.original)) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%rvar -.right.original) |(?=(%nvar -.right.original) ?=(%rnvar -.right.original))) ~
7556 =. actual (itype-walk actual sub)
8319 =. actual (itype-walk actual sub)
7557 =. expected (itype-walk expected sub)
8320 =. expected (itype-walk expected sub)
7558 ?: &(?=(%face -.expected) !?=(%face -.actual))
8321 ?: &(?=(%face -.expected) !?=(%face -.actual))
@@ -7602,9 +8365,10 @@
7602 [%| ["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)]]]]
8365 [%| ["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)]]]]
7603 [%& expected state.p.value(sub sub.fit, next next.fit)]
8366 [%& expected state.p.value(sub sub.fit, next next.fit)]
7605−:: A known gate whose result is still an inference variable can receive
7606−:: an enclosing target before its argument is inferred. Other products
8368+:: A known gate may receive an enclosing target before its argument is
8369+:: inferred when its result is open or a direct, matching named generic
8370+:: union. Opaque, recursive, tag-constrained and variable-bound union
7607−:: and unresolved calls use the existing directional path unchanged.
8371+:: results keep the existing directional path.
7608++ infer-contextual-call
8372++ infer-contextual-call
7609 |= [e=expr expected=itype env=ienv state=istate]
8373 |= [e=expr expected=itype env=ienv state=istate]
7610 ^- iresult
8374 ^- iresult
@@ -7615,13 +8379,181 @@
7615 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
8379 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
7616 ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
8380 ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
7617 =/ result=itype (itype-walk product.ht sub.state.p.head)
8381 =/ result=itype (itype-walk product.ht sub.state.p.head)
8383+ ?: ?=(%var -.result) &
8384+ :: A direct known generic union may receive the same nominal result
8385+ :: context before its arguments are checked. Variable-bound origins,
8386+ :: pending tags, recursive identities and unknown atoms stay open.
8387+ ?. &(?=(%union -.product.ht) ?=(%union -.result) ?=(%union -.expected)) |
8389+ ?. =(origin.result origin.expected) |
8391+ ?. =((lent args.result) (lent args.expected)) |
8392+ ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
8393+ ?: |((itype-has-recursive (itype-normalize result sub.state.p.head)) (itype-has-recursive (itype-normalize expected sub.state.p.head))) |
8394+ ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
7618− ?. ?=(%var -.result) (infer-call-with-head e env state head)
8396+ ?. eligible (infer-call-with-head e env state head)
7619− ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected) (itype-has-tag (itype-normalize expected sub.state.p.head)))
8397+ ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)) (itype-has-tag (itype-normalize expected sub.state.p.head)))
7620 (infer-call-with-head e env state head)
8398 (infer-call-with-head e env state head)
7621 =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
8399 =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
7622 ?~ sub (infer-call-with-head e env state head)
8400 ?~ sub (infer-call-with-head e env state head)
7623 (infer-call-with-head e env state [%& typ.p.head state.p.head(sub u.sub)])
8401 (infer-call-with-head e env state [%& typ.p.head state.p.head(sub u.sub)])
8403+:: An eligible fully faced literal receives context by name, in source order.
8404+++ width-literal-fields
8405+ |= [items=(list item) axis=@ud fuel=@ud]
8407+ =/ order=(list iwfield) ~
8408+ =/ index=(map term iwfield) *(map term iwfield)
8413+ =/ at-axis=@ud ?~(t.items axis (mul 2 axis))
8414+ =/ entry=iwfield [u.face.i.items at-axis [%noun ~]]
8415+ ?: ?=(^ (~(get by index) name.entry)) ~
8416+ =. index (~(put by index) name.entry entry)
8417+ =. order [entry order]
8418+ ?~ t.items `[(flop order) index]
8419+ $(items t.items, axis +((mul 2 axis)), fuel (dec fuel))
8420+++ width-infer-items
8421+ |= [items=(list item) expected=(map term iwfield) env=ienv state=istate context=span]
8423+ ?~ items [%| ["empty record is not supported" ~]]
8424+ ?~ face.i.items [%| ["record face needs unsupported inference" ~]]
8425+ =/ field=(unit iwfield) (~(get by expected) u.face.i.items)
8427+ ?~ field (infer-fragment val.i.items env state)
8428+ (infer-call-context-arg val.i.items typ.u.field env state context)
8429+ ?: ?=(%| -.head) head
8430+ =/ typ=itype [%face u.face.i.items typ.p.head]
8431+ ?~ t.items [%& typ state.p.head]
8432+ =/ tail=iresult $(items t.items, state state.p.head)
8433+ ?: ?=(%| -.tail) tail
8434+ [%& [%cell typ typ.p.tail] state.p.tail]
8435+++ width-infer-literal
8436+ |= [e=expr expected=itype env=ienv state=istate context=span]
8438+ ?. ?=(%tuple -.e) ~
8439+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) ~
8440+ =/ source=(unit iwfields) (width-literal-fields items.e 1 4.096)
8441+ =/ target=(unit iwfields) (width-scan expected sub.state 1 4.096)
8444+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
8445+ ?. (width-in-order order.u.source order.u.target)
8446+ `(infer-simple-items items.e env state)
8447+ `(width-infer-items items.e index.u.target env state context)
8449+:: Experimental intrinsic recognition; real bindings retain normal calls.
8450+++ explicit-proj-call
8451+ |= [e=expr env=ienv state=istate]
8454+ ?. ?=([* ~] args.e) |
8455+ ?. ?=(%wing -.head.e) |
8456+ ?. =(names.head.e ~[%proj]) |
8457+ ?: ?=(^ (ienv-lookup %proj env)) |
8458+ ?: (lien globals.state |=(n=term =(n %proj))) |
8460+ ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
8461+++ infer-proj-source
8462+ |= [e=expr expected=itype env=ienv state=istate context=span]
8464+ ?: ?=(%group -.e) $(e inner.e)
8465+ =/ literal=(unit iresult) (width-infer-literal e expected env state context)
8466+ ?^ literal u.literal
8467+ (infer-fragment e env state)
8468+++ infer-proj-context
8469+ |= [e=expr expected=itype env=ienv state=istate context=span]
8472+ ?~ args.e [%| ["proj needs one record" ~]]
8473+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) [%| ["proj needs an expected record type" ~]]
8474+ =/ value=iresult (infer-proj-source i.args.e expected env state context)
8475+ ?: ?=(%| -.value) value
8476+ =/ shape=(unit [source=iwfields target=iwfields])
8477+ (width-proj-shape typ.p.value expected sub.state.p.value)
8478+ ?~ shape [%| ["proj needs a known record containing its expected fields" ~]]
8479+ =/ project=(unit iwidth-result) (width-project u.shape sub.state.p.value next.state.p.value)
8480+ ?~ project [%| ["proj constraint needs unsupported inference" ~]]
8481+ =/ st=istate state.p.value(sub sub.u.project, next next.u.project)
8482+ [%& expected st(projections [[at.e e typ.p.value expected steps.u.project] projections.st])]
8484+:: A known literal singleton in a direct union can contextualize a
8485+:: loobean literal of the same noun. Only explicit singleton and cell
8486+:: competitors are considered; opaque or variable cases stay unknown.
8487+++ explicit-singleton-in-union
8488+ |= [t=itype noun=@]
8490+ ?. ?=(%union -.t) |
8491+ =/ cases=(list itype) cases.t
8496+ ?: ?=(%cell -.c) $(cases t.cases)
8497+ ?. ?=(%const -.c) |
8498+ ?: =(noun val.literal.c)
8500+ $(cases t.cases, found &)
8503+:: Select a written literal-headed case only when every competing case is
8504+:: also an explicit singleton-headed cell and exactly one matches. Opaque,
8505+:: variable-bound and differently shaped cases keep inference unchanged.
8506+:: This first slice supplies context to a directly called payload. Plain
8507+:: literal data and other expressions retain their existing inference path.
8508+++ contextual-atomic-arguments
8509+ |= args=(list expr)
8512+ ?. ?=(?(%lit %wing %ctor) -.i.args) |
8514+++ contextual-direct-payload-call
8517+ ?: ?=(%group -.e) $(e inner.e)
8519+ ?. ?=(%wing -.head.e) |
8521+ (contextual-atomic-arguments args.e)
8523+:: A walked variable may have concealed a union inside a substituted
8524+:: structure before this arm was called. Decline in that case rather than
8525+:: deriving provenance from the already-walked type.
8526+++ contextual-simple-sub
8530+ ?: ?=(?(%cell %face %fn %union %collection) -.val.i.sub) |
8533+++ contextual-direct-union
8536+ ?: ?=(%face -.target) $(target body.target)
8537+ ?=(%union -.target)
8538+++ contextual-tagged-case
8539+ |= [target=itype tag=@ sub=isub]
8541+ ?. ?=(%union -.target) ~
8542+ =/ remaining=(list itype) cases.target
8543+ =/ found=(unit itype) ~
8544+ =/ seen=(set @) *(set @)
8547+ =/ c=itype i.remaining
8549+ =/ head=itype hed.c
8550+ ?. ?=(%const -.head) ~
8551+ ?: (~(has in:..zuse seen) val.literal.head) ~
8552+ =. seen (~(put in:..zuse seen) val.literal.head)
8553+ ?: =(tag val.literal.head)
8554+ $(remaining t.remaining, found `c)
8555+ $(remaining t.remaining)
7625++ infer-call-context-arg
8557++ infer-call-context-arg
7626 |= [e=expr expected=itype env=ienv state=istate context=span]
8558 |= [e=expr expected=itype env=ienv state=istate context=span]
7627 ^- iresult
8559 ^- iresult
@@ -7635,25 +8567,43 @@
7635 =/ target=itype (itype-walk expected sub.state)
8567 =/ target=itype (itype-walk expected sub.state)
7637 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8569 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8570+ ?: (explicit-proj-call e env state)
8571+ (infer-proj-context e expected env state context)
8572+ :: Only the source-proven one-layer cell is exposed. Each recursive
8573+ :: descent consumes one written tuple; named values use ordinary fit.
8574+ ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
8575+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8576+ [%& target state(jrec-fuel (dec jrec-fuel.state))]
8577+ ?: &(?=(%jrec -.target) ?=(%tuple -.e))
8578+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8579+ =. state state(jrec-fuel (dec jrec-fuel.state))
8581+ [%cell [%face head.target [%atom aura.target]] [%face tail.target target]]
8582+ =/ value=iresult (infer-call-context-items items.e shape env state context)
8583+ ?: ?=(%| -.value) value
8584+ =/ fit=ifit (itype-fit typ.p.value shape sub.state.p.value next.state.p.value)
8585+ ?: ?=(%unknown -.fit) [%| ["recursive mold cell constraint needs unsupported inference" ~]]
8586+ ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
8587+ [%& target state.p.value(sub sub.fit, next next.fit)]
7638 ?: ?=(%call -.e) (infer-contextual-call e target env state)
8588 ?: ?=(%call -.e) (infer-contextual-call e target env state)
7639 ?: (single-structured-pattern e)
8589 ?: (single-structured-pattern e)
7640 (infer-single-case-branch e env state `[target context])
8590 (infer-single-case-branch e env state `[target context])
7641 ?: (cell-binder-pattern e)
8591 ?: (cell-binder-pattern e)
7642 (infer-cell-branch e env state `[target context])
8592 (infer-cell-branch e env state `[target context])
7643− :: In a loobean-singleton context retain the written loobean noun;
8593+ :: In an explicit singleton context retain the written loobean noun;
7644− :: the usual final fit decides whether that value is permitted.
8594+ :: the ordinary singleton fit compares its noun, not its spelling.
7645 =/ singleton=(unit itype)
8595 =/ singleton=(unit itype)
7646 ?. ?=(%lit -.e) ~
8596 ?. ?=(%lit -.e) ~
7647 ?. =(%loobean form.lit.e) ~
8597 ?. =(%loobean form.lit.e) ~
7648− ?. ?=(%const -.target) ~
8598+ ?. |(?=(%const -.target) &(?=(%union -.expected) (explicit-singleton-in-union expected val.lit.e))) ~
7649− ?. =(%loobean form.literal.target) ~
7650 `[%const lit.e]
8599 `[%const lit.e]
7651 ?^ singleton [%& u.singleton state]
8600 ?^ singleton [%& u.singleton state]
7652− =/ known=(unit itype)
8601+ =/ known=(unit iresult)
7653 ?: ?=(%branch -.e) (known-union-subject subject.e env state)
8602 ?: ?=(%branch -.e) (known-union-subject subject.e env state)
8604+ ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
7655− ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
8605+ ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
7656− (infer-known-union-context e target env state context)
8606+ (infer-known-union-context-subject e target env u.known context)
7657 ?: &(?=(%union -.target) ?=(%unit -.e))
8607 ?: &(?=(%union -.target) ?=(%unit -.e))
7658 (infer-unit-context e target env state context)
8608 (infer-unit-context e target env state context)
7659 ?: &(?=(%flag -.target) (context-union-branch e))
8609 ?: &(?=(%flag -.target) (context-union-branch e))
@@ -7664,17 +8614,53 @@
7664 (infer-union-context e target env state context)
8614 (infer-union-context e target env state context)
7665 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
8615 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
7666 (infer-list-context e target env state context)
8616 (infer-list-context e target env state context)
8617+ :: A literal-headed tuple can receive the unique case's payload
8618+ :: context. The ordinary final fit still checks the complete union.
8619+ =/ selected=(unit itype)
8620+ ?. &((contextual-simple-sub sub.state) (contextual-direct-union expected) ?=(%union -.target) ?=(%tuple -.e) ?=(^ items.e)) ~
8623+ ?. (contextual-direct-payload-call val.i.t.items.e) ~
8624+ =/ first=item i.items.e
8625+ ?. &(?=(~ face.first) ?=(%lit -.val.first) |(=(%term form.lit.val.first) =(%null form.lit.val.first) =(%loobean form.lit.val.first))) ~
8626+ (contextual-tagged-case target val.lit.val.first sub.state)
8629+ :: On this bounded shallow-call shape, preserve any inference that
8630+ :: already fits before trying the new contextual path. Neither pass
8631+ :: can recursively select a nested tuple from the atomic arguments.
8632+ =/ ordinary=(unit iresult)
8633+ =/ initial=iresult (infer-fragment e env state)
8634+ ?: ?=(%| -.initial) ~
8635+ =/ fit=ifit (itype-fit typ.p.initial target sub.state.p.initial next.state.p.initial)
8638+ ?^ ordinary u.ordinary
8639+ =/ value=iresult (infer-call-context-items items.e u.selected env state context)
8640+ ?: ?=(%| -.value) value
8641+ =/ fit=ifit (itype-fit typ.p.value u.selected sub.state.p.value next.state.p.value)
8642+ ?: ?=(%unknown -.fit) [%| ["tagged case needs unsupported inference" ~]]
8643+ ?: ?=(%bad -.fit) [%| ["tagged case does not fit its expected type" ~[[context "expected union case"] [(span-of e) "value"]]]]
8644+ [%& typ.p.value state.p.value(sub sub.fit, next next.fit)]
7667 ?: &(?=(%cell -.target) ?=(%tuple -.e))
8645 ?: &(?=(%cell -.target) ?=(%tuple -.e))
7668 (infer-call-context-items items.e target env state context)
8646 (infer-call-context-items items.e target env state context)
7669 (infer-fragment e env state)
8647 (infer-fragment e env state)
7671:: Preserve each written face; the final complete sample fit checks faces.
8649:: Preserve each written face; the final complete sample fit checks faces.
8650+:: A tuple or positional field face belongs to the enclosing sample,
8651+:: not to the expression at that position. A second face, if present,
8652+:: is part of the value's own expected type.
8653+++ projection-field-target
8656+ ?:(?=(%face -.expected) body.expected expected)
7672++ infer-call-context-items
8658++ infer-call-context-items
7673 |= [items=(list item) expected=itype env=ienv state=istate context=span]
8659 |= [items=(list item) expected=itype env=ienv state=istate context=span]
7674 ^- iresult
8660 ^- iresult
7675 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
8661 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
7676 ?~ t.items
8662 ?~ t.items
7677− =/ last=iresult (infer-call-context-arg val.i.items expected env state context)
8663+ =/ last=iresult (infer-call-context-arg val.i.items (projection-field-target expected) env state context)
7678 ?: ?=(%| -.last) last
8664 ?: ?=(%| -.last) last
7679 =/ typ=itype typ.p.last
8665 =/ typ=itype typ.p.last
7680 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8666 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
@@ -7683,7 +8669,7 @@
7684 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8670 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7685 ?. ?=(%cell -.target) (infer-simple-items items env state)
8671 ?. ?=(%cell -.target) (infer-simple-items items env state)
7686− =/ head=iresult (infer-call-context-arg val.i.items hed.target env state context)
8672+ =/ head=iresult (infer-call-context-arg val.i.items (projection-field-target hed.target) env state context)
7687 ?: ?=(%| -.head) head
8673 ?: ?=(%| -.head) head
7688 =/ typ=itype typ.p.head
8674 =/ typ=itype typ.p.head
7689 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8675 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
@@ -7695,13 +8681,13 @@
7695 |= [args=(list expr) expected=itype env=ienv state=istate context=span]
8681 |= [args=(list expr) expected=itype env=ienv state=istate context=span]
7696 ^- iresult
8682 ^- iresult
7697 ?~ args [%| ["call has no argument" ~]]
8683 ?~ args [%| ["call has no argument" ~]]
7698− ?~ t.args (infer-call-context-arg i.args expected env state context)
8684+ ?~ t.args (infer-call-context-arg i.args (projection-field-target expected) env state context)
7699 =/ target=itype (itype-walk expected sub.state)
8685 =/ target=itype (itype-walk expected sub.state)
7701 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8687 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7702 ?. ?=(%cell -.target)
8688 ?. ?=(%cell -.target)
7703 (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
8689 (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
7704− =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
8690+ =/ head=iresult (infer-call-context-arg i.args (projection-field-target hed.target) env state context)
7705 ?: ?=(%| -.head) head
8691 ?: ?=(%| -.head) head
7706 =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
8692 =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
7707 ?: ?=(%| -.tail) tail
8693 ?: ?=(%| -.tail) tail
@@ -7733,7 +8719,7 @@
7733 ?~ pats [%& ~]
8719 ?~ pats [%& ~]
7734 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
8720 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
7735 =/ name=term name.i.pats
8721 =/ name=term name.i.pats
7736− ?: |(?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
8722+ ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
7737 [%| 'pattern shadows a name']
8723 [%| 'pattern shadows a name']
7738 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
8724 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
7739 ?: ?=(%| -.rest) rest
8725 ?: ?=(%| -.rest) rest
@@ -7758,7 +8744,7 @@
7758 ?~ t.names |
8744 ?~ t.names |
7759 =. typ (itype-walk typ sub)
8745 =. typ (itype-walk typ sub)
7760 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8746 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
7761− |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
8747+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
7763++ cell-binder-pattern
8749++ cell-binder-pattern
7764 |= e=expr
8750 |= e=expr
@@ -7816,9 +8802,15 @@
7817 ?: (lth id.t 26) [(add 65 id.t) ~]
8803 ?: (lth id.t 26) [(add 65 id.t) ~]
7818 "T{<id.t>}"
8804 "T{<id.t>}"
8806+ ?: (lth id.t 26) [(add 65 id.t) ~]
7820 ?: (lth id.t 26) [(add 65 id.t) ~]
8809 ?: (lth id.t 26) [(add 65 id.t) ~]
7821 "T{<id.t>}"
8810 "T{<id.t>}"
8812+ ?: (lth id.t 26) [(add 65 id.t) ~]
7822 %atom "@{(trip aura.t)}"
8814 %atom "@{(trip aura.t)}"
7823 %any-atom "@"
8815 %any-atom "@"
7824 %flag "?"
8816 %flag "?"
@@ -7830,6 +8822,7 @@
7830 ?~ args.t (trip u.label.t)
8822 ?~ args.t (trip u.label.t)
7831 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
8823 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
7832 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8824 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8825+ %jrec ?~(label.t "recursive mold" (trip u.label.t))
7833 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
8826 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
7834 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
8827 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
7835 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
8828 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -7865,8 +8858,10 @@
7866 ?- -.typ
8859 ?- -.typ
7871 %any-atom |
8866 %any-atom |
@@ -7875,6 +8870,7 @@
7875 %const |
8870 %const |
7876 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
8871 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
7877 %recursive |
8872 %recursive |
7878 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
8874 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
7879 %face $(typ body.typ)
8875 %face $(typ body.typ)
7880 %fn |($(typ sample.typ) $(typ product.typ))
8876 %fn |($(typ sample.typ) $(typ product.typ))
@@ -7885,7 +8881,7 @@
7885 |= [label=tape typ=itype sub=isub]
8881 |= [label=tape typ=itype sub=isub]
7887 =/ normalized=itype (itype-normalize typ sub)
8883 =/ normalized=itype (itype-normalize typ sub)
7888− ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
8884+ ?: |(?=(%var -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
7889 ?: (itype-has-hidden-recursive normalized) label
8885 ?: (itype-has-hidden-recursive normalized) label
7890 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
8886 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
7891 ?: (gth (lent vars) 26) label
8887 ?: (gth (lent vars) 26) label
@@ -7907,6 +8903,7 @@
7907 ?+ -.resolved ~
8903 ?+ -.resolved ~
7908 %var `id.resolved
8904 %var `id.resolved
7909 %avar `id.resolved
8905 %avar `id.resolved
7911 ?~ ident $(caps t.caps)
8908 ?~ ident $(caps t.caps)
7912 ?: =(n u.ident) &
8909 ?: =(n u.ident) &
@@ -7921,6 +8918,7 @@
7921 ?+ -.resolved ~
8918 ?+ -.resolved ~
7922 %var `id.resolved
8919 %var `id.resolved
7923 %avar `id.resolved
8920 %avar `id.resolved
7925 ?~ ident $(caps t.caps)
8923 ?~ ident $(caps t.caps)
7926 ?: =(n u.ident) `i.caps
8924 ?: =(n u.ident) `i.caps
@@ -7935,6 +8933,7 @@
7935 ?+ -.resolved ~
8933 ?+ -.resolved ~
7936 %var `id.resolved
8934 %var `id.resolved
7937 %avar `id.resolved
8935 %avar `id.resolved
7939 ?~ ident $(caps t.caps)
8938 ?~ ident $(caps t.caps)
7940 =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
8939 =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
@@ -7950,6 +8949,7 @@
7950 ?+ -.resolved ~
8949 ?+ -.resolved ~
7951 %var `id.resolved
8950 %var `id.resolved
7952 %avar `id.resolved
8951 %avar `id.resolved
7954 ?~ ident &
8954 ?~ ident &
7955 ?: (cap-id-in u.ident t.caps sub) &
8955 ?: (cap-id-in u.ident t.caps sub) &
@@ -7964,8 +8964,8 @@
7965 ?~ caps |
8965 ?~ caps |
7966 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8966 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7967− ?: ?=(%avar -.resolved)
8967+ ?: |(?=(%avar -.resolved) ?=(%rvar -.resolved))
7968− ?: =(n id.resolved) &
8968+ ?: =(n +.resolved) &
7969 $(caps t.caps)
8969 $(caps t.caps)
7970 $(caps t.caps)
8970 $(caps t.caps)
@@ -7975,7 +8975,9 @@
7977 %avar =(n id.t)
8977 %avar =(n id.t)
7980 %any-atom |
8982 %any-atom |
@@ -7984,6 +8986,7 @@
7984 %const |
8986 %const |
7985 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
8987 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
7986 %recursive |
8988 %recursive |
7987 %collection (lien args.t |=(c=itype (has-atom-var n c)))
8990 %collection (lien args.t |=(c=itype (has-atom-var n c)))
7988 %face $(t body.t)
8991 %face $(t body.t)
7989 %fn |($(t sample.t) $(t product.t))
8992 %fn |($(t sample.t) $(t product.t))
@@ -8023,6 +9026,10 @@
8023 =/ out=tape ""
9026 =/ out=tape ""
8025 ?~ vars out
9028 ?~ vars out
9029+ ?: (itype-var-is-restricted i.vars t)
9030+ =/ sep=tape ?:(printed ", " " where ")
9031+ =/ clause=tape "{sep}{(show-itype [%rvar i.vars] ~)} is an atom other than ?"
9032+ $(vars t.vars, printed &, out (weld out clause))
8026 ?: (itype-var-is-atom i.vars t)
9033 ?: (itype-var-is-atom i.vars t)
8027 =/ sep=tape ?:(printed ", " " where ")
9034 =/ sep=tape ?:(printed ", " " where ")
8028 =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
9035 =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
@@ -8332,6 +9339,7 @@
8332 ?: (constrained-capitals caps.entry sub.state)
9339 ?: (constrained-capitals caps.entry sub.state)
8333 [%| ["explicit capital constraints are not supported by partial inference" ~]]
9340 [%| ["explicit capital constraints are not supported by partial inference" ~]]
8334 =/ typ=itype (itype-normalize typ.entry sub.state)
9341 =/ typ=itype (itype-normalize typ.entry sub.state)
9342+ ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
8335 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
9343 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
8336 [%| ["recursive group needs unsupported inference" ~]]
9344 [%| ["recursive group needs unsupported inference" ~]]
8337 =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
9345 =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
@@ -8356,35 +9364,64 @@
8356 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
9364 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
8357 =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
9365 =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
8358 ?: ?=(%| -.body) body
9366 ?: ?=(%| -.body) body
9367+ :: Per-member ownership through mutual recursion is not implemented.
9368+ ?: !=(projections.state.p.body projections.state)
9369+ [%| ["record projection in recursive groups needs unsupported inference" ~]]
9370+ ?: !=(holes.state.p.body holes.state)
9371+ [%| ["holes in recursive groups need unsupported inference" ~]]
8359 ?: (pending-tags tags.state.p.body sub.state.p.body)
9372 ?: (pending-tags tags.state.p.body sub.state.p.body)
8360 [%| ["recursive group has unresolved literal constraints" ~]]
9373 [%| ["recursive group has unresolved literal constraints" ~]]
8361 =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
9374 =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
8362 ?: ?=(%| -.schemes) schemes
9375 ?: ?=(%| -.schemes) schemes
8363 [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
9376 [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
9379+ |= [ps=(list iwprojection) sub=isub visible=(list @ud)]
9380+ ^- (unit (list iwprojection))
9382+ ?: (lien t.ps |=(p=iwprojection =(at.p at.i.ps))) ~
9383+ =/ src=itype (default-decimals (itype-normalize source.i.ps sub))
9384+ =/ dst=itype (default-decimals (itype-normalize target.i.ps sub))
9385+ ?: |((itype-has-nvar src) (itype-has-nvar dst) (itype-has-tag src) (itype-has-tag dst)) ~
9386+ =/ vars=(list @ud) (weld (itype-vars src) (itype-vars dst))
9387+ ?. (levy vars |=(n=@ud (lien visible |=(v=@ud =(n v))))) ~
9388+ =/ rest=(unit (list iwprojection)) $(ps t.ps)
9390+ =/ entry=iwprojection i.ps
9391+ =. entry entry(source src, target dst)
8365++ add-supported-defs
9394++ add-supported-defs
8366− |= [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)]
9395+ |= [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)]
8367− ^- ienv
9396+ ^- [env=ienv artifacts=(list iwidth-definition)]
8368− ?~ ds env
9397+ ?~ ds [env artifacts]
8369 =/ d=def i.ds
9398 =/ d=def i.ds
8370 ?: ?=(%mold -.d) $(ds t.ds)
9399 ?: ?=(%mold -.d) $(ds t.ds)
8371 ?. (unique-value-name name.d globals) $(ds t.ds)
9400 ?. (unique-value-name name.d globals) $(ds t.ds)
8372 ?^ (ienv-lookup name.d env) $(ds t.ds)
9401 ?^ (ienv-lookup name.d env) $(ds t.ds)
8373 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9402 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8374− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
9403+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
8375 =. initial (reserve-def-caps val.d initial)
9404 =. initial (reserve-def-caps val.d initial)
8376 =/ result=iresult (infer-fragment val.d env initial)
9405 =/ result=iresult (infer-fragment val.d env initial)
8377 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
9406 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
8378 ?: ?=(%| -.result) $(ds t.ds)
9407 ?: ?=(%| -.result) $(ds t.ds)
9408+ =. state.p.result (promote-restricted-numbers state.p.result env)
9409+ =. 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)))
9410+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
8379 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
9411 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
8380 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
9412 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
8381 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
9413 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
8382 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
9414 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
8383 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
9415 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8384 ?: (gth (lent vars) 26) $(ds t.ds)
9416 ?: (gth (lent vars) 26) $(ds t.ds)
9417+ =/ finalized=(unit (list iwprojection))
9418+ (width-finalize projections.state.p.result sub.state.p.result vars)
9419+ ?~ finalized $(ds t.ds)
9420+ =? artifacts ?=(^ u.finalized)
9421+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
8385 $(ds t.ds, env [[name.d [typ vars]] env])
9422 $(ds t.ds, env [[name.d [typ vars]] env])
8387−+$ iresolved [env=ienv grouped=(list term)]
9424++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
8388+$ iadj (map term (list term))
9425+$ iadj (map term (list term))
8389+$ ivisited (map term ?)
9426+$ ivisited (map term ?)
8390+$ iwork (list [name=term done=?])
9427+$ iwork (list [name=term done=?])
@@ -8478,9 +9515,9 @@
8478 (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
9515 (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
8480++ add-groups
9517++ add-groups
8481− |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) state=istate]
9518+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
8482 ^- iresolved
9519 ^- iresolved
8483− ?~ components [env grouped]
9520+ ?~ components [env grouped artifacts]
8484 =/ component=(list term) i.components
9521 =/ component=(list term) i.components
8485 ?. (graph-cycle component graph) $(components t.components)
9522 ?. (graph-cycle component graph) $(components t.components)
8486 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
9523 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -8499,17 +9536,19 @@
8499 ^- iresolved
9536 ^- iresolved
8500 =/ env=ienv ~
9537 =/ env=ienv ~
8501 =/ grouped=(list term) ~
9538 =/ grouped=(list term) ~
9539+ =/ artifacts=(list iwidth-definition) ~
8502 =/ names=(list term) (global-value-names ds)
9540 =/ names=(list term) (global-value-names ds)
8503 =/ nameset=ivisited (graph-nameset names ~)
9541 =/ nameset=ivisited (graph-nameset names ~)
8504 =/ graph=iadj (graph-make-forward ds nameset ~)
9542 =/ graph=iadj (graph-make-forward ds nameset ~)
8505 =/ components=icomponents (graph-components ds names)
9543 =/ components=icomponents (graph-components ds names)
8506 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9544 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9546+ =/ next=[env=ienv artifacts=(list iwidth-definition)]
8508− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
9547+ (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)
8509− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
9548+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
8510− =/ out=iresolved (add-groups ds components graph next grouped initial)
9549+ =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
8511 ?: =(env env.out) out
9550 ?: =(env env.out) out
8512− $(env env.out, grouped grouped.out)
9551+ $(env env.out, grouped grouped.out, artifacts artifacts.out)
8514++ resolve-supported-defs
9553++ resolve-supported-defs
8515 |= [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)]
9554 |= [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)]
@@ -8768,11 +9807,142 @@
8768 [at.first at.second (union-relate a (project-union-mold second molds ~))]
9807 [at.first at.second (union-relate a (project-union-mold second molds ~))]
8769 (weld pairs $(cases t.cases))
9808 (weld pairs $(cases t.cases))
9810+:: A closed structural mold supplies no equation to determine a hole.
9811+:: Applications, references, unbound capitals and unions are unproved.
9814+ ^- (unit (unit span))
9815+ ?: ?=(%generic -.sh)
9817+ ?. (distinct-params vars.sh) ~
9818+ (simple-mold-hole-in body.sh vars.sh)
9819+ (simple-mold-hole-in sh ~)
9820+++ simple-mold-hole-in
9821+ |= [sh=shape vars=(list @t)]
9822+ ^- (unit (unit span))
9825+ ?(%aura %noun %void %flag %const) `~
9826+ %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
9827+ %cell (simple-mold-field-holes fields.sh vars)
9829+ =/ a=(unit (unit span)) $(sh sample.sh)
9831+ =/ b=(unit (unit span)) $(sh product.sh)
9837+++ simple-mold-field-holes
9838+ |= [fields=(list field) vars=(list @t)]
9839+ ^- (unit (unit span))
9841+ =/ f=field i.fields
9842+ =/ first=(unit (unit span))
9844+ %face (simple-mold-hole-in shape.f vars)
9845+ %bare (simple-mold-hole-in shape.f vars)
9849+ =/ rest=(unit (unit span)) $(fields t.fields)
9851+ `?~(u.first u.rest u.first)
9852+++ simple-local-mold-hole
9856+ ?. ?=(%mold -.i.defs) $(defs t.defs)
9857+ =/ found=(unit (unit span)) (simple-mold-hole shape.i.defs)
9858+ ?~ found $(defs t.defs)
9862+:: A partial prelude may omit unsupported declarations, but may not
9863+:: publish an interface while a named mold's hole remains unchecked.
9869+ %path (lien segs.sh |=(s=pseg ?=(%inferred -.s)))
9870+ %apply (lien args.sh shape-has-hole)
9871+ %union (lien cases.sh shape-has-hole)
9872+ %cell (lien fields.sh field-has-hole)
9873+ %fn |($(sh sample.sh) $(sh product.sh))
9874+ %generic $(sh body.sh)
9881+ %face (shape-has-hole shape.f)
9882+ %bare (shape-has-hole shape.f)
9885+++ named-mold-has-hole
9889+ ?: &(?=(%mold -.i.ds) (shape-has-hole shape.i.ds)) &
9896+ %face (shape-has-hole shape.sam)
9897+ %bare (shape-has-hole shape.sam)
9898+ %cell (lien items.sam sample-has-hole)
9905+ %mold (shape-has-hole shape.d)
9906+ %value (expr-has-hole val.d)
9912+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9913+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9914+ %change (lien edits.e |=(p=edit (expr-has-hole val.p)))
9917+ %group $(e inner.e)
9918+ %list (lien items.e expr-has-hole)
9919+ %tuple (lien items.e |=(i=item (expr-has-hole val.i)))
9920+ ?(%gate %gate-wide) |((sample-has-hole sample.e) $(e body.e))
9921+ %cast |((shape-has-hole shape.e) $(e val.e))
9922+ %call |($(e head.e) (lien args.e expr-has-hole))
9923+ %trace |($(e val.e) $(e then.e))
9924+ %branch |($(e subject.e) (lien arms.e |=(a=arm (expr-has-hole val.a))))
9925+ %body |((lien defs.e def-has-hole) $(e final.e))
9928+++ hole-values-present
9929+ |= [ds=(list def) env=ienv]
9932+ ?. ?=(%value -.i.ds) $(ds t.ds)
9933+ ?: (expr-has-hole val.i.ds)
9934+ ?. ?=(^ (ienv-lookup name.i.ds env)) |
8771++ show-partial-mold
9937++ show-partial-mold
8772 |= [file=path src=@t d=def molds=imolds]
9938 |= [file=path src=@t d=def molds=imolds]
8774 ?> ?=(%mold -.d)
9940 ?> ?=(%mold -.d)
8775 =/ sh=shape shape.d
9941 =/ sh=shape shape.d
9942+ =/ hole=(unit (unit span)) (simple-mold-hole sh)
9943+ ?: &(?=(^ hole) ?=(^ u.hole))
9944+ =/ text=@t (show-error src [file line.beg.u.u.hole col.beg.u.u.hole "unresolved type hole"])
9945+ (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])
8776 =? sh ?=(%generic -.sh) body.sh
9946 =? sh ?=(%generic -.sh) body.sh
8777 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
9947 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
8778 =/ pairs=(list upair) (union-pairs cases.sh molds)
9948 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -8799,6 +9969,21 @@
8799 (show-error src [file line.beg.at.site col.beg.at.site note.site])
9969 (show-error src [file line.beg.at.site col.beg.at.site note.site])
8800 (of-wain:format [summary excerpts])
9970 (of-wain:format [summary excerpts])
9972+:: Both written field sites are shown in the source that declares them.
9973+++ show-duplicate-fields
9974+ |= [file=path src=@t diagnostic=idiag]
9976+ =/ excerpts=(list @t)
9977+ %+ turn sites.diagnostic
9978+ |= site=[at=span note=tape]
9979+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
9980+ (of-wain:format [(crip msg.diagnostic) excerpts])
9982+++ duplicate-fields-report
9983+ |= [file=path src=@t diagnostic=idiag]
9985+ (of-wain:format ~['partial inference; module not checked' (show-duplicate-fields file src diagnostic)])
8802:: +golden-types: a partial report; it does not claim the module checks
9987:: +golden-types: a partial report; it does not claim the module checks
8804++ golden-types
9989++ golden-types
@@ -8828,6 +10013,180 @@
8828+$ jfile-result (each [iface=ifile cache=jcache] @t)
10013+$ jfile-result (each [iface=ifile cache=jcache] @t)
8829+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
10014+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
10016+:: Written record fields each have their own lexical record scope.
10017++$ written-fields (map term span)
10018+++ duplicate-written-field
10019+ |= [name=term at=span seen=written-fields]
10021+ =/ prior=(unit span) (~(get by seen) name)
10023+ `["record field `{(trip name)}` is repeated" ~[[u.prior "first field"] [at "repeated field"]]]
10024+++ duplicate-shapes
10025+ |= xs=(list shape)
10028+ =/ first (duplicate-shape i.xs)
10031+++ duplicate-fields
10032+ |= [fields=(list field) seen=written-fields]
10035+ =/ f=field i.fields
10042+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.f seen))
10044+ =/ inner=(unit idiag)
10046+ %face (duplicate-shape shape.f)
10048+ %bare (duplicate-shape shape.f)
10051+ $(fields t.fields, seen ?~(n seen (~(put by seen) u.n at.f)))
10056+ %cell (duplicate-fields fields.s ~)
10057+ %apply (duplicate-shapes args.s)
10058+ %union (duplicate-shapes cases.s)
10060+ =/ left (duplicate-shape sample.s)
10062+ (duplicate-shape product.s)
10063+ %generic (duplicate-shape body.s)
10066+++ duplicate-samples
10067+ |= [items=(list sample) seen=written-fields]
10070+ =/ a=sample i.items
10078+ =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.a seen))
10080+ =/ inner (duplicate-sample a)
10082+ $(items t.items, seen ?~(n seen (~(put by seen) u.n at.a)))
10083+++ duplicate-sample
10087+ %cell (duplicate-samples items.s ~)
10088+ %face (duplicate-shape shape.s)
10089+ %bare (duplicate-shape shape.s)
10096+ =/ first (duplicate-expr i.xs)
10100+ |= [items=(list item) seen=written-fields]
10104+ =/ dup=(unit idiag) ?~(face.a ~ (duplicate-written-field u.face.a at.a seen))
10106+ =/ inner (duplicate-expr val.a)
10108+ $(items t.items, seen ?~(face.a seen (~(put by seen) u.face.a at.a)))
10109+++ duplicate-pieces
10110+ |= pieces=(list piece)
10113+ =/ first=(unit idiag) ?:(?=(%expr -.i.pieces) (duplicate-expr p.i.pieces) ~)
10115+ $(pieces t.pieces)
10117+ |= segs=(list qseg)
10120+ =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
10124+ |= edits=(list edit)
10127+ =/ first (duplicate-expr val.i.edits)
10131+ |= arms=(list arm)
10134+ =/ first (duplicate-expr val.i.arms)
10138+ |= defs=(list def)
10141+ =/ first=(unit idiag)
10143+ %mold (duplicate-shape shape.i.defs)
10144+ %value (duplicate-expr val.i.defs)
10152+ %str (duplicate-pieces pieces.e)
10153+ %qath (duplicate-qsegs segs.e)
10154+ %change (duplicate-edits edits.e)
10155+ %pair (duplicate-expr val.e)
10156+ %unit (duplicate-expr val.e)
10157+ %group (duplicate-expr inner.e)
10158+ %list (duplicate-exprs items.e)
10159+ %tuple (duplicate-items items.e ~)
10161+ =/ first (duplicate-sample sample.e)
10163+ (duplicate-expr body.e)
10165+ =/ first (duplicate-sample sample.e)
10167+ (duplicate-expr body.e)
10169+ =/ first (duplicate-shape shape.e)
10171+ (duplicate-expr val.e)
10173+ =/ first (duplicate-expr head.e)
10175+ (duplicate-exprs args.e)
10177+ =/ first (duplicate-expr val.e)
10179+ (duplicate-expr then.e)
10181+ =/ first (duplicate-expr subject.e)
10183+ (duplicate-arms arms.e)
10185+ =/ first (duplicate-defs defs.e)
10187+ (duplicate-expr final.e)
8831++ import-binding-names
10190++ import-binding-names
8832 |= imports=(list import)
10191 |= imports=(list import)
8833 ^- (list term)
10192 ^- (list term)
@@ -8840,6 +10199,60 @@
8841 [n $(imports t.imports)]
10200 [n $(imports t.imports)]
10202+++ reserved-proj-sample
10206+ %bind =(name.sam %proj)
10207+ %face =(name.sam %proj)
10208+ %pun =(name.sam %proj)
10209+ %cell (lien items.sam reserved-proj-sample)
10212+++ reserved-proj-pattern
10216+ %bind =(name.p %proj)
10217+ %cell (lien items.p reserved-proj-pattern)
10220+++ reserved-proj-def
10223+ ?: =(name.d %proj) &
10224+ ?: ?=(%value -.d) (reserved-proj-expr val.d)
10226+++ reserved-proj-expr
10230+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
10231+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
10232+ %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
10235+ %group $(e inner.e)
10236+ %list (lien items.e reserved-proj-expr)
10237+ %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
10238+ ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
10240+ %call |($(e head.e) (lien args.e reserved-proj-expr))
10241+ %trace |($(e val.e) $(e then.e))
10242+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
10243+ %body |((lien defs.e reserved-proj-def) $(e final.e))
10247+++ module-has-reserved-proj
10250+ =/ imported=(list term) (import-binding-names imports.mod)
10251+ =/ vals=(list term) (global-value-names defs.mod)
10252+ =/ molds=imolds (collect-simple-molds defs.mod)
10253+ =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10254+ |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
8843++ module-scope-valid
10256++ module-scope-valid
8844 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
10257 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -8847,6 +10260,7 @@
8847 =/ vals=(list term) (global-value-names defs.mod)
10260 =/ vals=(list term) (global-value-names defs.mod)
8848 =/ molds=imolds (collect-simple-molds defs.mod)
10261 =/ molds=imolds (collect-simple-molds defs.mod)
8849 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10262 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10263+ ?: (module-has-reserved-proj mod) |
8850 ?. %+ levy imported
10264 ?. %+ levy imported
8851 |= n=term
10265 |= n=term
8852 &((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))))
10266 &((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))))
@@ -8928,10 +10342,14 @@
8928 =(var name.i.args.tail)
10342 =(var name.i.args.tail)
8930++ prelude-label
10344++ prelude-label
8931− |= [typ=itype name=term]
10345+ |= [typ=itype name=term vars=(list @ud)]
8932 ^- itype
10346 ^- itype
10347+ ?: ?=(%jrec -.typ) typ(label `name)
8933 ?. ?=(%union -.typ) typ
10348 ?. ?=(%union -.typ) typ
10349+ ?. (identity-union-parameters vars args.typ)
10351+ ?: =(at.u.origin.typ /lib/jibb/internal/jibb) typ(label ~)
8934− ?^ args.typ typ
10352+ typ
8935 typ(label `name)
10353 typ(label `name)
8937++ partial-prelude-molds
10355++ partial-prelude-molds
@@ -8946,7 +10364,7 @@
8946 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
10364 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
8947 ?~ out $(molds t.molds)
10365 ?~ out $(molds t.molds)
8948 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
10366 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
8949− =. typ.template.u.out (prelude-label typ.template.u.out name.m)
10367+ =. typ.template.u.out (prelude-label typ.template.u.out name.m vars.template.u.out)
8950 [[name.m template.u.out] $(molds t.molds)]
10368 [[name.m template.u.out] $(molds t.molds)]
8952:: A compiler-owned interface available only to the dedicated
10370:: A compiler-owned interface available only to the dedicated
@@ -8955,16 +10373,20 @@
8955 ^- ifile
10373 ^- ifile
8956 =/ a=itype [%avar 0]
10374 =/ a=itype [%avar 0]
8957 =/ pair=itype [%cell a a]
10375 =/ pair=itype [%cell a a]
10376+ =/ b=itype [%rvar 0]
10377+ =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
10378+ =/ minus=ischeme [[%fn b b] ~[0]]
8958 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
10379 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
8959− [~[[%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~]
10380+ [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
8961++ infer-private-internal
10382++ infer-private-internal
8962− |= src=@t
10383+ |= [src=@t public-source=@t]
8963 ^- (unit ifile)
10384 ^- (unit ifile)
8964 =/ at=path /lib/jibb/internal/jibb
10385 =/ at=path /lib/jibb/internal/jibb
8965 =/ parsed (parse at src)
10386 =/ parsed (parse at src)
8966 ?: ?=(%| -.parsed) ~
10387 ?: ?=(%| -.parsed) ~
8967 =/ mod=module p.parsed
10388 =/ mod=module p.parsed
10389+ ?^ (duplicate-defs defs.mod) ~
8968 ?~ imports.mod
10390 ?~ imports.mod
8969 =/ built=jfile-result (infer-jibb-file at src ~ ~ ~ ~[at] ~ ~ ~ ~)
10391 =/ built=jfile-result (infer-jibb-file at src ~ ~ ~ ~[at] ~ ~ ~ ~)
8970 ?: ?=(%| -.built) ~
10392 ?: ?=(%| -.built) ~
@@ -8976,15 +10398,65 @@
8976 ?: (lien vals |=(n=term =(n %main))) ~
10398 ?: (lien vals |=(n=term =(n %main))) ~
8977 =/ molds=imolds (collect-simple-molds defs.mod)
10399 =/ molds=imolds (collect-simple-molds defs.mod)
8978 =/ globals=(list term) (weld (import-binding-names imports.mod) vals)
10400 =/ globals=(list term) (weld (import-binding-names imports.mod) vals)
10401+ :: The private source can use the public list and unit molds before the
10402+ :: prelude is otherwise prepared. Re-read the trusted public source here
10403+ :: and admit only its validated canonical templates; do not accept schemes
10404+ :: supplied independently by the caller.
10405+ =/ public=(each module error) (parse /lib/jibb/prelude/jibb public-source)
10406+ ?: ?=(%| -.public) ~
10407+ ?^ (duplicate-defs defs.p.public) ~
10408+ ?. (module-scope-valid p.public ~ ~) ~
10409+ =/ source-molds=imolds (collect-simple-molds defs.p.public)
10410+ =/ written-list=(unit shape) (find-simple-mold %list source-molds)
10411+ =/ source-list=(unit ischeme)
10413+ ?. (standard-prelude-list u.written-list) ~
10414+ `[[%collection %list ~[[%var 0]]] ~[0]]
10415+ :: Derive the public unit template from its actual source, then compare
10416+ :: the complete nominal template before making it available privately.
10417+ =/ unit-decl=(unit shape) (find-simple-mold %unit source-molds)
10418+ =/ source-unit=(unit ischeme)
10420+ =/ unit-molds=imolds ~[[%unit u.unit-decl]]
10421+ =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~]
10422+ =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
10423+ =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
10424+ =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
10426+ ?. (standard-unit-template u.found /lib/jibb/prelude/jibb) ~
10428+ =/ primitive=ifile private-primitive-interface
10429+ =? primitive ?=(^ source-list)
10430+ primitive(molds [[%list u.source-list] molds.primitive])
10431+ =? primitive ?=(^ source-unit)
10432+ primitive(molds [[%unit u.source-unit] molds.primitive])
8979− =/ js=ijimports ~[[face.i.imports.mod private-primitive-interface]]
10433+ =/ js=ijimports ~[[face.i.imports.mod primitive]]
8980 =/ reserved=(list term) ~[face.i.imports.mod]
10434 =/ reserved=(list term) ~[face.i.imports.mod]
8981 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10435 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8982− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~]
10436+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~]
8983 =/ mts=(each imold-types @t) (module-mold-types molds state)
10437 =/ mts=(each imold-types @t) (module-mold-types molds state)
8984− ?: ?=(%| -.mts) ~
10438+ =/ usable=(unit imold-types)
10439+ ?: ?=(%& -.mts) `p.mts
10440+ :: Missing public templates may make an unrelated internal mold
10441+ :: unavailable. Validate all molds once with isolated canonical
10442+ :: templates before admitting only those inferred using the actual
10443+ :: source-backed templates. The proof interface is never exported.
10444+ ?. |(?=(~ source-list) ?=(~ source-unit)) ~
10445+ =/ nil=itype [%const [%null %n 0 '~']]
10446+ =/ canonical-unit=ischeme
10447+ [[%union ~[nil [%cell nil [%face %u [%var 0]]]] `[/lib/jibb/prelude/jibb %unit] `%unit ~[[%var 0]]] ~[0]]
10448+ =/ canonical-list=ischeme [[%collection %list ~[[%var 0]]] ~[0]]
10449+ =/ proof-primitive=ifile private-primitive-interface
10450+ =. molds.proof-primitive ~[[%list canonical-list] [%unit canonical-unit]]
10451+ =/ proof-imports=ijimports ~[[face.i.imports.mod proof-primitive]]
10452+ =/ proof=(each imold-types @t) (module-mold-types molds state(jimports proof-imports))
10453+ ?: ?=(%| -.proof) ~
10454+ `(partial-prelude-molds molds state)
8985− =/ env=ienv (resolve-supported-defs defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
10456+ =/ resolution=iresolved (resolve-groups defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
10457+ =/ env=ienv env.resolution
8986 ?. (module-values-complete defs.mod env) ~
10458 ?. (module-values-complete defs.mod env) ~
8987− `[env p.mts at ~]
10459+ `[env u.usable at ~ artifacts.resolution ~ `src ~]
8989++ partial-prelude-interface-with-internal
10461++ partial-prelude-interface-with-internal
8990 |= [src=@t internal-source=(unit @t)]
10462 |= [src=@t internal-source=(unit @t)]
@@ -8993,12 +10465,14 @@
8993 =/ at=path /lib/jibb/prelude/jibb
10465 =/ at=path /lib/jibb/prelude/jibb
8994 =/ parsed (parse at src)
10466 =/ parsed (parse at src)
8995 ?: ?=(%| -.parsed) ~
10467 ?: ?=(%| -.parsed) ~
10468+ ?: (named-mold-has-hole defs.p.parsed) ~
10469+ ?^ (duplicate-defs defs.p.parsed) ~
8996 =/ private=(unit ijimports)
10470 =/ private=(unit ijimports)
8997 ?~ imports.p.parsed `~
10471 ?~ imports.p.parsed `~
8998 ?. ?=([[%jibb *] ~] imports.p.parsed) ~
10472 ?. ?=([[%jibb *] ~] imports.p.parsed) ~
8999 ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
10473 ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
9000 ?~ internal-source ~
10474 ?~ internal-source ~
9001− =/ built=(unit ifile) (infer-private-internal u.internal-source)
10475+ =/ built=(unit ifile) (infer-private-internal u.internal-source src)
9002 ?~ built ~
10476 ?~ built ~
9003 `~[[face.i.imports.p.parsed u.built]]
10477 `~[[face.i.imports.p.parsed u.built]]
9004 ?~ private ~
10478 ?~ private ~
@@ -9015,9 +10489,16 @@
9015 =? env-molds declared
10489 =? env-molds declared
9016 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
10490 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
9017 =/ reserved=(list term) ?:(declared ~[%list] ~)
10491 =/ reserved=(list term) ?:(declared ~[%list] ~)
9018− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~]
10492+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~]
10493+ :: Other prelude molds may use list only after its source has passed
10494+ :: the standard-list check. The raw declaration remains removed.
10495+ =/ declared-list=(unit shape) (find-simple-mold %list molds)
10496+ =/ mold-prelude=(unit ifile)
10497+ ?~ declared-list ~
10498+ ?. (standard-prelude-list u.declared-list) ~
10499+ `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~ ~]
9019− =/ mt=imold-types (partial-prelude-molds molds state)
10500+ =/ mt=imold-types (partial-prelude-molds molds state(prelude mold-prelude))
9020− =/ partial=ifile [~ mt at ~]
10501+ =/ partial=ifile [~ mt at ~ ~ ~ ~ ~]
9021 :: An explicitly qualified re-export must resolve. Other unsupported
10502 :: An explicitly qualified re-export must resolve. Other unsupported
9022 :: prelude declarations remain reserved but absent from the interface.
10503 :: prelude declarations remain reserved but absent from the interface.
9023 =/ required=imolds
10504 =/ required=imolds
@@ -9028,8 +10509,13 @@
9028 ?~ names.sh |
10509 ?~ names.sh |
9029 ?=(^ t.names.sh)
10510 ?=(^ t.names.sh)
9030 ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
10511 ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
9031− =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
10512+ =/ resolution=iresolved (resolve-groups ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
9032− `[env mt at ~]
10513+ =/ env=ienv env.resolution
10514+ ?. (hole-values-present ds env) ~
10515+ =/ deps=(list iwidth-dependency)
10517+ ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
10518+ `[env mt at ~ artifacts.resolution deps `src ~]
9034++ partial-prelude-interface
10520++ partial-prelude-interface
9035 |= src=@t
10521 |= src=@t
@@ -9080,6 +10566,66 @@
9080 ?: =(at at.i.cache) `iface.i.cache
10566 ?: =(at at.i.cache) `iface.i.cache
9081 $(cache t.cache)
10567 $(cache t.cache)
10569+:: These certificates retain the complete checked source closure. The
10570+:: trusted host must supply the identical prepared prelude and reader nouns.
10571+:: Exact bundle equality binds all source paths and versions; the set
10572+:: retains transitive paths for active-cycle checks. Request-bearing graphs
10573+:: alone have a size limit; incompatible diamond evidence fails closed.
10574+++ request-graph-requests-add
10575+ |= [pending=(list irequest-evidence) acc=(list irequest-evidence) fuel=@ud]
10576+ ^- (unit (list irequest-evidence))
10579+ =/ hit=(list irequest-evidence)
10580+ (skim acc |=(x=irequest-evidence &(=(api-at.x api-at.i.pending) =(name.x name.i.pending))))
10582+ ?. ?=([* ~] hit) ~
10583+ ?. =(i.hit i.pending) ~
10584+ $(pending t.pending, fuel (dec fuel))
10585+ $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
10586+++ request-graph-inputs-match
10587+ |= [g=irequest-graph externals=iexternals marks=imark-externals modules=jbundle values=(list term) molds=(list term) prelude=(unit ifile)]
10589+ ?& =(bundle-input.g modules)
10590+ =(prelude-input.g prelude)
10591+ =(prelude-values.g values)
10592+ =(prelude-molds.g molds)
10593+ =(externals.g externals)
10596+++ request-graph-merge
10597+ |= [imports=ijimports g=irequest-graph fuel=@ud]
10598+ ^- (unit irequest-graph)
10601+ =/ child=ifile interface.i.imports
10603+ =/ cg=irequest-graph u.graph.child
10604+ ?. ?& =(bundle-input.g bundle-input.cg)
10605+ =(prelude-input.g prelude-input.cg)
10606+ =(prelude-values.g prelude-values.cg)
10607+ =(prelude-molds.g prelude-molds.cg)
10608+ =(externals.g externals.cg)
10609+ =(marks.g marks.cg)
10612+ =/ merged=(set path) (~(uni in:..zuse paths.g) paths.cg)
10613+ =/ rs=(unit (list irequest-evidence))
10614+ (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
10616+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
10617+ $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
10618+++ request-graph-reusable
10619+ |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
10622+ ?. =(u.source.f src) |
10624+ =/ g=irequest-graph u.graph.f
10625+ ?. (request-graph-inputs-match g externals marks modules values molds prelude) |
10626+ ?. (~(has in:..zuse paths.g) at.f) |
10627+ !(lien active |=(p=path (~(has in:..zuse paths.g) p)))
9083++ resolve-jibb-imports
10629++ resolve-jibb-imports
9084 |= [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)]
10630 |= [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)]
9085 ^- jimports-result
10631 ^- jimports-result
@@ -9097,7 +10643,16 @@
9097 ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
10643 ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
9098 =/ cached=(unit ifile) (find-jibb-cache at cache)
10644 =/ cached=(unit ifile) (find-jibb-cache at cache)
9099 =/ iface=jfile-result
10645 =/ iface=jfile-result
10647+ ?. =(at.u.cached at) [%| 'cached module identity needs unsupported inference']
10649+ :: A detached legacy interface has unknown evidence. Rebuild it
10650+ :: against the current graph, without retaining any stale entry.
10651+ =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
10652+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
10653+ ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
10654+ [%| 'cached module evidence needs unsupported inference']
9100− ?^ cached [%& [u.cached cache]]
10655+ [%& [u.cached cache]]
9101 (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
10656 (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
9102 ?: ?=(%| -.iface) [%| p.iface]
10657 ?: ?=(%| -.iface) [%| p.iface]
9103 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
10658 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
@@ -9148,7 +10703,7 @@
9148 ?~ segments `~
10703 ?~ segments `~
9149 ?: ?=(%knot -.i.segments) $(segments t.segments)
10704 ?: ?=(%knot -.i.segments) $(segments t.segments)
9150 =/ seg=pseg i.segments
10705 =/ seg=pseg i.segments
9151− ?> ?=(%typed -.seg)
10706+ ?. ?=(%typed -.seg) ~
9152 ?: =(0 aura.seg) ~
10707 ?: =(0 aura.seg) ~
9153 ?: (lien seen |=(n=term =(n name.seg))) ~
10708 ?: (lien seen |=(n=term =(n name.seg))) ~
9154 =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
10709 =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
@@ -9234,6 +10789,7 @@
9235 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
10790 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
9236 =/ derived=(list term) (weld path-names poke-names)
10791 =/ derived=(list term) (weld path-names poke-names)
10792+ ?: (lien derived |=(n=term =(n %proj))) |
9237 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
10793 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
9238 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
10794 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
@@ -9279,6 +10835,8 @@
9279++ api-path-analysis
10835++ api-path-analysis
9280 |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
10836 |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
9281 ^- (unit (list iapi-path-typed))
10837 ^- (unit (list iapi-path-typed))
10838+ ?: (lien defs.mod def-has-hole) ~
10839+ ?^ (duplicate-defs defs.mod) ~
9282 =/ ds=(list def) defs.mod
10840 =/ ds=(list def) defs.mod
9283 =/ declarations=(list def)
10841 =/ declarations=(list def)
9284 (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
10842 (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
@@ -9306,9 +10864,11 @@
9306 |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
10864 |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
9307 ^- (each (list iapi-path-typed) @t)
10865 ^- (each (list iapi-path-typed) @t)
9308 ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
10866 ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
9309− ?~ prepared [%| 'API path analysis needs the prepared prelude']
9310 =/ parsed (parse file src)
10867 =/ parsed (parse file src)
9311 ?: ?=(%| -.parsed) [%| 'API path source does not parse']
10868 ?: ?=(%| -.parsed) [%| 'API path source does not parse']
10869+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10870+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
10871+ ?~ prepared [%| 'API path analysis needs the prepared prelude']
9312 =/ prelude=(unit ifile) `iface.u.prepared
10872 =/ prelude=(unit ifile) `iface.u.prepared
9313 =/ deps=jimports-result
10873 =/ deps=jimports-result
9314 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
10874 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
@@ -9318,6 +10878,346 @@
9318 ?~ paths [%| 'API path declaration needs unsupported analysis']
10878 ?~ paths [%| 'API path declaration needs unsupported analysis']
9319 [%& u.paths]
10879 [%& u.paths]
10881+:: Analysis evidence retains the API source, the prepared interface, the
10882+:: caller's reader results and the resolved Jibb dependency cache alongside
10883+:: the typed path declarations. Reader results and prepared interfaces are
10884+:: trusted inputs: this does not verify their underlying Hoon source/version,
10885+:: create requests or check the provenance of arbitrary values.
10886++$ iapi-path-evidence
10887+ [at=path source=@t prepared=iprelude externals=iexternals marks=imark-externals dependencies=jcache paths=(list iapi-path-typed)]
10888+++ api-path-evidence-source
10889+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
10890+ ^- (each iapi-path-evidence @t)
10891+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path evidence requires /ui/api/<agent>.jibb']
10892+ =/ parsed (parse file src)
10893+ ?: ?=(%| -.parsed) [%| 'API path evidence source does not parse']
10894+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10895+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
10896+ ?~ prepared [%| 'API path evidence needs the prepared prelude']
10897+ =/ public=ifile iface.u.prepared
10898+ =/ deps=jimports-result
10899+ (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
10900+ ?: ?=(%| -.deps) [%| p.deps]
10901+ =/ paths=(unit (list iapi-path-typed))
10902+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
10903+ ?~ paths [%| 'API path declaration needs unsupported analysis']
10904+ [%& [file src u.prepared externals marks cache.p.deps u.paths]]
10905+:: Graph-aware variant preserves the caller active stack and cache.
10906+++ api-path-evidence-graph
10907+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
10908+ ^- (each iapi-path-evidence @t)
10909+ ?~ active [%| 'API analysis needs an active graph']
10910+ ?. =(i.active file) [%| 'API analysis active graph does not start at the source']
10911+ ?: (lien t.active |=(p=path =(p file))) [%| 'API analysis active graph contains a cycle']
10912+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path evidence requires /ui/api/<agent>.jibb']
10913+ =/ parsed (parse file src)
10914+ ?: ?=(%| -.parsed) [%| 'API path evidence source does not parse']
10915+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10916+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
10917+ ?~ prepared [%| 'API path evidence needs the prepared prelude']
10918+ =/ public=ifile iface.u.prepared
10919+ =/ deps=jimports-result
10920+ (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
10921+ ?: ?=(%| -.deps) [%| p.deps]
10922+ =/ paths=(unit (list iapi-path-typed))
10923+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
10924+ ?~ paths [%| 'API path declaration needs unsupported analysis']
10925+ [%& [file src u.prepared externals marks cache.p.deps u.paths]]
10927+:: This query classifies a unique path declaration only. Missing evidence
10928+:: or a nonunique name is unknown; it proves nothing about an ask value.
10929+:: Like prepared interfaces, the supplied evidence is a trusted host input.
10930+++ api-path-watchability
10931+ |= [evidence=(unit iapi-path-evidence) case-name=term]
10932+ ^- ?(%watchable %not-watchable %unknown)
10933+ ?~ evidence %unknown
10934+ =/ found=(list iapi-path-typed)
10935+ (skim paths.u.evidence |=(p=iapi-path-typed =(name.path.p case-name)))
10936+ ?. ?=([* ~] found) %unknown
10937+ ?~ scry.path.i.found %watchable
10940+:: These are declaration-derived request components, not a callable gate,
10941+:: an ask value, or proof of a value's provenance. Keep the exact trusted
10942+:: source/reader evidence until a later checked interface and lowerer can
10943+:: attach it to a generated request. No argument ordering is claimed here.
10944++$ iapi-request-parameter [name=term typ=itype at=span]
10945++$ iapi-request-parts
10946+ [evidence=iapi-path-evidence path=iapi-path-typed parameters=(list iapi-request-parameter) reply-sample=itype fold=(unit itype) watchability=?(%watchable %not-watchable)]
10947+++ api-request-parameter-types
10948+ |= params=(list iapi-parameter)
10949+ ^- (unit (list iapi-request-parameter))
10951+ =/ aura=@ta aura.i.params
10952+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
10953+ =/ rest=(unit (list iapi-request-parameter)) $(params t.params)
10955+ `[[name.i.params [%atom aura] at.i.params] u.rest]
10957+:: A single diff's fold consumes the tagged diff and the previous full value.
10958+:: Multiple-diff unions need a checked union representation and remain open.
10959+++ api-request-fold-type
10960+ |= p=iapi-path-typed
10961+ ^- (unit (unit itype))
10964+ =/ d=iapi-mark-type i.diffs.p
10965+ =/ literal=lit [%term %tas name.d (crip ['%' (trip name.d)])]
10966+ =/ sample=itype [%cell [%cell [%const literal] typ.d] full.p]
10967+ ``[%fn sample full.p]
10969+++ api-request-parts
10970+ |= [evidence=(unit iapi-path-evidence) case-name=term]
10971+ ^- (unit iapi-request-parts)
10973+ =/ found=(list iapi-path-typed)
10974+ (skim paths.u.evidence |=(p=iapi-path-typed =(name.path.p case-name)))
10975+ ?. ?=([* ~] found) ~
10976+ =/ p=iapi-path-typed i.found
10977+ =/ raw=(unit (list iapi-parameter)) (api-path-parameters segments.path.p ~)
10979+ =/ params=(unit (list iapi-request-parameter)) (api-request-parameter-types u.raw)
10981+ =/ fold=(unit (unit itype)) (api-request-fold-type p)
10983+ =/ watch=?(%watchable %not-watchable) ?~(scry.path.p %watchable %not-watchable)
10984+ `[u.evidence p u.params full.p u.fold watch]
10986+:: Check ordinary API molds and values plus every declared mark type using
10987+:: the same trusted source, prepared prelude and reader inputs as path
10988+:: evidence. Keep elaborations with those inputs for a later interface.
10989+:: This is partial analysis: an unused /- core is not independently checked,
10990+:: definitions needing derived values remain unsupported, and no complete
10991+:: API, request or constructor is exported or given runtime behavior.
10992++$ iapi-support-evidence
10993+ [paths=iapi-path-evidence values=ienv molds=imold-types marks=(list iapi-mark-type) elaborations=(list iwidth-definition)]
10994+++ api-support-analysis-source
10995+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
10996+ ^- (each iapi-support-evidence @t)
10997+ =/ path-result (api-path-evidence-source file src externals marks modules prepared)
10998+ ?: ?=(%| -.path-result) [%| p.path-result]
10999+ =/ evidence=iapi-path-evidence p.path-result
11000+ =/ parsed (parse file src)
11001+ ?: ?=(%| -.parsed) [%| 'API source does not parse']
11002+ =/ mod=module p.parsed
11003+ =/ ordinary=(list def)
11004+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
11005+ =/ prep=iprelude prepared.evidence
11006+ ?. (module-scope-valid mod(defs ordinary) values.prep molds.prep) [%| 'API ordinary scope needs unsupported inference']
11007+ =/ vals=(list term) (global-value-names ordinary)
11008+ ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
11009+ =/ declared=(list term) (collect-mark-imports imports.mod)
11010+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
11011+ ?~ mark-types [%| 'API declared marks need unsupported inference']
11012+ =/ prelude=(unit ifile) `iface.prep
11013+ =/ deps=jimports-result
11014+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.prep molds.prep dependencies.evidence prelude)
11015+ ?: ?=(%| -.deps) [%| p.deps]
11016+ =/ molds=imolds (collect-simple-molds ordinary)
11017+ =/ globals=(list term) (weld values.prep (weld (import-binding-names imports.mod) vals))
11018+ =/ surs=(list term) (collect-sur-imports imports.mod)
11019+ =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11020+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11021+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~]
11022+ =/ mts=(each imold-types @t) (module-mold-types molds state)
11023+ ?: ?=(%| -.mts) [%| p.mts]
11024+ =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
11025+ ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
11026+ [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
11027+:: Preserve the same graph context through supporting definitions.
11028+++ api-support-analysis-graph
11029+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
11030+ ^- (each iapi-support-evidence @t)
11031+ =/ path-result (api-path-evidence-graph file src externals marks modules active cache prepared)
11032+ ?: ?=(%| -.path-result) [%| p.path-result]
11033+ =/ evidence=iapi-path-evidence p.path-result
11034+ =/ parsed (parse file src)
11035+ ?: ?=(%| -.parsed) [%| 'API source does not parse']
11036+ =/ mod=module p.parsed
11037+ =/ ordinary=(list def)
11038+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
11039+ =/ prep=iprelude prepared.evidence
11040+ ?. (module-scope-valid mod(defs ordinary) values.prep molds.prep) [%| 'API ordinary scope needs unsupported inference']
11041+ =/ vals=(list term) (global-value-names ordinary)
11042+ ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
11043+ =/ declared=(list term) (collect-mark-imports imports.mod)
11044+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
11045+ ?~ mark-types [%| 'API declared marks need unsupported inference']
11046+ =/ prelude=(unit ifile) `iface.prep
11047+ =/ deps=jimports-result
11048+ (resolve-jibb-imports imports.mod externals marks modules active values.prep molds.prep dependencies.evidence prelude)
11049+ ?: ?=(%| -.deps) [%| p.deps]
11050+ =/ molds=imolds (collect-simple-molds ordinary)
11051+ =/ globals=(list term) (weld values.prep (weld (import-binding-names imports.mod) vals))
11052+ =/ surs=(list term) (collect-sur-imports imports.mod)
11053+ =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
11054+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11055+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~]
11056+ =/ mts=(each imold-types @t) (module-mold-types molds state)
11057+ ?: ?=(%| -.mts) [%| p.mts]
11058+ =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
11059+ ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
11060+ [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
11062+:: Type-analysis artifact for one plain request. The resolver may publish
11063+:: its interface only together with trusted source and reader evidence.
11064+:: No lowering or runtime validator exists.
11065+:: Value watchability remains unproved even for a watchable declaration.
11066++$ ione-request-interface
11067+ [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
11068+++ request-compatible-ask
11069+ |= prelude=iprelude
11071+ =/ public=ifile iface.prelude
11072+ ?. =(at.public /lib/jibb/prelude/jibb) ~
11073+ =/ ask=(unit ischeme) (find-jibb-mold %ask public)
11075+ ?. ?=([@ ~] vars.u.ask) ~
11076+ ?. ?=(%union -.typ.u.ask) ~
11077+ ?. =(origin.typ.u.ask `[/lib/jibb/internal/jibb %ask]) ~
11078+ ?. (identity-union-parameters vars.u.ask args.typ.u.ask) ~
11079+ =/ m=@ud i.vars.u.ask
11080+ ?: (itype-var-is-atom m typ.u.ask) ~
11081+ ?. (levy (itype-vars typ.u.ask) |=(n=@ud =(n m))) ~
11082+ ?: (itype-has-tag typ.u.ask) ~
11083+ =/ private=(list iwidth-dependency)
11084+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
11085+ ?. ?=([* ~] private) ~
11086+ ?~ source.i.private ~
11087+ =/ path=(unit ischeme) (find-jibb-mold %path public)
11090+ =/ path-type=itype [%collection %list ~[[%atom %ta]]]
11091+ ?. =(typ.u.path path-type) ~
11092+ =/ unit-template=(unit ischeme) (find-jibb-mold %unit public)
11093+ ?~ unit-template ~
11094+ ?. (standard-unit-template u.unit-template /lib/jibb/prelude/jibb) ~
11095+ =/ state-unit=(unit itype) (template-apply u.unit-template ~[[%noun ~]])
11097+ =/ path-unit=(unit itype) (template-apply u.unit-template ~[path-type])
11099+ =/ output=itype [%cell [%face %state [%noun ~]] [%face %message [%var m]]]
11100+ =/ agent-input=itype [%cell [%face %mark [%atom %tas]] [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]]
11101+ =/ store-input=itype [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]
11102+ =/ pure-case=itype [%cell [%const [%term %tas %pure '%pure']] [%face %value [%var m]]]
11103+ =/ agent-case=itype
11104+ [%cell [%const [%term %tas %agent '%agent']] [%cell [%face %api [%atom %t]] [%cell [%face %case [%atom %tas]] [%cell [%face %agent [%atom %tas]] [%cell [%face %path path-type] [%cell [%face %scry u.path-unit] [%face %receive [%fn agent-input output]]]]]]]]
11105+ =/ store-case=itype
11106+ [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %name [%atom %tas]] [%face %receive [%fn store-input output]]]]]
11107+ ?. =(cases.typ.u.ask ~[pure-case agent-case store-case]) ~
11110+:: The first supported standalone API has exactly one mark import and one
11111+:: plain path declaration, with no other definitions or imports. No partial
11112+:: success is published when source, schema, or a required mold is unknown.
11113+++ one-request-interface-source
11114+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
11115+ ^- (each ione-request-interface @t)
11116+ =/ out (api-support-analysis-source file src externals marks modules prepared)
11117+ ?: ?=(%| -.out) [%| p.out]
11118+ =/ support=iapi-support-evidence p.out
11119+ =/ ev=iapi-path-evidence paths.support
11120+ =/ parsed (parse file src)
11121+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
11122+ =/ mod=module p.parsed
11123+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
11124+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
11125+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
11126+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
11127+ =/ p=iapi-path-typed i.paths.ev
11128+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
11129+ ?~ parts [%| 'request components need unsupported inference']
11130+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
11131+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
11132+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
11134+ ?~ fold.u.parts ?=([* ~] marks.support)
11135+ ?=([* [* ~]] marks.support)
11136+ ?. valid-marks [%| 'request marks need unsupported inference']
11139+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
11140+ ?: fold-open [%| 'request fold needs unsupported inference']
11141+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
11142+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
11143+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
11144+ ?~ ask [%| 'request ask needs unsupported inference']
11145+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
11146+ ?~ result [%| 'request ask needs unsupported inference']
11147+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
11149+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
11150+ ?~ parameters.u.parts callback
11151+ [%cell typ.i.parameters.u.parts callback]
11152+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
11153+ =/ exports=imold-types
11154+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
11155+ =/ prelude=iprelude prepared.ev
11156+ =/ public=ifile iface.prelude
11157+ ?~ source.public [%| 'request prelude source needs unsupported inference']
11158+ =/ private=(list iwidth-dependency)
11159+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
11160+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
11161+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
11162+ =/ req=irequest-evidence
11163+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
11164+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
11165+ [%& [support u.parts interface]]
11166+:: Graph-aware request artifact; resolver use remains type-only.
11167+++ one-request-interface-graph
11168+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
11169+ ^- (each ione-request-interface @t)
11170+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
11171+ ?: ?=(%| -.out) [%| p.out]
11172+ =/ support=iapi-support-evidence p.out
11173+ =/ ev=iapi-path-evidence paths.support
11174+ =/ parsed (parse file src)
11175+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
11176+ =/ mod=module p.parsed
11177+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
11178+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
11179+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
11180+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
11181+ =/ p=iapi-path-typed i.paths.ev
11182+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
11183+ ?~ parts [%| 'request components need unsupported inference']
11184+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
11185+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
11186+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
11188+ ?~ fold.u.parts ?=([* ~] marks.support)
11189+ ?=([* [* ~]] marks.support)
11190+ ?. valid-marks [%| 'request marks need unsupported inference']
11193+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
11194+ ?: fold-open [%| 'request fold needs unsupported inference']
11195+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
11196+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
11197+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
11198+ ?~ ask [%| 'request ask needs unsupported inference']
11199+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
11200+ ?~ result [%| 'request ask needs unsupported inference']
11201+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
11203+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
11204+ ?~ parameters.u.parts callback
11205+ [%cell typ.i.parameters.u.parts callback]
11206+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
11207+ =/ exports=imold-types
11208+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
11209+ =/ prelude=iprelude prepared.ev
11210+ =/ public=ifile iface.prelude
11211+ ?~ source.public [%| 'request prelude source needs unsupported inference']
11212+ =/ private=(list iwidth-dependency)
11213+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
11214+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
11215+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
11216+ =/ req=irequest-evidence
11217+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
11218+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
11219+ [%& [support u.parts interface]]
9321++ api-mark-exports
11221++ api-mark-exports
9322 |= [marks=(list term) all=(list term) externals=imark-externals]
11222 |= [marks=(list term) all=(list term) externals=imark-externals]
9323 ^- imold-types
11223 ^- imold-types
@@ -9331,7 +11231,9 @@
9331++ api-poke-interface
11231++ api-poke-interface
9332 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
11232 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
9333 ^- (unit ifile)
11233 ^- (unit ifile)
11234+ ?: (lien defs.mod def-has-hole) ~
9334 ?. ?=([%ui %api @ %jibb ~] at) ~
11235 ?. ?=([%ui %api @ %jibb ~] at) ~
11236+ ?^ (duplicate-defs defs.mod) ~
9335 ?~ prelude ~
11237 ?~ prelude ~
9336 ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
11238 ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
9337 =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
11239 =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
@@ -9359,7 +11261,133 @@
9359 =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
11261 =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
9360 ?~ mark ~
11262 ?~ mark ~
9361 =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
11263 =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
9362− `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]]]
11264+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
11266+:: Source-proven ordinary helpers validate each selected /sur dependency.
11267+:: Unused or less direct cores remain unsupported by this first interface.
11269+ |= [surs=(list term) defs=(list def) externals=iexternals all=(list term)]
11272+ =/ found=(list def)
11275+ ?. ?=(%mold -.d) |
11276+ ?. ?=(%ref -.shape.d) |
11277+ ?. ?=([@ [@ ~]] names.shape.d) |
11278+ =(i.t.names.shape.d i.surs)
11280+ =/ selected=def i.found
11281+ ?. ?=(%mold -.selected) |
11282+ =/ sh=shape shape.selected
11283+ ?. ?=(%ref -.sh) |
11284+ ?. ?=([@ [@ ~]] names.sh) |
11285+ =/ checked=(unit itype) (find-imported-mold i.surs i.names.sh externals all)
11289++$ imulti-request-gates [values=ienv requests=(list irequest-evidence)]
11290+++ api-request-gates
11291+ |= [paths=(list iapi-path-typed) ev=iapi-path-evidence ask=ischeme file=path src=@t public=@t internal=@t externals=iexternals marks=imark-externals fuel=@ud]
11292+ ^- (unit imulti-request-gates)
11295+ =/ p=iapi-path-typed i.paths
11296+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
11298+ ?. ?=(?(~ [* ~]) parameters.u.parts) ~
11299+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) ~
11301+ ?^ (itype-vars reply-sample.u.parts) ~
11302+ ?: (itype-has-tag reply-sample.u.parts) ~
11305+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
11307+ =/ result=(unit itype) (template-apply ask ~[[%var 0]])
11309+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
11311+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
11312+ ?~ parameters.u.parts callback
11313+ [%cell typ.i.parameters.u.parts callback]
11314+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
11315+ =/ prep=iprelude prepared.ev
11316+ =/ req=irequest-evidence
11317+ [file name.path.p p src public internal values.prep molds.prep externals marks]
11318+ =/ rest=(unit imulti-request-gates)
11319+ $(paths t.paths, fuel (dec fuel))
11321+ `[[[name.path.p scheme] values.u.rest] [req requests.u.rest]]
11323+++ api-poke-from-checked
11324+ |= [file=path mod=module marks=imark-externals values=(list term) molds=(list term) prelude=(unit ifile)]
11325+ ^- (unit [values=ienv derived=(list iderived)])
11326+ =/ pokes=(list def)
11327+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
11329+ ?. ?=([* ~] pokes) ~
11330+ =/ declared=(list term) (collect-mark-imports imports.mod)
11331+ =/ ns=(unit (list term)) (api-poke-mark-names pokes declared)
11333+ ?. ?=([@ ~] u.ns) ~
11334+ =/ matching=(list import)
11335+ %+ skim imports.mod
11337+ ?. ?=(%mark -.i) |
11339+ ?. ?=([* ~] matching) ~
11340+ =/ checked=(unit ifile)
11341+ (api-poke-interface file mod(defs pokes, imports matching) marks values molds prelude)
11343+ `[values.u.checked derived.u.checked]
11345+:: The partial interface is published atomically: all paths, ordinary
11346+:: source definitions, declared marks and the poke must check. Unselected
11347+:: /sur bindings, runtime validation and value watchability remain unproved.
11348+++ multi-request-interface-graph
11349+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
11350+ ^- (each [iface=ifile cache=jcache] @t)
11351+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
11352+ ?: ?=(%| -.out) [%| p.out]
11353+ =/ support=iapi-support-evidence p.out
11354+ =/ ev=iapi-path-evidence paths.support
11355+ =/ parsed (parse file src)
11356+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
11357+ =/ mod=module p.parsed
11358+ ?. (levy imports.mod |=(i=import ?=(?(%mark %sur) -.i)))
11359+ [%| 'request imports need unsupported inference']
11360+ =/ surs=(list term) (collect-sur-imports imports.mod)
11361+ ?. (api-sur-covered surs defs.mod externals surs)
11362+ [%| 'API source dependency needs unsupported inference']
11363+ ?~ paths.ev [%| 'request count needs unsupported inference']
11364+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
11365+ ?~ ask [%| 'request ask needs unsupported inference']
11366+ =/ prep=iprelude prepared.ev
11367+ =/ public=ifile iface.prep
11368+ ?~ source.public [%| 'request prelude source needs unsupported inference']
11369+ =/ private=(list iwidth-dependency)
11370+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
11371+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
11372+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
11373+ =/ gates=(unit imulti-request-gates)
11374+ (api-request-gates paths.ev ev u.ask file src u.source.public u.source.i.private externals marks 256)
11375+ ?~ gates [%| 'request paths need unsupported inference']
11376+ =/ poke=(unit [values=ienv derived=(list iderived)])
11377+ (api-poke-from-checked file mod marks values.prep molds.prep `public)
11378+ ?~ poke [%| 'API poke needs unsupported inference']
11379+ =/ mark-molds=imold-types
11380+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
11381+ =/ exports=imold-types (weld mark-molds molds.support)
11382+ =/ names=(list term) (turn exports |=(m=[name=term template=ischeme] name.m))
11383+ ?. (levy names |=(n=term (unique-value-name n names)))
11384+ [%| 'API exported molds need unsupported inference']
11385+ =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
11386+ =/ graph=irequest-graph
11387+ [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
11389+ [env exports file derived.u.poke elaborations.support ~ `src `graph]
11390+ [%& [iface dependencies.ev]]
9364++ infer-jibb-file
11392++ infer-jibb-file
9365 |= [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)]
11393 |= [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)]
@@ -9367,10 +11395,30 @@
9367 =/ parsed (parse at src)
11395 =/ parsed (parse at src)
9368 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
11396 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
9369 =/ mod=module p.parsed
11397 =/ mod=module p.parsed
11398+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
11399+ ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
9370 ?: ?=([%ui %api *] at)
11400 ?: ?=([%ui %api *] at)
9371 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
11401 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
11403+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
11404+ [%& [checked [[at checked] cache]]]
9372− ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
11405+ ?~ prelude [%| (crip "API module needs unsupported inference: {(spud at)}")]
9373− [%& [u.iface [[at u.iface] cache]]]
11406+ =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
11408+ ?. ?=([[%mark *] ~] imports.mod) |
11409+ ?. ?=([[%mold *] ~] defs.mod) |
11410+ ?. =(%paths name.i.defs.mod) |
11411+ !?=(%union -.shape.i.defs.mod)
11413+ =/ request=(each ione-request-interface @t)
11414+ (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
11415+ ?: ?=(%| -.request) [%| (crip "API module needs unsupported inference: {(spud at)}")]
11416+ =/ checked=ifile iface.p.request
11417+ [%& [checked [[at checked] dependencies.paths.support.p.request]]]
11418+ =/ multi=(each [iface=ifile cache=jcache] @t)
11419+ (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
11420+ ?: ?=(%| -.multi) [%| (crip "API module needs unsupported inference: {(spud at)}")]
11421+ [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
9374 ?. (module-scope-valid mod prelude-values prelude-molds)
11422 ?. (module-scope-valid mod prelude-values prelude-molds)
9375 ?: (pending-declared-poke at mod prelude-values prelude-molds)
11423 ?: (pending-declared-poke at mod prelude-values prelude-molds)
9376 [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
11424 [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
@@ -9386,13 +11434,72 @@
9386 =/ marks=(list term) (collect-mark-imports imports.mod)
11434 =/ marks=(list term) (collect-mark-imports imports.mod)
9387 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11435 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
9388 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11436 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9389− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
11437+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
9390 =/ mts=(each imold-types @t) (module-mold-types molds state)
11438 =/ mts=(each imold-types @t) (module-mold-types molds state)
9391 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
11439 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
9392− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
11440+ =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
11441+ =/ env=ienv env.resolution
9393 ?. (module-values-complete defs.mod env)
11442 ?. (module-values-complete defs.mod env)
9394 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
11443 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
9395− [%& [[env p.mts at ~] [[at [env p.mts at ~]] cache.p.js]]]
11444+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
11445+ =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
11446+ ?~ graph [%| 'module request evidence needs unsupported inference']
11447+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
11448+ [%& [iface [[at iface] cache.p.js]]]
11450+:: A source-bound analysis of one named mold, not a module, island,
11451+:: request, watchability or runtime check. The host owns the trusted
11452+:: prepared prelude, canonical paths and reader/source version identities.
11453+:: The 256-node cap covers only classification, not source/graph work.
11455+ [at=path source=@t name=term prepared=iprelude externals=iexternals marks=imark-externals modules=jbundle dependencies=jcache mold=ischeme requested=@ud budget=@ud result=igate-free]
11456+++ gate-free-mold-source
11457+ |= [file=path src=@t name=term externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude) fuel=@ud]
11458+ ^- (each igate-free-mold @t)
11459+ ?~ file [%| 'mold analysis needs a path ending in jibb']
11460+ ?. =(%jibb (rear file)) [%| 'mold analysis needs a path ending in jibb']
11461+ ?: |(=(file /lib/jibb/internal/jibb) =(file /lib/jibb/primitives/jibb))
11462+ [%| 'the prelude internal modules are private']
11463+ ?: ?=([%ui %api *] file) [%| 'API declarations need unsupported mold analysis']
11464+ ?: ?=([%ui %stores *] file) [%| 'store declarations need unsupported mold analysis']
11465+ =/ entries=jbundle (skim modules |=(m=jsource =(file at.m)))
11466+ ?: (gth (lent entries) 1) [%| 'duplicate root module sources']
11467+ =/ wrong-root=? ?~(entries | !=(source.i.entries src))
11468+ ?: wrong-root [%| 'root module source does not match bundle']
11469+ =/ parsed (parse file src)
11470+ ?: ?=(%| -.parsed) [%| 'mold source does not parse']
11471+ =/ mod=module p.parsed
11472+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
11473+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11474+ ?~ prepared [%| 'mold analysis needs the prepared prelude']
11475+ ?. (module-scope-valid mod values.u.prepared molds.u.prepared)
11476+ [%| 'mold source has conflicting or unsupported scope']
11477+ =/ selected=(list def)
11478+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(name.d name))))
11479+ ?~ selected [%| 'selected mold is not declared']
11480+ ?^ t.selected [%| 'selected mold is not unique']
11481+ ?> ?=(%mold -.i.selected)
11482+ =/ public=ifile iface.u.prepared
11483+ =/ js=jimports-result
11484+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
11485+ ?: ?=(%| -.js) [%| p.js]
11486+ =/ ms=imolds (collect-simple-molds defs.mod)
11487+ =/ vals=(list term) (global-value-names defs.mod)
11488+ =/ globals=(list term) (weld values.u.prepared (weld (import-binding-names imports.mod) vals))
11489+ =/ surs=(list term) (collect-sur-imports imports.mod)
11490+ =/ declared=(list term) (collect-mark-imports imports.mod)
11491+ =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11492+ =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))
11493+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~]
11494+ =/ inferred=(unit [template=ischeme state=istate])
11495+ (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
11496+ ?~ inferred [%| 'selected mold needs unsupported inference']
11497+ =/ template=ischeme template.u.inferred
11498+ =. typ.template (label-direct-union typ.template shape.i.selected name state)
11499+ =. typ.template (itype-normalize typ.template sub.state.u.inferred)
11500+ =/ cap=@ud (min fuel 256)
11501+ =/ analysis=igate-free (gate-free-type typ.template cap ~)
11502+ [%& [file src name u.prepared externals marks modules cache.p.js template fuel cap analysis]]
9397:: +golden-types-with-modules fails closed for imports without prelude
11504:: +golden-types-with-modules fails closed for imports without prelude
9398:: scope. +golden-types-with-prelude resolves supported library graphs;
11505:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -9403,6 +11510,8 @@
9404 =/ parsed (parse file src)
11511 =/ parsed (parse file src)
9405 ?: ?=(%| -.parsed) (show-error src p.parsed)
11512 ?: ?=(%| -.parsed) (show-error src p.parsed)
11513+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11514+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
9406 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
11515 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
9407 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
11516 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
9408 (golden-types-with-marks file src externals mark-externals)
11517 (golden-types-with-marks file src externals mark-externals)
@@ -9417,6 +11526,8 @@
9418 =/ parsed (parse file src)
11527 =/ parsed (parse file src)
9419 ?: ?=(%| -.parsed) (show-error src p.parsed)
11528 ?: ?=(%| -.parsed) (show-error src p.parsed)
11529+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11530+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
9420 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
11531 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
9421 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
11532 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
9422 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
11533 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
@@ -9435,6 +11546,8 @@
9436 =/ parsed (parse file src)
11547 =/ parsed (parse file src)
9437 ?: ?=(%| -.parsed) (show-error src p.parsed)
11548 ?: ?=(%| -.parsed) (show-error src p.parsed)
11549+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11550+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
9438 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
11551 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
9439 =/ prelude-values=(list term) values.u.prepared
11552 =/ prelude-values=(list term) values.u.prepared
9440 =/ prelude-molds=(list term) molds.u.prepared
11553 =/ prelude-molds=(list term) molds.u.prepared
@@ -9482,6 +11595,10 @@
9482 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
11595 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
9483 =/ parsed (parse file src)
11596 =/ parsed (parse file src)
9484 ?: ?=(%| -.parsed) (show-error src p.parsed)
11597 ?: ?=(%| -.parsed) (show-error src p.parsed)
11598+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11599+ ?^ duplicate (duplicate-fields-report file src u.duplicate)
11600+ ?: (module-has-reserved-proj p.parsed)
11601+ 'module has reserved proj name'
9485 =/ ds=(list def) defs.p.parsed
11602 =/ ds=(list def) defs.p.parsed
9486 =/ molds=imolds (collect-simple-molds ds)
11603 =/ molds=imolds (collect-simple-molds ds)
9487 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
11604 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -9509,7 +11626,7 @@
9509 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
11626 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
9510 $(ds t.ds, lines [line lines])
11627 $(ds t.ds, lines [line lines])
9511 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11628 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9512− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
11629+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~]
9513 =. initial (reserve-def-caps val.d initial)
11630 =. initial (reserve-def-caps val.d initial)
9514 =/ result=iresult
11631 =/ result=iresult
9515 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
11632 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -9517,6 +11634,11 @@
9517 (infer-fragment val.d env initial)
11634 (infer-fragment val.d env initial)
9518 ?: ?=(%| -.result)
11635 ?: ?=(%| -.result)
9519 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
11636 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
11637+ =. state.p.result (promote-restricted-numbers state.p.result env)
11638+ =. 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)))
11639+ =/ hole=(unit idiag) (unresolved-hole holes.state.p.result holes.initial state.p.result)
11641+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d u.hole) lines])
9520 =/ merged=(unit [first=icap second=icap])
11642 =/ merged=(unit [first=icap second=icap])
9521 (merged-capitals caps.state.p.result sub.state.p.result)
11643 (merged-capitals caps.state.p.result sub.state.p.result)
9522 ?^ merged
11644 ?^ merged
@@ -9539,6 +11661,8 @@
9539 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
11661 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
9540 ?: (gth (lent vars) 26)
11662 ?: (gth (lent vars) 26)
9541 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
11663 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
11664+ ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
11665+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
9542 =/ printable=itype (canonical-itype typ vars)
11666 =/ printable=itype (canonical-itype typ vars)
9543 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
11667 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
9544 $(ds t.ds, lines [line lines])
11668 $(ds t.ds, lines [line lines])