@@ -4607,6 +4607,8 @@
4607:: Atom constraints tied to an explicit capital or an inferred sample
4607:: Atom constraints tied to an explicit capital or an inferred sample
4608:: are generalized and printed. Other aura variables remain unsupported until
4608:: are generalized and printed. Other aura variables remain unsupported until
4609:: their defaulting and inferred generalization are implemented.
4609:: 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.
4610:: Bare @ is a separate unrestricted atom type. A directional fit check
4612:: Bare @ is a separate unrestricted atom type. A directional fit check
4611:: permits concrete atoms to widen to it, never the reverse. A fit that
4613:: permits concrete atoms to widen to it, never the reverse. A fit that
4612:: needs a not-yet-implemented constraint remains unsupported. Named unions
4614:: needs a not-yet-implemented constraint remains unsupported. Named unions
@@ -4665,11 +4667,13 @@
4665 [%any-atom ~]
4667 [%any-atom ~]
4666 [%flag ~]
4668 [%flag ~]
4667 [%noun ~]
4669 [%noun ~]
4668 [%tag id=@ud literal=lit constructor=?]
4671 [%tag id=@ud literal=lit constructor=?]
4669 [%const literal=lit]
4672 [%const literal=lit]
4670 [%collection name=term args=(list itype)]
4673 [%collection name=term args=(list itype)]
4671 [%recursive module=term name=term label=(unit @t)]
4674 [%recursive module=term name=term label=(unit @t)]
4672 [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
4675 [%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)]
4673 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4677 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4674 [%face name=term body=itype]
4678 [%face name=term body=itype]
4675 [%fn sample=itype product=itype]
4679 [%fn sample=itype product=itype]
@@ -4722,6 +4726,88 @@
4722 $(t u.found)
4726 $(t u.found)
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])
4735+ =/ first=(unit [empty=? left=@ud]) (itype-empty-proof i.xs sub fuel)
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])
4744+ =. typ (itype-walk typ sub)
4747+ %face $(typ body.typ)
4749+ =/ left=(unit [empty=? left=@ud]) $(typ hed.typ)
4751+ ?: empty.u.left `[& left.u.left]
4752+ $(typ tal.typ, fuel left.u.left)
4753+ %union (itype-empty-cases cases.typ sub fuel)
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)
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])
4774+ =. typ (itype-walk typ sub)
4777+ ?(%atom %any-atom %flag %const %noun %avar %rvar %nvar %rnvar %fn %jrec) `[%yes fuel]
4779+ ?: (lien caps |=(c=icap (hole-same-variable typ (itype-walk [%var id.c] sub)))) `[%yes fuel]
4781+ %face $(typ body.typ)
4783+ =/ head=(unit [result=?(%yes %no %unknown) left=@ud]) $(typ hed.typ)
4785+ ?: =(%no result.u.head) head
4786+ =/ tail=(unit [result=?(%yes %no %unknown) left=@ud]) $(typ tal.typ, fuel left.u.head)
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 |)
4793+ ?. &(|(=(%list name.typ) =(%unit name.typ)) ?=([* ~] args.typ)) `[%unknown fuel]
4795+ %grec ?:((grec-tree-proof name.typ proof.typ) `[%yes fuel] `[%unknown fuel])
4799+ |= [xs=(list itype) sub=isub caps=icaps fuel=@ud]
4800+ ^- (unit (list itype))
4802+ =/ first=(unit [result=?(%yes %no %unknown) left=@ud])
4803+ (itype-inhabited-proof i.xs sub caps fuel)
4805+ ?: =(%unknown result.u.first) ~
4806+ =/ rest=(unit (list itype)) $(xs t.xs, fuel left.u.first)
4808+ ?: =(%no result.u.first) rest
4725++ itype-occurs
4811++ itype-occurs
4726 |= [n=@ud t=itype sub=isub]
4812 |= [n=@ud t=itype sub=isub]
@@ -4736,11 +4822,13 @@
4736 %any-atom |
4822 %any-atom |
4739 %tag =(n id.t)
4826 %tag =(n id.t)
4740 %const |
4827 %const |
4741 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4828 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4742 %recursive |
4829 %recursive |
4831+ %grec (lien args.t |=(c=itype (itype-occurs n c sub)))
4744 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4832 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4745 %face $(t body.t)
4833 %face $(t body.t)
4746 %fn |($(t sample.t) $(t product.t))
4834 %fn |($(t sample.t) $(t product.t))
@@ -4759,6 +4847,9 @@
4759 =. a (itype-walk a sub)
4847 =. a (itype-walk a sub)
4760 =. b (itype-walk b sub)
4848 =. b (itype-walk b sub)
4761 ?: =(a b) `sub
4849 ?: =(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)
4762 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4853 ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4763 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
4854 ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
4764 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4855 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
@@ -4864,11 +4955,13 @@
4864 %any-atom &
4955 %any-atom &
4868 %const |
4960 %const |
4869 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4961 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4870 %recursive |
4962 %recursive |
4964+ %grec (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4872 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4965 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4873 %face $(t body.t)
4966 %face $(t body.t)
4874 %fn |($(t sample.t) $(t product.t))
4967 %fn |($(t sample.t) $(t product.t))
@@ -4938,11 +5031,13 @@
4938 %any-atom &
5031 %any-atom &
4942 %const &
5036 %const &
4943 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
5037 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4944 %recursive |
5038 %recursive |
5040+ %grec (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4946 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
5041 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4947 %face $(typ body.typ)
5042 %face $(typ body.typ)
4948 %fn |($(typ sample.typ) $(typ product.typ))
5043 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4971,6 +5066,7 @@
4972 =. t (itype-walk t sub)
5067 =. t (itype-walk t sub)
5069+ %grec (lien args.t |=(c=itype (itype-has-face c sub)))
4974 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
5070 %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4976 %cell |($(t hed.t) $(t tal.t))
5072 %cell |($(t hed.t) $(t tal.t))
@@ -5027,6 +5123,9 @@
5028 =. a (itype-walk a sub)
5124 =. a (itype-walk a sub)
5029 =. b (itype-walk b sub)
5125 =. 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)
5030 ?: &(?=(%collection -.a) ?=(%collection -.b))
5129 ?: &(?=(%collection -.a) ?=(%collection -.b))
5031 ?. =(name.a name.b) |
5130 ?. =(name.a name.b) |
5032 (itype-face-asym-collection-args args.a args.b sub)
5131 (itype-face-asym-collection-args args.a args.b sub)
@@ -5089,6 +5188,7 @@
5089 %union &
5188 %union &
5090 %recursive &
5189 %recursive &
5093 %collection &
5193 %collection &
5094 %face $(t body.t)
5194 %face $(t body.t)
@@ -5118,6 +5218,7 @@
5221+ %grec (lien args.t |=(c=itype (itype-has-tag c)))
5121 %collection (lien args.t |=(c=itype (itype-has-tag c)))
5222 %collection (lien args.t |=(c=itype (itype-has-tag c)))
5122 %face $(t body.t)
5223 %face $(t body.t)
5123 %fn |($(t sample.t) $(t product.t))
5224 %fn |($(t sample.t) $(t product.t))
@@ -5131,6 +5232,7 @@
5133 %union &
5234 %union &
5235+ %grec (lien args.t |=(c=itype (itype-has-union c)))
5134 %collection (lien args.t |=(c=itype (itype-has-union c)))
5236 %collection (lien args.t |=(c=itype (itype-has-union c)))
5135 %face $(t body.t)
5237 %face $(t body.t)
5136 %fn |($(t sample.t) $(t product.t))
5238 %fn |($(t sample.t) $(t product.t))
@@ -5149,6 +5251,7 @@
5150 ?: &(?=(~ label.t) ?=(^ args.t)) &
5252 ?: &(?=(~ label.t) ?=(^ args.t)) &
5151 (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
5253 (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))))
5152 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
5255 %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
5153 %face $(t body.t)
5256 %face $(t body.t)
5154 %fn |($(t sample.t) $(t product.t))
5257 %fn |($(t sample.t) $(t product.t))
@@ -5162,6 +5265,7 @@
5163 %recursive &
5266 %recursive &
5165 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5269 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
5166 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5270 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
5167 %face $(t body.t)
5271 %face $(t body.t)
@@ -5176,6 +5280,7 @@
5177 %recursive ?=(~ label.t)
5281 %recursive ?=(~ label.t)
5178 %jrec ?=(~ label.t)
5282 %jrec ?=(~ label.t)
5283+ %grec |(?=(~ label.t) (lien args.t |=(c=itype (itype-has-hidden-recursive c))))
5179 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5284 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5180 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5285 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5181 %face $(t body.t)
5286 %face $(t body.t)
@@ -5221,7 +5326,7 @@
5221 ?: ?=(%var -.raw)
5326 ?: ?=(%var -.raw)
5222 $(cases t.cases, pending &)
5327 $(cases t.cases, pending &)
5223 =/ c=itype (itype-walk raw sub)
5328 =/ c=itype (itype-walk raw sub)
5224− ?: ?=(?(%var %tag %recursive %jrec %union %face) -.c)
5329+ ?: ?=(?(%var %tag %recursive %jrec %grec %union %face) -.c)
5225 $(cases t.cases, pending &)
5330 $(cases t.cases, pending &)
5226 ?. ?=(%cell -.c) $(cases t.cases)
5331 ?. ?=(%cell -.c) $(cases t.cases)
5227 =/ raw-head=itype hed.c
5332 =/ raw-head=itype hed.c
@@ -5234,7 +5339,7 @@
5234 ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5339 ?: ?=(?(%atom %any-atom %flag %avar %rvar %nvar %rnvar) -.body.head)
5235 $(cases t.cases)
5340 $(cases t.cases)
5236 $(cases t.cases, pending &)
5341 $(cases t.cases, pending &)
5237− ?: ?=(?(%var %tag %recursive %jrec %union) -.head)
5342+ ?: ?=(?(%var %tag %recursive %jrec %grec %union) -.head)
5238 $(cases t.cases, pending &)
5343 $(cases t.cases, pending &)
5239 ?. ?=(%const -.head) $(cases t.cases)
5344 ?. ?=(%const -.head) $(cases t.cases)
5240 ?. =(val.literal.head val.tag) $(cases t.cases)
5345 ?. =(val.literal.head val.tag) $(cases t.cases)
@@ -5252,7 +5357,14 @@
5252++ itype-fit
5357++ itype-fit
5253 |= [actual=itype expected=itype sub=isub next=@ud]
5358 |= [actual=itype expected=itype sub=isub next=@ud]
5255− (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]
5256++ itype-fit-inner
5368++ itype-fit-inner
5257 |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5369 |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
@@ -5271,6 +5383,7 @@
5271 =. actual (itype-walk actual sub)
5383 =. actual (itype-walk actual sub)
5272 =. expected (itype-walk expected sub)
5384 =. expected (itype-walk expected sub)
5273 ?: =(actual expected) [%ok sub next]
5385 ?: =(actual expected) [%ok sub next]
5386+ ?: &(?=(%empty -.expected) |(?=(%cell -.actual) ?=(%face -.actual) ?=(%union -.actual) ?=(%grec -.actual) ?=(%recursive -.actual))) [%unknown ~]
5274 :: The relation of the source loobean mold to explicit @f is not yet
5387 :: The relation of the source loobean mold to explicit @f is not yet
5275 :: established. Keep it unsupported rather than asserting a mismatch.
5388 :: established. Keep it unsupported rather than asserting a mismatch.
5276 ?: &(?=(%flag -.actual) ?=(%atom -.expected) =(%f aura.expected)) [%unknown ~]
5389 ?: &(?=(%flag -.actual) ?=(%atom -.expected) =(%f aura.expected)) [%unknown ~]
@@ -5283,6 +5396,14 @@
5283 [%ok sub next]
5396 [%ok sub next]
5284 :: An arbitrary noun is not known to fit a narrower type.
5397 :: An arbitrary noun is not known to fit a narrower type.
5285 ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5398 ?: &(?=(%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 ~]
5286 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5407 ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5287 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5408 ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5288 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
5409 ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
@@ -5609,7 +5730,77 @@
5609 ?. (width-in-order order.source.shape order.target.shape) ~
5730 ?. (width-in-order order.source.shape order.target.shape) ~
5610 (width-fit-fields index.source.shape order.target.shape sub next)
5731 (width-fit-fields index.source.shape order.target.shape sub next)
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.
5740+ $% [%field name=term]
5746++$ igate-free [verdict=?(%yes %no %unknown) inhabited=? left=@ud path=(unit (list igf-segment))]
5748+ |= [types=(list itype) fuel=@ud path=(list igf-segment) index=@ud]
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 ~]
5760+ |= [typ=itype fuel=@ud path=(list igf-segment)]
5762+ ?: =(0 fuel) [%unknown | 0 ~]
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])
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 ~]
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])
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 ~]
5801++$ igate-prelude-evidence [iface=ifile gates=(map term def)]
5802++$ dgo [left=itype right=itype at=span context=span]
5612−+$ 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)]
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)]
5613+$ idiag [msg=tape sites=(list [at=span note=tape])]
5804+$ idiag [msg=tape sites=(list [at=span note=tape])]
5614+$ iresult (each [typ=itype state=istate] idiag)
5805+$ iresult (each [typ=itype state=istate] idiag)
5615+$ isample-result (each [typ=itype env=ienv state=istate] tape)
5806+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5629,6 +5820,7 @@
5629 |= [t=itype sub=isub]
5820 |= [t=itype sub=isub]
5630 ^- itype
5821 ^- itype
5631 =. t (itype-walk t sub)
5822 =. t (itype-walk t sub)
5823+ ?: ?=(%grec -.t) t(args (turn args.t |=(c=itype (itype-normalize c sub))))
5632 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5824 ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5633 ?: ?=(%union -.t)
5825 ?: ?=(%union -.t)
5634 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5826 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
@@ -5655,6 +5847,7 @@
5655 %cell |($(t hed.t) $(t tal.t))
5847 %cell |($(t hed.t) $(t tal.t))
5656 %recursive |
5848 %recursive |
5658 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5851 %collection (lien args.t |=(c=itype (itype-has-gate c)))
5659 %face $(t body.t)
5852 %face $(t body.t)
5660 %union (lien cases.t |=(c=itype (itype-has-gate c)))
5853 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5669,6 +5862,7 @@
5669 %any-atom |
5862 %any-atom |
5674++ default-decimals
5868++ default-decimals
@@ -5678,6 +5872,7 @@
5679 %nvar [%atom %ud]
5873 %nvar [%atom %ud]
5680 %rnvar [%atom %ud]
5874 %rnvar [%atom %ud]
5875+ %grec t(args (turn args.t |=(c=itype (default-decimals c))))
5681 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5876 %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5682 %face [%face name.t $(t body.t)]
5877 %face [%face name.t $(t body.t)]
5683 %cell [%cell $(t hed.t) $(t tal.t)]
5878 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5719,6 +5914,7 @@
5720 %any-atom &
5915 %any-atom &
5721 %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5916 %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)))
5722 %collection (levy args.t |=(c=itype (hole-known c state)))
5918 %collection (levy args.t |=(c=itype (hole-known c state)))
5723 %face $(t body.t)
5919 %face $(t body.t)
5724 %fn &($(t sample.t) $(t product.t))
5920 %fn &($(t sample.t) $(t product.t))
@@ -5728,6 +5924,8 @@
5728++ promote-restricted-numbers
5924++ promote-restricted-numbers
5729 |= [state=istate env=ienv]
5925 |= [state=istate env=ienv]
5730 ^- istate
5926 ^- istate
5927+ :: With no written capitals, there is nothing to promote.
5928+ ?~ caps.state state
5731 =/ ids=(list @ud) (turn caps.state |=(c=icap id.c))
5929 =/ ids=(list @ud) (turn caps.state |=(c=icap id.c))
5732 =/ free=(list @ud) (free-env-vars env sub.state)
5930 =/ free=(list @ud) (free-env-vars env sub.state)
@@ -5764,6 +5962,7 @@
5765 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
5963 ?(%tag %nvar %rnvar %avar %rvar) !(hole-known t state)
5766 %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5964 %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)))
5767 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5966 %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5768 %face $(t body.t)
5967 %face $(t body.t)
5769 %fn |($(t sample.t) $(t product.t))
5968 %fn |($(t sample.t) $(t product.t))
@@ -5795,11 +5994,13 @@
5795 %any-atom ~
5994 %any-atom ~
5799 %const ~
5999 %const ~
5800 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
6000 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5801 %recursive ~
6001 %recursive ~
6003+ %grec (zing (turn args.t |=(c=itype (itype-vars c))))
5803 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
6004 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5804 %face $(t body.t)
6005 %face $(t body.t)
5805 %fn (weld $(t sample.t) $(t product.t))
6006 %fn (weld $(t sample.t) $(t product.t))
@@ -5843,11 +6044,13 @@
5843 %any-atom t
6044 %any-atom t
5847 %const t
6049 %const t
5848 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
6050 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5849 %recursive t
6051 %recursive t
6053+ %grec t(args (turn args.t |=(c=itype (itype-rename c ren))))
5851 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
6054 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5852 %face [%face name.t $(t body.t)]
6055 %face [%face name.t $(t body.t)]
5853 %fn [%fn $(t sample.t) $(t product.t)]
6056 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5870,11 +6073,13 @@
5870 %any-atom |
6073 %any-atom |
5874 %const |
6078 %const |
5875 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
6079 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5876 %recursive |
6080 %recursive |
6082+ %grec (lien args.t |=(c=itype (itype-var-is-atom n c)))
5878 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
6083 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5879 %face $(t body.t)
6084 %face $(t body.t)
5880 %fn |($(t sample.t) $(t product.t))
6085 %fn |($(t sample.t) $(t product.t))
@@ -5893,11 +6098,13 @@
5893 %any-atom |
6098 %any-atom |
5897 %const |
6103 %const |
5898 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
6104 %union |((lien cases.t |=(c=itype (itype-var-is-restricted n c))) (lien args.t |=(c=itype (itype-var-is-restricted n c))))
5899 %recursive |
6105 %recursive |
6107+ %grec (lien args.t |=(c=itype (itype-var-is-restricted n c)))
5901 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
6108 %collection (lien args.t |=(c=itype (itype-var-is-restricted n c)))
5902 %face $(t body.t)
6109 %face $(t body.t)
5903 %fn |($(t sample.t) $(t product.t))
6110 %fn |($(t sample.t) $(t product.t))
@@ -6194,6 +6401,7 @@
6195 ?- -.typ
6402 ?- -.typ
6196 %noun [%all ~]
6403 %noun [%all ~]
6197 %atom [%atom ~]
6405 %atom [%atom ~]
6198 %flag [%or ~[[%atom `0] [%atom `1]]]
6406 %flag [%or ~[[%atom `0] [%atom `1]]]
6199 %const [%atom `val.literal.typ]
6407 %const [%atom `val.literal.typ]
@@ -6328,6 +6536,16 @@
6328 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6536 ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6329 $(molds t.molds)
6537 $(molds t.molds)
6539+++ grec-visible-alias
6540+ |= [origin=path name=term proof=shape args=(list itype) molds=imold-types]
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)
6331++ itype-in-import
6549++ itype-in-import
6332 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6550 |= [t=itype iface=ifile face=term prelude=(unit ifile)]
6333 ^- itype
6551 ^- itype
@@ -6347,6 +6565,11 @@
6347 `(crip "{(trip u.alias)}.{(trip face)}")
6565 `(crip "{(trip u.alias)}.{(trip face)}")
6348 [%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)))]
6566 [%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)))]
6349 %recursive [%recursive module.t name.t ~]
6567 %recursive [%recursive module.t name.t ~]
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))))
6351 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6574 =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6352 ?^ public t(label `u.public)
6575 ?^ public t(label `u.public)
@@ -6459,9 +6682,29 @@
6459 ?. =(names.tail ~[name]) ~
6682 ?. =(names.tail ~[name]) ~
6460 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6683 `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6685+++ simple-source-generic-recursive
6686+ |= [name=term sh=shape args=(list itype) state=istate]
6688+ ?. ?=(%generic -.sh) ~
6689+ ?. ?=([@ ~] vars.sh) ~
6690+ ?. ?=([* ~] args) ~
6691+ ?~ grec-index.state ~
6692+ ?. =(at.u.grec-index.state at.state) ~
6694+ ?. =(prelude.u.grec-index.state u.prelude.state) ~
6695+ =/ proof=(unit shape) (~(get by shapes.u.grec-index.state) name)
6698+ `[%grec at.state name `name sh args]
6462++ infer-mold-template
6701++ infer-mold-template
6463 |= [sh=shape state=istate]
6702 |= [sh=shape state=istate]
6464 ^- (unit [template=ischeme state=istate])
6703 ^- (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))]
6465 =/ direct=(unit itype)
6708 =/ direct=(unit itype)
6466 ?. ?=([@ ~] active.state) ~
6709 ?. ?=([@ ~] active.state) ~
6467 (simple-source-recursive i.active.state sh state)
6710 (simple-source-recursive i.active.state sh state)
@@ -6519,7 +6762,7 @@
6519 ?~ found ~
6762 ?~ found ~
6520 ?^ t.found ~
6763 ?^ t.found ~
6521 result.i.found
6764 result.i.found
6522− ?. ?=([%invalid ?(%aura %core) @] raw) ~
6765+ ?. ?=([%invalid ?(%aura %core %overlap) @] raw) ~
6523 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
6766 `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
6525:: Replay only the shape branches whose evaluation order we can prove.
6768:: Replay only the shape branches whose evaluation order we can prove.
@@ -6594,13 +6837,18 @@
6594 `[[%atom aura.sh] state]
6837 `[[%atom aura.sh] state]
6595 %flag `[[%flag ~] state]
6838 %flag `[[%flag ~] state]
6596 %noun `[[%noun ~] state]
6839 %noun `[[%noun ~] state]
6840+ %void `[[%empty ~] state]
6598 ?. |(=(%term form.lit.sh) =(%null form.lit.sh) =(%loobean form.lit.sh)) ~
6842 ?. |(=(%term form.lit.sh) =(%null form.lit.sh) =(%loobean form.lit.sh)) ~
6599 ?: &(=(%loobean form.lit.sh) !|(=(0 val.lit.sh) =(1 val.lit.sh))) ~
6843 ?: &(=(%loobean form.lit.sh) !|(=(0 val.lit.sh) =(1 val.lit.sh))) ~
6600 `[[%const lit.sh] state]
6844 `[[%const lit.sh] state]
6602 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6846 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6847+ ?: (lien pairs |=(p=upair =(%overlap relation.p))) ~
6603− ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
6849+ ?: (levy pairs |=(p=upair =(%disjoint relation.p))) &
6850+ &((union-source-state-safe state 256) (union-source-distinct-tags cases.sh molds.state 256))
6604 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
6852 =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
6606 `[[%union types.u.cs ~ ~ ~] state.u.cs]
6854 `[[%union types.u.cs ~ ~ ~] state.u.cs]
@@ -6674,6 +6922,8 @@
6674 ?~ applied ~
6922 ?~ applied ~
6675 `[u.applied state.u.args]
6923 `[u.applied state.u.args]
6676 ?. ?=(%generic -.u.found) ~
6924 ?. ?=(%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]
6677 ?. (distinct-params vars.u.found) ~
6927 ?. (distinct-params vars.u.found) ~
6678 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6928 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6679 ?~ params ~
6929 ?~ params ~
@@ -7002,6 +7252,7 @@
7002 =/ retried=? ?=(%| -.inferred)
7252 =/ retried=? ?=(%| -.inferred)
7003 =? inferred retried (infer-recursive-gate d env local-state)
7253 =? inferred retried (infer-recursive-gate d env local-state)
7004 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7254 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7255+ ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7005 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7256 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7006 =. 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)))
7257 =. 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)))
7007 =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
7258 =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
@@ -7111,6 +7362,8 @@
7111 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
7362 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
7112 (infer-list-context e expected env state context)
7363 (infer-list-context e expected env state context)
7113 ?: ?=(%branch -.e)
7364 ?: ?=(%branch -.e)
7365+ =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
7366+ ?^ empty-list u.empty-list
7114 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
7367 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
7115 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
7368 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
7116 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
7369 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -7224,7 +7477,12 @@
7224 =/ target=itype (itype-walk expected sub.state)
7477 =/ target=itype (itype-walk expected sub.state)
7225 =/ value=iresult (infer-call-context-arg i.items target env state context)
7478 =/ value=iresult (infer-call-context-arg i.items target env state context)
7226 ?: ?=(%| -.value) value
7479 ?: ?=(%| -.value) value
7227− =/ 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)
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)
7228 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7486 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7229 ?: ?=(%bad -.fit)
7487 ?: ?=(%bad -.fit)
7230 ?: |((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))
7488 ?: |((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))
@@ -7241,7 +7499,12 @@
7241 =/ target=itype (itype-walk expected sub.state)
7499 =/ target=itype (itype-walk expected sub.state)
7242 =/ value=iresult (infer-call-context-arg i.items target env state context)
7500 =/ value=iresult (infer-call-context-arg i.items target env state context)
7243 ?: ?=(%| -.value) value
7501 ?: ?=(%| -.value) value
7244− =/ 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)
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)
7245 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7508 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
7246 ?: ?=(%bad -.fit)
7509 ?: ?=(%bad -.fit)
7247 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
7510 =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
@@ -7328,6 +7591,11 @@
7328 [%| ["list pattern needs the standard prelude in partial inference" ~]]
7591 [%| ["list pattern needs the standard prelude in partial inference" ~]]
7329 ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
7592 ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
7330 ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
7593 ?^ 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" ~]]
7331 ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
7599 ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
7332 ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
7600 ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
7333 ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
7601 ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
@@ -7381,6 +7649,11 @@
7381 [%| ["pattern binder shadows a name" ~]]
7649 [%| ["pattern binder shadows a name" ~]]
7382 =/ payload=(unit itype) (unit-union-payload typ)
7650 =/ payload=(unit itype) (unit-union-payload typ)
7383 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
7651 ?~ 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" ~]]
7384 =/ extended=ienv [[u.binder [u.payload ~]] env]
7657 =/ extended=ienv [[u.binder [u.payload ~]] env]
7385 =/ left=iresult
7658 =/ left=iresult
7386 ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
7659 ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
@@ -7533,7 +7806,9 @@
7533 ?: ?=(%| -.subject) `subject
7806 ?: ?=(%| -.subject) `subject
7534 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7807 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7535 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7808 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7536− =/ 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)
7811+ =/ cases=(list itype) u.live
7537 =/ remaining=(list itype) cases
7812 =/ remaining=(list itype) cases
7538 =/ arms=(list arm) arms.e
7813 =/ arms=(list arm) arms.e
7539 =/ st=istate state.p.subject
7814 =/ st=istate state.p.subject
@@ -7570,7 +7845,9 @@
7570 ?: ?=(%| -.subject) `subject
7845 ?: ?=(%| -.subject) `subject
7571 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7846 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7572 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7847 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7573− =/ 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)
7850+ =/ cases=(list itype) u.live
7574 =/ remaining=(list itype) cases
7851 =/ remaining=(list itype) cases
7575 =/ arms=(list arm) arms.e
7852 =/ arms=(list arm) arms.e
7576 =/ st=istate state.p.subject
7853 =/ st=istate state.p.subject
@@ -7614,7 +7891,9 @@
7614 ?: ?=(%| -.subject) subject
7891 ?: ?=(%| -.subject) subject
7615 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7892 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7616 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7893 ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
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" ~]]
7617− =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7896+ =/ expanded=(unit (list ifinite)) (finite-cases u.live ~ 0)
7618 ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7897 ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7619 =/ cases=(list ifinite) u.expanded
7898 =/ cases=(list ifinite) u.expanded
7620 =/ remaining=(list ifinite) cases
7899 =/ remaining=(list ifinite) cases
@@ -7735,9 +8014,65 @@
7735 =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
8014 =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
7736 [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
8015 [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
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]
8023+ ?. ?=(%cell -.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 ~)
8030+ ?> ?=(%cell -.u.chosen)
8031+ =/ rest=(list pattern) t.items.pat
8032+ =/ arity=? ?:(?=(%cell -.tal.u.chosen) ?=([* [* ~]] rest) ?=([* ~] rest))
8034+ (levy rest |=(p=pattern |(?=(%bind -.p) ?=(%any -.p))))
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]
8043+ =/ pat=pattern pat.i.arms
8044+ ?. |(?=(%any -.pat) (grec-simple-pattern pat view)) |
8045+ $(arms t.arms, left (dec left))
8047+ |= [e=expr subject=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
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)]
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]
8066+ ?. ?=([@ ~] names.e) ~
8067+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8069+ ?. (grec-direct-context typ.u.scheme sub.state) ~
8070+ `(infer-fragment e env state)
7738++ infer-known-union-branch-subject
8072++ infer-known-union-branch-subject
7739 |= [e=expr env=ienv subject=iresult]
8073 |= [e=expr env=ienv subject=iresult]
7740 ^- iresult
8074 ^- iresult
8075+ =. subject (grec-match-view e subject)
7741 =. subject (jrec-match-view e subject)
8076 =. subject (jrec-match-view e subject)
7742 =/ whole=(unit iresult) (infer-known-union-whole e env subject)
8077 =/ whole=(unit iresult) (infer-known-union-whole e env subject)
7743 ?~ whole (infer-known-union-finite e env subject ~)
8078 ?~ whole (infer-known-union-finite e env subject ~)
@@ -7752,6 +8087,7 @@
7752++ infer-known-union-context-subject
8087++ infer-known-union-context-subject
7753 |= [e=expr expected=itype env=ienv subject=iresult context=span]
8088 |= [e=expr expected=itype env=ienv subject=iresult context=span]
7754 ^- iresult
8089 ^- iresult
8090+ =. subject (grec-match-view e subject)
7755 =. subject (jrec-match-view e subject)
8091 =. subject (jrec-match-view e subject)
7756 =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
8092 =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
7757 ?~ whole (infer-known-union-finite e env subject `[expected context])
8093 ?~ whole (infer-known-union-finite e env subject `[expected context])
@@ -7804,9 +8140,67 @@
7804 =/ subject=iresult (infer-fragment e env state)
8140 =/ subject=iresult (infer-fragment e env state)
7805 ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
8141 ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
7806 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8142 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7807− ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
8143+ ?. |(?=(%union -.typ) ?=(%jrec -.typ) &(?=(%grec -.typ) (grec-direct-context typ.p.subject sub.state.p.subject))) ~
7808 `subject
8144 `subject
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])]
8153+ ?. ?=(%branch -.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)
8161+ ?. ?=(%collection -.typ.u.scheme) ~
8162+ ?. =(%list name.typ.u.scheme) ~
8164+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb) ~
8165+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
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) ~
8175+ =/ proof=(unit [empty=? left=@ud]) (itype-empty-proof i.args.typ sub.state.p.subject 256)
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)]
8188+++ known-empty-union-wing
8189+ |= [e=expr env=ienv state=istate]
8192+ ?. ?=([@ ~] names.e) ~
8193+ =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
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)
8202+ ?: =(u.live cases.typ) ~
7811:: Infer changes only against a fully known record spine. Retain the
8205:: Infer changes only against a fully known record spine. Retain the
7812:: target type; unknown spines and repeated edits remain unsupported.
8206:: target type; unknown spines and repeated edits remain unsupported.
@@ -8051,7 +8445,10 @@
8051 =/ traced=iresult $(e val.e)
8445 =/ traced=iresult $(e val.e)
8052 ?: ?=(%| -.traced) traced
8446 ?: ?=(%| -.traced) traced
8053 $(e then.e, state state.p.traced)
8447 $(e then.e, state state.p.traced)
8449+ ?: &(?=(^ defer.state) ?=(^ prelude.state))
8450+ (dg-infer-tuple-items items.e env state)
8054− %tuple (infer-simple-items items.e env state)
8451+ (infer-simple-items items.e env state)
8056 ?~ defs.e $(e final.e)
8453 ?~ defs.e $(e final.e)
8057 =/ local-names=(list term) (global-value-names defs.e)
8454 =/ local-names=(list term) (global-value-names defs.e)
@@ -8074,8 +8471,15 @@
8074 ?: ?=(%| -.result) result
8471 ?: ?=(%| -.result) result
8075 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
8472 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
8474+ ?^ defer.state (dg-boolean-branch e env state)
8077 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
8475 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
8078 ?~ t.arms.e
8476 ?~ 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)
8079 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
8483 ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
8080 (infer-cell-branch e env state ~)
8484 (infer-cell-branch e env state ~)
8081 ?^ t.t.arms.e (infer-known-union-branch e env state)
8485 ?^ t.t.arms.e (infer-known-union-branch e env state)
@@ -8143,6 +8547,8 @@
8143 =/ 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)
8547 =/ 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)
8144 ?^ nested [%| u.nested]
8548 ?^ nested [%| u.nested]
8145 [%| ["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)]]]]
8549 [%| ["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" ~]]
8146 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
8552 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
8147 [%& merged state.p.value(sub sub.fit, next next.fit)]
8553 [%& merged state.p.value(sub sub.fit, next next.fit)]
8148 %crash [%& [%var next.state] state(next +(next.state))]
8554 %crash [%& [%var next.state] state(next +(next.state))]
@@ -8192,6 +8598,234 @@
8192 ?: ?=(%| -.out) [%| p.out]
8598 ?: ?=(%| -.out) [%| p.out]
8193 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
8599 [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
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]
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]
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) &
8623+++ direct-unique-names
8624+ |= [names=(list term) seen=ivisited]
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)
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)
8644+++ direct-checked-gates
8645+ |= [ds=(list def) env=ienv]
8647+ =/ names=(list term) (turn env |=(e=[name=term scheme=ischeme] name.e))
8648+ =/ known=ivisited (graph-nameset names ~)
8649+ =/ out=(map term def) ~
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))
8658+ |= [n=term ds=(list def)]
8661+ ?: &(?=(%value -.i.ds) =(n name.i.ds)) `i.ds
8663+++ direct-gate-sample
8666+ ?. ?=(%value -.d) ~
8668+ %gate `sample.val.d
8669+ %gate-wide `sample.val.d
8672+++ direct-sample-name
8681+++ direct-field-name
8690+ |= [typ=itype name=(unit term)]
8693+ ?. ?=(%face -.typ) ~
8694+ ?. =(name.typ u.name) ~
8697+ |= [a=itype b=itype sub=isub next=@ud]
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 ~]
8706+++ direct-function-fit
8707+ |= [a=itype b=itype sam=sample sh=shape sub=isub next=@ud]
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
8714+ ?~ t.as [%unknown ~]
8715+ ?^ t.t.as [%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)
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)
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]
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)
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)
8769+ =/ sample=(unit sample) (direct-gate-sample u.source)
8771+ =/ trial=ifit (direct-function-fit x y u.sample shape.i.slots sub next)
8772+ ?. ?=(%ok -.trial) ~
8774+ ?~ result [%unknown ~]
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)]
8785+ ?. ?=(%wing -.i.args) |
8786+ ?. ?=([@ ~] names.i.args) |
8787+ ?=(^ (~(get by defs) i.names.i.args))
8790+++ direct-gate-call-fit
8791+ |= [e=expr actual=itype expected=itype env=ienv state=istate]
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) ~
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)
8809+ =/ sam=(unit sample) (direct-gate-sample u.head)
8811+ ?. ?=(%cell -.u.sam) ~
8812+ =/ fit=ifit (direct-positional-fit args.e items.u.sam actual expected env state sub.state next.state)
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)) ~
8195++ infer-call-with-head
8829++ infer-call-with-head
8196 |= [e=expr env=ienv state=istate head=iresult]
8830 |= [e=expr env=ienv state=istate head=iresult]
8197 ^- iresult
8831 ^- iresult
@@ -8218,7 +8852,17 @@
8218 =/ fit=ifit
8852 =/ fit=ifit
8219 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
8853 ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
8220 (itype-fit typ.p.arg sample.ht sub.st next.st)
8854 (itype-fit typ.p.arg sample.ht sub.st next.st)
8855+ =/ direct=(unit ifit)
8857+ (direct-gate-call-fit e typ.p.arg sample.ht env st)
8858+ =. fit ?~(direct fit u.direct)
8859+ ?: ?=(%unknown -.fit)
8221− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
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])]
8222 ?: ?=(%bad -.fit)
8866 ?: ?=(%bad -.fit)
8223 ?~ t.args.e
8867 ?~ t.args.e
8224 =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
8868 =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
@@ -8233,7 +8877,10 @@
8233 =/ arg-at=span ?~(bad whole-args at.u.bad)
8877 =/ arg-at=span ?~(bad whole-args at.u.bad)
8234 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
8878 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
8235 [%| ["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)]]]]
8879 [%| ["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" ~]]
8236 =/ face-asym=?
8882 =/ face-asym=?
8237 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
8884 ?^ t.args.e (itype-positional-face-asym args.e typ.p.arg sample.ht sub.fit)
8238 (itype-face-asym typ.p.arg sample.ht sub.fit)
8885 (itype-face-asym typ.p.arg sample.ht sub.fit)
8239 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
8886 ?: &((itype-has-face typ.p.arg sub.fit) face-asym (itype-output-may-be-cell product.ht sub.fit))
@@ -8325,7 +8972,17 @@
8325 ?~ args.result |
8972 ?~ args.result |
8326 ?. =((lent args.result) (lent args.expected)) |
8973 ?. =((lent args.result) (lent args.expected)) |
8327 ?: |((itype-has-tag (itype-normalize result sub.state.p.head)) (itype-has-tag (itype-normalize expected sub.state.p.head))) |
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))
8328− ?: |((itype-has-recursive (itype-normalize result sub.state.p.head)) (itype-has-recursive (itype-normalize expected sub.state.p.head))) |
8976+ =/ expected-recursive=? (itype-has-recursive (itype-normalize expected sub.state.p.head))
8978+ ?. result-recursive &
8980+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.result `[at.u.prelude.state %element]))
8982+ ?. expected-recursive &
8984+ &(=(at.u.prelude.state /lib/jibb/prelude/jibb) =(origin.expected `[at.u.prelude.state %element]))
8985+ ?. &(result-ok expected-ok) |
8329 ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
8986 ?: |((itype-has-any-atom result sub.state.p.head) (itype-has-any-atom expected sub.state.p.head)) |
8331 ?. eligible (infer-call-with-head e env state head)
8988 ?. eligible (infer-call-with-head e env state head)
@@ -8465,6 +9122,20 @@
8465 ?: ?=(?(%cell %face %fn %union %collection) -.val.i.sub) |
9122 ?: ?=(?(%cell %face %fn %union %collection) -.val.i.sub) |
8466 $(sub t.sub)
9123 $(sub t.sub)
9125+:: Check the syntactic root before scanning; scan substitutions once.
9126+++ grec-direct-context
9127+ |= [expected=itype sub=isub]
9131+ ?: ?=(%face -.expected)
9133+ $(expected body.expected, left (dec left))
9134+ ?. ?=(%grec -.expected) |
9137+ ?: ?=(?(%cell %face %fn %union %collection %grec) -.val.i.sub) |
9138+ $(sub t.sub, left (dec left))
8468++ contextual-direct-union
9139++ contextual-direct-union
8469 |= target=itype
9140 |= target=itype
@@ -8489,9 +9160,112 @@
8489 $(remaining t.remaining, found `c)
9160 $(remaining t.remaining, found `c)
8490 $(remaining t.remaining)
9161 $(remaining t.remaining)
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]
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)
9179+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) |
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])
9191+++ closed-cell-sub-safe
9192+ |= [sub=isub fuel=@ud]
9196+ ?: ?=(?(%cell %face %fn %union %collection %grec %jrec %recursive) -.val.i.sub) |
9197+ $(sub t.sub, fuel (dec fuel))
9199+++ closed-cell-branch-eligible
9200+ |= [e=expr expected=itype sub=isub]
9202+ ?. &(?=(%branch -.e) ?=(%cell -.expected) (closed-cell-sub-safe sub 512)) |
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)
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]
9218+ ?> (closed-cell-branch-eligible e expected sub.state)
9222+ =/ ordinary=iresult (infer-fragment e env state)
9224+ ?: ?=(%| -.ordinary) |
9225+ =/ fit=ifit (itype-fit typ.p.ordinary expected sub.state.p.ordinary next.state.p.ordinary)
9227+ ?: ordinary-good ordinary
9228+ =/ attempt=(unit iresult)
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)
9237+ =/ left=iresult (infer-call-context-arg val.x expected env state.p.subject(sub u.su) context)
9239+ =/ lf=ifit (itype-fit typ.p.left expected sub.state.p.left next.state.p.left)
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)
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)
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
8492++ infer-call-context-arg
9263++ infer-call-context-arg
8493 |= [e=expr expected=itype env=ienv state=istate context=span]
9264 |= [e=expr expected=itype env=ienv state=istate context=span]
8494 ^- iresult
9265 ^- iresult
9266+ ?: &(?=(^ defer.state) ?=(%branch -.e)) (infer-fragment e env state)
9267+ ?: &(?=(^ defer.state) ?=(^ prelude.state) ?=(%tuple -.e))
9268+ (infer-fragment e env state)
8495 ?: ?=(%pair -.e) $(e (pair-as-cell e))
9269 ?: ?=(%pair -.e) $(e (pair-as-cell e))
8496 ?: ?=(%group -.e) $(e inner.e)
9270 ?: ?=(%group -.e) $(e inner.e)
8497 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9271 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
@@ -8504,6 +9278,23 @@
8504 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
9278 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8505 ?: (explicit-proj-call e env state)
9279 ?: (explicit-proj-call e env state)
8506 (infer-proj-context e expected env state context)
9280 (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)]
8507 :: Only the source-proven one-layer cell is exposed. Each recursive
9298 :: Only the source-proven one-layer cell is exposed. Each recursive
8508 :: descent consumes one written tuple; named values use ordinary fit.
9299 :: descent consumes one written tuple; named values use ordinary fit.
8509 ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
9300 ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
@@ -8521,7 +9312,14 @@
8521 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
9312 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
8522 [%& target state.p.value(sub sub.fit, next next.fit)]
9313 [%& target state.p.value(sub sub.fit, next next.fit)]
8523 ?: ?=(%call -.e) (infer-contextual-call e target env state)
9314 ?: ?=(%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
8524 ?: (single-structured-pattern e)
9317 ?: (single-structured-pattern 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)
8525 (infer-single-case-branch e env state `[target context])
9323 (infer-single-case-branch e env state `[target context])
8526 ?: (cell-binder-pattern e)
9324 ?: (cell-binder-pattern e)
8527 (infer-cell-branch e env state `[target context])
9325 (infer-cell-branch e env state `[target context])
@@ -8541,6 +9339,8 @@
8541 (infer-known-union-context-subject e target env u.known context)
9339 (infer-known-union-context-subject e target env u.known context)
8542 ?: &(?=(%union -.target) ?=(%unit -.e))
9340 ?: &(?=(%union -.target) ?=(%unit -.e))
8543 (infer-unit-context e target env state context)
9341 (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)
8544 ?: &(?=(%flag -.target) (context-union-branch e))
9344 ?: &(?=(%flag -.target) (context-union-branch e))
8545 (infer-union-context e target env state context)
9345 (infer-union-context e target env state context)
8546 ?: &(?=(%union -.target) (context-union-branch e))
9346 ?: &(?=(%union -.target) (context-union-branch e))
@@ -8679,7 +9479,7 @@
8679 ?~ t.names |
9479 ?~ t.names |
8680 =. typ (itype-walk typ sub)
9480 =. typ (itype-walk typ sub)
8681 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
9481 ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8682− |(?=(%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))
8684++ cell-binder-pattern
9484++ cell-binder-pattern
8685 |= e=expr
9485 |= e=expr
@@ -8750,6 +9550,7 @@
8750 %any-atom "@"
9550 %any-atom "@"
8751 %flag "?"
9551 %flag "?"
8752 %noun "*"
9552 %noun "*"
8753 %tag (trip txt.literal.t)
9554 %tag (trip txt.literal.t)
8754 %const (trip txt.literal.t)
9555 %const (trip txt.literal.t)
@@ -8758,6 +9559,7 @@
8758 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
9559 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
8759 %recursive ?~(label.t "recursive mold" (trip u.label.t))
9560 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8760 %jrec ?~(label.t "recursive mold" (trip u.label.t))
9561 %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)})")
8761 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
9563 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
8762 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
9564 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
8763 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
9565 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -8801,11 +9603,13 @@
8801 %any-atom |
9603 %any-atom |
8805 %const |
9608 %const |
8806 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
9609 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
8807 %recursive |
9610 %recursive |
9612+ %grec (lien args.typ |=(c=itype (itype-has-nvar c)))
8809 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
9613 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
8810 %face $(typ body.typ)
9614 %face $(typ body.typ)
8811 %fn |($(typ sample.typ) $(typ product.typ))
9615 %fn |($(typ sample.typ) $(typ product.typ))
@@ -8917,11 +9721,13 @@
8917 %any-atom |
9721 %any-atom |
8921 %const |
9726 %const |
8922 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
9727 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
8923 %recursive |
9728 %recursive |
9730+ %grec (lien args.t |=(c=itype (has-atom-var n c)))
8925 %collection (lien args.t |=(c=itype (has-atom-var n c)))
9731 %collection (lien args.t |=(c=itype (has-atom-var n c)))
8926 %face $(t body.t)
9732 %face $(t body.t)
8927 %fn |($(t sample.t) $(t product.t))
9733 %fn |($(t sample.t) $(t product.t))
@@ -9065,6 +9871,8 @@
9065++ infer-recursive-gate
9871++ infer-recursive-gate
9066 |= [d=def env=ienv state=istate]
9872 |= [d=def env=ienv state=istate]
9067 ^- iresult
9873 ^- iresult
9874+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
9875+ =. gate-defs.state ~
9068 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
9876 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
9069 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
9877 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
9070 [%| ["recursive definition is not a gate" ~]]
9878 [%| ["recursive definition is not a gate" ~]]
@@ -9288,12 +10096,13 @@
9288++ infer-gate-group
10096++ infer-gate-group
9289 |= [ds=(list def) env=ienv state=istate]
10097 |= [ds=(list def) env=ienv state=istate]
9290 ^- ilocal-result
10098 ^- ilocal-result
10099+ ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
9291 =/ names=(list term) (global-value-names ds)
10100 =/ names=(list term) (global-value-names ds)
9292 ?. (levy names |=(n=term (unique-value-name n names)))
10101 ?. (levy names |=(n=term (unique-value-name n names)))
9293 [%| ["recursive group contains duplicate names" ~]]
10102 [%| ["recursive group contains duplicate names" ~]]
9294 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
10103 ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
9295 [%| ["recursive group shadows a name" ~]]
10104 [%| ["recursive group shadows a name" ~]]
9296− =/ scoped=istate state(globals (weld names globals.state))
10105+ =/ scoped=istate state(globals (weld names globals.state), gate-defs ~)
9297 =/ seeded=igate-seeds (seed-gate-group ds env scoped)
10106 =/ seeded=igate-seeds (seed-gate-group ds env scoped)
9298 ?: ?=(%| -.seeded) seeded
10107 ?: ?=(%| -.seeded) seeded
9299 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
10108 =/ seeds=ienv (group-seed-env entries.p.seeded ~)
@@ -9327,35 +10136,11 @@
9327 `[entry u.rest]
10136 `[entry u.rest]
9329++ add-supported-defs
10138++ add-supported-defs
9330− |= [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)]
9331 ^- [env=ienv artifacts=(list iwidth-definition)]
10140 ^- [env=ienv artifacts=(list iwidth-definition)]
9332− ?~ ds [env artifacts]
9334− ?: ?=(%mold -.d) $(ds t.ds)
9335− ?. (unique-value-name name.d globals) $(ds t.ds)
9336− ?^ (ienv-lookup name.d env) $(ds t.ds)
9337− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9338− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
10141+ (add-supported-defs-core ds all-defs checked heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts ~)
9339− =. initial (reserve-def-caps val.d initial)
9340− =/ result=iresult (infer-fragment val.d env initial)
9341− =? result ?=(%| -.result) (infer-recursive-gate d env initial)
9342− ?: ?=(%| -.result) $(ds t.ds)
9343− =. state.p.result (promote-restricted-numbers state.p.result env)
9344− =. 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)))
9345− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
9346− ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
9347− =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
9348− ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
9349− ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
9350− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
9351− ?: (gth (lent vars) 26) $(ds t.ds)
9352− =/ finalized=(unit (list iwprojection))
9353− (width-finalize projections.state.p.result sub.state.p.result vars)
9354− ?~ finalized $(ds t.ds)
9355− =? artifacts ?=(^ u.finalized)
9356− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
9357− $(ds t.ds, env [[name.d [typ vars]] env])
9359+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
10144+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
9360+$ iadj (map term (list term))
10145+$ iadj (map term (list term))
9361+$ ivisited (map term ?)
10146+$ ivisited (map term ?)
@@ -9469,6 +10254,57 @@
9469++ resolve-groups
10254++ resolve-groups
9470 |= [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)]
10255 |= [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)]
9471 ^- iresolved
10256 ^- iresolved
10257+ (resolve-groups-core ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude ~)
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)
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)
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]
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)
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)])]
9472 =/ env=ienv ~
10308 =/ env=ienv ~
9473 =/ grouped=(list term) ~
10309 =/ grouped=(list term) ~
9474 =/ artifacts=(list iwidth-definition) ~
10310 =/ artifacts=(list iwidth-definition) ~
@@ -9477,10 +10313,12 @@
9477 =/ graph=iadj (graph-make-forward ds nameset ~)
10313 =/ graph=iadj (graph-make-forward ds nameset ~)
9478 =/ components=icomponents (graph-components ds names)
10314 =/ components=icomponents (graph-components ds names)
9479 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10315 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10316+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
9481 =/ next=[env=ienv artifacts=(list iwidth-definition)]
10318 =/ next=[env=ienv artifacts=(list iwidth-definition)]
9482− (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)
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)
9483− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
10320+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10321+ =. grec-index.initial index
9484 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
10322 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
9485 ?: =(env env.out) out
10323 ?: =(env env.out) out
9486 $(env env.out, grouped grouped.out, artifacts artifacts.out)
10324 $(env env.out, grouped grouped.out, artifacts artifacts.out)
@@ -9729,6 +10567,257 @@
9729 %overlap
10567 %overlap
9730 %unknown
10568 %unknown
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))]
10576+ =. fuel (dec fuel)
10578+ ?(%aura %noun %void %flag) `fuel
10581+ ?:((lien u.vars |=(n=@t =(n name.s))) `fuel ~)
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))) ~
10586+ %cell (union-simple-fields-budget fields.s fuel vars)
10588+ =/ left=(unit @ud) $(s sample.s, fuel fuel)
10590+ $(s product.s, fuel u.left)
10593+++ union-simple-fields-budget
10594+ |= [fields=(list field) fuel=@ud vars=(unit (list @t))]
10598+ =/ field-shape=shape
10600+ %bare shape.i.fields
10601+ %face shape.i.fields
10602+ %pun [%ref at.i.fields ~[name.i.fields]]
10604+ =/ head=(unit @ud) (union-simple-shape-budget field-shape (dec fuel) vars)
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) ~
10616+ ?: =(n name.i.molds)
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]
10623+ =/ seen=(set @t) *(set @t)
10625+ ?~ vars ?~(args `fuel ~)
10628+ ?: (~(has in:..zuse seen) i.vars) ~
10629+ =/ arg=(unit @ud) (union-simple-shape-budget i.args (dec fuel) ~)
10631+ $(vars t.vars, args t.args, fuel u.arg, seen (~(put in:..zuse seen) i.vars))
10632+++ union-source-cell-tag
10635+ ?. ?=(%cell -.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))) ~
10644+++ union-source-case-tag
10645+ |= [s=shape molds=imolds fuel=@ud]
10646+ ^- (unit [tag=@ left=@ud])
10648+ =/ tag=(unit @) (union-source-cell-tag s)
10650+ =/ left=(unit @ud) (union-simple-shape-budget s fuel ~)
10653+ ?. ?=(%apply -.s) ~
10654+ ?. ?=([@ ~] ref.s) ~
10656+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
10658+ ?. ?=(%generic -.body.u.found) ~
10659+ ?~ vars.body.u.found ~
10660+ =/ tag=(unit @) (union-source-cell-tag body.body.u.found)
10662+ =/ args=(unit @ud) (union-source-args-budget vars.body.u.found args.s left.u.found)
10664+ =/ left=(unit @ud) (union-simple-shape-budget body.body.u.found u.args `vars.body.u.found)
10667+++ union-source-distinct-tags
10668+ |= [cases=(list shape) molds=imolds fuel=@ud]
10670+ =/ seen=(set @) *(set @)
10671+ =/ has-application=? |
10673+ ?~ cases has-application
10675+ =/ item=(unit [tag=@ left=@ud]) (union-source-case-tag i.cases molds (dec fuel))
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)))
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
10685+ ?=(?(%var %avar %rvar %nvar %rnvar %atom %any-atom %flag %noun %empty %const) -.t)
10686+++ union-state-params-budget
10687+ |= [params=iparams fuel=@ud]
10691+ ?. (union-state-leaf typ.i.params) ~
10692+ $(params t.params, fuel (dec fuel))
10693+++ union-state-sub-budget
10694+ |= [sub=isub fuel=@ud]
10698+ ?. (union-state-leaf val.i.sub) ~
10699+ $(sub t.sub, fuel (dec fuel))
10700+++ union-state-caps-budget
10701+ |= [caps=icaps fuel=@ud]
10705+ $(caps t.caps, fuel (dec fuel))
10706+++ union-state-active-budget
10707+ |= [active=(list term) fuel=@ud]
10711+ $(active t.active, fuel (dec fuel))
10712+++ union-state-tags-budget
10713+ |= [tags=(list ipending) fuel=@ud]
10717+ $(tags t.tags, fuel (dec fuel))
10718+++ union-source-state-safe
10719+ |= [state=istate fuel=@ud]
10721+ ?^ grec-index.state |
10724+ ?^ obligations.state |
10725+ =/ params=(unit @ud) (union-state-params-budget params.state fuel)
10727+ =/ sub=(unit @ud) (union-state-sub-budget sub.state u.params)
10729+ =/ caps=(unit @ud) (union-state-caps-budget caps.state u.sub)
10731+ =/ active=(unit @ud) (union-state-active-budget active.state u.caps)
10733+ ?=(^ (union-state-tags-budget tags.state u.active))
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
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]
10752+++ union-overlap-case
10753+ |= [s=shape molds=imolds fuel=@ud]
10754+ ^- (unit [item=uow-case left=@ud])
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) ~
10766+ =/ found=(unit [body=shape left=@ud]) (union-source-find i.ref.s molds (dec fuel))
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)
10773+ `[body.body.u.found `[i.vars.body.u.found u.argument] (dec left.u.found)]
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)
10782+ =/ field=field i.t.fields.body
10787+ %pun [%ref at.field ~[name.field]]
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)
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])
10802+ =/ other=(unit [item=uow-case left=@ud]) (union-overlap-case i.rest molds (dec fuel))
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]
10813+ =/ first=(unit [item=uow-case left=@ud]) (union-overlap-case i.cases molds (dec fuel))
10815+ =/ found=(unit [witness=(unit upair) left=@ud])
10816+ (union-overlap-against item.u.first t.cases molds left.u.first)
10818+ ?^ witness.u.found witness.u.found
10819+ $(cases t.cases, fuel left.u.found)
9732++ union-pairs
10821++ union-pairs
9733 |= [cases=(list shape) molds=imolds]
10822 |= [cases=(list shape) molds=imolds]
9734 ^- (list upair)
10823 ^- (list upair)
@@ -9882,6 +10971,11 @@
9882 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
10971 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
9883 =/ pairs=(list upair) (union-pairs cases.sh molds)
10972 =/ pairs=(list upair) (union-pairs cases.sh molds)
9884 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
10973 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
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])
9885 ?^ overlapping
10979 ?^ overlapping
9886 =/ p=upair i.overlapping
10980 =/ p=upair i.overlapping
9887 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
10981 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
@@ -9889,7 +10983,9 @@
9889 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
10983 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
9890 (of-wain:format ~[summary first second])
10984 (of-wain:format ~[summary first second])
9891 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
10985 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
10986+ ?. (union-source-distinct-tags cases.sh molds 256)
9892− (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10987+ (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
10988+ (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
9893 (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
10989 (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
9895:: +show-inference-diagnostic: a partial report with both source sites
10991:: +show-inference-diagnostic: a partial report with both source sites
@@ -9946,7 +11042,14 @@
9946+$ jbundle (list jsource)
11042+$ jbundle (list jsource)
9947+$ jcache (list [at=path iface=ifile])
11043+$ jcache (list [at=path iface=ifile])
9948+$ jfile-result (each [iface=ifile cache=jcache] @t)
11044+$ 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)
9949+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
11050+$ 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)
9951:: Written record fields each have their own lexical record scope.
11054:: Written record fields each have their own lexical record scope.
9952+$ written-fields (map term span)
11055+$ written-fields (map term span)
@@ -10219,19 +11322,56 @@
10219 (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
11322 (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
10220 (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
11323 (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
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]
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]
11339+ =/ sh=shape body.m
11341+ ?. ?=(%generic -.sh) &
11343+ (module-mold-params-valid vars.sh *(set @t) 256)
11345+ =? sh ?=(%generic -.sh) body.sh
11346+ ?. ?=(%union -.sh) ~
11347+ (union-source-overlap cases.sh molds 256)
10222−++ module-mold-types
11348+++ module-mold-types-detail
10223 |= [molds=imolds state=istate]
11349 |= [molds=imolds state=istate]
10224− ^- (each imold-types @t)
11350+ ^- (each imold-types imold-failure)
10225 ?~ molds [%& ~]
11351 ?~ molds [%& ~]
10226 =/ m=[name=term body=shape] i.molds
11352 =/ m=[name=term body=shape] i.molds
10227 =/ t=(unit [template=ischeme state=istate])
11353 =/ t=(unit [template=ischeme state=istate])
10228 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11354 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11356+ =/ overlap=(unit upair) (module-mold-overlap m molds.state)
10229− ?~ t [%| 'module mold needs unsupported inference']
11357+ [%| ['module mold needs unsupported inference' ?~(overlap ~ `[name.m u.overlap])]]
10230 =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
11358 =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
10231− =/ rest=(each imold-types @t) $(molds t.molds)
11359+ =/ rest=(each imold-types imold-failure) $(molds t.molds)
10232 ?: ?=(%| -.rest) rest
11360 ?: ?=(%| -.rest) rest
10233 [%& [[name.m template.u.t] p.rest]]
11361 [%& [[name.m template.u.t] p.rest]]
11362+++ module-mold-types
11363+ |= [molds=imolds state=istate]
11364+ ^- (each imold-types @t)
11366+ =/ m=[name=term body=shape] i.molds
11367+ =/ t=(unit [template=ischeme state=istate])
11368+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
11369+ ?~ t [%| 'module mold needs unsupported inference']
11370+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
11371+ =/ rest=(each imold-types @t) $(molds t.molds)
11372+ ?: ?=(%| -.rest) rest
11373+ [%& [[name.m template.u.t] p.rest]]
10235:: Prepare a provisional interface from the trusted vendored source.
11375:: Prepare a provisional interface from the trusted vendored source.
10236:: Every declared name remains reserved, but only molds and values this
11376:: Every declared name remains reserved, but only molds and values this
10237:: fragment can infer are usable. Unsupported bodies are not validated.
11377:: fragment can infer are usable. Unsupported bodies are not validated.
@@ -10280,6 +11420,9 @@
10280 |= [typ=itype name=term vars=(list @ud)]
11420 |= [typ=itype name=term vars=(list @ud)]
10281 ^- itype
11421 ^- itype
10282 ?: ?=(%jrec -.typ) typ(label `name)
11422 ?: ?=(%jrec -.typ) typ(label `name)
11423+ ?: ?=(%grec -.typ)
11424+ ?. (identity-union-parameters vars args.typ) typ(label ~)
10283 ?. ?=(%union -.typ) typ
11426 ?. ?=(%union -.typ) typ
10284 ?. (identity-union-parameters vars args.typ)
11427 ?. (identity-union-parameters vars args.typ)
10285 ?~ origin.typ typ
11428 ?~ origin.typ typ
@@ -10312,7 +11455,12 @@
10312 =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
11455 =/ plus=ischeme [[%fn [%cell b b] b] ~[0]]
10313 =/ minus=ischeme [[%fn b b] ~[0]]
11456 =/ minus=ischeme [[%fn b b] ~[0]]
10314 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
11457 =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
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] ~]
10315− [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
11463+ [~[[%raw-add plus] [%raw-dec minus] [%raw-gth greater] [%raw-trip text-trip] [%raw-tuba text-tuba]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~ ~]
10317++ infer-private-internal
11465++ infer-private-internal
10318 |= [src=@t public-source=@t]
11466 |= [src=@t public-source=@t]
@@ -10353,7 +11501,7 @@
10353 =/ source-unit=(unit ischeme)
11501 =/ source-unit=(unit ischeme)
10354 ?~ unit-decl ~
11502 ?~ unit-decl ~
10355 =/ unit-molds=imolds ~[[%unit u.unit-decl]]
11503 =/ unit-molds=imolds ~[[%unit u.unit-decl]]
10356− =/ 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 ~ ~ ~ ~ ~ ~]
10357 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
11505 =/ unit-types=imold-types (partial-prelude-molds unit-molds unit-state)
10358 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
11506 =/ unit-iface=ifile [~ unit-types /lib/jibb/prelude/jibb ~ ~ ~ ~ ~]
10359 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
11507 =/ found=(unit ischeme) (find-jibb-mold %unit unit-iface)
@@ -10368,7 +11516,7 @@
10368 =/ js=ijimports ~[[face.i.imports.mod primitive]]
11516 =/ js=ijimports ~[[face.i.imports.mod primitive]]
10369 =/ reserved=(list term) ~[face.i.imports.mod]
11517 =/ reserved=(list term) ~[face.i.imports.mod]
10370 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11518 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10371− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~]
11519+ =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~ ~ ~ ~ ~ ~]
10372 =/ mts=(each imold-types @t) (module-mold-types molds state)
11520 =/ mts=(each imold-types @t) (module-mold-types molds state)
10373 =/ usable=(unit imold-types)
11521 =/ usable=(unit imold-types)
10374 ?: ?=(%& -.mts) `p.mts
11522 ?: ?=(%& -.mts) `p.mts
@@ -10424,7 +11572,7 @@
10424 =? env-molds declared
11572 =? env-molds declared
10425 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
11573 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
10426 =/ reserved=(list term) ?:(declared ~[%list] ~)
11574 =/ reserved=(list term) ?:(declared ~[%list] ~)
10427− =/ 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 ~ ~ ~ ~ ~ ~]
10428 :: Other prelude molds may use list only after its source has passed
11576 :: Other prelude molds may use list only after its source has passed
10429 :: the standard-list check. The raw declaration remains removed.
11577 :: the standard-list check. The raw declaration remains removed.
10430 =/ declared-list=(unit shape) (find-simple-mold %list molds)
11578 =/ declared-list=(unit shape) (find-simple-mold %list molds)
@@ -10564,33 +11712,40 @@
10564++ resolve-jibb-imports
11712++ resolve-jibb-imports
10565 |= [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)]
11713 |= [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)]
10566 ^- jimports-result
11714 ^- 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]
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
10567 ?~ imports [%& [~ cache]]
11722 ?~ imports [%& [~ cache]]
10568 ?. ?=(%jibb -.i.imports) $(imports t.imports)
11723 ?. ?=(%jibb -.i.imports) $(imports t.imports)
10569 =/ at=path (weld path.i.imports `path`~[%jibb])
11724 =/ at=path (weld path.i.imports `path`~[%jibb])
10570 ?: =(at /lib/jibb/internal/jibb)
11725 ?: =(at /lib/jibb/internal/jibb)
10571− [%| 'the prelude internal module is private']
11726+ [%| ['the prelude internal module is private' ~]]
10572 ?: =(at /lib/jibb/primitives/jibb)
11727 ?: =(at /lib/jibb/primitives/jibb)
10573− [%| 'the prelude primitive interface is private']
11728+ [%| ['the prelude primitive interface is private' ~]]
10574 ?: (lien active |=(p=path =(p at)))
11729 ?: (lien active |=(p=path =(p at)))
10575− [%| (crip "import cycle at {(spud at)}")]
11730+ [%| [(crip "import cycle at {(spud at)}") ~]]
10576 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
11731 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
10577− ?~ found [%| (crip "module source missing: {(spud at)}")]
11732+ ?~ found [%| [(crip "module source missing: {(spud at)}") ~]]
10578− ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
11733+ ?^ t.found [%| [(crip "duplicate module sources: {(spud at)}") ~]]
10579 =/ cached=(unit ifile) (find-jibb-cache at cache)
11734 =/ cached=(unit ifile) (find-jibb-cache at cache)
10580− =/ iface=jfile-result
11735+ =/ iface=jfile-detailed-result
10581 ?^ cached
11736 ?^ cached
10582− ?. =(at.u.cached at) [%| 'cached module identity needs unsupported inference']
11737+ ?. =(at.u.cached at) [%| ['cached module identity needs unsupported inference' ~]]
10583 ?~ graph.u.cached
11738 ?~ graph.u.cached
10584 :: A detached legacy interface has unknown evidence. Rebuild it
11739 :: A detached legacy interface has unknown evidence. Rebuild it
10585 :: against the current graph, without retaining any stale entry.
11740 :: against the current graph, without retaining any stale entry.
10586 =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
11741 =/ clean=jcache (skim cache |=(x=[at=path iface=ifile] !=(at.x at)))
10587− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
11742+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds clean prelude)
10588 ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
11743 ?. (request-graph-reusable u.cached source.i.found externals mark-externals modules active prelude-values prelude-molds prelude)
10589− [%| 'cached module evidence needs unsupported inference']
11744+ [%| ['cached module evidence needs unsupported inference' ~]]
10590 [%& [u.cached cache]]
11745 [%& [u.cached cache]]
10591− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
11746+ (infer-jibb-file-detailed at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
10592 ?: ?=(%| -.iface) [%| p.iface]
11747 ?: ?=(%| -.iface) [%| p.iface]
10593− =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
11748+ =/ rest=jimports-detailed-result $(imports t.imports, cache cache.p.iface)
10594 ?: ?=(%| -.rest) rest
11749 ?: ?=(%| -.rest) rest
10595 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
11750 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
@@ -10953,7 +12108,7 @@
10953 =/ surs=(list term) (collect-sur-imports imports.mod)
12108 =/ surs=(list term) (collect-sur-imports imports.mod)
10954 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
12109 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
10955 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12110 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10956− =/ 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 ~ ~ ~ ~ ~ ~]
10957 =/ mts=(each imold-types @t) (module-mold-types molds state)
12112 =/ mts=(each imold-types @t) (module-mold-types molds state)
10958 ?: ?=(%| -.mts) [%| p.mts]
12113 ?: ?=(%| -.mts) [%| p.mts]
10959 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
12114 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -10987,7 +12142,7 @@
10987 =/ surs=(list term) (collect-sur-imports imports.mod)
12142 =/ surs=(list term) (collect-sur-imports imports.mod)
10988 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
12143 =/ reserved=(list term) (weld molds.prep (turn resolved.p.deps |=(j=[face=term interface=ifile] face.j)))
10989 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12144 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10990− =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~]
12145+ =/ state=istate [0 ~ ~ ~ molds globals externals surs marks declared resolved.p.deps reserved ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10991 =/ mts=(each imold-types @t) (module-mold-types molds state)
12146 =/ mts=(each imold-types @t) (module-mold-types molds state)
10992 ?: ?=(%| -.mts) [%| p.mts]
12147 ?: ?=(%| -.mts) [%| p.mts]
10993 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
12148 =/ resolution=iresolved (resolve-groups ordinary molds globals externals surs marks declared resolved.p.deps reserved file prelude)
@@ -11324,20 +12479,1221 @@
11324 [env exports file derived.u.poke elaborations.support ~ `src `graph]
12479 [env exports file derived.u.poke elaborations.support ~ `src `graph]
11325 [%& [iface dependencies.ev]]
12480 [%& [iface dependencies.ev]]
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
12489+ ?: &(?=(%value -.i.ds) =(%main name.i.ds)) `i.ds
12492+++ program-main-wing
12495+ ?: ?=(%group -.e) $(e inner.e)
12496+ ?. ?=(%wing -.e) ~
12497+ ?. ?=([@ ~] names.e) ~
12500+++ program-main-args
12502+ ^- (unit (list expr))
12503+ ?. ?=(%value -.d) ~
12505+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12506+ ?. ?=(%call -.val.d) ~
12507+ =/ head=(unit term) (program-main-wing head.val.d)
12509+ ?. =(%program u.head) ~
12510+ ?. ?=([* * * * ~] args.val.d) ~
12513+++ program-main-parts
12515+ ^- (unit [init=term update=term view=term subs=term])
12516+ ?. ?=(%value -.d) ~
12518+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12519+ ?. ?=(%call -.val.d) ~
12520+ =/ head=(unit term) (program-main-wing head.val.d)
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)
12534+ `[u.init u.update u.view u.subs]
12536+:: A data page is only the direct two-component source call. Grouping is
12537+:: transparent, but page aliases, qualified wings and other kinds are not.
12540+ ^- (unit [load=term view=term])
12541+ ?. ?=(%value -.d) ~
12543+ ?: ?=(%group -.val.d) $(val.d inner.val.d)
12544+ ?. ?=(%call -.val.d) ~
12545+ =/ head=(unit term) (program-main-wing head.val.d)
12547+ ?. =(%page u.head) ~
12548+ ?. ?=([* * ~] args.val.d) ~
12549+ =/ args=(list expr) args.val.d
12550+ ?> ?=([* * ~] args)
12551+ =/ load=(unit term) (program-main-wing i.args)
12552+ =/ view=(unit term) (program-main-wing i.t.args)
12557+++ program-empty-null
12561+ %lit =(%null form.lit.e)
12563+ %group $(e inner.e)
12564+ %body ?~(defs.e $(e final.e) |)
12568+++ program-subs-empty
12571+ ?. ?=(%value -.d) |
12573+ %gate (program-empty-null body.val.d)
12574+ %gate-wide (program-empty-null body.val.d)
12578+++ program-transparent
12582+ %group $(e inner.e)
12584+ %body ?~(defs.e $(e final.e) e)
12587+++ program-init-tuple-null
12590+ ?. ?=(%value -.d) |
12591+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
12595+ %gate-wide body.val.d
12598+ =. body (program-transparent body)
12599+ ?. ?=(%tuple -.body) |
12601+ (program-empty-null val:(rear items.body))
12603+:: Recover only the update of an already recognized direct program main.
12604+:: Its written sample determines the message/model relationship; the canonical
12605+:: cmd, unit and update slot determine the result context. Publication is
12606+:: component-local so later subscription/view/initializer retries can accumulate.
12607+++ program-update-context
12608+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12609+ ^- (unit iresolved)
12610+ =/ env=ienv env.resolution
12611+ ?^ (ienv-lookup %main env) ~
12612+ ?^ (ienv-lookup update.parts env) ~
12613+ =/ updates=(list def)
12614+ (skim ds |=(d=def &(?=(%value -.d) =(update.parts name.d))))
12615+ ?. ?=([* ~] updates) ~
12616+ =/ update-def=def i.updates
12617+ ?> ?=(%value -.update-def)
12618+ =/ written-update=(unit sample) (direct-gate-sample update-def)
12619+ ?~ written-update ~
12620+ ?. ?=(%cell -.u.written-update) ~
12621+ ?. ?=([* * ~] items.u.written-update) ~
12622+ ?~ prelude.initial ~
12623+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12625+ =/ command=(unit ischeme) (find-jibb-mold %cmd u.prelude.initial)
12626+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12628+ ?~ list-template ~
12629+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12631+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12633+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12634+ ?~ written-sample ~
12635+ ?. ?=(%cell -.u.written-sample) ~
12636+ ?. ?=([* * * * ~] items.u.written-sample) ~
12637+ =/ checked=(map term def)
12638+ (~(put by (direct-checked-gates ds env)) update.parts update-def)
12640+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12641+ =/ scanned=(unit dgscan)
12642+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12644+ =. next.initial (dg-next-id ids.u.scanned 0)
12645+ =/ update-state=istate (reserve-def-caps val.update-def initial)
12646+ =/ sam=isample-result (infer-sample u.written-update env update-state)
12648+ =/ actual-sample=itype (itype-normalize typ.p.sam sub.state.p.sam)
12649+ ?. ?=(%cell -.actual-sample) ~
12650+ =/ message=(unit itype)
12651+ (direct-slot-body hed.actual-sample (direct-sample-name i.items.u.written-update))
12652+ =/ model=(unit itype)
12653+ (direct-slot-body tal.actual-sample (direct-sample-name i.t.items.u.written-update))
12656+ =/ cmd=(unit itype) (template-apply u.command ~[u.message])
12658+ =/ command-result=(unit itype) (template-apply u.list-template ~[u.cmd])
12659+ ?~ command-result ~
12660+ =/ product=itype [%cell u.model u.command-result]
12661+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program state.p.sam)
12662+ ?. ?=(%fn -.typ.instance) ~
12663+ ?. ?=(%cell -.sample.typ.instance) ~
12664+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12665+ =/ expected-update=(unit itype)
12666+ (direct-slot-body hed.tal.sample.typ.instance (direct-sample-name i.t.items.u.written-sample))
12667+ ?~ expected-update ~
12668+ ?. ?=(%fn -.u.expected-update) ~
12669+ :: Sample binders are not value faces. Strip only those two slot faces
12670+ :: for the invariant canonical-gate proof; the source-faced gate is still
12671+ :: used by the complete positional call and final ordinary result cast.
12672+ =/ canonical-candidate=itype [%fn [%cell u.message u.model] product]
12674+ (direct-invariant canonical-candidate u.expected-update sub.state.instance next.state.instance)
12675+ ?. ?=(%ok -.gate-fit) ~
12677+ (itype-normalize [%fn typ.p.sam product] sub.gate-fit)
12678+ ?. ?=(%fn -.closed) ~
12679+ :: The closed product no longer needs the canonical slot substitutions.
12680+ :: Start the body at its ordinary sample state so existing branch retries
12681+ :: keep their substitution guards, but retain the shared fresh-ID high water.
12682+ =/ st=istate state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12684+ ?- -.val.update-def
12685+ %gate body.val.update-def
12686+ %gate-wide body.val.update-def
12689+ =/ inferred=iresult
12690+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12691+ ?: ?=(%| -.inferred) ~
12692+ =/ product-fit=ifit
12693+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12694+ ?. ?=(%ok -.product-fit) ~
12695+ =/ merged-product=itype
12696+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12697+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12699+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12700+ ?. ?=(%ok -.cast) ~
12701+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12702+ =/ adjusted=iresult
12703+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12704+ =/ added=(unit iadded-definition)
12705+ (add-supported-result update-def adjusted update-state env checked artifacts.resolution)
12707+ =/ recovered=(unit ischeme) (ienv-lookup update.parts env.u.added)
12709+ ?. ?=(~ vars.u.recovered) ~
12710+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12711+ `[env.u.added grouped.resolution artifacts.u.added]
12713+++ program-inferred-slot
12714+ |= [typ=itype name=(unit term)]
12717+ ?: &(?=(%face -.typ) =(name.typ u.name)) body.typ
12720+++ program-inferred-sample
12721+ |= [typ=itype sam=sample]
12723+ (program-inferred-slot typ (direct-sample-name sam))
12725+++ program-two-slot-names
12727+ ^- (unit [first=(unit term) second=(unit term)])
12730+ ?. ?=([* * ~] items.sam) ~
12731+ `[(direct-sample-name i.items.sam) (direct-sample-name i.t.items.sam)]
12733+ ?. ?=(%cell -.shape.sam) ~
12734+ ?. ?=([* * ~] fields.shape.sam) ~
12735+ `[(direct-field-name i.fields.shape.sam) (direct-field-name i.t.fields.shape.sam)]
12739+:: Read message/model from the checked update and its written source layout.
12740+:: The source names strip only top-level sample binder faces; nested value
12741+:: faces remain part of the canonical message and model.
12742+++ program-update-relation
12743+ |= [name=term ds=(list def) env=ienv]
12744+ ^- (unit [message=itype model=itype])
12745+ =/ update=(unit ischeme) (ienv-lookup name env)
12747+ ?. ?=(~ vars.u.update) ~
12748+ ?. ?=(~ (itype-vars typ.u.update)) ~
12749+ ?. ?=(%fn -.typ.u.update) ~
12750+ ?. ?=(%cell -.sample.typ.u.update) ~
12751+ =/ defs=(list def)
12752+ (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
12753+ ?. ?=([* ~] defs) ~
12754+ =/ written=(unit sample) (direct-gate-sample i.defs)
12756+ ?. ?=(%cell -.u.written) ~
12757+ ?. ?=([* * ~] items.u.written) ~
12758+ =/ message=(unit itype)
12759+ (direct-slot-body hed.sample.typ.u.update (direct-sample-name i.items.u.written))
12760+ =/ model=(unit itype)
12761+ (direct-slot-body tal.sample.typ.u.update (direct-sample-name i.t.items.u.written))
12764+ `[u.message u.model]
12766+:: Recover an unannotated direct subscription component from the checked
12767+:: update relation and canonical fourth program slot. This establishes only
12768+:: the value type; the final program watch proof remains separate.
12769+++ program-subs-context
12770+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
12771+ ^- (unit iresolved)
12772+ =/ env=ienv env.resolution
12773+ ?^ (ienv-lookup %main env) ~
12774+ ?^ (ienv-lookup subs.parts env) ~
12775+ =/ relation=(unit [message=itype model=itype])
12776+ (program-update-relation update.parts ds env)
12778+ =/ subs=(list def)
12779+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
12780+ ?. ?=([* ~] subs) ~
12781+ =/ subs-def=def i.subs
12782+ ?> ?=(%value -.subs-def)
12783+ =/ written-subs=(unit sample) (direct-gate-sample subs-def)
12785+ ?~ prelude.initial ~
12786+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
12787+ =/ sub=(unit ischeme) (find-jibb-mold %sub u.prelude.initial)
12788+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
12791+ ?~ list-template ~
12792+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
12794+ =/ written=(unit def) (~(get by gates.u.heads) %program)
12796+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
12797+ ?~ written-sample ~
12798+ ?. ?=(%cell -.u.written-sample) ~
12799+ ?. ?=([* * * * ~] items.u.written-sample) ~
12800+ =/ checked=(map term def) (direct-checked-gates ds env)
12802+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12803+ =/ scanned=(unit dgscan)
12804+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
12806+ =. next.initial (dg-next-id ids.u.scanned 0)
12807+ =/ subs-state=istate (reserve-def-caps val.subs-def initial)
12808+ =/ sam=isample-result (infer-sample u.written-subs env subs-state)
12810+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-subs)
12811+ ?. ?=(~ (itype-vars actual-model)) ~
12812+ ?: (itype-has-tag actual-model) ~
12814+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
12815+ ?. ?=(%ok -.model-fit) ~
12816+ =/ message-sub=(unit itype) (template-apply u.sub ~[message.u.relation])
12818+ =/ product=(unit itype) (template-apply u.list-template ~[u.message-sub])
12820+ =/ instance=[typ=itype state=istate]
12821+ (instantiate-scheme u.program state.p.sam(sub sub.model-fit, next next.model-fit))
12822+ ?. ?=(%fn -.typ.instance) ~
12823+ ?. ?=(%cell -.sample.typ.instance) ~
12824+ ?. ?=(%cell -.tal.sample.typ.instance) ~
12825+ ?. ?=(%cell -.tal.tal.sample.typ.instance) ~
12826+ =/ expected-subs=(unit itype)
12827+ (direct-slot-body tal.tal.tal.sample.typ.instance (direct-sample-name i.t.t.t.items.u.written-sample))
12828+ ?~ expected-subs ~
12829+ ?. ?=(%fn -.u.expected-subs) ~
12830+ =/ canonical=itype [%fn model.u.relation u.product]
12832+ (direct-invariant canonical u.expected-subs sub.state.instance next.state.instance)
12833+ ?. ?=(%ok -.gate-fit) ~
12835+ (itype-normalize [%fn typ.p.sam u.product] sub.gate-fit)
12836+ ?. ?=(%fn -.closed) ~
12839+ %gate body.val.subs-def
12840+ %gate-wide body.val.subs-def
12844+ state.p.sam(next next.gate-fit, gate-defs checked, head-evidence heads)
12845+ =/ inferred=iresult
12846+ (infer-call-context-arg body product.closed env.p.sam st (span-of body))
12847+ ?: ?=(%| -.inferred) ~
12848+ =/ product-fit=ifit
12849+ (itype-fit typ.p.inferred product.closed sub.state.p.inferred next.state.p.inferred)
12850+ ?. ?=(%ok -.product-fit) ~
12851+ =/ merged-product=itype
12852+ (itype-merge-faces typ.p.inferred product.closed sub.product-fit)
12853+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
12855+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
12856+ ?. ?=(%ok -.cast) ~
12857+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
12858+ =/ adjusted=iresult
12859+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
12860+ =/ added=(unit iadded-definition)
12861+ (add-supported-result subs-def adjusted subs-state env checked artifacts.resolution)
12863+ =/ recovered=(unit ischeme) (ienv-lookup subs.parts env.u.added)
12865+ ?. ?=(~ vars.u.recovered) ~
12866+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
12867+ `[env.u.added grouped.resolution artifacts.u.added]
12869++$ iview-site [xs=expr mapper=term]
12870+++ program-view-site
12872+ ^- (unit iview-site)
12873+ =. e (program-transparent e)
12874+ ?. ?=(%call -.e) ~
12875+ ?. ?=([* ~] args.e) ~
12876+ =/ each=expr (program-transparent head.e)
12877+ ?. ?=(%wing -.each) ~
12878+ ?. ?=([%each ~] names.each) ~
12879+ =/ turned=expr (program-transparent i.args.e)
12880+ ?. ?=(%call -.turned) ~
12881+ ?. ?=([* * ~] args.turned) ~
12882+ =/ turn=expr (program-transparent head.turned)
12883+ ?. ?=(%wing -.turn) ~
12884+ ?. ?=([%turn ~] names.turn) ~
12885+ =/ xs=expr (program-transparent i.args.turned)
12886+ ?. ?=(%wing -.xs) ~
12888+ =/ mapper=(unit term) (program-main-wing i.t.args.turned)
12892+++ program-recovery-names
12895+ =/ main=(unit def) (program-main-def ds)
12897+ =/ parts=(unit [init=term update=term view=term subs=term])
12898+ (program-main-parts u.main)
12900+ =/ views=(list def)
12901+ (skim ds |=(d=def &(?=(%value -.d) =(view.u.parts name.d))))
12902+ ?. ?=([* ~] views) ~
12903+ =/ view-def=def i.views
12904+ ?> ?=(%value -.view-def)
12905+ =/ written=(unit sample) (direct-gate-sample view-def)
12909+ %gate body.val.view-def
12910+ %gate-wide body.val.view-def
12913+ =/ sites=(unit (list iview-site)) (program-view-sites body ~)
12915+ ?. ?=([* ~] u.sites) ~
12916+ =/ mapper=term mapper.i.u.sites
12917+ =/ components=(list term)
12923+ ?: (lien components |=(n=term =(n mapper))) ~
12924+ =/ mappers=(list def)
12925+ (skim ds |=(d=def &(?=(%value -.d) =(mapper name.d))))
12926+ ?. ?=([* ~] mappers) ~
12934+++ program-sample-binders
12941+ %cell (zing (turn items.sam |=(s=sample (program-sample-binders s))))
12945+++ program-pattern-binders
12950+ %cell (zing (turn items.pat |=(p=pattern (program-pattern-binders p))))
12954+++ program-view-sites-merge
12955+ |= [a=(unit (list iview-site)) b=(unit (list iview-site))]
12956+ ^- (unit (list iview-site))
12961+++ program-view-sites-exprs
12962+ |= [xs=(list expr) locals=(list term)]
12963+ ^- (unit (list iview-site))
12965+ (program-view-sites-merge (program-view-sites i.xs locals) $(xs t.xs))
12967+++ program-view-sites-items
12968+ |= [xs=(list item) locals=(list term)]
12969+ ^- (unit (list iview-site))
12971+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
12973+++ program-view-sites-pieces
12974+ |= [xs=(list piece) locals=(list term)]
12975+ ^- (unit (list iview-site))
12977+ =/ here=(unit (list iview-site))
12979+ %expr (program-view-sites p.i.xs locals)
12982+ (program-view-sites-merge here $(xs t.xs))
12984+++ program-view-sites-qsegs
12985+ |= [xs=(list qseg) locals=(list term)]
12986+ ^- (unit (list iview-site))
12988+ =/ here=(unit (list iview-site))
12990+ %expr (program-view-sites p.i.xs locals)
12993+ (program-view-sites-merge here $(xs t.xs))
12995+++ program-view-sites-edits
12996+ |= [xs=(list edit) locals=(list term)]
12997+ ^- (unit (list iview-site))
12999+ (program-view-sites-merge (program-view-sites val.i.xs locals) $(xs t.xs))
13001+++ program-view-sites-defs
13002+ |= [xs=(list def) locals=(list term)]
13003+ ^- (unit (list iview-site))
13005+ =/ here=(unit (list iview-site))
13006+ ?: ?=(%mold -.i.xs) `~
13007+ (program-view-sites val.i.xs locals)
13008+ (program-view-sites-merge here $(xs t.xs))
13010+++ program-view-sites-arms
13011+ |= [xs=(list arm) locals=(list term)]
13012+ ^- (unit (list iview-site))
13014+ =/ nested=(list term) (weld (program-pattern-binders pat.i.xs) locals)
13015+ (program-view-sites-merge (program-view-sites val.i.xs nested) $(xs t.xs))
13017+++ program-view-sites
13018+ |= [e=expr locals=(list term)]
13019+ ^- (unit (list iview-site))
13020+ =/ site=(unit iview-site) (program-view-site e)
13022+ =/ names=(list term) ~[%each %turn mapper.u.site]
13023+ ?> ?=(%wing -.xs.u.site)
13024+ =/ root=term (rear names.xs.u.site)
13025+ ?: |((lien names |=(n=term (lien locals |=(x=term =(n x))))) (lien locals |=(x=term =(root x))))
13029+ %str (program-view-sites-pieces pieces.e locals)
13030+ %qath (program-view-sites-qsegs segs.e locals)
13031+ %change (program-view-sites-edits edits.e locals)
13032+ %pair (program-view-sites val.e locals)
13033+ %unit (program-view-sites val.e locals)
13034+ %group (program-view-sites inner.e locals)
13035+ %list (program-view-sites-exprs items.e locals)
13036+ %tuple (program-view-sites-items items.e locals)
13038+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13040+ (program-view-sites body.e (weld (program-sample-binders sample.e) locals))
13042+ (program-view-sites-merge (program-view-sites head.e locals) (program-view-sites-exprs args.e locals))
13043+ %cast (program-view-sites val.e locals)
13045+ (program-view-sites-merge (program-view-sites val.e locals) (program-view-sites then.e locals))
13047+ (program-view-sites-merge (program-view-sites subject.e locals) (program-view-sites-arms arms.e locals))
13049+ =/ nested=(list term) (weld (global-value-names defs.e) locals)
13050+ (program-view-sites-merge (program-view-sites-defs defs.e nested) (program-view-sites final.e nested))
13054+++ program-union-tag-case
13055+ |= [expected=itype tag=@]
13057+ ?. ?=(%union -.expected) ~
13058+ =/ remaining=(list itype) cases.expected
13059+ =/ found=(unit itype) ~
13060+ =/ seen=(set @) *(set @)
13062+ ?~ remaining found
13063+ =/ case=itype i.remaining
13065+ ?: ?=(%const -.case) `val.literal.case
13066+ ?. ?=(%cell -.case) ~
13067+ ?. ?=(%const -.hed.case) ~
13068+ `val.literal.hed.case
13070+ ?: (~(has in:..zuse seen) u.head) ~
13071+ =. seen (~(put in:..zuse seen) u.head)
13072+ =? found =(tag u.head)
13074+ $(remaining t.remaining)
13076+++ program-single-case-fit
13077+ |= [actual=itype expected=itype sub=isub next=@ud]
13079+ =. actual (itype-normalize actual sub)
13080+ =. expected (itype-normalize expected sub)
13081+ ?. ?=(%union -.expected) [%unknown ~]
13082+ =/ found=(unit itype)
13083+ ?: ?=(%const -.actual) `actual
13084+ ?: ?=(%tag -.actual) `actual
13085+ ?: ?=(%cell -.actual) `actual
13086+ ?. ?=(%union -.actual) ~
13087+ ?. ?=([* ~] cases.actual) ~
13089+ ?~ found [%unknown ~]
13090+ =/ case=itype u.found
13092+ ?: ?=(%const -.case) `literal.case
13093+ ?: ?=(%tag -.case) `literal.case
13094+ ?. ?=(%cell -.case) ~
13095+ =/ head=itype (projection-field-target hed.case)
13096+ ?: ?=(%const -.head) `literal.head
13097+ ?: ?=(%tag -.head) `literal.head
13099+ ?~ tag [%unknown ~]
13100+ =/ chosen=(unit itype) (program-union-tag-case expected val.u.tag)
13101+ ?~ chosen [%unknown ~]
13102+ ?: |(?=(%const -.case) ?=(%tag -.case))
13103+ ?. ?=(%const -.u.chosen) [%unknown ~]
13104+ (itype-fit case u.chosen sub next)
13105+ ?. ?=(%cell -.case) [%unknown ~]
13106+ ?. ?=(%cell -.u.chosen) [%unknown ~]
13107+ =/ head-fit=ifit (itype-fit hed.case hed.u.chosen sub next)
13108+ ?. ?=(%ok -.head-fit) head-fit
13109+ (itype-fit tal.case tal.u.chosen sub.head-fit next.head-fit)
13111+++ program-single-generic-fit
13112+ |= [actual=itype expected=itype sub=isub next=@ud]
13114+ =. actual (itype-normalize actual sub)
13115+ =. expected (itype-normalize expected sub)
13116+ ?. &(?=(%union -.actual) ?=(%union -.expected)) [%unknown ~]
13117+ ?~ origin.actual [%unknown ~]
13118+ ?. =(origin.actual origin.expected) [%unknown ~]
13119+ ?. ?=([* ~] args.actual) [%unknown ~]
13120+ ?. ?=([* ~] args.expected) [%unknown ~]
13121+ =/ argument-fit=ifit (direct-invariant i.args.actual i.args.expected sub next)
13122+ ?: ?=(%ok -.argument-fit) argument-fit
13123+ (program-single-case-fit i.args.actual i.args.expected sub next)
13125+++ program-keyed-product-fit
13126+ |= [actual=itype expected=itype element=ischeme sub=isub next=@ud]
13128+ =. actual (itype-normalize actual sub)
13129+ =. expected (itype-normalize expected sub)
13130+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) [%unknown ~]
13132+ (itype-fit (projection-field-target hed.actual) (projection-field-target hed.expected) sub next)
13133+ ?. ?=(%ok -.key-fit) key-fit
13134+ =/ actual-el=itype
13135+ (itype-normalize (projection-field-target tal.actual) sub.key-fit)
13136+ =/ expected-el=itype
13137+ (itype-normalize (projection-field-target tal.expected) sub.key-fit)
13138+ ?. &(?=(%union -.actual-el) ?=(%union -.expected-el)) [%unknown ~]
13139+ ?. =(origin.actual-el origin.expected-el) [%unknown ~]
13140+ ?. ?=([* ~] args.actual-el) [%unknown ~]
13141+ ?. ?=([* ~] args.expected-el) [%unknown ~]
13142+ =/ canonical-actual=(unit itype)
13143+ (template-apply element ~[i.args.actual-el])
13144+ =/ canonical-expected=(unit itype)
13145+ (template-apply element ~[i.args.expected-el])
13146+ ?~ canonical-actual [%unknown ~]
13147+ ?~ canonical-expected [%unknown ~]
13148+ =/ actual-check=ifit
13149+ (direct-invariant actual-el u.canonical-actual sub.key-fit next.key-fit)
13150+ ?. ?=(%ok -.actual-check) actual-check
13151+ =/ expected-check=ifit
13152+ (direct-invariant expected-el u.canonical-expected sub.actual-check next.actual-check)
13153+ ?. ?=(%ok -.expected-check) expected-check
13155+ (program-single-case-fit i.args.actual-el i.args.expected-el sub.expected-check next.expected-check)
13158+:: Recover exactly one direct keyed each/turn row mapper, then its view.
13159+:: The prelude's own each and turn schemes determine the mapper gate: the
13160+:: key is inferred from the mapper body, never selected by this recovery.
13161+++ program-view-context
13162+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13163+ ^- (unit iresolved)
13164+ =/ env=ienv env.resolution
13165+ ?^ (ienv-lookup %main env) ~
13166+ ?^ (ienv-lookup view.parts env) ~
13167+ =/ relation=(unit [message=itype model=itype])
13168+ (program-update-relation update.parts ds env)
13170+ =/ views=(list def)
13171+ (skim ds |=(d=def &(?=(%value -.d) =(view.parts name.d))))
13172+ ?. ?=([* ~] views) ~
13173+ =/ view-def=def i.views
13174+ ?> ?=(%value -.view-def)
13175+ =/ written-view=(unit sample) (direct-gate-sample view-def)
13179+ %gate body.val.view-def
13180+ %gate-wide body.val.view-def
13183+ =/ sites=(unit (list iview-site)) (program-view-sites view-body ~)
13185+ ?. ?=([* ~] u.sites) ~
13186+ =/ site=iview-site i.u.sites
13187+ =/ component-names=(list term) ~[init.parts update.parts view.parts subs.parts]
13188+ ?: (lien component-names |=(n=term =(n mapper.site))) ~
13189+ ?^ (ienv-lookup mapper.site env) ~
13190+ =/ mappers=(list def)
13191+ (skim ds |=(d=def &(?=(%value -.d) =(mapper.site name.d))))
13192+ ?. ?=([* ~] mappers) ~
13193+ =/ mapper-def=def i.mappers
13194+ ?> ?=(%value -.mapper-def)
13195+ =/ written-mapper=(unit sample) (direct-gate-sample mapper-def)
13196+ ?~ written-mapper ~
13197+ ?~ prelude.initial ~
13198+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13199+ =/ each-scheme=(unit ischeme) (ienv-lookup %each values.u.prelude.initial)
13200+ =/ turn-scheme=(unit ischeme) (ienv-lookup %turn values.u.prelude.initial)
13201+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude.initial)
13202+ =/ list-template=(unit ischeme) (find-jibb-mold %list u.prelude.initial)
13207+ ?~ list-template ~
13208+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13210+ =/ written-program=(unit def) (~(get by gates.u.heads) %program)
13211+ =/ written-each=(unit def) (~(get by gates.u.heads) %each)
13212+ =/ written-turn=(unit def) (~(get by gates.u.heads) %turn)
13213+ ?~ written-program ~
13216+ =/ program-sample=(unit sample) (direct-gate-sample u.written-program)
13217+ =/ each-sample=(unit sample) (direct-gate-sample u.written-each)
13218+ =/ turn-sample=(unit sample) (direct-gate-sample u.written-turn)
13219+ ?~ program-sample ~
13222+ ?. ?=(%cell -.u.program-sample) ~
13223+ ?. ?=([* * * * ~] items.u.program-sample) ~
13224+ =/ turn-names=(unit [first=(unit term) second=(unit term)])
13225+ (program-two-slot-names u.turn-sample)
13227+ =/ checked=(map term def) (direct-checked-gates ds env)
13229+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13230+ =/ scanned=(unit dgscan)
13231+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13233+ =. next.initial (dg-next-id ids.u.scanned 0)
13234+ =/ view-state=istate (reserve-def-caps val.view-def initial)
13235+ =/ sam=isample-result (infer-sample u.written-view env view-state)
13237+ =/ actual-model=itype (program-inferred-sample typ.p.sam u.written-view)
13239+ (direct-invariant actual-model model.u.relation sub.state.p.sam next.state.p.sam)
13240+ ?. ?=(%ok -.model-fit) ~
13241+ =/ xs-result=iresult
13242+ (infer-fragment xs.site env.p.sam state.p.sam(sub sub.model-fit, next next.model-fit))
13243+ ?: ?=(%| -.xs-result) ~
13244+ =/ element-var=itype [%var next.state.p.xs-result]
13245+ =/ list-a=(unit itype) (template-apply u.list-template ~[element-var])
13248+ (itype-fit typ.p.xs-result u.list-a sub.state.p.xs-result +(next.state.p.xs-result))
13249+ ?. ?=(%ok -.xs-fit) ~
13250+ =/ closed-xs=itype (itype-normalize u.list-a sub.xs-fit)
13251+ ?^ (itype-vars closed-xs) ~
13252+ ?: (itype-has-tag closed-xs) ~
13253+ =/ each-instance=[typ=itype state=istate]
13254+ (instantiate-scheme u.each-scheme state.p.xs-result(sub sub.xs-fit, next next.xs-fit))
13255+ ?. ?=(%fn -.typ.each-instance) ~
13256+ =/ turn-instance=[typ=itype state=istate]
13257+ (instantiate-scheme u.turn-scheme state.each-instance)
13258+ ?. ?=(%fn -.typ.turn-instance) ~
13259+ ?. ?=(%cell -.sample.typ.turn-instance) ~
13260+ =/ element-message=(unit itype)
13261+ (template-apply u.element ~[message.u.relation])
13262+ ?~ element-message ~
13264+ (itype-fit product.typ.each-instance u.element-message sub.state.turn-instance next.state.turn-instance)
13265+ ?. ?=(%ok -.each-fit) ~
13266+ =/ each-input=itype
13267+ (program-inferred-sample sample.typ.each-instance u.each-sample)
13269+ (itype-fit product.typ.turn-instance each-input sub.each-fit next.each-fit)
13270+ ?. ?=(%ok -.turn-fit) ~
13271+ =/ turn-list=itype
13272+ (program-inferred-slot hed.sample.typ.turn-instance first.u.turn-names)
13274+ (itype-fit closed-xs turn-list sub.turn-fit next.turn-fit)
13275+ ?. ?=(%ok -.list-fit) ~
13276+ =/ mapper-type=itype
13277+ (program-inferred-slot tal.sample.typ.turn-instance second.u.turn-names)
13278+ =/ expected-mapper=itype (itype-normalize mapper-type sub.list-fit)
13279+ ?. ?=(%fn -.expected-mapper) ~
13280+ ?^ (itype-vars sample.expected-mapper) ~
13281+ ?: (itype-has-tag sample.expected-mapper) ~
13282+ :: These faces come from the source-backed each sample. Keeping them in
13283+ :: the expected mapper product lets ordinary tuple inference supply key/el.
13284+ ?. ?=(%cell -.product.expected-mapper) ~
13285+ ?. ?=(%face -.hed.product.expected-mapper) ~
13286+ ?. =(%key name.hed.product.expected-mapper) ~
13287+ ?. ?=(%face -.tal.product.expected-mapper) ~
13288+ ?. =(%el name.tal.product.expected-mapper) ~
13289+ =/ mapper-state=istate
13290+ (reserve-def-caps val.mapper-def initial(next next.list-fit))
13291+ =/ mapper-sam=isample-result (infer-sample u.written-mapper env mapper-state)
13292+ ?: ?=(%| -.mapper-sam) ~
13293+ =/ mapper-input=itype (program-inferred-sample typ.p.mapper-sam u.written-mapper)
13294+ =/ mapper-sample-fit=ifit
13295+ (direct-invariant mapper-input sample.expected-mapper sub.state.p.mapper-sam next.state.p.mapper-sam)
13296+ ?. ?=(%ok -.mapper-sample-fit) ~
13297+ =/ mapper-product=itype
13298+ (itype-normalize product.expected-mapper sub.mapper-sample-fit)
13299+ =/ mapper-body=expr
13300+ ?- -.val.mapper-def
13301+ %gate body.val.mapper-def
13302+ %gate-wide body.val.mapper-def
13305+ =/ mapper-inferred=iresult
13306+ (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))
13307+ ?: ?=(%| -.mapper-inferred) ~
13308+ =/ ordinary-product-fit=ifit
13309+ (itype-fit typ.p.mapper-inferred mapper-product sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13310+ =/ mapper-product-fit=ifit
13311+ ?: ?=(%ok -.ordinary-product-fit) ordinary-product-fit
13312+ (program-keyed-product-fit typ.p.mapper-inferred mapper-product u.element sub.state.p.mapper-inferred next.state.p.mapper-inferred)
13313+ ?. ?=(%ok -.mapper-product-fit) ~
13314+ =/ closed-mapper-product=itype
13315+ (itype-normalize mapper-product sub.mapper-product-fit)
13316+ ?^ (itype-vars closed-mapper-product) ~
13317+ ?: (itype-has-tag closed-mapper-product) ~
13318+ =/ merged-mapper-product=itype
13319+ (itype-merge-faces typ.p.mapper-inferred closed-mapper-product sub.mapper-product-fit)
13320+ =/ mapper-cast=itype [%fn typ.p.mapper-sam merged-mapper-product]
13321+ =/ closed-mapper=itype [%fn typ.p.mapper-sam closed-mapper-product]
13322+ =/ mapper-cast-fit=ifit
13323+ (itype-fit mapper-cast closed-mapper sub.mapper-product-fit next.mapper-product-fit)
13324+ ?. ?=(%ok -.mapper-cast-fit) ~
13325+ =/ merged-mapper=itype
13326+ (itype-merge-faces mapper-cast closed-mapper sub.mapper-cast-fit)
13327+ =/ mapper-adjusted=iresult
13328+ [%& merged-mapper state.p.mapper-inferred(sub sub.mapper-cast-fit, next next.mapper-cast-fit)]
13329+ =/ mapper-added=(unit iadded-definition)
13330+ (add-supported-result mapper-def mapper-adjusted mapper-state env checked artifacts.resolution)
13332+ =/ mapper-scheme=(unit ischeme) (ienv-lookup mapper.site env.u.mapper-added)
13333+ ?~ mapper-scheme ~
13334+ ?. ?=(~ vars.u.mapper-scheme) ~
13335+ ?. ?=(~ (itype-vars typ.u.mapper-scheme)) ~
13336+ =/ program-instance=[typ=itype state=istate]
13337+ (instantiate-scheme u.program state.p.sam(next next.mapper-cast-fit))
13338+ ?. ?=(%fn -.typ.program-instance) ~
13339+ ?. ?=(%cell -.sample.typ.program-instance) ~
13340+ ?. ?=(%cell -.tal.sample.typ.program-instance) ~
13341+ ?. ?=(%cell -.tal.tal.sample.typ.program-instance) ~
13342+ =/ expected-view=(unit itype)
13343+ (direct-slot-body hed.tal.tal.sample.typ.program-instance (direct-sample-name i.t.t.items.u.program-sample))
13344+ ?~ expected-view ~
13345+ ?. ?=(%fn -.u.expected-view) ~
13346+ =/ canonical-view=itype [%fn model.u.relation u.element-message]
13348+ (direct-invariant canonical-view u.expected-view sub.state.program-instance next.state.program-instance)
13349+ ?. ?=(%ok -.view-fit) ~
13350+ =/ closed-view=itype
13351+ (itype-normalize [%fn typ.p.sam u.element-message] sub.view-fit)
13352+ ?. ?=(%fn -.closed-view) ~
13353+ =/ view-env=ienv [[mapper.site u.mapper-scheme] env.p.sam]
13354+ =/ final-view-state=istate
13355+ (reserve-def-caps val.view-def state.p.sam(next next.view-fit, gate-defs checked.u.mapper-added, head-evidence heads))
13356+ =/ inferred=iresult
13357+ (infer-call-context-arg view-body product.closed-view view-env final-view-state (span-of view-body))
13358+ ?: ?=(%| -.inferred) ~
13359+ =/ product-fit=ifit
13360+ (itype-fit typ.p.inferred product.closed-view sub.state.p.inferred next.state.p.inferred)
13361+ ?. ?=(%ok -.product-fit) ~
13362+ =/ merged-product=itype
13363+ (itype-merge-faces typ.p.inferred product.closed-view sub.product-fit)
13364+ =/ actual-cast=itype [%fn typ.p.sam merged-product]
13366+ (itype-fit actual-cast closed-view sub.product-fit next.product-fit)
13367+ ?. ?=(%ok -.cast) ~
13368+ =/ merged=itype (itype-merge-faces actual-cast closed-view sub.cast)
13369+ =/ adjusted=iresult
13370+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13371+ =/ added=(unit iadded-definition)
13372+ (add-supported-result view-def adjusted final-view-state env.u.mapper-added checked.u.mapper-added artifacts.u.mapper-added)
13374+ =/ recovered=(unit ischeme) (ienv-lookup view.parts env.u.added)
13376+ ?. ?=(~ vars.u.recovered) ~
13377+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13378+ `[env.u.added grouped.resolution artifacts.u.added]
13380+:: Recover only the initializer of an already recognized direct program main.
13381+:: The derived call is evidence for an ordinary init/main retry, never an
13382+:: interface to publish on its own. Any failure returns the original resolution.
13383+++ program-init-context
13384+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13385+ ^- (unit iresolved)
13386+ =/ env=ienv env.resolution
13387+ ?^ (ienv-lookup %main env) ~
13388+ ?^ (ienv-lookup init.parts env) ~
13389+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
13390+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
13391+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
13395+ =/ inits=(list def)
13396+ (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13397+ ?. ?=([* ~] inits) ~
13398+ =/ init-def=def i.inits
13399+ ?> ?=(%value -.init-def)
13400+ ?. (program-init-tuple-null init-def) ~
13401+ =/ args=(unit (list expr)) (program-main-args main)
13403+ ?~ prelude.initial ~
13404+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13406+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13408+ =/ written=(unit def) (~(get by gates.u.heads) %program)
13410+ =/ written-sample=(unit sample) (direct-gate-sample u.written)
13411+ ?~ written-sample ~
13412+ ?. ?=(%cell -.u.written-sample) ~
13413+ ?~ items.u.written-sample ~
13414+ =/ checked=(map term def) (direct-checked-gates ds env)
13416+ (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13417+ =/ scanned=(unit dgscan)
13418+ (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13420+ =. next.initial (dg-next-id ids.u.scanned 0)
13421+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
13422+ ?. ?=(%fn -.typ.instance) ~
13423+ ?. ?=(%cell -.sample.typ.instance) ~
13424+ =/ expected-init=(unit itype)
13425+ (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
13426+ ?~ expected-init ~
13427+ ?. ?=(%fn -.u.expected-init) ~
13428+ ?. ?=(%var -.sample.u.expected-init) ~
13429+ =/ data=@ud id.sample.u.expected-init
13430+ =/ init-var=itype [%var next.state.instance]
13431+ =/ st=istate state.instance(next +(next.state.instance))
13432+ =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
13433+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
13434+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
13435+ =. st state.sb(gate-defs checked, head-evidence heads)
13436+ =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
13438+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
13439+ ?. ?=(%ok -.fit) ~
13440+ =/ actual-final=itype (itype-normalize actual sub.fit)
13441+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
13442+ =/ open=(list @ud)
13443+ (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
13444+ ?. (levy open |=(n=@ud =(data n))) ~
13445+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
13447+ (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
13448+ ?. ?=(%ok -.replay) ~
13449+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
13450+ =/ expected=itype (itype-normalize u.expected-init sub.fit)
13451+ ?. ?=(%fn -.expected) ~
13452+ =. st st(sub sub.fit, next next.fit)
13453+ =/ init-state=istate (reserve-def-caps val.init-def st)
13454+ =/ inferred=iresult (infer-fragment val.init-def env init-state)
13455+ =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
13456+ ?: ?=(%| -.inferred) ~
13457+ ?. ?=(%fn -.typ.p.inferred) ~
13459+ (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
13460+ ?. ?=(%ok -.data-fit) ~
13461+ =/ closed=itype (itype-normalize expected sub.data-fit)
13462+ ?. ?=(%fn -.closed) ~
13463+ :: Resolve the ordinary tuple cast first, then check the complete gate.
13464+ :: General function fit remains unchanged; only this recovered candidate
13465+ :: receives the derived result context before its whole-type cast fit.
13466+ =/ product-fit=ifit
13467+ (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
13468+ ?. ?=(%ok -.product-fit) ~
13470+ (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
13471+ =/ actual-cast=itype [%fn sample.typ.p.inferred product]
13473+ (itype-fit actual-cast closed sub.product-fit next.product-fit)
13474+ ?. ?=(%ok -.cast) ~
13475+ =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13476+ =/ adjusted=iresult
13477+ [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13478+ =/ added=(unit iadded-definition)
13479+ (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13481+ =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13483+ ?. ?=(~ vars.u.recovered) ~
13484+ ?. ?=(~ (itype-vars typ.u.recovered)) ~
13485+ `[env.u.added grouped.resolution artifacts.u.added]
13487+++ program-subs-watch
13488+ |= [d=def imports=ijimports graph=irequest-graph prelude=ifile]
13490+ ?. ?=(%value -.d) |
13491+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
13495+ %gate-wide body.val.d
13498+ =. body (program-transparent body)
13499+ ?. ?=(%list -.body) |
13500+ ?. ?=([* ~] items.body) |
13501+ =/ watch=expr (program-transparent i.items.body)
13502+ ?. ?=(%tuple -.watch) |
13503+ ?. ?=([* * ~] items.watch) |
13504+ =/ tag=item i.items.watch
13505+ =/ payload=item i.t.items.watch
13506+ ?. &(?=(~ face.tag) ?=(~ face.payload)) |
13507+ =/ tag-expr=expr (program-transparent val.tag)
13508+ ?. ?=(%lit -.tag-expr) |
13509+ ?. &(?=(%term form.lit.tag-expr) =(%watch val.lit.tag-expr)) |
13510+ =/ request=expr (program-transparent val.payload)
13511+ ?. ?=(%call -.request) |
13512+ ?. ?=([* ~] args.request) |
13513+ =/ head=expr (program-transparent head.request)
13514+ ?. ?=(%wing -.head) |
13515+ ?. ?=([@ @ ~] names.head) |
13516+ =/ case=term i.names.head
13517+ =/ face=term i.t.names.head
13518+ =/ callback=expr (program-transparent i.args.request)
13519+ ?. ?=(%ctor -.callback) |
13520+ ?. ?=(%term form.tag.callback) |
13521+ ?=(^ (derived-request-member case face imports graph prelude))
13523+:: Exact derived-member and request-evidence identity, shared by direct
13524+:: program watches and direct data-page loads. Only a plain request in the
13525+:: selected interface's own source-backed graph can establish this shape.
13526+++ derived-request-member
13527+ |= [case=term face=term imports=ijimports graph=irequest-graph prelude=ifile]
13529+ =/ selected=(list [face=term interface=ifile])
13530+ (skim imports |=(j=[face=term interface=ifile] =(face face.j)))
13531+ ?. ?=([* ~] selected) ~
13532+ =/ iface=ifile interface.i.selected
13533+ =/ member=(unit ischeme) (ienv-lookup case values.iface)
13536+ =/ evidence=(list irequest-evidence)
13537+ (skim requests.graph |=(r=irequest-evidence &(=(api-at.r at.iface) =(name.r case))))
13538+ ?. ?=([* ~] evidence) ~
13539+ =/ request-evidence=irequest-evidence i.evidence
13540+ ?. =(u.source.iface api-source.request-evidence) ~
13541+ ?. =(name.path.path.request-evidence case) ~
13543+ ?. (lien requests.u.graph.iface |=(r=irequest-evidence =(r request-evidence))) ~
13544+ ?. ?=(~ scry.path.path.request-evidence) ~
13545+ ?. &(?=(~ diffs.path.request-evidence) ?=(~ diffs.path.path.request-evidence)) ~
13546+ ?: (lien segments.path.path.request-evidence |=(p=pseg !?=(%knot -.p))) ~
13547+ ?. ?=([@ ~] vars.u.member) ~
13548+ =/ message=@ud i.vars.u.member
13549+ ?. ?=(%fn -.typ.u.member) ~
13550+ ?. ?=(%fn -.sample.typ.u.member) ~
13551+ ?. =(sample.sample.typ.u.member full.path.request-evidence) ~
13552+ ?. =(product.sample.typ.u.member [%var message]) ~
13553+ =/ prep=iprelude [prelude prelude-values.graph prelude-molds.graph]
13554+ =/ ask=(unit ischeme) (request-compatible-ask prep)
13556+ =/ result=(unit itype) (template-apply u.ask ~[[%var message]])
13558+ ?. =(product.typ.u.member u.result) ~
13561+++ program-main-context
13562+ |= [main=def ds=(list def) resolution=iresolved initial=istate]
13564+ ?^ (ienv-lookup %main env.resolution) resolution
13565+ =/ heads=(unit igate-prelude-evidence)
13566+ (direct-prelude-evidence ds prelude.initial)
13567+ ?~ heads resolution
13568+ =/ checked=(map term def) (direct-checked-gates ds env.resolution)
13569+ =/ completed=[env=ienv artifacts=(list iwidth-definition)]
13570+ (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)
13571+ [env.completed grouped.resolution artifacts.completed]
13573+:: A static main may retain a generic element message in its ordinary
13574+:: scheme. Instantiate that scheme, specialize it to canonical element !!,
13575+:: and publish only the resulting closed scheme.
13576+++ static-main-specialized
13577+ |= [env=ienv prelude=(unit ifile)]
13580+ =/ element=(unit ischeme) (find-jibb-mold %element u.prelude)
13582+ =/ main=(unit ischeme) (ienv-lookup %main env)
13584+ =/ canonical=(unit itype) (template-apply u.element ~[[%empty ~]])
13586+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.main *istate)
13587+ =/ fit=ifit (itype-fit typ.instance u.canonical ~ next.state.instance)
13588+ ?. ?=(%ok -.fit) ~
13589+ =/ closed=itype (itype-normalize typ.instance sub.fit)
13590+ ?^ (itype-vars closed) ~
13591+ ?: (itype-has-tag closed) ~
13592+ ?. ?=(%union -.closed) ~
13593+ ?. ?=(%union -.u.canonical) ~
13594+ ?. &(=(origin.closed origin.u.canonical) =(args.closed args.u.canonical)) ~
13595+ =/ exact=ifit (direct-invariant closed u.canonical ~ next.fit)
13596+ ?. ?=(%ok -.exact) ~
13599+:: The load of a direct data page must itself be a direct gate whose
13600+:: transparent body is one plain derived request with a wing or ctor reply.
13601+++ page-load-derived
13602+ |= [name=term ds=(list def) imports=ijimports graph=irequest-graph prelude=ifile]
13604+ =/ loads=(list def)
13605+ (skim ds |=(d=def &(?=(%value -.d) =(name name.d))))
13606+ ?. ?=([* ~] loads) |
13607+ =/ load=def i.loads
13608+ ?> ?=(%value -.load)
13609+ ?. |(?=(%gate -.val.load) ?=(%gate-wide -.val.load)) |
13612+ %gate body.val.load
13613+ %gate-wide body.val.load
13616+ =. body (program-transparent body)
13617+ ?. ?=(%call -.body) |
13618+ ?. ?=([* ~] args.body) |
13619+ =/ head=expr (program-transparent head.body)
13620+ ?. ?=(%wing -.head) |
13621+ ?. ?=([@ @ ~] names.head) |
13622+ =/ reply=expr (program-transparent i.args.body)
13623+ ?. ?| &(?=(%wing -.reply) ?=([@ ~] names.reply))
13624+ &(?=(%ctor -.reply) ?=(%term form.tag.reply))
13627+ ?=(^ (derived-request-member i.names.head i.t.names.head imports graph prelude))
13629+++ page-main-closed
13630+ |= [parts=[load=term view=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
13633+ =/ page=(unit ischeme) (find-jibb-mold %page u.prelude)
13635+ =/ main=(unit ischeme) (ienv-lookup %main env)
13637+ ?. ?=(~ vars.u.main) |
13638+ ?. ?=(~ (itype-vars typ.u.main)) |
13639+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.page *istate)
13640+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
13641+ ?. ?=(%ok -.main-fit) |
13642+ (page-load-derived load.parts ds imports graph u.prelude)
13644+++ program-main-closed
13645+ |= [parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv prelude=(unit ifile) imports=ijimports graph=irequest-graph]
13648+ ?~ (ienv-lookup %program values.u.prelude) |
13649+ =/ program=(unit ischeme) (find-jibb-mold %program u.prelude)
13651+ =/ main=(unit ischeme) (ienv-lookup %main env)
13653+ ?. ?=(~ vars.u.main) |
13654+ ?. ?=(~ (itype-vars typ.u.main)) |
13655+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.program *istate)
13656+ =/ main-fit=ifit (direct-invariant typ.u.main typ.instance ~ next.state.instance)
13657+ ?. ?=(%ok -.main-fit) |
13658+ =/ init=(unit ischeme) (ienv-lookup init.parts env)
13660+ ?. ?=(~ vars.u.init) |
13661+ ?. ?=(%fn -.typ.u.init) |
13662+ ?. ?=(~ (itype-vars sample.typ.u.init)) |
13663+ ?. ?=(~ (itype-vars product.typ.u.init)) |
13664+ =/ data=igate-free (gate-free-type sample.typ.u.init 256 ~)
13665+ ?. =(%yes verdict.data) |
13666+ =/ model=igate-free (gate-free-type product.typ.u.init left.data ~)
13667+ ?. =(%yes verdict.model) |
13668+ =/ subs=(list def)
13669+ (skim ds |=(d=def &(?=(%value -.d) =(subs.parts name.d))))
13670+ ?. ?=([* ~] subs) |
13671+ |((program-subs-empty i.subs) (program-subs-watch i.subs imports graph u.prelude))
11327++ infer-jibb-file
13673++ infer-jibb-file
11328 |= [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)]
13674 |= [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)]
11329 ^- jfile-result
13675 ^- jfile-result
13676+ =/ out=jfile-detailed-result
13677+ (infer-jibb-file-detailed at src externals mark-externals modules active prelude-values prelude-molds cache prelude)
13678+ ?: ?=(%| -.out) [%| message.p.out]
13680+:: Returns structured root-source overlap evidence after the same full check.
13681+++ infer-jibb-file-detailed
13682+ |= [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)]
13683+ ^- jfile-detailed-result
11330 =/ parsed (parse at src)
13684 =/ parsed (parse at src)
11331− ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
13685+ ?: ?=(%| -.parsed) [%| [(crip "module source does not parse: {(spud at)}") ~]]
11332 =/ mod=module p.parsed
13686 =/ mod=module p.parsed
11333 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
13687 =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
11334− ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
13688+ ?^ duplicate [%| [(show-duplicate-fields at src u.duplicate) ~]]
13689+ ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
13690+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
11335 ?: ?=([%ui %api *] at)
13691 ?: ?=([%ui %api *] at)
11336 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
13692 =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
11337 ?^ iface
13693 ?^ iface
11338 =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
13694 =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals])
11339 [%& [checked [[at checked] cache]]]
13695 [%& [checked [[at checked] cache]]]
11340− ?~ prelude [%| (crip "API module needs unsupported inference: {(spud at)}")]
13696+ ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
11341 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
13697 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
11342 =/ narrow=?
13698 =/ narrow=?
11343 ?. ?=([[%mark *] ~] imports.mod) |
13699 ?. ?=([[%mark *] ~] imports.mod) |
@@ -11347,41 +13703,167 @@
11347 ?: narrow
13703 ?: narrow
11348 =/ request=(each ione-request-interface @t)
13704 =/ request=(each ione-request-interface @t)
11349 (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
13705 (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
11350− ?: ?=(%| -.request) [%| (crip "API module needs unsupported inference: {(spud at)}")]
13706+ ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
11351 =/ checked=ifile iface.p.request
13707 =/ checked=ifile iface.p.request
11352 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
13708 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
11353 =/ multi=(each [iface=ifile cache=jcache] @t)
13709 =/ multi=(each [iface=ifile cache=jcache] @t)
11354 (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
13710 (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
11355− ?: ?=(%| -.multi) [%| (crip "API module needs unsupported inference: {(spud at)}")]
13711+ ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
11356 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
13712 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
11357 ?. (module-scope-valid mod prelude-values prelude-molds)
13713 ?. (module-scope-valid mod prelude-values prelude-molds)
11358 ?: (pending-declared-poke at mod prelude-values prelude-molds)
13714 ?: (pending-declared-poke at mod prelude-values prelude-molds)
11359− [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
13715+ [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
11360− [%| (crip "module has conflicting names: {(spud at)}")]
13716+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
11361 =/ vals=(list term) (global-value-names defs.mod)
13717 =/ vals=(list term) (global-value-names defs.mod)
11362− ?: (lien vals |=(n=term =(n %main)))
13718+ =/ main=(unit def) (program-main-def defs.mod)
13719+ =/ main-parts=(unit [init=term update=term view=term subs=term])
13720+ ?~(main ~ (program-main-parts u.main))
13721+ =/ page-parts=(unit [load=term view=term])
13722+ ?~(main ~ (page-main-parts u.main))
13723+ ?: &(?=([%ui %stores *] at) ?=(^ main))
11363− [%| (crip "module kind needs unsupported inference: {(spud at)}")]
13724+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
11364− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
13725+ =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
11365 ?: ?=(%| -.js) [%| p.js]
13726 ?: ?=(%| -.js) [%| p.js]
13727+ =/ collected=grec-collected
11366− =/ molds=imolds (collect-simple-molds defs.mod)
13728+ ?^ imports.mod [(collect-simple-molds defs.mod) *(map term shape)]
13729+ (grec-collect-molds defs.mod)
13730+ =/ molds=imolds molds.collected
11367 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
13731 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
11368 =/ surs=(list term) (collect-sur-imports imports.mod)
13732 =/ surs=(list term) (collect-sur-imports imports.mod)
11369 =/ marks=(list term) (collect-mark-imports imports.mod)
13733 =/ marks=(list term) (collect-mark-imports imports.mod)
11370 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
13734 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
11371 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
13735 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11372− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
13736+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
13737+ :: Source and scope were checked above; preserve that exact root and prelude.
13738+ :: This first integration only indexes import-free library sources.
13739+ =/ index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])
13742+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude)
13744+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]]) ~
13745+ =/ index=(map term shape) proofs.collected
13746+ ?. !=(index *(map term shape)) ~
13747+ ?: (lien molds |=(m=[name=term body=shape] =(%list name.m))) ~
13748+ `[at src u.prelude index]
13749+ =. grec-index.state index
11373− =/ mts=(each imold-types @t) (module-mold-types molds state)
13750+ =/ mts=(each imold-types imold-failure) (module-mold-types-detail molds state)
11374− ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
13752+ ?~ overlap.p.mts [%| [(crip "{(trip message.p.mts)}: {(spud at)}") ~]]
13753+ =/ witness=[name=term cases=upair] u.overlap.p.mts
13754+ =/ first=@t (show-error src [at line.beg.first.cases.witness col.beg.first.cases.witness "first union case"])
13755+ =/ second=@t (show-error src [at line.beg.second.cases.witness col.beg.second.cases.witness "overlapping case"])
13756+ =/ msg=@t (of-wain:format ~[(crip "module mold {(trip name.witness)} has overlapping cases") first second])
13757+ [%| [msg `[at src name.witness cases.witness]]]
13758+ =/ resolution=iresolved
11375− =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
13760+ (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
13761+ (resolve-groups-core defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude index)
11376 =/ env=ienv env.resolution
13762 =/ env=ienv env.resolution
13763+ =/ recovered=iresolved
13764+ ?~ main resolution
13765+ ?~ main-parts resolution
13766+ =/ updated=(unit iresolved)
13767+ (program-update-context u.main u.main-parts defs.mod resolution state)
13768+ =/ with-update=iresolved ?~(updated resolution u.updated)
13769+ =/ subscribed=(unit iresolved)
13770+ (program-subs-context u.main-parts defs.mod with-update state)
13771+ =/ with-subs=iresolved ?~(subscribed with-update u.subscribed)
13772+ =/ viewed=(unit iresolved)
13773+ (program-view-context u.main-parts defs.mod with-subs state)
13774+ =/ with-view=iresolved ?~(viewed with-subs u.viewed)
13775+ =/ initialized=(unit iresolved)
13776+ (program-init-context u.main u.main-parts defs.mod with-view state)
13777+ =/ components=iresolved ?~(initialized with-view u.initialized)
13778+ (program-main-context u.main defs.mod components state)
13779+ =. env env.recovered
13780+ =. artifacts.resolution artifacts.recovered
13782+ ?: (module-values-complete defs.mod env) env
13783+ ?: |(?=([%ui %stores *] at) ?=(^ imports.mod) ?=(^ prelude) ?=(^ prelude-values) ?=(^ prelude-molds)) env
13784+ ?: (gth (met 3 src) 65.536) env
13785+ ?: (gth (lent defs.mod) 64) env
13786+ ?. (dg-source-candidate defs.mod 64) env
13787+ =/ transaction=(unit dgcommit) (dg-root-source at src)
13788+ ?~ transaction env
13789+ ?: (dg-interface-safe env.u.transaction) env.u.transaction
11377 ?. (module-values-complete defs.mod env)
13791 ?. (module-values-complete defs.mod env)
11378− [%| (crip "module definitions need unsupported inference: {(spud at)}")]
13792+ [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
11379 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
13793 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ modules prelude prelude-values prelude-molds externals mark-externals]
11380 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
13794 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
11381− ?~ graph [%| 'module request evidence needs unsupported inference']
13795+ ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
13796+ =/ static-main=(unit ischeme)
13800+ (static-main-specialized env prelude)
13801+ =? env ?=(^ static-main)
13802+ [[%main u.static-main] (skim env |=(entry=[name=term scheme=ischeme] !=(%main name.entry)))]
13805+ ?^ main-parts (program-main-closed u.main-parts defs.mod env prelude resolved.p.js u.graph)
13806+ ?^ page-parts (page-main-closed u.page-parts defs.mod env prelude resolved.p.js u.graph)
13809+ [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
11382 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
13810 =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src graph]
11383 [%& [iface [[at iface] cache.p.js]]]
13811 [%& [iface [[at iface] cache.p.js]]]
13813+:: A source-bound analysis of one named mold, not a module, island,
13814+:: request, watchability or runtime check. The host owns the trusted
13815+:: prepared prelude, canonical paths and reader/source version identities.
13816+:: The 256-node cap covers only classification, not source/graph work.
13818+ [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]
13819+++ gate-free-mold-source
13820+ |= [file=path src=@t name=term externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude) fuel=@ud]
13821+ ^- (each igate-free-mold @t)
13822+ ?~ file [%| 'mold analysis needs a path ending in jibb']
13823+ ?. =(%jibb (rear file)) [%| 'mold analysis needs a path ending in jibb']
13824+ ?: |(=(file /lib/jibb/internal/jibb) =(file /lib/jibb/primitives/jibb))
13825+ [%| 'the prelude internal modules are private']
13826+ ?: ?=([%ui %api *] file) [%| 'API declarations need unsupported mold analysis']
13827+ ?: ?=([%ui %stores *] file) [%| 'store declarations need unsupported mold analysis']
13828+ =/ entries=jbundle (skim modules |=(m=jsource =(file at.m)))
13829+ ?: (gth (lent entries) 1) [%| 'duplicate root module sources']
13830+ =/ wrong-root=? ?~(entries | !=(source.i.entries src))
13831+ ?: wrong-root [%| 'root module source does not match bundle']
13832+ =/ parsed (parse file src)
13833+ ?: ?=(%| -.parsed) [%| 'mold source does not parse']
13834+ =/ mod=module p.parsed
13835+ =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
13836+ ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
13837+ ?~ prepared [%| 'mold analysis needs the prepared prelude']
13838+ ?. (module-scope-valid mod values.u.prepared molds.u.prepared)
13839+ [%| 'mold source has conflicting or unsupported scope']
13840+ =/ selected=(list def)
13841+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(name.d name))))
13842+ ?~ selected [%| 'selected mold is not declared']
13843+ ?^ t.selected [%| 'selected mold is not unique']
13844+ ?> ?=(%mold -.i.selected)
13845+ =/ public=ifile iface.u.prepared
13846+ =/ js=jimports-result
13847+ (resolve-jibb-imports imports.mod externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
13848+ ?: ?=(%| -.js) [%| p.js]
13849+ =/ ms=imolds (collect-simple-molds defs.mod)
13850+ =/ vals=(list term) (global-value-names defs.mod)
13851+ =/ globals=(list term) (weld values.u.prepared (weld (import-binding-names imports.mod) vals))
13852+ =/ surs=(list term) (collect-sur-imports imports.mod)
13853+ =/ declared=(list term) (collect-mark-imports imports.mod)
13854+ =/ reserved=(list term) (weld molds.u.prepared (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
13855+ =/ top=(list term) (turn ms |=(m=[name=term body=shape] name.m))
13856+ =/ state=istate [0 ~ ~ ~ ms globals externals surs marks declared resolved.p.js reserved ~ ~ ~ | file top `public ~ 256 ~ ~ ~ ~ ~ ~]
13857+ =/ inferred=(unit [template=ischeme state=istate])
13858+ (infer-mold-template shape.i.selected state(active ~[name], in-mold &))
13859+ ?~ inferred [%| 'selected mold needs unsupported inference']
13860+ =/ template=ischeme template.u.inferred
13861+ =. typ.template (label-direct-union typ.template shape.i.selected name state)
13862+ =. typ.template (itype-normalize typ.template sub.state.u.inferred)
13863+ =/ cap=@ud (min fuel 256)
13864+ =/ analysis=igate-free (gate-free-type typ.template cap ~)
13865+ [%& [file src name u.prepared externals marks modules cache.p.js template fuel cap analysis]]
11385:: +golden-types-with-modules fails closed for imports without prelude
13867:: +golden-types-with-modules fails closed for imports without prelude
11386:: scope. +golden-types-with-prelude resolves supported library graphs;
13868:: scope. +golden-types-with-prelude resolves supported library graphs;
11387:: its report remains partial and unreachable sources are not examined.
13869:: its report remains partial and unreachable sources are not examined.
@@ -11442,7 +13924,7 @@
11442 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
13924 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
11443 =/ scope-values=(list term)
13925 =/ scope-values=(list term)
11444 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
13926 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
11445− (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
13927+ (golden-types-in-context-core file src externals mark-externals resolved.p.js scope-values prelude-molds iface prepared)
11447:: +golden-types-with-marks: supply declared mark types separately from /sur
13929:: +golden-types-with-marks: supply declared mark types separately from /sur
11448:: entries, as [mark result] with the result from +read-mark:jibb-import.
13930:: entries, as [mark result] with the result from +read-mark:jibb-import.
@@ -11473,6 +13955,10 @@
11473++ golden-types-in-context
13955++ golden-types-in-context
11474 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
13956 |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
13958+ (golden-types-in-context-core file src externals mark-externals jimports prelude-values reserved-molds prelude ~)
13959+++ golden-types-in-context-core
13960+ |= [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)]
11476 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
13962 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
11477 =/ parsed (parse file src)
13963 =/ parsed (parse file src)
11478 ?: ?=(%| -.parsed) (show-error src p.parsed)
13964 ?: ?=(%| -.parsed) (show-error src p.parsed)
@@ -11488,6 +13974,41 @@
11488 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
13974 =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
11489 =/ cycles=(list icycle) (definite-value-cycles ds globals)
13975 =/ cycles=(list icycle) (definite-value-cycles ds globals)
11490 =/ env=ienv env.resolution
13976 =/ env=ienv env.resolution
13977+ =/ recovered=(list term) ~
13979+ ?& ?=(~ imports.p.parsed)
13981+ !?=([%ui %api *] file)
13982+ !?=([%ui %stores *] file)
13983+ !(lien (global-value-names ds) |=(n=term =(n %main)))
13984+ !(module-values-complete ds env)
13985+ (lte (met 3 src) 65.536)
13986+ (lte (lent ds) 64)
13987+ ?| &(?=(~ prepared) ?=(~ prelude) ?=(~ prelude-values) ?=(~ reserved-molds) (module-scope-valid p.parsed ~ ~) (dg-source-candidate ds 64))
13990+ =(u.prelude iface.u.prepared)
13991+ =(prelude-values values.u.prepared)
13992+ =(reserved-molds molds.u.prepared)
13993+ (module-scope-valid p.parsed values.u.prepared molds.u.prepared)
13994+ (dg-prepared-candidate ds 64)
13998+ =/ transaction=(unit dgcommit)
14000+ ?~ prepared (dg-root-source file src)
14001+ (dg-root-prepared file src u.prepared)
14004+ ?. &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) ~
14005+ (turn (skim env.u.transaction |=(entry=[name=term scheme=ischeme] ?=(~ (ienv-lookup name.entry env)))) |=(entry=[name=term scheme=ischeme] name.entry))
14007+ ?~ transaction env
14008+ ?: &((module-values-complete ds env.u.transaction) (dg-interface-safe env.u.transaction)) env.u.transaction
14010+ =/ source-defs=(map term def) (direct-checked-gates ds env)
14011+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11491 =/ lines=(list @t) ~
14012 =/ lines=(list @t) ~
11493 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
14014 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -11500,6 +14021,16 @@
11500 ?^ cycle
14021 ?^ cycle
11501 =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
14022 =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
11502 $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
14023 $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
14024+ ?: (lien recovered |=(n=term =(n name.d)))
14025+ =/ found=(unit ischeme) (ienv-lookup name.d env)
14026+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: committed definition unavailable") lines])
14027+ ?: (itype-has-hidden-recursive typ.u.found)
14028+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
14029+ ?: (itype-has-hidden-generic typ.u.found)
14030+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
14031+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
14032+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
14033+ $(ds t.ds, lines [line lines])
11503 ?: (lien grouped.resolution |=(n=term =(n name.d)))
14034 ?: (lien grouped.resolution |=(n=term =(n name.d)))
11504 =/ found=(unit ischeme) (ienv-lookup name.d env)
14035 =/ found=(unit ischeme) (ienv-lookup name.d env)
11505 ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
14036 ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
@@ -11507,7 +14038,9 @@
11507 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
14038 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
11508 $(ds t.ds, lines [line lines])
14039 $(ds t.ds, lines [line lines])
11509 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
14040 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11510− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~]
14041+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~ ~ ~ ~ ~ ~]
14042+ =. gate-defs.initial source-defs
14043+ =. head-evidence.initial heads
11511 =. initial (reserve-def-caps val.d initial)
14044 =. initial (reserve-def-caps val.d initial)
11512 =/ result=iresult
14045 =/ result=iresult
11513 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
14046 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -11547,4 +14080,667 @@
11547 =/ printable=itype (canonical-itype typ vars)
14080 =/ printable=itype (canonical-itype typ vars)
11548 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
14081 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
11549 $(ds t.ds, lines [line lines])
14082 $(ds t.ds, lines [line lines])
14083+:: Experimental module-owned pending-constraint generalization only.
14084+:: Inputs, IDs and substitution come from one checker-owned transaction.
14085++$ dgscan [ids=(list @ud) fuel=@ud]
14087+ |= [todo=(list itype) sub=isub fuel=@ud ids=(list @ud)]
14089+ ?~ todo `[ids fuel]
14091+ =. fuel (dec fuel)
14093+ ?: ?=(?(%var %avar %rvar %nvar %rnvar %tag) -.t)
14094+ =/ node-id=@ud ?:(?=(%tag -.t) id.t +.t)
14095+ =/ found=(unit itype) (itype-lookup node-id sub)
14096+ ?~ found $(todo t.todo, ids [node-id ids])
14097+ ?: &(?=(?(%rvar %rnvar) -.u.found) =(node-id +.u.found))
14098+ $(todo t.todo, ids [node-id ids])
14099+ $(todo [u.found t.todo])
14100+ ?: ?=(%jrec -.t) $(todo t.todo)
14102+ %collection $(todo (weld args.t t.todo))
14103+ %union $(todo (weld args.t (weld cases.t t.todo)))
14104+ %face $(todo [body.t t.todo])
14105+ %fn $(todo [sample.t product.t t.todo])
14106+ %cell $(todo [hed.t tal.t t.todo])
14107+ %atom $(todo t.todo)
14108+ %any-atom $(todo t.todo)
14109+ %flag $(todo t.todo)
14110+ %noun $(todo t.todo)
14111+ %empty $(todo t.todo)
14112+ %const $(todo t.todo)
14116+ |= [ids=(list @ud) sub=isub fuel=@ud blocked=(list @ud)]
14118+ ?~ ids `[blocked fuel]
14119+ =/ one=(unit dgscan) (dg-scan ~[[%var i.ids]] sub fuel blocked)
14121+ $(ids t.ids, fuel fuel.u.one, blocked ids.u.one)
14124+ |= [env=ienv sub=isub fuel=@ud blocked=(list @ud)]
14126+ ?~ env `[blocked fuel]
14127+ =/ sc=ischeme scheme.i.env
14128+ :: Quantifiers are local to the scheme: first find raw free IDs, then
14129+ :: follow those IDs in the module substitution without capturing them.
14130+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ fuel ~)
14132+ =/ free=(list @ud) (skim ids.u.raw |=(n=@ud !(lien vars.sc |=(q=@ud =(q n)))))
14133+ =/ resolved=(unit dgscan) (dg-scan-ids free sub fuel.u.raw blocked)
14135+ $(env t.env, fuel fuel.u.resolved, blocked ids.u.resolved)
14138+ |= [pending=(list dgo) sub=isub fuel=@ud blocked=(list @ud)]
14140+ ?~ pending `[blocked fuel]
14141+ =/ found=(unit dgscan) (dg-scan ~[left.i.pending right.i.pending] sub fuel blocked)
14143+ $(pending t.pending, fuel fuel.u.found, blocked ids.u.found)
14146+ |= [tags=(list ipending) sub=isub fuel=@ud blocked=(list @ud)]
14148+ ?~ tags `[blocked fuel]
14150+ =/ found=(unit itype) (itype-lookup id.i.tags sub)
14151+ ?~ found $(tags t.tags, fuel (dec fuel), blocked [id.i.tags blocked])
14152+ :: Until this entry is explicitly discharged, retain variables reachable
14153+ :: through its binding; mere existence of a substitution is not proof.
14154+ =/ reached=(unit dgscan) (dg-scan ~[u.found] sub (dec fuel) blocked)
14156+ $(tags t.tags, fuel fuel.u.reached, blocked ids.u.reached)
14159+ |= [typ=itype env=ienv pending=(list dgo) tags=(list ipending) captured=(list @ud) state=istate fuel=@ud]
14161+ :: Bound the obligation list and all graph/substitution walks. The
14162+ :: substitution is assumed checker-owned and occurs-checked.
14163+ ?: (gth (lent pending) 64) ~
14164+ =/ capt=(unit dgscan) (dg-scan-ids captured sub.state fuel ~)
14166+ =/ env-free=(unit dgscan) (dg-env env sub.state fuel.u.capt ids.u.capt)
14168+ =/ obligations=(unit dgscan) (dg-obligations pending sub.state fuel.u.env-free ids.u.env-free)
14170+ =/ tagged=(unit dgscan) (dg-tags tags sub.state fuel.u.obligations ids.u.obligations)
14172+ =/ bounded=(unit dgscan) (dg-scan ~[typ] sub.state fuel.u.tagged ~)
14174+ =/ normalized=itype (itype-normalize typ sub.state)
14175+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
14176+ =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
14177+ `[[normalized quantified]]
14179++$ dgcommit [env=ienv state=istate]
14180+:: A branch literal must not acquire a value face through replay.
14181+++ dg-literal-target-safe
14184+ ?: ?=(%union -.target)
14185+ (levy cases.target |=(c=itype ?=(?(%const %cell) -.c)))
14186+ ?=(?(%const %atom %any-atom %flag %noun) -.target)
14189+ |= [edges=(list dgo) state=istate fuel=@ud]
14193+ =/ trial=ifit (itype-fit left.i.edges right.i.edges sub.state next.state)
14194+ ?. ?=(%ok -.trial) ~
14196+ ?: ?=(%tag -.left.i.edges)
14197+ ?. constructor.left.i.edges
14198+ =/ closed=(unit dgscan) (dg-scan ~[right.i.edges] sub.trial 512 ~)
14201+ (dg-literal-target-safe (itype-normalize right.i.edges sub.trial))
14202+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
14203+ =((itype-walk left.i.edges sub.trial) (itype-walk right.i.edges sub.trial))
14205+ $(edges t.edges, state state(sub sub.trial, next next.trial), fuel (dec fuel))
14208+ |= [env=ienv sub=isub fuel=@ud]
14212+ =/ s=ischeme scheme.i.env
14213+ :: Quantified IDs are scheme-local and cannot be rewritten on publication.
14214+ ?. (levy vars.s |=(n=@ud ?=(~ (itype-lookup n sub)))) ~
14215+ =/ bounded=(unit dgscan) (dg-scan ~[typ.s] sub (dec fuel) ~)
14217+ =/ normalized=itype (itype-normalize typ.s sub)
14218+ ?: (itype-has-tag normalized) ~
14219+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
14220+ ?. (levy vars |=(n=@ud (lien vars.s |=(v=@ud =(v n))))) ~
14221+ =/ rest=(unit ienv) (dg-close-env t.env sub fuel.u.bounded)
14223+ `[[name.i.env [normalized vars.s]] u.rest]
14225+:: A deferred boolean branch has exactly the two literal flag patterns.
14226+:: Arms are inferred in order. Equal types are retained; two direct pending
14227+:: literals may instead retain source-owned obligations for later context.
14228+++ dg-boolean-patterns
14231+ ?. ?=(%branch -.e) |
14236+ =/ y=arm i.t.arms.e
14237+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) |
14238+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) |
14239+ !=(val.lit.pat.x val.lit.pat.y)
14240+:: Only a direct source literal which created its own unbound pending tag
14241+:: may create a branch edge. The caller must retain the exact source and state.
14242+++ dg-owned-arm-literal
14243+ |= [e=expr t=itype tags=(list ipending) sub=isub initial=@ud]
14247+ ?: constructor.t |
14248+ ?. =(lit.e literal.t) |
14249+ ?: (lth id.t initial) |
14250+ ?^ (itype-lookup id.t sub) |
14251+ (lien tags |=(x=ipending &(=(id.x id.t) =(literal.x literal.t))))
14252+++ dg-boolean-branch
14253+ |= [e=expr env=ienv state=istate]
14255+ ?. (dg-boolean-patterns e) [%| ["deferred branch patterns need unsupported inference" ~]]
14256+ ?> ?=(%branch -.e)
14260+ =/ y=arm i.t.arms.e
14261+ =/ subject=iresult (infer-fragment subject.e env state)
14262+ ?: ?=(%| -.subject) subject
14263+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
14264+ ?~ su [%| ["deferred branch subject does not unify with ?" ~]]
14265+ =/ left=iresult (infer-fragment val.x env state.p.subject(sub u.su))
14266+ ?: ?=(%| -.left) left
14267+ =/ right=iresult (infer-fragment val.y env state.p.left)
14268+ ?: ?=(%| -.right) right
14269+ ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)
14270+ =/ st=istate state.p.right
14271+ ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)
14272+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14273+ ?. (dg-owned-arm-literal val.y typ.p.right tags.st sub.st next.state)
14274+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14275+ ?> ?=(%tag -.typ.p.left)
14276+ ?> ?=(%tag -.typ.p.right)
14277+ ?: =(id.typ.p.left id.typ.p.right)
14278+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14279+ ?: (gth (lent obligations.st) 62)
14280+ [%| ["deferred branch arm context needs unsupported inference" ~]]
14281+ =/ result=itype [%var next.st]
14282+ =/ ex=dgo [typ.p.left result (span-of val.x) (span-of e)]
14283+ =/ ey=dgo [typ.p.right result (span-of val.y) (span-of e)]
14284+ [%& result st(next +(next.st), obligations [ex ey obligations.st])]
14285+ [%& typ.p.left state.p.right]
14287+:: A direct tuple literal may wait for a later exact result context.
14288+:: Each pending literal retains its source tag and its own fit obligation.
14289+++ dg-infer-tuple-items
14290+ |= [items=(list item) env=ienv state=istate]
14292+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
14293+ =/ head=iresult (infer-fragment val.i.items env state)
14294+ ?: ?=(%| -.head) head
14295+ =/ typ=itype typ.p.head
14296+ =/ st=istate state.p.head
14297+ =/ adjusted=(unit [typ=itype state=istate])
14298+ ?. (dg-owned-arm-literal val.i.items typ tags.st sub.st next.state) `[typ st]
14299+ ?: (gth (lent obligations.st) 63) ~
14300+ =/ pending=itype [%var next.st]
14301+ =/ edge=dgo [typ pending (span-of val.i.items) at.i.items]
14302+ `[pending st(next +(next.st), obligations [edge obligations.st])]
14303+ ?~ adjusted [%| ["deferred tuple context needs unsupported inference" ~]]
14304+ =. typ typ.u.adjusted
14305+ =. st state.u.adjusted
14306+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
14307+ ?~ t.items [%& typ st]
14308+ =/ tail=iresult $(items t.items, state st)
14309+ ?: ?=(%| -.tail) tail
14310+ [%& [%cell typ typ.p.tail] state.p.tail]
14312+:: Deferred inference uses only source forms whose successful fit sites are
14313+:: guarded below; a shared source-node budget bounds this screen.
14314+++ dg-safe-expressions
14315+ |= [todo=(list expr) fuel=@ud]
14318+ =/ first=(unit @ud) (dg-safe-expression i.todo fuel)
14320+ $(todo t.todo, fuel u.first)
14322+ |= [items=(list item) fuel=@ud]
14325+ =/ first=(unit @ud) (dg-safe-expression val.i.items fuel)
14327+ $(items t.items, fuel u.first)
14328+++ dg-safe-expression
14329+ |= [e=expr fuel=@ud]
14332+ =. fuel (dec fuel)
14334+ ?(%lit %ctor) `fuel
14335+ %wing ?:(?=([@ ~] names.e) `fuel ~)
14337+ ?. (levy pieces.e |=(p=piece ?=(%text -.p))) ~
14339+ %group $(e inner.e, fuel fuel)
14342+ $(e final.e, fuel fuel)
14343+ %gate $(e body.e, fuel fuel)
14344+ %gate-wide $(e body.e, fuel fuel)
14345+ %tuple (dg-safe-items items.e fuel)
14347+ ?. (dg-boolean-patterns e) ~
14350+ =/ subject=(unit @ud) $(e subject.e, fuel fuel)
14352+ (dg-safe-expressions ~[val.i.arms.e val.i.t.arms.e] u.subject)
14353+ %cast $(e val.e, fuel fuel)
14355+ =/ head=(unit @ud) $(e head.e, fuel fuel)
14357+ (dg-safe-expressions args.e u.head)
14359+:: Exact normalized equality is preserved by all later substitutions.
14360+:: The bounded scan declines opaque types and oversized inputs.
14362+ |= [actual=itype expected=itype sub=isub]
14364+ ?~ (dg-scan ~[actual expected] sub 512 ~) |
14365+ =((itype-normalize actual sub) (itype-normalize expected sub))
14367+:: A positional call peels sample-slot faces during its separate face check.
14368+:: Require its argument, sample and result closed so that check stays valid.
14369+++ dg-stable-call-fit
14370+ |= [actual=itype expected=itype product=itype sub=isub positional=?]
14372+ =/ checked=(unit dgscan) (dg-scan ~[actual expected product] sub 512 ~)
14374+ ?: &(positional ?=(^ ids.u.checked)) |
14375+ =((itype-normalize actual sub) (itype-normalize expected sub))
14377+:: One definition attempt retains state only when inference succeeds.
14378++$ dg-step [env=ienv state=istate pending=(list dgo)]
14380+ |= [d=def env=ienv state=istate]
14383+ ?~ (dg-safe-expression val.d 512) ~
14384+ =/ local=istate (reserve-def-caps val.d state)
14385+ :: This first slice declines all written capitals and holes/projections.
14387+ =/ ordinary=iresult (infer-fragment val.d env local)
14388+ ?: ?=(%| -.ordinary) ~
14389+ =/ typ=itype typ.p.ordinary
14390+ =/ after=istate state.p.ordinary
14391+ =/ edges=(list dgo) obligations.after
14392+ ?. =(binders.after binders.state) ~
14393+ ?. =(molds.after molds.state) ~
14394+ ?. =(globals.after globals.state) ~
14395+ ?. =(externals.after externals.state) ~
14396+ ?. =(surs.after surs.state) ~
14397+ ?. =(mark-externals.after mark-externals.state) ~
14398+ ?. =(marks.after marks.state) ~
14399+ ?. =(jimports.after jimports.state) ~
14400+ ?. =(reserved-molds.after reserved-molds.state) ~
14401+ ?. =(params.after params.state) ~
14402+ ?. =(active.after active.state) ~
14403+ ?. =(in-mold.after in-mold.state) ~
14404+ ?. =(at.after at.state) ~
14405+ ?. =(top-molds.after top-molds.state) ~
14406+ ?. =(prelude.after prelude.state) ~
14407+ ?. =(gate-defs.after gate-defs.state) ~
14408+ ?. =(head-evidence.after head-evidence.state) ~
14409+ ?. =(grec-index.after grec-index.state) ~
14410+ ?. =(defer.after defer.state) ~
14411+ ?. =(holes.after holes.state) ~
14412+ ?. =(caps.after caps.state) ~
14413+ ?. =(projections.after projections.state) ~
14414+ ?: (unsupported-atom-vars (itype-normalize typ sub.after) caps.after binders.after sub.after) ~
14415+ ?: (itype-has-nvar (itype-normalize typ sub.after)) ~
14416+ =/ scheme=(unit ischeme) (dg-generalize typ env edges tags.after ~ after 32.768)
14418+ `[[[name.d u.scheme] env] after edges]
14419+:: Retry only definitions that did not infer. Successful definitions are
14420+:: committed into the local transaction, never published until all close.
14422+ |= [ds=(list def) base=ienv env=ienv state=istate pending=(list dgo) fuel=@ud]
14423+ ^- (unit dgcommit)
14424+ ?: (gth fuel 64) ~
14425+ ?: (gth (lent ds) fuel) ~
14426+ =/ remaining=(list def) ds
14427+ =/ waiting=(list def) ~
14429+ =/ attempts=@ud (mul fuel fuel)
14434+ $(remaining (flop waiting), waiting ~, progress |)
14435+ =/ replayed=(unit istate) (dg-replay-edges pending state 64)
14437+ ?: (pending-tags tags.u.replayed sub.u.replayed) ~
14438+ =/ closed-edges=(unit dgscan) (dg-obligations pending sub.u.replayed 32.768 ~)
14440+ ?^ ids.u.closed-edges ~
14441+ =/ rechecked=(unit istate) (dg-replay-edges pending u.replayed 64)
14443+ ?. =(sub.u.rechecked sub.u.replayed) ~
14444+ ?. =(next.u.rechecked next.u.replayed) ~
14445+ =/ closed=(unit ienv) (dg-close-env env sub.u.replayed 32.768)
14447+ `[[u.closed u.replayed(defer ~, obligations ~)]]
14448+ ?: =(0 attempts) ~
14449+ =. attempts (dec attempts)
14450+ =/ d=def i.remaining
14451+ ?: ?=(%mold -.d) $(remaining t.remaining)
14452+ ?^ (ienv-lookup name.d base) $(remaining t.remaining)
14453+ ?^ (ienv-lookup name.d env) ~
14454+ =/ done=(unit dg-step) (dg-stage-one d env state)
14455+ ?~ done $(remaining t.remaining, waiting [d waiting])
14456+ $(remaining t.remaining, env env.u.done, state state.u.done, pending pending.u.done, progress &)
14458+:: Cheap bounded eligibility check on the already parsed source. This
14459+:: deliberately covers only direct constructor calls beneath transparent
14460+:: groups, gates, casts and definition-free bodies. Other shapes decline
14461+:: this fallback without a second parse or resolution pass.
14462+++ dg-direct-source
14463+ |= [e=expr fuel=@ud]
14467+ %group $(e inner.e, fuel (dec fuel))
14468+ %gate $(e body.e, fuel (dec fuel))
14469+ %gate-wide $(e body.e, fuel (dec fuel))
14470+ %cast $(e val.e, fuel (dec fuel))
14471+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
14473+ ?. ?=([* ~] args.e) |
14474+ ?=(%ctor -.i.args.e)
14476+++ dg-source-candidate
14477+ |= [ds=(list def) fuel=@ud]
14481+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
14482+ ?: (dg-direct-source val.i.ds 64) &
14483+ $(ds t.ds, fuel (dec fuel))
14485+++ dg-prepared-source
14486+ |= [e=expr fuel=@ud]
14488+ ?: (dg-direct-source e fuel) &
14491+ %group $(e inner.e, fuel (dec fuel))
14492+ %gate $(e body.e, fuel (dec fuel))
14493+ %gate-wide $(e body.e, fuel (dec fuel))
14494+ %cast $(e val.e, fuel (dec fuel))
14495+ %body ?~(defs.e $(e final.e, fuel (dec fuel)) |)
14498+++ dg-prepared-candidate
14499+ |= [ds=(list def) fuel=@ud]
14503+ ?. ?=(%value -.i.ds) $(ds t.ds, fuel (dec fuel))
14504+ ?: (dg-prepared-source val.i.ds 64) &
14505+ $(ds t.ds, fuel (dec fuel))
14507+++ dg-interface-safe
14511+ =/ sc=ischeme scheme.i.env
14512+ ?: |((itype-has-hidden-recursive typ.sc) (itype-has-hidden-generic typ.sc)) |
14513+ ?: (gth (lent vars.sc) 26) |
14515+:: Parse status and the transaction result come from the same source parse.
14516++$ dgparse [parsed=? result=(unit dgcommit)]
14518+ |= [at=path src=@t]
14519+ ^- (unit dgcommit)
14520+ result:(dg-root-detail at src)
14522+ |= [at=path src=@t]
14524+ =/ parsed (parse at src)
14525+ ?: ?=(%| -.parsed) [| ~]
14528+ ?^ imports.p.parsed ~
14529+ ?. (module-scope-valid p.parsed ~ ~) ~
14530+ ?^ (duplicate-defs defs.p.parsed) ~
14531+ =/ defs=(list def) defs.p.parsed
14532+ ?: (gth (lent defs) 64) ~
14533+ =/ molds=imolds (collect-simple-molds defs)
14534+ =/ globals=(list term) (global-value-names defs)
14535+ =/ resolution=iresolved (resolve-groups defs molds globals ~ ~ ~ ~ ~ ~ at ~)
14536+ ?^ grouped.resolution ~
14537+ ?^ artifacts.resolution ~
14538+ =/ base=ienv env.resolution
14539+ =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)
14542+ =/ all=(unit dgscan) (dg-all-env-ids base 32.768 ~)
14544+ =/ fresh=@ud (dg-next-id ids.u.all 0)
14545+ =/ st=istate *istate
14546+ =. 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)
14547+ =/ checked-molds=(each imold-types @t) (module-mold-types molds st)
14548+ ?: ?=(%| -.checked-molds) ~
14549+ (dg-stage defs base base st ~ 64)
14552+:: The caller supplies the trusted prepared prelude. This transaction is
14553+:: only report evidence; the ordinary module resolver does not publish it.
14554+++ dg-root-prepared
14555+ |= [at=path src=@t prepared=iprelude]
14556+ ^- (unit dgcommit)
14557+ ?: ?=([%ui %api *] at) ~
14558+ ?: ?=([%ui %stores *] at) ~
14559+ ?: (gth (met 3 src) 65.536) ~
14560+ =/ parsed (parse at src)
14561+ ?: ?=(%| -.parsed) ~
14562+ ?^ imports.p.parsed ~
14563+ ?. (module-scope-valid p.parsed values.prepared molds.prepared) ~
14564+ ?^ (duplicate-defs defs.p.parsed) ~
14565+ =/ defs=(list def) defs.p.parsed
14566+ ?: (gth (lent defs) 64) ~
14567+ ?: (lien (global-value-names defs) |=(n=term =(n %main))) ~
14568+ ?. (dg-prepared-candidate defs 64) ~
14569+ =/ local-molds=imolds (collect-simple-molds defs)
14570+ =/ globals=(list term) (weld values.prepared (global-value-names defs))
14571+ =/ iface=ifile iface.prepared
14572+ =/ prelude=(unit ifile) `iface
14573+ =/ resolution=iresolved
14574+ (resolve-groups defs local-molds globals ~ ~ ~ ~ ~ molds.prepared at prelude)
14575+ ?^ grouped.resolution ~
14576+ ?^ artifacts.resolution ~
14577+ =/ base=ienv env.resolution
14579+ (turn molds.iface |=(x=[name=term template=ischeme] [name.x template.x]))
14580+ =/ all-env=ienv (weld base (weld values.iface templates))
14581+ =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
14584+ =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)
14586+ =/ fresh=@ud (dg-next-id ids.u.all 0)
14587+ =/ st=istate *istate
14588+ =. 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)
14589+ =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
14590+ ?: ?=(%| -.checked-molds) ~
14591+ (dg-stage defs base base st ~ 64)
14594+ |= [env=ienv fuel=@ud ids=(list @ud)]
14596+ ?~ env `[ids fuel]
14598+ =/ sc=ischeme scheme.i.env
14599+ ?: (itype-has-tag typ.sc) ~
14600+ =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ (dec fuel) ids)
14602+ =/ quant=(unit dgscan) (dg-scan-ids vars.sc ~ fuel.u.raw ids.u.raw)
14604+ $(env t.env, fuel fuel.u.quant, ids ids.u.quant)
14607+ |= [ids=(list @ud) largest=@ud]
14610+ $(ids t.ids, largest (max largest i.ids))
14612+++ dg-eligible-ctor
14613+ |= [e=expr head=itype actual=itype expected=itype state=istate]
14615+ ?. ?=(%call -.e) ~
14616+ ?. ?=([* ~] args.e) ~
14617+ ?. ?=(%ctor -.i.args.e) ~
14618+ ?. ?=(%fn -.head) ~
14619+ ?. ?=(%fn -.expected) ~
14620+ ?. ?=(%tag -.actual) ~
14621+ ?. constructor.actual ~
14622+ ?. ?=(%var -.product.expected) ~
14623+ ?^ (itype-lookup id.product.expected sub.state) ~
14624+ =/ bounded=(unit dgscan) (dg-scan ~[sample.expected] sub.state 256 ~)
14626+ ?^ ids.u.bounded ~
14627+ `[[actual expected (span-of i.args.e) (span-of head.e)]]
14629+:: Experimental per-module, source-derived recursive tree index.
14630+:: The two tags and the exact children/list/self layout are fixed-shape
14631+:: checks, so ordinary definitions incur no type-tree or source scans.
14632+++ grec-tagged-fields
14634+ ^- (unit [tag=@ fields=(list field)])
14635+ ?. ?=(%cell -.sh) ~
14637+ =/ head=field i.fields.sh
14638+ ?. ?=(%bare -.head) ~
14639+ ?. ?=(%const -.shape.head) ~
14640+ ?. &(?=(%term form.lit.shape.head) =(%tas aura.lit.shape.head)) ~
14641+ `[val.lit.shape.head t.fields.sh]
14642+++ grec-tree-children
14643+ |= [fs=(list field) param=@t]
14648+ =/ event=field i.fs
14649+ =/ kids=field i.t.fs
14650+ ?. &(?=(%face -.event) ?=(%face -.kids)) ~
14651+ ?. !=(name.event name.kids) ~
14652+ ?. ?=(%fn -.shape.event) ~
14653+ ?. ?=(%aura -.sample.shape.event) ~
14654+ ?. =(%t aura.sample.shape.event) ~
14655+ ?. ?=(%tvar -.product.shape.event) ~
14656+ ?. =(param name.product.shape.event) ~
14660+ |= [name=term sh=shape]
14662+ ?. ?=(%generic -.sh) |
14663+ ?. ?=([@ ~] vars.sh) |
14664+ =/ param=@t i.vars.sh
14665+ ?. ?=(%union -.body.sh) |
14666+ ?. ?=([* [* ~]] cases.body.sh) |
14667+ =/ a=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.cases.body.sh)
14668+ =/ b=(unit [tag=@ fields=(list field)]) (grec-tagged-fields i.t.cases.body.sh)
14671+ ?. !=(tag.u.a tag.u.b) |
14672+ ?. ?=([* ~] fields.u.a) |
14673+ =/ value=field i.fields.u.a
14674+ ?. ?=(%face -.value) |
14675+ ?. ?=(%aura -.shape.value) |
14676+ ?. =(%t aura.shape.value) |
14677+ =/ selected=(unit field) (grec-tree-children fields.u.b param)
14679+ =/ kids=field u.selected
14680+ ?. ?=(%face -.kids) |
14681+ ?. ?=(%apply -.shape.kids) |
14682+ ?. =(ref.shape.kids ~[%list]) |
14683+ ?. ?=([* ~] args.shape.kids) |
14684+ =/ self=shape i.args.shape.kids
14685+ ?. ?=(%apply -.self) |
14686+ ?. =(ref.self ~[name]) |
14687+ ?. ?=([* ~] args.self) |
14688+ ?. ?=(%tvar -.i.args.self) |
14689+ =(name.i.args.self param)
14690++$ grec-collected [molds=imolds proofs=(map term shape)]
14691+:: Experimental one-layer analysis view, never an exported mold identity.
14692+++ grec-unfold-view
14693+ |= [typ=itype fuel=@ud]
14694+ ^- (unit [view=itype left=@ud])
14695+ ?. ?=(%grec -.typ) ~
14697+ ?. ?=([* ~] args.typ) ~
14698+ =/ sh=shape proof.typ
14699+ ?. (grec-tree-proof name.typ sh) ~
14700+ ?> ?=(%generic -.sh)
14701+ ?> ?=([@ ~] vars.sh)
14702+ ?> ?=(%union -.body.sh)
14703+ ?> ?=([* [* ~]] cases.body.sh)
14704+ =/ ca=shape i.cases.body.sh
14705+ =/ cb=shape i.t.cases.body.sh
14708+ ?> ?=([* [* ~]] fields.ca)
14709+ ?> ?=([* *] fields.cb)
14710+ =/ tag-a=field i.fields.ca
14711+ =/ tag-b=field i.fields.cb
14712+ ?> ?=(%bare -.tag-a)
14713+ ?> ?=(%bare -.tag-b)
14714+ ?> ?=(%const -.shape.tag-a)
14715+ ?> ?=(%const -.shape.tag-b)
14716+ =/ text-field=field i.t.fields.ca
14717+ ?> ?=(%face -.text-field)
14718+ =/ branch=(list field) t.fields.cb
14719+ =/ kids=(unit field) (grec-tree-children branch i.vars.sh)
14721+ ?> ?=(%face -.u.kids)
14722+ =/ children=itype [%face name.u.kids [%collection %list ~[typ]]]
14725+ ?~ t.branch children
14726+ =/ event=field i.branch
14727+ ?> ?=(%face -.event)
14728+ [%cell [%face name.event [%fn [%atom %t] i.args.typ]] children]
14729+ =/ leaf=itype [%cell [%const lit.shape.tag-a] [%face name.text-field [%atom %t]]]
14730+ =/ node=itype [%cell [%const lit.shape.tag-b] payload]
14731+ `[[%union ~[leaf node] ~ ~ ~] (dec fuel)]
14733+++ grec-collect-molds
14736+ ?~ ds [~ *(map term shape)]
14737+ =/ rest=grec-collected $(ds t.ds)
14738+ ?. ?=(%mold -.i.ds) rest
14739+ =/ name=term name.i.ds
14740+ =/ body=shape shape.i.ds
14741+ =/ proofs=(map term shape) proofs.rest
14742+ =? proofs (grec-tree-proof name body) (~(put by proofs) name body)
14743+ [[[name body] molds.rest] proofs]