@@ -4607,6 +4607,8 @@
46074607:: Atom constraints tied to an explicit capital or an inferred sample
46084608:: are generalized and printed. Other aura variables remain unsupported until
46094609:: their defaulting and inferred generalization are implemented.
4610+:: Restricted-number promotion considers written capitals only; if there
4611+:: are none, it skips the otherwise unnecessary environment traversal.
46104612:: Bare @ is a separate unrestricted atom type. A directional fit check
46114613:: permits concrete atoms to widen to it, never the reverse. A fit that
46124614:: needs a not-yet-implemented constraint remains unsupported. Named unions
@@ -4614,20 +4616,64 @@
46144616:: from their display name. Generic cases must be disjoint for all arguments.
46154617:: Unnamed union printing is informational; it is not Jibb syntax.
46164618::
4619+:: `proj` is a reserved, type-directed operation, not an ordinary gate.
4620+:: The supported fragment selects uniquely faced fields from a known record
4621+:: in source order (reordering is a doc question). It records the original
4622+:: call, source and target types, and source axes with its definition;
4623+:: A single selected field keeps its face and uses one source axis.
4624+:: Checked module interfaces retain that evidence and their source, including
4625+:: the private prelude dependency. A later lowerer must replace the call by
4626+:: an inline gate applied to the operand once; no lowering is implemented yet.
4627+:: Ordinary fits never insert a projection. Unknown or variable-origin record
4628+:: spines, nested projected fields and projections in
4629+:: recursive groups remain unsupported. Directional fits bound faced-spine
4630+:: proofs to fewer than 1,024 cells; the projection planner has a separate
4631+:: 4,096-step bound. These are inference limits, not language limits.
4632+::
4633+:: Supported API imports derive request-gate types atomically for multiple
4634+:: paths, including one typed segment or one diff fold per case. Their checked
4635+:: ordinary definitions, mark molds and supported poke constructor are also
4636+:: exported. A selected /sur mold is checked through its trusted reader result;
4637+:: unused cores and other bindings are not independently validated. APIs
4638+:: with /= imports, separate scry paths, multiple parameters or diffs, or a
4639+:: parameter together with a fold remain unsupported. The unchanged todo API
4640+:: fits this fragment, including named closed fold gates.
4641+::
4642+:: Each case's source-derived schema and canonical API identity travel in a
4643+:: dependency closure bound to the exact supplied bundle, prelude, scope and
4644+:: trusted reader results. Unknown cached entries are rebuilt. Request-bearing
4645+:: closures are limited to 256 source paths and requests. This is type
4646+:: inference only: no request lowering, runtime schema validator or proof that
4647+:: an arbitrary ask value is watchable is supplied.
4648+::
4649+:: A closed gate sample may omit one outer face from a known input slot when
4650+:: its product is identical. Distinct written names, nested value faces,
4651+:: ambiguous cell tails and raw-variable-origin fits retain their prior rules.
4652+::
4653+:: In one synthetic eval of a 48-module deep and 48-module wide request-free
4654+:: graph, baseline versus certificate inference took 21.53 s versus 23.10 s
4655+:: elapsed (21.10 s versus 22.34 s CPU), including startup. The deep cache's
4656+:: jam grew from 2,402 to 4,209 bytes (+1,807 bytes). These single-run figures
4657+:: are not production memory or performance benchmarks.
4658+::
46174659+$ itype
46184660 $~ [%var 0]
46194661 $% [%var id=@ud]
46204662 [%avar id=@ud]
4663+ [%rvar id=@ud]
46214664 [%nvar id=@ud]
4665+ [%rnvar id=@ud]
46224666 [%atom aura=@ta]
46234667 [%any-atom ~]
46244668 [%flag ~]
46254669 [%noun ~]
4670+ [%empty ~]
46264671 [%tag id=@ud literal=lit constructor=?]
46274672 [%const literal=lit]
46284673 [%collection name=term args=(list itype)]
46294674 [%recursive module=term name=term label=(unit @t)]
46304675 [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
4676+ [%grec at=path name=term label=(unit @t) proof=shape args=(list itype)]
46314677 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46324678 [%face name=term body=itype]
46334679 [%fn sample=itype product=itype]
@@ -4651,21 +4697,117 @@
46514697 %var
46524698 =/ found=(unit itype) (itype-lookup id.t sub)
46534699 ?~ found t
4700+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
46544701 $(t u.found)
46554702 %avar
46564703 =/ found=(unit itype) (itype-lookup id.t sub)
46574704 ?~ found t
4705+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4706+ $(t u.found)
4707+ %rvar
4708+ =/ found=(unit itype) (itype-lookup id.t sub)
4709+ ?~ found t
4710+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
46584711 $(t u.found)
46594712 %nvar
46604713 =/ found=(unit itype) (itype-lookup id.t sub)
46614714 ?~ found t
4715+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
4716+ $(t u.found)
4717+ %rnvar
4718+ =/ found=(unit itype) (itype-lookup id.t sub)
4719+ ?~ found t
4720+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
46624721 $(t u.found)
46634722 %tag
46644723 =/ found=(unit itype) (itype-lookup id.t sub)
46654724 ?~ found t
4725+ ?: &(|(?=(%rvar -.u.found) ?=(%rnvar -.u.found)) =(id.t +.u.found)) u.found
46664726 $(t u.found)
46674727 ==
46684728::
4729+:: Prove only emptiness; unknown types are never treated as empty.
4730+:: A shared node budget bounds each proof attempt.
4731+++ itype-empty-cases
4732+ |= [xs=(list itype) sub=isub fuel=@ud]
4733+ ^- (unit [empty=? left=@ud])
4734+ ?~ xs `[& fuel]
4735+ =/ first=(unit [empty=? left=@ud]) (itype-empty-proof i.xs sub fuel)
4736+ ?~ first ~
4737+ ?. empty.u.first `[| left.u.first]
4738+ $(xs t.xs, fuel left.u.first)
4739+++ itype-empty-proof
4740+ |= [typ=itype sub=isub fuel=@ud]
4741+ ^- (unit [empty=? left=@ud])
4742+ ?: =(0 fuel) ~
4743+ =. fuel (dec fuel)
4744+ =. typ (itype-walk typ sub)
4745+ ?- -.typ
4746+ %empty `[& fuel]
4747+ %face $(typ body.typ)
4748+ %cell
4749+ =/ left=(unit [empty=? left=@ud]) $(typ hed.typ)
4750+ ?~ left ~
4751+ ?: empty.u.left `[& left.u.left]
4752+ $(typ tal.typ, fuel left.u.left)
4753+ %union (itype-empty-cases cases.typ sub fuel)
4754+ * `[| fuel]
4755+ ==
4756+:: Prove reachability separately from emptiness. An unresolved fixed
4757+:: recursive type is not presumed inhabited. A written, still-unconstrained
4758+:: capital is existentially inhabited for pattern reachability; the normal
4759+:: definition-boundary checks reject subsequently constrained capitals.
4760+++ itype-inhabited-cases
4761+ |= [xs=(list itype) sub=isub caps=icaps fuel=@ud pending=?]
4762+ ^- (unit [result=?(%yes %no %unknown) left=@ud])
4763+ ?~ xs `[?:(pending %unknown %no) fuel]
4764+ =/ first=(unit [result=?(%yes %no %unknown) left=@ud])
4765+ (itype-inhabited-proof i.xs sub caps fuel)
4766+ ?~ first ~
4767+ ?: =(%yes result.u.first) first
4768+ $(xs t.xs, fuel left.u.first, pending |(pending =(%unknown result.u.first)))
4769+++ itype-inhabited-proof
4770+ |= [typ=itype sub=isub caps=icaps fuel=@ud]
4771+ ^- (unit [result=?(%yes %no %unknown) left=@ud])
4772+ ?: =(0 fuel) ~
4773+ =. fuel (dec fuel)
4774+ =. typ (itype-walk typ sub)
4775+ ?- -.typ
4776+ %empty `[%no fuel]
4777+ ?(%atom %any-atom %flag %const %noun %avar %rvar %nvar %rnvar %fn %jrec) `[%yes fuel]
4778+ %var
4779+ ?: (lien caps |=(c=icap (hole-same-variable typ (itype-walk [%var id.c] sub)))) `[%yes fuel]
4780+ `[%unknown fuel]
4781+ %face $(typ body.typ)
4782+ %cell
4783+ =/ head=(unit [result=?(%yes %no %unknown) left=@ud]) $(typ hed.typ)
4784+ ?~ head ~
4785+ ?: =(%no result.u.head) head
4786+ =/ tail=(unit [result=?(%yes %no %unknown) left=@ud]) $(typ tal.typ, fuel left.u.head)
4787+ ?~ tail ~
4788+ ?: =(%no result.u.tail) tail
4789+ ?: |(=(%unknown result.u.head) =(%unknown result.u.tail)) `[%unknown left.u.tail]
4790+ `[%yes left.u.tail]
4791+ %union (itype-inhabited-cases cases.typ sub caps fuel |)
4792+ %collection
4793+ ?. &(|(=(%list name.typ) =(%unit name.typ)) ?=([* ~] args.typ)) `[%unknown fuel]
4794+ `[%yes fuel]
4795+ %grec ?:((grec-tree-proof name.typ proof.typ) `[%yes fuel] `[%unknown fuel])
4796+ * `[%unknown fuel]
4797+ ==
4798+++ itype-live-cases
4799+ |= [xs=(list itype) sub=isub caps=icaps fuel=@ud]
4800+ ^- (unit (list itype))
4801+ ?~ xs `~
4802+ =/ first=(unit [result=?(%yes %no %unknown) left=@ud])
4803+ (itype-inhabited-proof i.xs sub caps fuel)
4804+ ?~ first ~
4805+ ?: =(%unknown result.u.first) ~
4806+ =/ rest=(unit (list itype)) $(xs t.xs, fuel left.u.first)
4807+ ?~ rest ~
4808+ ?: =(%no result.u.first) rest
4809+ `[i.xs u.rest]
4810+::
46694811++ itype-occurs
46704812 |= [n=@ud t=itype sub=isub]
46714813 ^- ?
@@ -4673,16 +4815,20 @@
46734815 ?- -.t
46744816 %var =(n id.t)
46754817 %avar =(n id.t)
4818+ %rvar =(n id.t)
46764819 %nvar =(n id.t)
4820+ %rnvar =(n id.t)
46774821 %atom |
46784822 %any-atom |
46794823 %flag |
46804824 %noun |
4825+ %empty |
46814826 %tag =(n id.t)
46824827 %const |
46834828 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
46844829 %recursive |
46854830 %jrec |
4831+ %grec (lien args.t |=(c=itype (itype-occurs n c sub)))
46864832 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
46874833 %face $(t body.t)
46884834 %fn |($(t sample.t) $(t product.t))
@@ -4701,6 +4847,9 @@
47014847 =. a (itype-walk a sub)
47024848 =. b (itype-walk b sub)
47034849 ?: =(a b) `sub
4850+ ?: &(?=(%grec -.a) ?=(%grec -.b))
4851+ ?. &(=(at.a at.b) =(name.a name.b)) ~
4852+ (itype-unify-args args.a args.b sub)
47044853 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
47054854 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
47064855 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
@@ -4719,6 +4868,32 @@
47194868 ?: ?=(%var -.b)
47204869 ?: (itype-occurs id.b a sub) ~
47214870 `[[id.b a] sub]
4871+ :: Arithmetic's aura variable excludes loobeans; decimal literals
4872+ :: remain defaultable until a later constraint makes them concrete.
4873+ ?: &(?=(%nvar -.a) ?=(%rvar -.b))
4874+ `[[id.b [%rnvar id.a]] [id.a [%rnvar id.a]] sub]
4875+ ?: &(?=(%rvar -.a) ?=(%nvar -.b))
4876+ `[[id.a [%rnvar id.b]] [id.b [%rnvar id.b]] sub]
4877+ ?: &(?=(%rnvar -.a) ?=(%rvar -.b)) `[[id.b a] sub]
4878+ ?: &(?=(%rvar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4879+ ?: &(?=(%rnvar -.a) ?=(%nvar -.b)) `[[id.b a] sub]
4880+ ?: &(?=(%nvar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4881+ ?: &(?=(%rnvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4882+ ?: &(?=(%avar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4883+ ?: ?=(%rnvar -.a)
4884+ ?. |(?=(%rnvar -.b) ?=(%atom -.b)) ~
4885+ `[[id.a b] sub]
4886+ ?: ?=(%rnvar -.b)
4887+ ?. ?=(%atom -.a) ~
4888+ `[[id.b a] sub]
4889+ ?: &(?=(%avar -.a) ?=(%rvar -.b)) `[[id.a b] sub]
4890+ ?: &(?=(%rvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4891+ ?: ?=(%rvar -.a)
4892+ ?. |(?=(%rvar -.b) ?=(%atom -.b)) ~
4893+ `[[id.a b] sub]
4894+ ?: ?=(%rvar -.b)
4895+ ?. ?=(%atom -.a) ~
4896+ `[[id.b a] sub]
47224897 :: The narrower decimal constraint survives a match with an atom
47234898 :: variable; decimal syntax alone does not make it a loobean.
47244899 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
@@ -4773,16 +4948,20 @@
47734948 ?- -.t
47744949 %var |
47754950 %avar |
4951+ %rvar |
47764952 %nvar |
4953+ %rnvar |
47774954 %atom |
47784955 %any-atom &
47794956 %flag |
47804957 %noun |
4958+ %empty |
47814959 %tag |
47824960 %const |
47834961 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
47844962 %recursive |
47854963 %jrec |
4964+ %grec (lien args.t |=(c=itype (itype-has-any-atom c sub)))
47864965 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
47874966 %face $(t body.t)
47884967 %fn |($(t sample.t) $(t product.t))
@@ -4845,16 +5024,20 @@
48455024 ?- -.typ
48465025 %var |
48475026 %avar |
5027+ %rvar |
48485028 %nvar |
5029+ %rnvar |
48495030 %atom &
48505031 %any-atom &
48515032 %flag &
48525033 %noun |
5034+ %empty |
48535035 %tag &
48545036 %const &
48555037 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
48565038 %recursive |
48575039 %jrec |
5040+ %grec (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
48585041 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
48595042 %face $(typ body.typ)
48605043 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4883,6 +5066,7 @@
48835066 ^- ?
48845067 =. t (itype-walk t sub)
48855068 ?- -.t
5069+ %grec (lien args.t |=(c=itype (itype-has-face c sub)))
48865070 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
48875071 %face &
48885072 %cell |($(t hed.t) $(t tal.t))
@@ -4890,6 +5074,42 @@
48905074 * |
48915075 ==
48925076::
5077+:: Closed function samples may omit a slot face, but a known name must
5078+:: match another known name. Keep nested value faces and require exact
5079+:: invariant compatibility; a faced tail against a cell is ambiguous.
5080+++ itype-closed-slot-match
5081+ |= [a=itype b=itype]
5082+ ^- ?
5083+ ?: &(?=(%face -.a) ?=(%face -.b))
5084+ ?. =(name.a name.b) |
5085+ ?=(^ (itype-unify body.a body.b ~))
5086+ ?: ?=(%face -.a) ?=(^ (itype-unify body.a b ~))
5087+ ?: ?=(%face -.b) ?=(^ (itype-unify a body.b ~))
5088+ ?=(^ (itype-unify a b ~))
5089+++ itype-closed-sample-match
5090+ |= [a=itype b=itype fuel=@ud]
5091+ ^- ?
5092+ ?: =(0 fuel) |
5093+ ?. &(?=(%cell -.a) ?=(%cell -.b)) |
5094+ ?. (itype-closed-slot-match hed.a hed.b) |
5095+ =/ x=itype tal.a
5096+ =/ y=itype tal.b
5097+ ?: &(?=(%cell -.x) ?=(%cell -.y))
5098+ ?=(^ (itype-unify x y ~))
5099+ ?: |(&(?=(%face -.x) ?=(%cell -.y)) &(?=(%cell -.x) ?=(%face -.y))) |
5100+ (itype-closed-slot-match x y)
5101+++ itype-closed-gates-match
5102+ |= [a=itype b=itype]
5103+ ^- ?
5104+ ?. &(?=(%fn -.a) ?=(%fn -.b)) |
5105+ ?. &(?=(%cell -.sample.a) ?=(%cell -.sample.b)) |
5106+ ?. =(product.a product.b) |
5107+ ?^ (itype-vars a) |
5108+ ?^ (itype-vars b) |
5109+ ?: |((itype-has-tag a) (itype-has-tag b)) |
5110+ ?. (itype-closed-sample-match sample.a sample.b 1.024) |
5111+ ?=(^ (itype-unify product.a product.b ~))
5112+::
48935113++ itype-face-asym-collection-args
48945114 |= [as=(list itype) bs=(list itype) sub=isub]
48955115 ^- ?
@@ -4903,12 +5123,15 @@
49035123 ^- ?
49045124 =. a (itype-walk a sub)
49055125 =. b (itype-walk b sub)
5126+ ?: &(?=(%grec -.a) ?=(%grec -.b))
5127+ ?. &(=(at.a at.b) =(name.a name.b)) |
5128+ (itype-face-asym-collection-args args.a args.b sub)
49065129 ?: &(?=(%collection -.a) ?=(%collection -.b))
49075130 ?. =(name.a name.b) |
49085131 (itype-face-asym-collection-args args.a args.b sub)
49095132 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4910− ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4911− ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
5133+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%rvar -.b) |(?=(%nvar -.b) ?=(%rnvar -.b)))
5134+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%rvar -.a) |(?=(%nvar -.a) ?=(%rnvar -.a)))
49125135 ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
49135136 ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
49145137 |
@@ -4931,6 +5154,30 @@
49315154 [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
49325155 expected
49335156::
5157+:: Positional call arguments do not write the sample's enclosing field
5158+:: labels. Ignore one raw sample-slot face per written argument while
5159+:: checking value faces as usual. An unknown or variable-bound cell spine
5160+:: cannot justify this distinction, so keep the existing conservative guard.
5161+++ itype-positional-slot-face-asym
5162+ |= [actual=itype expected=itype sub=isub]
5163+ ^- ?
5164+ ?: &(?=(%fn -.actual) ?=(%fn -.expected) (itype-closed-gates-match actual expected)) |
5165+ (itype-face-asym actual expected sub)
5166+::
5167+++ itype-positional-face-asym
5168+ |= [args=(list expr) actual=itype expected=itype sub=isub]
5169+ ^- ?
5170+ ?~ args &
5171+ ?~ t.args
5172+ =/ slot=itype expected
5173+ =? slot ?=(%face -.slot) body.slot
5174+ (itype-positional-slot-face-asym actual slot sub)
5175+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) &
5176+ =/ slot=itype hed.expected
5177+ =? slot ?=(%face -.slot) body.slot
5178+ ?: (itype-positional-slot-face-asym hed.actual slot sub) &
5179+ $(args t.args, actual tal.actual, expected tal.expected)
5180+::
49345181++ itype-output-may-be-cell
49355182 |= [t=itype sub=isub]
49365183 ^- ?
@@ -4941,6 +5188,7 @@
49415188 %union &
49425189 %recursive &
49435190 %jrec &
5191+ %grec &
49445192 %noun &
49455193 %collection &
49465194 %face $(t body.t)
@@ -4970,6 +5218,7 @@
49705218 ^- ?
49715219 ?- -.t
49725220 %tag &
5221+ %grec (lien args.t |=(c=itype (itype-has-tag c)))
49735222 %collection (lien args.t |=(c=itype (itype-has-tag c)))
49745223 %face $(t body.t)
49755224 %fn |($(t sample.t) $(t product.t))
@@ -4983,6 +5232,7 @@
49835232 ^- ?
49845233 ?- -.t
49855234 %union &
5235+ %grec (lien args.t |=(c=itype (itype-has-union c)))
49865236 %collection (lien args.t |=(c=itype (itype-has-union c)))
49875237 %face $(t body.t)
49885238 %fn |($(t sample.t) $(t product.t))
@@ -5001,6 +5251,7 @@
50015251 %union
50025252 ?: &(?=(~ label.t) ?=(^ args.t)) &
50035253 (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
5254+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-generic c))))
50045255 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
50055256 %face $(t body.t)
50065257 %fn |($(t sample.t) $(t product.t))
@@ -5014,6 +5265,7 @@
50145265 ?- -.t
50155266 %recursive &
50165267 %jrec &
5268+ %grec &
50175269 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
50185270 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
50195271 %face $(t body.t)
@@ -5028,6 +5280,7 @@
50285280 ?- -.t
50295281 %recursive ?=(~ label.t)
50305282 %jrec ?=(~ label.t)
5283+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-recursive c))))
50315284 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
50325285 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
50335286 %face $(t body.t)
@@ -5055,36 +5308,85 @@
50555308 $(cases t.cases, good `trial)
50565309 ==
50575310::
5058−:: A constructor needs a case with its tag at the head and a payload
5059−:: compatible with the expected gate sample. Other case forms do not
5060−:: identify a constructor.
5311+:: A constructor needs a case whose head has the same literal noun as its
5312+:: tag. An unresolved or opaque case may reveal one later, so it cannot
5313+:: prove a mismatch or a unique match. A broad atom mold is not a case.
50615314::
50625315++ itype-fit-ctor-cases
50635316 |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
50645317 ^- ifit
50655318 =/ found=(unit ifit) ~
5319+ =/ pending=? |
50665320 |-
5067− ?~ cases ?~(found [%bad ~] u.found)
5068− =/ c=itype (itype-walk i.cases sub)
5321+ ?~ cases
5322+ ?: pending [%unknown ~]
5323+ ?~ found [%bad ~]
5324+ u.found
5325+ =/ raw=itype i.cases
5326+ ?: ?=(%var -.raw)
5327+ $(cases t.cases, pending &)
5328+ =/ c=itype (itype-walk raw sub)
5329+ ?: ?=(?(%var %tag %recursive %jrec %grec %union %face) -.c)
5330+ $(cases t.cases, pending &)
50695331 ?. ?=(%cell -.c) $(cases t.cases)
5070− =/ head=itype (itype-walk hed.c sub)
5332+ =/ raw-head=itype hed.c
5333+ ?: ?=(%var -.raw-head)
5334+ $(cases t.cases, pending &)
5335+ =/ head=itype (itype-walk raw-head sub)
5336+ :: A single faced, explicitly atom-only head cannot be the tag case.
5337+ :: Do not follow variables or peel nested faces for this negative proof.
5338+ ?: ?=(%face -.head)
5339+ ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5340+ $(cases t.cases)
5341+ $(cases t.cases, pending &)
5342+ ?: ?=(?(%var %tag %recursive %jrec %grec %union) -.head)
5343+ $(cases t.cases, pending &)
50715344 ?. ?=(%const -.head) $(cases t.cases)
5072− ?. =(%term form.literal.head) $(cases t.cases)
50735345 ?. =(val.literal.head val.tag) $(cases t.cases)
5074− ?^ found [%unknown ~]
5346+ :: Equal heads can have disjoint payloads. Test each from the original
5347+ :: substitution; a unique success is usable only with no unknown rival.
50755348 =/ trial=ifit (itype-fit sample tal.c sub next)
5076− $(cases t.cases, found `trial)
5349+ ?- -.trial
5350+ %bad $(cases t.cases)
5351+ %unknown $(cases t.cases, pending &)
5352+ %ok
5353+ ?^ found [%unknown ~]
5354+ $(cases t.cases, found `trial)
5355+ ==
50775356::
50785357++ itype-fit
50795358 |= [actual=itype expected=itype sub=isub next=@ud]
50805359 ^- ifit
5360+ =/ result=ifit (itype-fit-inner actual expected sub next | |)
5361+ ?: ?=(%ok -.result) result
5362+ =/ source=itype (itype-walk actual sub)
5363+ ?. ?=(?(%empty %face %cell %union) -.source) result
5364+ =/ empty=(unit [empty=? left=@ud]) (itype-empty-proof actual sub 256)
5365+ ?~ empty [%unknown ~]
5366+ ?: empty.u.empty [%ok sub next]
5367+ result
5368+++ itype-fit-inner
5369+ |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5370+ ^- ifit
5371+ ?: &(!skip-width ?=(%cell -.actual) ?=(%cell -.expected) |((width-spine-exhausted actual 1.024) (width-spine-exhausted expected 1.024)))
5372+ [%unknown ~]
5373+ =/ known=(unit [source=iwfields target=iwfields])
5374+ ?: skip-width ~
5375+ (width-known-shape actual expected sub)
5376+ =/ too-wide=? ?~(known | (gth (lent order.source.u.known) (lent order.target.u.known)))
5377+ ?: too-wide [%unknown ~]
5378+ =/ spine-checked=? |(spine-proof ?=(^ known))
50815379 =/ uncertain=?
5082− |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5380+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)))
50835381 =/ actual-open=?
5084− |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
5382+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))
50855383 =. actual (itype-walk actual sub)
50865384 =. expected (itype-walk expected sub)
50875385 ?: =(actual expected) [%ok sub next]
5386+ ?: &(?=(%empty -.expected) |(?=(%cell -.actual) ?=(%face -.actual) ?=(%union -.actual) ?=(%grec -.actual) ?=(%recursive -.actual))) [%unknown ~]
5387+ :: The relation of the source loobean mold to explicit @f is not yet
5388+ :: established. Keep it unsupported rather than asserting a mismatch.
5389+ ?: &(?=(%flag -.actual) ?=(%atom -.expected) =(%f aura.expected)) [%unknown ~]
50885390 :: Any value can be used where a noun is expected. An unresolved
50895391 :: bare tag is fixed as a constant; a constructor still needs a gate.
50905392 ?: ?=(%noun -.expected)
@@ -5094,6 +5396,14 @@
50945396 [%ok sub next]
50955397 :: An arbitrary noun is not known to fit a narrower type.
50965398 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5399+ ?: &(!uncertain ?=(%grec -.actual) ?=(%face -.expected)) $(expected body.expected)
5400+ ?: &(!uncertain ?=(%face -.actual) ?=(%grec -.expected)) $(actual body.actual)
5401+ ?: &(?=(%grec -.actual) ?=(%grec -.expected))
5402+ ?. &(=(at.actual at.expected) =(name.actual name.expected)) [%unknown ~]
5403+ =/ matched=(unit isub) (itype-unify-args args.actual args.expected sub)
5404+ ?~ matched [%unknown ~]
5405+ [%ok u.matched next]
5406+ ?: &(|(?=(%grec -.actual) ?=(%grec -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
50975407 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
50985408 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
50995409 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
@@ -5124,7 +5434,7 @@
51245434 ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
51255435 $(expected body.expected)
51265436 ?: ?=(%union -.actual) [%unknown ~]
5127− ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
5437+ ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)))) [%unknown ~]
51285438 ?: &(?=(%union -.expected) !?=(%var -.actual))
51295439 (itype-fit-cases actual cases.expected sub next)
51305440 ?: ?=(%tag -.actual)
@@ -5132,7 +5442,7 @@
51325442 =/ u=(unit isub) (itype-unify actual expected sub)
51335443 ?~ u [%bad ~]
51345444 [%ok u.u next]
5135− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5445+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
51365446 ?: ?=(%face -.expected) $(expected body.expected)
51375447 ?: constructor.actual
51385448 ?. ?=(%fn -.expected) [%bad ~]
@@ -5160,13 +5470,17 @@
51605470 =/ u=(unit isub) (itype-unify actual expected sub)
51615471 ?~ u [%bad ~]
51625472 [%ok u.u next]
5163− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5473+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
51645474 ?: ?=(%face -.expected) $(expected body.expected)
51655475 ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
51665476 [%unknown ~]
51675477 ?: ?=(%const -.expected)
51685478 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
51695479 ?: ?=(%atom -.expected)
5480+ :: A loobean singleton must not silently widen into another aura.
5481+ ?: =(%loobean form.literal.actual)
5482+ ?: =(%f aura.expected) [%unknown ~]
5483+ [%bad ~]
51705484 ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
51715485 [%bad ~]
51725486 ?: ?=(%flag -.expected)
@@ -5174,8 +5488,14 @@
51745488 ?: ?=(%any-atom -.expected) [%ok sub next]
51755489 [%bad ~]
51765490 ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5491+ :: A known face labels the same noun. Peel it before applying the
5492+ :: directional unrestricted-atom rule, preserving raw-variable guards.
5493+ ?: &(!uncertain ?=(%any-atom -.actual) ?=(%face -.expected))
5494+ $(expected body.expected, skip-width |, spine-proof |)
5495+ ?: &(!uncertain ?=(%any-atom -.expected) ?=(%face -.actual))
5496+ $(actual body.actual, skip-width |, spine-proof |)
51775497 ?: ?=(%any-atom -.expected)
5178− ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
5498+ ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%rvar -.actual) |(?=(%nvar -.actual) ?=(%rnvar -.actual)) ?=(%flag -.actual)) [%ok sub next]
51795499 ?: ?=(%var -.actual)
51805500 =/ unified=(unit isub) (itype-unify actual [%avar next] sub)
51815501 ?~ unified [%bad ~]
@@ -5186,16 +5506,16 @@
51865506 =/ unified=(unit isub) (itype-unify actual expected sub)
51875507 ?~ unified [%bad ~]
51885508 [%ok u.unified next]
5189− ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5509+ ?: |(?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected))) [%unknown ~]
51905510 [%bad ~]
51915511 ?: &(?=(%atom -.actual) ?=(%atom -.expected))
51925512 ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
51935513 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
51945514 [%bad ~]
51955515 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5196− =/ first=ifit $(actual hed.actual, expected hed.expected)
5516+ =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
51975517 ?. ?=(%ok -.first) first
5198− $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
5518+ $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
51995519 :: A field may add a face to an occurrence of the very same type
52005520 :: variable. Binding that variable to a face around itself would fail
52015521 :: the occurs check, but its underlying type has already matched.
@@ -5217,9 +5537,10 @@
52175537 [%ok u.unified next]
52185538 ?: &(?=(%face -.actual) ?=(%face -.expected))
52195539 ?. =(name.actual name.expected) [%bad ~]
5220− $(actual body.actual, expected body.expected)
5221− ?: ?=(%face -.actual) $(actual body.actual)
5222− ?: ?=(%face -.expected) $(expected body.expected)
5540+ $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
5541+ ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
5542+ ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
5543+ ?: &(!uncertain (itype-closed-gates-match actual expected)) [%ok sub next]
52235544 ?: (itype-face-asym actual expected sub) [%unknown ~]
52245545 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
52255546 [%unknown ~]
@@ -5296,7 +5617,17 @@
52965617+$ ienv (list [name=term scheme=ischeme])
52975618+$ imold-types (list [name=term template=ischeme])
52985619+$ iderived [name=term agent=term mark=term]
5299−+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived)]
5620++$ iwidth-definition [name=term original=expr typ=itype sub=isub projections=(list iwprojection)]
5621++$ iwidth-dependency [at=path source=(unit @t) definitions=(list iwidth-definition)]
5622+:: Nonrecursive request evidence is compiler-owned metadata, not a property
5623+:: of an arbitrary ask value. Reader graphs and source inputs are trusted.
5624++$ irequest-evidence
5625+ [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]
5626+:: A unit distinguishes a verified empty closure from a detached legacy file.
5627+:: The opaque prelude is an exact trusted input, not a recursive interface mold.
5628++$ irequest-graph
5629+ [paths=(set path) requests=(list irequest-evidence) bundle-input=* prelude-input=* prelude-values=(list term) prelude-molds=(list term) externals=iexternals marks=imark-externals]
5630++$ 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)]
53005631+$ ijimports (list [face=term interface=ifile])
53015632+$ icap [name=@t id=@ud at=span]
53025633+$ icaps (list icap)
@@ -5312,7 +5643,164 @@
53125643:: Recursive-mold unfolding spends fuel in the threaded inference state.
53135644:: Retries can restart from an earlier state, so this bounds an attempt,
53145645:: not all parsing or module-checking work.
5315−+$ 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]
5646+:: Experimental: only closed, uniquely faced records have known axes.
5647++$ iwfield [name=term axis=@ud typ=itype]
5648++$ iwfields [order=(list iwfield) index=(map term iwfield)]
5649++$ iwstep [name=term axis=@ud]
5650++$ iwidth-result [steps=(list iwstep) sub=isub next=@ud]
5651++$ iwprojection [at=span original=expr source=itype target=itype steps=(list iwstep)]
5652+++ width-scan
5653+ |= [typ=itype sub=isub axis=@ud fuel=@ud]
5654+ ^- (unit iwfields)
5655+ =/ order=(list iwfield) ~
5656+ =/ index=(map term iwfield) *(map term iwfield)
5657+ |-
5658+ ?: =(0 fuel) ~
5659+ ?: |(?=(%var -.typ) ?=(%avar -.typ) ?=(%rvar -.typ) ?=(%nvar -.typ) ?=(%rnvar -.typ)) ~
5660+ ?: ?=(%face -.typ)
5661+ =/ entry=iwfield [name.typ axis body.typ]
5662+ ?: ?=(^ (~(get by index) name.entry)) ~
5663+ `[(flop [entry order]) (~(put by index) name.entry entry)]
5664+ ?. ?=(%cell -.typ) ~
5665+ =/ head=itype hed.typ
5666+ ?: |(?=(%var -.head) ?=(%avar -.head) ?=(%rvar -.head) ?=(%nvar -.head) ?=(%rnvar -.head)) ~
5667+ ?. ?=(%face -.head) ~
5668+ =/ entry=iwfield [name.head (mul 2 axis) body.head]
5669+ ?: ?=(^ (~(get by index) name.entry)) ~
5670+ $(typ tal.typ, axis +((mul 2 axis)), fuel (dec fuel), order [entry order], index (~(put by index) name.entry entry))
5671+++ width-in-order
5672+ |= [source=(list iwfield) target=(list iwfield)]
5673+ ^- ?
5674+ ?~ target &
5675+ ?~ source |
5676+ ?: =(name.i.source name.i.target) $(source t.source, target t.target)
5677+ $(source t.source)
5678+++ width-fit-fields
5679+ |= [source=(map term iwfield) target=(list iwfield) sub=isub next=@ud]
5680+ ^- (unit iwidth-result)
5681+ ?~ target `[~ sub next]
5682+ =/ found=(unit iwfield) (~(get by source) name.i.target)
5683+ ?~ found ~
5684+ =/ fit=ifit (itype-fit typ.u.found typ.i.target sub next)
5685+ ?. ?=(%ok -.fit) ~
5686+ =/ rest=(unit iwidth-result) $(target t.target, sub sub.fit, next next.fit)
5687+ ?~ rest ~
5688+ `[[[name.i.target axis.u.found] steps.u.rest] sub.u.rest next.u.rest]
5689+++ width-spine-exhausted
5690+ |= [t=itype fuel=@ud]
5691+ ^- ?
5692+ ?: =(0 fuel) &
5693+ ?. ?=(%cell -.t) |
5694+ ?. ?=(%face -.hed.t) |
5695+ $(t tal.t, fuel (dec fuel))
5696+++ width-known-shape
5697+ |= [actual=itype expected=itype sub=isub]
5698+ ^- (unit [source=iwfields target=iwfields])
5699+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5700+ =/ source=(unit iwfields) (width-scan actual sub 1 1.024)
5701+ =/ target=(unit iwfields) (width-scan expected sub 1 1.024)
5702+ ?~ source ~
5703+ ?~ target ~
5704+ `[u.source u.target]
5705+::
5706+++ width-shape
5707+ |= [actual=itype expected=itype sub=isub]
5708+ ^- (unit [source=iwfields target=iwfields])
5709+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5710+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5711+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5712+ ?~ source ~
5713+ ?~ target ~
5714+ ?. (gth (lent order.u.source) (lent order.u.target)) ~
5715+ `[u.source u.target]
5716+++ width-proj-shape
5717+ |= [actual=itype expected=itype sub=isub]
5718+ ^- (unit [source=iwfields target=iwfields])
5719+ ?. &(|(?=(%cell -.actual) ?=(%face -.actual)) |(?=(%cell -.expected) ?=(%face -.expected))) ~
5720+ =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5721+ =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5722+ ?~ source ~
5723+ ?~ target ~
5724+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
5725+ `[u.source u.target]
5726+::
5727+++ width-project
5728+ |= [shape=[source=iwfields target=iwfields] sub=isub next=@ud]
5729+ ^- (unit iwidth-result)
5730+ ?. (width-in-order order.source.shape order.target.shape) ~
5731+ (width-fit-fields index.source.shape order.target.shape sub next)
5732+::
5733+:: Provisional, globally budgeted gate-free proof. %no includes a
5734+:: gate-bearing witness; an uninhabited sibling could invalidate it.
5735+:: Input types must be resolved and normalized under valid substitutions,
5736+:: from trusted source-backed interfaces and reader results. Collection
5737+:: list/unit names rely on their existing identity invariant; this arm
5738+:: does not validate fabricated internal types.
5739++$ igf-segment
5740+ $% [%field name=term]
5741+ [%head ~]
5742+ [%tail ~]
5743+ [%item ~]
5744+ [%case index=@ud]
5745+ ==
5746++$ igate-free [verdict=?(%yes %no %unknown) inhabited=? left=@ud path=(unit (list igf-segment))]
5747+++ gate-free-types
5748+ |= [types=(list itype) fuel=@ud path=(list igf-segment) index=@ud]
5749+ ^- igate-free
5750+ ?~ types [%yes | fuel ~]
5751+ ?: =(0 fuel) [%unknown | 0 ~]
5752+ =/ first=igate-free (gate-free-type i.types fuel [[%case index] path])
5753+ ?: =(%no verdict.first) first
5754+ =/ rest=igate-free $(types t.types, fuel left.first, index +(index))
5755+ ?: =(%no verdict.rest) rest
5756+ =/ inhabited=? |(inhabited.first inhabited.rest)
5757+ ?: |(=(%unknown verdict.first) =(%unknown verdict.rest)) [%unknown inhabited left.rest ~]
5758+ [%yes inhabited left.rest ~]
5759+++ gate-free-type
5760+ |= [typ=itype fuel=@ud path=(list igf-segment)]
5761+ ^- igate-free
5762+ ?: =(0 fuel) [%unknown | 0 ~]
5763+ =. fuel (dec fuel)
5764+ ?- -.typ
5765+ %fn [%no & fuel `(flop path)]
5766+ %atom [%yes & fuel ~]
5767+ %any-atom [%yes & fuel ~]
5768+ %flag [%yes & fuel ~]
5769+ %const [%yes & fuel ~]
5770+ %face $(typ body.typ, path [[%field name.typ] path])
5771+ %cell
5772+ =/ head=igate-free $(typ hed.typ, path [[%head ~] path])
5773+ =/ tail=igate-free $(typ tal.typ, fuel left.head, path [[%tail ~] path])
5774+ =/ inhabited=? &(inhabited.head inhabited.tail)
5775+ ?: |(&(=(%yes verdict.head) !inhabited.head) &(=(%yes verdict.tail) !inhabited.tail)) [%yes | left.tail ~]
5776+ ?: &(=(%no verdict.head) inhabited.tail) head(left left.tail)
5777+ ?: &(=(%no verdict.tail) inhabited.head) tail
5778+ ?: |(!=(%yes verdict.head) !=(%yes verdict.tail)) [%unknown inhabited left.tail ~]
5779+ [%yes inhabited left.tail ~]
5780+ %collection
5781+ ?. |(=(%list name.typ) =(%unit name.typ)) [%unknown | fuel ~]
5782+ ?. ?=([* ~] args.typ) [%unknown | fuel ~]
5783+ =/ item=igate-free $(typ i.args.typ, path [[%item ~] path])
5784+ item(inhabited &)
5785+ %union
5786+ ?~ cases.typ [%unknown | fuel ~]
5787+ (gate-free-types cases.typ fuel path 0)
5788+ %noun [%unknown & fuel ~]
5789+ %empty [%yes | fuel ~]
5790+ %var [%unknown | fuel ~]
5791+ %avar [%yes & fuel ~]
5792+ %rvar [%yes & fuel ~]
5793+ %nvar [%yes & fuel ~]
5794+ %rnvar [%yes & fuel ~]
5795+ %tag [%unknown | fuel ~]
5796+ %recursive [%unknown | fuel ~]
5797+ %jrec [%yes & fuel ~]
5798+ %grec [%unknown | fuel ~]
5799+ ==
5800+::
5801++$ igate-prelude-evidence [iface=ifile gates=(map term def)]
5802++$ dgo [left=itype right=itype at=span context=span]
5803++$ 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) gate-defs=(map term def) head-evidence=(unit igate-prelude-evidence) grec-index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)]) defer=(unit ~) obligations=(list dgo)]
53165804+$ idiag [msg=tape sites=(list [at=span note=tape])]
53175805+$ iresult (each [typ=itype state=istate] idiag)
53185806+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5332,6 +5820,7 @@
53325820 |= [t=itype sub=isub]
53335821 ^- itype
53345822 =. t (itype-walk t sub)
5823+ ?: ?=(%grec -.t) t(args (turn args.t |=(c=itype (itype-normalize c sub))))
53355824 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
53365825 ?: ?=(%union -.t)
53375826 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
@@ -5358,6 +5847,7 @@
53585847 %cell |($(t hed.t) $(t tal.t))
53595848 %recursive |
53605849 %jrec |
5850+ %grec &
53615851 %collection (lien args.t |=(c=itype (itype-has-gate c)))
53625852 %face $(t body.t)
53635853 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5365,11 +5855,14 @@
53655855 %const |
53665856 %var |
53675857 %avar |
5858+ %rvar |
53685859 %nvar |
5860+ %rnvar |
53695861 %atom |
53705862 %any-atom |
53715863 %flag |
53725864 %noun |
5865+ %empty |
53735866 ==
53745867::
53755868++ default-decimals
@@ -5378,6 +5871,8 @@
53785871 ?: (itype-has-gate t) t
53795872 ?- -.t
53805873 %nvar [%atom %ud]
5874+ %rnvar [%atom %ud]
5875+ %grec t(args (turn args.t |=(c=itype (default-decimals c))))
53815876 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
53825877 %face [%face name.t $(t body.t)]
53835878 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5394,7 +5889,9 @@
53945889 ?- -.t
53955890 %var `id.t
53965891 %avar `id.t
5892+ %rvar `id.t
53975893 %nvar `id.t
5894+ %rnvar `id.t
53985895 %tag `id.t
53995896 * ~
54005897 ==
@@ -5411,18 +5908,33 @@
54115908 ^- ?
54125909 =. t (itype-walk t sub.state)
54135910 ?- -.t
5414− ?(%var %avar %nvar)
5911+ ?(%var %avar %rvar %nvar %rnvar)
54155912 ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
54165913 (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
54175914 %tag |
54185915 %any-atom &
54195916 %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5917+ %grec (levy args.t |=(c=itype (hole-known c state)))
54205918 %collection (levy args.t |=(c=itype (hole-known c state)))
54215919 %face $(t body.t)
54225920 %fn &($(t sample.t) $(t product.t))
54235921 %cell &($(t hed.t) $(t tal.t))
54245922 * &
54255923 ==
5924+++ promote-restricted-numbers
5925+ |= [state=istate env=ienv]
5926+ ^- istate
5927+ :: With no written capitals, there is nothing to promote.
5928+ ?~ caps.state state
5929+ =/ ids=(list @ud) (turn caps.state |=(c=icap id.c))
5930+ =/ free=(list @ud) (free-env-vars env sub.state)
5931+ |-
5932+ ?~ ids state
5933+ =/ t=itype (itype-walk [%var i.ids] sub.state)
5934+ ?: &(?=(%rnvar -.t) !(lien free |=(n=@ud =(n +.t))))
5935+ $(ids t.ids, state state(sub [[+.t [%rvar +.t]] sub.state]))
5936+ $(ids t.ids)
5937+::
54265938++ default-hole-numbers
54275939 |= [all=(list ihole) prior=(list ihole) state=istate env=ienv permit=?]
54285940 ^- istate
@@ -5432,7 +5944,7 @@
54325944 ?~ all state
54335945 =/ t=itype (itype-walk [%var id.i.all] sub.state)
54345946 =/ free=(list @ud) (free-env-vars env sub.state)
5435− =? state &(?=(%nvar -.t) !(hole-known t state) !(lien free |=(id=@ud =(id id.t))))
5947+ =? state &(?=(?(%nvar %rnvar) -.t) !(hole-known t state) !(lien free |=(id=@ud =(id id.t))))
54365948 state(sub [[id.t [%atom %ud]] sub.state])
54375949 $(all t.all)
54385950::
@@ -5448,8 +5960,9 @@
54485960 ^- ?
54495961 =. t (itype-walk t sub.state)
54505962 ?- -.t
5451− ?(%tag %nvar %avar) !(hole-known t state)
5963+ ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
54525964 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5965+ %grec (lien args.t |=(c=itype (hole-uncertain c state)))
54535966 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
54545967 %face $(t body.t)
54555968 %fn |($(t sample.t) $(t product.t))
@@ -5474,16 +5987,20 @@
54745987 ?- -.t
54755988 %var ~[id.t]
54765989 %avar ~[id.t]
5990+ %rvar ~[id.t]
54775991 %nvar ~[id.t]
5992+ %rnvar ~[id.t]
54785993 %atom ~
54795994 %any-atom ~
54805995 %flag ~
54815996 %noun ~
5997+ %empty ~
54825998 %tag ~
54835999 %const ~
54846000 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
54856001 %recursive ~
54866002 %jrec ~
6003+ %grec (zing (turn args.t |=(c=itype (itype-vars c))))
54876004 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
54886005 %face $(t body.t)
54896006 %fn (weld $(t sample.t) $(t product.t))
@@ -5511,19 +6028,29 @@
55116028 =/ found=(unit itype) (itype-lookup id.t ren)
55126029 ?~ found t
55136030 u.found
6031+ %rvar
6032+ =/ found=(unit itype) (itype-lookup id.t ren)
6033+ ?~ found t
6034+ u.found
55146035 %nvar
55156036 =/ found=(unit itype) (itype-lookup id.t ren)
55166037 ?~ found t
55176038 u.found
6039+ %rnvar
6040+ =/ found=(unit itype) (itype-lookup id.t ren)
6041+ ?~ found t
6042+ u.found
55186043 %atom t
55196044 %any-atom t
55206045 %flag t
55216046 %noun t
6047+ %empty t
55226048 %tag t
55236049 %const t
55246050 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
55256051 %recursive t
55266052 %jrec t
6053+ %grec t(args (turn args.t |=(c=itype (itype-rename c ren))))
55276054 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
55286055 %face [%face name.t $(t body.t)]
55296056 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5539,21 +6066,50 @@
55396066 ?- -.t
55406067 %var |
55416068 %avar =(n id.t)
6069+ %rvar =(n id.t)
55426070 %nvar =(n id.t)
6071+ %rnvar =(n id.t)
55436072 %atom |
55446073 %any-atom |
55456074 %flag |
55466075 %noun |
6076+ %empty |
55476077 %tag |
55486078 %const |
55496079 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
55506080 %recursive |
55516081 %jrec |
6082+ %grec (lien args.t |=(c=itype (itype-var-is-atom n c)))
55526083 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
55536084 %face $(t body.t)
55546085 %fn |($(t sample.t) $(t product.t))
55556086 %cell |($(t hed.t) $(t tal.t))
55566087 ==
6088+++ itype-var-is-restricted
6089+ |= [n=@ud t=itype]
6090+ ^- ?
6091+ ?- -.t
6092+ %var |
6093+ %avar |
6094+ %rvar =(n id.t)
6095+ %nvar |
6096+ %rnvar |
6097+ %atom |
6098+ %any-atom |
6099+ %flag |
6100+ %noun |
6101+ %empty |
6102+ %tag |
6103+ %const |
6104+ %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
6105+ %recursive |
6106+ %jrec |
6107+ %grec (lien args.t |=(c=itype (itype-var-is-restricted n c)))
6108+ %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
6109+ %face $(t body.t)
6110+ %fn |($(t sample.t) $(t product.t))
6111+ %cell |($(t hed.t) $(t tal.t))
6112+ ==
55576113::
55586114:: Canonical numbering makes printed variables independent of the order
55596115:: the unifier happened to allocate intermediates.
@@ -5565,7 +6121,7 @@
55656121 =/ n=@ud 0
55666122 |-
55676123 ?~ vars (itype-rename t ren)
5568− =/ replacement=itype ?:((itype-var-is-atom i.vars t) [%avar n] [%var n])
6124+ =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] [%var n]))
55696125 $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
55706126::
55716127++ instantiate-scheme
@@ -5576,11 +6132,11 @@
55766132 |-
55776133 ?~ vars [(itype-rename typ.scheme ren) state]
55786134 =/ replacement=itype
5579− ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] [%var next.state])
6135+ ?:((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]))
55806136 :: A generalized atom variable is a valid origin for re-generalizing
55816137 :: an alias, just as a sample binder is.
55826138 =/ st=istate state(next +(next.state))
5583− =? binders.st ?=(%avar -.replacement) [next.state binders.state]
6139+ =? binders.st |(?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
55846140 $(vars t.vars, ren [[i.vars replacement] ren], state st)
55856141::
55866142++ icap-lookup
@@ -5845,6 +6401,7 @@
58456401 ^- upat
58466402 ?- -.typ
58476403 %noun [%all ~]
6404+ %empty [%empty ~]
58486405 %atom [%atom ~]
58496406 %flag [%or ~[[%atom `0] [%atom `1]]]
58506407 %const [%atom `val.literal.typ]
@@ -5941,16 +6498,31 @@
59416498 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
59426499 $(molds t.molds)
59436500::
5944−:: A public non-generic alias names exactly its origin and arguments.
5945−:: Reusing only an origin could print a different generic instantiation.
6501+:: A prelude union alias is a display name, not a new union identity. An
6502+:: identity-generic alias can carry the origin's arguments only when the
6503+:: origin, arity and ordered parameters match. Swapped, repeated, fixed
6504+:: or phantom parameters cannot be printed that way and remain unsupported
6505+:: when their only available name is private. A nongeneric alias of a
6506+:: generic instantiation cannot be printed with the origin's arguments.
6507+++ identity-union-parameters
6508+ |= [vars=(list @ud) args=(list itype)]
6509+ ^- ?
6510+ ?~ vars ?=(~ args)
6511+ ?~ args |
6512+ ?. =([%var i.vars] i.args) |
6513+ $(vars t.vars, args t.args)
59466514++ prelude-union-alias
59476515 |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
59486516 ^- (unit term)
5949− ?^ args ~
59506517 ?~ molds ~
59516518 =/ template=ischeme template.i.molds
5952− ?: &(?=(~ vars.template) ?=(%union -.typ.template))
5953− ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
6519+ ?. ?=(%union -.typ.template) $(molds t.molds)
6520+ ?. =(`origin origin.typ.template) $(molds t.molds)
6521+ ?~ vars.template
6522+ ?^ args $(molds t.molds)
6523+ ?:(=(args args.typ.template) `name.i.molds $(molds t.molds))
6524+ ?: &((identity-union-parameters vars.template args.typ.template) =((lent vars.template) (lent args)))
6525+ `name.i.molds
59546526 $(molds t.molds)
59556527::
59566528:: Names exported by the directly imported module are visible through its
@@ -5964,6 +6536,16 @@
59646536 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
59656537 $(molds t.molds)
59666538::
6539+++ grec-visible-alias
6540+ |= [origin=path name=term proof=shape args=(list itype) molds=imold-types]
6541+ ^- (unit term)
6542+ ?~ molds ~
6543+ =/ template=ischeme template.i.molds
6544+ ?. ?=(%grec -.typ.template) $(molds t.molds)
6545+ ?. &(=(at.typ.template origin) =(name.typ.template name) =(proof.typ.template proof)) $(molds t.molds)
6546+ ?. &((identity-union-parameters vars.template args.typ.template) =((lent vars.template) (lent args))) $(molds t.molds)
6547+ `name.i.molds
6548+::
59676549++ itype-in-import
59686550 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
59696551 ^- itype
@@ -5983,6 +6565,11 @@
59836565 `(crip "{(trip u.alias)}.{(trip face)}")
59846566 [%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)))]
59856567 %recursive [%recursive module.t name.t ~]
6568+ %grec
6569+ =/ public=(unit term) ?~(prelude ~ (grec-visible-alias at.t name.t proof.t args.t molds.u.prelude))
6570+ =/ alias=(unit term) ?~(public (grec-visible-alias at.t name.t proof.t args.t molds.iface) public)
6571+ =/ label=(unit @t) ?~(alias ~ ?~(public `(crip "{(trip u.alias)}.{(trip face)}") `u.alias))
6572+ t(label label, args (turn args.t |=(c=itype (itype-in-import c iface face prelude))))
59866573 %jrec
59876574 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
59886575 ?^ public t(label `u.public)
@@ -6095,9 +6682,29 @@
60956682 ?. =(names.tail ~[name]) ~
60966683 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
60976684::
6685+++ simple-source-generic-recursive
6686+ |= [name=term sh=shape args=(list itype) state=istate]
6687+ ^- (unit itype)
6688+ ?. ?=(%generic -.sh) ~
6689+ ?. ?=([@ ~] vars.sh) ~
6690+ ?. ?=([* ~] args) ~
6691+ ?~ grec-index.state ~
6692+ ?. =(at.u.grec-index.state at.state) ~
6693+ ?~ prelude.state ~
6694+ ?. =(prelude.u.grec-index.state u.prelude.state) ~
6695+ =/ proof=(unit shape) (~(get by shapes.u.grec-index.state) name)
6696+ ?~ proof ~
6697+ ?. =(u.proof sh) ~
6698+ `[%grec at.state name `name sh args]
6699+::
6700+
60986701++ infer-mold-template
60996702 |= [sh=shape state=istate]
61006703 ^- (unit [template=ischeme state=istate])
6704+ =/ generic=(unit itype)
6705+ ?. ?=([@ ~] active.state) ~
6706+ (simple-source-generic-recursive i.active.state sh ~[[%var next.state]] state)
6707+ ?^ generic `[[u.generic ~[next.state]] state(next +(next.state))]
61016708 =/ direct=(unit itype)
61026709 ?. ?=([@ ~] active.state) ~
61036710 (simple-source-recursive i.active.state sh state)
@@ -6155,7 +6762,7 @@
61556762 ?~ found ~
61566763 ?^ t.found ~
61576764 result.i.found
6158− ?. ?=([%invalid ?(%aura %core) @] raw) ~
6765+ ?. ?=([%invalid ?(%aura %core %overlap) @] raw) ~
61596766 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
61606767::
61616768:: Replay only the shape branches whose evaluation order we can prove.
@@ -6230,12 +6837,18 @@
62306837 `[[%atom aura.sh] state]
62316838 %flag `[[%flag ~] state]
62326839 %noun `[[%noun ~] state]
6840+ %void `[[%empty ~] state]
62336841 %const
6234− ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
6842+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh) =(%loobean form.lit.sh)) ~
6843+ ?: &(=(%loobean form.lit.sh) !|(=(0 val.lit.sh) =(1 val.lit.sh))) ~
62356844 `[[%const lit.sh] state]
62366845 %union
62376846 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6238− ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
6847+ ?: (lien pairs |=(p=upair =(%overlap relation.p))) ~
6848+ =/ source-proof=?
6849+ ?: (levy pairs |=(p=upair =(%disjoint relation.p))) &
6850+ &((union-source-state-safe state 256) (union-source-distinct-tags cases.sh molds.state 256))
6851+ ?. source-proof ~
62396852 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
62406853 ?~ cs ~
62416854 `[[%union types.u.cs ~ ~ ~] state.u.cs]
@@ -6309,6 +6922,8 @@
63096922 ?~ applied ~
63106923 `[u.applied state.u.args]
63116924 ?. ?=(%generic -.u.found) ~
6925+ =/ grec=(unit itype) (simple-source-generic-recursive n u.found types.u.args state.u.args)
6926+ ?^ grec `[u.grec state.u.args]
63126927 ?. (distinct-params vars.u.found) ~
63136928 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
63146929 ?~ params ~
@@ -6360,12 +6975,12 @@
63606975 ^- isample-result
63616976 ?- -.s
63626977 %bind
6363− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6978+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
63646979 [%| "sample shadows a name"]
63656980 =/ t=itype [%var next.state]
63666981 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
63676982 %face
6368− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6983+ ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
63696984 [%| "sample shadows a name"]
63706985 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
63716986 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -6433,6 +7048,7 @@
64337048 |-
64347049 ?~ ds &
64357050 ?: ?=(%mold -.i.ds) $(ds t.ds)
7051+ ?: =(name.i.ds %proj) |
64367052 ?. (unique-value-name name.i.ds names) |
64377053 ?: ?=(^ (ienv-lookup name.i.ds env)) |
64387054 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -6456,6 +7072,7 @@
64567072 |-
64577073 ?~ locals &
64587074 =/ n=term name.i.locals
7075+ ?: =(n %proj) |
64597076 ?. (unique-value-name n names) |
64607077 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
64617078 ?: (lien marks.state |=(m=term =(n m))) |
@@ -6635,6 +7252,8 @@
66357252 =/ retried=? ?=(%| -.inferred)
66367253 =? inferred retried (infer-recursive-gate d env local-state)
66377254 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7255+ ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7256+ =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
66387257 =. 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)))
66397258 =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
66407259 ?^ hole [%| u.hole]
@@ -6743,6 +7362,8 @@
67437362 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
67447363 (infer-list-context e expected env state context)
67457364 ?: ?=(%branch -.e)
7365+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
7366+ ?^ empty-list u.empty-list
67467367 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
67477368 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
67487369 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -6960,6 +7581,11 @@
69607581 [%| ["list pattern needs the standard prelude in partial inference" ~]]
69617582 ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
69627583 ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
7584+ =/ item-live=(unit [result=?(%yes %no %unknown) left=@ud])
7585+ (itype-inhabited-proof i.args.typ sub.state caps.state 256)
7586+ ?~ item-live [%| ["list element reachability needs unsupported inference" ~]]
7587+ ?: =(%unknown result.u.item-live) [%| ["list element reachability needs unsupported inference" ~]]
7588+ ?: =(%no result.u.item-live) [%| ["list nonempty pattern is unreachable" ~]]
69637589 ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
69647590 ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
69657591 ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
@@ -6972,7 +7598,7 @@
69727598 [%| ["list branch pattern is not supported by partial inference" ~]]
69737599 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
69747600 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6975− ?: |(=(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)))))
7601+ ?: |(=(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)))))
69767602 [%| ["pattern binder shadows a name" ~]]
69777603 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
69787604 =/ left=iresult
@@ -7009,10 +7635,15 @@
70097635 [%| ["unit branch pattern is not supported by partial inference" ~]]
70107636 =/ binder=(unit term) ?:(first-empty second-name first-name)
70117637 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
7012− ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
7638+ ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
70137639 [%| ["pattern binder shadows a name" ~]]
70147640 =/ payload=(unit itype) (unit-union-payload typ)
70157641 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
7642+ =/ payload-live=(unit [result=?(%yes %no %unknown) left=@ud])
7643+ (itype-inhabited-proof u.payload sub.state.p.subject caps.state.p.subject 256)
7644+ ?~ payload-live [%| ["unit payload reachability needs unsupported inference" ~]]
7645+ ?: =(%unknown result.u.payload-live) [%| ["unit payload reachability needs unsupported inference" ~]]
7646+ ?: =(%no result.u.payload-live) [%| ["unit present pattern is unreachable" ~]]
70167647 =/ extended=ienv [[u.binder [u.payload ~]] env]
70177648 =/ left=iresult
70187649 ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
@@ -7041,12 +7672,14 @@
70417672 =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
70427673 ?: |(?=(%atom -.t) ?=(%any-atom -.t))
70437674 $(ps t.ps, state state.p.item)
7044− ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
7675+ ?: &(|(?=(%nvar -.t) ?=(%rnvar -.t)) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
70457676 $(ps t.ps, state state.p.item)
70467677 ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
70477678 $(ps t.ps, state state.p.item)
70487679 ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
70497680 [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
7681+ ?: &(?=(%rvar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
7682+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
70507683 ?: ?=(%cell -.t)
70517684 [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
70527685 [%| ["interpolation type needs unsupported inference" ~]]
@@ -7109,7 +7742,7 @@
71097742 ^- (unit ienv)
71107743 =. t ?:(?=(%face -.t) body.t t)
71117744 ?: ?=(%bind -.p)
7112− ?: |(?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
7745+ ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
71137746 `[[name.p [t ~]] env]
71147747 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
71157748 `env
@@ -7163,7 +7796,9 @@
71637796 ?: ?=(%| -.subject) `subject
71647797 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
71657798 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7166− =/ cases=(list itype) cases.typ
7799+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7800+ ?~ live ~
7801+ =/ cases=(list itype) u.live
71677802 =/ remaining=(list itype) cases
71687803 =/ arms=(list arm) arms.e
71697804 =/ st=istate state.p.subject
@@ -7200,7 +7835,9 @@
72007835 ?: ?=(%| -.subject) `subject
72017836 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
72027837 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7203− =/ cases=(list itype) cases.typ
7838+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7839+ ?~ live ~
7840+ =/ cases=(list itype) u.live
72047841 =/ remaining=(list itype) cases
72057842 =/ arms=(list arm) arms.e
72067843 =/ st=istate state.p.subject
@@ -7244,7 +7881,9 @@
72447881 ?: ?=(%| -.subject) subject
72457882 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
72467883 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7247− =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7884+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7885+ ?~ live [%| ["union emptiness needs unsupported inference" ~]]
7886+ =/ expanded=(unit (list ifinite)) (finite-cases u.live ~ 0)
72487887 ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
72497888 =/ cases=(list ifinite) u.expanded
72507889 =/ remaining=(list ifinite) cases
@@ -7365,9 +8004,65 @@
73658004 =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
73668005 [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
73678006::
8007+:: A bounded source-proven tree match permits flat tag patterns and
8008+:: nonbinding catch-alls. Whole-case binders cannot consume the temporary
8009+:: structural view. Pattern count and field arity are checked first.
8010+++ grec-simple-pattern
8011+ |= [pat=pattern view=itype]
8012+ ^- ?
8013+ ?. ?=(%cell -.pat) |
8014+ ?~ items.pat |
8015+ =/ first=pattern i.items.pat
8016+ ?. ?=(%lit -.first) |
8017+ ?. =(%term form.lit.first) |
8018+ =/ chosen=(unit itype) (contextual-tagged-case view val.lit.first ~)
8019+ ?~ chosen |
8020+ ?> ?=(%cell -.u.chosen)
8021+ =/ rest=(list pattern) t.items.pat
8022+ =/ arity=? ?:(?=(%cell -.tal.u.chosen) ?=([* [* ~]] rest) ?=([* ~] rest))
8023+ ?. arity |
8024+ (levy rest |=(p=pattern |(?=(%bind -.p) ?=(%any -.p))))
8025+::
8026+:: A catch-all with no binder is safe even when it covers both cases.
8027+:: A bound whole case still declines to avoid exporting the analysis view.
8028+++ grec-patterns-eligible
8029+ |= [arms=(list arm) view=itype left=@ud]
8030+ ^- ?
8031+ ?~ arms &
8032+ ?: =(0 left) |
8033+ =/ pat=pattern pat.i.arms
8034+ ?. |(?=(%any -.pat) (grec-simple-pattern pat view)) |
8035+ $(arms t.arms, left (dec left))
8036+++ grec-match-view
8037+ |= [e=expr subject=iresult]
8038+ ^- iresult
8039+ ?: ?=(%| -.subject) subject
8040+ ?. ?=(%branch -.e) subject
8041+ ?. (grec-direct-context typ.p.subject sub.state.p.subject) subject
8042+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8043+ ?. ?=(%grec -.typ) subject
8044+ ?~ arms.e subject
8045+ =/ view=(unit [view=itype left=@ud]) (grec-unfold-view typ jrec-fuel.state.p.subject)
8046+ ?~ view [%| ["recursive mold unfolding needs unsupported inference" ~]]
8047+ ?. (grec-patterns-eligible arms.e view.u.view 128) subject
8048+ [%& view.u.view state.p.subject(jrec-fuel left.u.view)]
8049+::
8050+:: A single-arm diagnostic only probes a direct, source-typed in-scope wing;
8051+:: other subjects retain the prior single-pattern inference path.
8052+++ grec-single-wing-subject
8053+ |= [e=expr env=ienv state=istate]
8054+ ^- (unit iresult)
8055+ ?. ?=(%wing -.e) ~
8056+ ?. ?=([@ ~] names.e) ~
8057+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8058+ ?~ scheme ~
8059+ ?. (grec-direct-context typ.u.scheme sub.state) ~
8060+ `(infer-fragment e env state)
8061+::
73688062++ infer-known-union-branch-subject
73698063 |= [e=expr env=ienv subject=iresult]
73708064 ^- iresult
8065+ =. subject (grec-match-view e subject)
73718066 =. subject (jrec-match-view e subject)
73728067 =/ whole=(unit iresult) (infer-known-union-whole e env subject)
73738068 ?~ whole (infer-known-union-finite e env subject ~)
@@ -7382,6 +8077,7 @@
73828077++ infer-known-union-context-subject
73838078 |= [e=expr expected=itype env=ienv subject=iresult context=span]
73848079 ^- iresult
8080+ =. subject (grec-match-view e subject)
73858081 =. subject (jrec-match-view e subject)
73868082 =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
73878083 ?~ whole (infer-known-union-finite e env subject `[expected context])
@@ -7434,9 +8130,67 @@
74348130 =/ subject=iresult (infer-fragment e env state)
74358131 ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
74368132 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7437− ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
8133+ ?. |(?=(%union -.typ) ?=(%jrec -.typ) &(?=(%grec -.typ) (grec-direct-context typ.p.subject sub.state.p.subject))) ~
74388134 `subject
74398135::
8136+:: A direct wing with an already-known union may skip genuinely empty cases
8137+:: when checking a one-arm match. Other subjects keep their existing path.
8138+:: A directly known canonical list of an empty element contains only null.
8139+:: This helper never refines an opaque or variable-bound subject.
8140+++ empty-list-null-branch
8141+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
8142+ ^- (unit iresult)
8143+ ?. ?=(%branch -.e) ~
8144+ ?~ arms.e ~
8145+ ?^ t.arms.e ~
8146+ ?. (unit-empty-pattern pat.i.arms.e) ~
8147+ ?. ?=(%wing -.subject.e) ~
8148+ ?. ?=([@ ~] names.subject.e) ~
8149+ =/ scheme=(unit ischeme) (ienv-lookup i.names.subject.e env)
8150+ ?~ scheme ~
8151+ ?. ?=(%collection -.typ.u.scheme) ~
8152+ ?. =(%list name.typ.u.scheme) ~
8153+ ?~ prelude.state ~
8154+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb) ~
8155+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
8156+ ?~ standard ~
8157+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~
8158+ =/ subject=iresult (infer-fragment subject.e env state)
8159+ ?: ?=(%| -.subject) ~
8160+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8161+ ?. ?=(%collection -.typ) ~
8162+ ?. =(%list name.typ) ~
8163+ ?~ args.typ ~
8164+ ?^ t.args.typ ~
8165+ =/ proof=(unit [empty=? left=@ud]) (itype-empty-proof i.args.typ sub.state.p.subject 256)
8166+ ?~ proof ~
8167+ ?. empty.u.proof ~
8168+ ?~ expected `(infer-fragment val.i.arms.e env state.p.subject)
8169+ =/ body=iresult (infer-call-context-arg val.i.arms.e typ.u.expected env state.p.subject context.u.expected)
8170+ ?: ?=(%| -.body) `body
8171+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
8172+ ?: ?=(%unknown -.fit) `[%| ["single-case branch result constraint is not supported by partial inference" ~]]
8173+ ?: ?=(%bad -.fit) `[%| ["single-case branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.i.arms.e) "branch arm"]]]]
8174+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8175+ `[%| ["single-case branch result needs context in partial inference" ~]]
8176+ `[%& typ.p.body state.p.body(sub sub.fit, next next.fit)]
8177+::
8178+++ known-empty-union-wing
8179+ |= [e=expr env=ienv state=istate]
8180+ ^- (unit iresult)
8181+ ?. ?=(%wing -.e) ~
8182+ ?. ?=([@ ~] names.e) ~
8183+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8184+ ?~ scheme ~
8185+ ?. (contextual-direct-union typ.u.scheme) ~
8186+ =/ subject=iresult (infer-fragment e env state)
8187+ ?: ?=(%| -.subject) ~
8188+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8189+ ?. ?=(%union -.typ) ~
8190+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
8191+ ?~ live ~
8192+ ?: =(u.live cases.typ) ~
8193+ `subject
74408194::
74418195:: Infer changes only against a fully known record spine. Retain the
74428196:: target type; unknown spines and repeated edits remain unsupported.
@@ -7543,7 +8297,7 @@
75438297 |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
75448298 ^- (unit idiag)
75458299 =/ original=[left=itype right=itype] [actual expected]
7546− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
8300+ ?: |(?=(%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))) ~
75478301 =/ fit=ifit (itype-fit actual expected sub next)
75488302 ?. ?=(%bad -.fit) ~
75498303 =. actual (itype-walk actual sub)
@@ -7564,7 +8318,7 @@
75648318 ?~ items ~
75658319 ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
75668320 =/ original=[left=itype right=itype] [actual expected]
7567− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
8321+ ?: |(?=(%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))) ~
75688322 =. actual (itype-walk actual sub)
75698323 =. expected (itype-walk expected sub)
75708324 ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
@@ -7704,8 +8458,15 @@
77048458 ?: ?=(%| -.result) result
77058459 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
77068460 %branch
8461+ ?^ defer.state (dg-boolean-branch e env state)
77078462 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
77088463 ?~ t.arms.e
8464+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state ~)
8465+ ?^ empty-list u.empty-list
8466+ =/ empty-union=(unit iresult) (known-empty-union-wing subject.e env state)
8467+ ?^ empty-union (infer-known-union-branch-subject e env u.empty-union)
8468+ =/ single=(unit iresult) (grec-single-wing-subject subject.e env state)
8469+ ?^ single (infer-known-union-branch-subject e env u.single)
77098470 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
77108471 (infer-cell-branch e env state ~)
77118472 ?^ t.t.arms.e (infer-known-union-branch e env state)
@@ -7762,6 +8523,9 @@
77628523 =/ value=iresult
77638524 (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
77648525 ?: ?=(%| -.value) value
8526+ =/ shape=(unit [source=iwfields target=iwfields])
8527+ (width-shape typ.p.value typ.u.target sub.state.p.value)
8528+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
77658529 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
77668530 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
77678531 ?: ?=(%bad -.fit)
@@ -7770,6 +8534,8 @@
77708534 =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value at.shape.e)
77718535 ?^ nested [%| u.nested]
77728536 [%| ["cast mold and expression type do not unify" ~[[at.shape.e (site-type-note "cast mold" typ.u.target sub.state.p.value)] [(span-of val.e) (site-type-note "expression" typ.p.value sub.state.p.value)]]]]
8537+ ?: &(?=(^ defer.state.p.value) !(dg-stable-fit typ.p.value typ.u.target sub.fit))
8538+ [%| ["deferred cast fit needs stable inference" ~]]
77738539 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
77748540 [%& merged state.p.value(sub sub.fit, next next.fit)]
77758541 %crash [%& [%var next.state] state(next +(next.state))]
@@ -7793,6 +8559,8 @@
77938559 [%& [%fn typ.p.sam typ.p.body] state.p.body]
77948560 %call
77958561 ?~ args.e [%| ["call has no argument" ~]]
8562+ ?: (explicit-proj-call e env state)
8563+ [%| ["proj needs an expected record type" ~]]
77968564 (infer-call-with-head e env state (infer-fragment head.e env state))
77978565 * [%| ["expression is not supported by partial inference" ~]]
77988566 ==
@@ -7803,6 +8571,248 @@
78038571::
78048572:: Check a call using the head already inferred in this state. Keeping
78058573:: this shared avoids evaluating or instantiating a contextual head twice.
8574+++ width-has-projections
8575+ |= ps=(list iwprojection)
8576+ ^- ?
8577+ ?~ ps |
8578+ &
8579+::
8580++$ iwidth-elaboration [original=expr typ=itype sub=isub projections=(list iwprojection)]
8581+++ infer-width-elaboration
8582+ |= [e=expr env=ienv state=istate]
8583+ ^- (each iwidth-elaboration idiag)
8584+ =/ out=iresult (infer-fragment e env state)
8585+ ?: ?=(%| -.out) [%| p.out]
8586+ [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
8587+::
8588+:: Source-bound gate-layout evidence, confined to checked root gate
8589+:: definitions and direct unshadowed prelude calls. The prepared prelude
8590+:: interface and its retained source are trusted as a matching artifact.
8591+:: Layouts identify sample binder faces; they do not change call arity or
8592+:: authorize stripping nested value faces. Unknown origins use ordinary fit.
8593+++ direct-written-gates
8594+ |= [ds=(list def) out=ivisited]
8595+ ^- ivisited
8596+ ?~ ds out
8597+ ?: ?=(%mold -.i.ds) $(ds t.ds)
8598+ ?. |(?=(%gate -.val.i.ds) ?=(%gate-wide -.val.i.ds)) $(ds t.ds)
8599+ $(ds t.ds, out (~(put by out) name.i.ds &))
8600+++ direct-may-use-prelude
8601+ |= [ds=(list def) root=ivisited heads=ivisited]
8602+ ^- ?
8603+ ?~ ds |
8604+ ?: ?=(%mold -.i.ds) $(ds t.ds)
8605+ =/ refs=(list term) (dependency-expr val.i.ds)
8606+ =/ has-root=? (lien refs |=(n=term ?=(^ (~(get by root) n))))
8607+ =/ has-head=? (lien refs |=(n=term ?=(^ (~(get by heads) n))))
8608+ ?: &(has-root has-head) &
8609+ $(ds t.ds)
8610+++ direct-unique-names
8611+ |= [names=(list term) seen=ivisited]
8612+ ^- ?
8613+ ?~ names &
8614+ ?: ?=(^ (~(get by seen) i.names)) |
8615+ $(names t.names, seen (~(put by seen) i.names &))
8616+++ direct-prelude-evidence
8617+ |= [ds=(list def) prelude=(unit ifile)]
8618+ ^- (unit igate-prelude-evidence)
8619+ ?~ prelude ~
8620+ ?~ source.u.prelude ~
8621+ =/ root=ivisited (direct-written-gates ds ~)
8622+ =/ names=(list term) (turn values.u.prelude |=(e=[name=term scheme=ischeme] name.e))
8623+ =/ heads=ivisited (graph-nameset names ~)
8624+ ?. (direct-may-use-prelude ds root heads) ~
8625+ =/ parsed (parse at.u.prelude u.source.u.prelude)
8626+ ?: ?=(%| -.parsed) ~
8627+ ?^ (duplicate-defs defs.p.parsed) ~
8628+ ?. (direct-unique-names (global-value-names defs.p.parsed) ~) ~
8629+ =/ gates=(map term def) (direct-checked-gates defs.p.parsed values.u.prelude)
8630+ `[u.prelude gates]
8631+++ direct-checked-gates
8632+ |= [ds=(list def) env=ienv]
8633+ ^- (map term def)
8634+ =/ names=(list term) (turn env |=(e=[name=term scheme=ischeme] name.e))
8635+ =/ known=ivisited (graph-nameset names ~)
8636+ =/ out=(map term def) ~
8637+ |-
8638+ ?~ ds out
8639+ =/ d=def i.ds
8640+ ?: ?=(%mold -.d) $(ds t.ds)
8641+ ?. ?=(^ (~(get by known) name.d)) $(ds t.ds)
8642+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) $(ds t.ds)
8643+ $(ds t.ds, out (~(put by out) name.d d))
8644+++ direct-find-gate
8645+ |= [n=term ds=(list def)]
8646+ ^- (unit def)
8647+ ?~ ds ~
8648+ ?: &(?=(%value -.i.ds) =(n name.i.ds)) `i.ds
8649+ $(ds t.ds)
8650+++ direct-gate-sample
8651+ |= d=def
8652+ ^- (unit sample)
8653+ ?. ?=(%value -.d) ~
8654+ ?- -.val.d
8655+ %gate `sample.val.d
8656+ %gate-wide `sample.val.d
8657+ * ~
8658+ ==
8659+++ direct-sample-name
8660+ |= sam=sample
8661+ ^- (unit term)
8662+ ?- -.sam
8663+ %bind `name.sam
8664+ %face `name.sam
8665+ %pun `name.sam
8666+ * ~
8667+ ==
8668+++ direct-field-name
8669+ |= f=field
8670+ ^- (unit term)
8671+ ?- -.f
8672+ %face `name.f
8673+ %pun `name.f
8674+ * ~
8675+ ==
8676+++ direct-slot-body
8677+ |= [typ=itype name=(unit term)]
8678+ ^- (unit itype)
8679+ ?~ name `typ
8680+ ?. ?=(%face -.typ) ~
8681+ ?. =(name.typ u.name) ~
8682+ `body.typ
8683+++ direct-invariant
8684+ |= [a=itype b=itype sub=isub next=@ud]
8685+ ^- ifit
8686+ ?: (itype-face-asym a b sub) [%unknown ~]
8687+ =/ forward=ifit (itype-fit a b sub next)
8688+ ?. ?=(%ok -.forward) [%unknown ~]
8689+ ?: (itype-face-asym a b sub.forward) [%unknown ~]
8690+ =/ reverse=ifit (itype-fit b a sub.forward next.forward)
8691+ ?. ?=(%ok -.reverse) [%unknown ~]
8692+ reverse
8693+++ direct-function-fit
8694+ |= [a=itype b=itype sam=sample sh=shape sub=isub next=@ud]
8695+ ^- ifit
8696+ ?. &(?=(%fn -.a) ?=(%fn -.b) ?=(%cell -.sam) ?=(%fn -.sh)) [%unknown ~]
8697+ ?. ?=(%cell -.sample.sh) [%unknown ~]
8698+ =/ as=(list sample) items.sam
8699+ =/ bs=(list field) fields.sample.sh
8700+ ?~ as [%unknown ~]
8701+ ?~ t.as [%unknown ~]
8702+ ?^ t.t.as [%unknown ~]
8703+ ?~ bs [%unknown ~]
8704+ ?~ t.bs [%unknown ~]
8705+ ?^ t.t.bs [%unknown ~]
8706+ ?. &(?=(%cell -.sample.a) ?=(%cell -.sample.b)) [%unknown ~]
8707+ =/ an=(unit term) (direct-sample-name i.as)
8708+ =/ bn=(unit term) (direct-field-name i.bs)
8709+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]
8710+ =/ x=(unit itype) (direct-slot-body hed.sample.a an)
8711+ =/ y=(unit itype) (direct-slot-body hed.sample.b bn)
8712+ ?~ x [%unknown ~]
8713+ ?~ y [%unknown ~]
8714+ =/ first=ifit (direct-invariant u.x u.y sub next)
8715+ ?. ?=(%ok -.first) [%unknown ~]
8716+ =. an (direct-sample-name i.t.as)
8717+ =. bn (direct-field-name i.t.bs)
8718+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]
8719+ =/ x2=(unit itype) (direct-slot-body tal.sample.a an)
8720+ =/ y2=(unit itype) (direct-slot-body tal.sample.b bn)
8721+ ?~ x2 [%unknown ~]
8722+ ?~ y2 [%unknown ~]
8723+ =/ second=ifit (direct-invariant u.x2 u.y2 sub.first next.first)
8724+ ?. ?=(%ok -.second) [%unknown ~]
8725+ (direct-invariant product.a product.b sub.second next.second)
8726+:: This is a tentative proof: its caller must require closed call samples
8727+:: and repeat every positional check under the stable final substitution.
8728+++ direct-positional-fit
8729+ |= [args=(list expr) slots=(list sample) actual=itype expected=itype env=ienv state=istate sub=isub next=@ud]
8730+ ^- ifit
8731+ ?~ args [%unknown ~]
8732+ ?~ slots [%unknown ~]
8733+ =/ last=? ?=(~ t.args)
8734+ ?: !=(last ?=(~ t.slots)) [%unknown ~]
8735+ =/ split=(unit [left=itype right=itype])
8736+ ?: last `[actual expected]
8737+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8738+ `[hed.actual hed.expected]
8739+ ?~ split [%unknown ~]
8740+ =/ x=itype left.u.split
8741+ =/ y=itype right.u.split
8742+ =/ expected-name=(unit term) (direct-sample-name i.slots)
8743+ =/ expected-body=(unit itype) (direct-slot-body y expected-name)
8744+ ?~ expected-body [%unknown ~]
8745+ =. y u.expected-body
8746+ =/ fit=ifit (itype-fit x y sub next)
8747+ =/ accepted=? &(?=(%ok -.fit) !(itype-positional-slot-face-asym x y sub.fit))
8748+ =/ result=(unit ifit)
8749+ ?: accepted `fit
8750+ ?. &(?=(%face -.i.slots) ?=(%fn -.shape.i.slots)) ~
8751+ ?. ?=(%wing -.i.args) ~
8752+ ?. ?=([@ ~] names.i.args) ~
8753+ ?. (unique-value-name i.names.i.args globals.state) ~
8754+ =/ source=(unit def) (~(get by gate-defs.state) i.names.i.args)
8755+ ?~ source ~
8756+ =/ sample=(unit sample) (direct-gate-sample u.source)
8757+ ?~ sample ~
8758+ =/ trial=ifit (direct-function-fit x y u.sample shape.i.slots sub next)
8759+ ?. ?=(%ok -.trial) ~
8760+ `trial
8761+ ?~ result [%unknown ~]
8762+ =. fit u.result
8763+ ?: last fit
8764+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
8765+ ?. ?=(%ok -.fit) [%unknown ~]
8766+ $(args t.args, slots t.slots, actual tal.actual, expected tal.expected, sub sub.fit, next next.fit)
8767+++ direct-any-gate-arg
8768+ |= [args=(list expr) defs=(map term def)]
8769+ ^- ?
8770+ ?~ args |
8771+ =/ found=?
8772+ ?. ?=(%wing -.i.args) |
8773+ ?. ?=([@ ~] names.i.args) |
8774+ ?=(^ (~(get by defs) i.names.i.args))
8775+ ?: found &
8776+ $(args t.args)
8777+++ direct-gate-call-fit
8778+ |= [e=expr actual=itype expected=itype env=ienv state=istate]
8779+ ^- (unit ifit)
8780+ ?. ?=(%call -.e) ~
8781+ ?~ args.e ~
8782+ ?~ t.args.e ~
8783+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8784+ ?. ?=(%wing -.head.e) ~
8785+ ?. ?=([@ ~] names.head.e) ~
8786+ ?. ?=(~ (ienv-lookup i.names.head.e env)) ~
8787+ ?. (unique-value-name i.names.head.e globals.state) ~
8788+ ?. (direct-any-gate-arg args.e gate-defs.state) ~
8789+ ?~ prelude.state ~
8790+ ?~ source.u.prelude.state ~
8791+ ?~ head-evidence.state ~
8792+ ?. =(u.prelude.state iface.u.head-evidence.state) ~
8793+ ?. ?=(^ (ienv-lookup i.names.head.e values.u.prelude.state)) ~
8794+ =/ head=(unit def) (~(get by gates.u.head-evidence.state) i.names.head.e)
8795+ ?~ head ~
8796+ =/ sam=(unit sample) (direct-gate-sample u.head)
8797+ ?~ sam ~
8798+ ?. ?=(%cell -.u.sam) ~
8799+ =/ fit=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.state next.state)
8800+ ?. ?=(%ok -.fit) ~
8801+ :: Enclosing inference may add constraints after this call. Only a
8802+ :: closed call-sample proof can remain stable under those later bindings.
8803+ =/ actual-final=itype (itype-normalize actual sub.fit)
8804+ =/ expected-final=itype (itype-normalize expected sub.fit)
8805+ ?^ (itype-vars actual-final) ~
8806+ ?^ (itype-vars expected-final) ~
8807+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
8808+ :: A later argument may resolve a variable used by an earlier slot.
8809+ :: Recheck every fit and face against the completed substitution; no
8810+ :: additional binding or fresh variable is permitted in the second pass.
8811+ =/ verified=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.fit next.fit)
8812+ ?. ?=(%ok -.verified) ~
8813+ ?. &(=(sub.fit sub.verified) =(next.fit next.verified)) ~
8814+ `fit
8815+::
78068816++ infer-call-with-head
78078817 |= [e=expr env=ienv state=istate head=iresult]
78088818 ^- iresult
@@ -7822,8 +8832,24 @@
78228832 =/ st=istate state.p.arg
78238833 =/ ht=itype (itype-walk typ.p.head sub.st)
78248834 ?: ?=(%fn -.ht)
7825− =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
7826− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
8835+ =/ shape=(unit [source=iwfields target=iwfields])
8836+ ?^ t.args.e ~
8837+ (width-shape typ.p.arg sample.ht sub.st)
8838+ ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
8839+ =/ fit=ifit
8840+ ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
8841+ (itype-fit typ.p.arg sample.ht sub.st next.st)
8842+ =/ direct=(unit ifit)
8843+ ?: ?=(%ok -.fit) ~
8844+ (direct-gate-call-fit e typ.p.arg sample.ht env st)
8845+ =. fit ?~(direct fit u.direct)
8846+ ?: ?=(%unknown -.fit)
8847+ ?~ defer.st [%| ["call constraint is not supported by partial inference" ~]]
8848+ =/ edge=(unit dgo) (dg-eligible-ctor e typ.p.head typ.p.arg sample.ht st)
8849+ ?~ edge [%| ["call constraint is not supported by partial inference" ~]]
8850+ ?: (gth (lent obligations.st) 63) [%| ["call constraint is not supported by partial inference" ~]]
8851+ [%& product.ht st(obligations [u.edge obligations.st])]
8852+
78278853 ?: ?=(%bad -.fit)
78288854 ?~ t.args.e
78298855 =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
@@ -7838,7 +8864,13 @@
78388864 =/ arg-at=span ?~(bad whole-args at.u.bad)
78398865 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
78408866 [%| ["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)]]]]
7841− ?: &((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))
8867+ ?: &(?=(^ defer.st) !(dg-stable-call-fit typ.p.arg sample.ht product.ht sub.fit ?=(^ t.args.e)))
8868+ [%| ["deferred call fit needs stable inference" ~]]
8869+ =/ face-asym=?
8870+ ?^ direct |
8871+ ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
8872+ (itype-face-asym typ.p.arg sample.ht sub.fit)
8873+ ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
78428874 [%| ["call result face propagation is not supported by partial inference" ~]]
78438875 [%& product.ht st(sub sub.fit, next next.fit)]
78448876 =/ result=itype [%var next.st]
@@ -7852,7 +8884,7 @@
78528884 ^- (unit [at=span typ=itype])
78538885 ?~ args ~
78548886 =/ original=[left=itype right=itype] [actual expected]
7855− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
8887+ ?: |(?=(%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))) ~
78568888 =. actual (itype-walk actual sub)
78578889 =. expected (itype-walk expected sub)
78588890 ?: &(?=(%face -.expected) !?=(%face -.actual))
@@ -7902,9 +8934,10 @@
79028934 [%| ["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)]]]]
79038935 [%& expected state.p.value(sub sub.fit, next next.fit)]
79048936::
7905−:: A known gate whose result is still an inference variable can receive
7906−:: an enclosing target before its argument is inferred. Other products
7907−:: and unresolved calls use the existing directional path unchanged.
8937+:: A known gate may receive an enclosing target before its argument is
8938+:: inferred when its result is open or a direct, matching named generic
8939+:: union. Opaque, recursive, tag-constrained and variable-bound union
8940+:: results keep the existing directional path.
79088941++ infer-contextual-call
79098942 |= [e=expr expected=itype env=ienv state=istate]
79108943 ^- iresult
@@ -7915,64 +8948,374 @@
79158948 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
79168949 ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
79178950 =/ result=itype (itype-walk product.ht sub.state.p.head)
7918− ?. ?=(%var -.result) (infer-call-with-head e env state head)
7919− ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected) (itype-has-tag (itype-normalize expected sub.state.p.head)))
8951+ =/ eligible=?
8952+ ?: ?=(%var -.result) &
8953+ :: A direct known generic union may receive the same nominal result
8954+ :: context before its arguments are checked. Variable-bound origins,
8955+ :: pending tags, recursive identities and unknown atoms stay open.
8956+ ?. &(?=(%union -.product.ht) ?=(%union -.result) ?=(%union -.expected)) |
8957+ ?~ origin.result |
8958+ ?. =(origin.result origin.expected) |
8959+ ?~ args.result |
8960+ ?. =((lent args.result) (lent args.expected)) |
8961+ ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
8962+ ?: |((itype-has-recursive (itype-normalize result sub.state.p.head)) (itype-has-recursive (itype-normalize expected sub.state.p.head))) |
8963+ ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
8964+ &
8965+ ?. eligible (infer-call-with-head e env state head)
8966+ ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)) (itype-has-tag (itype-normalize expected sub.state.p.head)))
79208967 (infer-call-with-head e env state head)
79218968 =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
79228969 ?~ sub (infer-call-with-head e env state head)
79238970 (infer-call-with-head e env state [%& typ.p.head state.p.head(sub u.sub)])
79248971::
7925−++ infer-call-context-arg
8972+:: An eligible fully faced literal receives context by name, in source order.
8973+++ width-literal-fields
8974+ |= [items=(list item) axis=@ud fuel=@ud]
8975+ ^- (unit iwfields)
8976+ =/ order=(list iwfield) ~
8977+ =/ index=(map term iwfield) *(map term iwfield)
8978+ |-
8979+ ?~ items ~
8980+ ?: =(0 fuel) ~
8981+ ?~ face.i.items ~
8982+ =/ at-axis=@ud ?~(t.items axis (mul 2 axis))
8983+ =/ entry=iwfield [u.face.i.items at-axis [%noun ~]]
8984+ ?: ?=(^ (~(get by index) name.entry)) ~
8985+ =. index (~(put by index) name.entry entry)
8986+ =. order [entry order]
8987+ ?~ t.items `[(flop order) index]
8988+ $(items t.items, axis +((mul 2 axis)), fuel (dec fuel))
8989+++ width-infer-items
8990+ |= [items=(list item) expected=(map term iwfield) env=ienv state=istate context=span]
8991+ ^- iresult
8992+ ?~ items [%| ["empty record is not supported" ~]]
8993+ ?~ face.i.items [%| ["record face needs unsupported inference" ~]]
8994+ =/ field=(unit iwfield) (~(get by expected) u.face.i.items)
8995+ =/ head=iresult
8996+ ?~ field (infer-fragment val.i.items env state)
8997+ (infer-call-context-arg val.i.items typ.u.field env state context)
8998+ ?: ?=(%| -.head) head
8999+ =/ typ=itype [%face u.face.i.items typ.p.head]
9000+ ?~ t.items [%& typ state.p.head]
9001+ =/ tail=iresult $(items t.items, state state.p.head)
9002+ ?: ?=(%| -.tail) tail
9003+ [%& [%cell typ typ.p.tail] state.p.tail]
9004+++ width-infer-literal
9005+ |= [e=expr expected=itype env=ienv state=istate context=span]
9006+ ^- (unit iresult)
9007+ ?. ?=(%tuple -.e) ~
9008+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) ~
9009+ =/ source=(unit iwfields) (width-literal-fields items.e 1 4.096)
9010+ =/ target=(unit iwfields) (width-scan expected sub.state 1 4.096)
9011+ ?~ source ~
9012+ ?~ target ~
9013+ ?: (lth (lent order.u.source) (lent order.u.target)) ~
9014+ ?. (width-in-order order.u.source order.u.target)
9015+ `(infer-simple-items items.e env state)
9016+ `(width-infer-items items.e index.u.target env state context)
9017+::
9018+:: Experimental intrinsic recognition; real bindings retain normal calls.
9019+++ explicit-proj-call
9020+ |= [e=expr env=ienv state=istate]
9021+ ^- ?
9022+ ?. ?=(%call -.e) |
9023+ ?. ?=([* ~] args.e) |
9024+ ?. ?=(%wing -.head.e) |
9025+ ?. =(names.head.e ~[%proj]) |
9026+ ?: ?=(^ (ienv-lookup %proj env)) |
9027+ ?: (lien globals.state |=(n=term =(n %proj))) |
9028+ ?~ prelude.state &
9029+ ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
9030+++ infer-proj-source
79269031 |= [e=expr expected=itype env=ienv state=istate context=span]
79279032 ^- iresult
7928− ?: ?=(%pair -.e) $(e (pair-as-cell e))
79299033 ?: ?=(%group -.e) $(e inner.e)
7930− ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7931− ?: ?=(%trace -.e)
7932− =/ traced=iresult (infer-fragment val.e env state)
7933− ?: ?=(%| -.traced) traced
7934− $(e then.e, state state.p.traced)
7935− =/ target=itype (itype-walk expected sub.state)
9034+ =/ literal=(unit iresult) (width-infer-literal e expected env state context)
9035+ ?^ literal u.literal
9036+ (infer-fragment e env state)
9037+++ infer-proj-context
9038+ |= [e=expr expected=itype env=ienv state=istate context=span]
9039+ ^- iresult
9040+ ?> ?=(%call -.e)
9041+ ?~ args.e [%| ["proj needs one record" ~]]
9042+ ?. |(?=(%cell -.expected) ?=(%face -.expected)) [%| ["proj needs an expected record type" ~]]
9043+ =/ value=iresult (infer-proj-source i.args.e expected env state context)
9044+ ?: ?=(%| -.value) value
9045+ =/ shape=(unit [source=iwfields target=iwfields])
9046+ (width-proj-shape typ.p.value expected sub.state.p.value)
9047+ ?~ shape [%| ["proj needs a known record containing its expected fields" ~]]
9048+ =/ project=(unit iwidth-result) (width-project u.shape sub.state.p.value next.state.p.value)
9049+ ?~ project [%| ["proj constraint needs unsupported inference" ~]]
9050+ =/ st=istate state.p.value(sub sub.u.project, next next.u.project)
9051+ [%& expected st(projections [[at.e e typ.p.value expected steps.u.project] projections.st])]
9052+::
9053+:: A known literal singleton in a direct union can contextualize a
9054+:: loobean literal of the same noun. Only explicit singleton and cell
9055+:: competitors are considered; opaque or variable cases stay unknown.
9056+++ explicit-singleton-in-union
9057+ |= [t=itype noun=@]
9058+ ^- ?
9059+ ?. ?=(%union -.t) |
9060+ =/ cases=(list itype) cases.t
9061+ =/ found=? |
79369062 |-
7937− ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7938− :: Only the source-proven one-layer cell is exposed. Each recursive
7939− :: descent consumes one written tuple; named values use ordinary fit.
7940− ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
7941− ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
7942− [%& target state(jrec-fuel (dec jrec-fuel.state))]
7943− ?: &(?=(%jrec -.target) ?=(%tuple -.e))
7944− ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
7945− =. state state(jrec-fuel (dec jrec-fuel.state))
7946− =/ shape=itype
7947− [%cell [%face head.target [%atom aura.target]] [%face tail.target target]]
7948− =/ value=iresult (infer-call-context-items items.e shape env state context)
7949− ?: ?=(%| -.value) value
7950− =/ fit=ifit (itype-fit typ.p.value shape sub.state.p.value next.state.p.value)
7951− ?: ?=(%unknown -.fit) [%| ["recursive mold cell constraint needs unsupported inference" ~]]
7952− ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
7953− [%& target state.p.value(sub sub.fit, next next.fit)]
7954− ?: ?=(%call -.e) (infer-contextual-call e target env state)
7955− ?: (single-structured-pattern e)
7956− (infer-single-case-branch e env state `[target context])
7957− ?: (cell-binder-pattern e)
7958− (infer-cell-branch e env state `[target context])
7959− :: In a loobean-singleton context retain the written loobean noun;
7960− :: the usual final fit decides whether that value is permitted.
7961− =/ singleton=(unit itype)
7962− ?. ?=(%lit -.e) ~
7963− ?. =(%loobean form.lit.e) ~
7964− ?. ?=(%const -.target) ~
7965− ?. =(%loobean form.literal.target) ~
7966− `[%const lit.e]
7967− ?^ singleton [%& u.singleton state]
7968− =/ known=(unit iresult)
7969− ?: ?=(%branch -.e) (known-union-subject subject.e env state)
7970− ~
7971− ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
7972− ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
7973− (infer-known-union-context-subject e target env u.known context)
9063+ ?~ cases found
9064+ =/ c=itype i.cases
9065+ ?: ?=(%cell -.c) $(cases t.cases)
9066+ ?. ?=(%const -.c) |
9067+ ?: =(noun val.literal.c)
9068+ ?: found |
9069+ $(cases t.cases, found &)
9070+ $(cases t.cases)
9071+::
9072+:: Select a written literal-headed case only when every competing case is
9073+:: also an explicit singleton-headed cell and exactly one matches. Opaque,
9074+:: variable-bound and differently shaped cases keep inference unchanged.
9075+:: This first slice supplies context to a directly called payload. Plain
9076+:: literal data and other expressions retain their existing inference path.
9077+++ contextual-atomic-arguments
9078+ |= args=(list expr)
9079+ ^- ?
9080+ ?~ args &
9081+ ?. ?=(?(%lit %wing %ctor) -.i.args) |
9082+ $(args t.args)
9083+++ contextual-direct-payload-call
9084+ |= e=expr
9085+ ^- ?
9086+ ?: ?=(%group -.e) $(e inner.e)
9087+ ?. ?=(%call -.e) |
9088+ ?. ?=(%wing -.head.e) |
9089+ ?~ args.e |
9090+ (contextual-atomic-arguments args.e)
9091+::
9092+:: A walked variable may have concealed a union inside a substituted
9093+:: structure before this arm was called. Decline in that case rather than
9094+:: deriving provenance from the already-walked type.
9095+++ contextual-simple-sub
9096+ |= sub=isub
9097+ ^- ?
9098+ ?~ sub &
9099+ ?: ?=(?(%cell %face %fn %union %collection) -.val.i.sub) |
9100+ $(sub t.sub)
9101+::
9102+:: Check the syntactic root before scanning; scan substitutions once.
9103+++ grec-direct-context
9104+ |= [expected=itype sub=isub]
9105+ ^- ?
9106+ =/ left=@ud 4.096
9107+ |-
9108+ ?: ?=(%face -.expected)
9109+ ?: =(0 left) |
9110+ $(expected body.expected, left (dec left))
9111+ ?. ?=(%grec -.expected) |
9112+ ?~ sub &
9113+ ?: =(0 left) |
9114+ ?: ?=(?(%cell %face %fn %union %collection %grec) -.val.i.sub) |
9115+ $(sub t.sub, left (dec left))
9116+++ contextual-direct-union
9117+ |= target=itype
9118+ ^- ?
9119+ ?: ?=(%face -.target) $(target body.target)
9120+ ?=(%union -.target)
9121+++ contextual-tagged-case
9122+ |= [target=itype tag=@ sub=isub]
9123+ ^- (unit itype)
9124+ ?. ?=(%union -.target) ~
9125+ =/ remaining=(list itype) cases.target
9126+ =/ found=(unit itype) ~
9127+ =/ seen=(set @) *(set @)
9128+ |-
9129+ ?~ remaining found
9130+ =/ c=itype i.remaining
9131+ ?. ?=(%cell -.c) ~
9132+ =/ head=itype hed.c
9133+ ?. ?=(%const -.head) ~
9134+ ?: (~(has in:..zuse seen) val.literal.head) ~
9135+ =. seen (~(put in:..zuse seen) val.literal.head)
9136+ ?: =(tag val.literal.head)
9137+ $(remaining t.remaining, found `c)
9138+ $(remaining t.remaining)
9139+::
9140+:: A bounded syntactic screen: no nested branch, cast, gate or local body
9141+:: can re-enter cell-branch retry during either inference attempt.
9142+++ closed-cell-retry-safe
9143+ |= [todo=(list expr) fuel=@ud]
9144+ ^- ?
9145+ ?~ todo &
9146+ ?: =(0 fuel) |
9147+ =/ e=expr i.todo
9148+ =. fuel (dec fuel)
9149+ ?+ -.e |
9150+ %lit $(todo t.todo)
9151+ %wing $(todo t.todo)
9152+ %ctor $(todo t.todo)
9153+ %path $(todo t.todo)
9154+ %crash $(todo t.todo)
9155+ %str
9156+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) |
9157+ $(todo t.todo)
9158+ %group $(todo [inner.e t.todo])
9159+ %pair $(todo [val.e t.todo])
9160+ %unit $(todo [val.e t.todo])
9161+ %list $(todo (weld items.e t.todo))
9162+ %tuple $(todo (weld (turn items.e |=(i=item val.i)) t.todo))
9163+ %change $(todo (weld (turn edits.e |=(ed=edit val.ed)) t.todo))
9164+ %call $(todo [head.e (weld args.e t.todo)])
9165+ %trace $(todo [val.e then.e t.todo])
9166+ ==
9167+::
9168+++ closed-cell-sub-safe
9169+ |= [sub=isub fuel=@ud]
9170+ ^- ?
9171+ ?~ sub &
9172+ ?: =(0 fuel) |
9173+ ?: ?=(?(%cell %face %fn %union %collection %grec %jrec %recursive) -.val.i.sub) |
9174+ $(sub t.sub, fuel (dec fuel))
9175+::
9176+++ closed-cell-branch-eligible
9177+ |= [e=expr expected=itype sub=isub]
9178+ ^- ?
9179+ ?. &(?=(%branch -.e) ?=(%cell -.expected) (closed-cell-sub-safe sub 512)) |
9180+ ?~ arms.e |
9181+ ?~ t.arms.e |
9182+ ?^ t.t.arms.e |
9183+ =/ x=arm i.arms.e
9184+ =/ y=arm i.t.arms.e
9185+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) |
9186+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) |
9187+ ?: =(val.lit.pat.x val.lit.pat.y) |
9188+ (closed-cell-retry-safe ~[subject.e val.x val.y] 512)
9189+::
9190+:: Attempt ordinary inference first; retry from the same state only for
9191+:: the bounded non-reentrant syntax above. Preserve original value faces.
9192+++ infer-closed-cell-branch
9193+ |= [e=expr expected=itype env=ienv state=istate context=span]
9194+ ^- iresult
9195+ ?> (closed-cell-branch-eligible e expected sub.state)
9196+ ?> ?=(%branch -.e)
9197+ ?> ?=(^ arms.e)
9198+ ?> ?=(^ t.arms.e)
9199+ =/ ordinary=iresult (infer-fragment e env state)
9200+ =/ ordinary-good=?
9201+ ?: ?=(%| -.ordinary) |
9202+ =/ fit=ifit (itype-fit typ.p.ordinary expected sub.state.p.ordinary next.state.p.ordinary)
9203+ ?=(%ok -.fit)
9204+ ?: ordinary-good ordinary
9205+ =/ attempt=(unit iresult)
9206+ =/ x=arm i.arms.e
9207+ =/ y=arm i.t.arms.e
9208+ =/ subject=iresult (infer-fragment subject.e env state)
9209+ ?: ?=(%| -.subject) ~
9210+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
9211+ ?: ?=(%union -.subject-type) ~
9212+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
9213+ ?~ su ~
9214+ =/ left=iresult (infer-call-context-arg val.x expected env state.p.subject(sub u.su) context)
9215+ ?: ?=(%| -.left) ~
9216+ =/ lf=ifit (itype-fit typ.p.left expected sub.state.p.left next.state.p.left)
9217+ ?. ?=(%ok -.lf) ~
9218+ =/ right=iresult (infer-call-context-arg val.y expected env state.p.left(sub sub.lf, next next.lf) context)
9219+ ?: ?=(%| -.right) ~
9220+ =/ rf=ifit (itype-fit typ.p.right expected sub.state.p.right next.state.p.right)
9221+ ?. ?=(%ok -.rf) ~
9222+ =/ sub=isub sub.rf
9223+ =/ next=@ud next.rf
9224+ =/ lt=itype (itype-normalize typ.p.left sub)
9225+ =/ rt=itype (itype-normalize typ.p.right sub)
9226+ =/ et=itype (itype-normalize expected sub)
9227+ ?. =(lt rt) ~
9228+ ?: |(?=(^ (itype-vars lt)) ?=(^ (itype-vars rt)) ?=(^ (itype-vars et))) ~
9229+ ?: |((itype-has-tag lt) (itype-has-tag rt) (itype-has-tag et)) ~
9230+ =/ lcheck=ifit (itype-fit typ.p.left expected sub next)
9231+ ?. ?=(%ok -.lcheck) ~
9232+ ?. &(=(sub.lcheck sub) =(next.lcheck next)) ~
9233+ =/ rcheck=ifit (itype-fit typ.p.right expected sub next)
9234+ ?. ?=(%ok -.rcheck) ~
9235+ ?. &(=(sub.rcheck sub) =(next.rcheck next)) ~
9236+ `[%& typ.p.left state.p.right(sub sub, next next)]
9237+ ?~ attempt ordinary
9238+ u.attempt
9239+::
9240+++ infer-call-context-arg
9241+ |= [e=expr expected=itype env=ienv state=istate context=span]
9242+ ^- iresult
9243+ ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9244+ ?: ?=(%pair -.e) $(e (pair-as-cell e))
9245+ ?: ?=(%group -.e) $(e inner.e)
9246+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9247+ ?: ?=(%trace -.e)
9248+ =/ traced=iresult (infer-fragment val.e env state)
9249+ ?: ?=(%| -.traced) traced
9250+ $(e then.e, state state.p.traced)
9251+ =/ target=itype (itype-walk expected sub.state)
9252+ |-
9253+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
9254+ ?: (explicit-proj-call e env state)
9255+ (infer-proj-context e expected env state context)
9256+ :: Experimental construction only for a source-proven direct target.
9257+ :: Decline any walked structural binding to retain raw-variable provenance.
9258+ ?: &(?=(%grec -.target) ?=(%tuple -.e) (grec-direct-context expected sub.state))
9259+ =/ unfolded=(unit [view=itype left=@ud]) (grec-unfold-view target jrec-fuel.state)
9260+ ?~ unfolded [%| ["recursive mold unfolding needs unsupported inference" ~]]
9261+ ?~ items.e [%| ["recursive mold constructor needs unsupported inference" ~]]
9262+ =/ first=item i.items.e
9263+ ?. &(?=(~ face.first) ?=(%lit -.val.first) =(%term form.lit.val.first))
9264+ [%| ["recursive mold constructor needs unsupported inference" ~]]
9265+ =/ chosen=(unit itype) (contextual-tagged-case view.u.unfolded val.lit.val.first sub.state)
9266+ ?~ chosen [%| ["recursive mold constructor has no matching case" ~]]
9267+ =/ value=iresult (infer-call-context-items items.e u.chosen env state(jrec-fuel left.u.unfolded) context)
9268+ ?: ?=(%| -.value) value
9269+ =/ fit=ifit (itype-fit typ.p.value u.chosen sub.state.p.value next.state.p.value)
9270+ ?: ?=(%unknown -.fit) [%| ["recursive mold case needs unsupported inference" ~]]
9271+ ?: ?=(%bad -.fit) [%| ["recursive mold case does not fit its source shape" ~]]
9272+ [%& target state.p.value(sub sub.fit, next next.fit)]
9273+ :: Only the source-proven one-layer cell is exposed. Each recursive
9274+ :: descent consumes one written tuple; named values use ordinary fit.
9275+ ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
9276+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
9277+ [%& target state(jrec-fuel (dec jrec-fuel.state))]
9278+ ?: &(?=(%jrec -.target) ?=(%tuple -.e))
9279+ ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
9280+ =. state state(jrec-fuel (dec jrec-fuel.state))
9281+ =/ shape=itype
9282+ [%cell [%face head.target [%atom aura.target]] [%face tail.target target]]
9283+ =/ value=iresult (infer-call-context-items items.e shape env state context)
9284+ ?: ?=(%| -.value) value
9285+ =/ fit=ifit (itype-fit typ.p.value shape sub.state.p.value next.state.p.value)
9286+ ?: ?=(%unknown -.fit) [%| ["recursive mold cell constraint needs unsupported inference" ~]]
9287+ ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
9288+ [%& target state.p.value(sub sub.fit, next next.fit)]
9289+ ?: ?=(%call -.e) (infer-contextual-call e target env state)
9290+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[target context])
9291+ ?^ empty-list u.empty-list
9292+ ?: (single-structured-pattern e)
9293+ ?> ?=(%branch -.e)
9294+ =/ empty-union=(unit iresult) (known-empty-union-wing subject.e env state)
9295+ ?^ empty-union (infer-known-union-context-subject e target env u.empty-union context)
9296+ =/ single=(unit iresult) (grec-single-wing-subject subject.e env state)
9297+ ?^ single (infer-known-union-context-subject e target env u.single context)
9298+ (infer-single-case-branch e env state `[target context])
9299+ ?: (cell-binder-pattern e)
9300+ (infer-cell-branch e env state `[target context])
9301+ :: In an explicit singleton context retain the written loobean noun;
9302+ :: the ordinary singleton fit compares its noun, not its spelling.
9303+ =/ singleton=(unit itype)
9304+ ?. ?=(%lit -.e) ~
9305+ ?. =(%loobean form.lit.e) ~
9306+ ?. |(?=(%const -.target) &(?=(%union -.expected) (explicit-singleton-in-union expected val.lit.e))) ~
9307+ `[%const lit.e]
9308+ ?^ singleton [%& u.singleton state]
9309+ =/ known=(unit iresult)
9310+ ?: ?=(%branch -.e) (known-union-subject subject.e env state)
9311+ ~
9312+ ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
9313+ ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
9314+ (infer-known-union-context-subject e target env u.known context)
79749315 ?: &(?=(%union -.target) ?=(%unit -.e))
79759316 (infer-unit-context e target env state context)
9317+ ?: (closed-cell-branch-eligible e expected sub.state)
9318+ (infer-closed-cell-branch e expected env state context)
79769319 ?: &(?=(%flag -.target) (context-union-branch e))
79779320 (infer-union-context e target env state context)
79789321 ?: &(?=(%union -.target) (context-union-branch e))
@@ -7981,17 +9324,53 @@
79819324 (infer-union-context e target env state context)
79829325 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
79839326 (infer-list-context e target env state context)
9327+ :: A literal-headed tuple can receive the unique case's payload
9328+ :: context. The ordinary final fit still checks the complete union.
9329+ =/ selected=(unit itype)
9330+ ?. &((contextual-simple-sub sub.state) (contextual-direct-union expected) ?=(%union -.target) ?=(%tuple -.e) ?=(^ items.e)) ~
9331+ ?~ t.items.e ~
9332+ ?^ t.t.items.e ~
9333+ ?. (contextual-direct-payload-call val.i.t.items.e) ~
9334+ =/ first=item i.items.e
9335+ ?. &(?=(~ face.first) ?=(%lit -.val.first) |(=(%term form.lit.val.first) =(%null form.lit.val.first) =(%loobean form.lit.val.first))) ~
9336+ (contextual-tagged-case target val.lit.val.first sub.state)
9337+ ?^ selected
9338+ ?> ?=(%tuple -.e)
9339+ :: On this bounded shallow-call shape, preserve any inference that
9340+ :: already fits before trying the new contextual path. Neither pass
9341+ :: can recursively select a nested tuple from the atomic arguments.
9342+ =/ ordinary=(unit iresult)
9343+ =/ initial=iresult (infer-fragment e env state)
9344+ ?: ?=(%| -.initial) ~
9345+ =/ fit=ifit (itype-fit typ.p.initial target sub.state.p.initial next.state.p.initial)
9346+ ?. ?=(%ok -.fit) ~
9347+ `initial
9348+ ?^ ordinary u.ordinary
9349+ =/ value=iresult (infer-call-context-items items.e u.selected env state context)
9350+ ?: ?=(%| -.value) value
9351+ =/ fit=ifit (itype-fit typ.p.value u.selected sub.state.p.value next.state.p.value)
9352+ ?: ?=(%unknown -.fit) [%| ["tagged case needs unsupported inference" ~]]
9353+ ?: ?=(%bad -.fit) [%| ["tagged case does not fit its expected type" ~[[context "expected union case"] [(span-of e) "value"]]]]
9354+ [%& typ.p.value state.p.value(sub sub.fit, next next.fit)]
79849355 ?: &(?=(%cell -.target) ?=(%tuple -.e))
79859356 (infer-call-context-items items.e target env state context)
79869357 (infer-fragment e env state)
79879358::
79889359:: Preserve each written face; the final complete sample fit checks faces.
9360+:: A tuple or positional field face belongs to the enclosing sample,
9361+:: not to the expression at that position. A second face, if present,
9362+:: is part of the value's own expected type.
9363+++ projection-field-target
9364+ |= expected=itype
9365+ ^- itype
9366+ ?:(?=(%face -.expected) body.expected expected)
9367+::
79899368++ infer-call-context-items
79909369 |= [items=(list item) expected=itype env=ienv state=istate context=span]
79919370 ^- iresult
79929371 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
79939372 ?~ t.items
7994− =/ last=iresult (infer-call-context-arg val.i.items expected env state context)
9373+ =/ last=iresult (infer-call-context-arg val.i.items (projection-field-target expected) env state context)
79959374 ?: ?=(%| -.last) last
79969375 =/ typ=itype typ.p.last
79979376 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
@@ -8000,7 +9379,7 @@
80009379 |-
80019380 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
80029381 ?. ?=(%cell -.target) (infer-simple-items items env state)
8003− =/ head=iresult (infer-call-context-arg val.i.items hed.target env state context)
9382+ =/ head=iresult (infer-call-context-arg val.i.items (projection-field-target hed.target) env state context)
80049383 ?: ?=(%| -.head) head
80059384 =/ typ=itype typ.p.head
80069385 =. typ ?~(face.i.items typ [%face u.face.i.items typ])
@@ -8012,13 +9391,13 @@
80129391 |= [args=(list expr) expected=itype env=ienv state=istate context=span]
80139392 ^- iresult
80149393 ?~ args [%| ["call has no argument" ~]]
8015− ?~ t.args (infer-call-context-arg i.args expected env state context)
9394+ ?~ t.args (infer-call-context-arg i.args (projection-field-target expected) env state context)
80169395 =/ target=itype (itype-walk expected sub.state)
80179396 |-
80189397 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
80199398 ?. ?=(%cell -.target)
80209399 (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
8021− =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
9400+ =/ head=iresult (infer-call-context-arg i.args (projection-field-target hed.target) env state context)
80229401 ?: ?=(%| -.head) head
80239402 =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
80249403 ?: ?=(%| -.tail) tail
@@ -8050,7 +9429,7 @@
80509429 ?~ pats [%& ~]
80519430 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
80529431 =/ name=term name.i.pats
8053− ?: |(?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
9432+ ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
80549433 [%| 'pattern shadows a name']
80559434 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
80569435 ?: ?=(%| -.rest) rest
@@ -8075,7 +9454,7 @@
80759454 ?~ t.names |
80769455 =. typ (itype-walk typ sub)
80779456 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8078− |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
9457+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%grec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
80799458::
80809459++ cell-binder-pattern
80819460 |= e=expr
@@ -8133,13 +9512,20 @@
81339512 %avar
81349513 ?: (lth id.t 26) [(add 65 id.t) ~]
81359514 "T{<id.t>}"
9515+ %rvar
9516+ ?: (lth id.t 26) [(add 65 id.t) ~]
9517+ "T{<id.t>}"
81369518 %nvar
81379519 ?: (lth id.t 26) [(add 65 id.t) ~]
81389520 "T{<id.t>}"
9521+ %rnvar
9522+ ?: (lth id.t 26) [(add 65 id.t) ~]
9523+ "T{<id.t>}"
81399524 %atom "@{(trip aura.t)}"
81409525 %any-atom "@"
81419526 %flag "?"
81429527 %noun "*"
9528+ %empty "!!"
81439529 %tag (trip txt.literal.t)
81449530 %const (trip txt.literal.t)
81459531 %union
@@ -8148,6 +9534,7 @@
81489534 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
81499535 %recursive ?~(label.t "recursive mold" (trip u.label.t))
81509536 %jrec ?~(label.t "recursive mold" (trip u.label.t))
9537+ %grec ?~(label.t "recursive mold" "({(trip u.label.t)} {(show-itype-cases args.t sub)})")
81519538 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
81529539 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
81539540 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -8183,17 +9570,21 @@
81839570 ^- ?
81849571 ?- -.typ
81859572 %nvar &
9573+ %rnvar &
81869574 %var |
81879575 %avar |
9576+ %rvar |
81889577 %atom |
81899578 %any-atom |
81909579 %flag |
81919580 %noun |
9581+ %empty |
81929582 %tag |
81939583 %const |
81949584 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
81959585 %recursive |
81969586 %jrec |
9587+ %grec (lien args.typ |=(c=itype (itype-has-nvar c)))
81979588 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
81989589 %face $(typ body.typ)
81999590 %fn |($(typ sample.typ) $(typ product.typ))
@@ -8204,7 +9595,7 @@
82049595 |= [label=tape typ=itype sub=isub]
82059596 ^- tape
82069597 =/ normalized=itype (itype-normalize typ sub)
8207− ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
9598+ ?: |(?=(%var -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
82089599 ?: (itype-has-hidden-recursive normalized) label
82099600 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
82109601 ?: (gth (lent vars) 26) label
@@ -8226,6 +9617,7 @@
82269617 ?+ -.resolved ~
82279618 %var `id.resolved
82289619 %avar `id.resolved
9620+ %rvar `id.resolved
82299621 ==
82309622 ?~ ident $(caps t.caps)
82319623 ?: =(n u.ident) &
@@ -8240,6 +9632,7 @@
82409632 ?+ -.resolved ~
82419633 %var `id.resolved
82429634 %avar `id.resolved
9635+ %rvar `id.resolved
82439636 ==
82449637 ?~ ident $(caps t.caps)
82459638 ?: =(n u.ident) `i.caps
@@ -8254,6 +9647,7 @@
82549647 ?+ -.resolved ~
82559648 %var `id.resolved
82569649 %avar `id.resolved
9650+ %rvar `id.resolved
82579651 ==
82589652 ?~ ident $(caps t.caps)
82599653 =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
@@ -8269,6 +9663,7 @@
82699663 ?+ -.resolved ~
82709664 %var `id.resolved
82719665 %avar `id.resolved
9666+ %rvar `id.resolved
82729667 ==
82739668 ?~ ident &
82749669 ?: (cap-id-in u.ident t.caps sub) &
@@ -8283,8 +9678,8 @@
82839678 ^- ?
82849679 ?~ caps |
82859680 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
8286− ?: ?=(%avar -.resolved)
8287− ?: =(n id.resolved) &
9681+ ?: |(?=(%avar -.resolved) ?=(%rvar -.resolved))
9682+ ?: =(n +.resolved) &
82889683 $(caps t.caps)
82899684 $(caps t.caps)
82909685::
@@ -8294,16 +9689,20 @@
82949689 ?- -.t
82959690 %var |
82969691 %avar =(n id.t)
9692+ %rvar =(n id.t)
82979693 %nvar |
9694+ %rnvar |
82989695 %atom |
82999696 %any-atom |
83009697 %flag |
83019698 %noun |
9699+ %empty |
83029700 %tag |
83039701 %const |
83049702 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
83059703 %recursive |
83069704 %jrec |
9705+ %grec (lien args.t |=(c=itype (has-atom-var n c)))
83079706 %collection (lien args.t |=(c=itype (has-atom-var n c)))
83089707 %face $(t body.t)
83099708 %fn |($(t sample.t) $(t product.t))
@@ -8343,6 +9742,10 @@
83439742 =/ out=tape ""
83449743 |-
83459744 ?~ vars out
9745+ ?: (itype-var-is-restricted i.vars t)
9746+ =/ sep=tape ?:(printed ", " " where ")
9747+ =/ clause=tape "{sep}{(show-itype [%rvar i.vars] ~)} is an atom other than ?"
9748+ $(vars t.vars, printed &, out (weld out clause))
83469749 ?: (itype-var-is-atom i.vars t)
83479750 =/ sep=tape ?:(printed ", " " where ")
83489751 =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
@@ -8443,6 +9846,8 @@
84439846++ infer-recursive-gate
84449847 |= [d=def env=ienv state=istate]
84459848 ^- iresult
9849+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
9850+ =. gate-defs.state ~
84469851 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
84479852 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
84489853 [%| ["recursive definition is not a gate" ~]]
@@ -8652,6 +10057,7 @@
865210057 ?: (constrained-capitals caps.entry sub.state)
865310058 [%| ["explicit capital constraints are not supported by partial inference" ~]]
865410059 =/ typ=itype (itype-normalize typ.entry sub.state)
10060+ ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
865510061 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
865610062 [%| ["recursive group needs unsupported inference" ~]]
865710063 =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
@@ -8665,18 +10071,21 @@
866510071++ infer-gate-group
866610072 |= [ds=(list def) env=ienv state=istate]
866710073 ^- ilocal-result
10074+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
866810075 =/ names=(list term) (global-value-names ds)
866910076 ?. (levy names |=(n=term (unique-value-name n names)))
867010077 [%| ["recursive group contains duplicate names" ~]]
867110078 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
867210079 [%| ["recursive group shadows a name" ~]]
8673− =/ scoped=istate state(globals (weld names globals.state))
10080+ =/ scoped=istate state(globals (weld names globals.state), gate-defs ~)
867410081 =/ seeded=igate-seeds (seed-gate-group ds env scoped)
867510082 ?: ?=(%| -.seeded) seeded
867610083 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
867710084 =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
867810085 ?: ?=(%| -.body) body
867910086 :: Per-member ownership through mutual recursion is not implemented.
10087+ ?: !=(projections.state.p.body projections.state)
10088+ [%| ["record projection in recursive groups needs unsupported inference" ~]]
868010089 ?: !=(holes.state.p.body holes.state)
868110090 [%| ["holes in recursive groups need unsupported inference" ~]]
868210091 ?: (pending-tags tags.state.p.body sub.state.p.body)
@@ -8685,31 +10094,29 @@
868510094 ?: ?=(%| -.schemes) schemes
868610095 [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
868710096::
10097+++ width-finalize
10098+ |= [ps=(list iwprojection) sub=isub visible=(list @ud)]
10099+ ^- (unit (list iwprojection))
10100+ ?~ ps `~
10101+ ?: (lien t.ps |=(p=iwprojection =(at.p at.i.ps))) ~
10102+ =/ src=itype (default-decimals (itype-normalize source.i.ps sub))
10103+ =/ dst=itype (default-decimals (itype-normalize target.i.ps sub))
10104+ ?: |((itype-has-nvar src) (itype-has-nvar dst) (itype-has-tag src) (itype-has-tag dst)) ~
10105+ =/ vars=(list @ud) (weld (itype-vars src) (itype-vars dst))
10106+ ?. (levy vars |=(n=@ud (lien visible |=(v=@ud =(n v))))) ~
10107+ =/ rest=(unit (list iwprojection)) $(ps t.ps)
10108+ ?~ rest ~
10109+ =/ entry=iwprojection i.ps
10110+ =. entry entry(source src, target dst)
10111+ `[entry u.rest]
10112+::
868810113++ add-supported-defs
8689− |= [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)]
8690− ^- ienv
8691− ?~ ds env
8692− =/ d=def i.ds
8693− ?: ?=(%mold -.d) $(ds t.ds)
8694− ?. (unique-value-name name.d globals) $(ds t.ds)
8695− ?^ (ienv-lookup name.d env) $(ds t.ds)
8696− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8697− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256]
8698− =. initial (reserve-def-caps val.d initial)
8699− =/ result=iresult (infer-fragment val.d env initial)
8700− =? result ?=(%| -.result) (infer-recursive-gate d env initial)
8701− ?: ?=(%| -.result) $(ds t.ds)
8702− =. 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)))
8703− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
8704− ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
8705− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
8706− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
8707− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
8708− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8709− ?: (gth (lent vars) 26) $(ds t.ds)
8710− $(ds t.ds, env [[name.d [typ vars]] env])
10114+ |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) 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)]
10115+ ^- [env=ienv artifacts=(list iwidth-definition)]
10116+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)
871110117::
8712−+$ iresolved [env=ienv grouped=(list term)]
10118+
10119++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
871310120+$ iadj (map term (list term))
871410121+$ ivisited (map term ?)
871510122+$ iwork (list [name=term done=?])
@@ -8803,9 +10210,9 @@
880310210 (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
880410211::
880510212++ add-groups
8806− |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) state=istate]
10213+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
880710214 ^- iresolved
8808− ?~ components [env grouped]
10215+ ?~ components [env grouped artifacts]
880910216 =/ component=(list term) i.components
881010217 ?. (graph-cycle component graph) $(components t.components)
881110218 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -8822,19 +10229,63 @@
882210229++ resolve-groups
882310230 |= [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)]
882410231 ^- iresolved
10232+ (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
10233+::
10234+
10235+++ add-supported-defs-core
10236+ |= [ds=(list def) all-defs=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) 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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10237+ ^- [env=ienv artifacts=(list iwidth-definition)]
10238+ ?~ ds [env artifacts]
10239+ =/ d=def i.ds
10240+ ?: ?=(%mold -.d) $(ds t.ds)
10241+ ?. (unique-value-name name.d globals) $(ds t.ds)
10242+ ?^ (ienv-lookup name.d env) $(ds t.ds)
10243+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10244+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10245+ =. grec-index.initial index
10246+ =. gate-defs.initial checked
10247+ =. head-evidence.initial heads
10248+ =. initial (reserve-def-caps val.d initial)
10249+ =/ result=iresult (infer-fragment val.d env initial)
10250+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10251+ ?: ?=(%| -.result) $(ds t.ds)
10252+ =. state.p.result (promote-restricted-numbers state.p.result env)
10253+ =. 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)))
10254+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
10255+ ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
10256+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10257+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
10258+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
10259+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10260+ ?: (gth (lent vars) 26) $(ds t.ds)
10261+ =/ finalized=(unit (list iwprojection))
10262+ (width-finalize projections.state.p.result sub.state.p.result vars)
10263+ ?~ finalized $(ds t.ds)
10264+ =? artifacts ?=(^ u.finalized)
10265+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10266+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10267+ $(ds t.ds, env [[name.d [typ vars]] env], checked checked)
10268+::
10269+++ resolve-groups-core
10270+ |= [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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10271+ ^- iresolved
882510272 =/ env=ienv ~
882610273 =/ grouped=(list term) ~
10274+ =/ artifacts=(list iwidth-definition) ~
882710275 =/ names=(list term) (global-value-names ds)
882810276 =/ nameset=ivisited (graph-nameset names ~)
882910277 =/ graph=iadj (graph-make-forward ds nameset ~)
883010278 =/ components=icomponents (graph-components ds names)
883110279 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10280+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
883210281 |-
8833− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
8834− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256]
8835− =/ out=iresolved (add-groups ds components graph next grouped initial)
10282+ =/ next=[env=ienv artifacts=(list iwidth-definition)]
10283+ (add-supported-defs-core ds ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
10284+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10285+ =. grec-index.initial index
10286+ =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
883610287 ?: =(env env.out) out
8837− $(env env.out, grouped grouped.out)
10288+ $(env env.out, grouped grouped.out, artifacts artifacts.out)
883810289::
883910290++ resolve-supported-defs
884010291 |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]
@@ -9080,6 +10531,257 @@
908010531 %overlap
908110532 %unknown
908210533::
10534+:: A source-only fallback for literal-tagged cells and one-hop local
10535+:: generic applications. It screens all work before ordinary inference.
10536+++ union-simple-shape-budget
10537+ |= [s=shape fuel=@ud vars=(unit (list @t))]
10538+ ^- (unit @ud)
10539+ ?: =(0 fuel) ~
10540+ =. fuel (dec fuel)
10541+ ?- -.s
10542+ ?(%aura %noun %void %flag) `fuel
10543+ %tvar
10544+ ?~ vars `fuel
10545+ ?:((lien u.vars |=(n=@t =(n name.s))) `fuel ~)
10546+ %const
10547+ ?. |(=(%term form.lit.s) =(%null form.lit.s) =(%loobean form.lit.s)) ~
10548+ ?: &(=(%loobean form.lit.s) !|(=(0 val.lit.s) =(1 val.lit.s))) ~
10549+ `fuel
10550+ %cell (union-simple-fields-budget fields.s fuel vars)
10551+ %fn
10552+ =/ left=(unit @ud) $(s sample.s, fuel fuel)
10553+ ?~ left ~
10554+ $(s product.s, fuel u.left)
10555+ * ~
10556+ ==
10557+++ union-simple-fields-budget
10558+ |= [fields=(list field) fuel=@ud vars=(unit (list @t))]
10559+ ^- (unit @ud)
10560+ ?~ fields `fuel
10561+ ?: =(0 fuel) ~
10562+ =/ field-shape=shape
10563+ ?- -.i.fields
10564+ %bare shape.i.fields
10565+ %face shape.i.fields
10566+ %pun [%ref at.i.fields ~[name.i.fields]]
10567+ ==
10568+ =/ head=(unit @ud) (union-simple-shape-budget field-shape (dec fuel) vars)
10569+ ?~ head ~
10570+ $(fields t.fields, fuel u.head)
10571+++ union-source-find
10572+ |= [n=term molds=imolds fuel=@ud]
10573+ ^- (unit [body=shape left=@ud])
10574+ =/ found=(unit shape) ~
10575+ |-
10576+ ?~ molds
10577+ ?~ found ~
10578+ `[u.found fuel]
10579+ ?: =(0 fuel) ~
10580+ ?: =(n name.i.molds)
10581+ ?^ found ~
10582+ $(molds t.molds, fuel (dec fuel), found `body.i.molds)
10583+ $(molds t.molds, fuel (dec fuel))
10584+++ union-source-args-budget
10585+ |= [vars=(list @t) args=(list shape) fuel=@ud]
10586+ ^- (unit @ud)
10587+ =/ seen=(set @t) *(set @t)
10588+ |-
10589+ ?~ vars ?~(args `fuel ~)
10590+ ?~ args ~
10591+ ?: =(0 fuel) ~
10592+ ?: (~(has in:..zuse seen) i.vars) ~
10593+ =/ arg=(unit @ud) (union-simple-shape-budget i.args (dec fuel) ~)
10594+ ?~ arg ~
10595+ $(vars t.vars, args t.args, fuel u.arg, seen (~(put in:..zuse seen) i.vars))
10596+++ union-source-cell-tag
10597+ |= s=shape
10598+ ^- (unit @)
10599+ ?. ?=(%cell -.s) ~
10600+ ?~ fields.s ~
10601+ ?~ t.fields.s ~
10602+ ?. ?=(%bare -.i.fields.s) ~
10603+ =/ head=shape shape.i.fields.s
10604+ ?. ?=(%const -.head) ~
10605+ ?. |(=(%term form.lit.head) =(%null form.lit.head) =(%loobean form.lit.head)) ~
10606+ ?: &(=(%loobean form.lit.head) !|(=(0 val.lit.head) =(1 val.lit.head))) ~
10607+ `val.lit.head
10608+++ union-source-case-tag
10609+ |= [s=shape molds=imolds fuel=@ud]
10610+ ^- (unit [tag=@ left=@ud])
10611+ ?: ?=(%cell -.s)
10612+ =/ tag=(unit @) (union-source-cell-tag s)
10613+ ?~ tag ~
10614+ =/ left=(unit @ud) (union-simple-shape-budget s fuel ~)
10615+ ?~ left ~
10616+ `[u.tag u.left]
10617+ ?. ?=(%apply -.s) ~
10618+ ?. ?=([@ ~] ref.s) ~
10619+ ?: =(0 fuel) ~
10620+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
10621+ ?~ found ~
10622+ ?. ?=(%generic -.body.u.found) ~
10623+ ?~ vars.body.u.found ~
10624+ =/ tag=(unit @) (union-source-cell-tag body.body.u.found)
10625+ ?~ tag ~
10626+ =/ args=(unit @ud) (union-source-args-budget vars.body.u.found args.s left.u.found)
10627+ ?~ args ~
10628+ =/ left=(unit @ud) (union-simple-shape-budget body.body.u.found u.args `vars.body.u.found)
10629+ ?~ left ~
10630+ `[u.tag u.left]
10631+++ union-source-distinct-tags
10632+ |= [cases=(list shape) molds=imolds fuel=@ud]
10633+ ^- ?
10634+ =/ seen=(set @) *(set @)
10635+ =/ has-application=? |
10636+ |-
10637+ ?~ cases has-application
10638+ ?: =(0 fuel) |
10639+ =/ item=(unit [tag=@ left=@ud]) (union-source-case-tag i.cases molds (dec fuel))
10640+ ?~ item |
10641+ ?: (~(has in:..zuse seen) tag.u.item) |
10642+ $(cases t.cases, fuel left.u.item, seen (~(put in:..zuse seen) tag.u.item), has-application |(has-application ?=(%apply -.i.cases)))
10643+::
10644+:: This inference-only screen bounds inherited work that the small source
10645+:: slice may consult. It does not authenticate a caller-created state.
10646+++ union-state-leaf
10647+ |= t=itype
10648+ ^- ?
10649+ ?=(?(%var %avar %rvar %nvar %rnvar %atom %any-atom %flag %noun %empty %const) -.t)
10650+++ union-state-params-budget
10651+ |= [params=iparams fuel=@ud]
10652+ ^- (unit @ud)
10653+ ?~ params `fuel
10654+ ?: =(0 fuel) ~
10655+ ?. (union-state-leaf typ.i.params) ~
10656+ $(params t.params, fuel (dec fuel))
10657+++ union-state-sub-budget
10658+ |= [sub=isub fuel=@ud]
10659+ ^- (unit @ud)
10660+ ?~ sub `fuel
10661+ ?: =(0 fuel) ~
10662+ ?. (union-state-leaf val.i.sub) ~
10663+ $(sub t.sub, fuel (dec fuel))
10664+++ union-state-caps-budget
10665+ |= [caps=icaps fuel=@ud]
10666+ ^- (unit @ud)
10667+ ?~ caps `fuel
10668+ ?: =(0 fuel) ~
10669+ $(caps t.caps, fuel (dec fuel))
10670+++ union-state-active-budget
10671+ |= [active=(list term) fuel=@ud]
10672+ ^- (unit @ud)
10673+ ?~ active `fuel
10674+ ?: =(0 fuel) ~
10675+ $(active t.active, fuel (dec fuel))
10676+++ union-state-tags-budget
10677+ |= [tags=(list ipending) fuel=@ud]
10678+ ^- (unit @ud)
10679+ ?~ tags `fuel
10680+ ?: =(0 fuel) ~
10681+ $(tags t.tags, fuel (dec fuel))
10682+++ union-source-state-safe
10683+ |= [state=istate fuel=@ud]
10684+ ^- ?
10685+ ?^ grec-index.state |
10686+ ?^ holes.state |
10687+ ?^ defer.state |
10688+ ?^ obligations.state |
10689+ =/ params=(unit @ud) (union-state-params-budget params.state fuel)
10690+ ?~ params |
10691+ =/ sub=(unit @ud) (union-state-sub-budget sub.state u.params)
10692+ ?~ sub |
10693+ =/ caps=(unit @ud) (union-state-caps-budget caps.state u.sub)
10694+ ?~ caps |
10695+ =/ active=(unit @ud) (union-state-active-budget active.state u.caps)
10696+ ?~ active |
10697+ ?=(^ (union-state-tags-budget tags.state u.active))
10698+::
10699+:: Positive overlap witnesses from parsed, one-hop local source only.
10700+:: Unknown or exhausted work returns no witness, never disjointness.
10701++$ uow-case [at=span head=@ payload=upat]
10702+++ union-overlap-primitive
10703+ |= s=shape
10704+ ^- (unit upat)
10705+ ?- -.s
10706+ %aura `[%atom ~]
10707+ %noun `[%all ~]
10708+ %void `[%empty ~]
10709+ %flag `[%flag ~]
10710+ %const
10711+ ?. |(=(%term form.lit.s) =(%null form.lit.s) =(%loobean form.lit.s)) ~
10712+ ?: &(=(%loobean form.lit.s) !|(=(0 val.lit.s) =(1 val.lit.s))) ~
10713+ `[%atom `val.lit.s]
10714+ * ~
10715+ ==
10716+++ union-overlap-case
10717+ |= [s=shape molds=imolds fuel=@ud]
10718+ ^- (unit [item=uow-case left=@ud])
10719+ ?: =(0 fuel) ~
10720+ =. fuel (dec fuel)
10721+ :: Each body has exactly two fields; an application has exactly one
10722+ :: parameter and one concrete primitive argument. The full mold table
10723+ :: is scanned to establish unique ownership.
10724+ =/ expanded=(unit [body=shape param=(unit [name=@t pat=upat]) left=@ud])
10725+ ?: ?=(%cell -.s) `[s ~ fuel]
10726+ ?. ?=(%apply -.s) ~
10727+ ?. ?=([@ ~] ref.s) ~
10728+ ?. ?=([* ~] args.s) ~
10729+ ?: =(0 fuel) ~
10730+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
10731+ ?~ found ~
10732+ ?. ?=(%generic -.body.u.found) ~
10733+ ?. ?=([@ ~] vars.body.u.found) ~
10734+ ?: =(0 left.u.found) ~
10735+ =/ argument=(unit upat) (union-overlap-primitive i.args.s)
10736+ ?~ argument ~
10737+ `[body.body.u.found `[i.vars.body.u.found u.argument] (dec left.u.found)]
10738+ ?~ expanded ~
10739+ =/ body=shape body.u.expanded
10740+ ?. ?=(%cell -.body) ~
10741+ ?. ?=([* * ~] fields.body) ~
10742+ :: Charge the cell, two fields, and the head and payload nodes.
10743+ ?: (lth left.u.expanded 5) ~
10744+ =/ head=(unit @) (union-source-cell-tag body)
10745+ ?~ head ~
10746+ =/ field=field i.t.fields.body
10747+ =/ payload=shape
10748+ ?- -.field
10749+ %bare shape.field
10750+ %face shape.field
10751+ %pun [%ref at.field ~[name.field]]
10752+ ==
10753+ =/ pattern=(unit upat)
10754+ ?: ?=(%tvar -.payload)
10755+ ?~ param.u.expanded ~
10756+ ?. =(name.payload name.u.param.u.expanded) ~
10757+ `pat.u.param.u.expanded
10758+ (union-overlap-primitive payload)
10759+ ?~ pattern ~
10760+ `[[at.s u.head u.pattern] (sub left.u.expanded 5)]
10761+++ union-overlap-against
10762+ |= [first=uow-case rest=(list shape) molds=imolds fuel=@ud]
10763+ ^- (unit [witness=(unit upair) left=@ud])
10764+ ?~ rest `[~ fuel]
10765+ ?: =(0 fuel) ~
10766+ =/ other=(unit [item=uow-case left=@ud]) (union-overlap-case i.rest molds (dec fuel))
10767+ ?~ other ~
10768+ ?: &(=(head.first head.item.u.other) =(%overlap (union-relate payload.first payload.item.u.other)))
10769+ `[`[at.first at.item.u.other %overlap] left.u.other]
10770+ $(rest t.rest, fuel left.u.other)
10771+++ union-source-overlap
10772+ |= [cases=(list shape) molds=imolds fuel=@ud]
10773+ ^- (unit upair)
10774+ ?~ cases ~
10775+ ?~ t.cases ~
10776+ ?: =(0 fuel) ~
10777+ =/ first=(unit [item=uow-case left=@ud]) (union-overlap-case i.cases molds (dec fuel))
10778+ ?~ first ~
10779+ =/ found=(unit [witness=(unit upair) left=@ud])
10780+ (union-overlap-against item.u.first t.cases molds left.u.first)
10781+ ?~ found ~
10782+ ?^ witness.u.found witness.u.found
10783+ $(cases t.cases, fuel left.u.found)
10784+::
908310785++ union-pairs
908410786 |= [cases=(list shape) molds=imolds]
908510787 ^- (list upair)
@@ -9233,6 +10935,11 @@
923310935 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
923410936 =/ pairs=(list upair) (union-pairs cases.sh molds)
923510937 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
10938+ =. overlapping
10939+ ?^ overlapping overlapping
10940+ ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
10941+ =/ witness=(unit upair) (union-source-overlap cases.sh molds 256)
10942+ ?~(witness ~ ~[u.witness])
923610943 ?^ overlapping
923710944 =/ p=upair i.overlapping
923810945 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
@@ -9240,7 +10947,9 @@
924010947 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
924110948 (of-wain:format ~[summary first second])
924210949 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
9243− (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10950+ ?. (union-source-distinct-tags cases.sh molds 256)
10951+ (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10952+ (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
924410953 (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
924510954::
924610955:: +show-inference-diagnostic: a partial report with both source sites
@@ -9297,7 +11006,14 @@
929711006+$ jbundle (list jsource)
929811007+$ jcache (list [at=path iface=ifile])
929911008+$ jfile-result (each [iface=ifile cache=jcache] @t)
11009+:: Overlap evidence retains the exact source that supplied its spans.
11010+:: Ordinary Jibb imports preserve this evidence through the resolver.
11011++$ jfile-overlap [file=path source=@t name=term cases=upair]
11012++$ jfile-failure [message=@t overlap=(unit jfile-overlap)]
11013++$ jfile-detailed-result (each [iface=ifile cache=jcache] jfile-failure)
930011014+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
11015+:: Preserve an imported overlap's original file and source across the graph.
11016++$ jimports-detailed-result (each [resolved=ijimports cache=jcache] jfile-failure)
930111017::
930211018:: Written record fields each have their own lexical record scope.
930311019+$ written-fields (map term span)
@@ -9485,6 +11201,60 @@
948511201 ==
948611202 [n $(imports t.imports)]
948711203::
11204+++ reserved-proj-sample
11205+ |= sam=sample
11206+ ^- ?
11207+ ?- -.sam
11208+ %bind =(name.sam %proj)
11209+ %face =(name.sam %proj)
11210+ %pun =(name.sam %proj)
11211+ %cell (lien items.sam reserved-proj-sample)
11212+ * |
11213+ ==
11214+++ reserved-proj-pattern
11215+ |= p=pattern
11216+ ^- ?
11217+ ?- -.p
11218+ %bind =(name.p %proj)
11219+ %cell (lien items.p reserved-proj-pattern)
11220+ * |
11221+ ==
11222+++ reserved-proj-def
11223+ |= d=def
11224+ ^- ?
11225+ ?: =(name.d %proj) &
11226+ ?: ?=(%value -.d) (reserved-proj-expr val.d)
11227+ |
11228+++ reserved-proj-expr
11229+ |= e=expr
11230+ ^- ?
11231+ ?- -.e
11232+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
11233+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
11234+ %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
11235+ %pair $(e val.e)
11236+ %unit $(e val.e)
11237+ %group $(e inner.e)
11238+ %list (lien items.e reserved-proj-expr)
11239+ %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
11240+ ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
11241+ %cast $(e val.e)
11242+ %call |($(e head.e) (lien args.e reserved-proj-expr))
11243+ %trace |($(e val.e) $(e then.e))
11244+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
11245+ %body |((lien defs.e reserved-proj-def) $(e final.e))
11246+ * |
11247+ ==
11248+::
11249+++ module-has-reserved-proj
11250+ |= mod=module
11251+ ^- ?
11252+ =/ imported=(list term) (import-binding-names imports.mod)
11253+ =/ vals=(list term) (global-value-names defs.mod)
11254+ =/ molds=imolds (collect-simple-molds defs.mod)
11255+ =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11256+ |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
11257+::
948811258++ module-scope-valid
948911259 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
949011260 ^- ?
@@ -9492,6 +11262,7 @@
949211262 =/ vals=(list term) (global-value-names defs.mod)
949311263 =/ molds=imolds (collect-simple-molds defs.mod)
949411264 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11265+ ?: (module-has-reserved-proj mod) |
949511266 ?. %+ levy imported
949611267 |= n=term
949711268 &((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))))
@@ -9515,6 +11286,43 @@
951511286 (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
951611287 (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
951711288::
11289+:: A detailed failure is attached only to the first mold that actually
11290+:: failed in this check, using that module's checked source mold table.
11291++$ imold-failure [message=@t overlap=(unit [name=term cases=upair])]
11292+:: Validate a generic wrapper without an unbounded duplicate-name pass.
11293+++ module-mold-params-valid
11294+ |= [vars=(list @t) seen=(set @t) fuel=@ud]
11295+ ^- ?
11296+ ?~ vars &
11297+ ?: =(0 fuel) |
11298+ ?: (~(has in:..zuse seen) i.vars) |
11299+ $(vars t.vars, seen (~(put in:..zuse seen) i.vars), fuel (dec fuel))
11300+++ module-mold-overlap
11301+ |= [m=[name=term body=shape] molds=imolds]
11302+ ^- (unit upair)
11303+ =/ sh=shape body.m
11304+ =/ valid=?
11305+ ?. ?=(%generic -.sh) &
11306+ ?~ vars.sh |
11307+ (module-mold-params-valid vars.sh *(set @t) 256)
11308+ ?. valid ~
11309+ =? sh ?=(%generic -.sh) body.sh
11310+ ?. ?=(%union -.sh) ~
11311+ (union-source-overlap cases.sh molds 256)
11312+++ module-mold-types-detail
11313+ |= [molds=imolds state=istate]
11314+ ^- (each imold-types imold-failure)
11315+ ?~ molds [%& ~]
11316+ =/ m=[name=term body=shape] i.molds
11317+ =/ t=(unit [template=ischeme state=istate])
11318+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11319+ ?~ t
11320+ =/ overlap=(unit upair) (module-mold-overlap m molds.state)
11321+ [%| ['module mold needs unsupported inference' ?~(overlap ~ `[name.m u.overlap])]]
11322+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
11323+ =/ rest=(each imold-types imold-failure) $(molds t.molds)
11324+ ?: ?=(%| -.rest) rest
11325+ [%& [[name.m template.u.t] p.rest]]
951811326++ module-mold-types
951911327 |= [molds=imolds state=istate]
952011328 ^- (each imold-types @t)
@@ -9573,11 +11381,17 @@
957311381 =(var name.i.args.tail)
957411382::
957511383++ prelude-label
9576− |= [typ=itype name=term]
11384+ |= [typ=itype name=term vars=(list @ud)]
957711385 ^- itype
957811386 ?: ?=(%jrec -.typ) typ(label `name)
11387+ ?: ?=(%grec -.typ)
11388+ ?. (identity-union-parameters vars args.typ) typ(label ~)
11389+ typ(label `name)
957911390 ?. ?=(%union -.typ) typ
9580− ?^ args.typ typ
11391+ ?. (identity-union-parameters vars args.typ)
11392+ ?~ origin.typ typ
11393+ ?: =(at.u.origin.typ /lib/jibb/internal/jibb) typ(label ~)
11394+ typ
958111395 typ(label `name)
958211396::
958311397++ partial-prelude-molds
@@ -9592,7 +11406,7 @@
959211406 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
959311407 ?~ out $(molds t.molds)
959411408 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
9595− =. typ.template.u.out (prelude-label typ.template.u.out name.m)
11409+ =. typ.template.u.out (prelude-label typ.template.u.out name.m vars.template.u.out)
959611410 [[name.m template.u.out] $(molds t.molds)]
959711411::
959811412:: A compiler-owned interface available only to the dedicated
@@ -9601,11 +11415,19 @@
960111415 ^- ifile
960211416 =/ a=itype [%avar 0]
960311417 =/ pair=itype [%cell a a]
11418+ =/ b=itype [%rvar 0]
11419+ =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
11420+ =/ minus=ischeme [[%fn b b] ~[0]]
960411421 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
9605− [~[[%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~]
11422+ =/ utf8=itype [%atom 'tD']
11423+ =/ tape=itype [%collection %list ~[utf8]]
11424+ =/ codepoints=itype [%collection %list ~[[%atom %c]]]
11425+ =/ text-trip=ischeme [[%fn [%atom %t] tape] ~]
11426+ =/ text-tuba=ischeme [[%fn tape codepoints] ~]
11427+ [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater] [%raw-trip text-trip] [%raw-tuba text-tuba]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
960611428::
960711429++ infer-private-internal
9608− |= src=@t
11430+ |= [src=@t public-source=@t]
960911431 ^- (unit ifile)
961011432 =/ at=path /lib/jibb/internal/jibb
961111433 =/ parsed (parse at src)
@@ -9623,15 +11445,65 @@
962311445 ?: (lien vals |=(n=term =(n %main))) ~
962411446 =/ molds=imolds (collect-simple-molds defs.mod)
962511447 =/ globals=(list term) (weld (import-binding-names imports.mod) vals)
9626− =/ js=ijimports ~[[face.i.imports.mod private-primitive-interface]]
11448+ :: The private source can use the public list and unit molds before the
11449+ :: prelude is otherwise prepared. Re-read the trusted public source here
11450+ :: and admit only its validated canonical templates; do not accept schemes
11451+ :: supplied independently by the caller.
11452+ =/ public=(each module error) (parse /lib/jibb/prelude/jibb public-source)
11453+ ?: ?=(%| -.public) ~
11454+ ?^ (duplicate-defs defs.p.public) ~
11455+ ?. (module-scope-valid p.public ~ ~) ~
11456+ =/ source-molds=imolds (collect-simple-molds defs.p.public)
11457+ =/ written-list=(unit shape) (find-simple-mold %list source-molds)
11458+ =/ source-list=(unit ischeme)
11459+ ?~ written-list ~
11460+ ?. (standard-prelude-list u.written-list) ~
11461+ `[[%collection %list ~[[%var 0]]] ~[0]]
11462+ :: Derive the public unit template from its actual source, then compare
11463+ :: the complete nominal template before making it available privately.
11464+ =/ unit-decl=(unit shape) (find-simple-mold %unit source-molds)
11465+ =/ source-unit=(unit ischeme)
11466+ ?~ unit-decl ~
11467+ =/ unit-molds=imolds ~[[%unit u.unit-decl]]
11468+ =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~ ~ ~ ~ ~ ~]
11469+ =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
11470+ =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
11471+ =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
11472+ ?~ found ~
11473+ ?. (standard-unit-template u.found /lib/jibb/prelude/jibb) ~
11474+ found
11475+ =/ primitive=ifile private-primitive-interface
11476+ =? primitive ?=(^ source-list)
11477+ primitive(molds [[%list u.source-list] molds.primitive])
11478+ =? primitive ?=(^ source-unit)
11479+ primitive(molds [[%unit u.source-unit] molds.primitive])
11480+ =/ js=ijimports ~[[face.i.imports.mod primitive]]
962711481 =/ reserved=(list term) ~[face.i.imports.mod]
962811482 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9629− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256]
11483+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~ ~ ~ ~ ~ ~]
963011484 =/ mts=(each imold-types @t) (module-mold-types molds state)
9631− ?: ?=(%| -.mts) ~
9632− =/ env=ienv (resolve-supported-defs defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
11485+ =/ usable=(unit imold-types)
11486+ ?: ?=(%& -.mts) `p.mts
11487+ :: Missing public templates may make an unrelated internal mold
11488+ :: unavailable. Validate all molds once with isolated canonical
11489+ :: templates before admitting only those inferred using the actual
11490+ :: source-backed templates. The proof interface is never exported.
11491+ ?. |(?=(~ source-list) ?=(~ source-unit)) ~
11492+ =/ nil=itype [%const [%null %n 0 '~']]
11493+ =/ canonical-unit=ischeme
11494+ [[%union ~[nil [%cell nil [%face %u [%var 0]]]] `[/lib/jibb/prelude/jibb %unit] `%unit ~[[%var 0]]] ~[0]]
11495+ =/ canonical-list=ischeme [[%collection %list ~[[%var 0]]] ~[0]]
11496+ =/ proof-primitive=ifile private-primitive-interface
11497+ =. molds.proof-primitive ~[[%list canonical-list] [%unit canonical-unit]]
11498+ =/ proof-imports=ijimports ~[[face.i.imports.mod proof-primitive]]
11499+ =/ proof=(each imold-types @t) (module-mold-types molds state(jimports proof-imports))
11500+ ?: ?=(%| -.proof) ~
11501+ `(partial-prelude-molds molds state)
11502+ ?~ usable ~
11503+ =/ resolution=iresolved (resolve-groups defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
11504+ =/ env=ienv env.resolution
963311505 ?. (module-values-complete defs.mod env) ~
9634− `[env p.mts at ~]
11506+ `[env u.usable at ~ artifacts.resolution ~ `src ~]
963511507::
963611508++ partial-prelude-interface-with-internal
963711509 |= [src=@t internal-source=(unit @t)]
@@ -9647,7 +11519,7 @@
964711519 ?. ?=([[%jibb *] ~] imports.p.parsed) ~
964811520 ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
964911521 ?~ internal-source ~
9650− =/ built=(unit ifile) (infer-private-internal u.internal-source)
11522+ =/ built=(unit ifile) (infer-private-internal u.internal-source src)
965111523 ?~ built ~
965211524 `~[[face.i.imports.p.parsed u.built]]
965311525 ?~ private ~
@@ -9664,16 +11536,16 @@
966411536 =? env-molds declared
966511537 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
966611538 =/ reserved=(list term) ?:(declared ~[%list] ~)
9667− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256]
11539+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~ ~ ~ ~ ~ ~]
966811540 :: Other prelude molds may use list only after its source has passed
966911541 :: the standard-list check. The raw declaration remains removed.
967011542 =/ declared-list=(unit shape) (find-simple-mold %list molds)
967111543 =/ mold-prelude=(unit ifile)
967211544 ?~ declared-list ~
967311545 ?. (standard-prelude-list u.declared-list) ~
9674− `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~]
11546+ `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~ ~]
967511547 =/ mt=imold-types (partial-prelude-molds molds state(prelude mold-prelude))
9676− =/ partial=ifile [~ mt at ~]
11548+ =/ partial=ifile [~ mt at ~ ~ ~ ~ ~]
967711549 :: An explicitly qualified re-export must resolve. Other unsupported
967811550 :: prelude declarations remain reserved but absent from the interface.
967911551 =/ required=imolds
@@ -9684,9 +11556,13 @@
968411556 ?~ names.sh |
968511557 ?=(^ t.names.sh)
968611558 ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
9687− =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
11559+ =/ resolution=iresolved (resolve-groups ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
11560+ =/ env=ienv env.resolution
968811561 ?. (hole-values-present ds env) ~
9689− `[env mt at ~]
11562+ =/ deps=(list iwidth-dependency)
11563+ ?~ u.private ~
11564+ ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
11565+ `[env mt at ~ artifacts.resolution deps `src ~]
969011566::
969111567++ partial-prelude-interface
969211568 |= src=@t
@@ -9737,27 +11613,103 @@
973711613 ?: =(at at.i.cache) `iface.i.cache
973811614 $(cache t.cache)
973911615::
11616+:: These certificates retain the complete checked source closure. The
11617+:: trusted host must supply the identical prepared prelude and reader nouns.
11618+:: Exact bundle equality binds all source paths and versions; the set
11619+:: retains transitive paths for active-cycle checks. Request-bearing graphs
11620+:: alone have a size limit; incompatible diamond evidence fails closed.
11621+++ request-graph-requests-add
11622+ |= [pending=(list irequest-evidence) acc=(list irequest-evidence) fuel=@ud]
11623+ ^- (unit (list irequest-evidence))
11624+ ?~ pending `acc
11625+ ?: =(0 fuel) ~
11626+ =/ hit=(list irequest-evidence)
11627+ (skim acc |=(x=irequest-evidence &(=(api-at.x api-at.i.pending) =(name.x name.i.pending))))
11628+ ?^ hit
11629+ ?. ?=([* ~] hit) ~
11630+ ?. =(i.hit i.pending) ~
11631+ $(pending t.pending, fuel (dec fuel))
11632+ $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
11633+++ request-graph-inputs-match
11634+ |= [g=irequest-graph externals=iexternals marks=imark-externals modules=jbundle values=(list term) molds=(list term) prelude=(unit ifile)]
11635+ ^- ?
11636+ ?& =(bundle-input.g modules)
11637+ =(prelude-input.g prelude)
11638+ =(prelude-values.g values)
11639+ =(prelude-molds.g molds)
11640+ =(externals.g externals)
11641+ =(marks.g marks)
11642+ ==
11643+++ request-graph-merge
11644+ |= [imports=ijimports g=irequest-graph fuel=@ud]
11645+ ^- (unit irequest-graph)
11646+ ?~ imports `g
11647+ ?: =(0 fuel) ~
11648+ =/ child=ifile interface.i.imports
11649+ ?~ graph.child ~
11650+ =/ cg=irequest-graph u.graph.child
11651+ ?. ?& =(bundle-input.g bundle-input.cg)
11652+ =(prelude-input.g prelude-input.cg)
11653+ =(prelude-values.g prelude-values.cg)
11654+ =(prelude-molds.g prelude-molds.cg)
11655+ =(externals.g externals.cg)
11656+ =(marks.g marks.cg)
11657+ ==
11658+ ~
11659+ =/ merged=(set path) (~(uni in:..zuse paths.g) paths.cg)
11660+ =/ rs=(unit (list irequest-evidence))
11661+ (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
11662+ ?~ rs ~
11663+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
11664+ $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
11665+++ request-graph-reusable
11666+ |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
11667+ ^- ?
11668+ ?~ source.f |
11669+ ?. =(u.source.f src) |
11670+ ?~ graph.f |
11671+ =/ g=irequest-graph u.graph.f
11672+ ?. (request-graph-inputs-match g externals marks modules values molds prelude) |
11673+ ?. (~(has in:..zuse paths.g) at.f) |
11674+ !(lien active |=(p=path (~(has in:..zuse paths.g) p)))
11675+::
974011676++ resolve-jibb-imports
974111677 |= [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)]
974211678 ^- jimports-result
11679+ =/ result=jimports-detailed-result
11680+ (resolve-jibb-imports-detailed imports externals mark-externals modules active prelude-values prelude-molds cache prelude)
11681+ ?: ?=(%| -.result) [%| message.p.result]
11682+ [%& p.result]
11683+++ resolve-jibb-imports-detailed
11684+ |= [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)]
11685+ ^- jimports-detailed-result
974311686 ?~ imports [%& [~ cache]]
974411687 ?. ?=(%jibb -.i.imports) $(imports t.imports)
974511688 =/ at=path (weld path.i.imports `path`~[%jibb])
974611689 ?: =(at /lib/jibb/internal/jibb)
9747− [%| 'the prelude internal module is private']
11690+ [%| ['the prelude internal module is private' ~]]
974811691 ?: =(at /lib/jibb/primitives/jibb)
9749− [%| 'the prelude primitive interface is private']
11692+ [%| ['the prelude primitive interface is private' ~]]
975011693 ?: (lien active |=(p=path =(p at)))
9751− [%| (crip "import cycle at {(spud at)}")]
11694+ [%| [(crip "import cycle at {(spud at)}") ~]]
975211695 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
9753− ?~ found [%| (crip "module source missing: {(spud at)}")]
9754− ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
11696+ ?~ found [%| [(crip "module source missing: {(spud at)}") ~]]
11697+ ?^ t.found [%| [(crip "duplicate module sources: {(spud at)}") ~]]
975511698 =/ cached=(unit ifile) (find-jibb-cache at cache)
9756− =/ iface=jfile-result
9757− ?^ cached [%& [u.cached cache]]
9758− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
11699+ =/ iface=jfile-detailed-result
11700+ ?^ cached
11701+ ?. =(at.u.cached at) [%| ['cached module identity needs unsupported inference' ~]]
11702+ ?~ graph.u.cached
11703+ :: A detached legacy interface has unknown evidence. Rebuild it
11704+ :: against the current graph, without retaining any stale entry.
11705+ =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
11706+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
11707+ ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
11708+ [%| ['cached module evidence needs unsupported inference' ~]]
11709+ [%& [u.cached cache]]
11710+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
975911711 ?: ?=(%| -.iface) [%| p.iface]
9760− =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
11712+ =/ rest=jimports-detailed-result $(imports t.imports, cache cache.p.iface)
976111713 ?: ?=(%| -.rest) rest
976211714 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
976311715::
@@ -9891,6 +11843,7 @@
989111843 ^- ?
989211844 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
989311845 =/ derived=(list term) (weld path-names poke-names)
11846+ ?: (lien derived |=(n=term =(n %proj))) |
989411847 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
989511848 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
989611849::
@@ -9979,6 +11932,346 @@
997911932 ?~ paths [%| 'API path declaration needs unsupported analysis']
998011933 [%& u.paths]
998111934::
11935+:: Analysis evidence retains the API source, the prepared interface, the
11936+:: caller's reader results and the resolved Jibb dependency cache alongside
11937+:: the typed path declarations. Reader results and prepared interfaces are
11938+:: trusted inputs: this does not verify their underlying Hoon source/version,
11939+:: create requests or check the provenance of arbitrary values.
11940++$ iapi-path-evidence
11941+ [at=path source=@t prepared=iprelude externals=iexternals marks=imark-externals dependencies=jcache paths=(list iapi-path-typed)]
11942+++ api-path-evidence-source
11943+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
11944+ ^- (each iapi-path-evidence @t)
11945+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path evidence requires /ui/api/<agent>.jibb']
11946+ =/ parsed (parse file src)
11947+ ?: ?=(%| -.parsed) [%| 'API path evidence source does not parse']
11948+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11949+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11950+ ?~ prepared [%| 'API path evidence needs the prepared prelude']
11951+ =/ public=ifile iface.u.prepared
11952+ =/ deps=jimports-result
11953+ (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
11954+ ?: ?=(%| -.deps) [%| p.deps]
11955+ =/ paths=(unit (list iapi-path-typed))
11956+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
11957+ ?~ paths [%| 'API path declaration needs unsupported analysis']
11958+ [%& [file src u.prepared externals marks cache.p.deps u.paths]]
11959+:: Graph-aware variant preserves the caller active stack and cache.
11960+++ api-path-evidence-graph
11961+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
11962+ ^- (each iapi-path-evidence @t)
11963+ ?~ active [%| 'API analysis needs an active graph']
11964+ ?. =(i.active file) [%| 'API analysis active graph does not start at the source']
11965+ ?: (lien t.active |=(p=path =(p file))) [%| 'API analysis active graph contains a cycle']
11966+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path evidence requires /ui/api/<agent>.jibb']
11967+ =/ parsed (parse file src)
11968+ ?: ?=(%| -.parsed) [%| 'API path evidence source does not parse']
11969+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
11970+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
11971+ ?~ prepared [%| 'API path evidence needs the prepared prelude']
11972+ =/ public=ifile iface.u.prepared
11973+ =/ deps=jimports-result
11974+ (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
11975+ ?: ?=(%| -.deps) [%| p.deps]
11976+ =/ paths=(unit (list iapi-path-typed))
11977+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
11978+ ?~ paths [%| 'API path declaration needs unsupported analysis']
11979+ [%& [file src u.prepared externals marks cache.p.deps u.paths]]
11980+::
11981+:: This query classifies a unique path declaration only. Missing evidence
11982+:: or a nonunique name is unknown; it proves nothing about an ask value.
11983+:: Like prepared interfaces, the supplied evidence is a trusted host input.
11984+++ api-path-watchability
11985+ |= [evidence=(unit iapi-path-evidence) case-name=term]
11986+ ^- ?(%watchable %not-watchable %unknown)
11987+ ?~ evidence %unknown
11988+ =/ found=(list iapi-path-typed)
11989+ (skim paths.u.evidence |=(p=iapi-path-typed =(name.path.p case-name)))
11990+ ?. ?=([* ~] found) %unknown
11991+ ?~ scry.path.i.found %watchable
11992+ %not-watchable
11993+::
11994+:: These are declaration-derived request components, not a callable gate,
11995+:: an ask value, or proof of a value's provenance. Keep the exact trusted
11996+:: source/reader evidence until a later checked interface and lowerer can
11997+:: attach it to a generated request. No argument ordering is claimed here.
11998++$ iapi-request-parameter [name=term typ=itype at=span]
11999++$ iapi-request-parts
12000+ [evidence=iapi-path-evidence path=iapi-path-typed parameters=(list iapi-request-parameter) reply-sample=itype fold=(unit itype) watchability=?(%watchable %not-watchable)]
12001+++ api-request-parameter-types
12002+ |= params=(list iapi-parameter)
12003+ ^- (unit (list iapi-request-parameter))
12004+ ?~ params `~
12005+ =/ aura=@ta aura.i.params
12006+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
12007+ =/ rest=(unit (list iapi-request-parameter)) $(params t.params)
12008+ ?~ rest ~
12009+ `[[name.i.params [%atom aura] at.i.params] u.rest]
12010+::
12011+:: A single diff's fold consumes the tagged diff and the previous full value.
12012+:: Multiple-diff unions need a checked union representation and remain open.
12013+++ api-request-fold-type
12014+ |= p=iapi-path-typed
12015+ ^- (unit (unit itype))
12016+ ?~ diffs.p `~
12017+ ?^ t.diffs.p ~
12018+ =/ d=iapi-mark-type i.diffs.p
12019+ =/ literal=lit [%term %tas name.d (crip ['%' (trip name.d)])]
12020+ =/ sample=itype [%cell [%cell [%const literal] typ.d] full.p]
12021+ ``[%fn sample full.p]
12022+::
12023+++ api-request-parts
12024+ |= [evidence=(unit iapi-path-evidence) case-name=term]
12025+ ^- (unit iapi-request-parts)
12026+ ?~ evidence ~
12027+ =/ found=(list iapi-path-typed)
12028+ (skim paths.u.evidence |=(p=iapi-path-typed =(name.path.p case-name)))
12029+ ?. ?=([* ~] found) ~
12030+ =/ p=iapi-path-typed i.found
12031+ =/ raw=(unit (list iapi-parameter)) (api-path-parameters segments.path.p ~)
12032+ ?~ raw ~
12033+ =/ params=(unit (list iapi-request-parameter)) (api-request-parameter-types u.raw)
12034+ ?~ params ~
12035+ =/ fold=(unit (unit itype)) (api-request-fold-type p)
12036+ ?~ fold ~
12037+ =/ watch=?(%watchable %not-watchable) ?~(scry.path.p %watchable %not-watchable)
12038+ `[u.evidence p u.params full.p u.fold watch]
12039+::
12040+:: Check ordinary API molds and values plus every declared mark type using
12041+:: the same trusted source, prepared prelude and reader inputs as path
12042+:: evidence. Keep elaborations with those inputs for a later interface.
12043+:: This is partial analysis: an unused /- core is not independently checked,
12044+:: definitions needing derived values remain unsupported, and no complete
12045+:: API, request or constructor is exported or given runtime behavior.
12046++$ iapi-support-evidence
12047+ [paths=iapi-path-evidence values=ienv molds=imold-types marks=(list iapi-mark-type) elaborations=(list iwidth-definition)]
12048+++ api-support-analysis-source
12049+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
12050+ ^- (each iapi-support-evidence @t)
12051+ =/ path-result (api-path-evidence-source file src externals marks modules prepared)
12052+ ?: ?=(%| -.path-result) [%| p.path-result]
12053+ =/ evidence=iapi-path-evidence p.path-result
12054+ =/ parsed (parse file src)
12055+ ?: ?=(%| -.parsed) [%| 'API source does not parse']
12056+ =/ mod=module p.parsed
12057+ =/ ordinary=(list def)
12058+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
12059+ =/ prep=iprelude prepared.evidence
12060+ ?. (module-scope-valid mod(defs ordinary) values.prep molds.prep) [%| 'API ordinary scope needs unsupported inference']
12061+ =/ vals=(list term) (global-value-names ordinary)
12062+ ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12063+ =/ declared=(list term) (collect-mark-imports imports.mod)
12064+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
12065+ ?~ mark-types [%| 'API declared marks need unsupported inference']
12066+ =/ prelude=(unit ifile) `iface.prep
12067+ =/ deps=jimports-result
12068+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.prep molds.prep dependencies.evidence prelude)
12069+ ?: ?=(%| -.deps) [%| p.deps]
12070+ =/ molds=imolds (collect-simple-molds ordinary)
12071+ =/ globals=(list term) (weld values.prep (weld (import-binding-names imports.mod) vals))
12072+ =/ surs=(list term) (collect-sur-imports imports.mod)
12073+ =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
12074+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12075+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
12076+ =/ mts=(each imold-types @t) (module-mold-types molds state)
12077+ ?: ?=(%| -.mts) [%| p.mts]
12078+ =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
12079+ ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
12080+ [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
12081+:: Preserve the same graph context through supporting definitions.
12082+++ api-support-analysis-graph
12083+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12084+ ^- (each iapi-support-evidence @t)
12085+ =/ path-result (api-path-evidence-graph file src externals marks modules active cache prepared)
12086+ ?: ?=(%| -.path-result) [%| p.path-result]
12087+ =/ evidence=iapi-path-evidence p.path-result
12088+ =/ parsed (parse file src)
12089+ ?: ?=(%| -.parsed) [%| 'API source does not parse']
12090+ =/ mod=module p.parsed
12091+ =/ ordinary=(list def)
12092+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
12093+ =/ prep=iprelude prepared.evidence
12094+ ?. (module-scope-valid mod(defs ordinary) values.prep molds.prep) [%| 'API ordinary scope needs unsupported inference']
12095+ =/ vals=(list term) (global-value-names ordinary)
12096+ ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12097+ =/ declared=(list term) (collect-mark-imports imports.mod)
12098+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
12099+ ?~ mark-types [%| 'API declared marks need unsupported inference']
12100+ =/ prelude=(unit ifile) `iface.prep
12101+ =/ deps=jimports-result
12102+ (resolve-jibb-imports imports.mod externals marks modules active values.prep molds.prep dependencies.evidence prelude)
12103+ ?: ?=(%| -.deps) [%| p.deps]
12104+ =/ molds=imolds (collect-simple-molds ordinary)
12105+ =/ globals=(list term) (weld values.prep (weld (import-binding-names imports.mod) vals))
12106+ =/ surs=(list term) (collect-sur-imports imports.mod)
12107+ =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
12108+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12109+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
12110+ =/ mts=(each imold-types @t) (module-mold-types molds state)
12111+ ?: ?=(%| -.mts) [%| p.mts]
12112+ =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
12113+ ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
12114+ [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
12115+::
12116+:: Type-analysis artifact for one plain request. The resolver may publish
12117+:: its interface only together with trusted source and reader evidence.
12118+:: No lowering or runtime validator exists.
12119+:: Value watchability remains unproved even for a watchable declaration.
12120++$ ione-request-interface
12121+ [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12122+++ request-compatible-ask
12123+ |= prelude=iprelude
12124+ ^- (unit ischeme)
12125+ =/ public=ifile iface.prelude
12126+ ?. =(at.public /lib/jibb/prelude/jibb) ~
12127+ =/ ask=(unit ischeme) (find-jibb-mold %ask public)
12128+ ?~ ask ~
12129+ ?. ?=([@ ~] vars.u.ask) ~
12130+ ?. ?=(%union -.typ.u.ask) ~
12131+ ?. =(origin.typ.u.ask `[/lib/jibb/internal/jibb %ask]) ~
12132+ ?. (identity-union-parameters vars.u.ask args.typ.u.ask) ~
12133+ =/ m=@ud i.vars.u.ask
12134+ ?: (itype-var-is-atom m typ.u.ask) ~
12135+ ?. (levy (itype-vars typ.u.ask) |=(n=@ud =(n m))) ~
12136+ ?: (itype-has-tag typ.u.ask) ~
12137+ =/ private=(list iwidth-dependency)
12138+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12139+ ?. ?=([* ~] private) ~
12140+ ?~ source.i.private ~
12141+ =/ path=(unit ischeme) (find-jibb-mold %path public)
12142+ ?~ path ~
12143+ ?^ vars.u.path ~
12144+ =/ path-type=itype [%collection %list ~[[%atom %ta]]]
12145+ ?. =(typ.u.path path-type) ~
12146+ =/ unit-template=(unit ischeme) (find-jibb-mold %unit public)
12147+ ?~ unit-template ~
12148+ ?. (standard-unit-template u.unit-template /lib/jibb/prelude/jibb) ~
12149+ =/ state-unit=(unit itype) (template-apply u.unit-template ~[[%noun ~]])
12150+ ?~ state-unit ~
12151+ =/ path-unit=(unit itype) (template-apply u.unit-template ~[path-type])
12152+ ?~ path-unit ~
12153+ =/ output=itype [%cell [%face %state [%noun ~]] [%face %message [%var m]]]
12154+ =/ agent-input=itype [%cell [%face %mark [%atom %tas]] [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]]
12155+ =/ store-input=itype [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]
12156+ =/ pure-case=itype [%cell [%const [%term %tas %pure '%pure']] [%face %value [%var m]]]
12157+ =/ agent-case=itype
12158+ [%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]]]]]]]]
12159+ =/ store-case=itype
12160+ [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %name [%atom %tas]] [%face %receive [%fn store-input output]]]]]
12161+ ?. =(cases.typ.u.ask ~[pure-case agent-case store-case]) ~
12162+ ask
12163+::
12164+:: The first supported standalone API has exactly one mark import and one
12165+:: plain path declaration, with no other definitions or imports. No partial
12166+:: success is published when source, schema, or a required mold is unknown.
12167+++ one-request-interface-source
12168+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
12169+ ^- (each ione-request-interface @t)
12170+ =/ out (api-support-analysis-source file src externals marks modules prepared)
12171+ ?: ?=(%| -.out) [%| p.out]
12172+ =/ support=iapi-support-evidence p.out
12173+ =/ ev=iapi-path-evidence paths.support
12174+ =/ parsed (parse file src)
12175+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12176+ =/ mod=module p.parsed
12177+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
12178+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
12179+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
12180+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
12181+ =/ p=iapi-path-typed i.paths.ev
12182+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12183+ ?~ parts [%| 'request components need unsupported inference']
12184+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
12185+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
12186+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
12187+ =/ valid-marks=?
12188+ ?~ fold.u.parts ?=([* ~] marks.support)
12189+ ?=([* [* ~]] marks.support)
12190+ ?. valid-marks [%| 'request marks need unsupported inference']
12191+ =/ fold-open=?
12192+ ?~ fold.u.parts |
12193+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12194+ ?: fold-open [%| 'request fold needs unsupported inference']
12195+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12196+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12197+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12198+ ?~ ask [%| 'request ask needs unsupported inference']
12199+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
12200+ ?~ result [%| 'request ask needs unsupported inference']
12201+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12202+ =/ sample=itype
12203+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12204+ ?~ parameters.u.parts callback
12205+ [%cell typ.i.parameters.u.parts callback]
12206+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12207+ =/ exports=imold-types
12208+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12209+ =/ prelude=iprelude prepared.ev
12210+ =/ public=ifile iface.prelude
12211+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12212+ =/ private=(list iwidth-dependency)
12213+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12214+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12215+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12216+ =/ req=irequest-evidence
12217+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12218+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12219+ [%& [support u.parts interface]]
12220+:: Graph-aware request artifact; resolver use remains type-only.
12221+++ one-request-interface-graph
12222+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12223+ ^- (each ione-request-interface @t)
12224+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
12225+ ?: ?=(%| -.out) [%| p.out]
12226+ =/ support=iapi-support-evidence p.out
12227+ =/ ev=iapi-path-evidence paths.support
12228+ =/ parsed (parse file src)
12229+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12230+ =/ mod=module p.parsed
12231+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
12232+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
12233+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
12234+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
12235+ =/ p=iapi-path-typed i.paths.ev
12236+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12237+ ?~ parts [%| 'request components need unsupported inference']
12238+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
12239+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
12240+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
12241+ =/ valid-marks=?
12242+ ?~ fold.u.parts ?=([* ~] marks.support)
12243+ ?=([* [* ~]] marks.support)
12244+ ?. valid-marks [%| 'request marks need unsupported inference']
12245+ =/ fold-open=?
12246+ ?~ fold.u.parts |
12247+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12248+ ?: fold-open [%| 'request fold needs unsupported inference']
12249+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12250+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12251+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12252+ ?~ ask [%| 'request ask needs unsupported inference']
12253+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
12254+ ?~ result [%| 'request ask needs unsupported inference']
12255+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12256+ =/ sample=itype
12257+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12258+ ?~ parameters.u.parts callback
12259+ [%cell typ.i.parameters.u.parts callback]
12260+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12261+ =/ exports=imold-types
12262+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12263+ =/ prelude=iprelude prepared.ev
12264+ =/ public=ifile iface.prelude
12265+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12266+ =/ private=(list iwidth-dependency)
12267+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12268+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12269+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12270+ =/ req=irequest-evidence
12271+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12272+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12273+ [%& [support u.parts interface]]
12274+::
998212275++ api-mark-exports
998312276 |= [marks=(list term) all=(list term) externals=imark-externals]
998412277 ^- imold-types
@@ -10022,42 +12315,288 @@
1002212315 =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
1002312316 ?~ mark ~
1002412317 =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
10025− `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]]]
12318+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
12319+::
12320+:: Source-proven ordinary helpers validate each selected /sur dependency.
12321+:: Unused or less direct cores remain unsupported by this first interface.
12322+++ api-sur-covered
12323+ |= [surs=(list term) defs=(list def) externals=iexternals all=(list term)]
12324+ ^- ?
12325+ ?~ surs &
12326+ =/ found=(list def)
12327+ %+ skim defs
12328+ |= d=def
12329+ ?. ?=(%mold -.d) |
12330+ ?. ?=(%ref -.shape.d) |
12331+ ?. ?=([@ [@ ~]] names.shape.d) |
12332+ =(i.t.names.shape.d i.surs)
12333+ ?~ found |
12334+ =/ selected=def i.found
12335+ ?. ?=(%mold -.selected) |
12336+ =/ sh=shape shape.selected
12337+ ?. ?=(%ref -.sh) |
12338+ ?. ?=([@ [@ ~]] names.sh) |
12339+ =/ checked=(unit itype) (find-imported-mold i.surs i.names.sh externals all)
12340+ ?~ checked |
12341+ $(surs t.surs)
12342+::
12343++$ imulti-request-gates [values=ienv requests=(list irequest-evidence)]
12344+++ api-request-gates
12345+ |= [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]
12346+ ^- (unit imulti-request-gates)
12347+ ?~ paths `[~ ~]
12348+ ?: =(0 fuel) ~
12349+ =/ p=iapi-path-typed i.paths
12350+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12351+ ?~ parts ~
12352+ ?. ?=(?(~ [* ~]) parameters.u.parts) ~
12353+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) ~
12354+ ?^ scry.path.p ~
12355+ ?^ (itype-vars reply-sample.u.parts) ~
12356+ ?: (itype-has-tag reply-sample.u.parts) ~
12357+ =/ open-fold=?
12358+ ?~ fold.u.parts |
12359+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12360+ ?: open-fold ~
12361+ =/ result=(unit itype) (template-apply ask ~[[%var 0]])
12362+ ?~ result ~
12363+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12364+ =/ sample=itype
12365+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12366+ ?~ parameters.u.parts callback
12367+ [%cell typ.i.parameters.u.parts callback]
12368+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12369+ =/ prep=iprelude prepared.ev
12370+ =/ req=irequest-evidence
12371+ [file name.path.p p src public internal values.prep molds.prep externals marks]
12372+ =/ rest=(unit imulti-request-gates)
12373+ $(paths t.paths, fuel (dec fuel))
12374+ ?~ rest ~
12375+ `[[[name.path.p scheme] values.u.rest] [req requests.u.rest]]
12376+::
12377+++ api-poke-from-checked
12378+ |= [file=path mod=module marks=imark-externals values=(list term) molds=(list term) prelude=(unit ifile)]
12379+ ^- (unit [values=ienv derived=(list iderived)])
12380+ =/ pokes=(list def)
12381+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12382+ ?~ pokes `[~ ~]
12383+ ?. ?=([* ~] pokes) ~
12384+ =/ declared=(list term) (collect-mark-imports imports.mod)
12385+ =/ ns=(unit (list term)) (api-poke-mark-names pokes declared)
12386+ ?~ ns ~
12387+ ?. ?=([@ ~] u.ns) ~
12388+ =/ matching=(list import)
12389+ %+ skim imports.mod
12390+ |= i=import
12391+ ?. ?=(%mark -.i) |
12392+ =(mark.i i.u.ns)
12393+ ?. ?=([* ~] matching) ~
12394+ =/ checked=(unit ifile)
12395+ (api-poke-interface file mod(defs pokes, imports matching) marks values molds prelude)
12396+ ?~ checked ~
12397+ `[values.u.checked derived.u.checked]
12398+::
12399+:: The partial interface is published atomically: all paths, ordinary
12400+:: source definitions, declared marks and the poke must check. Unselected
12401+:: /sur bindings, runtime validation and value watchability remain unproved.
12402+++ multi-request-interface-graph
12403+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12404+ ^- (each [iface=ifile cache=jcache] @t)
12405+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
12406+ ?: ?=(%| -.out) [%| p.out]
12407+ =/ support=iapi-support-evidence p.out
12408+ =/ ev=iapi-path-evidence paths.support
12409+ =/ parsed (parse file src)
12410+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12411+ =/ mod=module p.parsed
12412+ ?. (levy imports.mod |=(i=import ?=(?(%mark %sur) -.i)))
12413+ [%| 'request imports need unsupported inference']
12414+ =/ surs=(list term) (collect-sur-imports imports.mod)
12415+ ?. (api-sur-covered surs defs.mod externals surs)
12416+ [%| 'API source dependency needs unsupported inference']
12417+ ?~ paths.ev [%| 'request count needs unsupported inference']
12418+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12419+ ?~ ask [%| 'request ask needs unsupported inference']
12420+ =/ prep=iprelude prepared.ev
12421+ =/ public=ifile iface.prep
12422+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12423+ =/ private=(list iwidth-dependency)
12424+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12425+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12426+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12427+ =/ gates=(unit imulti-request-gates)
12428+ (api-request-gates paths.ev ev u.ask file src u.source.public u.source.i.private externals marks 256)
12429+ ?~ gates [%| 'request paths need unsupported inference']
12430+ =/ poke=(unit [values=ienv derived=(list iderived)])
12431+ (api-poke-from-checked file mod marks values.prep molds.prep `public)
12432+ ?~ poke [%| 'API poke needs unsupported inference']
12433+ =/ mark-molds=imold-types
12434+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12435+ =/ exports=imold-types (weld mark-molds molds.support)
12436+ =/ names=(list term) (turn exports |=(m=[name=term template=ischeme] name.m))
12437+ ?. (levy names |=(n=term (unique-value-name n names)))
12438+ [%| 'API exported molds need unsupported inference']
12439+ =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
12440+ =/ graph=irequest-graph
12441+ [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
12442+ =/ iface=ifile
12443+ [env exports file derived.u.poke elaborations.support ~ `src `graph]
12444+ [%& [iface dependencies.ev]]
1002612445::
1002712446++ infer-jibb-file
1002812447 |= [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)]
1002912448 ^- jfile-result
12449+ =/ out=jfile-detailed-result
12450+ (infer-jibb-file-detailed at src externals mark-externals modules active prelude-values prelude-molds cache prelude)
12451+ ?: ?=(%| -.out) [%| message.p.out]
12452+ [%& p.out]
12453+:: Returns structured root-source overlap evidence after the same full check.
12454+++ infer-jibb-file-detailed
12455+ |= [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)]
12456+ ^- jfile-detailed-result
1003012457 =/ parsed (parse at src)
10031− ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
12458+ ?: ?=(%| -.parsed) [%| [(crip "module source does not parse: {(spud at)}") ~]]
1003212459 =/ mod=module p.parsed
1003312460 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
10034− ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
12461+ ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]
1003512462 ?: ?=([%ui %api *] at)
1003612463 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
10037− ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
10038− [%& [u.iface [[at u.iface] cache]]]
12464+ ?^ iface
12465+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
12466+ [%& [checked [[at checked] cache]]]
12467+ ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
12468+ =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
12469+ =/ narrow=?
12470+ ?. ?=([[%mark *] ~] imports.mod) |
12471+ ?. ?=([[%mold *] ~] defs.mod) |
12472+ ?. =(%paths name.i.defs.mod) |
12473+ !?=(%union -.shape.i.defs.mod)
12474+ ?: narrow
12475+ =/ request=(each ione-request-interface @t)
12476+ (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
12477+ ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
12478+ =/ checked=ifile iface.p.request
12479+ [%& [checked [[at checked] dependencies.paths.support.p.request]]]
12480+ =/ multi=(each [iface=ifile cache=jcache] @t)
12481+ (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
12482+ ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
12483+ [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
1003912484 ?. (module-scope-valid mod prelude-values prelude-molds)
1004012485 ?: (pending-declared-poke at mod prelude-values prelude-molds)
10041− [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
10042− [%| (crip "module has conflicting names: {(spud at)}")]
12486+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
12487+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1004312488 =/ vals=(list term) (global-value-names defs.mod)
1004412489 ?: (lien vals |=(n=term =(n %main)))
10045− [%| (crip "module kind needs unsupported inference: {(spud at)}")]
10046− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
12490+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
12491+ =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
1004712492 ?: ?=(%| -.js) [%| p.js]
10048− =/ molds=imolds (collect-simple-molds defs.mod)
12493+ =/ collected=grec-collected
12494+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
12495+ (grec-collect-molds defs.mod)
12496+ =/ molds=imolds molds.collected
1004912497 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
1005012498 =/ surs=(list term) (collect-sur-imports imports.mod)
1005112499 =/ marks=(list term) (collect-mark-imports imports.mod)
1005212500 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
1005312501 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10054− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256]
10055− =/ mts=(each imold-types @t) (module-mold-types molds state)
10056− ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
10057− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
12502+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
12503+ :: Source and scope were checked above; preserve that exact root and prelude.
12504+ :: This first integration only indexes import-free library sources.
12505+ =/ index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])
12506+ ?^ imports.mod ~
12507+ ?~ prelude ~
12508+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude)
12509+ ?~ standard ~
12510+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~
12511+ =/ index=(map term shape) proofs.collected
12512+ ?. !=(index *(map term shape)) ~
12513+ ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~
12514+ `[at src u.prelude index]
12515+ =. grec-index.state index
12516+ =/ mts=(each imold-types imold-failure) (module-mold-types-detail molds state)
12517+ ?: ?=(%| -.mts)
12518+ ?~ overlap.p.mts [%| [(crip "{(trip message.p.mts)}: {(spud at)}") ~]]
12519+ =/ witness=[name=term cases=upair] u.overlap.p.mts
12520+ =/ first=@t (show-error src [at line.beg.first.cases.witness col.beg.first.cases.witness "first union case"])
12521+ =/ second=@t (show-error src [at line.beg.second.cases.witness col.beg.second.cases.witness "overlapping case"])
12522+ =/ msg=@t (of-wain:format ~[(crip "module mold {(trip name.witness)} has overlapping cases") first second])
12523+ [%| [msg `[at src name.witness cases.witness]]]
12524+ =/ resolution=iresolved
12525+ ?~ index
12526+ (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
12527+ (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
12528+ =/ env=ienv env.resolution
12529+ =. env
12530+ ?: (module-values-complete defs.mod env) env
12531+ ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
12532+ ?: (gth (met 3 src) 65.536) env
12533+ ?: (gth (lent defs.mod) 64) env
12534+ ?. (dg-source-candidate defs.mod 64) env
12535+ =/ transaction=(unit dgcommit) (dg-root-source at src)
12536+ ?~ transaction env
12537+ ?: (dg-interface-safe env.u.transaction) env.u.transaction
12538+ env
1005812539 ?. (module-values-complete defs.mod env)
10059− [%| (crip "module definitions need unsupported inference: {(spud at)}")]
10060− [%& [[env p.mts at ~] [[at [env p.mts at ~]] cache.p.js]]]
12540+ [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
12541+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
12542+ =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
12543+ ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
12544+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
12545+ [%& [iface [[at iface] cache.p.js]]]
12546+::
12547+:: A source-bound analysis of one named mold, not a module, island,
12548+:: request, watchability or runtime check. The host owns the trusted
12549+:: prepared prelude, canonical paths and reader/source version identities.
12550+:: The 256-node cap covers only classification, not source/graph work.
12551++$ igate-free-mold
12552+ [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]
12553+++ gate-free-mold-source
12554+ |= [file=path src=@t name=term externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude) fuel=@ud]
12555+ ^- (each igate-free-mold @t)
12556+ ?~ file [%| 'mold analysis needs a path ending in jibb']
12557+ ?. =(%jibb (rear file)) [%| 'mold analysis needs a path ending in jibb']
12558+ ?: |(=(file /lib/jibb/internal/jibb) =(file /lib/jibb/primitives/jibb))
12559+ [%| 'the prelude internal modules are private']
12560+ ?: ?=([%ui %api *] file) [%| 'API declarations need unsupported mold analysis']
12561+ ?: ?=([%ui %stores *] file) [%| 'store declarations need unsupported mold analysis']
12562+ =/ entries=jbundle (skim modules |=(m=jsource =(file at.m)))
12563+ ?: (gth (lent entries) 1) [%| 'duplicate root module sources']
12564+ =/ wrong-root=? ?~(entries | !=(source.i.entries src))
12565+ ?: wrong-root [%| 'root module source does not match bundle']
12566+ =/ parsed (parse file src)
12567+ ?: ?=(%| -.parsed) [%| 'mold source does not parse']
12568+ =/ mod=module p.parsed
12569+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
12570+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12571+ ?~ prepared [%| 'mold analysis needs the prepared prelude']
12572+ ?. (module-scope-valid mod values.u.prepared molds.u.prepared)
12573+ [%| 'mold source has conflicting or unsupported scope']
12574+ =/ selected=(list def)
12575+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(name.d name))))
12576+ ?~ selected [%| 'selected mold is not declared']
12577+ ?^ t.selected [%| 'selected mold is not unique']
12578+ ?> ?=(%mold -.i.selected)
12579+ =/ public=ifile iface.u.prepared
12580+ =/ js=jimports-result
12581+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
12582+ ?: ?=(%| -.js) [%| p.js]
12583+ =/ ms=imolds (collect-simple-molds defs.mod)
12584+ =/ vals=(list term) (global-value-names defs.mod)
12585+ =/ globals=(list term) (weld values.u.prepared (weld (import-binding-names imports.mod) vals))
12586+ =/ surs=(list term) (collect-sur-imports imports.mod)
12587+ =/ declared=(list term) (collect-mark-imports imports.mod)
12588+ =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
12589+ =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))
12590+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~ ~ ~ ~ ~ ~]
12591+ =/ inferred=(unit [template=ischeme state=istate])
12592+ (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
12593+ ?~ inferred [%| 'selected mold needs unsupported inference']
12594+ =/ template=ischeme template.u.inferred
12595+ =. typ.template (label-direct-union typ.template shape.i.selected name state)
12596+ =. typ.template (itype-normalize typ.template sub.state.u.inferred)
12597+ =/ cap=@ud (min fuel 256)
12598+ =/ analysis=igate-free (gate-free-type typ.template cap ~)
12599+ [%& [file src name u.prepared externals marks modules cache.p.js template fuel cap analysis]]
1006112600::
1006212601:: +golden-types-with-modules fails closed for imports without prelude
1006312602:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -10155,6 +12694,8 @@
1015512694 ?: ?=(%| -.parsed) (show-error src p.parsed)
1015612695 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
1015712696 ?^ duplicate (duplicate-fields-report file src u.duplicate)
12697+ ?: (module-has-reserved-proj p.parsed)
12698+ 'module has reserved proj name'
1015812699 =/ ds=(list def) defs.p.parsed
1015912700 =/ molds=imolds (collect-simple-molds ds)
1016012701 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -10163,6 +12704,33 @@
1016312704 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
1016412705 =/ cycles=(list icycle) (definite-value-cycles ds globals)
1016512706 =/ env=ienv env.resolution
12707+ =/ recovered=(list term) ~
12708+ =/ eligible=?
12709+ ?& ?=(~ imports.p.parsed)
12710+ ?=(~ jimports)
12711+ ?=(~ prelude)
12712+ ?=(~ prelude-values)
12713+ ?=(~ reserved-molds)
12714+ !?=([%ui %api *] file)
12715+ !?=([%ui %stores *] file)
12716+ !(lien (global-value-names ds) |=(n=term =(n %main)))
12717+ (module-scope-valid p.parsed ~ ~)
12718+ !(module-values-complete ds env)
12719+ (lte (met 3 src) 65.536)
12720+ (lte (lent ds) 64)
12721+ (dg-source-candidate ds 64)
12722+ ==
12723+ =/ transaction=(unit dgcommit) ?:(eligible (dg-root-source file src) ~)
12724+ =. recovered
12725+ ?~ transaction ~
12726+ ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
12727+ (turn (skim env.u.transaction |=(entry=[name=term scheme=ischeme] ?=(~ (ienv-lookup name.entry env)))) |=(entry=[name=term scheme=ischeme] name.entry))
12728+ =. env
12729+ ?~ transaction env
12730+ ?: &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) env.u.transaction
12731+ env
12732+ =/ source-defs=(map term def) (direct-checked-gates ds env)
12733+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1016612734 =/ lines=(list @t) ~
1016712735 |-
1016812736 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -10175,6 +12743,16 @@
1017512743 ?^ cycle
1017612744 =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
1017712745 $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
12746+ ?: (lien recovered |=(n=term =(n name.d)))
12747+ =/ found=(unit ischeme) (ienv-lookup name.d env)
12748+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: committed definition unavailable") lines])
12749+ ?: (itype-has-hidden-recursive typ.u.found)
12750+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
12751+ ?: (itype-has-hidden-generic typ.u.found)
12752+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
12753+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
12754+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
12755+ $(ds t.ds, lines [line lines])
1017812756 ?: (lien grouped.resolution |=(n=term =(n name.d)))
1017912757 =/ found=(unit ischeme) (ienv-lookup name.d env)
1018012758 ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
@@ -10182,7 +12760,9 @@
1018212760 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
1018312761 $(ds t.ds, lines [line lines])
1018412762 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10185− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256]
12763+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
12764+ =. gate-defs.initial source-defs
12765+ =. head-evidence.initial heads
1018612766 =. initial (reserve-def-caps val.d initial)
1018712767 =/ result=iresult
1018812768 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -10190,6 +12770,7 @@
1019012770 (infer-fragment val.d env initial)
1019112771 ?: ?=(%| -.result)
1019212772 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
12773+ =. state.p.result (promote-restricted-numbers state.p.result env)
1019312774 =. 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)))
1019412775 =/ hole=(unit idiag) (unresolved-hole holes.state.p.result holes.initial state.p.result)
1019512776 ?^ hole
@@ -10216,7 +12797,576 @@
1021612797 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
1021712798 ?: (gth (lent vars) 26)
1021812799 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
12800+ ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
12801+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
1021912802 =/ printable=itype (canonical-itype typ vars)
1022012803 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
1022112804 $(ds t.ds, lines [line lines])
12805+:: Experimental module-owned pending-constraint generalization only.
12806+:: Inputs, IDs and substitution come from one checker-owned transaction.
12807++$ dgscan [ids=(list @ud) fuel=@ud]
12808+++ dg-scan
12809+ |= [todo=(list itype) sub=isub fuel=@ud ids=(list @ud)]
12810+ ^- (unit dgscan)
12811+ ?~ todo `[ids fuel]
12812+ ?: =(0 fuel) ~
12813+ =. fuel (dec fuel)
12814+ =/ t=itype i.todo
12815+ ?: ?=(?(%var %avar %rvar %nvar %rnvar %tag) -.t)
12816+ =/ node-id=@ud ?:(?=(%tag -.t) id.t +.t)
12817+ =/ found=(unit itype) (itype-lookup node-id sub)
12818+ ?~ found $(todo t.todo, ids [node-id ids])
12819+ ?: &(?=(?(%rvar %rnvar) -.u.found) =(node-id +.u.found))
12820+ $(todo t.todo, ids [node-id ids])
12821+ $(todo [u.found t.todo])
12822+ ?: ?=(%jrec -.t) $(todo t.todo)
12823+ ?+ -.t ~
12824+ %collection $(todo (weld args.t t.todo))
12825+ %union $(todo (weld args.t (weld cases.t t.todo)))
12826+ %face $(todo [body.t t.todo])
12827+ %fn $(todo [sample.t product.t t.todo])
12828+ %cell $(todo [hed.t tal.t t.todo])
12829+ %atom $(todo t.todo)
12830+ %any-atom $(todo t.todo)
12831+ %flag $(todo t.todo)
12832+ %noun $(todo t.todo)
12833+ %empty $(todo t.todo)
12834+ %const $(todo t.todo)
12835+ ==
12836+::
12837+++ dg-scan-ids
12838+ |= [ids=(list @ud) sub=isub fuel=@ud blocked=(list @ud)]
12839+ ^- (unit dgscan)
12840+ ?~ ids `[blocked fuel]
12841+ =/ one=(unit dgscan) (dg-scan ~[[%var i.ids]] sub fuel blocked)
12842+ ?~ one ~
12843+ $(ids t.ids, fuel fuel.u.one, blocked ids.u.one)
12844+::
12845+++ dg-env
12846+ |= [env=ienv sub=isub fuel=@ud blocked=(list @ud)]
12847+ ^- (unit dgscan)
12848+ ?~ env `[blocked fuel]
12849+ =/ sc=ischeme scheme.i.env
12850+ :: Quantifiers are local to the scheme: first find raw free IDs, then
12851+ :: follow those IDs in the module substitution without capturing them.
12852+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ fuel ~)
12853+ ?~ raw ~
12854+ =/ free=(list @ud) (skim ids.u.raw |=(n=@ud !(lien vars.sc |=(q=@ud =(q n)))))
12855+ =/ resolved=(unit dgscan) (dg-scan-ids free sub fuel.u.raw blocked)
12856+ ?~ resolved ~
12857+ $(env t.env, fuel fuel.u.resolved, blocked ids.u.resolved)
12858+::
12859+++ dg-obligations
12860+ |= [pending=(list dgo) sub=isub fuel=@ud blocked=(list @ud)]
12861+ ^- (unit dgscan)
12862+ ?~ pending `[blocked fuel]
12863+ =/ found=(unit dgscan) (dg-scan ~[left.i.pending right.i.pending] sub fuel blocked)
12864+ ?~ found ~
12865+ $(pending t.pending, fuel fuel.u.found, blocked ids.u.found)
12866+::
12867+++ dg-tags
12868+ |= [tags=(list ipending) sub=isub fuel=@ud blocked=(list @ud)]
12869+ ^- (unit dgscan)
12870+ ?~ tags `[blocked fuel]
12871+ ?: =(0 fuel) ~
12872+ =/ found=(unit itype) (itype-lookup id.i.tags sub)
12873+ ?~ found $(tags t.tags, fuel (dec fuel), blocked [id.i.tags blocked])
12874+ :: Until this entry is explicitly discharged, retain variables reachable
12875+ :: through its binding; mere existence of a substitution is not proof.
12876+ =/ reached=(unit dgscan) (dg-scan ~[u.found] sub (dec fuel) blocked)
12877+ ?~ reached ~
12878+ $(tags t.tags, fuel fuel.u.reached, blocked ids.u.reached)
12879+::
12880+++ dg-generalize
12881+ |= [typ=itype env=ienv pending=(list dgo) tags=(list ipending) captured=(list @ud) state=istate fuel=@ud]
12882+ ^- (unit ischeme)
12883+ :: Bound the obligation list and all graph/substitution walks. The
12884+ :: substitution is assumed checker-owned and occurs-checked.
12885+ ?: (gth (lent pending) 64) ~
12886+ =/ capt=(unit dgscan) (dg-scan-ids captured sub.state fuel ~)
12887+ ?~ capt ~
12888+ =/ env-free=(unit dgscan) (dg-env env sub.state fuel.u.capt ids.u.capt)
12889+ ?~ env-free ~
12890+ =/ obligations=(unit dgscan) (dg-obligations pending sub.state fuel.u.env-free ids.u.env-free)
12891+ ?~ obligations ~
12892+ =/ tagged=(unit dgscan) (dg-tags tags sub.state fuel.u.obligations ids.u.obligations)
12893+ ?~ tagged ~
12894+ =/ bounded=(unit dgscan) (dg-scan ~[typ] sub.state fuel.u.tagged ~)
12895+ ?~ bounded ~
12896+ =/ normalized=itype (itype-normalize typ sub.state)
12897+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
12898+ =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
12899+ `[[normalized quantified]]
12900+::
12901++$ dgcommit [env=ienv state=istate]
12902+:: A branch literal must not acquire a value face through replay.
12903+++ dg-literal-target-safe
12904+ |= target=itype
12905+ ^- ?
12906+ ?: ?=(%union -.target)
12907+ (levy cases.target |=(c=itype ?=(?(%const %cell) -.c)))
12908+ ?=(?(%const %atom %any-atom %flag %noun) -.target)
12909+::
12910+++ dg-replay-edges
12911+ |= [edges=(list dgo) state=istate fuel=@ud]
12912+ ^- (unit istate)
12913+ ?~ edges `state
12914+ ?: =(0 fuel) ~
12915+ =/ trial=ifit (itype-fit left.i.edges right.i.edges sub.state next.state)
12916+ ?. ?=(%ok -.trial) ~
12917+ =/ valid=?
12918+ ?: ?=(%tag -.left.i.edges)
12919+ ?. constructor.left.i.edges
12920+ =/ closed=(unit dgscan) (dg-scan ~[right.i.edges] sub.trial 512 ~)
12921+ ?~ closed |
12922+ ?^ ids.u.closed |
12923+ (dg-literal-target-safe (itype-normalize right.i.edges sub.trial))
12924+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
12925+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
12926+ ?. valid ~
12927+ $(edges t.edges, state state(sub sub.trial, next next.trial), fuel (dec fuel))
12928+::
12929+++ dg-close-env
12930+ |= [env=ienv sub=isub fuel=@ud]
12931+ ^- (unit ienv)
12932+ ?~ env `~
12933+ ?: =(0 fuel) ~
12934+ =/ s=ischeme scheme.i.env
12935+ :: Quantified IDs are scheme-local and cannot be rewritten on publication.
12936+ ?. (levy vars.s |=(n=@ud ?=(~ (itype-lookup n sub)))) ~
12937+ =/ bounded=(unit dgscan) (dg-scan ~[typ.s] sub (dec fuel) ~)
12938+ ?~ bounded ~
12939+ =/ normalized=itype (itype-normalize typ.s sub)
12940+ ?: (itype-has-tag normalized) ~
12941+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
12942+ ?. (levy vars |=(n=@ud (lien vars.s |=(v=@ud =(v n))))) ~
12943+ =/ rest=(unit ienv) (dg-close-env t.env sub fuel.u.bounded)
12944+ ?~ rest ~
12945+ `[[name.i.env [normalized vars.s]] u.rest]
12946+::
12947+:: A deferred boolean branch has exactly the two literal flag patterns.
12948+:: Arms are inferred in order. Equal types are retained; two direct pending
12949+:: literals may instead retain source-owned obligations for later context.
12950+++ dg-boolean-patterns
12951+ |= e=expr
12952+ ^- ?
12953+ ?. ?=(%branch -.e) |
12954+ ?~ arms.e |
12955+ ?~ t.arms.e |
12956+ ?^ t.t.arms.e |
12957+ =/ x=arm i.arms.e
12958+ =/ y=arm i.t.arms.e
12959+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) |
12960+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) |
12961+ !=(val.lit.pat.x val.lit.pat.y)
12962+:: Only a direct source literal which created its own unbound pending tag
12963+:: may create a branch edge. The caller must retain the exact source and state.
12964+++ dg-owned-arm-literal
12965+ |= [e=expr t=itype tags=(list ipending) sub=isub initial=@ud]
12966+ ^- ?
12967+ ?. ?=(%lit -.e) |
12968+ ?. ?=(%tag -.t) |
12969+ ?: constructor.t |
12970+ ?. =(lit.e literal.t) |
12971+ ?: (lth id.t initial) |
12972+ ?^ (itype-lookup id.t sub) |
12973+ (lien tags |=(x=ipending &(=(id.x id.t) =(literal.x literal.t))))
12974+++ dg-boolean-branch
12975+ |= [e=expr env=ienv state=istate]
12976+ ^- iresult
12977+ ?. (dg-boolean-patterns e) [%| ["deferred branch patterns need unsupported inference" ~]]
12978+ ?> ?=(%branch -.e)
12979+ ?> ?=(^ arms.e)
12980+ ?> ?=(^ t.arms.e)
12981+ =/ x=arm i.arms.e
12982+ =/ y=arm i.t.arms.e
12983+ =/ subject=iresult (infer-fragment subject.e env state)
12984+ ?: ?=(%| -.subject) subject
12985+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
12986+ ?~ su [%| ["deferred branch subject does not unify with ?" ~]]
12987+ =/ left=iresult (infer-fragment val.x env state.p.subject(sub u.su))
12988+ ?: ?=(%| -.left) left
12989+ =/ right=iresult (infer-fragment val.y env state.p.left)
12990+ ?: ?=(%| -.right) right
12991+ ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)
12992+ =/ st=istate state.p.right
12993+ ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)
12994+ [%| ["deferred branch arm context needs unsupported inference" ~]]
12995+ ?. (dg-owned-arm-literal val.y typ.p.right tags.st sub.st next.state)
12996+ [%| ["deferred branch arm context needs unsupported inference" ~]]
12997+ ?> ?=(%tag -.typ.p.left)
12998+ ?> ?=(%tag -.typ.p.right)
12999+ ?: =(id.typ.p.left id.typ.p.right)
13000+ [%| ["deferred branch arm context needs unsupported inference" ~]]
13001+ ?: (gth (lent obligations.st) 62)
13002+ [%| ["deferred branch arm context needs unsupported inference" ~]]
13003+ =/ result=itype [%var next.st]
13004+ =/ ex=dgo [typ.p.left result (span-of val.x) (span-of e)]
13005+ =/ ey=dgo [typ.p.right result (span-of val.y) (span-of e)]
13006+ [%& result st(next +(next.st), obligations [ex ey obligations.st])]
13007+ [%& typ.p.left state.p.right]
13008+::
13009+:: Deferred inference uses only source forms whose successful fit sites are
13010+:: guarded below; a shared source-node budget bounds this screen.
13011+++ dg-safe-expressions
13012+ |= [todo=(list expr) fuel=@ud]
13013+ ^- (unit @ud)
13014+ ?~ todo `fuel
13015+ =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
13016+ ?~ first ~
13017+ $(todo t.todo, fuel u.first)
13018+++ dg-safe-expression
13019+ |= [e=expr fuel=@ud]
13020+ ^- (unit @ud)
13021+ ?: =(0 fuel) ~
13022+ =. fuel (dec fuel)
13023+ ?+ -.e ~
13024+ ?(%lit %ctor) `fuel
13025+ %wing ?:(?=([@ ~] names.e) `fuel ~)
13026+ %str
13027+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) ~
13028+ `fuel
13029+ %group $(e inner.e, fuel fuel)
13030+ %body
13031+ ?^ defs.e ~
13032+ $(e final.e, fuel fuel)
13033+ %gate $(e body.e, fuel fuel)
13034+ %gate-wide $(e body.e, fuel fuel)
13035+ %branch
13036+ ?. (dg-boolean-patterns e) ~
13037+ ?> ?=(^ arms.e)
13038+ ?> ?=(^ t.arms.e)
13039+ =/ subject=(unit @ud) $(e subject.e, fuel fuel)
13040+ ?~ subject ~
13041+ (dg-safe-expressions ~[val.i.arms.e val.i.t.arms.e] u.subject)
13042+ %cast $(e val.e, fuel fuel)
13043+ %call
13044+ =/ head=(unit @ud) $(e head.e, fuel fuel)
13045+ ?~ head ~
13046+ (dg-safe-expressions args.e u.head)
13047+ ==
13048+:: Exact normalized equality is preserved by all later substitutions.
13049+:: The bounded scan declines opaque types and oversized inputs.
13050+++ dg-stable-fit
13051+ |= [actual=itype expected=itype sub=isub]
13052+ ^- ?
13053+ ?~ (dg-scan ~[actual expected] sub 512 ~) |
13054+ =((itype-normalize actual sub) (itype-normalize expected sub))
13055+::
13056+:: A positional call peels sample-slot faces during its separate face check.
13057+:: Require its argument, sample and result closed so that check stays valid.
13058+++ dg-stable-call-fit
13059+ |= [actual=itype expected=itype product=itype sub=isub positional=?]
13060+ ^- ?
13061+ =/ checked=(unit dgscan) (dg-scan ~[actual expected product] sub 512 ~)
13062+ ?~ checked |
13063+ ?: &(positional ?=(^ ids.u.checked)) |
13064+ =((itype-normalize actual sub) (itype-normalize expected sub))
13065+::
13066+:: One definition attempt retains state only when inference succeeds.
13067++$ dg-step [env=ienv state=istate pending=(list dgo)]
13068+++ dg-stage-one
13069+ |= [d=def env=ienv state=istate]
13070+ ^- (unit dg-step)
13071+ ?> ?=(%value -.d)
13072+ ?~ (dg-safe-expression val.d 512) ~
13073+ =/ local=istate (reserve-def-caps val.d state)
13074+ :: This first slice declines all written capitals and holes/projections.
13075+ ?^ caps.local ~
13076+ =/ ordinary=iresult (infer-fragment val.d env local)
13077+ ?: ?=(%| -.ordinary) ~
13078+ =/ typ=itype typ.p.ordinary
13079+ =/ after=istate state.p.ordinary
13080+ =/ edges=(list dgo) obligations.after
13081+ ?. =(binders.after binders.state) ~
13082+ ?. =(molds.after molds.state) ~
13083+ ?. =(globals.after globals.state) ~
13084+ ?. =(externals.after externals.state) ~
13085+ ?. =(surs.after surs.state) ~
13086+ ?. =(mark-externals.after mark-externals.state) ~
13087+ ?. =(marks.after marks.state) ~
13088+ ?. =(jimports.after jimports.state) ~
13089+ ?. =(reserved-molds.after reserved-molds.state) ~
13090+ ?. =(params.after params.state) ~
13091+ ?. =(active.after active.state) ~
13092+ ?. =(in-mold.after in-mold.state) ~
13093+ ?. =(at.after at.state) ~
13094+ ?. =(top-molds.after top-molds.state) ~
13095+ ?. =(prelude.after prelude.state) ~
13096+ ?. =(gate-defs.after gate-defs.state) ~
13097+ ?. =(head-evidence.after head-evidence.state) ~
13098+ ?. =(grec-index.after grec-index.state) ~
13099+ ?. =(defer.after defer.state) ~
13100+ ?. =(holes.after holes.state) ~
13101+ ?. =(caps.after caps.state) ~
13102+ ?. =(projections.after projections.state) ~
13103+ ?: (unsupported-atom-vars (itype-normalize typ sub.after) caps.after binders.after sub.after) ~
13104+ ?: (itype-has-nvar (itype-normalize typ sub.after)) ~
13105+ =/ scheme=(unit ischeme) (dg-generalize typ env edges tags.after ~ after 32.768)
13106+ ?~ scheme ~
13107+ `[[[name.d u.scheme] env] after edges]
13108+:: Retry only definitions that did not infer. Successful definitions are
13109+:: committed into the local transaction, never published until all close.
13110+++ dg-stage
13111+ |= [ds=(list def) base=ienv env=ienv state=istate pending=(list dgo) fuel=@ud]
13112+ ^- (unit dgcommit)
13113+ ?: (gth fuel 64) ~
13114+ ?: (gth (lent ds) fuel) ~
13115+ =/ remaining=(list def) ds
13116+ =/ waiting=(list def) ~
13117+ =/ progress=? |
13118+ =/ attempts=@ud (mul fuel fuel)
13119+ |-
13120+ ?~ remaining
13121+ ?^ waiting
13122+ ?. progress ~
13123+ $(remaining (flop waiting), waiting ~, progress |)
13124+ =/ replayed=(unit istate) (dg-replay-edges pending state 64)
13125+ ?~ replayed ~
13126+ ?: (pending-tags tags.u.replayed sub.u.replayed) ~
13127+ =/ closed-edges=(unit dgscan) (dg-obligations pending sub.u.replayed 32.768 ~)
13128+ ?~ closed-edges ~
13129+ ?^ ids.u.closed-edges ~
13130+ =/ rechecked=(unit istate) (dg-replay-edges pending u.replayed 64)
13131+ ?~ rechecked ~
13132+ ?. =(sub.u.rechecked sub.u.replayed) ~
13133+ ?. =(next.u.rechecked next.u.replayed) ~
13134+ =/ closed=(unit ienv) (dg-close-env env sub.u.replayed 32.768)
13135+ ?~ closed ~
13136+ `[[u.closed u.replayed(defer ~, obligations ~)]]
13137+ ?: =(0 attempts) ~
13138+ =. attempts (dec attempts)
13139+ =/ d=def i.remaining
13140+ ?: ?=(%mold -.d) $(remaining t.remaining)
13141+ ?^ (ienv-lookup name.d base) $(remaining t.remaining)
13142+ ?^ (ienv-lookup name.d env) ~
13143+ =/ done=(unit dg-step) (dg-stage-one d env state)
13144+ ?~ done $(remaining t.remaining, waiting [d waiting])
13145+ $(remaining t.remaining, env env.u.done, state state.u.done, pending pending.u.done, progress &)
13146+::
13147+:: Cheap bounded eligibility check on the already parsed source. This
13148+:: deliberately covers only direct constructor calls beneath transparent
13149+:: groups, gates, casts and definition-free bodies. Other shapes decline
13150+:: this fallback without a second parse or resolution pass.
13151+++ dg-direct-source
13152+ |= [e=expr fuel=@ud]
13153+ ^- ?
13154+ ?: =(0 fuel) |
13155+ ?+ -.e |
13156+ %group $(e inner.e, fuel (dec fuel))
13157+ %gate $(e body.e, fuel (dec fuel))
13158+ %gate-wide $(e body.e, fuel (dec fuel))
13159+ %cast $(e val.e, fuel (dec fuel))
13160+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
13161+ %call
13162+ ?. ?=([* ~] args.e) |
13163+ ?=(%ctor -.i.args.e)
13164+ ==
13165+++ dg-source-candidate
13166+ |= [ds=(list def) fuel=@ud]
13167+ ^- ?
13168+ ?~ ds |
13169+ ?: =(0 fuel) |
13170+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
13171+ ?: (dg-direct-source val.i.ds 64) &
13172+ $(ds t.ds, fuel (dec fuel))
13173+::
13174+++ dg-interface-safe
13175+ |= [env=ienv]
13176+ ^- ?
13177+ ?~ env &
13178+ =/ sc=ischeme scheme.i.env
13179+ ?: |((itype-has-hidden-recursive typ.sc) (itype-has-hidden-generic typ.sc)) |
13180+ ?: (gth (lent vars.sc) 26) |
13181+ $(env t.env)
13182+:: Parse status and the transaction result come from the same source parse.
13183++$ dgparse [parsed=? result=(unit dgcommit)]
13184+++ dg-root-source
13185+ |= [at=path src=@t]
13186+ ^- (unit dgcommit)
13187+ result:(dg-root-detail at src)
13188+++ dg-root-detail
13189+ |= [at=path src=@t]
13190+ ^- dgparse
13191+ =/ parsed (parse at src)
13192+ ?: ?=(%| -.parsed) [| ~]
13193+ =/ transact
13194+ |.
13195+ ?^ imports.p.parsed ~
13196+ ?. (module-scope-valid p.parsed ~ ~) ~
13197+ ?^ (duplicate-defs defs.p.parsed) ~
13198+ =/ defs=(list def) defs.p.parsed
13199+ ?: (gth (lent defs) 64) ~
13200+ =/ molds=imolds (collect-simple-molds defs)
13201+ =/ globals=(list term) (global-value-names defs)
13202+ =/ resolution=iresolved (resolve-groups defs molds globals ~ ~ ~ ~ ~ ~ at ~)
13203+ ?^ grouped.resolution ~
13204+ ?^ artifacts.resolution ~
13205+ =/ base=ienv env.resolution
13206+ =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)
13207+ ?~ free ~
13208+ ?^ ids.u.free ~
13209+ =/ all=(unit dgscan) (dg-all-env-ids base 32.768 ~)
13210+ ?~ all ~
13211+ =/ fresh=@ud (dg-next-id ids.u.all 0)
13212+ =/ st=istate *istate
13213+ =. st st(next fresh, defer `~, molds molds, globals globals, at at, top-molds (turn molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
13214+ =/ checked-molds=(each imold-types @t) (module-mold-types molds st)
13215+ ?: ?=(%| -.checked-molds) ~
13216+ (dg-stage defs base base st ~ 64)
13217+ ::
13218+ [& (transact)]
13219+++ dg-all-env-ids
13220+ |= [env=ienv fuel=@ud ids=(list @ud)]
13221+ ^- (unit dgscan)
13222+ ?~ env `[ids fuel]
13223+ ?: =(0 fuel) ~
13224+ =/ sc=ischeme scheme.i.env
13225+ ?: (itype-has-tag typ.sc) ~
13226+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ (dec fuel) ids)
13227+ ?~ raw ~
13228+ =/ quant=(unit dgscan) (dg-scan-ids vars.sc ~ fuel.u.raw ids.u.raw)
13229+ ?~ quant ~
13230+ $(env t.env, fuel fuel.u.quant, ids ids.u.quant)
13231+::
13232+++ dg-next-id
13233+ |= [ids=(list @ud) largest=@ud]
13234+ ^- @ud
13235+ ?~ ids +(largest)
13236+ $(ids t.ids, largest (max largest i.ids))
13237+::
13238+++ dg-eligible-ctor
13239+ |= [e=expr head=itype actual=itype expected=itype state=istate]
13240+ ^- (unit dgo)
13241+ ?. ?=(%call -.e) ~
13242+ ?. ?=([* ~] args.e) ~
13243+ ?. ?=(%ctor -.i.args.e) ~
13244+ ?. ?=(%fn -.head) ~
13245+ ?. ?=(%fn -.expected) ~
13246+ ?. ?=(%tag -.actual) ~
13247+ ?. constructor.actual ~
13248+ ?. ?=(%var -.product.expected) ~
13249+ ?^ (itype-lookup id.product.expected sub.state) ~
13250+ =/ bounded=(unit dgscan) (dg-scan ~[sample.expected] sub.state 256 ~)
13251+ ?~ bounded ~
13252+ ?^ ids.u.bounded ~
13253+ `[[actual expected (span-of i.args.e) (span-of head.e)]]
13254+::
13255+:: Experimental per-module, source-derived recursive tree index.
13256+:: The two tags and the exact children/list/self layout are fixed-shape
13257+:: checks, so ordinary definitions incur no type-tree or source scans.
13258+++ grec-tagged-fields
13259+ |= sh=shape
13260+ ^- (unit [tag=@ fields=(list field)])
13261+ ?. ?=(%cell -.sh) ~
13262+ ?~ fields.sh ~
13263+ =/ head=field i.fields.sh
13264+ ?. ?=(%bare -.head) ~
13265+ ?. ?=(%const -.shape.head) ~
13266+ ?. &(?=(%term form.lit.shape.head) =(%tas aura.lit.shape.head)) ~
13267+ `[val.lit.shape.head t.fields.sh]
13268+++ grec-tree-children
13269+ |= [fs=(list field) param=@t]
13270+ ^- (unit field)
13271+ ?~ fs ~
13272+ ?~ t.fs `i.fs
13273+ ?^ t.t.fs ~
13274+ =/ event=field i.fs
13275+ =/ kids=field i.t.fs
13276+ ?. &(?=(%face -.event) ?=(%face -.kids)) ~
13277+ ?. !=(name.event name.kids) ~
13278+ ?. ?=(%fn -.shape.event) ~
13279+ ?. ?=(%aura -.sample.shape.event) ~
13280+ ?. =(%t aura.sample.shape.event) ~
13281+ ?. ?=(%tvar -.product.shape.event) ~
13282+ ?. =(param name.product.shape.event) ~
13283+ `kids
13284+::
13285+++ grec-tree-proof
13286+ |= [name=term sh=shape]
13287+ ^- ?
13288+ ?. ?=(%generic -.sh) |
13289+ ?. ?=([@ ~] vars.sh) |
13290+ =/ param=@t i.vars.sh
13291+ ?. ?=(%union -.body.sh) |
13292+ ?. ?=([* [* ~]] cases.body.sh) |
13293+ =/ a=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.cases.body.sh)
13294+ =/ b=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.t.cases.body.sh)
13295+ ?~ a |
13296+ ?~ b |
13297+ ?. !=(tag.u.a tag.u.b) |
13298+ ?. ?=([* ~] fields.u.a) |
13299+ =/ value=field i.fields.u.a
13300+ ?. ?=(%face -.value) |
13301+ ?. ?=(%aura -.shape.value) |
13302+ ?. =(%t aura.shape.value) |
13303+ =/ selected=(unit field) (grec-tree-children fields.u.b param)
13304+ ?~ selected |
13305+ =/ kids=field u.selected
13306+ ?. ?=(%face -.kids) |
13307+ ?. ?=(%apply -.shape.kids) |
13308+ ?. =(ref.shape.kids ~[%list]) |
13309+ ?. ?=([* ~] args.shape.kids) |
13310+ =/ self=shape i.args.shape.kids
13311+ ?. ?=(%apply -.self) |
13312+ ?. =(ref.self ~[name]) |
13313+ ?. ?=([* ~] args.self) |
13314+ ?. ?=(%tvar -.i.args.self) |
13315+ =(name.i.args.self param)
13316++$ grec-collected [molds=imolds proofs=(map term shape)]
13317+:: Experimental one-layer analysis view, never an exported mold identity.
13318+++ grec-unfold-view
13319+ |= [typ=itype fuel=@ud]
13320+ ^- (unit [view=itype left=@ud])
13321+ ?. ?=(%grec -.typ) ~
13322+ ?: =(fuel 0) ~
13323+ ?. ?=([* ~] args.typ) ~
13324+ =/ sh=shape proof.typ
13325+ ?. (grec-tree-proof name.typ sh) ~
13326+ ?> ?=(%generic -.sh)
13327+ ?> ?=([@ ~] vars.sh)
13328+ ?> ?=(%union -.body.sh)
13329+ ?> ?=([* [* ~]] cases.body.sh)
13330+ =/ ca=shape i.cases.body.sh
13331+ =/ cb=shape i.t.cases.body.sh
13332+ ?> ?=(%cell -.ca)
13333+ ?> ?=(%cell -.cb)
13334+ ?> ?=([* [* ~]] fields.ca)
13335+ ?> ?=([* *] fields.cb)
13336+ =/ tag-a=field i.fields.ca
13337+ =/ tag-b=field i.fields.cb
13338+ ?> ?=(%bare -.tag-a)
13339+ ?> ?=(%bare -.tag-b)
13340+ ?> ?=(%const -.shape.tag-a)
13341+ ?> ?=(%const -.shape.tag-b)
13342+ =/ text-field=field i.t.fields.ca
13343+ ?> ?=(%face -.text-field)
13344+ =/ branch=(list field) t.fields.cb
13345+ =/ kids=(unit field) (grec-tree-children branch i.vars.sh)
13346+ ?~ kids ~
13347+ ?> ?=(%face -.u.kids)
13348+ =/ children=itype [%face name.u.kids [%collection %list ~[typ]]]
13349+ ?> ?=(^ branch)
13350+ =/ payload=itype
13351+ ?~ t.branch children
13352+ =/ event=field i.branch
13353+ ?> ?=(%face -.event)
13354+ [%cell [%face name.event [%fn [%atom %t] i.args.typ]] children]
13355+ =/ leaf=itype [%cell [%const lit.shape.tag-a] [%face name.text-field [%atom %t]]]
13356+ =/ node=itype [%cell [%const lit.shape.tag-b] payload]
13357+ `[[%union ~[leaf node] ~ ~ ~] (dec fuel)]
13358+::
13359+++ grec-collect-molds
13360+ |= ds=(list def)
13361+ ^- grec-collected
13362+ ?~ ds [~ *(map term shape)]
13363+ =/ rest=grec-collected $(ds t.ds)
13364+ ?. ?=(%mold -.i.ds) rest
13365+ =/ name=term name.i.ds
13366+ =/ body=shape shape.i.ds
13367+ =/ proofs=(map term shape) proofs.rest
13368+ =? proofs (grec-tree-proof name body) (~(put by proofs) name body)
13369+ [[[name body] molds.rest] proofs]
13370+::
13371+
1022213372--