@@ -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
@@ -4628,6 +4630,32 @@
46284630:: proofs to fewer than 1,024 cells; the projection planner has a separate
46294631:: 4,096-step bound. These are inference limits, not language limits.
46304632::
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+::
46314659+$ itype
46324660 $~ [%var 0]
46334661 $% [%var id=@ud]
@@ -4639,11 +4667,13 @@
46394667 [%any-atom ~]
46404668 [%flag ~]
46414669 [%noun ~]
4670+ [%empty ~]
46424671 [%tag id=@ud literal=lit constructor=?]
46434672 [%const literal=lit]
46444673 [%collection name=term args=(list itype)]
46454674 [%recursive module=term name=term label=(unit @t)]
46464675 [%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)]
46474677 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46484678 [%face name=term body=itype]
46494679 [%fn sample=itype product=itype]
@@ -4696,6 +4726,88 @@
46964726 $(t u.found)
46974727 ==
46984728::
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+::
46994811++ itype-occurs
47004812 |= [n=@ud t=itype sub=isub]
47014813 ^- ?
@@ -4710,11 +4822,13 @@
47104822 %any-atom |
47114823 %flag |
47124824 %noun |
4825+ %empty |
47134826 %tag =(n id.t)
47144827 %const |
47154828 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
47164829 %recursive |
47174830 %jrec |
4831+ %grec (lien args.t |=(c=itype (itype-occurs n c sub)))
47184832 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
47194833 %face $(t body.t)
47204834 %fn |($(t sample.t) $(t product.t))
@@ -4733,6 +4847,9 @@
47334847 =. a (itype-walk a sub)
47344848 =. b (itype-walk b sub)
47354849 ?: =(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)
47364853 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
47374854 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
47384855 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
@@ -4838,11 +4955,13 @@
48384955 %any-atom &
48394956 %flag |
48404957 %noun |
4958+ %empty |
48414959 %tag |
48424960 %const |
48434961 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
48444962 %recursive |
48454963 %jrec |
4964+ %grec (lien args.t |=(c=itype (itype-has-any-atom c sub)))
48464965 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
48474966 %face $(t body.t)
48484967 %fn |($(t sample.t) $(t product.t))
@@ -4912,11 +5031,13 @@
49125031 %any-atom &
49135032 %flag &
49145033 %noun |
5034+ %empty |
49155035 %tag &
49165036 %const &
49175037 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
49185038 %recursive |
49195039 %jrec |
5040+ %grec (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
49205041 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
49215042 %face $(typ body.typ)
49225043 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4945,6 +5066,7 @@
49455066 ^- ?
49465067 =. t (itype-walk t sub)
49475068 ?- -.t
5069+ %grec (lien args.t |=(c=itype (itype-has-face c sub)))
49485070 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
49495071 %face &
49505072 %cell |($(t hed.t) $(t tal.t))
@@ -4952,6 +5074,42 @@
49525074 * |
49535075 ==
49545076::
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+::
49555113++ itype-face-asym-collection-args
49565114 |= [as=(list itype) bs=(list itype) sub=isub]
49575115 ^- ?
@@ -4965,6 +5123,9 @@
49655123 ^- ?
49665124 =. a (itype-walk a sub)
49675125 =. 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)
49685129 ?: &(?=(%collection -.a) ?=(%collection -.b))
49695130 ?. =(name.a name.b) |
49705131 (itype-face-asym-collection-args args.a args.b sub)
@@ -4997,6 +5158,12 @@
49975158:: labels. Ignore one raw sample-slot face per written argument while
49985159:: checking value faces as usual. An unknown or variable-bound cell spine
49995160:: 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+::
50005167++ itype-positional-face-asym
50015168 |= [args=(list expr) actual=itype expected=itype sub=isub]
50025169 ^- ?
@@ -5004,11 +5171,11 @@
50045171 ?~ t.args
50055172 =/ slot=itype expected
50065173 =? slot ?=(%face -.slot) body.slot
5007− (itype-face-asym actual slot sub)
5174+ (itype-positional-slot-face-asym actual slot sub)
50085175 ?. &(?=(%cell -.actual) ?=(%cell -.expected)) &
50095176 =/ slot=itype hed.expected
50105177 =? slot ?=(%face -.slot) body.slot
5011− ?: (itype-face-asym hed.actual slot sub) &
5178+ ?: (itype-positional-slot-face-asym hed.actual slot sub) &
50125179 $(args t.args, actual tal.actual, expected tal.expected)
50135180::
50145181++ itype-output-may-be-cell
@@ -5021,6 +5188,7 @@
50215188 %union &
50225189 %recursive &
50235190 %jrec &
5191+ %grec &
50245192 %noun &
50255193 %collection &
50265194 %face $(t body.t)
@@ -5050,6 +5218,7 @@
50505218 ^- ?
50515219 ?- -.t
50525220 %tag &
5221+ %grec (lien args.t |=(c=itype (itype-has-tag c)))
50535222 %collection (lien args.t |=(c=itype (itype-has-tag c)))
50545223 %face $(t body.t)
50555224 %fn |($(t sample.t) $(t product.t))
@@ -5063,6 +5232,7 @@
50635232 ^- ?
50645233 ?- -.t
50655234 %union &
5235+ %grec (lien args.t |=(c=itype (itype-has-union c)))
50665236 %collection (lien args.t |=(c=itype (itype-has-union c)))
50675237 %face $(t body.t)
50685238 %fn |($(t sample.t) $(t product.t))
@@ -5081,6 +5251,7 @@
50815251 %union
50825252 ?: &(?=(~ label.t) ?=(^ args.t)) &
50835253 (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))))
50845255 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
50855256 %face $(t body.t)
50865257 %fn |($(t sample.t) $(t product.t))
@@ -5094,6 +5265,7 @@
50945265 ?- -.t
50955266 %recursive &
50965267 %jrec &
5268+ %grec &
50975269 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
50985270 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
50995271 %face $(t body.t)
@@ -5108,6 +5280,7 @@
51085280 ?- -.t
51095281 %recursive ?=(~ label.t)
51105282 %jrec ?=(~ label.t)
5283+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-recursive c))))
51115284 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
51125285 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
51135286 %face $(t body.t)
@@ -5135,30 +5308,63 @@
51355308 $(cases t.cases, good `trial)
51365309 ==
51375310::
5138−:: A constructor needs a case with its tag at the head and a payload
5139−:: compatible with the expected gate sample. Other case forms do not
5140−:: 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.
51415314::
51425315++ itype-fit-ctor-cases
51435316 |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
51445317 ^- ifit
51455318 =/ found=(unit ifit) ~
5319+ =/ pending=? |
51465320 |-
5147− ?~ cases ?~(found [%bad ~] u.found)
5148− =/ 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 &)
51495331 ?. ?=(%cell -.c) $(cases t.cases)
5150− =/ 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 &)
51515344 ?. ?=(%const -.head) $(cases t.cases)
5152− ?. =(%term form.literal.head) $(cases t.cases)
51535345 ?. =(val.literal.head val.tag) $(cases t.cases)
5154− ?^ 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.
51555348 =/ trial=ifit (itype-fit sample tal.c sub next)
5156− $(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+ ==
51575356::
51585357++ itype-fit
51595358 |= [actual=itype expected=itype sub=isub next=@ud]
51605359 ^- ifit
5161− (itype-fit-inner actual expected sub next | |)
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
51625368++ itype-fit-inner
51635369 |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
51645370 ^- ifit
@@ -5177,6 +5383,10 @@
51775383 =. actual (itype-walk actual sub)
51785384 =. expected (itype-walk expected sub)
51795385 ?: =(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 ~]
51805390 :: Any value can be used where a noun is expected. An unresolved
51815391 :: bare tag is fixed as a constant; a constructor still needs a gate.
51825392 ?: ?=(%noun -.expected)
@@ -5186,6 +5396,14 @@
51865396 [%ok sub next]
51875397 :: An arbitrary noun is not known to fit a narrower type.
51885398 ?: &(?=(%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 ~]
51895407 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
51905408 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
51915409 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
@@ -5259,6 +5477,10 @@
52595477 ?: ?=(%const -.expected)
52605478 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
52615479 ?: ?=(%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 ~]
52625484 ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
52635485 [%bad ~]
52645486 ?: ?=(%flag -.expected)
@@ -5318,6 +5540,7 @@
53185540 $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
53195541 ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
53205542 ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
5543+ ?: &(!uncertain (itype-closed-gates-match actual expected)) [%ok sub next]
53215544 ?: (itype-face-asym actual expected sub) [%unknown ~]
53225545 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
53235546 [%unknown ~]
@@ -5396,7 +5619,15 @@
53965619+$ iderived [name=term agent=term mark=term]
53975620+$ iwidth-definition [name=term original=expr typ=itype sub=isub projections=(list iwprojection)]
53985621+$ iwidth-dependency [at=path source=(unit @t) definitions=(list iwidth-definition)]
5399−+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t)]
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)]
54005631+$ ijimports (list [face=term interface=ifile])
54015632+$ icap [name=@t id=@ud at=span]
54025633+$ icaps (list icap)
@@ -5499,7 +5730,77 @@
54995730 ?. (width-in-order order.source.shape order.target.shape) ~
55005731 (width-fit-fields index.source.shape order.target.shape sub next)
55015732::
5502−+$ 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)]
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)]
55035804+$ idiag [msg=tape sites=(list [at=span note=tape])]
55045805+$ iresult (each [typ=itype state=istate] idiag)
55055806+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5519,6 +5820,7 @@
55195820 |= [t=itype sub=isub]
55205821 ^- itype
55215822 =. t (itype-walk t sub)
5823+ ?: ?=(%grec -.t) t(args (turn args.t |=(c=itype (itype-normalize c sub))))
55225824 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
55235825 ?: ?=(%union -.t)
55245826 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
@@ -5545,6 +5847,7 @@
55455847 %cell |($(t hed.t) $(t tal.t))
55465848 %recursive |
55475849 %jrec |
5850+ %grec &
55485851 %collection (lien args.t |=(c=itype (itype-has-gate c)))
55495852 %face $(t body.t)
55505853 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5559,6 +5862,7 @@
55595862 %any-atom |
55605863 %flag |
55615864 %noun |
5865+ %empty |
55625866 ==
55635867::
55645868++ default-decimals
@@ -5568,6 +5872,7 @@
55685872 ?- -.t
55695873 %nvar [%atom %ud]
55705874 %rnvar [%atom %ud]
5875+ %grec t(args (turn args.t |=(c=itype (default-decimals c))))
55715876 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
55725877 %face [%face name.t $(t body.t)]
55735878 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5609,6 +5914,7 @@
56095914 %tag |
56105915 %any-atom &
56115916 %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)))
56125918 %collection (levy args.t |=(c=itype (hole-known c state)))
56135919 %face $(t body.t)
56145920 %fn &($(t sample.t) $(t product.t))
@@ -5618,6 +5924,8 @@
56185924++ promote-restricted-numbers
56195925 |= [state=istate env=ienv]
56205926 ^- istate
5927+ :: With no written capitals, there is nothing to promote.
5928+ ?~ caps.state state
56215929 =/ ids=(list @ud) (turn caps.state |=(c=icap id.c))
56225930 =/ free=(list @ud) (free-env-vars env sub.state)
56235931 |-
@@ -5654,6 +5962,7 @@
56545962 ?- -.t
56555963 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
56565964 %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)))
56575966 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
56585967 %face $(t body.t)
56595968 %fn |($(t sample.t) $(t product.t))
@@ -5685,11 +5994,13 @@
56855994 %any-atom ~
56865995 %flag ~
56875996 %noun ~
5997+ %empty ~
56885998 %tag ~
56895999 %const ~
56906000 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
56916001 %recursive ~
56926002 %jrec ~
6003+ %grec (zing (turn args.t |=(c=itype (itype-vars c))))
56936004 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
56946005 %face $(t body.t)
56956006 %fn (weld $(t sample.t) $(t product.t))
@@ -5733,11 +6044,13 @@
57336044 %any-atom t
57346045 %flag t
57356046 %noun t
6047+ %empty t
57366048 %tag t
57376049 %const t
57386050 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
57396051 %recursive t
57406052 %jrec t
6053+ %grec t(args (turn args.t |=(c=itype (itype-rename c ren))))
57416054 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
57426055 %face [%face name.t $(t body.t)]
57436056 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5760,11 +6073,13 @@
57606073 %any-atom |
57616074 %flag |
57626075 %noun |
6076+ %empty |
57636077 %tag |
57646078 %const |
57656079 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
57666080 %recursive |
57676081 %jrec |
6082+ %grec (lien args.t |=(c=itype (itype-var-is-atom n c)))
57686083 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
57696084 %face $(t body.t)
57706085 %fn |($(t sample.t) $(t product.t))
@@ -5783,11 +6098,13 @@
57836098 %any-atom |
57846099 %flag |
57856100 %noun |
6101+ %empty |
57866102 %tag |
57876103 %const |
57886104 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
57896105 %recursive |
57906106 %jrec |
6107+ %grec (lien args.t |=(c=itype (itype-var-is-restricted n c)))
57916108 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
57926109 %face $(t body.t)
57936110 %fn |($(t sample.t) $(t product.t))
@@ -6084,6 +6401,7 @@
60846401 ^- upat
60856402 ?- -.typ
60866403 %noun [%all ~]
6404+ %empty [%empty ~]
60876405 %atom [%atom ~]
60886406 %flag [%or ~[[%atom `0] [%atom `1]]]
60896407 %const [%atom `val.literal.typ]
@@ -6218,6 +6536,16 @@
62186536 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
62196537 $(molds t.molds)
62206538::
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+::
62216549++ itype-in-import
62226550 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
62236551 ^- itype
@@ -6237,6 +6565,11 @@
62376565 `(crip "{(trip u.alias)}.{(trip face)}")
62386566 [%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)))]
62396567 %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))))
62406573 %jrec
62416574 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
62426575 ?^ public t(label `u.public)
@@ -6349,9 +6682,29 @@
63496682 ?. =(names.tail ~[name]) ~
63506683 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
63516684::
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+
63526701++ infer-mold-template
63536702 |= [sh=shape state=istate]
63546703 ^- (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))]
63556708 =/ direct=(unit itype)
63566709 ?. ?=([@ ~] active.state) ~
63576710 (simple-source-recursive i.active.state sh state)
@@ -6409,7 +6762,7 @@
64096762 ?~ found ~
64106763 ?^ t.found ~
64116764 result.i.found
6412− ?. ?=([%invalid ?(%aura %core) @] raw) ~
6765+ ?. ?=([%invalid ?(%aura %core %overlap) @] raw) ~
64136766 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
64146767::
64156768:: Replay only the shape branches whose evaluation order we can prove.
@@ -6484,12 +6837,18 @@
64846837 `[[%atom aura.sh] state]
64856838 %flag `[[%flag ~] state]
64866839 %noun `[[%noun ~] state]
6840+ %void `[[%empty ~] state]
64876841 %const
6488− ?. |(=(%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))) ~
64896844 `[[%const lit.sh] state]
64906845 %union
64916846 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6492− ?. (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 ~
64936852 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
64946853 ?~ cs ~
64956854 `[[%union types.u.cs ~ ~ ~] state.u.cs]
@@ -6563,6 +6922,8 @@
65636922 ?~ applied ~
65646923 `[u.applied state.u.args]
65656924 ?. ?=(%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]
65666927 ?. (distinct-params vars.u.found) ~
65676928 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
65686929 ?~ params ~
@@ -6891,6 +7252,7 @@
68917252 =/ retried=? ?=(%| -.inferred)
68927253 =? inferred retried (infer-recursive-gate d env local-state)
68937254 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7255+ ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
68947256 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
68957257 =. 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)))
68967258 =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
@@ -7000,6 +7362,8 @@
70007362 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
70017363 (infer-list-context e expected env state context)
70027364 ?: ?=(%branch -.e)
7365+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
7366+ ?^ empty-list u.empty-list
70037367 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
70047368 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
70057369 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -7113,7 +7477,12 @@
71137477 =/ target=itype (itype-walk expected sub.state)
71147478 =/ value=iresult (infer-call-context-arg i.items target env state context)
71157479 ?: ?=(%| -.value) value
7116− =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7480+ =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7481+ =/ fit=ifit
7482+ ?: ?=(%ok -.ordinary-fit) ordinary-fit
7483+ ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7484+ (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7485+ ordinary-fit
71177486 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
71187487 ?: ?=(%bad -.fit)
71197488 ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
@@ -7130,7 +7499,12 @@
71307499 =/ target=itype (itype-walk expected sub.state)
71317500 =/ value=iresult (infer-call-context-arg i.items target env state context)
71327501 ?: ?=(%| -.value) value
7133− =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7502+ =/ ordinary-fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
7503+ =/ fit=ifit
7504+ ?: ?=(%ok -.ordinary-fit) ordinary-fit
7505+ ?: ?&(?=(%union -.target) ?=(^ prelude.state) =(origin.target `[at.u.prelude.state %element]))
7506+ (program-single-generic-fit typ.p.value target sub.state.p.value next.state.p.value)
7507+ ordinary-fit
71347508 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
71357509 ?: ?=(%bad -.fit)
71367510 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
@@ -7217,6 +7591,11 @@
72177591 [%| ["list pattern needs the standard prelude in partial inference" ~]]
72187592 ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
72197593 ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
7594+ =/ item-live=(unit [result=?(%yes %no %unknown) left=@ud])
7595+ (itype-inhabited-proof i.args.typ sub.state caps.state 256)
7596+ ?~ item-live [%| ["list element reachability needs unsupported inference" ~]]
7597+ ?: =(%unknown result.u.item-live) [%| ["list element reachability needs unsupported inference" ~]]
7598+ ?: =(%no result.u.item-live) [%| ["list nonempty pattern is unreachable" ~]]
72207599 ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
72217600 ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
72227601 ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
@@ -7270,6 +7649,11 @@
72707649 [%| ["pattern binder shadows a name" ~]]
72717650 =/ payload=(unit itype) (unit-union-payload typ)
72727651 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
7652+ =/ payload-live=(unit [result=?(%yes %no %unknown) left=@ud])
7653+ (itype-inhabited-proof u.payload sub.state.p.subject caps.state.p.subject 256)
7654+ ?~ payload-live [%| ["unit payload reachability needs unsupported inference" ~]]
7655+ ?: =(%unknown result.u.payload-live) [%| ["unit payload reachability needs unsupported inference" ~]]
7656+ ?: =(%no result.u.payload-live) [%| ["unit present pattern is unreachable" ~]]
72737657 =/ extended=ienv [[u.binder [u.payload ~]] env]
72747658 =/ left=iresult
72757659 ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
@@ -7422,7 +7806,9 @@
74227806 ?: ?=(%| -.subject) `subject
74237807 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
74247808 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7425− =/ cases=(list itype) cases.typ
7809+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7810+ ?~ live ~
7811+ =/ cases=(list itype) u.live
74267812 =/ remaining=(list itype) cases
74277813 =/ arms=(list arm) arms.e
74287814 =/ st=istate state.p.subject
@@ -7459,7 +7845,9 @@
74597845 ?: ?=(%| -.subject) `subject
74607846 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
74617847 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7462− =/ cases=(list itype) cases.typ
7848+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7849+ ?~ live ~
7850+ =/ cases=(list itype) u.live
74637851 =/ remaining=(list itype) cases
74647852 =/ arms=(list arm) arms.e
74657853 =/ st=istate state.p.subject
@@ -7503,7 +7891,9 @@
75037891 ?: ?=(%| -.subject) subject
75047892 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
75057893 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7506− =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7894+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
7895+ ?~ live [%| ["union emptiness needs unsupported inference" ~]]
7896+ =/ expanded=(unit (list ifinite)) (finite-cases u.live ~ 0)
75077897 ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
75087898 =/ cases=(list ifinite) u.expanded
75097899 =/ remaining=(list ifinite) cases
@@ -7624,9 +8014,65 @@
76248014 =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
76258015 [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
76268016::
8017+:: A bounded source-proven tree match permits flat tag patterns and
8018+:: nonbinding catch-alls. Whole-case binders cannot consume the temporary
8019+:: structural view. Pattern count and field arity are checked first.
8020+++ grec-simple-pattern
8021+ |= [pat=pattern view=itype]
8022+ ^- ?
8023+ ?. ?=(%cell -.pat) |
8024+ ?~ items.pat |
8025+ =/ first=pattern i.items.pat
8026+ ?. ?=(%lit -.first) |
8027+ ?. =(%term form.lit.first) |
8028+ =/ chosen=(unit itype) (contextual-tagged-case view val.lit.first ~)
8029+ ?~ chosen |
8030+ ?> ?=(%cell -.u.chosen)
8031+ =/ rest=(list pattern) t.items.pat
8032+ =/ arity=? ?:(?=(%cell -.tal.u.chosen) ?=([* [* ~]] rest) ?=([* ~] rest))
8033+ ?. arity |
8034+ (levy rest |=(p=pattern |(?=(%bind -.p) ?=(%any -.p))))
8035+::
8036+:: A catch-all with no binder is safe even when it covers both cases.
8037+:: A bound whole case still declines to avoid exporting the analysis view.
8038+++ grec-patterns-eligible
8039+ |= [arms=(list arm) view=itype left=@ud]
8040+ ^- ?
8041+ ?~ arms &
8042+ ?: =(0 left) |
8043+ =/ pat=pattern pat.i.arms
8044+ ?. |(?=(%any -.pat) (grec-simple-pattern pat view)) |
8045+ $(arms t.arms, left (dec left))
8046+++ grec-match-view
8047+ |= [e=expr subject=iresult]
8048+ ^- iresult
8049+ ?: ?=(%| -.subject) subject
8050+ ?. ?=(%branch -.e) subject
8051+ ?. (grec-direct-context typ.p.subject sub.state.p.subject) subject
8052+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8053+ ?. ?=(%grec -.typ) subject
8054+ ?~ arms.e subject
8055+ =/ view=(unit [view=itype left=@ud]) (grec-unfold-view typ jrec-fuel.state.p.subject)
8056+ ?~ view [%| ["recursive mold unfolding needs unsupported inference" ~]]
8057+ ?. (grec-patterns-eligible arms.e view.u.view 128) subject
8058+ [%& view.u.view state.p.subject(jrec-fuel left.u.view)]
8059+::
8060+:: A single-arm diagnostic only probes a direct, source-typed in-scope wing;
8061+:: other subjects retain the prior single-pattern inference path.
8062+++ grec-single-wing-subject
8063+ |= [e=expr env=ienv state=istate]
8064+ ^- (unit iresult)
8065+ ?. ?=(%wing -.e) ~
8066+ ?. ?=([@ ~] names.e) ~
8067+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8068+ ?~ scheme ~
8069+ ?. (grec-direct-context typ.u.scheme sub.state) ~
8070+ `(infer-fragment e env state)
8071+::
76278072++ infer-known-union-branch-subject
76288073 |= [e=expr env=ienv subject=iresult]
76298074 ^- iresult
8075+ =. subject (grec-match-view e subject)
76308076 =. subject (jrec-match-view e subject)
76318077 =/ whole=(unit iresult) (infer-known-union-whole e env subject)
76328078 ?~ whole (infer-known-union-finite e env subject ~)
@@ -7641,6 +8087,7 @@
76418087++ infer-known-union-context-subject
76428088 |= [e=expr expected=itype env=ienv subject=iresult context=span]
76438089 ^- iresult
8090+ =. subject (grec-match-view e subject)
76448091 =. subject (jrec-match-view e subject)
76458092 =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
76468093 ?~ whole (infer-known-union-finite e env subject `[expected context])
@@ -7693,9 +8140,67 @@
76938140 =/ subject=iresult (infer-fragment e env state)
76948141 ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
76958142 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7696− ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
8143+ ?. |(?=(%union -.typ) ?=(%jrec -.typ) &(?=(%grec -.typ) (grec-direct-context typ.p.subject sub.state.p.subject))) ~
76978144 `subject
76988145::
8146+:: A direct wing with an already-known union may skip genuinely empty cases
8147+:: when checking a one-arm match. Other subjects keep their existing path.
8148+:: A directly known canonical list of an empty element contains only null.
8149+:: This helper never refines an opaque or variable-bound subject.
8150+++ empty-list-null-branch
8151+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
8152+ ^- (unit iresult)
8153+ ?. ?=(%branch -.e) ~
8154+ ?~ arms.e ~
8155+ ?^ t.arms.e ~
8156+ ?. (unit-empty-pattern pat.i.arms.e) ~
8157+ ?. ?=(%wing -.subject.e) ~
8158+ ?. ?=([@ ~] names.subject.e) ~
8159+ =/ scheme=(unit ischeme) (ienv-lookup i.names.subject.e env)
8160+ ?~ scheme ~
8161+ ?. ?=(%collection -.typ.u.scheme) ~
8162+ ?. =(%list name.typ.u.scheme) ~
8163+ ?~ prelude.state ~
8164+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb) ~
8165+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
8166+ ?~ standard ~
8167+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~
8168+ =/ subject=iresult (infer-fragment subject.e env state)
8169+ ?: ?=(%| -.subject) ~
8170+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8171+ ?. ?=(%collection -.typ) ~
8172+ ?. =(%list name.typ) ~
8173+ ?~ args.typ ~
8174+ ?^ t.args.typ ~
8175+ =/ proof=(unit [empty=? left=@ud]) (itype-empty-proof i.args.typ sub.state.p.subject 256)
8176+ ?~ proof ~
8177+ ?. empty.u.proof ~
8178+ ?~ expected `(infer-fragment val.i.arms.e env state.p.subject)
8179+ =/ body=iresult (infer-call-context-arg val.i.arms.e typ.u.expected env state.p.subject context.u.expected)
8180+ ?: ?=(%| -.body) `body
8181+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
8182+ ?: ?=(%unknown -.fit) `[%| ["single-case branch result constraint is not supported by partial inference" ~]]
8183+ ?: ?=(%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"]]]]
8184+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8185+ `[%| ["single-case branch result needs context in partial inference" ~]]
8186+ `[%& typ.p.body state.p.body(sub sub.fit, next next.fit)]
8187+::
8188+++ known-empty-union-wing
8189+ |= [e=expr env=ienv state=istate]
8190+ ^- (unit iresult)
8191+ ?. ?=(%wing -.e) ~
8192+ ?. ?=([@ ~] names.e) ~
8193+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8194+ ?~ scheme ~
8195+ ?. (contextual-direct-union typ.u.scheme) ~
8196+ =/ subject=iresult (infer-fragment e env state)
8197+ ?: ?=(%| -.subject) ~
8198+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8199+ ?. ?=(%union -.typ) ~
8200+ =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
8201+ ?~ live ~
8202+ ?: =(u.live cases.typ) ~
8203+ `subject
76998204::
77008205:: Infer changes only against a fully known record spine. Retain the
77018206:: target type; unknown spines and repeated edits remain unsupported.
@@ -7940,7 +8445,10 @@
79408445 =/ traced=iresult $(e val.e)
79418446 ?: ?=(%| -.traced) traced
79428447 $(e then.e, state state.p.traced)
7943− %tuple (infer-simple-items items.e env state)
8448+ %tuple
8449+ ?: &(?=(^ defer.state) ?=(^ prelude.state))
8450+ (dg-infer-tuple-items items.e env state)
8451+ (infer-simple-items items.e env state)
79448452 %body
79458453 ?~ defs.e $(e final.e)
79468454 =/ local-names=(list term) (global-value-names defs.e)
@@ -7963,8 +8471,15 @@
79638471 ?: ?=(%| -.result) result
79648472 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
79658473 %branch
8474+ ?^ defer.state (dg-boolean-branch e env state)
79668475 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
79678476 ?~ t.arms.e
8477+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state ~)
8478+ ?^ empty-list u.empty-list
8479+ =/ empty-union=(unit iresult) (known-empty-union-wing subject.e env state)
8480+ ?^ empty-union (infer-known-union-branch-subject e env u.empty-union)
8481+ =/ single=(unit iresult) (grec-single-wing-subject subject.e env state)
8482+ ?^ single (infer-known-union-branch-subject e env u.single)
79688483 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
79698484 (infer-cell-branch e env state ~)
79708485 ?^ t.t.arms.e (infer-known-union-branch e env state)
@@ -8032,6 +8547,8 @@
80328547 =/ 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)
80338548 ?^ nested [%| u.nested]
80348549 [%| ["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)]]]]
8550+ ?: &(?=(^ defer.state.p.value) !(dg-stable-fit typ.p.value typ.u.target sub.fit))
8551+ [%| ["deferred cast fit needs stable inference" ~]]
80358552 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
80368553 [%& merged state.p.value(sub sub.fit, next next.fit)]
80378554 %crash [%& [%var next.state] state(next +(next.state))]
@@ -8081,6 +8598,234 @@
80818598 ?: ?=(%| -.out) [%| p.out]
80828599 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
80838600::
8601+:: Source-bound gate-layout evidence, confined to checked root gate
8602+:: definitions and direct unshadowed prelude calls. The prepared prelude
8603+:: interface and its retained source are trusted as a matching artifact.
8604+:: Layouts identify sample binder faces; they do not change call arity or
8605+:: authorize stripping nested value faces. Unknown origins use ordinary fit.
8606+++ direct-written-gates
8607+ |= [ds=(list def) out=ivisited]
8608+ ^- ivisited
8609+ ?~ ds out
8610+ ?: ?=(%mold -.i.ds) $(ds t.ds)
8611+ ?. |(?=(%gate -.val.i.ds) ?=(%gate-wide -.val.i.ds)) $(ds t.ds)
8612+ $(ds t.ds, out (~(put by out) name.i.ds &))
8613+++ direct-may-use-prelude
8614+ |= [ds=(list def) root=ivisited heads=ivisited]
8615+ ^- ?
8616+ ?~ ds |
8617+ ?: ?=(%mold -.i.ds) $(ds t.ds)
8618+ =/ refs=(list term) (dependency-expr val.i.ds)
8619+ =/ has-root=? (lien refs |=(n=term ?=(^ (~(get by root) n))))
8620+ =/ has-head=? (lien refs |=(n=term ?=(^ (~(get by heads) n))))
8621+ ?: &(has-root has-head) &
8622+ $(ds t.ds)
8623+++ direct-unique-names
8624+ |= [names=(list term) seen=ivisited]
8625+ ^- ?
8626+ ?~ names &
8627+ ?: ?=(^ (~(get by seen) i.names)) |
8628+ $(names t.names, seen (~(put by seen) i.names &))
8629+++ direct-prelude-evidence
8630+ |= [ds=(list def) prelude=(unit ifile)]
8631+ ^- (unit igate-prelude-evidence)
8632+ ?~ prelude ~
8633+ ?~ source.u.prelude ~
8634+ =/ root=ivisited (direct-written-gates ds ~)
8635+ =/ names=(list term) (turn values.u.prelude |=(e=[name=term scheme=ischeme] name.e))
8636+ =/ heads=ivisited (graph-nameset names ~)
8637+ ?. (direct-may-use-prelude ds root heads) ~
8638+ =/ parsed (parse at.u.prelude u.source.u.prelude)
8639+ ?: ?=(%| -.parsed) ~
8640+ ?^ (duplicate-defs defs.p.parsed) ~
8641+ ?. (direct-unique-names (global-value-names defs.p.parsed) ~) ~
8642+ =/ gates=(map term def) (direct-checked-gates defs.p.parsed values.u.prelude)
8643+ `[u.prelude gates]
8644+++ direct-checked-gates
8645+ |= [ds=(list def) env=ienv]
8646+ ^- (map term def)
8647+ =/ names=(list term) (turn env |=(e=[name=term scheme=ischeme] name.e))
8648+ =/ known=ivisited (graph-nameset names ~)
8649+ =/ out=(map term def) ~
8650+ |-
8651+ ?~ ds out
8652+ =/ d=def i.ds
8653+ ?: ?=(%mold -.d) $(ds t.ds)
8654+ ?. ?=(^ (~(get by known) name.d)) $(ds t.ds)
8655+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) $(ds t.ds)
8656+ $(ds t.ds, out (~(put by out) name.d d))
8657+++ direct-find-gate
8658+ |= [n=term ds=(list def)]
8659+ ^- (unit def)
8660+ ?~ ds ~
8661+ ?: &(?=(%value -.i.ds) =(n name.i.ds)) `i.ds
8662+ $(ds t.ds)
8663+++ direct-gate-sample
8664+ |= d=def
8665+ ^- (unit sample)
8666+ ?. ?=(%value -.d) ~
8667+ ?- -.val.d
8668+ %gate `sample.val.d
8669+ %gate-wide `sample.val.d
8670+ * ~
8671+ ==
8672+++ direct-sample-name
8673+ |= sam=sample
8674+ ^- (unit term)
8675+ ?- -.sam
8676+ %bind `name.sam
8677+ %face `name.sam
8678+ %pun `name.sam
8679+ * ~
8680+ ==
8681+++ direct-field-name
8682+ |= f=field
8683+ ^- (unit term)
8684+ ?- -.f
8685+ %face `name.f
8686+ %pun `name.f
8687+ * ~
8688+ ==
8689+++ direct-slot-body
8690+ |= [typ=itype name=(unit term)]
8691+ ^- (unit itype)
8692+ ?~ name `typ
8693+ ?. ?=(%face -.typ) ~
8694+ ?. =(name.typ u.name) ~
8695+ `body.typ
8696+++ direct-invariant
8697+ |= [a=itype b=itype sub=isub next=@ud]
8698+ ^- ifit
8699+ ?: (itype-face-asym a b sub) [%unknown ~]
8700+ =/ forward=ifit (itype-fit a b sub next)
8701+ ?. ?=(%ok -.forward) [%unknown ~]
8702+ ?: (itype-face-asym a b sub.forward) [%unknown ~]
8703+ =/ reverse=ifit (itype-fit b a sub.forward next.forward)
8704+ ?. ?=(%ok -.reverse) [%unknown ~]
8705+ reverse
8706+++ direct-function-fit
8707+ |= [a=itype b=itype sam=sample sh=shape sub=isub next=@ud]
8708+ ^- ifit
8709+ ?. &(?=(%fn -.a) ?=(%fn -.b) ?=(%cell -.sam) ?=(%fn -.sh)) [%unknown ~]
8710+ ?. ?=(%cell -.sample.sh) [%unknown ~]
8711+ =/ as=(list sample) items.sam
8712+ =/ bs=(list field) fields.sample.sh
8713+ ?~ as [%unknown ~]
8714+ ?~ t.as [%unknown ~]
8715+ ?^ t.t.as [%unknown ~]
8716+ ?~ bs [%unknown ~]
8717+ ?~ t.bs [%unknown ~]
8718+ ?^ t.t.bs [%unknown ~]
8719+ ?. &(?=(%cell -.sample.a) ?=(%cell -.sample.b)) [%unknown ~]
8720+ =/ an=(unit term) (direct-sample-name i.as)
8721+ =/ bn=(unit term) (direct-field-name i.bs)
8722+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]
8723+ =/ x=(unit itype) (direct-slot-body hed.sample.a an)
8724+ =/ y=(unit itype) (direct-slot-body hed.sample.b bn)
8725+ ?~ x [%unknown ~]
8726+ ?~ y [%unknown ~]
8727+ =/ first=ifit (direct-invariant u.x u.y sub next)
8728+ ?. ?=(%ok -.first) [%unknown ~]
8729+ =. an (direct-sample-name i.t.as)
8730+ =. bn (direct-field-name i.t.bs)
8731+ ?: &(?=(^ an) ?=(^ bn) !=(u.an u.bn)) [%unknown ~]
8732+ =/ x2=(unit itype) (direct-slot-body tal.sample.a an)
8733+ =/ y2=(unit itype) (direct-slot-body tal.sample.b bn)
8734+ ?~ x2 [%unknown ~]
8735+ ?~ y2 [%unknown ~]
8736+ =/ second=ifit (direct-invariant u.x2 u.y2 sub.first next.first)
8737+ ?. ?=(%ok -.second) [%unknown ~]
8738+ (direct-invariant product.a product.b sub.second next.second)
8739+:: This is a tentative proof: its caller must require closed call samples
8740+:: and repeat every positional check under the stable final substitution.
8741+++ direct-positional-fit
8742+ |= [args=(list expr) slots=(list sample) actual=itype expected=itype env=ienv state=istate sub=isub next=@ud]
8743+ ^- ifit
8744+ ?~ args [%unknown ~]
8745+ ?~ slots [%unknown ~]
8746+ =/ last=? ?=(~ t.args)
8747+ ?: !=(last ?=(~ t.slots)) [%unknown ~]
8748+ =/ split=(unit [left=itype right=itype])
8749+ ?: last `[actual expected]
8750+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8751+ `[hed.actual hed.expected]
8752+ ?~ split [%unknown ~]
8753+ =/ x=itype left.u.split
8754+ =/ y=itype right.u.split
8755+ =/ expected-name=(unit term) (direct-sample-name i.slots)
8756+ =/ expected-body=(unit itype) (direct-slot-body y expected-name)
8757+ ?~ expected-body [%unknown ~]
8758+ =. y u.expected-body
8759+ =/ fit=ifit (itype-fit x y sub next)
8760+ =/ accepted=? &(?=(%ok -.fit) !(itype-positional-slot-face-asym x y sub.fit))
8761+ =/ result=(unit ifit)
8762+ ?: accepted `fit
8763+ ?. &(?=(%face -.i.slots) ?=(%fn -.shape.i.slots)) ~
8764+ ?. ?=(%wing -.i.args) ~
8765+ ?. ?=([@ ~] names.i.args) ~
8766+ ?. (unique-value-name i.names.i.args globals.state) ~
8767+ =/ source=(unit def) (~(get by gate-defs.state) i.names.i.args)
8768+ ?~ source ~
8769+ =/ sample=(unit sample) (direct-gate-sample u.source)
8770+ ?~ sample ~
8771+ =/ trial=ifit (direct-function-fit x y u.sample shape.i.slots sub next)
8772+ ?. ?=(%ok -.trial) ~
8773+ `trial
8774+ ?~ result [%unknown ~]
8775+ =. fit u.result
8776+ ?: last fit
8777+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
8778+ ?. ?=(%ok -.fit) [%unknown ~]
8779+ $(args t.args, slots t.slots, actual tal.actual, expected tal.expected, sub sub.fit, next next.fit)
8780+++ direct-any-gate-arg
8781+ |= [args=(list expr) defs=(map term def)]
8782+ ^- ?
8783+ ?~ args |
8784+ =/ found=?
8785+ ?. ?=(%wing -.i.args) |
8786+ ?. ?=([@ ~] names.i.args) |
8787+ ?=(^ (~(get by defs) i.names.i.args))
8788+ ?: found &
8789+ $(args t.args)
8790+++ direct-gate-call-fit
8791+ |= [e=expr actual=itype expected=itype env=ienv state=istate]
8792+ ^- (unit ifit)
8793+ ?. ?=(%call -.e) ~
8794+ ?~ args.e ~
8795+ ?~ t.args.e ~
8796+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
8797+ ?. ?=(%wing -.head.e) ~
8798+ ?. ?=([@ ~] names.head.e) ~
8799+ ?. ?=(~ (ienv-lookup i.names.head.e env)) ~
8800+ ?. (unique-value-name i.names.head.e globals.state) ~
8801+ ?. (direct-any-gate-arg args.e gate-defs.state) ~
8802+ ?~ prelude.state ~
8803+ ?~ source.u.prelude.state ~
8804+ ?~ head-evidence.state ~
8805+ ?. =(u.prelude.state iface.u.head-evidence.state) ~
8806+ ?. ?=(^ (ienv-lookup i.names.head.e values.u.prelude.state)) ~
8807+ =/ head=(unit def) (~(get by gates.u.head-evidence.state) i.names.head.e)
8808+ ?~ head ~
8809+ =/ sam=(unit sample) (direct-gate-sample u.head)
8810+ ?~ sam ~
8811+ ?. ?=(%cell -.u.sam) ~
8812+ =/ fit=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.state next.state)
8813+ ?. ?=(%ok -.fit) ~
8814+ :: Enclosing inference may add constraints after this call. Only a
8815+ :: closed call-sample proof can remain stable under those later bindings.
8816+ =/ actual-final=itype (itype-normalize actual sub.fit)
8817+ =/ expected-final=itype (itype-normalize expected sub.fit)
8818+ ?^ (itype-vars actual-final) ~
8819+ ?^ (itype-vars expected-final) ~
8820+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
8821+ :: A later argument may resolve a variable used by an earlier slot.
8822+ :: Recheck every fit and face against the completed substitution; no
8823+ :: additional binding or fresh variable is permitted in the second pass.
8824+ =/ verified=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.fit next.fit)
8825+ ?. ?=(%ok -.verified) ~
8826+ ?. &(=(sub.fit sub.verified) =(next.fit next.verified)) ~
8827+ `fit
8828+::
80848829++ infer-call-with-head
80858830 |= [e=expr env=ienv state=istate head=iresult]
80868831 ^- iresult
@@ -8107,7 +8852,17 @@
81078852 =/ fit=ifit
81088853 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
81098854 (itype-fit typ.p.arg sample.ht sub.st next.st)
8110− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
8855+ =/ direct=(unit ifit)
8856+ ?: ?=(%ok -.fit) ~
8857+ (direct-gate-call-fit e typ.p.arg sample.ht env st)
8858+ =. fit ?~(direct fit u.direct)
8859+ ?: ?=(%unknown -.fit)
8860+ ?~ defer.st [%| ["call constraint is not supported by partial inference" ~]]
8861+ =/ edge=(unit dgo) (dg-eligible-ctor e typ.p.head typ.p.arg sample.ht st)
8862+ ?~ edge [%| ["call constraint is not supported by partial inference" ~]]
8863+ ?: (gth (lent obligations.st) 63) [%| ["call constraint is not supported by partial inference" ~]]
8864+ [%& product.ht st(obligations [u.edge obligations.st])]
8865+
81118866 ?: ?=(%bad -.fit)
81128867 ?~ t.args.e
81138868 =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
@@ -8122,7 +8877,10 @@
81228877 =/ arg-at=span ?~(bad whole-args at.u.bad)
81238878 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
81248879 [%| ["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)]]]]
8880+ ?: &(?=(^ defer.st) !(dg-stable-call-fit typ.p.arg sample.ht product.ht sub.fit ?=(^ t.args.e)))
8881+ [%| ["deferred call fit needs stable inference" ~]]
81258882 =/ face-asym=?
8883+ ?^ direct |
81268884 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
81278885 (itype-face-asym typ.p.arg sample.ht sub.fit)
81288886 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
@@ -8189,9 +8947,10 @@
81898947 [%| ["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)]]]]
81908948 [%& expected state.p.value(sub sub.fit, next next.fit)]
81918949::
8192−:: A known gate whose result is still an inference variable can receive
8193−:: an enclosing target before its argument is inferred. Other products
8194−:: and unresolved calls use the existing directional path unchanged.
8950+:: A known gate may receive an enclosing target before its argument is
8951+:: inferred when its result is open or a direct, matching named generic
8952+:: union. Opaque, recursive, tag-constrained and variable-bound union
8953+:: results keep the existing directional path.
81958954++ infer-contextual-call
81968955 |= [e=expr expected=itype env=ienv state=istate]
81978956 ^- iresult
@@ -8202,7 +8961,31 @@
82028961 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
82038962 ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
82048963 =/ result=itype (itype-walk product.ht sub.state.p.head)
8205− ?. ?=(%var -.result) (infer-call-with-head e env state head)
8964+ =/ eligible=?
8965+ ?: ?=(%var -.result) &
8966+ :: A direct known generic union may receive the same nominal result
8967+ :: context before its arguments are checked. Variable-bound origins,
8968+ :: pending tags, recursive identities and unknown atoms stay open.
8969+ ?. &(?=(%union -.product.ht) ?=(%union -.result) ?=(%union -.expected)) |
8970+ ?~ origin.result |
8971+ ?. =(origin.result origin.expected) |
8972+ ?~ args.result |
8973+ ?. =((lent args.result) (lent args.expected)) |
8974+ ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
8975+ =/ result-recursive=? (itype-has-recursive (itype-normalize result sub.state.p.head))
8976+ =/ expected-recursive=? (itype-has-recursive (itype-normalize expected sub.state.p.head))
8977+ =/ result-ok=?
8978+ ?. result-recursive &
8979+ ?~ prelude.state |
8980+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.result `[at.u.prelude.state %element]))
8981+ =/ expected-ok=?
8982+ ?. expected-recursive &
8983+ ?~ prelude.state |
8984+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.expected `[at.u.prelude.state %element]))
8985+ ?. &(result-ok expected-ok) |
8986+ ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
8987+ &
8988+ ?. eligible (infer-call-with-head e env state head)
82068989 ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%rvar -.expected) |(?=(%nvar -.expected) ?=(%rnvar -.expected)) (itype-has-tag (itype-normalize expected sub.state.p.head)))
82078990 (infer-call-with-head e env state head)
82088991 =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
@@ -8290,9 +9073,199 @@
82909073 =/ st=istate state.p.value(sub sub.u.project, next next.u.project)
82919074 [%& expected st(projections [[at.e e typ.p.value expected steps.u.project] projections.st])]
82929075::
9076+:: A known literal singleton in a direct union can contextualize a
9077+:: loobean literal of the same noun. Only explicit singleton and cell
9078+:: competitors are considered; opaque or variable cases stay unknown.
9079+++ explicit-singleton-in-union
9080+ |= [t=itype noun=@]
9081+ ^- ?
9082+ ?. ?=(%union -.t) |
9083+ =/ cases=(list itype) cases.t
9084+ =/ found=? |
9085+ |-
9086+ ?~ cases found
9087+ =/ c=itype i.cases
9088+ ?: ?=(%cell -.c) $(cases t.cases)
9089+ ?. ?=(%const -.c) |
9090+ ?: =(noun val.literal.c)
9091+ ?: found |
9092+ $(cases t.cases, found &)
9093+ $(cases t.cases)
9094+::
9095+:: Select a written literal-headed case only when every competing case is
9096+:: also an explicit singleton-headed cell and exactly one matches. Opaque,
9097+:: variable-bound and differently shaped cases keep inference unchanged.
9098+:: This first slice supplies context to a directly called payload. Plain
9099+:: literal data and other expressions retain their existing inference path.
9100+++ contextual-atomic-arguments
9101+ |= args=(list expr)
9102+ ^- ?
9103+ ?~ args &
9104+ ?. ?=(?(%lit %wing %ctor) -.i.args) |
9105+ $(args t.args)
9106+++ contextual-direct-payload-call
9107+ |= e=expr
9108+ ^- ?
9109+ ?: ?=(%group -.e) $(e inner.e)
9110+ ?. ?=(%call -.e) |
9111+ ?. ?=(%wing -.head.e) |
9112+ ?~ args.e |
9113+ (contextual-atomic-arguments args.e)
9114+::
9115+:: A walked variable may have concealed a union inside a substituted
9116+:: structure before this arm was called. Decline in that case rather than
9117+:: deriving provenance from the already-walked type.
9118+++ contextual-simple-sub
9119+ |= sub=isub
9120+ ^- ?
9121+ ?~ sub &
9122+ ?: ?=(?(%cell %face %fn %union %collection) -.val.i.sub) |
9123+ $(sub t.sub)
9124+::
9125+:: Check the syntactic root before scanning; scan substitutions once.
9126+++ grec-direct-context
9127+ |= [expected=itype sub=isub]
9128+ ^- ?
9129+ =/ left=@ud 4.096
9130+ |-
9131+ ?: ?=(%face -.expected)
9132+ ?: =(0 left) |
9133+ $(expected body.expected, left (dec left))
9134+ ?. ?=(%grec -.expected) |
9135+ ?~ sub &
9136+ ?: =(0 left) |
9137+ ?: ?=(?(%cell %face %fn %union %collection %grec) -.val.i.sub) |
9138+ $(sub t.sub, left (dec left))
9139+++ contextual-direct-union
9140+ |= target=itype
9141+ ^- ?
9142+ ?: ?=(%face -.target) $(target body.target)
9143+ ?=(%union -.target)
9144+++ contextual-tagged-case
9145+ |= [target=itype tag=@ sub=isub]
9146+ ^- (unit itype)
9147+ ?. ?=(%union -.target) ~
9148+ =/ remaining=(list itype) cases.target
9149+ =/ found=(unit itype) ~
9150+ =/ seen=(set @) *(set @)
9151+ |-
9152+ ?~ remaining found
9153+ =/ c=itype i.remaining
9154+ ?. ?=(%cell -.c) ~
9155+ =/ head=itype hed.c
9156+ ?. ?=(%const -.head) ~
9157+ ?: (~(has in:..zuse seen) val.literal.head) ~
9158+ =. seen (~(put in:..zuse seen) val.literal.head)
9159+ ?: =(tag val.literal.head)
9160+ $(remaining t.remaining, found `c)
9161+ $(remaining t.remaining)
9162+::
9163+:: A bounded syntactic screen: no nested branch, cast, gate or local body
9164+:: can re-enter cell-branch retry during either inference attempt.
9165+++ closed-cell-retry-safe
9166+ |= [todo=(list expr) fuel=@ud]
9167+ ^- ?
9168+ ?~ todo &
9169+ ?: =(0 fuel) |
9170+ =/ e=expr i.todo
9171+ =. fuel (dec fuel)
9172+ ?+ -.e |
9173+ %lit $(todo t.todo)
9174+ %wing $(todo t.todo)
9175+ %ctor $(todo t.todo)
9176+ %path $(todo t.todo)
9177+ %crash $(todo t.todo)
9178+ %str
9179+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) |
9180+ $(todo t.todo)
9181+ %group $(todo [inner.e t.todo])
9182+ %pair $(todo [val.e t.todo])
9183+ %unit $(todo [val.e t.todo])
9184+ %list $(todo (weld items.e t.todo))
9185+ %tuple $(todo (weld (turn items.e |=(i=item val.i)) t.todo))
9186+ %change $(todo (weld (turn edits.e |=(ed=edit val.ed)) t.todo))
9187+ %call $(todo [head.e (weld args.e t.todo)])
9188+ %trace $(todo [val.e then.e t.todo])
9189+ ==
9190+::
9191+++ closed-cell-sub-safe
9192+ |= [sub=isub fuel=@ud]
9193+ ^- ?
9194+ ?~ sub &
9195+ ?: =(0 fuel) |
9196+ ?: ?=(?(%cell %face %fn %union %collection %grec %jrec %recursive) -.val.i.sub) |
9197+ $(sub t.sub, fuel (dec fuel))
9198+::
9199+++ closed-cell-branch-eligible
9200+ |= [e=expr expected=itype sub=isub]
9201+ ^- ?
9202+ ?. &(?=(%branch -.e) ?=(%cell -.expected) (closed-cell-sub-safe sub 512)) |
9203+ ?~ arms.e |
9204+ ?~ t.arms.e |
9205+ ?^ t.t.arms.e |
9206+ =/ x=arm i.arms.e
9207+ =/ y=arm i.t.arms.e
9208+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) |
9209+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) |
9210+ ?: =(val.lit.pat.x val.lit.pat.y) |
9211+ (closed-cell-retry-safe ~[subject.e val.x val.y] 512)
9212+::
9213+:: Attempt ordinary inference first; retry from the same state only for
9214+:: the bounded non-reentrant syntax above. Preserve original value faces.
9215+++ infer-closed-cell-branch
9216+ |= [e=expr expected=itype env=ienv state=istate context=span]
9217+ ^- iresult
9218+ ?> (closed-cell-branch-eligible e expected sub.state)
9219+ ?> ?=(%branch -.e)
9220+ ?> ?=(^ arms.e)
9221+ ?> ?=(^ t.arms.e)
9222+ =/ ordinary=iresult (infer-fragment e env state)
9223+ =/ ordinary-good=?
9224+ ?: ?=(%| -.ordinary) |
9225+ =/ fit=ifit (itype-fit typ.p.ordinary expected sub.state.p.ordinary next.state.p.ordinary)
9226+ ?=(%ok -.fit)
9227+ ?: ordinary-good ordinary
9228+ =/ attempt=(unit iresult)
9229+ =/ x=arm i.arms.e
9230+ =/ y=arm i.t.arms.e
9231+ =/ subject=iresult (infer-fragment subject.e env state)
9232+ ?: ?=(%| -.subject) ~
9233+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
9234+ ?: ?=(%union -.subject-type) ~
9235+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
9236+ ?~ su ~
9237+ =/ left=iresult (infer-call-context-arg val.x expected env state.p.subject(sub u.su) context)
9238+ ?: ?=(%| -.left) ~
9239+ =/ lf=ifit (itype-fit typ.p.left expected sub.state.p.left next.state.p.left)
9240+ ?. ?=(%ok -.lf) ~
9241+ =/ right=iresult (infer-call-context-arg val.y expected env state.p.left(sub sub.lf, next next.lf) context)
9242+ ?: ?=(%| -.right) ~
9243+ =/ rf=ifit (itype-fit typ.p.right expected sub.state.p.right next.state.p.right)
9244+ ?. ?=(%ok -.rf) ~
9245+ =/ sub=isub sub.rf
9246+ =/ next=@ud next.rf
9247+ =/ lt=itype (itype-normalize typ.p.left sub)
9248+ =/ rt=itype (itype-normalize typ.p.right sub)
9249+ =/ et=itype (itype-normalize expected sub)
9250+ ?. =(lt rt) ~
9251+ ?: |(?=(^ (itype-vars lt)) ?=(^ (itype-vars rt)) ?=(^ (itype-vars et))) ~
9252+ ?: |((itype-has-tag lt) (itype-has-tag rt) (itype-has-tag et)) ~
9253+ =/ lcheck=ifit (itype-fit typ.p.left expected sub next)
9254+ ?. ?=(%ok -.lcheck) ~
9255+ ?. &(=(sub.lcheck sub) =(next.lcheck next)) ~
9256+ =/ rcheck=ifit (itype-fit typ.p.right expected sub next)
9257+ ?. ?=(%ok -.rcheck) ~
9258+ ?. &(=(sub.rcheck sub) =(next.rcheck next)) ~
9259+ `[%& typ.p.left state.p.right(sub sub, next next)]
9260+ ?~ attempt ordinary
9261+ u.attempt
9262+::
82939263++ infer-call-context-arg
82949264 |= [e=expr expected=itype env=ienv state=istate context=span]
82959265 ^- iresult
9266+ ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9267+ ?: &(?=(^ defer.state) ?=(^ prelude.state) ?=(%tuple -.e))
9268+ (infer-fragment e env state)
82969269 ?: ?=(%pair -.e) $(e (pair-as-cell e))
82979270 ?: ?=(%group -.e) $(e inner.e)
82989271 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
@@ -8305,6 +9278,23 @@
83059278 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
83069279 ?: (explicit-proj-call e env state)
83079280 (infer-proj-context e expected env state context)
9281+ :: Experimental construction only for a source-proven direct target.
9282+ :: Decline any walked structural binding to retain raw-variable provenance.
9283+ ?: &(?=(%grec -.target) ?=(%tuple -.e) (grec-direct-context expected sub.state))
9284+ =/ unfolded=(unit [view=itype left=@ud]) (grec-unfold-view target jrec-fuel.state)
9285+ ?~ unfolded [%| ["recursive mold unfolding needs unsupported inference" ~]]
9286+ ?~ items.e [%| ["recursive mold constructor needs unsupported inference" ~]]
9287+ =/ first=item i.items.e
9288+ ?. &(?=(~ face.first) ?=(%lit -.val.first) =(%term form.lit.val.first))
9289+ [%| ["recursive mold constructor needs unsupported inference" ~]]
9290+ =/ chosen=(unit itype) (contextual-tagged-case view.u.unfolded val.lit.val.first sub.state)
9291+ ?~ chosen [%| ["recursive mold constructor has no matching case" ~]]
9292+ =/ value=iresult (infer-call-context-items items.e u.chosen env state(jrec-fuel left.u.unfolded) context)
9293+ ?: ?=(%| -.value) value
9294+ =/ fit=ifit (itype-fit typ.p.value u.chosen sub.state.p.value next.state.p.value)
9295+ ?: ?=(%unknown -.fit) [%| ["recursive mold case needs unsupported inference" ~]]
9296+ ?: ?=(%bad -.fit) [%| ["recursive mold case does not fit its source shape" ~]]
9297+ [%& target state.p.value(sub sub.fit, next next.fit)]
83089298 :: Only the source-proven one-layer cell is exposed. Each recursive
83099299 :: descent consumes one written tuple; named values use ordinary fit.
83109300 ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
@@ -8322,17 +9312,23 @@
83229312 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
83239313 [%& target state.p.value(sub sub.fit, next next.fit)]
83249314 ?: ?=(%call -.e) (infer-contextual-call e target env state)
9315+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[target context])
9316+ ?^ empty-list u.empty-list
83259317 ?: (single-structured-pattern e)
9318+ ?> ?=(%branch -.e)
9319+ =/ empty-union=(unit iresult) (known-empty-union-wing subject.e env state)
9320+ ?^ empty-union (infer-known-union-context-subject e target env u.empty-union context)
9321+ =/ single=(unit iresult) (grec-single-wing-subject subject.e env state)
9322+ ?^ single (infer-known-union-context-subject e target env u.single context)
83269323 (infer-single-case-branch e env state `[target context])
83279324 ?: (cell-binder-pattern e)
83289325 (infer-cell-branch e env state `[target context])
8329− :: In a loobean-singleton context retain the written loobean noun;
8330− :: the usual final fit decides whether that value is permitted.
9326+ :: In an explicit singleton context retain the written loobean noun;
9327+ :: the ordinary singleton fit compares its noun, not its spelling.
83319328 =/ singleton=(unit itype)
83329329 ?. ?=(%lit -.e) ~
83339330 ?. =(%loobean form.lit.e) ~
8334− ?. ?=(%const -.target) ~
8335− ?. =(%loobean form.literal.target) ~
9331+ ?. |(?=(%const -.target) &(?=(%union -.expected) (explicit-singleton-in-union expected val.lit.e))) ~
83369332 `[%const lit.e]
83379333 ?^ singleton [%& u.singleton state]
83389334 =/ known=(unit iresult)
@@ -8343,6 +9339,8 @@
83439339 (infer-known-union-context-subject e target env u.known context)
83449340 ?: &(?=(%union -.target) ?=(%unit -.e))
83459341 (infer-unit-context e target env state context)
9342+ ?: (closed-cell-branch-eligible e expected sub.state)
9343+ (infer-closed-cell-branch e expected env state context)
83469344 ?: &(?=(%flag -.target) (context-union-branch e))
83479345 (infer-union-context e target env state context)
83489346 ?: &(?=(%union -.target) (context-union-branch e))
@@ -8351,6 +9349,34 @@
83519349 (infer-union-context e target env state context)
83529350 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
83539351 (infer-list-context e target env state context)
9352+ :: A literal-headed tuple can receive the unique case's payload
9353+ :: context. The ordinary final fit still checks the complete union.
9354+ =/ selected=(unit itype)
9355+ ?. &((contextual-simple-sub sub.state) (contextual-direct-union expected) ?=(%union -.target) ?=(%tuple -.e) ?=(^ items.e)) ~
9356+ ?~ t.items.e ~
9357+ ?^ t.t.items.e ~
9358+ ?. (contextual-direct-payload-call val.i.t.items.e) ~
9359+ =/ first=item i.items.e
9360+ ?. &(?=(~ face.first) ?=(%lit -.val.first) |(=(%term form.lit.val.first) =(%null form.lit.val.first) =(%loobean form.lit.val.first))) ~
9361+ (contextual-tagged-case target val.lit.val.first sub.state)
9362+ ?^ selected
9363+ ?> ?=(%tuple -.e)
9364+ :: On this bounded shallow-call shape, preserve any inference that
9365+ :: already fits before trying the new contextual path. Neither pass
9366+ :: can recursively select a nested tuple from the atomic arguments.
9367+ =/ ordinary=(unit iresult)
9368+ =/ initial=iresult (infer-fragment e env state)
9369+ ?: ?=(%| -.initial) ~
9370+ =/ fit=ifit (itype-fit typ.p.initial target sub.state.p.initial next.state.p.initial)
9371+ ?. ?=(%ok -.fit) ~
9372+ `initial
9373+ ?^ ordinary u.ordinary
9374+ =/ value=iresult (infer-call-context-items items.e u.selected env state context)
9375+ ?: ?=(%| -.value) value
9376+ =/ fit=ifit (itype-fit typ.p.value u.selected sub.state.p.value next.state.p.value)
9377+ ?: ?=(%unknown -.fit) [%| ["tagged case needs unsupported inference" ~]]
9378+ ?: ?=(%bad -.fit) [%| ["tagged case does not fit its expected type" ~[[context "expected union case"] [(span-of e) "value"]]]]
9379+ [%& typ.p.value state.p.value(sub sub.fit, next next.fit)]
83549380 ?: &(?=(%cell -.target) ?=(%tuple -.e))
83559381 (infer-call-context-items items.e target env state context)
83569382 (infer-fragment e env state)
@@ -8453,7 +9479,7 @@
84539479 ?~ t.names |
84549480 =. typ (itype-walk typ sub)
84559481 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8456− |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
9482+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%grec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
84579483::
84589484++ cell-binder-pattern
84599485 |= e=expr
@@ -8524,6 +9550,7 @@
85249550 %any-atom "@"
85259551 %flag "?"
85269552 %noun "*"
9553+ %empty "!!"
85279554 %tag (trip txt.literal.t)
85289555 %const (trip txt.literal.t)
85299556 %union
@@ -8532,6 +9559,7 @@
85329559 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
85339560 %recursive ?~(label.t "recursive mold" (trip u.label.t))
85349561 %jrec ?~(label.t "recursive mold" (trip u.label.t))
9562+ %grec ?~(label.t "recursive mold" "({(trip u.label.t)} {(show-itype-cases args.t sub)})")
85359563 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
85369564 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
85379565 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -8575,11 +9603,13 @@
85759603 %any-atom |
85769604 %flag |
85779605 %noun |
9606+ %empty |
85789607 %tag |
85799608 %const |
85809609 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
85819610 %recursive |
85829611 %jrec |
9612+ %grec (lien args.typ |=(c=itype (itype-has-nvar c)))
85839613 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
85849614 %face $(typ body.typ)
85859615 %fn |($(typ sample.typ) $(typ product.typ))
@@ -8691,11 +9721,13 @@
86919721 %any-atom |
86929722 %flag |
86939723 %noun |
9724+ %empty |
86949725 %tag |
86959726 %const |
86969727 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
86979728 %recursive |
86989729 %jrec |
9730+ %grec (lien args.t |=(c=itype (has-atom-var n c)))
86999731 %collection (lien args.t |=(c=itype (has-atom-var n c)))
87009732 %face $(t body.t)
87019733 %fn |($(t sample.t) $(t product.t))
@@ -8839,6 +9871,8 @@
88399871++ infer-recursive-gate
88409872 |= [d=def env=ienv state=istate]
88419873 ^- iresult
9874+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
9875+ =. gate-defs.state ~
88429876 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
88439877 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
88449878 [%| ["recursive definition is not a gate" ~]]
@@ -9062,12 +10096,13 @@
906210096++ infer-gate-group
906310097 |= [ds=(list def) env=ienv state=istate]
906410098 ^- ilocal-result
10099+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
906510100 =/ names=(list term) (global-value-names ds)
906610101 ?. (levy names |=(n=term (unique-value-name n names)))
906710102 [%| ["recursive group contains duplicate names" ~]]
906810103 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
906910104 [%| ["recursive group shadows a name" ~]]
9070− =/ scoped=istate state(globals (weld names globals.state))
10105+ =/ scoped=istate state(globals (weld names globals.state), gate-defs ~)
907110106 =/ seeded=igate-seeds (seed-gate-group ds env scoped)
907210107 ?: ?=(%| -.seeded) seeded
907310108 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
@@ -9101,35 +10136,11 @@
910110136 `[entry u.rest]
910210137::
910310138++ add-supported-defs
9104− |= [ds=(list def) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition)]
10139+ |= [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)]
910510140 ^- [env=ienv artifacts=(list iwidth-definition)]
9106− ?~ ds [env artifacts]
9107− =/ d=def i.ds
9108− ?: ?=(%mold -.d) $(ds t.ds)
9109− ?. (unique-value-name name.d globals) $(ds t.ds)
9110− ?^ (ienv-lookup name.d env) $(ds t.ds)
9111− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9112− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
9113− =. initial (reserve-def-caps val.d initial)
9114− =/ result=iresult (infer-fragment val.d env initial)
9115− =? result ?=(%| -.result) (infer-recursive-gate d env initial)
9116− ?: ?=(%| -.result) $(ds t.ds)
9117− =. state.p.result (promote-restricted-numbers state.p.result env)
9118− =. 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)))
9119− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
9120− ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
9121− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
9122− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
9123− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
9124− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
9125− ?: (gth (lent vars) 26) $(ds t.ds)
9126− =/ finalized=(unit (list iwprojection))
9127− (width-finalize projections.state.p.result sub.state.p.result vars)
9128− ?~ finalized $(ds t.ds)
9129− =? artifacts ?=(^ u.finalized)
9130− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
9131− $(ds t.ds, env [[name.d [typ vars]] env])
10141+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)
913210142::
10143+
913310144+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
913410145+$ iadj (map term (list term))
913510146+$ ivisited (map term ?)
@@ -9243,6 +10254,57 @@
924310254++ resolve-groups
924410255 |= [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)]
924510256 ^- iresolved
10257+ (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
10258+::
10259+
10260++$ iadded-definition
10261+ [env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10262+++ add-supported-result
10263+ |= [d=def result=iresult initial=istate env=ienv checked=(map term def) artifacts=(list iwidth-definition)]
10264+ ^- (unit iadded-definition)
10265+ ?> ?=(%value -.d)
10266+ ?: ?=(%| -.result) ~
10267+ =. state.p.result (promote-restricted-numbers state.p.result env)
10268+ =. 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)))
10269+ ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) ~
10270+ ?: (constrained-capitals caps.state.p.result sub.state.p.result) ~
10271+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
10272+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) ~
10273+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) ~
10274+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10275+ ?: (gth (lent vars) 26) ~
10276+ =/ finalized=(unit (list iwprojection))
10277+ (width-finalize projections.state.p.result sub.state.p.result vars)
10278+ ?~ finalized ~
10279+ =? artifacts ?=(^ u.finalized)
10280+ [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10281+ =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10282+ `[[[name.d [typ vars]] env] checked artifacts]
10283+++ add-supported-defs-core
10284+ |= [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)])]
10285+ ^- [env=ienv artifacts=(list iwidth-definition)]
10286+ ?~ ds [env artifacts]
10287+ =/ d=def i.ds
10288+ ?: ?=(%mold -.d) $(ds t.ds)
10289+ ?: (lien (program-recovery-names all-defs) |=(n=term =(n name.d))) $(ds t.ds)
10290+ ?. (unique-value-name name.d globals) $(ds t.ds)
10291+ ?^ (ienv-lookup name.d env) $(ds t.ds)
10292+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10293+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10294+ =. grec-index.initial index
10295+ =. gate-defs.initial checked
10296+ =. head-evidence.initial heads
10297+ =. initial (reserve-def-caps val.d initial)
10298+ =/ result=iresult (infer-fragment val.d env initial)
10299+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10300+ =/ added=(unit iadded-definition)
10301+ (add-supported-result d result initial env checked artifacts)
10302+ ?~ added $(ds t.ds)
10303+ $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
10304+::
10305+++ resolve-groups-core
10306+ |= [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)])]
10307+ ^- iresolved
924610308 =/ env=ienv ~
924710309 =/ grouped=(list term) ~
924810310 =/ artifacts=(list iwidth-definition) ~
@@ -9251,10 +10313,12 @@
925110313 =/ graph=iadj (graph-make-forward ds nameset ~)
925210314 =/ components=icomponents (graph-components ds names)
925310315 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10316+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
925410317 |-
925510318 =/ next=[env=ienv artifacts=(list iwidth-definition)]
9256− (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)
9257− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
10319+ (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)
10320+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10321+ =. grec-index.initial index
925810322 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
925910323 ?: =(env env.out) out
926010324 $(env env.out, grouped grouped.out, artifacts artifacts.out)
@@ -9503,42 +10567,293 @@
950310567 %overlap
950410568 %unknown
950510569::
9506−++ union-pairs
9507− |= [cases=(list shape) molds=imolds]
9508− ^- (list upair)
9509− ?~ cases ~
9510− =/ first=shape i.cases
9511− =/ a=upat (project-union-mold first molds ~)
9512− =/ pairs=(list upair)
9513− %+ turn t.cases
9514− |= second=shape
9515− ^- upair
9516− [at.first at.second (union-relate a (project-union-mold second molds ~))]
9517− (weld pairs $(cases t.cases))
9518−::
9519−:: A closed structural mold supplies no equation to determine a hole.
9520−:: Applications, references, unbound capitals and unions are unproved.
9521−++ simple-mold-hole
9522− |= sh=shape
9523− ^- (unit (unit span))
9524− ?: ?=(%generic -.sh)
9525− ?~ vars.sh ~
9526− ?. (distinct-params vars.sh) ~
9527− (simple-mold-hole-in body.sh vars.sh)
9528− (simple-mold-hole-in sh ~)
9529−++ simple-mold-hole-in
9530− |= [sh=shape vars=(list @t)]
9531− ^- (unit (unit span))
9532− ?- -.sh
9533− %hole ``at.sh
9534− ?(%aura %noun %void %flag %const) `~
9535− %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
9536− %cell (simple-mold-field-holes fields.sh vars)
10570+:: A source-only fallback for literal-tagged cells and one-hop local
10571+:: generic applications. It screens all work before ordinary inference.
10572+++ union-simple-shape-budget
10573+ |= [s=shape fuel=@ud vars=(unit (list @t))]
10574+ ^- (unit @ud)
10575+ ?: =(0 fuel) ~
10576+ =. fuel (dec fuel)
10577+ ?- -.s
10578+ ?(%aura %noun %void %flag) `fuel
10579+ %tvar
10580+ ?~ vars `fuel
10581+ ?:((lien u.vars |=(n=@t =(n name.s))) `fuel ~)
10582+ %const
10583+ ?. |(=(%term form.lit.s) =(%null form.lit.s) =(%loobean form.lit.s)) ~
10584+ ?: &(=(%loobean form.lit.s) !|(=(0 val.lit.s) =(1 val.lit.s))) ~
10585+ `fuel
10586+ %cell (union-simple-fields-budget fields.s fuel vars)
953710587 %fn
9538− =/ a=(unit (unit span)) $(sh sample.sh)
9539− ?~ a ~
9540− =/ b=(unit (unit span)) $(sh product.sh)
9541− ?~ b ~
10588+ =/ left=(unit @ud) $(s sample.s, fuel fuel)
10589+ ?~ left ~
10590+ $(s product.s, fuel u.left)
10591+ * ~
10592+ ==
10593+++ union-simple-fields-budget
10594+ |= [fields=(list field) fuel=@ud vars=(unit (list @t))]
10595+ ^- (unit @ud)
10596+ ?~ fields `fuel
10597+ ?: =(0 fuel) ~
10598+ =/ field-shape=shape
10599+ ?- -.i.fields
10600+ %bare shape.i.fields
10601+ %face shape.i.fields
10602+ %pun [%ref at.i.fields ~[name.i.fields]]
10603+ ==
10604+ =/ head=(unit @ud) (union-simple-shape-budget field-shape (dec fuel) vars)
10605+ ?~ head ~
10606+ $(fields t.fields, fuel u.head)
10607+++ union-source-find
10608+ |= [n=term molds=imolds fuel=@ud]
10609+ ^- (unit [body=shape left=@ud])
10610+ =/ found=(unit shape) ~
10611+ |-
10612+ ?~ molds
10613+ ?~ found ~
10614+ `[u.found fuel]
10615+ ?: =(0 fuel) ~
10616+ ?: =(n name.i.molds)
10617+ ?^ found ~
10618+ $(molds t.molds, fuel (dec fuel), found `body.i.molds)
10619+ $(molds t.molds, fuel (dec fuel))
10620+++ union-source-args-budget
10621+ |= [vars=(list @t) args=(list shape) fuel=@ud]
10622+ ^- (unit @ud)
10623+ =/ seen=(set @t) *(set @t)
10624+ |-
10625+ ?~ vars ?~(args `fuel ~)
10626+ ?~ args ~
10627+ ?: =(0 fuel) ~
10628+ ?: (~(has in:..zuse seen) i.vars) ~
10629+ =/ arg=(unit @ud) (union-simple-shape-budget i.args (dec fuel) ~)
10630+ ?~ arg ~
10631+ $(vars t.vars, args t.args, fuel u.arg, seen (~(put in:..zuse seen) i.vars))
10632+++ union-source-cell-tag
10633+ |= s=shape
10634+ ^- (unit @)
10635+ ?. ?=(%cell -.s) ~
10636+ ?~ fields.s ~
10637+ ?~ t.fields.s ~
10638+ ?. ?=(%bare -.i.fields.s) ~
10639+ =/ head=shape shape.i.fields.s
10640+ ?. ?=(%const -.head) ~
10641+ ?. |(=(%term form.lit.head) =(%null form.lit.head) =(%loobean form.lit.head)) ~
10642+ ?: &(=(%loobean form.lit.head) !|(=(0 val.lit.head) =(1 val.lit.head))) ~
10643+ `val.lit.head
10644+++ union-source-case-tag
10645+ |= [s=shape molds=imolds fuel=@ud]
10646+ ^- (unit [tag=@ left=@ud])
10647+ ?: ?=(%cell -.s)
10648+ =/ tag=(unit @) (union-source-cell-tag s)
10649+ ?~ tag ~
10650+ =/ left=(unit @ud) (union-simple-shape-budget s fuel ~)
10651+ ?~ left ~
10652+ `[u.tag u.left]
10653+ ?. ?=(%apply -.s) ~
10654+ ?. ?=([@ ~] ref.s) ~
10655+ ?: =(0 fuel) ~
10656+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
10657+ ?~ found ~
10658+ ?. ?=(%generic -.body.u.found) ~
10659+ ?~ vars.body.u.found ~
10660+ =/ tag=(unit @) (union-source-cell-tag body.body.u.found)
10661+ ?~ tag ~
10662+ =/ args=(unit @ud) (union-source-args-budget vars.body.u.found args.s left.u.found)
10663+ ?~ args ~
10664+ =/ left=(unit @ud) (union-simple-shape-budget body.body.u.found u.args `vars.body.u.found)
10665+ ?~ left ~
10666+ `[u.tag u.left]
10667+++ union-source-distinct-tags
10668+ |= [cases=(list shape) molds=imolds fuel=@ud]
10669+ ^- ?
10670+ =/ seen=(set @) *(set @)
10671+ =/ has-application=? |
10672+ |-
10673+ ?~ cases has-application
10674+ ?: =(0 fuel) |
10675+ =/ item=(unit [tag=@ left=@ud]) (union-source-case-tag i.cases molds (dec fuel))
10676+ ?~ item |
10677+ ?: (~(has in:..zuse seen) tag.u.item) |
10678+ $(cases t.cases, fuel left.u.item, seen (~(put in:..zuse seen) tag.u.item), has-application |(has-application ?=(%apply -.i.cases)))
10679+::
10680+:: This inference-only screen bounds inherited work that the small source
10681+:: slice may consult. It does not authenticate a caller-created state.
10682+++ union-state-leaf
10683+ |= t=itype
10684+ ^- ?
10685+ ?=(?(%var %avar %rvar %nvar %rnvar %atom %any-atom %flag %noun %empty %const) -.t)
10686+++ union-state-params-budget
10687+ |= [params=iparams fuel=@ud]
10688+ ^- (unit @ud)
10689+ ?~ params `fuel
10690+ ?: =(0 fuel) ~
10691+ ?. (union-state-leaf typ.i.params) ~
10692+ $(params t.params, fuel (dec fuel))
10693+++ union-state-sub-budget
10694+ |= [sub=isub fuel=@ud]
10695+ ^- (unit @ud)
10696+ ?~ sub `fuel
10697+ ?: =(0 fuel) ~
10698+ ?. (union-state-leaf val.i.sub) ~
10699+ $(sub t.sub, fuel (dec fuel))
10700+++ union-state-caps-budget
10701+ |= [caps=icaps fuel=@ud]
10702+ ^- (unit @ud)
10703+ ?~ caps `fuel
10704+ ?: =(0 fuel) ~
10705+ $(caps t.caps, fuel (dec fuel))
10706+++ union-state-active-budget
10707+ |= [active=(list term) fuel=@ud]
10708+ ^- (unit @ud)
10709+ ?~ active `fuel
10710+ ?: =(0 fuel) ~
10711+ $(active t.active, fuel (dec fuel))
10712+++ union-state-tags-budget
10713+ |= [tags=(list ipending) fuel=@ud]
10714+ ^- (unit @ud)
10715+ ?~ tags `fuel
10716+ ?: =(0 fuel) ~
10717+ $(tags t.tags, fuel (dec fuel))
10718+++ union-source-state-safe
10719+ |= [state=istate fuel=@ud]
10720+ ^- ?
10721+ ?^ grec-index.state |
10722+ ?^ holes.state |
10723+ ?^ defer.state |
10724+ ?^ obligations.state |
10725+ =/ params=(unit @ud) (union-state-params-budget params.state fuel)
10726+ ?~ params |
10727+ =/ sub=(unit @ud) (union-state-sub-budget sub.state u.params)
10728+ ?~ sub |
10729+ =/ caps=(unit @ud) (union-state-caps-budget caps.state u.sub)
10730+ ?~ caps |
10731+ =/ active=(unit @ud) (union-state-active-budget active.state u.caps)
10732+ ?~ active |
10733+ ?=(^ (union-state-tags-budget tags.state u.active))
10734+::
10735+:: Positive overlap witnesses from parsed, one-hop local source only.
10736+:: Unknown or exhausted work returns no witness, never disjointness.
10737++$ uow-case [at=span head=@ payload=upat]
10738+++ union-overlap-primitive
10739+ |= s=shape
10740+ ^- (unit upat)
10741+ ?- -.s
10742+ %aura `[%atom ~]
10743+ %noun `[%all ~]
10744+ %void `[%empty ~]
10745+ %flag `[%flag ~]
10746+ %const
10747+ ?. |(=(%term form.lit.s) =(%null form.lit.s) =(%loobean form.lit.s)) ~
10748+ ?: &(=(%loobean form.lit.s) !|(=(0 val.lit.s) =(1 val.lit.s))) ~
10749+ `[%atom `val.lit.s]
10750+ * ~
10751+ ==
10752+++ union-overlap-case
10753+ |= [s=shape molds=imolds fuel=@ud]
10754+ ^- (unit [item=uow-case left=@ud])
10755+ ?: =(0 fuel) ~
10756+ =. fuel (dec fuel)
10757+ :: Each body has exactly two fields; an application has exactly one
10758+ :: parameter and one concrete primitive argument. The full mold table
10759+ :: is scanned to establish unique ownership.
10760+ =/ expanded=(unit [body=shape param=(unit [name=@t pat=upat]) left=@ud])
10761+ ?: ?=(%cell -.s) `[s ~ fuel]
10762+ ?. ?=(%apply -.s) ~
10763+ ?. ?=([@ ~] ref.s) ~
10764+ ?. ?=([* ~] args.s) ~
10765+ ?: =(0 fuel) ~
10766+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
10767+ ?~ found ~
10768+ ?. ?=(%generic -.body.u.found) ~
10769+ ?. ?=([@ ~] vars.body.u.found) ~
10770+ ?: =(0 left.u.found) ~
10771+ =/ argument=(unit upat) (union-overlap-primitive i.args.s)
10772+ ?~ argument ~
10773+ `[body.body.u.found `[i.vars.body.u.found u.argument] (dec left.u.found)]
10774+ ?~ expanded ~
10775+ =/ body=shape body.u.expanded
10776+ ?. ?=(%cell -.body) ~
10777+ ?. ?=([* * ~] fields.body) ~
10778+ :: Charge the cell, two fields, and the head and payload nodes.
10779+ ?: (lth left.u.expanded 5) ~
10780+ =/ head=(unit @) (union-source-cell-tag body)
10781+ ?~ head ~
10782+ =/ field=field i.t.fields.body
10783+ =/ payload=shape
10784+ ?- -.field
10785+ %bare shape.field
10786+ %face shape.field
10787+ %pun [%ref at.field ~[name.field]]
10788+ ==
10789+ =/ pattern=(unit upat)
10790+ ?: ?=(%tvar -.payload)
10791+ ?~ param.u.expanded ~
10792+ ?. =(name.payload name.u.param.u.expanded) ~
10793+ `pat.u.param.u.expanded
10794+ (union-overlap-primitive payload)
10795+ ?~ pattern ~
10796+ `[[at.s u.head u.pattern] (sub left.u.expanded 5)]
10797+++ union-overlap-against
10798+ |= [first=uow-case rest=(list shape) molds=imolds fuel=@ud]
10799+ ^- (unit [witness=(unit upair) left=@ud])
10800+ ?~ rest `[~ fuel]
10801+ ?: =(0 fuel) ~
10802+ =/ other=(unit [item=uow-case left=@ud]) (union-overlap-case i.rest molds (dec fuel))
10803+ ?~ other ~
10804+ ?: &(=(head.first head.item.u.other) =(%overlap (union-relate payload.first payload.item.u.other)))
10805+ `[`[at.first at.item.u.other %overlap] left.u.other]
10806+ $(rest t.rest, fuel left.u.other)
10807+++ union-source-overlap
10808+ |= [cases=(list shape) molds=imolds fuel=@ud]
10809+ ^- (unit upair)
10810+ ?~ cases ~
10811+ ?~ t.cases ~
10812+ ?: =(0 fuel) ~
10813+ =/ first=(unit [item=uow-case left=@ud]) (union-overlap-case i.cases molds (dec fuel))
10814+ ?~ first ~
10815+ =/ found=(unit [witness=(unit upair) left=@ud])
10816+ (union-overlap-against item.u.first t.cases molds left.u.first)
10817+ ?~ found ~
10818+ ?^ witness.u.found witness.u.found
10819+ $(cases t.cases, fuel left.u.found)
10820+::
10821+++ union-pairs
10822+ |= [cases=(list shape) molds=imolds]
10823+ ^- (list upair)
10824+ ?~ cases ~
10825+ =/ first=shape i.cases
10826+ =/ a=upat (project-union-mold first molds ~)
10827+ =/ pairs=(list upair)
10828+ %+ turn t.cases
10829+ |= second=shape
10830+ ^- upair
10831+ [at.first at.second (union-relate a (project-union-mold second molds ~))]
10832+ (weld pairs $(cases t.cases))
10833+::
10834+:: A closed structural mold supplies no equation to determine a hole.
10835+:: Applications, references, unbound capitals and unions are unproved.
10836+++ simple-mold-hole
10837+ |= sh=shape
10838+ ^- (unit (unit span))
10839+ ?: ?=(%generic -.sh)
10840+ ?~ vars.sh ~
10841+ ?. (distinct-params vars.sh) ~
10842+ (simple-mold-hole-in body.sh vars.sh)
10843+ (simple-mold-hole-in sh ~)
10844+++ simple-mold-hole-in
10845+ |= [sh=shape vars=(list @t)]
10846+ ^- (unit (unit span))
10847+ ?- -.sh
10848+ %hole ``at.sh
10849+ ?(%aura %noun %void %flag %const) `~
10850+ %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
10851+ %cell (simple-mold-field-holes fields.sh vars)
10852+ %fn
10853+ =/ a=(unit (unit span)) $(sh sample.sh)
10854+ ?~ a ~
10855+ =/ b=(unit (unit span)) $(sh product.sh)
10856+ ?~ b ~
954210857 `?~(u.a u.b u.a)
954310858 %generic ~
954410859 * ~
@@ -9656,6 +10971,11 @@
965610971 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
965710972 =/ pairs=(list upair) (union-pairs cases.sh molds)
965810973 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
10974+ =. overlapping
10975+ ?^ overlapping overlapping
10976+ ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
10977+ =/ witness=(unit upair) (union-source-overlap cases.sh molds 256)
10978+ ?~(witness ~ ~[u.witness])
965910979 ?^ overlapping
966010980 =/ p=upair i.overlapping
966110981 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
@@ -9663,7 +10983,9 @@
966310983 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
966410984 (of-wain:format ~[summary first second])
966510985 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
9666− (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10986+ ?. (union-source-distinct-tags cases.sh molds 256)
10987+ (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10988+ (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
966710989 (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
966810990::
966910991:: +show-inference-diagnostic: a partial report with both source sites
@@ -9720,7 +11042,14 @@
972011042+$ jbundle (list jsource)
972111043+$ jcache (list [at=path iface=ifile])
972211044+$ jfile-result (each [iface=ifile cache=jcache] @t)
11045+:: Overlap evidence retains the exact source that supplied its spans.
11046+:: Ordinary Jibb imports preserve this evidence through the resolver.
11047++$ jfile-overlap [file=path source=@t name=term cases=upair]
11048++$ jfile-failure [message=@t overlap=(unit jfile-overlap)]
11049++$ jfile-detailed-result (each [iface=ifile cache=jcache] jfile-failure)
972311050+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
11051+:: Preserve an imported overlap's original file and source across the graph.
11052++$ jimports-detailed-result (each [resolved=ijimports cache=jcache] jfile-failure)
972411053::
972511054:: Written record fields each have their own lexical record scope.
972611055+$ written-fields (map term span)
@@ -9993,6 +11322,43 @@
999311322 (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
999411323 (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
999511324::
11325+:: A detailed failure is attached only to the first mold that actually
11326+:: failed in this check, using that module's checked source mold table.
11327++$ imold-failure [message=@t overlap=(unit [name=term cases=upair])]
11328+:: Validate a generic wrapper without an unbounded duplicate-name pass.
11329+++ module-mold-params-valid
11330+ |= [vars=(list @t) seen=(set @t) fuel=@ud]
11331+ ^- ?
11332+ ?~ vars &
11333+ ?: =(0 fuel) |
11334+ ?: (~(has in:..zuse seen) i.vars) |
11335+ $(vars t.vars, seen (~(put in:..zuse seen) i.vars), fuel (dec fuel))
11336+++ module-mold-overlap
11337+ |= [m=[name=term body=shape] molds=imolds]
11338+ ^- (unit upair)
11339+ =/ sh=shape body.m
11340+ =/ valid=?
11341+ ?. ?=(%generic -.sh) &
11342+ ?~ vars.sh |
11343+ (module-mold-params-valid vars.sh *(set @t) 256)
11344+ ?. valid ~
11345+ =? sh ?=(%generic -.sh) body.sh
11346+ ?. ?=(%union -.sh) ~
11347+ (union-source-overlap cases.sh molds 256)
11348+++ module-mold-types-detail
11349+ |= [molds=imolds state=istate]
11350+ ^- (each imold-types imold-failure)
11351+ ?~ molds [%& ~]
11352+ =/ m=[name=term body=shape] i.molds
11353+ =/ t=(unit [template=ischeme state=istate])
11354+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11355+ ?~ t
11356+ =/ overlap=(unit upair) (module-mold-overlap m molds.state)
11357+ [%| ['module mold needs unsupported inference' ?~(overlap ~ `[name.m u.overlap])]]
11358+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
11359+ =/ rest=(each imold-types imold-failure) $(molds t.molds)
11360+ ?: ?=(%| -.rest) rest
11361+ [%& [[name.m template.u.t] p.rest]]
999611362++ module-mold-types
999711363 |= [molds=imolds state=istate]
999811364 ^- (each imold-types @t)
@@ -10054,6 +11420,9 @@
1005411420 |= [typ=itype name=term vars=(list @ud)]
1005511421 ^- itype
1005611422 ?: ?=(%jrec -.typ) typ(label `name)
11423+ ?: ?=(%grec -.typ)
11424+ ?. (identity-union-parameters vars args.typ) typ(label ~)
11425+ typ(label `name)
1005711426 ?. ?=(%union -.typ) typ
1005811427 ?. (identity-union-parameters vars args.typ)
1005911428 ?~ origin.typ typ
@@ -10086,7 +11455,12 @@
1008611455 =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
1008711456 =/ minus=ischeme [[%fn b b] ~[0]]
1008811457 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
10089− [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~]
11458+ =/ utf8=itype [%atom 'tD']
11459+ =/ tape=itype [%collection %list ~[utf8]]
11460+ =/ codepoints=itype [%collection %list ~[[%atom %c]]]
11461+ =/ text-trip=ischeme [[%fn [%atom %t] tape] ~]
11462+ =/ text-tuba=ischeme [[%fn tape codepoints] ~]
11463+ [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater] [%raw-trip text-trip] [%raw-tuba text-tuba]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
1009011464::
1009111465++ infer-private-internal
1009211466 |= [src=@t public-source=@t]
@@ -10127,9 +11501,9 @@
1012711501 =/ source-unit=(unit ischeme)
1012811502 ?~ unit-decl ~
1012911503 =/ unit-molds=imolds ~[[%unit u.unit-decl]]
10130− =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~]
11504+ =/ unit-state=istate [0 ~ ~ ~ unit-molds ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ | /lib/jibb/prelude/jibb ~[%unit] ~ ~ 256 ~ ~ ~ ~ ~ ~]
1013111505 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
10132− =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~]
11506+ =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
1013311507 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
1013411508 ?~ found ~
1013511509 ?. (standard-unit-template u.found /lib/jibb/prelude/jibb) ~
@@ -10142,7 +11516,7 @@
1014211516 =/ js=ijimports ~[[face.i.imports.mod primitive]]
1014311517 =/ reserved=(list term) ~[face.i.imports.mod]
1014411518 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10145− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~]
11519+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~ ~ ~ ~ ~ ~]
1014611520 =/ mts=(each imold-types @t) (module-mold-types molds state)
1014711521 =/ usable=(unit imold-types)
1014811522 ?: ?=(%& -.mts) `p.mts
@@ -10165,7 +11539,7 @@
1016511539 =/ resolution=iresolved (resolve-groups defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
1016611540 =/ env=ienv env.resolution
1016711541 ?. (module-values-complete defs.mod env) ~
10168− `[env u.usable at ~ artifacts.resolution ~ `src]
11542+ `[env u.usable at ~ artifacts.resolution ~ `src ~]
1016911543::
1017011544++ partial-prelude-interface-with-internal
1017111545 |= [src=@t internal-source=(unit @t)]
@@ -10198,16 +11572,16 @@
1019811572 =? env-molds declared
1019911573 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
1020011574 =/ reserved=(list term) ?:(declared ~[%list] ~)
10201− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~]
11575+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~ ~ ~ ~ ~ ~]
1020211576 :: Other prelude molds may use list only after its source has passed
1020311577 :: the standard-list check. The raw declaration remains removed.
1020411578 =/ declared-list=(unit shape) (find-simple-mold %list molds)
1020511579 =/ mold-prelude=(unit ifile)
1020611580 ?~ declared-list ~
1020711581 ?. (standard-prelude-list u.declared-list) ~
10208− `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~]
11582+ `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~ ~]
1020911583 =/ mt=imold-types (partial-prelude-molds molds state(prelude mold-prelude))
10210− =/ partial=ifile [~ mt at ~ ~ ~ ~]
11584+ =/ partial=ifile [~ mt at ~ ~ ~ ~ ~]
1021111585 :: An explicitly qualified re-export must resolve. Other unsupported
1021211586 :: prelude declarations remain reserved but absent from the interface.
1021311587 =/ required=imolds
@@ -10224,7 +11598,7 @@
1022411598 =/ deps=(list iwidth-dependency)
1022511599 ?~ u.private ~
1022611600 ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
10227− `[env mt at ~ artifacts.resolution deps `src]
11601+ `[env mt at ~ artifacts.resolution deps `src ~]
1022811602::
1022911603++ partial-prelude-interface
1023011604 |= src=@t
@@ -10275,27 +11649,103 @@
1027511649 ?: =(at at.i.cache) `iface.i.cache
1027611650 $(cache t.cache)
1027711651::
11652+:: These certificates retain the complete checked source closure. The
11653+:: trusted host must supply the identical prepared prelude and reader nouns.
11654+:: Exact bundle equality binds all source paths and versions; the set
11655+:: retains transitive paths for active-cycle checks. Request-bearing graphs
11656+:: alone have a size limit; incompatible diamond evidence fails closed.
11657+++ request-graph-requests-add
11658+ |= [pending=(list irequest-evidence) acc=(list irequest-evidence) fuel=@ud]
11659+ ^- (unit (list irequest-evidence))
11660+ ?~ pending `acc
11661+ ?: =(0 fuel) ~
11662+ =/ hit=(list irequest-evidence)
11663+ (skim acc |=(x=irequest-evidence &(=(api-at.x api-at.i.pending) =(name.x name.i.pending))))
11664+ ?^ hit
11665+ ?. ?=([* ~] hit) ~
11666+ ?. =(i.hit i.pending) ~
11667+ $(pending t.pending, fuel (dec fuel))
11668+ $(pending t.pending, acc [i.pending acc], fuel (dec fuel))
11669+++ request-graph-inputs-match
11670+ |= [g=irequest-graph externals=iexternals marks=imark-externals modules=jbundle values=(list term) molds=(list term) prelude=(unit ifile)]
11671+ ^- ?
11672+ ?& =(bundle-input.g modules)
11673+ =(prelude-input.g prelude)
11674+ =(prelude-values.g values)
11675+ =(prelude-molds.g molds)
11676+ =(externals.g externals)
11677+ =(marks.g marks)
11678+ ==
11679+++ request-graph-merge
11680+ |= [imports=ijimports g=irequest-graph fuel=@ud]
11681+ ^- (unit irequest-graph)
11682+ ?~ imports `g
11683+ ?: =(0 fuel) ~
11684+ =/ child=ifile interface.i.imports
11685+ ?~ graph.child ~
11686+ =/ cg=irequest-graph u.graph.child
11687+ ?. ?& =(bundle-input.g bundle-input.cg)
11688+ =(prelude-input.g prelude-input.cg)
11689+ =(prelude-values.g prelude-values.cg)
11690+ =(prelude-molds.g prelude-molds.cg)
11691+ =(externals.g externals.cg)
11692+ =(marks.g marks.cg)
11693+ ==
11694+ ~
11695+ =/ merged=(set path) (~(uni in:..zuse paths.g) paths.cg)
11696+ =/ rs=(unit (list irequest-evidence))
11697+ (request-graph-requests-add requests.cg requests.g (add 1 (lent requests.cg)))
11698+ ?~ rs ~
11699+ ?: &(?=(^ u.rs) |((gth (lent ~(tap in:..zuse merged)) 256) (gth (lent u.rs) 256))) ~
11700+ $(imports t.imports, g g(paths merged, requests u.rs), fuel (dec fuel))
11701+++ request-graph-reusable
11702+ |= [f=ifile src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) values=(list term) molds=(list term) prelude=(unit ifile)]
11703+ ^- ?
11704+ ?~ source.f |
11705+ ?. =(u.source.f src) |
11706+ ?~ graph.f |
11707+ =/ g=irequest-graph u.graph.f
11708+ ?. (request-graph-inputs-match g externals marks modules values molds prelude) |
11709+ ?. (~(has in:..zuse paths.g) at.f) |
11710+ !(lien active |=(p=path (~(has in:..zuse paths.g) p)))
11711+::
1027811712++ resolve-jibb-imports
1027911713 |= [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)]
1028011714 ^- jimports-result
11715+ =/ result=jimports-detailed-result
11716+ (resolve-jibb-imports-detailed imports externals mark-externals modules active prelude-values prelude-molds cache prelude)
11717+ ?: ?=(%| -.result) [%| message.p.result]
11718+ [%& p.result]
11719+++ resolve-jibb-imports-detailed
11720+ |= [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)]
11721+ ^- jimports-detailed-result
1028111722 ?~ imports [%& [~ cache]]
1028211723 ?. ?=(%jibb -.i.imports) $(imports t.imports)
1028311724 =/ at=path (weld path.i.imports `path`~[%jibb])
1028411725 ?: =(at /lib/jibb/internal/jibb)
10285− [%| 'the prelude internal module is private']
11726+ [%| ['the prelude internal module is private' ~]]
1028611727 ?: =(at /lib/jibb/primitives/jibb)
10287− [%| 'the prelude primitive interface is private']
11728+ [%| ['the prelude primitive interface is private' ~]]
1028811729 ?: (lien active |=(p=path =(p at)))
10289− [%| (crip "import cycle at {(spud at)}")]
11730+ [%| [(crip "import cycle at {(spud at)}") ~]]
1029011731 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
10291− ?~ found [%| (crip "module source missing: {(spud at)}")]
10292− ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
11732+ ?~ found [%| [(crip "module source missing: {(spud at)}") ~]]
11733+ ?^ t.found [%| [(crip "duplicate module sources: {(spud at)}") ~]]
1029311734 =/ cached=(unit ifile) (find-jibb-cache at cache)
10294− =/ iface=jfile-result
10295− ?^ cached [%& [u.cached cache]]
10296− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
11735+ =/ iface=jfile-detailed-result
11736+ ?^ cached
11737+ ?. =(at.u.cached at) [%| ['cached module identity needs unsupported inference' ~]]
11738+ ?~ graph.u.cached
11739+ :: A detached legacy interface has unknown evidence. Rebuild it
11740+ :: against the current graph, without retaining any stale entry.
11741+ =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
11742+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
11743+ ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
11744+ [%| ['cached module evidence needs unsupported inference' ~]]
11745+ [%& [u.cached cache]]
11746+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
1029711747 ?: ?=(%| -.iface) [%| p.iface]
10298− =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
11748+ =/ rest=jimports-detailed-result $(imports t.imports, cache cache.p.iface)
1029911749 ?: ?=(%| -.rest) rest
1030011750 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
1030111751::
@@ -10542,6 +11992,27 @@
1054211992 (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
1054311993 ?~ paths [%| 'API path declaration needs unsupported analysis']
1054411994 [%& [file src u.prepared externals marks cache.p.deps u.paths]]
11995+:: Graph-aware variant preserves the caller active stack and cache.
11996+++ api-path-evidence-graph
11997+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
11998+ ^- (each iapi-path-evidence @t)
11999+ ?~ active [%| 'API analysis needs an active graph']
12000+ ?. =(i.active file) [%| 'API analysis active graph does not start at the source']
12001+ ?: (lien t.active |=(p=path =(p file))) [%| 'API analysis active graph contains a cycle']
12002+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path evidence requires /ui/api/<agent>.jibb']
12003+ =/ parsed (parse file src)
12004+ ?: ?=(%| -.parsed) [%| 'API path evidence source does not parse']
12005+ =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12006+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12007+ ?~ prepared [%| 'API path evidence needs the prepared prelude']
12008+ =/ public=ifile iface.u.prepared
12009+ =/ deps=jimports-result
12010+ (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
12011+ ?: ?=(%| -.deps) [%| p.deps]
12012+ =/ paths=(unit (list iapi-path-typed))
12013+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
12014+ ?~ paths [%| 'API path declaration needs unsupported analysis']
12015+ [%& [file src u.prepared externals marks cache.p.deps u.paths]]
1054512016::
1054612017:: This query classifies a unique path declaration only. Missing evidence
1054712018:: or a nonunique name is unknown; it proves nothing about an ask value.
@@ -10637,13 +12108,206 @@
1063712108 =/ surs=(list term) (collect-sur-imports imports.mod)
1063812109 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
1063912110 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10640− =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~]
12111+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
12112+ =/ mts=(each imold-types @t) (module-mold-types molds state)
12113+ ?: ?=(%| -.mts) [%| p.mts]
12114+ =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
12115+ ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
12116+ [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
12117+:: Preserve the same graph context through supporting definitions.
12118+++ api-support-analysis-graph
12119+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12120+ ^- (each iapi-support-evidence @t)
12121+ =/ path-result (api-path-evidence-graph file src externals marks modules active cache prepared)
12122+ ?: ?=(%| -.path-result) [%| p.path-result]
12123+ =/ evidence=iapi-path-evidence p.path-result
12124+ =/ parsed (parse file src)
12125+ ?: ?=(%| -.parsed) [%| 'API source does not parse']
12126+ =/ mod=module p.parsed
12127+ =/ ordinary=(list def)
12128+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
12129+ =/ prep=iprelude prepared.evidence
12130+ ?. (module-scope-valid mod(defs ordinary) values.prep molds.prep) [%| 'API ordinary scope needs unsupported inference']
12131+ =/ vals=(list term) (global-value-names ordinary)
12132+ ?: (lien vals |=(n=term =(n %main))) [%| 'API module kind needs unsupported inference']
12133+ =/ declared=(list term) (collect-mark-imports imports.mod)
12134+ =/ mark-types=(unit (list iapi-mark-type)) (api-diff-types declared marks declared)
12135+ ?~ mark-types [%| 'API declared marks need unsupported inference']
12136+ =/ prelude=(unit ifile) `iface.prep
12137+ =/ deps=jimports-result
12138+ (resolve-jibb-imports imports.mod externals marks modules active values.prep molds.prep dependencies.evidence prelude)
12139+ ?: ?=(%| -.deps) [%| p.deps]
12140+ =/ molds=imolds (collect-simple-molds ordinary)
12141+ =/ globals=(list term) (weld values.prep (weld (import-binding-names imports.mod) vals))
12142+ =/ surs=(list term) (collect-sur-imports imports.mod)
12143+ =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
12144+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12145+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
1064112146 =/ mts=(each imold-types @t) (module-mold-types molds state)
1064212147 ?: ?=(%| -.mts) [%| p.mts]
1064312148 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
1064412149 ?. (module-values-complete ordinary env.resolution) [%| 'API ordinary definitions need unsupported inference']
1064512150 [%& [evidence env.resolution p.mts u.mark-types artifacts.resolution]]
1064612151::
12152+:: Type-analysis artifact for one plain request. The resolver may publish
12153+:: its interface only together with trusted source and reader evidence.
12154+:: No lowering or runtime validator exists.
12155+:: Value watchability remains unproved even for a watchable declaration.
12156++$ ione-request-interface
12157+ [support=iapi-support-evidence parts=iapi-request-parts iface=ifile]
12158+++ request-compatible-ask
12159+ |= prelude=iprelude
12160+ ^- (unit ischeme)
12161+ =/ public=ifile iface.prelude
12162+ ?. =(at.public /lib/jibb/prelude/jibb) ~
12163+ =/ ask=(unit ischeme) (find-jibb-mold %ask public)
12164+ ?~ ask ~
12165+ ?. ?=([@ ~] vars.u.ask) ~
12166+ ?. ?=(%union -.typ.u.ask) ~
12167+ ?. =(origin.typ.u.ask `[/lib/jibb/internal/jibb %ask]) ~
12168+ ?. (identity-union-parameters vars.u.ask args.typ.u.ask) ~
12169+ =/ m=@ud i.vars.u.ask
12170+ ?: (itype-var-is-atom m typ.u.ask) ~
12171+ ?. (levy (itype-vars typ.u.ask) |=(n=@ud =(n m))) ~
12172+ ?: (itype-has-tag typ.u.ask) ~
12173+ =/ private=(list iwidth-dependency)
12174+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12175+ ?. ?=([* ~] private) ~
12176+ ?~ source.i.private ~
12177+ =/ path=(unit ischeme) (find-jibb-mold %path public)
12178+ ?~ path ~
12179+ ?^ vars.u.path ~
12180+ =/ path-type=itype [%collection %list ~[[%atom %ta]]]
12181+ ?. =(typ.u.path path-type) ~
12182+ =/ unit-template=(unit ischeme) (find-jibb-mold %unit public)
12183+ ?~ unit-template ~
12184+ ?. (standard-unit-template u.unit-template /lib/jibb/prelude/jibb) ~
12185+ =/ state-unit=(unit itype) (template-apply u.unit-template ~[[%noun ~]])
12186+ ?~ state-unit ~
12187+ =/ path-unit=(unit itype) (template-apply u.unit-template ~[path-type])
12188+ ?~ path-unit ~
12189+ =/ output=itype [%cell [%face %state [%noun ~]] [%face %message [%var m]]]
12190+ =/ agent-input=itype [%cell [%face %mark [%atom %tas]] [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]]
12191+ =/ store-input=itype [%cell [%face %state u.state-unit] [%face %fact [%noun ~]]]
12192+ =/ pure-case=itype [%cell [%const [%term %tas %pure '%pure']] [%face %value [%var m]]]
12193+ =/ agent-case=itype
12194+ [%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]]]]]]]]
12195+ =/ store-case=itype
12196+ [%cell [%const [%term %tas %store '%store']] [%cell [%face %module [%atom %t]] [%cell [%face %name [%atom %tas]] [%face %receive [%fn store-input output]]]]]
12197+ ?. =(cases.typ.u.ask ~[pure-case agent-case store-case]) ~
12198+ ask
12199+::
12200+:: The first supported standalone API has exactly one mark import and one
12201+:: plain path declaration, with no other definitions or imports. No partial
12202+:: success is published when source, schema, or a required mold is unknown.
12203+++ one-request-interface-source
12204+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
12205+ ^- (each ione-request-interface @t)
12206+ =/ out (api-support-analysis-source file src externals marks modules prepared)
12207+ ?: ?=(%| -.out) [%| p.out]
12208+ =/ support=iapi-support-evidence p.out
12209+ =/ ev=iapi-path-evidence paths.support
12210+ =/ parsed (parse file src)
12211+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12212+ =/ mod=module p.parsed
12213+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
12214+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
12215+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
12216+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
12217+ =/ p=iapi-path-typed i.paths.ev
12218+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12219+ ?~ parts [%| 'request components need unsupported inference']
12220+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
12221+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
12222+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
12223+ =/ valid-marks=?
12224+ ?~ fold.u.parts ?=([* ~] marks.support)
12225+ ?=([* [* ~]] marks.support)
12226+ ?. valid-marks [%| 'request marks need unsupported inference']
12227+ =/ fold-open=?
12228+ ?~ fold.u.parts |
12229+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12230+ ?: fold-open [%| 'request fold needs unsupported inference']
12231+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12232+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12233+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12234+ ?~ ask [%| 'request ask needs unsupported inference']
12235+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
12236+ ?~ result [%| 'request ask needs unsupported inference']
12237+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12238+ =/ sample=itype
12239+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12240+ ?~ parameters.u.parts callback
12241+ [%cell typ.i.parameters.u.parts callback]
12242+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12243+ =/ exports=imold-types
12244+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12245+ =/ prelude=iprelude prepared.ev
12246+ =/ public=ifile iface.prelude
12247+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12248+ =/ private=(list iwidth-dependency)
12249+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12250+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12251+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12252+ =/ req=irequest-evidence
12253+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12254+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12255+ [%& [support u.parts interface]]
12256+:: Graph-aware request artifact; resolver use remains type-only.
12257+++ one-request-interface-graph
12258+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12259+ ^- (each ione-request-interface @t)
12260+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
12261+ ?: ?=(%| -.out) [%| p.out]
12262+ =/ support=iapi-support-evidence p.out
12263+ =/ ev=iapi-path-evidence paths.support
12264+ =/ parsed (parse file src)
12265+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12266+ =/ mod=module p.parsed
12267+ ?. ?=(?([[%mark *] ~] [[%mark *] [%mark *] ~]) imports.mod) [%| 'request imports need unsupported inference']
12268+ ?. ?=([[%mold *] ~] defs.mod) [%| 'request definitions need unsupported inference']
12269+ ?. =(%paths name.i.defs.mod) [%| 'request declaration needs unsupported inference']
12270+ ?. ?=([* ~] paths.ev) [%| 'request count needs unsupported inference']
12271+ =/ p=iapi-path-typed i.paths.ev
12272+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12273+ ?~ parts [%| 'request components need unsupported inference']
12274+ ?. ?=(?(~ [* ~]) parameters.u.parts) [%| 'request parameters need unsupported inference']
12275+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) [%| 'request parameter and fold need unsupported inference']
12276+ ?^ scry.path.p [%| 'request scry needs unsupported inference']
12277+ =/ valid-marks=?
12278+ ?~ fold.u.parts ?=([* ~] marks.support)
12279+ ?=([* [* ~]] marks.support)
12280+ ?. valid-marks [%| 'request marks need unsupported inference']
12281+ =/ fold-open=?
12282+ ?~ fold.u.parts |
12283+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12284+ ?: fold-open [%| 'request fold needs unsupported inference']
12285+ ?^ (itype-vars reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12286+ ?: (itype-has-tag reply-sample.u.parts) [%| 'request payload needs unsupported inference']
12287+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12288+ ?~ ask [%| 'request ask needs unsupported inference']
12289+ =/ result=(unit itype) (template-apply u.ask ~[[%var 0]])
12290+ ?~ result [%| 'request ask needs unsupported inference']
12291+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12292+ =/ sample=itype
12293+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12294+ ?~ parameters.u.parts callback
12295+ [%cell typ.i.parameters.u.parts callback]
12296+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12297+ =/ exports=imold-types
12298+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12299+ =/ prelude=iprelude prepared.ev
12300+ =/ public=ifile iface.prelude
12301+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12302+ =/ private=(list iwidth-dependency)
12303+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12304+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12305+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12306+ =/ req=irequest-evidence
12307+ [file name.path.p p src u.source.public u.source.i.private values.prelude molds.prelude externals marks]
12308+ =/ interface=ifile [~[[name.path.p scheme]] exports file ~ ~ ~ `src `[(silt `(list path)`~[file]) ~[req] modules `public values.prelude molds.prelude externals marks]]
12309+ [%& [support u.parts interface]]
12310+::
1064712311++ api-mark-exports
1064812312 |= [marks=(list term) all=(list term) externals=imark-externals]
1064912313 ^- imold-types
@@ -10687,46 +12351,1404 @@
1068712351 =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
1068812352 ?~ mark ~
1068912353 =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
10690− `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~]
12354+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
12355+::
12356+:: Source-proven ordinary helpers validate each selected /sur dependency.
12357+:: Unused or less direct cores remain unsupported by this first interface.
12358+++ api-sur-covered
12359+ |= [surs=(list term) defs=(list def) externals=iexternals all=(list term)]
12360+ ^- ?
12361+ ?~ surs &
12362+ =/ found=(list def)
12363+ %+ skim defs
12364+ |= d=def
12365+ ?. ?=(%mold -.d) |
12366+ ?. ?=(%ref -.shape.d) |
12367+ ?. ?=([@ [@ ~]] names.shape.d) |
12368+ =(i.t.names.shape.d i.surs)
12369+ ?~ found |
12370+ =/ selected=def i.found
12371+ ?. ?=(%mold -.selected) |
12372+ =/ sh=shape shape.selected
12373+ ?. ?=(%ref -.sh) |
12374+ ?. ?=([@ [@ ~]] names.sh) |
12375+ =/ checked=(unit itype) (find-imported-mold i.surs i.names.sh externals all)
12376+ ?~ checked |
12377+ $(surs t.surs)
12378+::
12379++$ imulti-request-gates [values=ienv requests=(list irequest-evidence)]
12380+++ api-request-gates
12381+ |= [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]
12382+ ^- (unit imulti-request-gates)
12383+ ?~ paths `[~ ~]
12384+ ?: =(0 fuel) ~
12385+ =/ p=iapi-path-typed i.paths
12386+ =/ parts=(unit iapi-request-parts) (api-request-parts `ev name.path.p)
12387+ ?~ parts ~
12388+ ?. ?=(?(~ [* ~]) parameters.u.parts) ~
12389+ ?: &(?=(^ fold.u.parts) ?=(^ parameters.u.parts)) ~
12390+ ?^ scry.path.p ~
12391+ ?^ (itype-vars reply-sample.u.parts) ~
12392+ ?: (itype-has-tag reply-sample.u.parts) ~
12393+ =/ open-fold=?
12394+ ?~ fold.u.parts |
12395+ |(?=(^ (itype-vars u.fold.u.parts)) (itype-has-tag u.fold.u.parts))
12396+ ?: open-fold ~
12397+ =/ result=(unit itype) (template-apply ask ~[[%var 0]])
12398+ ?~ result ~
12399+ =/ callback=itype [%fn reply-sample.u.parts [%var 0]]
12400+ =/ sample=itype
12401+ ?^ fold.u.parts [%cell callback u.fold.u.parts]
12402+ ?~ parameters.u.parts callback
12403+ [%cell typ.i.parameters.u.parts callback]
12404+ =/ scheme=ischeme [[%fn sample u.result] ~[0]]
12405+ =/ prep=iprelude prepared.ev
12406+ =/ req=irequest-evidence
12407+ [file name.path.p p src public internal values.prep molds.prep externals marks]
12408+ =/ rest=(unit imulti-request-gates)
12409+ $(paths t.paths, fuel (dec fuel))
12410+ ?~ rest ~
12411+ `[[[name.path.p scheme] values.u.rest] [req requests.u.rest]]
12412+::
12413+++ api-poke-from-checked
12414+ |= [file=path mod=module marks=imark-externals values=(list term) molds=(list term) prelude=(unit ifile)]
12415+ ^- (unit [values=ienv derived=(list iderived)])
12416+ =/ pokes=(list def)
12417+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12418+ ?~ pokes `[~ ~]
12419+ ?. ?=([* ~] pokes) ~
12420+ =/ declared=(list term) (collect-mark-imports imports.mod)
12421+ =/ ns=(unit (list term)) (api-poke-mark-names pokes declared)
12422+ ?~ ns ~
12423+ ?. ?=([@ ~] u.ns) ~
12424+ =/ matching=(list import)
12425+ %+ skim imports.mod
12426+ |= i=import
12427+ ?. ?=(%mark -.i) |
12428+ =(mark.i i.u.ns)
12429+ ?. ?=([* ~] matching) ~
12430+ =/ checked=(unit ifile)
12431+ (api-poke-interface file mod(defs pokes, imports matching) marks values molds prelude)
12432+ ?~ checked ~
12433+ `[values.u.checked derived.u.checked]
12434+::
12435+:: The partial interface is published atomically: all paths, ordinary
12436+:: source definitions, declared marks and the poke must check. Unselected
12437+:: /sur bindings, runtime validation and value watchability remain unproved.
12438+++ multi-request-interface-graph
12439+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle active=(list path) cache=jcache prepared=(unit iprelude)]
12440+ ^- (each [iface=ifile cache=jcache] @t)
12441+ =/ out (api-support-analysis-graph file src externals marks modules active cache prepared)
12442+ ?: ?=(%| -.out) [%| p.out]
12443+ =/ support=iapi-support-evidence p.out
12444+ =/ ev=iapi-path-evidence paths.support
12445+ =/ parsed (parse file src)
12446+ ?: ?=(%| -.parsed) [%| 'request source does not parse']
12447+ =/ mod=module p.parsed
12448+ ?. (levy imports.mod |=(i=import ?=(?(%mark %sur) -.i)))
12449+ [%| 'request imports need unsupported inference']
12450+ =/ surs=(list term) (collect-sur-imports imports.mod)
12451+ ?. (api-sur-covered surs defs.mod externals surs)
12452+ [%| 'API source dependency needs unsupported inference']
12453+ ?~ paths.ev [%| 'request count needs unsupported inference']
12454+ =/ ask=(unit ischeme) (request-compatible-ask prepared.ev)
12455+ ?~ ask [%| 'request ask needs unsupported inference']
12456+ =/ prep=iprelude prepared.ev
12457+ =/ public=ifile iface.prep
12458+ ?~ source.public [%| 'request prelude source needs unsupported inference']
12459+ =/ private=(list iwidth-dependency)
12460+ (skim dependencies.public |=(d=iwidth-dependency =(at.d /lib/jibb/internal/jibb)))
12461+ ?. ?=([* ~] private) [%| 'request internal source needs unsupported inference']
12462+ ?~ source.i.private [%| 'request internal source needs unsupported inference']
12463+ =/ gates=(unit imulti-request-gates)
12464+ (api-request-gates paths.ev ev u.ask file src u.source.public u.source.i.private externals marks 256)
12465+ ?~ gates [%| 'request paths need unsupported inference']
12466+ =/ poke=(unit [values=ienv derived=(list iderived)])
12467+ (api-poke-from-checked file mod marks values.prep molds.prep `public)
12468+ ?~ poke [%| 'API poke needs unsupported inference']
12469+ =/ mark-molds=imold-types
12470+ (turn marks.support |=(m=iapi-mark-type [name.m [typ.m ~]]))
12471+ =/ exports=imold-types (weld mark-molds molds.support)
12472+ =/ names=(list term) (turn exports |=(m=[name=term template=ischeme] name.m))
12473+ ?. (levy names |=(n=term (unique-value-name n names)))
12474+ [%| 'API exported molds need unsupported inference']
12475+ =/ env=ienv (weld values.u.gates (weld values.u.poke values.support))
12476+ =/ graph=irequest-graph
12477+ [(silt `(list path)`~[file]) requests.u.gates modules `public values.prep molds.prep externals marks]
12478+ =/ iface=ifile
12479+ [env exports file derived.u.poke elaborations.support ~ `src `graph]
12480+ [%& [iface dependencies.ev]]
12481+::
12482+:: A checked program main is only the direct four-component source call.
12483+:: Grouping is transparent, but aliases, qualified wings and other module
12484+:: kinds remain outside this slice.
12485+++ program-main-def
12486+ |= ds=(list def)
12487+ ^- (unit def)
12488+ ?~ ds ~
12489+ ?: &(?=(%value -.i.ds) =(%main name.i.ds)) `i.ds
12490+ $(ds t.ds)
12491+::
12492+++ program-main-wing
12493+ |= e=expr
12494+ ^- (unit term)
12495+ ?: ?=(%group -.e) $(e inner.e)
12496+ ?. ?=(%wing -.e) ~
12497+ ?. ?=([@ ~] names.e) ~
12498+ `i.names.e
12499+::
12500+++ program-main-args
12501+ |= d=def
12502+ ^- (unit (list expr))
12503+ ?. ?=(%value -.d) ~
12504+ |-
12505+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12506+ ?. ?=(%call -.val.d) ~
12507+ =/ head=(unit term) (program-main-wing head.val.d)
12508+ ?~ head ~
12509+ ?. =(%program u.head) ~
12510+ ?. ?=([* * * * ~] args.val.d) ~
12511+ `args.val.d
12512+::
12513+++ program-main-parts
12514+ |= d=def
12515+ ^- (unit [init=term update=term view=term subs=term])
12516+ ?. ?=(%value -.d) ~
12517+ |-
12518+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12519+ ?. ?=(%call -.val.d) ~
12520+ =/ head=(unit term) (program-main-wing head.val.d)
12521+ ?~ head ~
12522+ ?. =(%program u.head) ~
12523+ ?. ?=([* * * * ~] args.val.d) ~
12524+ =/ args=(list expr) args.val.d
12525+ ?> ?=([* * * * ~] args)
12526+ =/ init=(unit term) (program-main-wing i.args)
12527+ =/ update=(unit term) (program-main-wing i.t.args)
12528+ =/ view=(unit term) (program-main-wing i.t.t.args)
12529+ =/ subs=(unit term) (program-main-wing i.t.t.t.args)
12530+ ?~ init ~
12531+ ?~ update ~
12532+ ?~ view ~
12533+ ?~ subs ~
12534+ `[u.init u.update u.view u.subs]
12535+::
12536+++ program-empty-null
12537+ |= e=expr
12538+ ^- ?
12539+ ?- -.e
12540+ %lit =(%null form.lit.e)
12541+ %cast $(e val.e)
12542+ %group $(e inner.e)
12543+ %body ?~(defs.e $(e final.e) |)
12544+ * |
12545+ ==
12546+::
12547+++ program-subs-empty
12548+ |= d=def
12549+ ^- ?
12550+ ?. ?=(%value -.d) |
12551+ ?- -.val.d
12552+ %gate (program-empty-null body.val.d)
12553+ %gate-wide (program-empty-null body.val.d)
12554+ * |
12555+ ==
12556+::
12557+++ program-transparent
12558+ |= e=expr
12559+ ^- expr
12560+ ?- -.e
12561+ %group $(e inner.e)
12562+ %cast $(e val.e)
12563+ %body ?~(defs.e $(e final.e) e)
12564+ * e
12565+ ==
12566+++ program-init-tuple-null
12567+ |= d=def
12568+ ^- ?
12569+ ?. ?=(%value -.d) |
12570+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
12571+ =/ body=expr
12572+ ?- -.val.d
12573+ %gate body.val.d
12574+ %gate-wide body.val.d
12575+ * !!
12576+ ==
12577+ =. body (program-transparent body)
12578+ ?. ?=(%tuple -.body) |
12579+ ?~ items.body |
12580+ (program-empty-null val:(rear items.body))
12581+::
12582+:: Recover only the update of an already recognized direct program main.
12583+:: Its written sample determines the message/model relationship; the canonical
12584+:: cmd, unit and update slot determine the result context. Publication is
12585+:: component-local so later subscription/view/initializer retries can accumulate.
12586+++ program-update-context
12587+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12588+ ^- (unit iresolved)
12589+ =/ env=ienv env.resolution
12590+ ?^ (ienv-lookup %main env) ~
12591+ ?^ (ienv-lookup update.parts env) ~
12592+ =/ updates=(list def)
12593+ (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
12594+ ?. ?=([* ~] updates) ~
12595+ =/ update-def=def i.updates
12596+ ?> ?=(%value -.update-def)
12597+ =/ written-update=(unit sample) (direct-gate-sample update-def)
12598+ ?~ written-update ~
12599+ ?. ?=(%cell -.u.written-update) ~
12600+ ?. ?=([* * ~] items.u.written-update) ~
12601+ ?~ prelude.initial ~
12602+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12603+ ?~ program ~
12604+ =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
12605+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12606+ ?~ command ~
12607+ ?~ list-template ~
12608+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12609+ ?~ heads ~
12610+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12611+ ?~ written ~
12612+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12613+ ?~ written-sample ~
12614+ ?. ?=(%cell -.u.written-sample) ~
12615+ ?. ?=([* * * * ~] items.u.written-sample) ~
12616+ =/ checked=(map term def)
12617+ (~(put by (direct-checked-gates ds env)) update.parts update-def)
12618+ =/ templates=ienv
12619+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12620+ =/ scanned=(unit dgscan)
12621+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12622+ ?~ scanned ~
12623+ =. next.initial (dg-next-id ids.u.scanned 0)
12624+ =/ update-state=istate (reserve-def-caps val.update-def initial)
12625+ =/ sam=isample-result (infer-sample u.written-update env update-state)
12626+ ?: ?=(%| -.sam) ~
12627+ =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
12628+ ?. ?=(%cell -.actual-sample) ~
12629+ =/ message=(unit itype)
12630+ (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
12631+ =/ model=(unit itype)
12632+ (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
12633+ ?~ message ~
12634+ ?~ model ~
12635+ =/ cmd=(unit itype) (template-apply u.command ~[u.message])
12636+ ?~ cmd ~
12637+ =/ command-result=(unit itype) (template-apply u.list-template ~[u.cmd])
12638+ ?~ command-result ~
12639+ =/ product=itype [%cell u.model u.command-result]
12640+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
12641+ ?. ?=(%fn -.typ.instance) ~
12642+ ?. ?=(%cell -.sample.typ.instance) ~
12643+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12644+ =/ expected-update=(unit itype)
12645+ (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
12646+ ?~ expected-update ~
12647+ ?. ?=(%fn -.u.expected-update) ~
12648+ :: Sample binders are not value faces. Strip only those two slot faces
12649+ :: for the invariant canonical-gate proof; the source-faced gate is still
12650+ :: used by the complete positional call and final ordinary result cast.
12651+ =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
12652+ =/ gate-fit=ifit
12653+ (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
12654+ ?. ?=(%ok -.gate-fit) ~
12655+ =/ closed=itype
12656+ (itype-normalize [%fn typ.p.sam product] sub.gate-fit)
12657+ ?. ?=(%fn -.closed) ~
12658+ :: The closed product no longer needs the canonical slot substitutions.
12659+ :: Start the body at its ordinary sample state so existing branch retries
12660+ :: keep their substitution guards, but retain the shared fresh-ID high water.
12661+ =/ st=istate state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12662+ =/ body=expr
12663+ ?- -.val.update-def
12664+ %gate body.val.update-def
12665+ %gate-wide body.val.update-def
12666+ * !!
12667+ ==
12668+ =/ inferred=iresult
12669+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12670+ ?: ?=(%| -.inferred) ~
12671+ =/ product-fit=ifit
12672+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12673+ ?. ?=(%ok -.product-fit) ~
12674+ =/ merged-product=itype
12675+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12676+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12677+ =/ cast=ifit
12678+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12679+ ?. ?=(%ok -.cast) ~
12680+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12681+ =/ adjusted=iresult
12682+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12683+ =/ added=(unit iadded-definition)
12684+ (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
12685+ ?~ added ~
12686+ =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
12687+ ?~ recovered ~
12688+ ?. ?=(~ vars.u.recovered) ~
12689+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12690+ `[env.u.added grouped.resolution artifacts.u.added]
12691+::
12692+++ program-inferred-slot
12693+ |= [typ=itype name=(unit term)]
12694+ ^- itype
12695+ ?~ name typ
12696+ ?: &(?=(%face -.typ) =(name.typ u.name)) body.typ
12697+ typ
12698+::
12699+++ program-inferred-sample
12700+ |= [typ=itype sam=sample]
12701+ ^- itype
12702+ (program-inferred-slot typ (direct-sample-name sam))
12703+::
12704+++ program-two-slot-names
12705+ |= sam=sample
12706+ ^- (unit [first=(unit term) second=(unit term)])
12707+ ?- -.sam
12708+ %cell
12709+ ?. ?=([* * ~] items.sam) ~
12710+ `[(direct-sample-name i.items.sam) (direct-sample-name i.t.items.sam)]
12711+ %face
12712+ ?. ?=(%cell -.shape.sam) ~
12713+ ?. ?=([* * ~] fields.shape.sam) ~
12714+ `[(direct-field-name i.fields.shape.sam) (direct-field-name i.t.fields.shape.sam)]
12715+ * ~
12716+ ==
12717+::
12718+:: Read message/model from the checked update and its written source layout.
12719+:: The source names strip only top-level sample binder faces; nested value
12720+:: faces remain part of the canonical message and model.
12721+++ program-update-relation
12722+ |= [name=term ds=(list def) env=ienv]
12723+ ^- (unit [message=itype model=itype])
12724+ =/ update=(unit ischeme) (ienv-lookup name env)
12725+ ?~ update ~
12726+ ?. ?=(~ vars.u.update) ~
12727+ ?. ?=(~ (itype-vars typ.u.update)) ~
12728+ ?. ?=(%fn -.typ.u.update) ~
12729+ ?. ?=(%cell -.sample.typ.u.update) ~
12730+ =/ defs=(list def)
12731+ (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
12732+ ?. ?=([* ~] defs) ~
12733+ =/ written=(unit sample) (direct-gate-sample i.defs)
12734+ ?~ written ~
12735+ ?. ?=(%cell -.u.written) ~
12736+ ?. ?=([* * ~] items.u.written) ~
12737+ =/ message=(unit itype)
12738+ (direct-slot-body hed.sample.typ.u.update (direct-sample-name i.items.u.written))
12739+ =/ model=(unit itype)
12740+ (direct-slot-body tal.sample.typ.u.update (direct-sample-name i.t.items.u.written))
12741+ ?~ message ~
12742+ ?~ model ~
12743+ `[u.message u.model]
12744+::
12745+:: Recover an unannotated direct subscription component from the checked
12746+:: update relation and canonical fourth program slot. This establishes only
12747+:: the value type; the final program watch proof remains separate.
12748+++ program-subs-context
12749+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12750+ ^- (unit iresolved)
12751+ =/ env=ienv env.resolution
12752+ ?^ (ienv-lookup %main env) ~
12753+ ?^ (ienv-lookup subs.parts env) ~
12754+ =/ relation=(unit [message=itype model=itype])
12755+ (program-update-relation update.parts ds env)
12756+ ?~ relation ~
12757+ =/ subs=(list def)
12758+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
12759+ ?. ?=([* ~] subs) ~
12760+ =/ subs-def=def i.subs
12761+ ?> ?=(%value -.subs-def)
12762+ =/ written-subs=(unit sample) (direct-gate-sample subs-def)
12763+ ?~ written-subs ~
12764+ ?~ prelude.initial ~
12765+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12766+ =/ sub=(unit ischeme) (find-jibb-mold %sub u.prelude.initial)
12767+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12768+ ?~ program ~
12769+ ?~ sub ~
12770+ ?~ list-template ~
12771+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12772+ ?~ heads ~
12773+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12774+ ?~ written ~
12775+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12776+ ?~ written-sample ~
12777+ ?. ?=(%cell -.u.written-sample) ~
12778+ ?. ?=([* * * * ~] items.u.written-sample) ~
12779+ =/ checked=(map term def) (direct-checked-gates ds env)
12780+ =/ templates=ienv
12781+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12782+ =/ scanned=(unit dgscan)
12783+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12784+ ?~ scanned ~
12785+ =. next.initial (dg-next-id ids.u.scanned 0)
12786+ =/ subs-state=istate (reserve-def-caps val.subs-def initial)
12787+ =/ sam=isample-result (infer-sample u.written-subs env subs-state)
12788+ ?: ?=(%| -.sam) ~
12789+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-subs)
12790+ ?. ?=(~ (itype-vars actual-model)) ~
12791+ ?: (itype-has-tag actual-model) ~
12792+ =/ model-fit=ifit
12793+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
12794+ ?. ?=(%ok -.model-fit) ~
12795+ =/ message-sub=(unit itype) (template-apply u.sub ~[message.u.relation])
12796+ ?~ message-sub ~
12797+ =/ product=(unit itype) (template-apply u.list-template ~[u.message-sub])
12798+ ?~ product ~
12799+ =/ instance=[typ=itype state=istate]
12800+ (instantiate-scheme u.program state.p.sam(sub sub.model-fit, next next.model-fit))
12801+ ?. ?=(%fn -.typ.instance) ~
12802+ ?. ?=(%cell -.sample.typ.instance) ~
12803+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12804+ ?. ?=(%cell -.tal.tal.sample.typ.instance) ~
12805+ =/ expected-subs=(unit itype)
12806+ (direct-slot-body tal.tal.tal.sample.typ.instance (direct-sample-name i.t.t.t.items.u.written-sample))
12807+ ?~ expected-subs ~
12808+ ?. ?=(%fn -.u.expected-subs) ~
12809+ =/ canonical=itype [%fn model.u.relation u.product]
12810+ =/ gate-fit=ifit
12811+ (direct-invariant canonical u.expected-subs sub.state.instance next.state.instance)
12812+ ?. ?=(%ok -.gate-fit) ~
12813+ =/ closed=itype
12814+ (itype-normalize [%fn typ.p.sam u.product] sub.gate-fit)
12815+ ?. ?=(%fn -.closed) ~
12816+ =/ body=expr
12817+ ?- -.val.subs-def
12818+ %gate body.val.subs-def
12819+ %gate-wide body.val.subs-def
12820+ * !!
12821+ ==
12822+ =/ st=istate
12823+ state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12824+ =/ inferred=iresult
12825+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12826+ ?: ?=(%| -.inferred) ~
12827+ =/ product-fit=ifit
12828+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12829+ ?. ?=(%ok -.product-fit) ~
12830+ =/ merged-product=itype
12831+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12832+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12833+ =/ cast=ifit
12834+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12835+ ?. ?=(%ok -.cast) ~
12836+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12837+ =/ adjusted=iresult
12838+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12839+ =/ added=(unit iadded-definition)
12840+ (add-supported-result subs-def adjusted subs-state env checked artifacts.resolution)
12841+ ?~ added ~
12842+ =/ recovered=(unit ischeme) (ienv-lookup subs.parts env.u.added)
12843+ ?~ recovered ~
12844+ ?. ?=(~ vars.u.recovered) ~
12845+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12846+ `[env.u.added grouped.resolution artifacts.u.added]
12847+::
12848++$ iview-site [xs=expr mapper=term]
12849+++ program-view-site
12850+ |= e=expr
12851+ ^- (unit iview-site)
12852+ =. e (program-transparent e)
12853+ ?. ?=(%call -.e) ~
12854+ ?. ?=([* ~] args.e) ~
12855+ =/ each=expr (program-transparent head.e)
12856+ ?. ?=(%wing -.each) ~
12857+ ?. ?=([%each ~] names.each) ~
12858+ =/ turned=expr (program-transparent i.args.e)
12859+ ?. ?=(%call -.turned) ~
12860+ ?. ?=([* * ~] args.turned) ~
12861+ =/ turn=expr (program-transparent head.turned)
12862+ ?. ?=(%wing -.turn) ~
12863+ ?. ?=([%turn ~] names.turn) ~
12864+ =/ xs=expr (program-transparent i.args.turned)
12865+ ?. ?=(%wing -.xs) ~
12866+ ?~ names.xs ~
12867+ =/ mapper=(unit term) (program-main-wing i.t.args.turned)
12868+ ?~ mapper ~
12869+ `[xs u.mapper]
12870+::
12871+++ program-recovery-names
12872+ |= ds=(list def)
12873+ ^- (list term)
12874+ =/ main=(unit def) (program-main-def ds)
12875+ ?~ main ~
12876+ =/ parts=(unit [init=term update=term view=term subs=term])
12877+ (program-main-parts u.main)
12878+ ?~ parts ~
12879+ =/ views=(list def)
12880+ (skim ds |=(d=def &(?=(%value -.d) =(view.u.parts name.d))))
12881+ ?. ?=([* ~] views) ~
12882+ =/ view-def=def i.views
12883+ ?> ?=(%value -.view-def)
12884+ =/ written=(unit sample) (direct-gate-sample view-def)
12885+ ?~ written ~
12886+ =/ body=expr
12887+ ?- -.val.view-def
12888+ %gate body.val.view-def
12889+ %gate-wide body.val.view-def
12890+ * !!
12891+ ==
12892+ =/ sites=(unit (list iview-site)) (program-view-sites body ~)
12893+ ?~ sites ~
12894+ ?. ?=([* ~] u.sites) ~
12895+ =/ mapper=term mapper.i.u.sites
12896+ =/ components=(list term)
12897+ :~ init.u.parts
12898+ update.u.parts
12899+ view.u.parts
12900+ subs.u.parts
12901+ ==
12902+ ?: (lien components |=(n=term =(n mapper))) ~
12903+ =/ mappers=(list def)
12904+ (skim ds |=(d=def &(?=(%value -.d) =(mapper name.d))))
12905+ ?. ?=([* ~] mappers) ~
12906+ :~ init.u.parts
12907+ update.u.parts
12908+ view.u.parts
12909+ subs.u.parts
12910+ mapper
12911+ ==
12912+::
12913+++ program-sample-binders
12914+ |= sam=sample
12915+ ^- (list term)
12916+ ?- -.sam
12917+ %bind ~[name.sam]
12918+ %face ~[name.sam]
12919+ %pun ~[name.sam]
12920+ %cell (zing (turn items.sam |=(s=sample (program-sample-binders s))))
12921+ * ~
12922+ ==
12923+::
12924+++ program-pattern-binders
12925+ |= pat=pattern
12926+ ^- (list term)
12927+ ?- -.pat
12928+ %bind ~[name.pat]
12929+ %cell (zing (turn items.pat |=(p=pattern (program-pattern-binders p))))
12930+ * ~
12931+ ==
12932+::
12933+++ program-view-sites-merge
12934+ |= [a=(unit (list iview-site)) b=(unit (list iview-site))]
12935+ ^- (unit (list iview-site))
12936+ ?~ a ~
12937+ ?~ b ~
12938+ `(weld u.a u.b)
12939+::
12940+++ program-view-sites-exprs
12941+ |= [xs=(list expr) locals=(list term)]
12942+ ^- (unit (list iview-site))
12943+ ?~ xs `~
12944+ (program-view-sites-merge (program-view-sites i.xs locals) $(xs t.xs))
12945+::
12946+++ program-view-sites-items
12947+ |= [xs=(list item) locals=(list term)]
12948+ ^- (unit (list iview-site))
12949+ ?~ xs `~
12950+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
12951+::
12952+++ program-view-sites-pieces
12953+ |= [xs=(list piece) locals=(list term)]
12954+ ^- (unit (list iview-site))
12955+ ?~ xs `~
12956+ =/ here=(unit (list iview-site))
12957+ ?- -.i.xs
12958+ %expr (program-view-sites p.i.xs locals)
12959+ %text `~
12960+ ==
12961+ (program-view-sites-merge here $(xs t.xs))
12962+::
12963+++ program-view-sites-qsegs
12964+ |= [xs=(list qseg) locals=(list term)]
12965+ ^- (unit (list iview-site))
12966+ ?~ xs `~
12967+ =/ here=(unit (list iview-site))
12968+ ?- -.i.xs
12969+ %expr (program-view-sites p.i.xs locals)
12970+ %knot `~
12971+ ==
12972+ (program-view-sites-merge here $(xs t.xs))
12973+::
12974+++ program-view-sites-edits
12975+ |= [xs=(list edit) locals=(list term)]
12976+ ^- (unit (list iview-site))
12977+ ?~ xs `~
12978+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
12979+::
12980+++ program-view-sites-defs
12981+ |= [xs=(list def) locals=(list term)]
12982+ ^- (unit (list iview-site))
12983+ ?~ xs `~
12984+ =/ here=(unit (list iview-site))
12985+ ?: ?=(%mold -.i.xs) `~
12986+ (program-view-sites val.i.xs locals)
12987+ (program-view-sites-merge here $(xs t.xs))
12988+::
12989+++ program-view-sites-arms
12990+ |= [xs=(list arm) locals=(list term)]
12991+ ^- (unit (list iview-site))
12992+ ?~ xs `~
12993+ =/ nested=(list term) (weld (program-pattern-binders pat.i.xs) locals)
12994+ (program-view-sites-merge (program-view-sites val.i.xs nested) $(xs t.xs))
12995+::
12996+++ program-view-sites
12997+ |= [e=expr locals=(list term)]
12998+ ^- (unit (list iview-site))
12999+ =/ site=(unit iview-site) (program-view-site e)
13000+ ?^ site
13001+ =/ names=(list term) ~[%each %turn mapper.u.site]
13002+ ?> ?=(%wing -.xs.u.site)
13003+ =/ root=term (rear names.xs.u.site)
13004+ ?: |((lien names |=(n=term (lien locals |=(x=term =(n x))))) (lien locals |=(x=term =(root x))))
13005+ ~
13006+ `~[u.site]
13007+ ?- -.e
13008+ %str (program-view-sites-pieces pieces.e locals)
13009+ %qath (program-view-sites-qsegs segs.e locals)
13010+ %change (program-view-sites-edits edits.e locals)
13011+ %pair (program-view-sites val.e locals)
13012+ %unit (program-view-sites val.e locals)
13013+ %group (program-view-sites inner.e locals)
13014+ %list (program-view-sites-exprs items.e locals)
13015+ %tuple (program-view-sites-items items.e locals)
13016+ %gate
13017+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13018+ %gate-wide
13019+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13020+ %call
13021+ (program-view-sites-merge (program-view-sites head.e locals) (program-view-sites-exprs args.e locals))
13022+ %cast (program-view-sites val.e locals)
13023+ %trace
13024+ (program-view-sites-merge (program-view-sites val.e locals) (program-view-sites then.e locals))
13025+ %branch
13026+ (program-view-sites-merge (program-view-sites subject.e locals) (program-view-sites-arms arms.e locals))
13027+ %body
13028+ =/ nested=(list term) (weld (global-value-names defs.e) locals)
13029+ (program-view-sites-merge (program-view-sites-defs defs.e nested) (program-view-sites final.e nested))
13030+ * `~
13031+ ==
13032+::
13033+++ program-union-tag-case
13034+ |= [expected=itype tag=@]
13035+ ^- (unit itype)
13036+ ?. ?=(%union -.expected) ~
13037+ =/ remaining=(list itype) cases.expected
13038+ =/ found=(unit itype) ~
13039+ =/ seen=(set @) *(set @)
13040+ |-
13041+ ?~ remaining found
13042+ =/ case=itype i.remaining
13043+ =/ head=(unit @)
13044+ ?: ?=(%const -.case) `val.literal.case
13045+ ?. ?=(%cell -.case) ~
13046+ ?. ?=(%const -.hed.case) ~
13047+ `val.literal.hed.case
13048+ ?~ head ~
13049+ ?: (~(has in:..zuse seen) u.head) ~
13050+ =. seen (~(put in:..zuse seen) u.head)
13051+ =? found =(tag u.head)
13052+ ?^(found ~ `case)
13053+ $(remaining t.remaining)
13054+::
13055+++ program-single-case-fit
13056+ |= [actual=itype expected=itype sub=isub next=@ud]
13057+ ^- ifit
13058+ =. actual (itype-normalize actual sub)
13059+ =. expected (itype-normalize expected sub)
13060+ ?. ?=(%union -.expected) [%unknown ~]
13061+ =/ found=(unit itype)
13062+ ?: ?=(%const -.actual) `actual
13063+ ?: ?=(%tag -.actual) `actual
13064+ ?: ?=(%cell -.actual) `actual
13065+ ?. ?=(%union -.actual) ~
13066+ ?. ?=([* ~] cases.actual) ~
13067+ `i.cases.actual
13068+ ?~ found [%unknown ~]
13069+ =/ case=itype u.found
13070+ =/ tag=(unit lit)
13071+ ?: ?=(%const -.case) `literal.case
13072+ ?: ?=(%tag -.case) `literal.case
13073+ ?. ?=(%cell -.case) ~
13074+ =/ head=itype (projection-field-target hed.case)
13075+ ?: ?=(%const -.head) `literal.head
13076+ ?: ?=(%tag -.head) `literal.head
13077+ ~
13078+ ?~ tag [%unknown ~]
13079+ =/ chosen=(unit itype) (program-union-tag-case expected val.u.tag)
13080+ ?~ chosen [%unknown ~]
13081+ ?: |(?=(%const -.case) ?=(%tag -.case))
13082+ ?. ?=(%const -.u.chosen) [%unknown ~]
13083+ (itype-fit case u.chosen sub next)
13084+ ?. ?=(%cell -.case) [%unknown ~]
13085+ ?. ?=(%cell -.u.chosen) [%unknown ~]
13086+ =/ head-fit=ifit (itype-fit hed.case hed.u.chosen sub next)
13087+ ?. ?=(%ok -.head-fit) head-fit
13088+ (itype-fit tal.case tal.u.chosen sub.head-fit next.head-fit)
13089+::
13090+++ program-single-generic-fit
13091+ |= [actual=itype expected=itype sub=isub next=@ud]
13092+ ^- ifit
13093+ =. actual (itype-normalize actual sub)
13094+ =. expected (itype-normalize expected sub)
13095+ ?. &(?=(%union -.actual) ?=(%union -.expected)) [%unknown ~]
13096+ ?~ origin.actual [%unknown ~]
13097+ ?. =(origin.actual origin.expected) [%unknown ~]
13098+ ?. ?=([* ~] args.actual) [%unknown ~]
13099+ ?. ?=([* ~] args.expected) [%unknown ~]
13100+ =/ argument-fit=ifit (direct-invariant i.args.actual i.args.expected sub next)
13101+ ?: ?=(%ok -.argument-fit) argument-fit
13102+ (program-single-case-fit i.args.actual i.args.expected sub next)
13103+::
13104+++ program-keyed-product-fit
13105+ |= [actual=itype expected=itype element=ischeme sub=isub next=@ud]
13106+ ^- ifit
13107+ =. actual (itype-normalize actual sub)
13108+ =. expected (itype-normalize expected sub)
13109+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
13110+ =/ key-fit=ifit
13111+ (itype-fit (projection-field-target hed.actual) (projection-field-target hed.expected) sub next)
13112+ ?. ?=(%ok -.key-fit) key-fit
13113+ =/ actual-el=itype
13114+ (itype-normalize (projection-field-target tal.actual) sub.key-fit)
13115+ =/ expected-el=itype
13116+ (itype-normalize (projection-field-target tal.expected) sub.key-fit)
13117+ ?. &(?=(%union -.actual-el) ?=(%union -.expected-el)) [%unknown ~]
13118+ ?. =(origin.actual-el origin.expected-el) [%unknown ~]
13119+ ?. ?=([* ~] args.actual-el) [%unknown ~]
13120+ ?. ?=([* ~] args.expected-el) [%unknown ~]
13121+ =/ canonical-actual=(unit itype)
13122+ (template-apply element ~[i.args.actual-el])
13123+ =/ canonical-expected=(unit itype)
13124+ (template-apply element ~[i.args.expected-el])
13125+ ?~ canonical-actual [%unknown ~]
13126+ ?~ canonical-expected [%unknown ~]
13127+ =/ actual-check=ifit
13128+ (direct-invariant actual-el u.canonical-actual sub.key-fit next.key-fit)
13129+ ?. ?=(%ok -.actual-check) actual-check
13130+ =/ expected-check=ifit
13131+ (direct-invariant expected-el u.canonical-expected sub.actual-check next.actual-check)
13132+ ?. ?=(%ok -.expected-check) expected-check
13133+ =/ case-fit=ifit
13134+ (program-single-case-fit i.args.actual-el i.args.expected-el sub.expected-check next.expected-check)
13135+ case-fit
13136+::
13137+:: Recover exactly one direct keyed each/turn row mapper, then its view.
13138+:: The prelude's own each and turn schemes determine the mapper gate: the
13139+:: key is inferred from the mapper body, never selected by this recovery.
13140+++ program-view-context
13141+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13142+ ^- (unit iresolved)
13143+ =/ env=ienv env.resolution
13144+ ?^ (ienv-lookup %main env) ~
13145+ ?^ (ienv-lookup view.parts env) ~
13146+ =/ relation=(unit [message=itype model=itype])
13147+ (program-update-relation update.parts ds env)
13148+ ?~ relation ~
13149+ =/ views=(list def)
13150+ (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13151+ ?. ?=([* ~] views) ~
13152+ =/ view-def=def i.views
13153+ ?> ?=(%value -.view-def)
13154+ =/ written-view=(unit sample) (direct-gate-sample view-def)
13155+ ?~ written-view ~
13156+ =/ view-body=expr
13157+ ?- -.val.view-def
13158+ %gate body.val.view-def
13159+ %gate-wide body.val.view-def
13160+ * !!
13161+ ==
13162+ =/ sites=(unit (list iview-site)) (program-view-sites view-body ~)
13163+ ?~ sites ~
13164+ ?. ?=([* ~] u.sites) ~
13165+ =/ site=iview-site i.u.sites
13166+ =/ component-names=(list term) ~[init.parts update.parts view.parts subs.parts]
13167+ ?: (lien component-names |=(n=term =(n mapper.site))) ~
13168+ ?^ (ienv-lookup mapper.site env) ~
13169+ =/ mappers=(list def)
13170+ (skim ds |=(d=def &(?=(%value -.d) =(mapper.site name.d))))
13171+ ?. ?=([* ~] mappers) ~
13172+ =/ mapper-def=def i.mappers
13173+ ?> ?=(%value -.mapper-def)
13174+ =/ written-mapper=(unit sample) (direct-gate-sample mapper-def)
13175+ ?~ written-mapper ~
13176+ ?~ prelude.initial ~
13177+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13178+ =/ each-scheme=(unit ischeme) (ienv-lookup %each values.u.prelude.initial)
13179+ =/ turn-scheme=(unit ischeme) (ienv-lookup %turn values.u.prelude.initial)
13180+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13181+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13182+ ?~ program ~
13183+ ?~ each-scheme ~
13184+ ?~ turn-scheme ~
13185+ ?~ element ~
13186+ ?~ list-template ~
13187+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13188+ ?~ heads ~
13189+ =/ written-program=(unit def) (~(get by gates.u.heads) %program)
13190+ =/ written-each=(unit def) (~(get by gates.u.heads) %each)
13191+ =/ written-turn=(unit def) (~(get by gates.u.heads) %turn)
13192+ ?~ written-program ~
13193+ ?~ written-each ~
13194+ ?~ written-turn ~
13195+ =/ program-sample=(unit sample) (direct-gate-sample u.written-program)
13196+ =/ each-sample=(unit sample) (direct-gate-sample u.written-each)
13197+ =/ turn-sample=(unit sample) (direct-gate-sample u.written-turn)
13198+ ?~ program-sample ~
13199+ ?~ each-sample ~
13200+ ?~ turn-sample ~
13201+ ?. ?=(%cell -.u.program-sample) ~
13202+ ?. ?=([* * * * ~] items.u.program-sample) ~
13203+ =/ turn-names=(unit [first=(unit term) second=(unit term)])
13204+ (program-two-slot-names u.turn-sample)
13205+ ?~ turn-names ~
13206+ =/ checked=(map term def) (direct-checked-gates ds env)
13207+ =/ templates=ienv
13208+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13209+ =/ scanned=(unit dgscan)
13210+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13211+ ?~ scanned ~
13212+ =. next.initial (dg-next-id ids.u.scanned 0)
13213+ =/ view-state=istate (reserve-def-caps val.view-def initial)
13214+ =/ sam=isample-result (infer-sample u.written-view env view-state)
13215+ ?: ?=(%| -.sam) ~
13216+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13217+ =/ model-fit=ifit
13218+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13219+ ?. ?=(%ok -.model-fit) ~
13220+ =/ xs-result=iresult
13221+ (infer-fragment xs.site env.p.sam state.p.sam(sub sub.model-fit, next next.model-fit))
13222+ ?: ?=(%| -.xs-result) ~
13223+ =/ element-var=itype [%var next.state.p.xs-result]
13224+ =/ list-a=(unit itype) (template-apply u.list-template ~[element-var])
13225+ ?~ list-a ~
13226+ =/ xs-fit=ifit
13227+ (itype-fit typ.p.xs-result u.list-a sub.state.p.xs-result +(next.state.p.xs-result))
13228+ ?. ?=(%ok -.xs-fit) ~
13229+ =/ closed-xs=itype (itype-normalize u.list-a sub.xs-fit)
13230+ ?^ (itype-vars closed-xs) ~
13231+ ?: (itype-has-tag closed-xs) ~
13232+ =/ each-instance=[typ=itype state=istate]
13233+ (instantiate-scheme u.each-scheme state.p.xs-result(sub sub.xs-fit, next next.xs-fit))
13234+ ?. ?=(%fn -.typ.each-instance) ~
13235+ =/ turn-instance=[typ=itype state=istate]
13236+ (instantiate-scheme u.turn-scheme state.each-instance)
13237+ ?. ?=(%fn -.typ.turn-instance) ~
13238+ ?. ?=(%cell -.sample.typ.turn-instance) ~
13239+ =/ element-message=(unit itype)
13240+ (template-apply u.element ~[message.u.relation])
13241+ ?~ element-message ~
13242+ =/ each-fit=ifit
13243+ (itype-fit product.typ.each-instance u.element-message sub.state.turn-instance next.state.turn-instance)
13244+ ?. ?=(%ok -.each-fit) ~
13245+ =/ each-input=itype
13246+ (program-inferred-sample sample.typ.each-instance u.each-sample)
13247+ =/ turn-fit=ifit
13248+ (itype-fit product.typ.turn-instance each-input sub.each-fit next.each-fit)
13249+ ?. ?=(%ok -.turn-fit) ~
13250+ =/ turn-list=itype
13251+ (program-inferred-slot hed.sample.typ.turn-instance first.u.turn-names)
13252+ =/ list-fit=ifit
13253+ (itype-fit closed-xs turn-list sub.turn-fit next.turn-fit)
13254+ ?. ?=(%ok -.list-fit) ~
13255+ =/ mapper-type=itype
13256+ (program-inferred-slot tal.sample.typ.turn-instance second.u.turn-names)
13257+ =/ expected-mapper=itype (itype-normalize mapper-type sub.list-fit)
13258+ ?. ?=(%fn -.expected-mapper) ~
13259+ ?^ (itype-vars sample.expected-mapper) ~
13260+ ?: (itype-has-tag sample.expected-mapper) ~
13261+ :: These faces come from the source-backed each sample. Keeping them in
13262+ :: the expected mapper product lets ordinary tuple inference supply key/el.
13263+ ?. ?=(%cell -.product.expected-mapper) ~
13264+ ?. ?=(%face -.hed.product.expected-mapper) ~
13265+ ?. =(%key name.hed.product.expected-mapper) ~
13266+ ?. ?=(%face -.tal.product.expected-mapper) ~
13267+ ?. =(%el name.tal.product.expected-mapper) ~
13268+ =/ mapper-state=istate
13269+ (reserve-def-caps val.mapper-def initial(next next.list-fit))
13270+ =/ mapper-sam=isample-result (infer-sample u.written-mapper env mapper-state)
13271+ ?: ?=(%| -.mapper-sam) ~
13272+ =/ mapper-input=itype (program-inferred-sample typ.p.mapper-sam u.written-mapper)
13273+ =/ mapper-sample-fit=ifit
13274+ (direct-invariant mapper-input sample.expected-mapper sub.state.p.mapper-sam next.state.p.mapper-sam)
13275+ ?. ?=(%ok -.mapper-sample-fit) ~
13276+ =/ mapper-product=itype
13277+ (itype-normalize product.expected-mapper sub.mapper-sample-fit)
13278+ =/ mapper-body=expr
13279+ ?- -.val.mapper-def
13280+ %gate body.val.mapper-def
13281+ %gate-wide body.val.mapper-def
13282+ * !!
13283+ ==
13284+ =/ mapper-inferred=iresult
13285+ (infer-call-context-arg mapper-body mapper-product env.p.mapper-sam state.p.mapper-sam(sub sub.mapper-sample-fit, next next.mapper-sample-fit) (span-of mapper-body))
13286+ ?: ?=(%| -.mapper-inferred) ~
13287+ =/ ordinary-product-fit=ifit
13288+ (itype-fit typ.p.mapper-inferred mapper-product sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13289+ =/ mapper-product-fit=ifit
13290+ ?: ?=(%ok -.ordinary-product-fit) ordinary-product-fit
13291+ (program-keyed-product-fit typ.p.mapper-inferred mapper-product u.element sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13292+ ?. ?=(%ok -.mapper-product-fit) ~
13293+ =/ closed-mapper-product=itype
13294+ (itype-normalize mapper-product sub.mapper-product-fit)
13295+ ?^ (itype-vars closed-mapper-product) ~
13296+ ?: (itype-has-tag closed-mapper-product) ~
13297+ =/ merged-mapper-product=itype
13298+ (itype-merge-faces typ.p.mapper-inferred closed-mapper-product sub.mapper-product-fit)
13299+ =/ mapper-cast=itype [%fn typ.p.mapper-sam merged-mapper-product]
13300+ =/ closed-mapper=itype [%fn typ.p.mapper-sam closed-mapper-product]
13301+ =/ mapper-cast-fit=ifit
13302+ (itype-fit mapper-cast closed-mapper sub.mapper-product-fit next.mapper-product-fit)
13303+ ?. ?=(%ok -.mapper-cast-fit) ~
13304+ =/ merged-mapper=itype
13305+ (itype-merge-faces mapper-cast closed-mapper sub.mapper-cast-fit)
13306+ =/ mapper-adjusted=iresult
13307+ [%& merged-mapper state.p.mapper-inferred(sub sub.mapper-cast-fit, next next.mapper-cast-fit)]
13308+ =/ mapper-added=(unit iadded-definition)
13309+ (add-supported-result mapper-def mapper-adjusted mapper-state env checked artifacts.resolution)
13310+ ?~ mapper-added ~
13311+ =/ mapper-scheme=(unit ischeme) (ienv-lookup mapper.site env.u.mapper-added)
13312+ ?~ mapper-scheme ~
13313+ ?. ?=(~ vars.u.mapper-scheme) ~
13314+ ?. ?=(~ (itype-vars typ.u.mapper-scheme)) ~
13315+ =/ program-instance=[typ=itype state=istate]
13316+ (instantiate-scheme u.program state.p.sam(next next.mapper-cast-fit))
13317+ ?. ?=(%fn -.typ.program-instance) ~
13318+ ?. ?=(%cell -.sample.typ.program-instance) ~
13319+ ?. ?=(%cell -.tal.sample.typ.program-instance) ~
13320+ ?. ?=(%cell -.tal.tal.sample.typ.program-instance) ~
13321+ =/ expected-view=(unit itype)
13322+ (direct-slot-body hed.tal.tal.sample.typ.program-instance (direct-sample-name i.t.t.items.u.program-sample))
13323+ ?~ expected-view ~
13324+ ?. ?=(%fn -.u.expected-view) ~
13325+ =/ canonical-view=itype [%fn model.u.relation u.element-message]
13326+ =/ view-fit=ifit
13327+ (direct-invariant canonical-view u.expected-view sub.state.program-instance next.state.program-instance)
13328+ ?. ?=(%ok -.view-fit) ~
13329+ =/ closed-view=itype
13330+ (itype-normalize [%fn typ.p.sam u.element-message] sub.view-fit)
13331+ ?. ?=(%fn -.closed-view) ~
13332+ =/ view-env=ienv [[mapper.site u.mapper-scheme] env.p.sam]
13333+ =/ final-view-state=istate
13334+ (reserve-def-caps val.view-def state.p.sam(next next.view-fit, gate-defs checked.u.mapper-added, head-evidence heads))
13335+ =/ inferred=iresult
13336+ (infer-call-context-arg view-body product.closed-view view-env final-view-state (span-of view-body))
13337+ ?: ?=(%| -.inferred) ~
13338+ =/ product-fit=ifit
13339+ (itype-fit typ.p.inferred product.closed-view sub.state.p.inferred next.state.p.inferred)
13340+ ?. ?=(%ok -.product-fit) ~
13341+ =/ merged-product=itype
13342+ (itype-merge-faces typ.p.inferred product.closed-view sub.product-fit)
13343+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13344+ =/ cast=ifit
13345+ (itype-fit actual-cast closed-view sub.product-fit next.product-fit)
13346+ ?. ?=(%ok -.cast) ~
13347+ =/ merged=itype (itype-merge-faces actual-cast closed-view sub.cast)
13348+ =/ adjusted=iresult
13349+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13350+ =/ added=(unit iadded-definition)
13351+ (add-supported-result view-def adjusted final-view-state env.u.mapper-added checked.u.mapper-added artifacts.u.mapper-added)
13352+ ?~ added ~
13353+ =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13354+ ?~ recovered ~
13355+ ?. ?=(~ vars.u.recovered) ~
13356+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13357+ `[env.u.added grouped.resolution artifacts.u.added]
13358+::
13359+:: Recover only the initializer of an already recognized direct program main.
13360+:: The derived call is evidence for an ordinary init/main retry, never an
13361+:: interface to publish on its own. Any failure returns the original resolution.
13362+++ program-init-context
13363+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13364+ ^- (unit iresolved)
13365+ =/ env=ienv env.resolution
13366+ ?^ (ienv-lookup %main env) ~
13367+ ?^ (ienv-lookup init.parts env) ~
13368+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
13369+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
13370+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
13371+ ?~ update ~
13372+ ?~ view ~
13373+ ?~ subs ~
13374+ =/ inits=(list def)
13375+ (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13376+ ?. ?=([* ~] inits) ~
13377+ =/ init-def=def i.inits
13378+ ?> ?=(%value -.init-def)
13379+ ?. (program-init-tuple-null init-def) ~
13380+ =/ args=(unit (list expr)) (program-main-args main)
13381+ ?~ args ~
13382+ ?~ prelude.initial ~
13383+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13384+ ?~ program ~
13385+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13386+ ?~ heads ~
13387+ =/ written=(unit def) (~(get by gates.u.heads) %program)
13388+ ?~ written ~
13389+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
13390+ ?~ written-sample ~
13391+ ?. ?=(%cell -.u.written-sample) ~
13392+ ?~ items.u.written-sample ~
13393+ =/ checked=(map term def) (direct-checked-gates ds env)
13394+ =/ templates=ienv
13395+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13396+ =/ scanned=(unit dgscan)
13397+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13398+ ?~ scanned ~
13399+ =. next.initial (dg-next-id ids.u.scanned 0)
13400+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
13401+ ?. ?=(%fn -.typ.instance) ~
13402+ ?. ?=(%cell -.sample.typ.instance) ~
13403+ =/ expected-init=(unit itype)
13404+ (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
13405+ ?~ expected-init ~
13406+ ?. ?=(%fn -.u.expected-init) ~
13407+ ?. ?=(%var -.sample.u.expected-init) ~
13408+ =/ data=@ud id.sample.u.expected-init
13409+ =/ init-var=itype [%var next.state.instance]
13410+ =/ st=istate state.instance(next +(next.state.instance))
13411+ =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
13412+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
13413+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
13414+ =. st state.sb(gate-defs checked, head-evidence heads)
13415+ =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
13416+ =/ fit=ifit
13417+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
13418+ ?. ?=(%ok -.fit) ~
13419+ =/ actual-final=itype (itype-normalize actual sub.fit)
13420+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
13421+ =/ open=(list @ud)
13422+ (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
13423+ ?. (levy open |=(n=@ud =(data n))) ~
13424+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
13425+ =/ replay=ifit
13426+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
13427+ ?. ?=(%ok -.replay) ~
13428+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
13429+ =/ expected=itype (itype-normalize u.expected-init sub.fit)
13430+ ?. ?=(%fn -.expected) ~
13431+ =. st st(sub sub.fit, next next.fit)
13432+ =/ init-state=istate (reserve-def-caps val.init-def st)
13433+ =/ inferred=iresult (infer-fragment val.init-def env init-state)
13434+ =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
13435+ ?: ?=(%| -.inferred) ~
13436+ ?. ?=(%fn -.typ.p.inferred) ~
13437+ =/ data-fit=ifit
13438+ (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
13439+ ?. ?=(%ok -.data-fit) ~
13440+ =/ closed=itype (itype-normalize expected sub.data-fit)
13441+ ?. ?=(%fn -.closed) ~
13442+ :: Resolve the ordinary tuple cast first, then check the complete gate.
13443+ :: General function fit remains unchanged; only this recovered candidate
13444+ :: receives the derived result context before its whole-type cast fit.
13445+ =/ product-fit=ifit
13446+ (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
13447+ ?. ?=(%ok -.product-fit) ~
13448+ =/ product=itype
13449+ (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
13450+ =/ actual-cast=itype [%fn sample.typ.p.inferred product]
13451+ =/ cast=ifit
13452+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13453+ ?. ?=(%ok -.cast) ~
13454+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13455+ =/ adjusted=iresult
13456+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13457+ =/ added=(unit iadded-definition)
13458+ (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13459+ ?~ added ~
13460+ =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13461+ ?~ recovered ~
13462+ ?. ?=(~ vars.u.recovered) ~
13463+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13464+ `[env.u.added grouped.resolution artifacts.u.added]
13465+::
13466+++ program-subs-watch
13467+ |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
13468+ ^- ?
13469+ ?. ?=(%value -.d) |
13470+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
13471+ =/ body=expr
13472+ ?- -.val.d
13473+ %gate body.val.d
13474+ %gate-wide body.val.d
13475+ * val.d
13476+ ==
13477+ =. body (program-transparent body)
13478+ ?. ?=(%list -.body) |
13479+ ?. ?=([* ~] items.body) |
13480+ =/ watch=expr (program-transparent i.items.body)
13481+ ?. ?=(%tuple -.watch) |
13482+ ?. ?=([* * ~] items.watch) |
13483+ =/ tag=item i.items.watch
13484+ =/ payload=item i.t.items.watch
13485+ ?. &(?=(~ face.tag) ?=(~ face.payload)) |
13486+ =/ tag-expr=expr (program-transparent val.tag)
13487+ ?. ?=(%lit -.tag-expr) |
13488+ ?. &(?=(%term form.lit.tag-expr) =(%watch val.lit.tag-expr)) |
13489+ =/ request=expr (program-transparent val.payload)
13490+ ?. ?=(%call -.request) |
13491+ ?. ?=([* ~] args.request) |
13492+ =/ head=expr (program-transparent head.request)
13493+ ?. ?=(%wing -.head) |
13494+ ?. ?=([@ @ ~] names.head) |
13495+ =/ case=term i.names.head
13496+ =/ face=term i.t.names.head
13497+ =/ callback=expr (program-transparent i.args.request)
13498+ ?. ?=(%ctor -.callback) |
13499+ ?. ?=(%term form.tag.callback) |
13500+ =/ selected=(list [face=term interface=ifile])
13501+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
13502+ ?. ?=([* ~] selected) |
13503+ =/ iface=ifile interface.i.selected
13504+ =/ member=(unit ischeme) (ienv-lookup case values.iface)
13505+ ?~ member |
13506+ ?~ source.iface |
13507+ =/ evidence=(list irequest-evidence)
13508+ (skim requests.graph |=(r=irequest-evidence &(=(api-at.r at.iface) =(name.r case))))
13509+ ?. ?=([* ~] evidence) |
13510+ =/ request-evidence=irequest-evidence i.evidence
13511+ ?. =(u.source.iface api-source.request-evidence) |
13512+ ?. =(name.path.path.request-evidence case) |
13513+ ?~ graph.iface |
13514+ ?. (lien requests.u.graph.iface |=(r=irequest-evidence =(r request-evidence))) |
13515+ ?. ?=(~ scry.path.path.request-evidence) |
13516+ ?. &(?=(~ diffs.path.request-evidence) ?=(~ diffs.path.path.request-evidence)) |
13517+ ?: (lien segments.path.path.request-evidence |=(p=pseg !?=(%knot -.p))) |
13518+ ?. ?=([@ ~] vars.u.member) |
13519+ =/ message=@ud i.vars.u.member
13520+ ?. ?=(%fn -.typ.u.member) |
13521+ ?. ?=(%fn -.sample.typ.u.member) |
13522+ ?. =(sample.sample.typ.u.member full.path.request-evidence) |
13523+ ?. =(product.sample.typ.u.member [%var message]) |
13524+ =/ prep=iprelude [prelude prelude-values.graph prelude-molds.graph]
13525+ =/ ask=(unit ischeme) (request-compatible-ask prep)
13526+ ?~ ask |
13527+ =/ result=(unit itype) (template-apply u.ask ~[[%var message]])
13528+ ?~ result |
13529+ =(product.typ.u.member u.result)
13530+::
13531+++ program-main-context
13532+ |= [main=def ds=(list def) resolution=iresolved initial=istate]
13533+ ^- iresolved
13534+ ?^ (ienv-lookup %main env.resolution) resolution
13535+ =/ heads=(unit igate-prelude-evidence)
13536+ (direct-prelude-evidence ds prelude.initial)
13537+ ?~ heads resolution
13538+ =/ checked=(map term def) (direct-checked-gates ds env.resolution)
13539+ =/ completed=[env=ienv artifacts=(list iwidth-definition)]
13540+ (add-supported-defs-core ~[main] ds checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
13541+ [env.completed grouped.resolution artifacts.completed]
13542+::
13543+++ program-main-closed
13544+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
13545+ ^- ?
13546+ ?~ prelude |
13547+ ?~ (ienv-lookup %program values.u.prelude) |
13548+ =/ program=(unit ischeme) (find-jibb-mold %program u.prelude)
13549+ ?~ program |
13550+ =/ main=(unit ischeme) (ienv-lookup %main env)
13551+ ?~ main |
13552+ ?. ?=(~ vars.u.main) |
13553+ ?. ?=(~ (itype-vars typ.u.main)) |
13554+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program *istate)
13555+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
13556+ ?. ?=(%ok -.main-fit) |
13557+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
13558+ ?~ init |
13559+ ?. ?=(~ vars.u.init) |
13560+ ?. ?=(%fn -.typ.u.init) |
13561+ ?. ?=(~ (itype-vars sample.typ.u.init)) |
13562+ ?. ?=(~ (itype-vars product.typ.u.init)) |
13563+ =/ data=igate-free (gate-free-type sample.typ.u.init 256 ~)
13564+ ?. =(%yes verdict.data) |
13565+ =/ model=igate-free (gate-free-type product.typ.u.init left.data ~)
13566+ ?. =(%yes verdict.model) |
13567+ =/ subs=(list def)
13568+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
13569+ ?. ?=([* ~] subs) |
13570+ |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
1069113571::
1069213572++ infer-jibb-file
1069313573 |= [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)]
1069413574 ^- jfile-result
13575+ =/ out=jfile-detailed-result
13576+ (infer-jibb-file-detailed at src externals mark-externals modules active prelude-values prelude-molds cache prelude)
13577+ ?: ?=(%| -.out) [%| message.p.out]
13578+ [%& p.out]
13579+:: Returns structured root-source overlap evidence after the same full check.
13580+++ infer-jibb-file-detailed
13581+ |= [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)]
13582+ ^- jfile-detailed-result
1069513583 =/ parsed (parse at src)
10696− ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
13584+ ?: ?=(%| -.parsed) [%| [(crip "module source does not parse: {(spud at)}") ~]]
1069713585 =/ mod=module p.parsed
1069813586 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
10699− ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
13587+ ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]
13588+ ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
13589+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
1070013590 ?: ?=([%ui %api *] at)
1070113591 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
10702− ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
10703− =/ checked=ifile u.iface(source `src)
10704− [%& [checked [[at checked] cache]]]
13592+ ?^ iface
13593+ =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
13594+ [%& [checked [[at checked] cache]]]
13595+ ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
13596+ =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
13597+ =/ narrow=?
13598+ ?. ?=([[%mark *] ~] imports.mod) |
13599+ ?. ?=([[%mold *] ~] defs.mod) |
13600+ ?. =(%paths name.i.defs.mod) |
13601+ !?=(%union -.shape.i.defs.mod)
13602+ ?: narrow
13603+ =/ request=(each ione-request-interface @t)
13604+ (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
13605+ ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
13606+ =/ checked=ifile iface.p.request
13607+ [%& [checked [[at checked] dependencies.paths.support.p.request]]]
13608+ =/ multi=(each [iface=ifile cache=jcache] @t)
13609+ (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
13610+ ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
13611+ [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
1070513612 ?. (module-scope-valid mod prelude-values prelude-molds)
1070613613 ?: (pending-declared-poke at mod prelude-values prelude-molds)
10707− [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
10708− [%| (crip "module has conflicting names: {(spud at)}")]
13614+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
13615+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1070913616 =/ vals=(list term) (global-value-names defs.mod)
10710− ?: (lien vals |=(n=term =(n %main)))
10711− [%| (crip "module kind needs unsupported inference: {(spud at)}")]
10712− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
13617+ =/ main=(unit def) (program-main-def defs.mod)
13618+ =/ main-parts=(unit [init=term update=term view=term subs=term])
13619+ ?~(main ~ (program-main-parts u.main))
13620+ ?. ?~(main & &(!?=([%ui %stores *] at) ?=(^ main-parts)))
13621+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
13622+ =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
1071313623 ?: ?=(%| -.js) [%| p.js]
10714− =/ molds=imolds (collect-simple-molds defs.mod)
13624+ =/ collected=grec-collected
13625+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
13626+ (grec-collect-molds defs.mod)
13627+ =/ molds=imolds molds.collected
1071513628 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
1071613629 =/ surs=(list term) (collect-sur-imports imports.mod)
1071713630 =/ marks=(list term) (collect-mark-imports imports.mod)
1071813631 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
1071913632 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10720− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
10721− =/ mts=(each imold-types @t) (module-mold-types molds state)
10722− ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
10723− =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
13633+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
13634+ :: Source and scope were checked above; preserve that exact root and prelude.
13635+ :: This first integration only indexes import-free library sources.
13636+ =/ index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])
13637+ ?^ imports.mod ~
13638+ ?~ prelude ~
13639+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude)
13640+ ?~ standard ~
13641+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~
13642+ =/ index=(map term shape) proofs.collected
13643+ ?. !=(index *(map term shape)) ~
13644+ ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~
13645+ `[at src u.prelude index]
13646+ =. grec-index.state index
13647+ =/ mts=(each imold-types imold-failure) (module-mold-types-detail molds state)
13648+ ?: ?=(%| -.mts)
13649+ ?~ overlap.p.mts [%| [(crip "{(trip message.p.mts)}: {(spud at)}") ~]]
13650+ =/ witness=[name=term cases=upair] u.overlap.p.mts
13651+ =/ first=@t (show-error src [at line.beg.first.cases.witness col.beg.first.cases.witness "first union case"])
13652+ =/ second=@t (show-error src [at line.beg.second.cases.witness col.beg.second.cases.witness "overlapping case"])
13653+ =/ msg=@t (of-wain:format ~[(crip "module mold {(trip name.witness)} has overlapping cases") first second])
13654+ [%| [msg `[at src name.witness cases.witness]]]
13655+ =/ resolution=iresolved
13656+ ?~ index
13657+ (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
13658+ (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
1072413659 =/ env=ienv env.resolution
13660+ =/ recovered=iresolved
13661+ ?~ main resolution
13662+ ?~ main-parts resolution
13663+ =/ updated=(unit iresolved)
13664+ (program-update-context u.main u.main-parts defs.mod resolution state)
13665+ =/ with-update=iresolved ?~(updated resolution u.updated)
13666+ =/ subscribed=(unit iresolved)
13667+ (program-subs-context u.main-parts defs.mod with-update state)
13668+ =/ with-subs=iresolved ?~(subscribed with-update u.subscribed)
13669+ =/ viewed=(unit iresolved)
13670+ (program-view-context u.main-parts defs.mod with-subs state)
13671+ =/ with-view=iresolved ?~(viewed with-subs u.viewed)
13672+ =/ initialized=(unit iresolved)
13673+ (program-init-context u.main u.main-parts defs.mod with-view state)
13674+ =/ components=iresolved ?~(initialized with-view u.initialized)
13675+ (program-main-context u.main defs.mod components state)
13676+ =. env env.recovered
13677+ =. artifacts.resolution artifacts.recovered
13678+ =. env
13679+ ?: (module-values-complete defs.mod env) env
13680+ ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
13681+ ?: (gth (met 3 src) 65.536) env
13682+ ?: (gth (lent defs.mod) 64) env
13683+ ?. (dg-source-candidate defs.mod 64) env
13684+ =/ transaction=(unit dgcommit) (dg-root-source at src)
13685+ ?~ transaction env
13686+ ?: (dg-interface-safe env.u.transaction) env.u.transaction
13687+ env
1072513688 ?. (module-values-complete defs.mod env)
10726− [%| (crip "module definitions need unsupported inference: {(spud at)}")]
10727− =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src]
13689+ [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
13690+ =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
13691+ =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
13692+ ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
13693+ ?. ?~(main & ?~(main-parts | (program-main-closed u.main-parts defs.mod env prelude resolved.p.js u.graph)))
13694+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
13695+ =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
1072813696 [%& [iface [[at iface] cache.p.js]]]
1072913697::
13698+:: A source-bound analysis of one named mold, not a module, island,
13699+:: request, watchability or runtime check. The host owns the trusted
13700+:: prepared prelude, canonical paths and reader/source version identities.
13701+:: The 256-node cap covers only classification, not source/graph work.
13702++$ igate-free-mold
13703+ [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]
13704+++ gate-free-mold-source
13705+ |= [file=path src=@t name=term externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude) fuel=@ud]
13706+ ^- (each igate-free-mold @t)
13707+ ?~ file [%| 'mold analysis needs a path ending in jibb']
13708+ ?. =(%jibb (rear file)) [%| 'mold analysis needs a path ending in jibb']
13709+ ?: |(=(file /lib/jibb/internal/jibb) =(file /lib/jibb/primitives/jibb))
13710+ [%| 'the prelude internal modules are private']
13711+ ?: ?=([%ui %api *] file) [%| 'API declarations need unsupported mold analysis']
13712+ ?: ?=([%ui %stores *] file) [%| 'store declarations need unsupported mold analysis']
13713+ =/ entries=jbundle (skim modules |=(m=jsource =(file at.m)))
13714+ ?: (gth (lent entries) 1) [%| 'duplicate root module sources']
13715+ =/ wrong-root=? ?~(entries | !=(source.i.entries src))
13716+ ?: wrong-root [%| 'root module source does not match bundle']
13717+ =/ parsed (parse file src)
13718+ ?: ?=(%| -.parsed) [%| 'mold source does not parse']
13719+ =/ mod=module p.parsed
13720+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
13721+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
13722+ ?~ prepared [%| 'mold analysis needs the prepared prelude']
13723+ ?. (module-scope-valid mod values.u.prepared molds.u.prepared)
13724+ [%| 'mold source has conflicting or unsupported scope']
13725+ =/ selected=(list def)
13726+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(name.d name))))
13727+ ?~ selected [%| 'selected mold is not declared']
13728+ ?^ t.selected [%| 'selected mold is not unique']
13729+ ?> ?=(%mold -.i.selected)
13730+ =/ public=ifile iface.u.prepared
13731+ =/ js=jimports-result
13732+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
13733+ ?: ?=(%| -.js) [%| p.js]
13734+ =/ ms=imolds (collect-simple-molds defs.mod)
13735+ =/ vals=(list term) (global-value-names defs.mod)
13736+ =/ globals=(list term) (weld values.u.prepared (weld (import-binding-names imports.mod) vals))
13737+ =/ surs=(list term) (collect-sur-imports imports.mod)
13738+ =/ declared=(list term) (collect-mark-imports imports.mod)
13739+ =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
13740+ =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))
13741+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~ ~ ~ ~ ~ ~]
13742+ =/ inferred=(unit [template=ischeme state=istate])
13743+ (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
13744+ ?~ inferred [%| 'selected mold needs unsupported inference']
13745+ =/ template=ischeme template.u.inferred
13746+ =. typ.template (label-direct-union typ.template shape.i.selected name state)
13747+ =. typ.template (itype-normalize typ.template sub.state.u.inferred)
13748+ =/ cap=@ud (min fuel 256)
13749+ =/ analysis=igate-free (gate-free-type typ.template cap ~)
13750+ [%& [file src name u.prepared externals marks modules cache.p.js template fuel cap analysis]]
13751+::
1073013752:: +golden-types-with-modules fails closed for imports without prelude
1073113753:: scope. +golden-types-with-prelude resolves supported library graphs;
1073213754:: its report remains partial and unreachable sources are not examined.
@@ -10787,7 +13809,7 @@
1078713809 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
1078813810 =/ scope-values=(list term)
1078913811 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
10790− (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
13812+ (golden-types-in-context-core file src externals mark-externals resolved.p.js scope-values prelude-molds iface prepared)
1079113813::
1079213814:: +golden-types-with-marks: supply declared mark types separately from /sur
1079313815:: entries, as [mark result] with the result from +read-mark:jibb-import.
@@ -10818,6 +13840,10 @@
1081813840++ golden-types-in-context
1081913841 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
1082013842 ^- @t
13843+ (golden-types-in-context-core file src externals mark-externals jimports prelude-values reserved-molds prelude ~)
13844+++ golden-types-in-context-core
13845+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile) prepared=(unit iprelude)]
13846+ ^- @t
1082113847 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
1082213848 =/ parsed (parse file src)
1082313849 ?: ?=(%| -.parsed) (show-error src p.parsed)
@@ -10833,6 +13859,41 @@
1083313859 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
1083413860 =/ cycles=(list icycle) (definite-value-cycles ds globals)
1083513861 =/ env=ienv env.resolution
13862+ =/ recovered=(list term) ~
13863+ =/ eligible=?
13864+ ?& ?=(~ imports.p.parsed)
13865+ ?=(~ jimports)
13866+ !?=([%ui %api *] file)
13867+ !?=([%ui %stores *] file)
13868+ !(lien (global-value-names ds) |=(n=term =(n %main)))
13869+ !(module-values-complete ds env)
13870+ (lte (met 3 src) 65.536)
13871+ (lte (lent ds) 64)
13872+ ?| &(?=(~ prepared) ?=(~ prelude) ?=(~ prelude-values) ?=(~ reserved-molds) (module-scope-valid p.parsed ~ ~) (dg-source-candidate ds 64))
13873+ ?& ?=(^ prepared)
13874+ ?=(^ prelude)
13875+ =(u.prelude iface.u.prepared)
13876+ =(prelude-values values.u.prepared)
13877+ =(reserved-molds molds.u.prepared)
13878+ (module-scope-valid p.parsed values.u.prepared molds.u.prepared)
13879+ (dg-prepared-candidate ds 64)
13880+ ==
13881+ ==
13882+ ==
13883+ =/ transaction=(unit dgcommit)
13884+ ?. eligible ~
13885+ ?~ prepared (dg-root-source file src)
13886+ (dg-root-prepared file src u.prepared)
13887+ =. recovered
13888+ ?~ transaction ~
13889+ ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
13890+ (turn (skim env.u.transaction |=(entry=[name=term scheme=ischeme] ?=(~ (ienv-lookup name.entry env)))) |=(entry=[name=term scheme=ischeme] name.entry))
13891+ =. env
13892+ ?~ transaction env
13893+ ?: &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) env.u.transaction
13894+ env
13895+ =/ source-defs=(map term def) (direct-checked-gates ds env)
13896+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1083613897 =/ lines=(list @t) ~
1083713898 |-
1083813899 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -10845,6 +13906,16 @@
1084513906 ?^ cycle
1084613907 =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
1084713908 $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
13909+ ?: (lien recovered |=(n=term =(n name.d)))
13910+ =/ found=(unit ischeme) (ienv-lookup name.d env)
13911+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: committed definition unavailable") lines])
13912+ ?: (itype-has-hidden-recursive typ.u.found)
13913+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
13914+ ?: (itype-has-hidden-generic typ.u.found)
13915+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
13916+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
13917+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
13918+ $(ds t.ds, lines [line lines])
1084813919 ?: (lien grouped.resolution |=(n=term =(n name.d)))
1084913920 =/ found=(unit ischeme) (ienv-lookup name.d env)
1085013921 ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
@@ -10852,7 +13923,9 @@
1085213923 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
1085313924 $(ds t.ds, lines [line lines])
1085413925 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10855− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~]
13926+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
13927+ =. gate-defs.initial source-defs
13928+ =. head-evidence.initial heads
1085613929 =. initial (reserve-def-caps val.d initial)
1085713930 =/ result=iresult
1085813931 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -10892,4 +13965,667 @@
1089213965 =/ printable=itype (canonical-itype typ vars)
1089313966 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
1089413967 $(ds t.ds, lines [line lines])
13968+:: Experimental module-owned pending-constraint generalization only.
13969+:: Inputs, IDs and substitution come from one checker-owned transaction.
13970++$ dgscan [ids=(list @ud) fuel=@ud]
13971+++ dg-scan
13972+ |= [todo=(list itype) sub=isub fuel=@ud ids=(list @ud)]
13973+ ^- (unit dgscan)
13974+ ?~ todo `[ids fuel]
13975+ ?: =(0 fuel) ~
13976+ =. fuel (dec fuel)
13977+ =/ t=itype i.todo
13978+ ?: ?=(?(%var %avar %rvar %nvar %rnvar %tag) -.t)
13979+ =/ node-id=@ud ?:(?=(%tag -.t) id.t +.t)
13980+ =/ found=(unit itype) (itype-lookup node-id sub)
13981+ ?~ found $(todo t.todo, ids [node-id ids])
13982+ ?: &(?=(?(%rvar %rnvar) -.u.found) =(node-id +.u.found))
13983+ $(todo t.todo, ids [node-id ids])
13984+ $(todo [u.found t.todo])
13985+ ?: ?=(%jrec -.t) $(todo t.todo)
13986+ ?+ -.t ~
13987+ %collection $(todo (weld args.t t.todo))
13988+ %union $(todo (weld args.t (weld cases.t t.todo)))
13989+ %face $(todo [body.t t.todo])
13990+ %fn $(todo [sample.t product.t t.todo])
13991+ %cell $(todo [hed.t tal.t t.todo])
13992+ %atom $(todo t.todo)
13993+ %any-atom $(todo t.todo)
13994+ %flag $(todo t.todo)
13995+ %noun $(todo t.todo)
13996+ %empty $(todo t.todo)
13997+ %const $(todo t.todo)
13998+ ==
13999+::
14000+++ dg-scan-ids
14001+ |= [ids=(list @ud) sub=isub fuel=@ud blocked=(list @ud)]
14002+ ^- (unit dgscan)
14003+ ?~ ids `[blocked fuel]
14004+ =/ one=(unit dgscan) (dg-scan ~[[%var i.ids]] sub fuel blocked)
14005+ ?~ one ~
14006+ $(ids t.ids, fuel fuel.u.one, blocked ids.u.one)
14007+::
14008+++ dg-env
14009+ |= [env=ienv sub=isub fuel=@ud blocked=(list @ud)]
14010+ ^- (unit dgscan)
14011+ ?~ env `[blocked fuel]
14012+ =/ sc=ischeme scheme.i.env
14013+ :: Quantifiers are local to the scheme: first find raw free IDs, then
14014+ :: follow those IDs in the module substitution without capturing them.
14015+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ fuel ~)
14016+ ?~ raw ~
14017+ =/ free=(list @ud) (skim ids.u.raw |=(n=@ud !(lien vars.sc |=(q=@ud =(q n)))))
14018+ =/ resolved=(unit dgscan) (dg-scan-ids free sub fuel.u.raw blocked)
14019+ ?~ resolved ~
14020+ $(env t.env, fuel fuel.u.resolved, blocked ids.u.resolved)
14021+::
14022+++ dg-obligations
14023+ |= [pending=(list dgo) sub=isub fuel=@ud blocked=(list @ud)]
14024+ ^- (unit dgscan)
14025+ ?~ pending `[blocked fuel]
14026+ =/ found=(unit dgscan) (dg-scan ~[left.i.pending right.i.pending] sub fuel blocked)
14027+ ?~ found ~
14028+ $(pending t.pending, fuel fuel.u.found, blocked ids.u.found)
14029+::
14030+++ dg-tags
14031+ |= [tags=(list ipending) sub=isub fuel=@ud blocked=(list @ud)]
14032+ ^- (unit dgscan)
14033+ ?~ tags `[blocked fuel]
14034+ ?: =(0 fuel) ~
14035+ =/ found=(unit itype) (itype-lookup id.i.tags sub)
14036+ ?~ found $(tags t.tags, fuel (dec fuel), blocked [id.i.tags blocked])
14037+ :: Until this entry is explicitly discharged, retain variables reachable
14038+ :: through its binding; mere existence of a substitution is not proof.
14039+ =/ reached=(unit dgscan) (dg-scan ~[u.found] sub (dec fuel) blocked)
14040+ ?~ reached ~
14041+ $(tags t.tags, fuel fuel.u.reached, blocked ids.u.reached)
14042+::
14043+++ dg-generalize
14044+ |= [typ=itype env=ienv pending=(list dgo) tags=(list ipending) captured=(list @ud) state=istate fuel=@ud]
14045+ ^- (unit ischeme)
14046+ :: Bound the obligation list and all graph/substitution walks. The
14047+ :: substitution is assumed checker-owned and occurs-checked.
14048+ ?: (gth (lent pending) 64) ~
14049+ =/ capt=(unit dgscan) (dg-scan-ids captured sub.state fuel ~)
14050+ ?~ capt ~
14051+ =/ env-free=(unit dgscan) (dg-env env sub.state fuel.u.capt ids.u.capt)
14052+ ?~ env-free ~
14053+ =/ obligations=(unit dgscan) (dg-obligations pending sub.state fuel.u.env-free ids.u.env-free)
14054+ ?~ obligations ~
14055+ =/ tagged=(unit dgscan) (dg-tags tags sub.state fuel.u.obligations ids.u.obligations)
14056+ ?~ tagged ~
14057+ =/ bounded=(unit dgscan) (dg-scan ~[typ] sub.state fuel.u.tagged ~)
14058+ ?~ bounded ~
14059+ =/ normalized=itype (itype-normalize typ sub.state)
14060+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
14061+ =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
14062+ `[[normalized quantified]]
14063+::
14064++$ dgcommit [env=ienv state=istate]
14065+:: A branch literal must not acquire a value face through replay.
14066+++ dg-literal-target-safe
14067+ |= target=itype
14068+ ^- ?
14069+ ?: ?=(%union -.target)
14070+ (levy cases.target |=(c=itype ?=(?(%const %cell) -.c)))
14071+ ?=(?(%const %atom %any-atom %flag %noun) -.target)
14072+::
14073+++ dg-replay-edges
14074+ |= [edges=(list dgo) state=istate fuel=@ud]
14075+ ^- (unit istate)
14076+ ?~ edges `state
14077+ ?: =(0 fuel) ~
14078+ =/ trial=ifit (itype-fit left.i.edges right.i.edges sub.state next.state)
14079+ ?. ?=(%ok -.trial) ~
14080+ =/ valid=?
14081+ ?: ?=(%tag -.left.i.edges)
14082+ ?. constructor.left.i.edges
14083+ =/ closed=(unit dgscan) (dg-scan ~[right.i.edges] sub.trial 512 ~)
14084+ ?~ closed |
14085+ ?^ ids.u.closed |
14086+ (dg-literal-target-safe (itype-normalize right.i.edges sub.trial))
14087+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
14088+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
14089+ ?. valid ~
14090+ $(edges t.edges, state state(sub sub.trial, next next.trial), fuel (dec fuel))
14091+::
14092+++ dg-close-env
14093+ |= [env=ienv sub=isub fuel=@ud]
14094+ ^- (unit ienv)
14095+ ?~ env `~
14096+ ?: =(0 fuel) ~
14097+ =/ s=ischeme scheme.i.env
14098+ :: Quantified IDs are scheme-local and cannot be rewritten on publication.
14099+ ?. (levy vars.s |=(n=@ud ?=(~ (itype-lookup n sub)))) ~
14100+ =/ bounded=(unit dgscan) (dg-scan ~[typ.s] sub (dec fuel) ~)
14101+ ?~ bounded ~
14102+ =/ normalized=itype (itype-normalize typ.s sub)
14103+ ?: (itype-has-tag normalized) ~
14104+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
14105+ ?. (levy vars |=(n=@ud (lien vars.s |=(v=@ud =(v n))))) ~
14106+ =/ rest=(unit ienv) (dg-close-env t.env sub fuel.u.bounded)
14107+ ?~ rest ~
14108+ `[[name.i.env [normalized vars.s]] u.rest]
14109+::
14110+:: A deferred boolean branch has exactly the two literal flag patterns.
14111+:: Arms are inferred in order. Equal types are retained; two direct pending
14112+:: literals may instead retain source-owned obligations for later context.
14113+++ dg-boolean-patterns
14114+ |= e=expr
14115+ ^- ?
14116+ ?. ?=(%branch -.e) |
14117+ ?~ arms.e |
14118+ ?~ t.arms.e |
14119+ ?^ t.t.arms.e |
14120+ =/ x=arm i.arms.e
14121+ =/ y=arm i.t.arms.e
14122+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) |
14123+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) |
14124+ !=(val.lit.pat.x val.lit.pat.y)
14125+:: Only a direct source literal which created its own unbound pending tag
14126+:: may create a branch edge. The caller must retain the exact source and state.
14127+++ dg-owned-arm-literal
14128+ |= [e=expr t=itype tags=(list ipending) sub=isub initial=@ud]
14129+ ^- ?
14130+ ?. ?=(%lit -.e) |
14131+ ?. ?=(%tag -.t) |
14132+ ?: constructor.t |
14133+ ?. =(lit.e literal.t) |
14134+ ?: (lth id.t initial) |
14135+ ?^ (itype-lookup id.t sub) |
14136+ (lien tags |=(x=ipending &(=(id.x id.t) =(literal.x literal.t))))
14137+++ dg-boolean-branch
14138+ |= [e=expr env=ienv state=istate]
14139+ ^- iresult
14140+ ?. (dg-boolean-patterns e) [%| ["deferred branch patterns need unsupported inference" ~]]
14141+ ?> ?=(%branch -.e)
14142+ ?> ?=(^ arms.e)
14143+ ?> ?=(^ t.arms.e)
14144+ =/ x=arm i.arms.e
14145+ =/ y=arm i.t.arms.e
14146+ =/ subject=iresult (infer-fragment subject.e env state)
14147+ ?: ?=(%| -.subject) subject
14148+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
14149+ ?~ su [%| ["deferred branch subject does not unify with ?" ~]]
14150+ =/ left=iresult (infer-fragment val.x env state.p.subject(sub u.su))
14151+ ?: ?=(%| -.left) left
14152+ =/ right=iresult (infer-fragment val.y env state.p.left)
14153+ ?: ?=(%| -.right) right
14154+ ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)
14155+ =/ st=istate state.p.right
14156+ ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)
14157+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14158+ ?. (dg-owned-arm-literal val.y typ.p.right tags.st sub.st next.state)
14159+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14160+ ?> ?=(%tag -.typ.p.left)
14161+ ?> ?=(%tag -.typ.p.right)
14162+ ?: =(id.typ.p.left id.typ.p.right)
14163+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14164+ ?: (gth (lent obligations.st) 62)
14165+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14166+ =/ result=itype [%var next.st]
14167+ =/ ex=dgo [typ.p.left result (span-of val.x) (span-of e)]
14168+ =/ ey=dgo [typ.p.right result (span-of val.y) (span-of e)]
14169+ [%& result st(next +(next.st), obligations [ex ey obligations.st])]
14170+ [%& typ.p.left state.p.right]
14171+::
14172+:: A direct tuple literal may wait for a later exact result context.
14173+:: Each pending literal retains its source tag and its own fit obligation.
14174+++ dg-infer-tuple-items
14175+ |= [items=(list item) env=ienv state=istate]
14176+ ^- iresult
14177+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
14178+ =/ head=iresult (infer-fragment val.i.items env state)
14179+ ?: ?=(%| -.head) head
14180+ =/ typ=itype typ.p.head
14181+ =/ st=istate state.p.head
14182+ =/ adjusted=(unit [typ=itype state=istate])
14183+ ?. (dg-owned-arm-literal val.i.items typ tags.st sub.st next.state) `[typ st]
14184+ ?: (gth (lent obligations.st) 63) ~
14185+ =/ pending=itype [%var next.st]
14186+ =/ edge=dgo [typ pending (span-of val.i.items) at.i.items]
14187+ `[pending st(next +(next.st), obligations [edge obligations.st])]
14188+ ?~ adjusted [%| ["deferred tuple context needs unsupported inference" ~]]
14189+ =. typ typ.u.adjusted
14190+ =. st state.u.adjusted
14191+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
14192+ ?~ t.items [%& typ st]
14193+ =/ tail=iresult $(items t.items, state st)
14194+ ?: ?=(%| -.tail) tail
14195+ [%& [%cell typ typ.p.tail] state.p.tail]
14196+::
14197+:: Deferred inference uses only source forms whose successful fit sites are
14198+:: guarded below; a shared source-node budget bounds this screen.
14199+++ dg-safe-expressions
14200+ |= [todo=(list expr) fuel=@ud]
14201+ ^- (unit @ud)
14202+ ?~ todo `fuel
14203+ =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
14204+ ?~ first ~
14205+ $(todo t.todo, fuel u.first)
14206+++ dg-safe-items
14207+ |= [items=(list item) fuel=@ud]
14208+ ^- (unit @ud)
14209+ ?~ items `fuel
14210+ =/ first=(unit @ud) (dg-safe-expression val.i.items fuel)
14211+ ?~ first ~
14212+ $(items t.items, fuel u.first)
14213+++ dg-safe-expression
14214+ |= [e=expr fuel=@ud]
14215+ ^- (unit @ud)
14216+ ?: =(0 fuel) ~
14217+ =. fuel (dec fuel)
14218+ ?+ -.e ~
14219+ ?(%lit %ctor) `fuel
14220+ %wing ?:(?=([@ ~] names.e) `fuel ~)
14221+ %str
14222+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) ~
14223+ `fuel
14224+ %group $(e inner.e, fuel fuel)
14225+ %body
14226+ ?^ defs.e ~
14227+ $(e final.e, fuel fuel)
14228+ %gate $(e body.e, fuel fuel)
14229+ %gate-wide $(e body.e, fuel fuel)
14230+ %tuple (dg-safe-items items.e fuel)
14231+ %branch
14232+ ?. (dg-boolean-patterns e) ~
14233+ ?> ?=(^ arms.e)
14234+ ?> ?=(^ t.arms.e)
14235+ =/ subject=(unit @ud) $(e subject.e, fuel fuel)
14236+ ?~ subject ~
14237+ (dg-safe-expressions ~[val.i.arms.e val.i.t.arms.e] u.subject)
14238+ %cast $(e val.e, fuel fuel)
14239+ %call
14240+ =/ head=(unit @ud) $(e head.e, fuel fuel)
14241+ ?~ head ~
14242+ (dg-safe-expressions args.e u.head)
14243+ ==
14244+:: Exact normalized equality is preserved by all later substitutions.
14245+:: The bounded scan declines opaque types and oversized inputs.
14246+++ dg-stable-fit
14247+ |= [actual=itype expected=itype sub=isub]
14248+ ^- ?
14249+ ?~ (dg-scan ~[actual expected] sub 512 ~) |
14250+ =((itype-normalize actual sub) (itype-normalize expected sub))
14251+::
14252+:: A positional call peels sample-slot faces during its separate face check.
14253+:: Require its argument, sample and result closed so that check stays valid.
14254+++ dg-stable-call-fit
14255+ |= [actual=itype expected=itype product=itype sub=isub positional=?]
14256+ ^- ?
14257+ =/ checked=(unit dgscan) (dg-scan ~[actual expected product] sub 512 ~)
14258+ ?~ checked |
14259+ ?: &(positional ?=(^ ids.u.checked)) |
14260+ =((itype-normalize actual sub) (itype-normalize expected sub))
14261+::
14262+:: One definition attempt retains state only when inference succeeds.
14263++$ dg-step [env=ienv state=istate pending=(list dgo)]
14264+++ dg-stage-one
14265+ |= [d=def env=ienv state=istate]
14266+ ^- (unit dg-step)
14267+ ?> ?=(%value -.d)
14268+ ?~ (dg-safe-expression val.d 512) ~
14269+ =/ local=istate (reserve-def-caps val.d state)
14270+ :: This first slice declines all written capitals and holes/projections.
14271+ ?^ caps.local ~
14272+ =/ ordinary=iresult (infer-fragment val.d env local)
14273+ ?: ?=(%| -.ordinary) ~
14274+ =/ typ=itype typ.p.ordinary
14275+ =/ after=istate state.p.ordinary
14276+ =/ edges=(list dgo) obligations.after
14277+ ?. =(binders.after binders.state) ~
14278+ ?. =(molds.after molds.state) ~
14279+ ?. =(globals.after globals.state) ~
14280+ ?. =(externals.after externals.state) ~
14281+ ?. =(surs.after surs.state) ~
14282+ ?. =(mark-externals.after mark-externals.state) ~
14283+ ?. =(marks.after marks.state) ~
14284+ ?. =(jimports.after jimports.state) ~
14285+ ?. =(reserved-molds.after reserved-molds.state) ~
14286+ ?. =(params.after params.state) ~
14287+ ?. =(active.after active.state) ~
14288+ ?. =(in-mold.after in-mold.state) ~
14289+ ?. =(at.after at.state) ~
14290+ ?. =(top-molds.after top-molds.state) ~
14291+ ?. =(prelude.after prelude.state) ~
14292+ ?. =(gate-defs.after gate-defs.state) ~
14293+ ?. =(head-evidence.after head-evidence.state) ~
14294+ ?. =(grec-index.after grec-index.state) ~
14295+ ?. =(defer.after defer.state) ~
14296+ ?. =(holes.after holes.state) ~
14297+ ?. =(caps.after caps.state) ~
14298+ ?. =(projections.after projections.state) ~
14299+ ?: (unsupported-atom-vars (itype-normalize typ sub.after) caps.after binders.after sub.after) ~
14300+ ?: (itype-has-nvar (itype-normalize typ sub.after)) ~
14301+ =/ scheme=(unit ischeme) (dg-generalize typ env edges tags.after ~ after 32.768)
14302+ ?~ scheme ~
14303+ `[[[name.d u.scheme] env] after edges]
14304+:: Retry only definitions that did not infer. Successful definitions are
14305+:: committed into the local transaction, never published until all close.
14306+++ dg-stage
14307+ |= [ds=(list def) base=ienv env=ienv state=istate pending=(list dgo) fuel=@ud]
14308+ ^- (unit dgcommit)
14309+ ?: (gth fuel 64) ~
14310+ ?: (gth (lent ds) fuel) ~
14311+ =/ remaining=(list def) ds
14312+ =/ waiting=(list def) ~
14313+ =/ progress=? |
14314+ =/ attempts=@ud (mul fuel fuel)
14315+ |-
14316+ ?~ remaining
14317+ ?^ waiting
14318+ ?. progress ~
14319+ $(remaining (flop waiting), waiting ~, progress |)
14320+ =/ replayed=(unit istate) (dg-replay-edges pending state 64)
14321+ ?~ replayed ~
14322+ ?: (pending-tags tags.u.replayed sub.u.replayed) ~
14323+ =/ closed-edges=(unit dgscan) (dg-obligations pending sub.u.replayed 32.768 ~)
14324+ ?~ closed-edges ~
14325+ ?^ ids.u.closed-edges ~
14326+ =/ rechecked=(unit istate) (dg-replay-edges pending u.replayed 64)
14327+ ?~ rechecked ~
14328+ ?. =(sub.u.rechecked sub.u.replayed) ~
14329+ ?. =(next.u.rechecked next.u.replayed) ~
14330+ =/ closed=(unit ienv) (dg-close-env env sub.u.replayed 32.768)
14331+ ?~ closed ~
14332+ `[[u.closed u.replayed(defer ~, obligations ~)]]
14333+ ?: =(0 attempts) ~
14334+ =. attempts (dec attempts)
14335+ =/ d=def i.remaining
14336+ ?: ?=(%mold -.d) $(remaining t.remaining)
14337+ ?^ (ienv-lookup name.d base) $(remaining t.remaining)
14338+ ?^ (ienv-lookup name.d env) ~
14339+ =/ done=(unit dg-step) (dg-stage-one d env state)
14340+ ?~ done $(remaining t.remaining, waiting [d waiting])
14341+ $(remaining t.remaining, env env.u.done, state state.u.done, pending pending.u.done, progress &)
14342+::
14343+:: Cheap bounded eligibility check on the already parsed source. This
14344+:: deliberately covers only direct constructor calls beneath transparent
14345+:: groups, gates, casts and definition-free bodies. Other shapes decline
14346+:: this fallback without a second parse or resolution pass.
14347+++ dg-direct-source
14348+ |= [e=expr fuel=@ud]
14349+ ^- ?
14350+ ?: =(0 fuel) |
14351+ ?+ -.e |
14352+ %group $(e inner.e, fuel (dec fuel))
14353+ %gate $(e body.e, fuel (dec fuel))
14354+ %gate-wide $(e body.e, fuel (dec fuel))
14355+ %cast $(e val.e, fuel (dec fuel))
14356+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
14357+ %call
14358+ ?. ?=([* ~] args.e) |
14359+ ?=(%ctor -.i.args.e)
14360+ ==
14361+++ dg-source-candidate
14362+ |= [ds=(list def) fuel=@ud]
14363+ ^- ?
14364+ ?~ ds |
14365+ ?: =(0 fuel) |
14366+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
14367+ ?: (dg-direct-source val.i.ds 64) &
14368+ $(ds t.ds, fuel (dec fuel))
14369+::
14370+++ dg-prepared-source
14371+ |= [e=expr fuel=@ud]
14372+ ^- ?
14373+ ?: (dg-direct-source e fuel) &
14374+ ?: =(0 fuel) |
14375+ ?+ -.e |
14376+ %group $(e inner.e, fuel (dec fuel))
14377+ %gate $(e body.e, fuel (dec fuel))
14378+ %gate-wide $(e body.e, fuel (dec fuel))
14379+ %cast $(e val.e, fuel (dec fuel))
14380+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
14381+ %tuple &
14382+ ==
14383+++ dg-prepared-candidate
14384+ |= [ds=(list def) fuel=@ud]
14385+ ^- ?
14386+ ?~ ds |
14387+ ?: =(0 fuel) |
14388+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
14389+ ?: (dg-prepared-source val.i.ds 64) &
14390+ $(ds t.ds, fuel (dec fuel))
14391+::
14392+++ dg-interface-safe
14393+ |= [env=ienv]
14394+ ^- ?
14395+ ?~ env &
14396+ =/ sc=ischeme scheme.i.env
14397+ ?: |((itype-has-hidden-recursive typ.sc) (itype-has-hidden-generic typ.sc)) |
14398+ ?: (gth (lent vars.sc) 26) |
14399+ $(env t.env)
14400+:: Parse status and the transaction result come from the same source parse.
14401++$ dgparse [parsed=? result=(unit dgcommit)]
14402+++ dg-root-source
14403+ |= [at=path src=@t]
14404+ ^- (unit dgcommit)
14405+ result:(dg-root-detail at src)
14406+++ dg-root-detail
14407+ |= [at=path src=@t]
14408+ ^- dgparse
14409+ =/ parsed (parse at src)
14410+ ?: ?=(%| -.parsed) [| ~]
14411+ =/ transact
14412+ |.
14413+ ?^ imports.p.parsed ~
14414+ ?. (module-scope-valid p.parsed ~ ~) ~
14415+ ?^ (duplicate-defs defs.p.parsed) ~
14416+ =/ defs=(list def) defs.p.parsed
14417+ ?: (gth (lent defs) 64) ~
14418+ =/ molds=imolds (collect-simple-molds defs)
14419+ =/ globals=(list term) (global-value-names defs)
14420+ =/ resolution=iresolved (resolve-groups defs molds globals ~ ~ ~ ~ ~ ~ at ~)
14421+ ?^ grouped.resolution ~
14422+ ?^ artifacts.resolution ~
14423+ =/ base=ienv env.resolution
14424+ =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)
14425+ ?~ free ~
14426+ ?^ ids.u.free ~
14427+ =/ all=(unit dgscan) (dg-all-env-ids base 32.768 ~)
14428+ ?~ all ~
14429+ =/ fresh=@ud (dg-next-id ids.u.all 0)
14430+ =/ st=istate *istate
14431+ =. 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)
14432+ =/ checked-molds=(each imold-types @t) (module-mold-types molds st)
14433+ ?: ?=(%| -.checked-molds) ~
14434+ (dg-stage defs base base st ~ 64)
14435+ ::
14436+ [& (transact)]
14437+:: The caller supplies the trusted prepared prelude. This transaction is
14438+:: only report evidence; the ordinary module resolver does not publish it.
14439+++ dg-root-prepared
14440+ |= [at=path src=@t prepared=iprelude]
14441+ ^- (unit dgcommit)
14442+ ?: ?=([%ui %api *] at) ~
14443+ ?: ?=([%ui %stores *] at) ~
14444+ ?: (gth (met 3 src) 65.536) ~
14445+ =/ parsed (parse at src)
14446+ ?: ?=(%| -.parsed) ~
14447+ ?^ imports.p.parsed ~
14448+ ?. (module-scope-valid p.parsed values.prepared molds.prepared) ~
14449+ ?^ (duplicate-defs defs.p.parsed) ~
14450+ =/ defs=(list def) defs.p.parsed
14451+ ?: (gth (lent defs) 64) ~
14452+ ?: (lien (global-value-names defs) |=(n=term =(n %main))) ~
14453+ ?. (dg-prepared-candidate defs 64) ~
14454+ =/ local-molds=imolds (collect-simple-molds defs)
14455+ =/ globals=(list term) (weld values.prepared (global-value-names defs))
14456+ =/ iface=ifile iface.prepared
14457+ =/ prelude=(unit ifile) `iface
14458+ =/ resolution=iresolved
14459+ (resolve-groups defs local-molds globals ~ ~ ~ ~ ~ molds.prepared at prelude)
14460+ ?^ grouped.resolution ~
14461+ ?^ artifacts.resolution ~
14462+ =/ base=ienv env.resolution
14463+ =/ templates=ienv
14464+ (turn molds.iface |=(x=[name=term template=ischeme] [name.x template.x]))
14465+ =/ all-env=ienv (weld base (weld values.iface templates))
14466+ =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
14467+ ?~ free ~
14468+ ?^ ids.u.free ~
14469+ =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)
14470+ ?~ all ~
14471+ =/ fresh=@ud (dg-next-id ids.u.all 0)
14472+ =/ st=istate *istate
14473+ =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
14474+ =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
14475+ ?: ?=(%| -.checked-molds) ~
14476+ (dg-stage defs base base st ~ 64)
14477+::
14478+++ dg-all-env-ids
14479+ |= [env=ienv fuel=@ud ids=(list @ud)]
14480+ ^- (unit dgscan)
14481+ ?~ env `[ids fuel]
14482+ ?: =(0 fuel) ~
14483+ =/ sc=ischeme scheme.i.env
14484+ ?: (itype-has-tag typ.sc) ~
14485+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ (dec fuel) ids)
14486+ ?~ raw ~
14487+ =/ quant=(unit dgscan) (dg-scan-ids vars.sc ~ fuel.u.raw ids.u.raw)
14488+ ?~ quant ~
14489+ $(env t.env, fuel fuel.u.quant, ids ids.u.quant)
14490+::
14491+++ dg-next-id
14492+ |= [ids=(list @ud) largest=@ud]
14493+ ^- @ud
14494+ ?~ ids +(largest)
14495+ $(ids t.ids, largest (max largest i.ids))
14496+::
14497+++ dg-eligible-ctor
14498+ |= [e=expr head=itype actual=itype expected=itype state=istate]
14499+ ^- (unit dgo)
14500+ ?. ?=(%call -.e) ~
14501+ ?. ?=([* ~] args.e) ~
14502+ ?. ?=(%ctor -.i.args.e) ~
14503+ ?. ?=(%fn -.head) ~
14504+ ?. ?=(%fn -.expected) ~
14505+ ?. ?=(%tag -.actual) ~
14506+ ?. constructor.actual ~
14507+ ?. ?=(%var -.product.expected) ~
14508+ ?^ (itype-lookup id.product.expected sub.state) ~
14509+ =/ bounded=(unit dgscan) (dg-scan ~[sample.expected] sub.state 256 ~)
14510+ ?~ bounded ~
14511+ ?^ ids.u.bounded ~
14512+ `[[actual expected (span-of i.args.e) (span-of head.e)]]
14513+::
14514+:: Experimental per-module, source-derived recursive tree index.
14515+:: The two tags and the exact children/list/self layout are fixed-shape
14516+:: checks, so ordinary definitions incur no type-tree or source scans.
14517+++ grec-tagged-fields
14518+ |= sh=shape
14519+ ^- (unit [tag=@ fields=(list field)])
14520+ ?. ?=(%cell -.sh) ~
14521+ ?~ fields.sh ~
14522+ =/ head=field i.fields.sh
14523+ ?. ?=(%bare -.head) ~
14524+ ?. ?=(%const -.shape.head) ~
14525+ ?. &(?=(%term form.lit.shape.head) =(%tas aura.lit.shape.head)) ~
14526+ `[val.lit.shape.head t.fields.sh]
14527+++ grec-tree-children
14528+ |= [fs=(list field) param=@t]
14529+ ^- (unit field)
14530+ ?~ fs ~
14531+ ?~ t.fs `i.fs
14532+ ?^ t.t.fs ~
14533+ =/ event=field i.fs
14534+ =/ kids=field i.t.fs
14535+ ?. &(?=(%face -.event) ?=(%face -.kids)) ~
14536+ ?. !=(name.event name.kids) ~
14537+ ?. ?=(%fn -.shape.event) ~
14538+ ?. ?=(%aura -.sample.shape.event) ~
14539+ ?. =(%t aura.sample.shape.event) ~
14540+ ?. ?=(%tvar -.product.shape.event) ~
14541+ ?. =(param name.product.shape.event) ~
14542+ `kids
14543+::
14544+++ grec-tree-proof
14545+ |= [name=term sh=shape]
14546+ ^- ?
14547+ ?. ?=(%generic -.sh) |
14548+ ?. ?=([@ ~] vars.sh) |
14549+ =/ param=@t i.vars.sh
14550+ ?. ?=(%union -.body.sh) |
14551+ ?. ?=([* [* ~]] cases.body.sh) |
14552+ =/ a=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.cases.body.sh)
14553+ =/ b=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.t.cases.body.sh)
14554+ ?~ a |
14555+ ?~ b |
14556+ ?. !=(tag.u.a tag.u.b) |
14557+ ?. ?=([* ~] fields.u.a) |
14558+ =/ value=field i.fields.u.a
14559+ ?. ?=(%face -.value) |
14560+ ?. ?=(%aura -.shape.value) |
14561+ ?. =(%t aura.shape.value) |
14562+ =/ selected=(unit field) (grec-tree-children fields.u.b param)
14563+ ?~ selected |
14564+ =/ kids=field u.selected
14565+ ?. ?=(%face -.kids) |
14566+ ?. ?=(%apply -.shape.kids) |
14567+ ?. =(ref.shape.kids ~[%list]) |
14568+ ?. ?=([* ~] args.shape.kids) |
14569+ =/ self=shape i.args.shape.kids
14570+ ?. ?=(%apply -.self) |
14571+ ?. =(ref.self ~[name]) |
14572+ ?. ?=([* ~] args.self) |
14573+ ?. ?=(%tvar -.i.args.self) |
14574+ =(name.i.args.self param)
14575++$ grec-collected [molds=imolds proofs=(map term shape)]
14576+:: Experimental one-layer analysis view, never an exported mold identity.
14577+++ grec-unfold-view
14578+ |= [typ=itype fuel=@ud]
14579+ ^- (unit [view=itype left=@ud])
14580+ ?. ?=(%grec -.typ) ~
14581+ ?: =(fuel 0) ~
14582+ ?. ?=([* ~] args.typ) ~
14583+ =/ sh=shape proof.typ
14584+ ?. (grec-tree-proof name.typ sh) ~
14585+ ?> ?=(%generic -.sh)
14586+ ?> ?=([@ ~] vars.sh)
14587+ ?> ?=(%union -.body.sh)
14588+ ?> ?=([* [* ~]] cases.body.sh)
14589+ =/ ca=shape i.cases.body.sh
14590+ =/ cb=shape i.t.cases.body.sh
14591+ ?> ?=(%cell -.ca)
14592+ ?> ?=(%cell -.cb)
14593+ ?> ?=([* [* ~]] fields.ca)
14594+ ?> ?=([* *] fields.cb)
14595+ =/ tag-a=field i.fields.ca
14596+ =/ tag-b=field i.fields.cb
14597+ ?> ?=(%bare -.tag-a)
14598+ ?> ?=(%bare -.tag-b)
14599+ ?> ?=(%const -.shape.tag-a)
14600+ ?> ?=(%const -.shape.tag-b)
14601+ =/ text-field=field i.t.fields.ca
14602+ ?> ?=(%face -.text-field)
14603+ =/ branch=(list field) t.fields.cb
14604+ =/ kids=(unit field) (grec-tree-children branch i.vars.sh)
14605+ ?~ kids ~
14606+ ?> ?=(%face -.u.kids)
14607+ =/ children=itype [%face name.u.kids [%collection %list ~[typ]]]
14608+ ?> ?=(^ branch)
14609+ =/ payload=itype
14610+ ?~ t.branch children
14611+ =/ event=field i.branch
14612+ ?> ?=(%face -.event)
14613+ [%cell [%face name.event [%fn [%atom %t] i.args.typ]] children]
14614+ =/ leaf=itype [%cell [%const lit.shape.tag-a] [%face name.text-field [%atom %t]]]
14615+ =/ node=itype [%cell [%const lit.shape.tag-b] payload]
14616+ `[[%union ~[leaf node] ~ ~ ~] (dec fuel)]
14617+::
14618+++ grec-collect-molds
14619+ |= ds=(list def)
14620+ ^- grec-collected
14621+ ?~ ds [~ *(map term shape)]
14622+ =/ rest=grec-collected $(ds t.ds)
14623+ ?. ?=(%mold -.i.ds) rest
14624+ =/ name=term name.i.ds
14625+ =/ body=shape shape.i.ds
14626+ =/ proofs=(map term shape) proofs.rest
14627+ =? proofs (grec-tree-proof name body) (~(put by proofs) name body)
14628+ [[[name body] molds.rest] proofs]
14629+::
14630+
1089514631--