@@ -4608,8 +4608,11 @@
46084608 [%atom aura=@ta]
46094609 [%any-atom ~]
46104610 [%flag ~]
4611+ [%noun ~]
46114612 [%tag id=@ud literal=lit constructor=?]
46124613 [%const literal=lit]
4614+ [%collection name=term args=(list itype)]
4615+ [%recursive module=term name=term label=(unit @t)]
46134616 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46144617 [%face name=term body=itype]
46154618 [%fn sample=itype product=itype]
@@ -4617,6 +4620,7 @@
46174620 ==
46184621+$ ibinding [id=@ud val=itype]
46194622+$ isub (list ibinding)
4623++$ ipending [id=@ud literal=lit]
46204624::
46214625++ itype-lookup
46224626 |= [n=@ud sub=isub]
@@ -4658,9 +4662,12 @@
46584662 %atom |
46594663 %any-atom |
46604664 %flag |
4665+ %noun |
46614666 %tag =(n id.t)
46624667 %const |
46634668 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4669+ %recursive |
4670+ %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
46644671 %face $(t body.t)
46654672 %fn |($(t sample.t) $(t product.t))
46664673 %cell |($(t hed.t) $(t tal.t))
@@ -4678,11 +4685,16 @@
46784685 =. a (itype-walk a sub)
46794686 =. b (itype-walk b sub)
46804687 ?: =(a b) `sub
4688+ ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4689+ ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
46814690 ?: &(?=(%union -.a) ?=(%union -.b))
46824691 ?. =(origin.a origin.b) ~
46834692 ?: &(?=(~ args.a) ?=(~ args.b)) ?:(=(cases.a cases.b) `sub ~)
46844693 ?~ origin.a ~
46854694 (itype-unify-args args.a args.b sub)
4695+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4696+ ?. =(name.a name.b) ~
4697+ (itype-unify-args args.a args.b sub)
46864698 ?: ?=(%var -.a)
46874699 ?: (itype-occurs id.a b sub) ~
46884700 `[[id.a b] sub]
@@ -4747,9 +4759,12 @@
47474759 %atom |
47484760 %any-atom &
47494761 %flag |
4762+ %noun |
47504763 %tag |
47514764 %const |
47524765 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4766+ %recursive |
4767+ %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
47534768 %face $(t body.t)
47544769 %fn |($(t sample.t) $(t product.t))
47554770 %cell |($(t hed.t) $(t tal.t))
@@ -4773,6 +4788,14 @@
47734788:: Related auras in a structural unification need a common-type rule;
47744789:: until that rule is implemented, report an unknown rather than error.
47754790::
4791+++ itype-family-related-collection-args
4792+ |= [as=(list itype) bs=(list itype) sub=isub]
4793+ ^- ?
4794+ ?~ as |
4795+ ?~ bs |
4796+ ?: (itype-family-related i.as i.bs sub) &
4797+ $(as t.as, bs t.bs)
4798+::
47764799++ itype-family-related
47774800 |= [a=itype b=itype sub=isub]
47784801 ^- ?
@@ -4781,6 +4804,9 @@
47814804 ?: &(?=(%atom -.a) ?=(%atom -.b))
47824805 ?. !=(aura.a aura.b) |
47834806 |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4807+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4808+ ?. =(name.a name.b) |
4809+ (itype-family-related-collection-args args.a args.b sub)
47844810 ?: &(?=(%face -.a) ?=(%face -.b))
47854811 ?. =(name.a name.b) |
47864812 $(a body.a, b body.b)
@@ -4804,9 +4830,12 @@
48044830 %atom &
48054831 %any-atom &
48064832 %flag &
4833+ %noun |
48074834 %tag &
48084835 %const &
48094836 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4837+ %recursive |
4838+ %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
48104839 %face $(typ body.typ)
48114840 %fn |($(typ sample.typ) $(typ product.typ))
48124841 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -4834,17 +4863,29 @@
48344863 ^- ?
48354864 =. t (itype-walk t sub)
48364865 ?- -.t
4866+ %collection (lien args.t |=(c=itype (itype-has-face c sub)))
48374867 %face &
48384868 %cell |($(t hed.t) $(t tal.t))
48394869 %fn |($(t sample.t) $(t product.t))
48404870 * |
48414871 ==
48424872::
4873+++ itype-face-asym-collection-args
4874+ |= [as=(list itype) bs=(list itype) sub=isub]
4875+ ^- ?
4876+ ?~ as |
4877+ ?~ bs |
4878+ ?: (itype-face-asym i.as i.bs sub) &
4879+ $(as t.as, bs t.bs)
4880+::
48434881++ itype-face-asym
48444882 |= [a=itype b=itype sub=isub]
48454883 ^- ?
48464884 =. a (itype-walk a sub)
48474885 =. b (itype-walk b sub)
4886+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4887+ ?. =(name.a name.b) |
4888+ (itype-face-asym-collection-args args.a args.b sub)
48484889 ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
48494890 ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
48504891 ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
@@ -4878,16 +4919,26 @@
48784919 %var &
48794920 %cell &
48804921 %union &
4922+ %recursive &
4923+ %noun &
4924+ %collection &
48814925 %face $(t body.t)
48824926 %fn |($(t sample.t) $(t product.t))
48834927 * |
48844928 ==
48854929::
48864930++ pending-tags
4887− |= [tags=(list @ud) sub=isub]
4931+ |= [tags=(list ipending) sub=isub]
48884932 ^- ?
48894933 ?~ tags |
4890− ?~ (itype-lookup i.tags sub) &
4934+ ?~ (itype-lookup id.i.tags sub) &
4935+ $(tags t.tags)
4936+::
4937+++ pending-null
4938+ |= [tags=(list ipending) sub=isub]
4939+ ^- ?
4940+ ?~ tags |
4941+ ?: &(?=(%null form.literal.i.tags) ?=(~ (itype-lookup id.i.tags sub))) &
48914942 $(tags t.tags)
48924943::
48934944:: Tags remain constrained until a mold selects a case or permitted atom
@@ -4898,6 +4949,7 @@
48984949 ^- ?
48994950 ?- -.t
49004951 %tag &
4952+ %collection (lien args.t |=(c=itype (itype-has-tag c)))
49014953 %face $(t body.t)
49024954 %fn |($(t sample.t) $(t product.t))
49034955 %cell |($(t hed.t) $(t tal.t))
@@ -4910,6 +4962,7 @@
49104962 ^- ?
49114963 ?- -.t
49124964 %union &
4965+ %collection (lien args.t |=(c=itype (itype-has-union c)))
49134966 %face $(t body.t)
49144967 %fn |($(t sample.t) $(t product.t))
49154968 %cell |($(t hed.t) $(t tal.t))
@@ -4927,12 +4980,39 @@
49274980 %union
49284981 ?: &(?=(~ label.t) ?=(^ args.t)) &
49294982 (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
4983+ %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
49304984 %face $(t body.t)
49314985 %fn |($(t sample.t) $(t product.t))
49324986 %cell |($(t hed.t) $(t tal.t))
49334987 * |
49344988 ==
49354989::
4990+++ itype-has-recursive
4991+ |= t=itype
4992+ ^- ?
4993+ ?- -.t
4994+ %recursive &
4995+ %collection (lien args.t |=(c=itype (itype-has-recursive c)))
4996+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
4997+ %face $(t body.t)
4998+ %cell |($(t hed.t) $(t tal.t))
4999+ %fn |($(t sample.t) $(t product.t))
5000+ * |
5001+ ==
5002+::
5003+++ itype-has-hidden-recursive
5004+ |= t=itype
5005+ ^- ?
5006+ ?- -.t
5007+ %recursive ?=(~ label.t)
5008+ %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5009+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5010+ %face $(t body.t)
5011+ %cell |($(t hed.t) $(t tal.t))
5012+ %fn |($(t sample.t) $(t product.t))
5013+ * |
5014+ ==
5015+::
49365016++ itype-fit-cases
49375017 |= [actual=itype cases=(list itype) sub=isub next=@ud]
49385018 ^- ifit
@@ -4966,6 +5046,7 @@
49665046 ?. ?=(%cell -.c) $(cases t.cases)
49675047 =/ head=itype (itype-walk hed.c sub)
49685048 ?. ?=(%const -.head) $(cases t.cases)
5049+ ?. =(%term form.literal.head) $(cases t.cases)
49695050 ?. =(val.literal.head val.tag) $(cases t.cases)
49705051 ?^ found [%unknown ~]
49715052 =/ trial=ifit (itype-fit sample tal.c sub next)
@@ -4979,6 +5060,18 @@
49795060 =. actual (itype-walk actual sub)
49805061 =. expected (itype-walk expected sub)
49815062 ?: =(actual expected) [%ok sub next]
5063+ :: Any value can be used where a noun is expected. An unresolved
5064+ :: bare tag is fixed as a constant; a constructor still needs a gate.
5065+ ?: ?=(%noun -.expected)
5066+ ?: ?=(%tag -.actual)
5067+ ?: constructor.actual [%unknown ~]
5068+ [%ok [[id.actual expected] sub] next]
5069+ [%ok sub next]
5070+ :: An arbitrary noun is not known to fit a narrower type.
5071+ ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5072+ ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
5073+ ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
5074+ ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
49825075 ?: &(?=(%union -.actual) ?=(%union -.expected))
49835076 ?. =(origin.actual origin.expected) [%unknown ~]
49845077 ?: &(?=(~ args.actual) ?=(~ args.expected))
@@ -4987,6 +5080,10 @@
49875080 =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
49885081 ?^ unified [%ok u.unified next]
49895082 [%unknown ~]
5083+ :: A concrete union value in a tuple may acquire the expected field's
5084+ :: face. A variable-bound union still needs face propagation support.
5085+ ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5086+ $(expected body.expected)
49905087 ?: ?=(%union -.actual) [%unknown ~]
49915088 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
49925089 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -5005,6 +5102,10 @@
50055102 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
50065103 ?. ?=(%ok -.trial) trial
50075104 [%ok [[id.actual expected] sub.trial] next.trial]
5105+ :: Zero may be the empty list. A nested cell fit lacks the context
5106+ :: needed to resolve it here, so do not report a definite mismatch.
5107+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5108+ [%unknown ~]
50085109 ?: ?=(%const -.expected)
50095110 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
50105111 ?: ?=(%atom -.expected)
@@ -5022,6 +5123,8 @@
50225123 [%ok u.u next]
50235124 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
50245125 ?: ?=(%face -.expected) $(expected body.expected)
5126+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5127+ [%unknown ~]
50255128 ?: ?=(%const -.expected)
50265129 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
50275130 ?: ?=(%atom -.expected)
@@ -5054,11 +5157,22 @@
50545157 =/ first=ifit $(actual hed.actual, expected hed.expected)
50555158 ?. ?=(%ok -.first) first
50565159 $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
5160+ :: A field may add a face to an occurrence of the very same type
5161+ :: variable. Binding that variable to a face around itself would fail
5162+ :: the occurs check, but its underlying type has already matched.
5163+ ?: &(?=(%var -.actual) ?=(%face -.expected) =(actual (itype-walk body.expected sub)))
5164+ [%ok sub next]
5165+ :: Differing variables and faces need propagation that is not yet
5166+ :: represented. Binding one to the face can create a false mismatch.
5167+ ?: &(?=(%var -.actual) ?=(%face -.expected)) [%unknown ~]
5168+ ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
50575169 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
50585170 [%unknown ~]
50595171 ?: |(?=(%var -.actual) ?=(%var -.expected))
50605172 =/ unified=(unit isub) (itype-unify actual expected sub)
50615173 ?~ unified
5174+ ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5175+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
50625176 ?: (itype-family-related actual expected sub) [%unknown ~]
50635177 [%bad ~]
50645178 [%ok u.unified next]
@@ -5073,6 +5187,7 @@
50735187 =/ unified=(unit isub) (itype-unify actual expected sub)
50745188 ?~ unified
50755189 ?: |((itype-has-union (itype-normalize actual sub)) (itype-has-union (itype-normalize expected sub))) [%unknown ~]
5190+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
50765191 ?: (itype-family-related actual expected sub) [%unknown ~]
50775192 [%bad ~]
50785193 [%ok u.unified next]
@@ -5101,25 +5216,58 @@
51015216 ["a shared type variable should reject incompatible arguments" problems]
51025217 =? problems ?=(~ (itype-unify same fine ~))
51035218 ["a shared type variable should accept equal arguments" problems]
5219+ =/ list-a=itype [%collection %list ~[a]]
5220+ =/ list-t=itype [%collection %list ~[txt]]
5221+ =/ list-n=itype [%collection %list ~[num]]
5222+ =? problems ?=(^ (itype-unify a list-a ~))
5223+ ["occurs check should look through collection arguments" problems]
5224+ =? problems !=((itype-vars list-a) ~[0])
5225+ ["generalization should see collection argument variables" problems]
5226+ =? problems !=((itype-rename list-a ~[[0 num]]) list-n)
5227+ ["instantiation should rename collection argument variables" problems]
5228+ =? problems ?=(^ (itype-unify list-t list-n ~))
5229+ ["collection arguments with different auras should conflict" problems]
5230+ =? problems ?=(^ (itype-unify list-t [%collection %unit ~[txt]] ~))
5231+ ["different collection names should conflict" problems]
5232+ =? problems !(itype-family-related list-t [%collection %list ~[[%atom 'tD']]] ~)
5233+ ["collection arguments should preserve aura-family uncertainty" problems]
5234+ =? problems !(itype-face-asym [%collection %list ~[[%face %x txt]]] list-t ~)
5235+ ["collection arguments should preserve face uncertainty" problems]
5236+ =/ recursive=itype [%recursive %fixture %chain `'chain.fixture']
5237+ =/ same-recursive=itype [%recursive %fixture %chain ~]
5238+ =/ other-recursive=itype [%recursive %other %chain `'chain.other']
5239+ =? problems ?=(~ (itype-unify recursive same-recursive ~))
5240+ ["recursive identity should not depend on its visible name" problems]
5241+ =? problems ?=(^ (itype-unify recursive other-recursive ~))
5242+ ["recursive identity should include the source module" problems]
5243+ =/ recursive-fit=ifit (itype-fit recursive txt ~ 0)
5244+ =? problems !?=(%unknown -.recursive-fit)
5245+ ["opaque recursive types should not be unfolded by a fit" problems]
5246+ =/ nested-fit=ifit
5247+ (itype-fit [%collection %list ~[a]] list-t ~[[0 recursive]] 1)
5248+ =? problems !?=(%unknown -.nested-fit)
5249+ ["recursive types behind substitutions should remain uncertain" problems]
51045250 problems
51055251::
51065252:: The expression inference below is deliberately a fragment: bindings,
5107−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5253+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
51085254:: result for unsupported syntax is a diagnostic, never a checked module.
51095255::
51105256+$ ischeme [typ=itype vars=(list @ud)]
51115257+$ ienv (list [name=term scheme=ischeme])
51125258+$ imold-types (list [name=term template=ischeme])
5113−+$ ifile [values=ienv molds=imold-types at=path]
5259++$ iderived [name=term agent=term mark=term]
5260++$ ifile [values=ienv molds=imold-types at=path derived=(list iderived)]
51145261+$ ijimports (list [face=term interface=ifile])
5115−+$ icaps (list [name=@t id=@ud])
5262++$ icap [name=@t id=@ud at=span]
5263++$ icaps (list icap)
51165264+$ iparams (list [name=@t typ=itype])
51175265+$ imolds (list [name=term body=shape])
51185266:: A caller supplies the exact noun returned by +read-mold:jibb-import.
51195267:: This core has no Ford dependencies; unrecognized payloads fail closed.
51205268+$ iexternals (list [module=term name=term result=*])
51215269+$ imark-externals (list [mark=term result=*])
5122−+$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list @ud) in-mold=? at=path top-molds=(list term)]
5270++$ 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)]
51235271+$ idiag [msg=tape sites=(list [at=span note=tape])]
51245272+$ iresult (each [typ=itype state=istate] idiag)
51255273+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5139,6 +5287,7 @@
51395287 |= [t=itype sub=isub]
51405288 ^- itype
51415289 =. t (itype-walk t sub)
5290+ ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
51425291 ?: ?=(%union -.t)
51435292 [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
51445293 ?: ?=(%face -.t)
@@ -5154,12 +5303,16 @@
51545303:: generalize an aura from its sample, which requires constraint analysis
51555304:: beyond this fragment; leave those cases unresolved.
51565305::
5306+:: This helper only controls decimal defaulting in visible types. A noun
5307+:: may contain gates and is not proof of a gate-free value.
51575308++ itype-has-gate
51585309 |= t=itype
51595310 ^- ?
51605311 ?- -.t
51615312 %fn &
51625313 %cell |($(t hed.t) $(t tal.t))
5314+ %recursive |
5315+ %collection (lien args.t |=(c=itype (itype-has-gate c)))
51635316 %face $(t body.t)
51645317 %union (lien cases.t |=(c=itype (itype-has-gate c)))
51655318 %tag |
@@ -5170,6 +5323,7 @@
51705323 %atom |
51715324 %any-atom |
51725325 %flag |
5326+ %noun |
51735327 ==
51745328::
51755329++ default-decimals
@@ -5178,6 +5332,7 @@
51785332 ?: (itype-has-gate t) t
51795333 ?- -.t
51805334 %nvar [%atom %ud]
5335+ %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
51815336 %face [%face name.t $(t body.t)]
51825337 %cell [%cell $(t hed.t) $(t tal.t)]
51835338 * t
@@ -5193,9 +5348,12 @@
51935348 %atom ~
51945349 %any-atom ~
51955350 %flag ~
5351+ %noun ~
51965352 %tag ~
51975353 %const ~
51985354 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5355+ %recursive ~
5356+ %collection (zing (turn args.t |=(c=itype (itype-vars c))))
51995357 %face $(t body.t)
52005358 %fn (weld $(t sample.t) $(t product.t))
52015359 %cell (weld $(t hed.t) $(t tal.t))
@@ -5229,9 +5387,12 @@
52295387 %atom t
52305388 %any-atom t
52315389 %flag t
5390+ %noun t
52325391 %tag t
52335392 %const t
52345393 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5394+ %recursive t
5395+ %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
52355396 %face [%face name.t $(t body.t)]
52365397 %fn [%fn $(t sample.t) $(t product.t)]
52375398 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5250,9 +5411,12 @@
52505411 %atom |
52515412 %any-atom |
52525413 %flag |
5414+ %noun |
52535415 %tag |
52545416 %const |
52555417 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5418+ %recursive |
5419+ %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
52565420 %face $(t body.t)
52575421 %fn |($(t sample.t) $(t product.t))
52585422 %cell |($(t hed.t) $(t tal.t))
@@ -5314,9 +5478,12 @@
53145478 $(ds t.ds)
53155479::
53165480::
5317−:: The importer owns its algebra. Fixed atoms, cells and Jibb-named faces
5318−:: are decoded recursively. Singletons, unions, collections, recursive
5319−:: references and invalid face names remain unsupported, never widened.
5481+:: The caller supplies unchanged results from the source-aware importer.
5482+:: That boundary is trusted for source provenance: a fork alone cannot
5483+:: reveal cases Hoon collapsed before it was constructed. Validate the
5484+:: supplied graph independently, including pairwise disjointness. Fixed
5485+:: atoms, term singletons, cells, faces and proven forks are decoded;
5486+:: unsupported singletons, collections and recursive references fail.
53205487::
53215488++ jibb-face-name
53225489 |= name=@
@@ -5326,16 +5493,162 @@
53265493 ?. (is-lower i.chars) |
53275494 (levy t.chars |=(c=@tD (in c name-mask)))
53285495::
5496+:: A source-aware reader result is trusted for origin. Validate every
5497+:: supplied branch and keep the recursive mold opaque: unfolding its
5498+:: root while naming only its tail would change its type identity.
5499++$ irec-pattern [pat=upat has=?]
5500+++ rec-pattern
5501+ |= [node=* module=term name=term]
5502+ ^- (unit irec-pattern)
5503+ ?@ node ~
5504+ ?+ -.node ~
5505+ %atom
5506+ ?: ?=([%atom %n [~ @]] node)
5507+ ?. =(0 +>+.node) ~
5508+ `[[%atom `0] |]
5509+ ?: ?=([%atom %tas [~ @]] node)
5510+ =/ value=@ +>+.node
5511+ ?. |(=(value 0) (jibb-face-name value)) ~
5512+ `[[%atom `value] |]
5513+ ?. ?=([%atom @ ~] node) ~
5514+ =/ aura=@ta (@ta +<.node)
5515+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5516+ `[[%atom ~] |]
5517+ %ref
5518+ ?. ?=([%ref @ @] node) ~
5519+ ?. &(=(module +<.node) =(name +>.node)) ~
5520+ `[[%unknown ~] &]
5521+ %face
5522+ ?. ?=([%face @ *] node) ~
5523+ ?. (jibb-face-name +<.node) ~
5524+ $(node +>.node)
5525+ %cell
5526+ ?. ?=([%cell * *] node) ~
5527+ =/ left $(node +<.node)
5528+ ?~ left ~
5529+ =/ right $(node +>.node)
5530+ ?~ right ~
5531+ `[[%cell pat.u.left pat.u.right] |(has.u.left has.u.right)]
5532+ %fork
5533+ =/ cases (rec-patterns +.node module name)
5534+ ?~ cases ~
5535+ ?~ pats.u.cases ~
5536+ ?~ t.pats.u.cases ~
5537+ ?. (rec-patterns-disjoint pats.u.cases) ~
5538+ `[[%or pats.u.cases] has.u.cases]
5539+ ==
5540+::
5541+++ rec-patterns
5542+ |= [nodes=* module=term name=term]
5543+ ^- (unit [pats=(list upat) has=?])
5544+ ?@ nodes ?:(=(nodes 0) `[~ |] ~)
5545+ =/ first (rec-pattern -.nodes module name)
5546+ ?~ first ~
5547+ =/ rest $(nodes +.nodes)
5548+ ?~ rest ~
5549+ `[[pat.u.first pats.u.rest] |(has.u.first has.u.rest)]
5550+::
5551+++ rec-patterns-disjoint
5552+ |= pats=(list upat)
5553+ ^- ?
5554+ ?~ pats &
5555+ ?. (levy t.pats |=(p=upat =(%disjoint (union-relate i.pats p)))) |
5556+ $(pats t.pats)
5557+::
5558+::
5559+::
5560+:: Repeated faces along an imported record spine fail closed. Hoon's type
5561+:: graph can erase unfaced nested-cell boundaries, so that alone does not
5562+:: prove the original source repeated a name within one record. A faced
5563+:: body and each union alternative have separate scopes. Check recursive
5564+:: roots before making them opaque; unused molds are never inspected.
5565+::
5566+++ imported-faces-valid
5567+ |= node=*
5568+ ^- ?
5569+ ?@ node &
5570+ ?+ -.node &
5571+ %face ?:(?=([%face @ *] node) $(node +>.node) |)
5572+ %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
5573+ %fork (imported-faces-valid-list +.node)
5574+ %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
5575+ ==
5576+::
5577+++ imported-faces-valid-list
5578+ |= nodes=*
5579+ ^- ?
5580+ ?@ nodes =(nodes 0)
5581+ ?. (imported-faces-valid -.nodes) |
5582+ $(nodes +.nodes)
5583+::
5584+++ imported-record-faces-valid
5585+ |= [node=* names=(list @)]
5586+ ^- ?
5587+ ?: ?=([%cell * *] node)
5588+ =/ head=* +<.node
5589+ =/ rest=* +>.node
5590+ ?: ?=([%face @ *] head)
5591+ ?: (lien names |=(n=@ =(n +<.head))) |
5592+ ?. (imported-faces-valid +>.head) |
5593+ $(node rest, names [+<.head names])
5594+ ?. (imported-faces-valid head) |
5595+ $(node rest)
5596+ ?: ?=([%face @ *] node)
5597+ ?: (lien names |=(n=@ =(n +<.node))) |
5598+ (imported-faces-valid +>.node)
5599+ (imported-faces-valid node)
5600+::
53295601++ import-to-itype
53305602 |= node=*
53315603 ^- (unit itype)
53325604 ?@ node ~
53335605 ?+ -.node ~
5606+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
53345607 %atom
5608+ :: A Hoon loobean singleton is one of the two Jibb loobeans.
5609+ ?: ?=([%atom %f [~ @]] node)
5610+ =/ value=@ +>+.node
5611+ ?. |(=(value 0) =(value 1)) ~
5612+ =/ printed=@t ?:(=(value 0) '%.y' '%.n')
5613+ `[%const [%loobean %f value printed]]
5614+ :: Hoon's null singleton is the same noun as Jibb's `~` mold.
5615+ :: Other non-term singleton atoms remain unsupported here.
5616+ ?: ?=([%atom %n [~ @]] node)
5617+ ?. =(0 +>+.node) ~
5618+ `[%const [%null %n 0 '~']]
5619+ ?: ?=([%atom %tas [~ @]] node)
5620+ =/ value=@ +>+.node
5621+ ?. |(=(value 0) (jibb-face-name value)) ~
5622+ =/ printed=@t ?:(=(value 0) '%$' (cat 3 '%' value))
5623+ `[%const [%term %tas value printed]]
53355624 ?. ?=([%atom @ ~] node) ~
53365625 =/ aura=@ta (@ta +<.node)
53375626 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
53385627 `[%atom aura]
5628+ %apply
5629+ ?. ?=([%apply @ *] node) ~
5630+ =/ name=term (@tas +<.node)
5631+ =/ arity=@ud
5632+ ?: |(=(%list name) =(%unit name) =(%set name) =(%qeu name)) 1
5633+ ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
5634+ 0
5635+ ?: =(arity 0) ~
5636+ =/ args=(unit (list itype)) (import-to-itypes +>.node)
5637+ ?~ args ~
5638+ ?. =(arity (lent u.args)) ~
5639+ `[%collection name u.args]
5640+ %fork
5641+ :: Hoon's ordinary ? mold is the fork of its two %f singletons.
5642+ =/ raw=* +.node
5643+ ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
5644+ `[%flag ~]
5645+ =/ cases=(unit (list itype)) (import-to-itypes raw)
5646+ ?~ cases ~
5647+ ?~ u.cases ~
5648+ ?~ t.u.cases ~
5649+ ?: (import-has-loobean-singleton u.cases) ~
5650+ ?. (import-cases-disjoint u.cases) ~
5651+ `[%union u.cases ~ ~ ~]
53395652 %face
53405653 ?. ?=([%face @ *] node) ~
53415654 =/ name=@ +<.node
@@ -5352,6 +5665,52 @@
53525665 `[%cell u.left u.right]
53535666 ==
53545667::
5668+++ import-direct-loobean
5669+ |= t=itype
5670+ ^- ?
5671+ ?: ?=(%face -.t) $(t body.t)
5672+ ?: ?=(%union -.t) (import-has-loobean-singleton cases.t)
5673+ ?=([%const [%loobean *]] t)
5674+::
5675+++ import-has-loobean-singleton
5676+ |= cases=(list itype)
5677+ ^- ?
5678+ ?~ cases |
5679+ ?: (import-direct-loobean i.cases) &
5680+ $(cases t.cases)
5681+::
5682+++ import-to-itypes
5683+ |= nodes=*
5684+ ^- (unit (list itype))
5685+ ?@ nodes ?:(=(nodes 0) `~ ~)
5686+ =/ first (import-to-itype -.nodes)
5687+ ?~ first ~
5688+ =/ rest $(nodes +.nodes)
5689+ ?~ rest ~
5690+ `[u.first u.rest]
5691+::
5692+++ import-type-pattern
5693+ |= typ=itype
5694+ ^- upat
5695+ ?- -.typ
5696+ %noun [%all ~]
5697+ %atom [%atom ~]
5698+ %flag [%or ~[[%atom `0] [%atom `1]]]
5699+ %const [%atom `val.literal.typ]
5700+ %face $(typ body.typ)
5701+ %cell [%cell $(typ hed.typ) $(typ tal.typ)]
5702+ %union [%or (turn cases.typ |=(t=itype (import-type-pattern t)))]
5703+ * [%unknown ~]
5704+ ==
5705+::
5706+++ import-cases-disjoint
5707+ |= cases=(list itype)
5708+ ^- ?
5709+ ?~ cases &
5710+ =/ first=upat (import-type-pattern i.cases)
5711+ ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
5712+ $(cases t.cases)
5713+::
53555714++ find-imported-mold
53565715 |= [module=term name=term externals=iexternals surs=(list term)]
53575716 ^- (unit itype)
@@ -5363,7 +5722,15 @@
53635722 =/ result=* result.i.found
53645723 ?@ result ~
53655724 ?. ?=(%& -.result) ~
5366− (import-to-itype +.result)
5725+ =/ node=* +.result
5726+ ?. (imported-faces-valid node) ~
5727+ ?@ node (import-to-itype node)
5728+ ?: ?=(%ref -.node) (import-to-itype node)
5729+ =/ pattern=(unit irec-pattern) (rec-pattern node module name)
5730+ ?~ pattern (import-to-itype node)
5731+ ?. has.u.pattern (import-to-itype node)
5732+ `[%recursive module name `(crip "{(trip name)}.{(trip module)}")]
5733+
53675734::
53685735++ collect-sur-imports
53695736 |= imports=(list import)
@@ -5392,6 +5759,7 @@
53925759 =/ result=* result.i.found
53935760 ?@ result ~
53945761 ?. ?=(%& -.result) ~
5762+ ?. (imported-faces-valid +.result) ~
53955763 (import-to-itype +.result)
53965764::
53975765++ find-jibb-interface
@@ -5422,22 +5790,41 @@
54225790 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
54235791 $(molds t.molds)
54245792::
5425−:: Only names exported by this directly imported module are visible through
5426−:: its face. Other origins retain identity but print as unnamed unions.
5793+:: A public non-generic alias names exactly its origin and arguments.
5794+:: Reusing only an origin could print a different generic instantiation.
5795+++ prelude-union-alias
5796+ |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
5797+ ^- (unit term)
5798+ ?^ args ~
5799+ ?~ molds ~
5800+ =/ template=ischeme template.i.molds
5801+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
5802+ ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
5803+ $(molds t.molds)
5804+::
5805+:: Names exported by the directly imported module are visible through its
5806+:: face; a matching prelude alias is also visible without a qualifier.
54275807::
54285808++ itype-in-import
5429− |= [t=itype iface=ifile face=term]
5809+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
54305810 ^- itype
54315811 ?- -.t
54325812 %union
54335813 =/ label=(unit @t)
54345814 ?~ origin.t ~
5815+ ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
5816+ =/ public=(unit term)
5817+ ?~ prelude ~
5818+ (prelude-union-alias u.origin.t args.t molds.u.prelude)
5819+ ?^ public `u.public
54355820 =/ alias=(unit term) ~
54365821 =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
54375822 =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
54385823 ?~ alias ~
54395824 `(crip "{(trip u.alias)}.{(trip face)}")
5440− [%union (turn cases.t |=(c=itype (itype-in-import c iface face))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face)))]
5825+ [%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)))]
5826+ %recursive [%recursive module.t name.t ~]
5827+ %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
54415828 %face [%face name.t $(t body.t)]
54425829 %fn [%fn $(t sample.t) $(t product.t)]
54435830 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5457,6 +5844,8 @@
54575844:: Generic mold parameters are lexical and distinct from the enclosing
54585845:: value's capital variables. Arguments are substituted only once, so
54595846:: an argument's variable ID cannot be captured by a template ID.
5847+:: A generic alias of a named union keeps the underlying union's origin
5848+:: and substituted argument order; an originless union stays unsupported.
54605849::
54615850++ iparam-lookup
54625851 |= [name=@t params=iparams]
@@ -5518,8 +5907,8 @@
55185907 =/ out=(unit [typ=itype state=istate])
55195908 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
55205909 ?~ out ~
5521− ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh)) ~
5522− =? typ.u.out ?=(%union -.typ.u.out)
5910+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
5911+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
55235912 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
55245913 =/ used=(list @ud) (itype-vars typ.u.out)
55255914 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
@@ -5530,6 +5919,103 @@
55305919 ?: ?=(^ (itype-vars typ.u.out)) ~
55315920 `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
55325921::
5922+:: A direct imported reference may carry definite reader evidence. Only
5923+:: uniquely supplied, declared inputs are used; unsupported data stay generic.
5924+++ direct-import-invalid
5925+ |= [sh=shape state=istate]
5926+ ^- (unit idiag)
5927+ ?. ?=(%ref -.sh) ~
5928+ ?~ names.sh ~
5929+ =/ n=term i.names.sh
5930+ =/ raw=*
5931+ ?~ t.names.sh
5932+ ?. (unique-value-name n marks.state) ~
5933+ ?: (lien surs.state |=(x=term =(x n))) ~
5934+ ?: ?=(^ (find-jibb-interface n jimports.state)) ~
5935+ ?: (lien globals.state |=(x=term =(x n))) ~
5936+ ?: (lien reserved-molds.state |=(x=term =(x n))) ~
5937+ ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) ~
5938+ =/ found=imark-externals (skim mark-externals.state |=(e=[mark=term result=*] =(mark.e n)))
5939+ ?~ found ~
5940+ ?^ t.found ~
5941+ result.i.found
5942+ ?^ t.t.names.sh ~
5943+ =/ mod=term i.t.names.sh
5944+ ?: ?=(^ (find-jibb-interface mod jimports.state)) ~
5945+ ?. (unique-value-name mod surs.state) ~
5946+ ?: (lien marks.state |=(x=term =(x mod))) ~
5947+ ?: (lien globals.state |=(x=term =(x mod))) ~
5948+ ?: (lien reserved-molds.state |=(x=term =(x mod))) ~
5949+ ?: (lien molds.state |=(m=[name=term body=shape] =(mod name.m))) ~
5950+ =/ found=iexternals (skim externals.state |=(e=[module=term name=term result=*] &(=(module.e mod) =(name.e n))))
5951+ ?~ found ~
5952+ ?^ t.found ~
5953+ result.i.found
5954+ ?. ?=([%invalid ?(%aura %core) @] raw) ~
5955+ `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
5956+::
5957+:: Replay only the shape branches whose evaluation order we can prove.
5958+:: Successful prefixes must be checked before descending to a failure.
5959+++ nested-import-invalid
5960+ |= [sh=shape state=istate]
5961+ ^- (unit idiag)
5962+ ?: ?=(^ (infer-simple-shape sh state)) ~
5963+ ?- -.sh
5964+ %ref
5965+ =/ direct=(unit idiag) (direct-import-invalid sh state)
5966+ ?^ direct direct
5967+ ?~ names.sh ~
5968+ ?^ t.names.sh ~
5969+ =/ n=term i.names.sh
5970+ ?: (lien marks.state |=(x=term =(x n))) ~
5971+ ?: (lien active.state |=(x=term =(x n))) ~
5972+ =/ found=(unit shape) (find-simple-mold n molds.state)
5973+ ?~ found ~
5974+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
5975+ %fn
5976+ =/ first=(unit [typ=itype state=istate]) (infer-simple-shape sample.sh state)
5977+ ?~ first $(sh sample.sh)
5978+ $(sh product.sh, state state.u.first)
5979+ %cell (nested-field-invalid fields.sh state)
5980+ * ~
5981+ ==
5982+::
5983+++ nested-field-invalid
5984+ |= [fields=(list field) state=istate]
5985+ ^- (unit idiag)
5986+ ?~ fields ~
5987+ =/ sh=shape
5988+ ?- -.i.fields
5989+ %bare shape.i.fields
5990+ %face shape.i.fields
5991+ %pun [%ref at.i.fields ~[name.i.fields]]
5992+ ==
5993+ =/ out=(unit [typ=itype state=istate]) (infer-simple-shape sh state)
5994+ ?~ out (nested-import-invalid sh state)
5995+ $(fields t.fields, state state.u.out)
5996+::
5997+++ sample-import-invalid
5998+ |= [s=sample env=ienv state=istate]
5999+ ^- (unit idiag)
6000+ =/ result=isample-result (infer-sample s env state)
6001+ ?: ?=(%& -.result) ~
6002+ ?. =(p.result "sample mold is not supported by partial inference") ~
6003+ ?- s
6004+ [%face *] (nested-import-invalid shape.s state)
6005+ [%bare *] (nested-import-invalid shape.s state)
6006+ [%pun *] (nested-import-invalid [%ref at.s ~[name.s]] state)
6007+ [%cell *] (nested-samples-invalid items.s env state)
6008+ * ~
6009+ ==
6010+::
6011+++ nested-samples-invalid
6012+ |= [items=(list sample) env=ienv state=istate]
6013+ ^- (unit idiag)
6014+ ?~ items ~
6015+ =/ head=isample-result (infer-sample i.items env state)
6016+ ?: ?=(%| -.head) (sample-import-invalid i.items env state)
6017+ $(items t.items, env env.p.head, state state.p.head)
6018+::
55336019++ infer-simple-shape
55346020 |= [sh=shape state=istate]
55356021 ^- (unit [typ=itype state=istate])
@@ -5538,8 +6024,9 @@
55386024 ?: =(0 aura.sh) `[[%any-atom ~] state]
55396025 `[[%atom aura.sh] state]
55406026 %flag `[[%flag ~] state]
6027+ %noun `[[%noun ~] state]
55416028 %const
5542− ?. =(%term form.lit.sh) ~
6029+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
55436030 `[[%const lit.sh] state]
55446031 %union
55456032 =/ pairs=(list upair) (union-pairs cases.sh molds.state)
@@ -5564,7 +6051,7 @@
55646051 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
55656052 ?~ found ~
55666053 ?^ vars.u.found ~
5567− `[(itype-in-import typ.u.found u.iface i.t.names.sh) state]
6054+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
55686055 =/ found=(unit itype)
55696056 (find-imported-mold i.t.names.sh n externals.state surs.state)
55706057 ?~ found ~
@@ -5576,7 +6063,13 @@
55766063 `[u.imported state]
55776064 ?: (lien active.state |=(x=term =(x n))) ~
55786065 =/ found=(unit shape) (find-simple-mold n molds.state)
5579− ?~ found ~
6066+ ?~ found
6067+ ?: (lien molds.state |=(m=[name=term body=shape] =(name.m n))) ~
6068+ ?~ prelude.state ~
6069+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state)
6070+ ?~ prelude-entry ~
6071+ ?^ vars.u.prelude-entry ~
6072+ `[typ.u.prelude-entry state]
55806073 =/ out=(unit [typ=itype state=istate])
55816074 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
55826075 ?~ out ~
@@ -5595,10 +6088,18 @@
55956088 ?~ vars.u.template ~
55966089 =/ applied=(unit itype) (template-apply u.template types.u.args)
55976090 ?~ applied ~
5598− `[(itype-in-import u.applied u.iface i.t.ref.sh) state.u.args]
6091+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
55996092 ?: (lien active.state.u.args |=(x=term =(x n))) ~
56006093 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
5601− ?~ found ~
6094+ ?~ found
6095+ ?: (lien molds.state.u.args |=(m=[name=term body=shape] =(name.m n))) ~
6096+ ?~ prelude.state.u.args ~
6097+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state.u.args)
6098+ ?~ prelude-entry ~
6099+ ?~ vars.u.prelude-entry ~
6100+ =/ applied=(unit itype) (template-apply u.prelude-entry types.u.args)
6101+ ?~ applied ~
6102+ `[u.applied state.u.args]
56026103 ?. ?=(%generic -.u.found) ~
56036104 ?. (distinct-params vars.u.found) ~
56046105 =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
@@ -5606,9 +6107,9 @@
56066107 =/ out=(unit [typ=itype state=istate])
56076108 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
56086109 ?~ out ~
5609− ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found)) ~
5610− ?: &(?=(%union -.typ.u.out) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
5611− =? typ.u.out ?=(%union -.typ.u.out)
6110+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
6111+ ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
6112+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
56126113 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
56136114 `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
56146115 %tvar
@@ -5617,7 +6118,7 @@
56176118 ?: in-mold.state ~
56186119 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
56196120 ?^ n `[[%var u.n] state]
5620− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state] caps.state])]
6121+ `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
56216122 * ~
56226123 ==
56236124::
@@ -5693,8 +6194,8 @@
56936194 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
56946195::
56956196:: Local definitions generalize only variables outside their enclosing
5696−:: environment and explicit-capital scope. Unresolved groups stay
5697−:: unsupported: this fragment does not infer recursive definitions.
6197+:: environment and explicit-capital scope. Recursive gate groups use
6198+:: monomorphic placeholders while their bodies are checked.
56986199::
56996200+$ ilocal-result (each [env=ienv state=istate] idiag)
57006201++ free-env-vars
@@ -5763,6 +6264,145 @@
57636264 ?~ inferred |
57646265 $(locals t.locals)
57656266::
6267+:: Gather written capitals belonging to one ++. Nested local definitions
6268+:: establish their own scopes; inline gates remain in the enclosing scope.
6269++$ icap-site [name=@t at=span]
6270+++ scope-shape
6271+ |= s=shape
6272+ ^- (list icap-site)
6273+ ?- -.s
6274+ %tvar ~[[name.s at.s]]
6275+ %apply (zing (turn args.s scope-shape))
6276+ %cell (zing (turn fields.s scope-field))
6277+ %union (zing (turn cases.s scope-shape))
6278+ %fn (weld (scope-shape sample.s) (scope-shape product.s))
6279+ %generic
6280+ =/ inside=(list icap-site) (scope-shape body.s)
6281+ (skim inside |=(site=icap-site !(lien vars.s |=(v=@t =(v name.site)))))
6282+ * ~
6283+ ==
6284+::
6285+++ scope-field
6286+ |= f=field
6287+ ^- (list icap-site)
6288+ ?- -.f
6289+ %face (scope-shape shape.f)
6290+ %bare (scope-shape shape.f)
6291+ %pun ~
6292+ ==
6293+::
6294+++ scope-sample
6295+ |= s=sample
6296+ ^- (list icap-site)
6297+ ?- -.s
6298+ %face (scope-shape shape.s)
6299+ %bare (scope-shape shape.s)
6300+ %cell (zing (turn items.s scope-sample))
6301+ * ~
6302+ ==
6303+::
6304+++ scope-pieces
6305+ |= ps=(list piece)
6306+ ^- (list icap-site)
6307+ ?~ ps ~
6308+ =/ first=(list icap-site)
6309+ ?- -.i.ps
6310+ %expr (scope-expr p.i.ps)
6311+ %text ~
6312+ ==
6313+ (weld first $(ps t.ps))
6314+::
6315+++ scope-qsegs
6316+ |= ps=(list qseg)
6317+ ^- (list icap-site)
6318+ ?~ ps ~
6319+ =/ first=(list icap-site)
6320+ ?- -.i.ps
6321+ %expr (scope-expr p.i.ps)
6322+ %knot ~
6323+ ==
6324+ (weld first $(ps t.ps))
6325+::
6326+++ scope-edits
6327+ |= xs=(list edit)
6328+ ^- (list icap-site)
6329+ ?~ xs ~
6330+ =/ first=(list icap-site) (scope-expr val.i.xs)
6331+ (weld first $(xs t.xs))
6332+::
6333+++ scope-items
6334+ |= xs=(list item)
6335+ ^- (list icap-site)
6336+ ?~ xs ~
6337+ =/ first=(list icap-site) (scope-expr val.i.xs)
6338+ (weld first $(xs t.xs))
6339+::
6340+++ scope-arms
6341+ |= xs=(list arm)
6342+ ^- (list icap-site)
6343+ ?~ xs ~
6344+ =/ first=(list icap-site) (scope-expr val.i.xs)
6345+ (weld first $(xs t.xs))
6346+::
6347+++ scope-exprs
6348+ |= xs=(list expr)
6349+ ^- (list icap-site)
6350+ ?~ xs ~
6351+ =/ first=(list icap-site) (scope-expr i.xs)
6352+ (weld first $(xs t.xs))
6353+::
6354+++ scope-expr
6355+ |= e=expr
6356+ ^- (list icap-site)
6357+ ?- -.e
6358+ %str (scope-pieces pieces.e)
6359+ %qath (scope-qsegs segs.e)
6360+ %change (scope-edits edits.e)
6361+ %pair (scope-expr val.e)
6362+ %unit (scope-expr val.e)
6363+ %group (scope-expr inner.e)
6364+ %list (scope-exprs items.e)
6365+ %tuple (scope-items items.e)
6366+ %gate
6367+ =/ first=(list icap-site) (scope-sample sample.e)
6368+ =/ last=(list icap-site) (scope-expr body.e)
6369+ (weld first last)
6370+ %gate-wide
6371+ =/ first=(list icap-site) (scope-sample sample.e)
6372+ =/ last=(list icap-site) (scope-expr body.e)
6373+ (weld first last)
6374+ %call
6375+ =/ first=(list icap-site) (scope-expr head.e)
6376+ =/ last=(list icap-site) (scope-exprs args.e)
6377+ (weld first last)
6378+ %cast
6379+ =/ first=(list icap-site) (scope-shape shape.e)
6380+ =/ last=(list icap-site) (scope-expr val.e)
6381+ (weld first last)
6382+ %trace
6383+ =/ first=(list icap-site) (scope-expr val.e)
6384+ =/ last=(list icap-site) (scope-expr then.e)
6385+ (weld first last)
6386+ %branch
6387+ =/ first=(list icap-site) (scope-expr subject.e)
6388+ =/ last=(list icap-site) (scope-arms arms.e)
6389+ (weld first last)
6390+ %body (scope-expr final.e)
6391+ * ~
6392+ ==
6393+::
6394+++ reserve-cap-sites
6395+ |= [sites=(list icap-site) state=istate]
6396+ ^- istate
6397+ ?~ sites state
6398+ ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
6399+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
6400+::
6401+++ reserve-def-caps
6402+ |= [e=expr state=istate]
6403+ ^- istate
6404+ (reserve-cap-sites (scope-expr e) state)
6405+::
57666406++ infer-local-defs
57676407 |= [ds=(list def) env=ienv state=istate]
57686408 ^- ilocal-result
@@ -5771,26 +6411,62 @@
57716411 |-
57726412 ?~ ds
57736413 ?~ remaining [%& env state]
5774− ?. progressed [%| ["local definitions need unsupported inference" ~]]
6414+ ?. progressed
6415+ =/ pending=(list def) (flop remaining)
6416+ =/ groups=icomponents (graph-components pending (global-value-names pending))
6417+ =/ grouped=(unit [rest=(list def) env=ienv state=istate])
6418+ (try-local-group pending groups env state)
6419+ ?~ grouped [%| ["local definitions need unsupported inference" ~]]
6420+ $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
57756421 $(ds (flop remaining), remaining ~, progressed |)
57766422 =/ d=def i.ds
57776423 ?> ?=(%value -.d)
5778− =/ inferred=iresult (infer-fragment val.d env state)
6424+ =/ local-state=istate (reserve-def-caps val.d state)
6425+ =/ inferred=iresult (infer-fragment val.d env local-state)
6426+ =/ retried=? ?=(%| -.inferred)
6427+ =? inferred retried (infer-recursive-gate d env local-state)
57796428 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6429+ =/ merged=(unit [first=icap second=icap])
6430+ (merged-capitals caps.state.p.inferred sub.state.p.inferred)
6431+ ?^ merged
6432+ [%| ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
6433+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred)
6434+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
57806435 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
57816436 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
57826437 $(ds t.ds, remaining [d remaining])
57836438 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
57846439 $(ds t.ds, remaining [d remaining])
57856440 =/ free=(list @ud)
5786− (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state.p.inferred sub.state.p.inferred))
6441+ (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
57876442 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
57886443 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
5789− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred, progressed &)
6444+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
6445+::
6446+:: Try complete cyclic local groups after individual definitions stall.
6447+:: Components with non-gates or unresolved constraints stay unavailable.
6448+::
6449+++ try-local-group
6450+ |= [ds=(list def) groups=icomponents env=ienv state=istate]
6451+ ^- (unit [rest=(list def) env=ienv state=istate])
6452+ ?~ groups ~
6453+ =/ names=(list term) i.groups
6454+ ?. (gth (lent names) 1) $(groups t.groups)
6455+ =/ members=(list def)
6456+ (skim ds |=(d=def &(?=(%value -.d) (lien names |=(n=term =(n name.d))))))
6457+ ?. =((lent members) (lent names)) $(groups t.groups)
6458+ =/ result=ilocal-result (infer-gate-group members env state)
6459+ ?: ?=(%| -.result) $(groups t.groups)
6460+ =/ rest=(list def)
6461+ (skim ds |=(d=def !(lien names |=(n=term =(n name.d)))))
6462+ =/ more=(unit [rest=(list def) env=ienv state=istate])
6463+ $(ds rest, groups t.groups, env env.p.result, state state.p.result)
6464+ ?^ more more
6465+ `[rest env.p.result state.p.result]
57906466::
57916467:: Read only fields of a known record. Unresolved field constraints and
5792−:: ambiguous repeated faces are outside this fragment (doc question:
5793−:: whether duplicate imported Hoon faces are valid or select a field).
6468+:: ambiguous repeated faces are outside this fragment. Imported record
6469+:: spines with repeated names are unavailable when used.
57946470::
57956471++ record-fields-named
57966472 |= [name=term t=itype sub=isub]
@@ -5821,9 +6497,9 @@
58216497 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
58226498 $(fields t.fields, typ i.found)
58236499::
5824−:: Propagate a known union through a direct loobean branch. Empty bodies
5825−:: and groups are transparent; bodies with definitions keep their normal
5826−:: scoping and wait for general bidirectional inference.
6500+:: Propagate a known union or list through supported loobean, unit and list
6501+:: branches. Empty bodies and groups are transparent; bodies with definitions
6502+:: keep their normal scoping and wait for general bidirectional inference.
58276503::
58286504++ context-union-branch
58296505 |= e=expr
@@ -5840,12 +6516,16 @@
58406516 ^- iresult
58416517 ?: ?=(%group -.e) $(e inner.e)
58426518 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6519+ ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
6520+ (infer-list-context e expected env state context)
58436521 ?: ?=(%branch -.e)
58446522 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
58456523 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
58466524 ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
58476525 =/ x=arm i.arms.e
58486526 =/ y=arm i.t.arms.e
6527+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
6528+ (infer-unit-branch e env state `[expected context])
58496529 ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y))
58506530 [%| ["branch pattern is not supported by partial inference" ~]]
58516531 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
@@ -5854,6 +6534,9 @@
58546534 [%| ["branch does not cover both loobeans" ~]]
58556535 =/ subject=iresult (infer-fragment subject.e env state)
58566536 ?: ?=(%| -.subject) subject
6537+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
6538+ ?: ?=(%union -.subject-type)
6539+ [%| ["contextual union-pattern branch is not supported by partial inference" ~]]
58576540 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
58586541 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
58596542 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -5865,11 +6548,685 @@
58656548 ?: ?=(%| -.value) value
58666549 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
58676550 ?: ?=(%unknown -.fit)
6551+ ?: &(?=(%collection -.expected) =(%list name.expected))
6552+ [%| ["branch list constraint is not supported by partial inference" ~]]
58686553 [%| ["branch union constraint is not supported by partial inference" ~]]
58696554 ?: ?=(%bad -.fit)
6555+ =/ missing=(unit idiag) (missing-union-tag e expected sub.state.p.value context)
6556+ ?^ missing [%| u.missing]
6557+ =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
6558+ ?^ nested [%| u.nested]
6559+ ?: &(?=(%collection -.expected) =(%list name.expected))
6560+ [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
58706561 [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
58716562 [%& expected state.p.value(sub sub.fit, next next.fit)]
58726563::
6564+:: A list expression needs a known list target and the validated prelude list.
6565+:: Literal items and unfaced two-item cons cells receive that target one by
6566+:: one; pending constraints elsewhere stay in the threaded state.
6567+::
6568+++ context-list-expression
6569+ |= e=expr
6570+ ^- ?
6571+ ?- -.e
6572+ %list &
6573+ %tuple &
6574+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6575+ %group $(e inner.e)
6576+ %body ?~(defs.e $(e final.e) |)
6577+ * |
6578+ ==
6579+::
6580+++ infer-list-context
6581+ |= [e=expr expected=itype env=ienv state=istate context=span]
6582+ ^- iresult
6583+ ?: ?=(%group -.e) $(e inner.e)
6584+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6585+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
6586+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
6587+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6588+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
6589+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
6590+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
6591+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6592+ =/ target=itype (itype-walk expected sub.state)
6593+ ?. ?=(%collection -.target) [%| ["list context is not supported by partial inference" ~]]
6594+ ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
6595+ ?~ args.target [%| ["list context is not supported by partial inference" ~]]
6596+ ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
6597+ ?: ?=(%lit -.e)
6598+ ?. |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6599+ [%| ["list expression is not supported by partial inference" ~]]
6600+ [%& target state]
6601+ ?: ?=(%list -.e)
6602+ =/ result=iresult (infer-list-items items.e i.args.target env state context)
6603+ ?: ?=(%| -.result) result
6604+ [%& target state.p.result]
6605+ ?. ?=(%tuple -.e) [%| ["list expression is not supported by partial inference" ~]]
6606+ ?~ items.e [%| ["cons shape is not supported by partial inference" ~]]
6607+ ?~ t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6608+ ?^ t.t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6609+ ?^ face.i.items.e [%| ["faced cons is not supported by partial inference" ~]]
6610+ ?^ face.i.t.items.e [%| ["faced cons is not supported by partial inference" ~]]
6611+ =/ head=iresult (infer-list-items ~[val.i.items.e] i.args.target env state context)
6612+ ?: ?=(%| -.head) head
6613+ =/ target=itype (itype-walk target sub.state.p.head)
6614+ =/ tail=iresult
6615+ ?: (context-list-expression val.i.t.items.e)
6616+ (infer-list-context val.i.t.items.e target env state.p.head context)
6617+ (infer-fragment val.i.t.items.e env state.p.head)
6618+ ?: ?=(%| -.tail) tail
6619+ =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
6620+ ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
6621+ ?: ?=(%bad -.fit)
6622+ [%| ["list tail does not fit its expected type" ~[[context (site-type-note "expected list" target sub.state.p.tail)] [(span-of val.i.t.items.e) (site-type-note "list tail" typ.p.tail sub.state.p.tail)]]]]
6623+ [%& target state.p.tail(sub sub.fit, next next.fit)]
6624+::
6625+++ infer-open-list-items
6626+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6627+ ^- iresult
6628+ ?~ items [%& expected state]
6629+ =/ target=itype (itype-walk expected sub.state)
6630+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6631+ ?: ?=(%| -.value) value
6632+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6633+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6634+ ?: ?=(%bad -.fit)
6635+ ?: |((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))
6636+ [%| ["list item widening is not supported by partial inference" ~]]
6637+ [%| ["list items do not have compatible types" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
6638+ ?: (itype-has-tag (itype-normalize expected sub.fit))
6639+ [%| ["list item needs context in partial inference" ~]]
6640+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
6641+::
6642+++ infer-list-items
6643+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6644+ ^- iresult
6645+ ?~ items [%& expected state]
6646+ =/ target=itype (itype-walk expected sub.state)
6647+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6648+ ?: ?=(%| -.value) value
6649+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6650+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6651+ ?: ?=(%bad -.fit)
6652+ =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
6653+ ?^ missing [%| u.missing]
6654+ =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
6655+ ?^ nested [%| u.nested]
6656+ [%| ["list item does not fit its expected type" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
6657+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
6658+::
6659+:: The supported unit pattern covers exactly an atom zero and a cell
6660+:: headed by zero, with a single binder for its payload. Unresolved
6661+:: subjects and all other pattern matrices stay outside this fragment.
6662+::
6663+++ unit-empty-pattern
6664+ |= p=pattern
6665+ ^- ?
6666+ ?. ?=(%lit -.p) |
6667+ =(%null form.lit.p)
6668+::
6669+++ unit-payload-pattern
6670+ |= p=pattern
6671+ ^- (unit term)
6672+ ?. ?=(%cell -.p) ~
6673+ ?~ items.p ~
6674+ ?~ t.items.p ~
6675+ ?^ t.t.items.p ~
6676+ ?. (unit-empty-pattern i.items.p) ~
6677+ ?. ?=(%bind -.i.t.items.p) ~
6678+ `name.i.t.items.p
6679+::
6680+++ unit-empty-case
6681+ |= t=itype
6682+ ^- ?
6683+ ?. ?=(%const -.t) |
6684+ =(0 val.literal.t)
6685+::
6686+++ unit-payload-case
6687+ |= t=itype
6688+ ^- (unit itype)
6689+ ?. ?=(%cell -.t) ~
6690+ ?. (unit-empty-case hed.t) ~
6691+ =/ payload=itype tal.t
6692+ =? payload ?=(%face -.payload) body.payload
6693+ `payload
6694+::
6695+++ unit-union-payload
6696+ |= t=itype
6697+ ^- (unit itype)
6698+ ?. ?=(%union -.t) ~
6699+ ?~ cases.t ~
6700+ ?~ t.cases.t ~
6701+ ?^ t.t.cases.t ~
6702+ ?: (unit-empty-case i.cases.t) (unit-payload-case i.t.cases.t)
6703+ ?: (unit-empty-case i.t.cases.t) (unit-payload-case i.cases.t)
6704+ ~
6705+::
6706+:: List matching currently covers exactly null and a cell of two binders.
6707+:: The head has the element type and the tail has the whole list type.
6708+:: Other patterns and lists whose element mold is empty remain unsupported.
6709+::
6710+++ list-payload-pattern
6711+ |= p=pattern
6712+ ^- (unit [head=term tail=term])
6713+ ?. ?=(%cell -.p) ~
6714+ ?~ items.p ~
6715+ ?~ t.items.p ~
6716+ ?^ t.t.items.p ~
6717+ ?. ?=(%bind -.i.items.p) ~
6718+ ?. ?=(%bind -.i.t.items.p) ~
6719+ `[name.i.items.p name.i.t.items.p]
6720+::
6721+++ infer-list-branch
6722+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span]) typ=itype]
6723+ ^- iresult
6724+ ?> ?=(%branch -.e)
6725+ ?> ?=(%collection -.typ)
6726+ ?. =(%list name.typ) [%| ["list pattern is not supported by partial inference" ~]]
6727+ ?~ prelude.state [%| ["list pattern needs the standard prelude in partial inference" ~]]
6728+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
6729+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
6730+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
6731+ ?~ standard [%| ["list pattern needs the standard prelude in partial inference" ~]]
6732+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
6733+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
6734+ ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
6735+ ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
6736+ ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
6737+ ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
6738+ ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
6739+ =/ x=arm i.arms.e
6740+ =/ y=arm i.t.arms.e
6741+ =/ first-empty=? (unit-empty-pattern pat.x)
6742+ =/ first-name=(unit [head=term tail=term]) (list-payload-pattern pat.x)
6743+ =/ second-name=(unit [head=term tail=term]) (list-payload-pattern pat.y)
6744+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
6745+ [%| ["list branch pattern is not supported by partial inference" ~]]
6746+ =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
6747+ ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6748+ ?: |(=(head.u.binder tail.u.binder) ?=(^ (ienv-lookup head.u.binder env)) ?=(^ (ienv-lookup tail.u.binder env)) (lien globals.state |=(n=term |(=(n head.u.binder) =(n tail.u.binder)))))
6749+ [%| ["pattern binder shadows a name" ~]]
6750+ =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
6751+ =/ left=iresult
6752+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state)
6753+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state context.u.expected)
6754+ ?: ?=(%| -.left) left
6755+ =/ right=iresult
6756+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6757+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
6758+ ?: ?=(%| -.right) right
6759+ ?^ expected [%& typ.u.expected state.p.right]
6760+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
6761+ ?~ joined [%| ["list branch results need unsupported inference" ~]]
6762+ [%& typ.p.left state.p.right(sub u.joined)]
6763+::
6764+++ infer-unit-branch
6765+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
6766+ ^- iresult
6767+ ?> ?=(%branch -.e)
6768+ ?~ arms.e [%| ["unit branch is not supported by partial inference" ~]]
6769+ ?~ t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
6770+ ?^ t.t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
6771+ =/ subject=iresult (infer-fragment subject.e env state)
6772+ ?: ?=(%| -.subject) subject
6773+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6774+ ?: &(?=(%collection -.typ) =(%list name.typ))
6775+ (infer-list-branch e env state.p.subject expected typ)
6776+ =/ x=arm i.arms.e
6777+ =/ y=arm i.t.arms.e
6778+ =/ first-empty=? (unit-empty-pattern pat.x)
6779+ =/ first-name=(unit term) (unit-payload-pattern pat.x)
6780+ =/ second-name=(unit term) (unit-payload-pattern pat.y)
6781+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
6782+ [%| ["unit branch pattern is not supported by partial inference" ~]]
6783+ =/ binder=(unit term) ?:(first-empty second-name first-name)
6784+ ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
6785+ ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
6786+ [%| ["pattern binder shadows a name" ~]]
6787+ =/ payload=(unit itype) (unit-union-payload typ)
6788+ ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
6789+ =/ extended=ienv [[u.binder [u.payload ~]] env]
6790+ =/ left=iresult
6791+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
6792+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state.p.subject context.u.expected)
6793+ ?: ?=(%| -.left) left
6794+ =/ right=iresult
6795+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6796+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
6797+ ?: ?=(%| -.right) right
6798+ ?^ expected [%& typ.u.expected state.p.right]
6799+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
6800+ ?~ joined [%| ["unit branch results need unsupported inference" ~]]
6801+ [%& typ.p.left state.p.right(sub u.joined)]
6802+::
6803+:: Infer pieces in order, retaining their substitutions and pending tags.
6804+:: A bare decimal literal has no outside type constraint, so it takes its
6805+:: normal @ud default here. Other open numeric and aura variables wait for
6806+:: deferred constraints, which this fragment does not implement yet.
6807+++ infer-string-pieces
6808+ |= [ps=(list piece) env=ienv state=istate]
6809+ ^- iresult
6810+ ?~ ps [%& [%atom %t] state]
6811+ ?: ?=(%text -.i.ps) $(ps t.ps)
6812+ =/ item=iresult (infer-fragment p.i.ps env state)
6813+ ?: ?=(%| -.item) item
6814+ =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
6815+ ?: |(?=(%atom -.t) ?=(%any-atom -.t))
6816+ $(ps t.ps, state state.p.item)
6817+ ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
6818+ $(ps t.ps, state state.p.item)
6819+ ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
6820+ $(ps t.ps, state state.p.item)
6821+ ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
6822+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
6823+ ?: ?=(%cell -.t)
6824+ [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
6825+ [%| ["interpolation type needs unsupported inference" ~]]
6826+::
6827+:: Whole-case coverage for a known union. When a pattern may cover only
6828+:: part of a case, finite loobean refinements are tried below; other
6829+:: partial coverage stays unsupported until the general pattern matrix.
6830++$ imatch ?(%full %none %unknown)
6831+++ union-pattern-items
6832+ |= [ps=(list pattern) t=itype]
6833+ ^- imatch
6834+ ?~ ps %unknown
6835+ ?~ t.ps (union-pattern i.ps t)
6836+ =. t ?:(?=(%face -.t) body.t t)
6837+ ?. ?=(%cell -.t)
6838+ ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
6839+ %unknown
6840+ =/ a=imatch (union-pattern i.ps hed.t)
6841+ =/ b=imatch $(ps t.ps, t tal.t)
6842+ ?: |(=(%none a) =(%none b)) %none
6843+ ?:(&(=(%full a) =(%full b)) %full %unknown)
6844+::
6845+++ union-pattern
6846+ |= [p=pattern t=itype]
6847+ ^- imatch
6848+ =. t ?:(?=(%face -.t) body.t t)
6849+ ?- -.p
6850+ %any %full
6851+ %bind %full
6852+ %lit
6853+ ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
6854+ ?: ?=(%cell -.t) %none
6855+ ?: ?=(%flag -.t)
6856+ ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
6857+ %unknown
6858+ %str ?:(?=(%cell -.t) %none %unknown)
6859+ %cell (union-pattern-items items.p t)
6860+ ==
6861+::
6862+++ union-pattern-has-bind
6863+ |= p=pattern
6864+ ^- ?
6865+ ?: ?=(%bind -.p) &
6866+ ?. ?=(%cell -.p) |
6867+ (lien items.p union-pattern-has-bind)
6868+::
6869+++ union-pattern-bind-items
6870+ |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
6871+ ^- (unit ienv)
6872+ ?~ ps ~
6873+ ?~ t.ps (union-pattern-bind i.ps t env globals)
6874+ =. t ?:(?=(%face -.t) body.t t)
6875+ ?. ?=(%cell -.t) ~
6876+ =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
6877+ ?~ first ~
6878+ $(ps t.ps, t tal.t, env u.first)
6879+::
6880+++ union-pattern-bind
6881+ |= [p=pattern t=itype env=ienv globals=(list term)]
6882+ ^- (unit ienv)
6883+ =. t ?:(?=(%face -.t) body.t t)
6884+ ?: ?=(%bind -.p)
6885+ ?: |(?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
6886+ `[[name.p [t ~]] env]
6887+ ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
6888+ `env
6889+::
6890+:: Split loobean fields into finite refinements for partial patterns.
6891+:: Keep original cases for binder types and preserve whole-case matching
6892+:: before trying refinements. Cap products at 64; unknown, empty or opaque
6893+:: shapes stay unsupported rather than implying complete pattern checking.
6894++$ ifinite [origin=@ud base=itype part=itype]
6895+++ finite-product
6896+ |= [hs=(list itype) ts=(list itype) out=(list itype)]
6897+ ^- (list itype)
6898+ ?~ hs out
6899+ =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
6900+ $(hs t.hs, out (weld rows out))
6901+::
6902+++ finite-type
6903+ |= t=itype
6904+ ^- (unit (list itype))
6905+ ?- -.t
6906+ %flag
6907+ `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
6908+ %face
6909+ =/ body=(unit (list itype)) $(t body.t)
6910+ ?~ body ~
6911+ `(turn u.body |=(x=itype [%face name.t x]))
6912+ %cell
6913+ =/ hed=(unit (list itype)) $(t hed.t)
6914+ ?~ hed ~
6915+ =/ tal=(unit (list itype)) $(t tal.t)
6916+ ?~ tal ~
6917+ ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
6918+ `(finite-product u.hed u.tal ~)
6919+ * `~[t]
6920+ ==
6921+::
6922+++ finite-cases
6923+ |= [xs=(list itype) out=(list ifinite) origin=@ud]
6924+ ^- (unit (list ifinite))
6925+ ?~ xs `out
6926+ =/ parts=(unit (list itype)) (finite-type i.xs)
6927+ ?~ parts ~
6928+ ?: (gth (add (lent out) (lent u.parts)) 64) ~
6929+ =/ rows=(list ifinite) (turn u.parts |=(t=itype [origin i.xs t]))
6930+ $(xs t.xs, out (weld out rows), origin +(origin))
6931+::
6932+++ infer-known-union-whole
6933+ |= [e=expr env=ienv state=istate]
6934+ ^- (unit iresult)
6935+ ?> ?=(%branch -.e)
6936+ =/ subject=iresult (infer-fragment subject.e env state)
6937+ ?: ?=(%| -.subject) `subject
6938+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6939+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
6940+ =/ cases=(list itype) cases.typ
6941+ =/ remaining=(list itype) cases
6942+ =/ arms=(list arm) arms.e
6943+ =/ st=istate state.p.subject
6944+ =/ answer=(unit itype) ~
6945+ |-
6946+ ?~ arms
6947+ ?^ remaining
6948+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
6949+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
6950+ `[%& u.answer st]
6951+ =/ a=arm i.arms
6952+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
6953+ ~
6954+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
6955+ ?~ matching
6956+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
6957+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6958+ `[%| ["union pattern is not supported by partial inference" ~]]
6959+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
6960+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6961+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
6962+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
6963+ =/ body=iresult (infer-fragment val.a u.bound st)
6964+ ?: ?=(%| -.body) `body
6965+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
6966+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
6967+ ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
6968+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
6969+::
6970+++ infer-known-union-context-whole
6971+ |= [e=expr expected=itype env=ienv state=istate context=span]
6972+ ^- (unit iresult)
6973+ ?> ?=(%branch -.e)
6974+ =/ subject=iresult (infer-fragment subject.e env state)
6975+ ?: ?=(%| -.subject) `subject
6976+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6977+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
6978+ =/ cases=(list itype) cases.typ
6979+ =/ remaining=(list itype) cases
6980+ =/ arms=(list arm) arms.e
6981+ =/ st=istate state.p.subject
6982+ =/ answer=(unit itype) ~
6983+ |-
6984+ ?~ arms
6985+ ?^ remaining
6986+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
6987+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
6988+ `[%& expected st]
6989+ =/ a=arm i.arms
6990+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
6991+ ~
6992+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
6993+ ?~ matching
6994+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
6995+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6996+ `[%| ["union pattern is not supported by partial inference" ~]]
6997+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
6998+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6999+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7000+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
7001+ =/ body=iresult (infer-call-context-arg val.a expected u.bound st context)
7002+ ?: ?=(%| -.body) `body
7003+ =/ fit=ifit (itype-fit typ.p.body expected sub.state.p.body next.state.p.body)
7004+ ?: ?=(%unknown -.fit) `[%| ["union branch result constraint is not supported by partial inference" ~]]
7005+ ?: ?=(%bad -.fit)
7006+ =/ missing=(unit idiag) (missing-union-tag val.a expected sub.state.p.body context)
7007+ ?^ missing `[%| u.missing]
7008+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body expected sub.state.p.body next.state.p.body context)
7009+ ?^ nested `[%| u.nested]
7010+ `[%| ["union branch arm does not fit its expected type" ~[[context "expected type"] [(span-of val.a) "branch arm"]]]]
7011+ ?: (itype-has-tag (itype-normalize expected sub.fit))
7012+ `[%| ["union branch result needs context in partial inference" ~]]
7013+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body(sub sub.fit, next next.fit), answer `expected)
7014+::
7015+++ infer-known-union-finite
7016+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7017+ ^- iresult
7018+ ?> ?=(%branch -.e)
7019+ =/ subject=iresult (infer-fragment subject.e env state)
7020+ ?: ?=(%| -.subject) subject
7021+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7022+ ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7023+ =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7024+ ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7025+ =/ cases=(list ifinite) u.expanded
7026+ =/ remaining=(list ifinite) cases
7027+ =/ arms=(list arm) arms.e
7028+ =/ st=istate state.p.subject
7029+ =/ answer=(unit itype) ~
7030+ |-
7031+ ?~ arms
7032+ ?^ remaining
7033+ [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
7034+ ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
7035+ ?~ expected [%& u.answer st]
7036+ [%& typ.u.expected st]
7037+ =/ a=arm i.arms
7038+ ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
7039+ [%| ["partial union pattern is not supported by partial inference" ~]]
7040+ =/ matching=(list ifinite) (skim remaining |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7041+ ?~ matching
7042+ ?: (lien cases |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7043+ [%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7044+ [%| ["union pattern is not supported by partial inference" ~]]
7045+ ?: &((union-pattern-has-bind pat.a) (lien t.matching |=(c=ifinite !=(origin.c origin.i.matching))))
7046+ [%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7047+ =/ bound=(unit ienv) (union-pattern-bind pat.a base.i.matching env globals.st)
7048+ ?~ bound [%| ["pattern binder shadows a name" ~]]
7049+ =/ body=iresult
7050+ ?~ expected (infer-fragment val.a u.bound st)
7051+ (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7052+ ?: ?=(%| -.body) body
7053+ ?^ expected
7054+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7055+ ?: ?=(%unknown -.fit) [%| ["union branch result constraint is not supported by partial inference" ~]]
7056+ ?: ?=(%bad -.fit)
7057+ =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7058+ ?^ missing [%| u.missing]
7059+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body typ.u.expected sub.state.p.body next.state.p.body context.u.expected)
7060+ ?^ nested [%| u.nested]
7061+ [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7062+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7063+ [%| ["union branch result needs context in partial inference" ~]]
7064+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body(sub sub.fit, next next.fit), answer `typ.u.expected)
7065+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7066+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7067+ ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
7068+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
7069+::
7070+++ infer-known-union-branch
7071+ |= [e=expr env=ienv state=istate]
7072+ ^- iresult
7073+ =/ whole=(unit iresult) (infer-known-union-whole e env state)
7074+ ?~ whole (infer-known-union-finite e env state ~)
7075+ u.whole
7076+::
7077+++ infer-known-union-context
7078+ |= [e=expr expected=itype env=ienv state=istate context=span]
7079+ ^- iresult
7080+ =/ whole=(unit iresult) (infer-known-union-context-whole e expected env state context)
7081+ ?~ whole (infer-known-union-finite e env state `[expected context])
7082+ u.whole
7083+::
7084+++ known-union-subject
7085+ |= [e=expr env=ienv state=istate]
7086+ ^- (unit itype)
7087+ ?. ?=(%wing -.e) ~
7088+ =/ subject=iresult (infer-fragment e env state)
7089+ ?: ?=(%| -.subject) ~
7090+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7091+ ?. ?=(%union -.typ) ~
7092+ `typ
7093+::
7094+:: Infer changes only against a fully known record spine. Retain the
7095+:: target type; unknown spines and repeated edits remain unsupported.
7096+++ change-spine-known
7097+ |= [t=itype sub=isub]
7098+ ^- ?
7099+ =. t (itype-walk t sub)
7100+ ?: ?=(%face -.t) &
7101+ ?. ?=(%cell -.t) |
7102+ =/ first=itype (itype-walk hed.t sub)
7103+ ?. ?=(%face -.first) |
7104+ $(t tal.t)
7105+::
7106+++ infer-change-edits
7107+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
7108+ ^- iresult
7109+ ?~ edits [%& target state]
7110+ =/ entry=edit i.edits
7111+ ?: (lien seen |=(name=term =(name name.entry)))
7112+ [%| ["repeated change fields are not supported by partial inference" ~]]
7113+ ?. (change-spine-known target sub.state)
7114+ [%| ["change target needs a known record in partial inference" ~]]
7115+ =/ found=(list itype) (record-fields-named name.entry target sub.state)
7116+ ?~ found
7117+ [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
7118+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
7119+ =/ expected=itype i.found
7120+ =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
7121+ ?: ?=(%| -.value) value
7122+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
7123+ ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
7124+ ?: ?=(%bad -.fit)
7125+ [%| ["change field and replacement do not unify" ~[[at.entry (site-type-note "expected replacement" expected sub.state.p.value)] [(span-of val.entry) (site-type-note "replacement" typ.p.value sub.state.p.value)]]]]
7126+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
7127+::
7128+:: Backtick constructs the canonical prelude unit, after checking its
7129+:: prepared template has the standard null and [~ u=A] cases.
7130+++ standard-unit-template
7131+ |= [template=ischeme at=path]
7132+ ^- ?
7133+ ?. =(at /lib/jibb/prelude/jibb) |
7134+ ?~ vars.template |
7135+ ?^ t.vars.template |
7136+ =/ v=@ud i.vars.template
7137+ =/ nil=itype [%const [%null %n 0 '~']]
7138+ =/ expected=itype
7139+ [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
7140+ =(typ.template expected)
7141+::
7142+:: A named missing-case diagnostic needs more than a failed fit: a case
7143+:: with that tag but the wrong payload is not a missing case. Unknown
7144+:: shapes and atom types that accept terms keep the proof conservative.
7145++$ itag-presence ?(%yes %no %maybe)
7146+++ tag-presence-cases
7147+ |= [cases=(list itype) value=@ sub=isub]
7148+ ^- itag-presence
7149+ ?~ cases %no
7150+ =/ first=itag-presence (tag-presence i.cases value sub)
7151+ ?: =(%yes first) %yes
7152+ =/ rest=itag-presence $(cases t.cases)
7153+ ?: =(%yes rest) %yes
7154+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7155+ %no
7156+::
7157+++ tag-presence
7158+ |= [t=itype value=@ sub=isub]
7159+ ^- itag-presence
7160+ =. t (itype-walk t sub)
7161+ ?- -.t
7162+ %const ?:(=(value val.literal.t) %yes %no)
7163+ %flag ?:(|(=(value 0) =(value 1)) %yes %no)
7164+ %atom ?:(|(=(%tas aura.t) =(%ta aura.t)) %maybe %no)
7165+ %face $(t body.t)
7166+ %cell
7167+ =/ first=itag-presence $(t hed.t)
7168+ ?: =(%yes first) %yes
7169+ =/ rest=itag-presence $(t tal.t)
7170+ ?: =(%yes rest) %yes
7171+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7172+ %no
7173+ %union (tag-presence-cases cases.t value sub)
7174+ * %maybe
7175+ ==
7176+::
7177+++ missing-union-tag
7178+ |= [e=expr expected=itype sub=isub context=span]
7179+ ^- (unit idiag)
7180+ ?. ?=(%lit -.e) ~
7181+ ?. =(%term form.lit.e) ~
7182+ =. expected (itype-walk expected sub)
7183+ |-
7184+ ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
7185+ ?. ?=(%union -.expected) ~
7186+ ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
7187+ =/ label=tape
7188+ ?~ label.expected "union {(show-itype expected sub)}"
7189+ (show-itype expected sub)
7190+ `["{label} has no case `{(trip txt.lit.e)}`" ~[[context "expected union"] [(span-of e) "tag"]]]
7191+::
7192+:: Locate a missing tag inside a syntactic tuple only by replaying the
7193+:: directional fit in source order. Uncertain or earlier failures stop
7194+:: the walk, preserving the generic diagnostic rather than guessing.
7195+++ nested-missing-tag
7196+ |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7197+ ^- (unit idiag)
7198+ =/ original=[left=itype right=itype] [actual expected]
7199+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7200+ =/ fit=ifit (itype-fit actual expected sub next)
7201+ ?. ?=(%bad -.fit) ~
7202+ =. actual (itype-walk actual sub)
7203+ =. expected (itype-walk expected sub)
7204+ ?: &(?=(%face -.actual) ?=(%face -.expected))
7205+ ?. =(name.actual name.expected) ~
7206+ $(actual body.actual, expected body.expected)
7207+ ?: ?=(%face -.actual) $(actual body.actual)
7208+ ?: ?=(%face -.expected) $(expected body.expected)
7209+ =/ direct=(unit idiag) (missing-union-tag e expected sub context)
7210+ ?^ direct direct
7211+ ?. ?=(%tuple -.e) ~
7212+ (nested-missing-items items.e actual expected sub next context)
7213+::
7214+++ nested-missing-items
7215+ |= [items=(list item) actual=itype expected=itype sub=isub next=@ud context=span]
7216+ ^- (unit idiag)
7217+ ?~ items ~
7218+ ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
7219+ =/ original=[left=itype right=itype] [actual expected]
7220+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7221+ =. actual (itype-walk actual sub)
7222+ =. expected (itype-walk expected sub)
7223+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7224+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7225+ ?: ?=(%bad -.first)
7226+ (nested-missing-tag val.i.items hed.actual hed.expected sub next context)
7227+ ?. ?=(%ok -.first) ~
7228+ $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7229+::
58737230++ infer-fragment
58747231 |= [e=expr env=ienv state=istate]
58757232 ^- iresult
@@ -5884,13 +7241,33 @@
58847241 %duration [%& [%atom %dr] state]
58857242 %knot [%& [%atom %ta] state]
58867243 %loobean [%& [%flag ~] state]
5887− %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [next.state tags.state])]
5888− * [%| ["literal needs contextual inference" ~]]
7244+ %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
7245+ %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
58897246 ==
5890− %str
5891− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
5892− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
5893− [%& [%atom %t] state]
7247+ %unit
7248+ ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
7249+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7250+ ?~ standard [%| ["unit construction needs the standard prelude in partial inference" ~]]
7251+ ?. (standard-unit-template u.standard at.u.prelude.state)
7252+ [%| ["unit construction needs the standard prelude in partial inference" ~]]
7253+ =/ value=iresult $(e val.e)
7254+ ?: ?=(%| -.value) value
7255+ =/ result=(unit itype) (template-apply u.standard ~[typ.p.value])
7256+ ?~ result [%| ["unit construction is not supported by partial inference" ~]]
7257+ [%& u.result state.p.value]
7258+ %list
7259+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
7260+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7261+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7262+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
7263+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
7264+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
7265+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7266+ =/ element=itype [%var next.state]
7267+ =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
7268+ ?: ?=(%| -.result) result
7269+ [%& [%collection %list ~[element]] state.p.result]
7270+ %str (infer-string-pieces pieces.e env state)
58947271 %wing
58957272 ?~ names.e [%| ["empty wing" ~]]
58967273 ?^ t.names.e
@@ -5899,15 +7276,25 @@
58997276 ?~ iface (infer-field-wing names.e env state)
59007277 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
59017278 ?~ member [%| ["module member is not available to partial inference" ~]]
5902− =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e)
7279+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
59037280 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
59047281 [%& typ.instance state.instance]
59057282 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
5906− ?~ scheme [%| ["name is not available to partial inference" ~]]
7283+ ?~ scheme
7284+ ?~ prelude.state [%| ["name is not available to partial inference" ~]]
7285+ =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
7286+ ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
7287+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.prelude-entry state)
7288+ [%& typ.inst state.inst]
59077289 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
59087290 [%& typ.instance state.instance]
59097291 %group $(e inner.e)
5910− %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [next.state tags.state])]
7292+ %change
7293+ ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
7294+ =/ target=iresult $(e [%wing at.e target.e])
7295+ ?: ?=(%| -.target) target
7296+ (infer-change-edits edits.e typ.p.target env state.p.target ~)
7297+ %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
59117298 %trace
59127299 =/ traced=iresult $(e val.e)
59137300 ?: ?=(%| -.traced) traced
@@ -5934,17 +7321,26 @@
59347321 %branch
59357322 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
59367323 ?~ t.arms.e (infer-cell-branch e env state)
5937− ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
7324+ ?^ t.t.arms.e (infer-known-union-branch e env state)
7325+ =/ known=(unit itype) (known-union-subject subject.e env state)
7326+ ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
7327+ (infer-known-union-branch e env state)
59387328 =/ x=arm i.arms.e
59397329 =/ y=arm i.t.arms.e
5940− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
5941− ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
7330+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
7331+ (infer-unit-branch e env state ~)
7332+ ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7333+ ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
59427334 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
5943− [%| ["branch pattern is not supported by partial inference" ~]]
7335+ (infer-known-union-branch e env state)
7336+ ?^ known (infer-known-union-branch e env state)
59447337 ?: =(val.lit.pat.x val.lit.pat.y)
59457338 [%| ["branch does not cover both loobeans" ~]]
59467339 =/ subject=iresult $(e subject.e)
59477340 ?: ?=(%| -.subject) subject
7341+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
7342+ ?: ?=(%union -.subject-type)
7343+ [%| ["union-pattern branch subject is not supported by partial inference" ~]]
59487344 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
59497345 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
59507346 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -5957,6 +7353,8 @@
59577353 [%| ["branch widening is not supported by partial inference" ~]]
59587354 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
59597355 ?~ joined
7356+ ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
7357+ [%| ["recursive branch matching is not supported by partial inference" ~]]
59607358 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
59617359 [%| ["branch tag or union context is not supported by partial inference" ~]]
59627360 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
@@ -5969,40 +7367,54 @@
59697367 [%& typ.p.left state.p.right(sub u.joined)]
59707368 %cast
59717369 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
5972− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
7370+ ?~ target
7371+ =/ diag=(unit idiag) (nested-import-invalid shape.e state)
7372+ ?^ diag [%| u.diag]
7373+ [%| ["cast mold is not supported by partial inference" ~]]
59737374 =/ value=iresult
5974− ?: &(?=(%union -.typ.u.target) (context-union-branch val.e))
5975− (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
5976− $(e val.e, state state.u.target)
7375+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
59777376 ?: ?=(%| -.value) value
59787377 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
59797378 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
59807379 ?: ?=(%bad -.fit)
7380+ =/ missing=(unit idiag) (missing-union-tag val.e typ.u.target sub.state.p.value at.shape.e)
7381+ ?^ missing [%| u.missing]
7382+ =/ 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)
7383+ ?^ nested [%| u.nested]
59817384 [%| ["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)]]]]
59827385 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
59837386 [%& merged state.p.value(sub sub.fit, next next.fit)]
59847387 %crash [%& [%var next.state] state(next +(next.state))]
59857388 %gate
59867389 =/ sam=isample-result (infer-sample sample.e env state)
5987− ?: ?=(%| -.sam) [%| [p.sam ~]]
7390+ ?: ?=(%| -.sam)
7391+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7392+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7393+ [%| [p.sam ~]]
59887394 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
59897395 ?: ?=(%| -.body) body
59907396 [%& [%fn typ.p.sam typ.p.body] state.p.body]
59917397 %gate-wide
59927398 =/ sam=isample-result (infer-sample sample.e env state)
5993− ?: ?=(%| -.sam) [%| [p.sam ~]]
7399+ ?: ?=(%| -.sam)
7400+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7401+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7402+ [%| [p.sam ~]]
59947403 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
59957404 ?: ?=(%| -.body) body
59967405 [%& [%fn typ.p.sam typ.p.body] state.p.body]
59977406 %call
59987407 ?~ args.e [%| ["call has no argument" ~]]
5999− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
60007408 =/ head=iresult $(e head.e)
60017409 ?: ?=(%| -.head) head
60027410 =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
60037411 =/ arg=iresult
6004− ?: &(?=(%fn -.head-type) ?=(%union -.sample.head-type) (context-union-branch i.args.e))
6005− (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
7412+ ?^ t.args.e
7413+ ?: ?=(%fn -.head-type)
7414+ (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
7415+ (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
7416+ ?: ?=(%fn -.head-type)
7417+ (infer-call-context-arg i.args.e sample.head-type env state.p.head (span-of head.e))
60067418 $(e i.args.e, state state.p.head)
60077419 ?: ?=(%| -.arg) arg
60087420 =/ st=istate state.p.arg
@@ -6011,7 +7423,19 @@
60117423 =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
60127424 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
60137425 ?: ?=(%bad -.fit)
6014− [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7426+ ?~ t.args.e
7427+ =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
7428+ ?^ missing [%| u.missing]
7429+ =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
7430+ ?^ nested [%| u.nested]
7431+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7432+ =/ bad=(unit [at=span typ=itype])
7433+ (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
7434+ =/ whole-args=span
7435+ [beg:(span-of i.args.e) end:(span-of (rear args.e))]
7436+ =/ arg-at=span ?~(bad whole-args at.u.bad)
7437+ =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7438+ [%| ["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)]]]]
60157439 ?: &((itype-has-face typ.p.arg sub.fit) (itype-face-asym typ.p.arg sample.ht sub.fit) (itype-output-may-be-cell product.ht sub.fit))
60167440 [%| ["call result face propagation is not supported by partial inference" ~]]
60177441 [%& product.ht st(sub sub.fit, next next.fit)]
@@ -6023,6 +7447,142 @@
60237447 * [%| ["expression is not supported by partial inference" ~]]
60247448 ==
60257449::
7450+:: Locate a definite failing argument after the complete sample fit has
7451+:: failed. If an intermediate fit is uncertain, retain the whole argument
7452+:: span rather than assigning blame to a particular argument.
7453+::
7454+++ call-error-site
7455+ |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
7456+ ^- (unit [at=span typ=itype])
7457+ ?~ args ~
7458+ =/ original=[left=itype right=itype] [actual expected]
7459+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7460+ =. actual (itype-walk actual sub)
7461+ =. expected (itype-walk expected sub)
7462+ ?: &(?=(%face -.expected) !?=(%face -.actual))
7463+ $(expected body.expected)
7464+ ?~ t.args
7465+ =/ fit=ifit (itype-fit actual expected sub next)
7466+ ?. ?=(%bad -.fit) ~
7467+ `[(span-of i.args) (itype-normalize actual sub)]
7468+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7469+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7470+ ?: ?=(%bad -.first) `[(span-of i.args) (itype-normalize hed.actual sub)]
7471+ ?: ?=(%unknown -.first) ~
7472+ $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7473+::
7474+:: Context can help a call argument or cast value while the final fit
7475+:: checks the complete right-nested type, including any written faces.
7476+::
7477+:: Context can resolve the payload of a canonical prelude unit, but an
7478+:: unrelated union with a similar noun shape is not the same mold.
7479+++ infer-unit-context
7480+ |= [e=expr expected=itype env=ienv state=istate context=span]
7481+ ^- iresult
7482+ ?> ?=(%unit -.e)
7483+ ?> ?=(%union -.expected)
7484+ ?~ prelude.state (infer-fragment e env state)
7485+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7486+ ?~ standard (infer-fragment e env state)
7487+ ?. (standard-unit-template u.standard at.u.prelude.state) (infer-fragment e env state)
7488+ ?. =(origin.expected `[at.u.prelude.state %unit]) (infer-fragment e env state)
7489+ ?~ args.expected (infer-fragment e env state)
7490+ ?^ t.args.expected (infer-fragment e env state)
7491+ =/ payload=itype i.args.expected
7492+ =/ canonical=(unit itype) (template-apply u.standard ~[payload])
7493+ ?~ canonical (infer-fragment e env state)
7494+ ?> ?=(%union -.u.canonical)
7495+ ?. =((itype-normalize expected(label ~) sub.state) (itype-normalize u.canonical(label ~) sub.state))
7496+ (infer-fragment e env state)
7497+ =/ value=iresult (infer-call-context-arg val.e payload env state context)
7498+ ?: ?=(%| -.value) value
7499+ =/ fit=ifit (itype-fit typ.p.value payload sub.state.p.value next.state.p.value)
7500+ ?: ?=(%unknown -.fit) [%| ["unit payload constraint is not supported by partial inference" ~]]
7501+ ?: ?=(%bad -.fit)
7502+ =/ missing=(unit idiag) (missing-union-tag val.e payload sub.state.p.value context)
7503+ ?^ missing [%| u.missing]
7504+ =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
7505+ ?^ nested [%| u.nested]
7506+ [%| ["unit payload does not fit its expected type" ~[[context (site-type-note "expected unit payload" payload sub.state.p.value)] [(span-of val.e) (site-type-note "payload" typ.p.value sub.state.p.value)]]]]
7507+ [%& expected state.p.value(sub sub.fit, next next.fit)]
7508+::
7509+++ infer-call-context-arg
7510+ |= [e=expr expected=itype env=ienv state=istate context=span]
7511+ ^- iresult
7512+ ?: ?=(%group -.e) $(e inner.e)
7513+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7514+ ?: ?=(%trace -.e)
7515+ =/ traced=iresult (infer-fragment val.e env state)
7516+ ?: ?=(%| -.traced) traced
7517+ $(e then.e, state state.p.traced)
7518+ =/ target=itype (itype-walk expected sub.state)
7519+ |-
7520+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7521+ :: In a loobean-singleton context retain the written loobean noun;
7522+ :: the usual final fit decides whether that value is permitted.
7523+ =/ singleton=(unit itype)
7524+ ?. ?=(%lit -.e) ~
7525+ ?. =(%loobean form.lit.e) ~
7526+ ?. ?=(%const -.target) ~
7527+ ?. =(%loobean form.literal.target) ~
7528+ `[%const lit.e]
7529+ ?^ singleton [%& u.singleton state]
7530+ =/ known=(unit itype)
7531+ ?: ?=(%branch -.e) (known-union-subject subject.e env state)
7532+ ~
7533+ ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
7534+ (infer-known-union-context e target env state context)
7535+ ?: &(?=(%union -.target) ?=(%unit -.e))
7536+ (infer-unit-context e target env state context)
7537+ ?: &(?=(%union -.target) (context-union-branch e))
7538+ (infer-union-context e target env state context)
7539+ ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
7540+ (infer-union-context e target env state context)
7541+ ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
7542+ (infer-list-context e target env state context)
7543+ ?: &(?=(%cell -.target) ?=(%tuple -.e))
7544+ (infer-call-context-items items.e target env state context)
7545+ (infer-fragment e env state)
7546+::
7547+:: Preserve each written face; the final complete sample fit checks faces.
7548+++ infer-call-context-items
7549+ |= [items=(list item) expected=itype env=ienv state=istate context=span]
7550+ ^- iresult
7551+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
7552+ ?~ t.items
7553+ =/ last=iresult (infer-call-context-arg val.i.items expected env state context)
7554+ ?: ?=(%| -.last) last
7555+ =/ typ=itype typ.p.last
7556+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7557+ [%& typ state.p.last]
7558+ =/ target=itype (itype-walk expected sub.state)
7559+ |-
7560+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7561+ ?. ?=(%cell -.target) (infer-simple-items items env state)
7562+ =/ head=iresult (infer-call-context-arg val.i.items hed.target env state context)
7563+ ?: ?=(%| -.head) head
7564+ =/ typ=itype typ.p.head
7565+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7566+ =/ tail=iresult (infer-call-context-items t.items tal.target env state.p.head context)
7567+ ?: ?=(%| -.tail) tail
7568+ [%& [%cell typ typ.p.tail] state.p.tail]
7569+::
7570+++ infer-call-context-args
7571+ |= [args=(list expr) expected=itype env=ienv state=istate context=span]
7572+ ^- iresult
7573+ ?~ args [%| ["call has no argument" ~]]
7574+ ?~ t.args (infer-call-context-arg i.args expected env state context)
7575+ =/ target=itype (itype-walk expected sub.state)
7576+ |-
7577+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7578+ ?. ?=(%cell -.target)
7579+ (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
7580+ =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
7581+ ?: ?=(%| -.head) head
7582+ =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
7583+ ?: ?=(%| -.tail) tail
7584+ [%& [%cell typ.p.head typ.p.tail] state.p.tail]
7585+::
60267586:: Tuple and record expressions preserve their explicitly written faces.
60277587::
60287588++ infer-simple-items
@@ -6038,8 +7598,43 @@
60387598 ?: ?=(%| -.tail) tail
60397599 [%& [%cell ht typ.p.tail] state.p.tail]
60407600::
6041−:: A single two-binder cell pattern covers every value of a cell type.
6042−:: No other pattern matrix is implemented here.
7601+:: A single all-binder cell pattern covers a known cell spine; the final
7602+:: binder captures the remaining noun. Other pattern matrices stay partial.
7603+::
7604+:: Validate binders before reading the subject, preserving shadow-error
7605+:: precedence. The last binder receives the entire remaining tail.
7606+++ cell-pattern-names
7607+ |= [pats=(list pattern) env=ienv globals=(list term) seen=(list term)]
7608+ ^- (each (list term) @t)
7609+ ?~ pats [%& ~]
7610+ ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
7611+ =/ name=term name.i.pats
7612+ ?: |(?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
7613+ [%| 'pattern shadows a name']
7614+ =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
7615+ ?: ?=(%| -.rest) rest
7616+ [%& [name p.rest]]
7617+::
7618+++ cell-pattern-types
7619+ |= [names=(list term) env=ienv next=@ud]
7620+ ^- [typ=itype env=ienv next=@ud]
7621+ ?~ names !!
7622+ =/ head=itype [%var next]
7623+ =/ scope=ienv [[i.names [head ~]] env]
7624+ ?~ t.names [head scope +(next)]
7625+ =/ tail=[typ=itype env=ienv next=@ud] $(names t.names, env scope, next +(next))
7626+ [[%cell head typ.tail] env.tail next.tail]
7627+::
7628+:: At every position that must be a cell, opaque or sum types may still
7629+:: contain cells. Do not report a definite mismatch without unfolding them.
7630+++ cell-pattern-spine-unknown
7631+ |= [typ=itype names=(list term) sub=isub]
7632+ ^- ?
7633+ ?~ names |
7634+ ?~ t.names |
7635+ =. typ (itype-walk typ sub)
7636+ ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
7637+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
60437638::
60447639++ infer-cell-branch
60457640 |= [e=expr env=ienv state=istate]
@@ -6051,23 +7646,22 @@
60517646 =/ pats=(list pattern) items.pat.arm
60527647 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
60537648 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6054− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6055− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6056− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6057− =/ one=term name.i.pats
6058− =/ two=term name.i.t.pats
6059− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
6060− [%| ["pattern shadows a name" ~]]
7649+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
7650+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
60617651 =/ subject=iresult (infer-fragment subject.e env state)
60627652 ?: ?=(%| -.subject) subject
60637653 =/ st=istate state.p.subject
7654+ =/ subject-type=itype (itype-normalize typ.p.subject sub.st)
7655+ ?: (itype-has-recursive subject-type)
7656+ [%| ["recursive pattern is not supported by partial inference" ~]]
60647657 ?: (itype-has-face typ.p.subject sub.st)
60657658 [%| ["record patterns are not supported by partial inference" ~]]
6066− =/ head=itype [%var next.st]
6067− =/ tail=itype [%var +(next.st)]
6068− =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
7659+ ?: (cell-pattern-spine-unknown subject-type p.names sub.st)
7660+ [%| ["cell pattern subject is not supported by partial inference" ~]]
7661+ =/ binders=[typ=itype env=ienv next=@ud] (cell-pattern-types p.names env next.st)
7662+ =/ sub=(unit isub) (itype-unify typ.p.subject typ.binders sub.st)
60697663 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
6070− (infer-fragment val.arm [[one [head ~]] [two [tail ~]] env] st(next (add 2 next.st), sub u.sub))
7664+ (infer-fragment val.arm env.binders st(next next.binders, sub u.sub))
60717665::
60727666++ show-itype
60737667 |= [t=itype sub=isub]
@@ -6086,12 +7680,15 @@
60867680 %atom "@{(trip aura.t)}"
60877681 %any-atom "@"
60887682 %flag "?"
7683+ %noun "*"
60897684 %tag (trip txt.literal.t)
60907685 %const (trip txt.literal.t)
60917686 %union
60927687 ?~ label.t (show-itype-cases cases.t sub)
60937688 ?~ args.t (trip u.label.t)
60947689 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
7690+ %recursive ?~(label.t "recursive mold" (trip u.label.t))
7691+ %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
60957692 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
60967693 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
60977694 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
@@ -6131,9 +7728,12 @@
61317728 %atom |
61327729 %any-atom |
61337730 %flag |
7731+ %noun |
61347732 %tag |
61357733 %const |
61367734 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
7735+ %recursive |
7736+ %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
61377737 %face $(typ body.typ)
61387738 %fn |($(typ sample.typ) $(typ product.typ))
61397739 %cell |($(typ hed.typ) $(typ tal.typ))
@@ -6144,6 +7744,7 @@
61447744 ^- tape
61457745 =/ normalized=itype (itype-normalize typ sub)
61467746 ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
7747+ ?: (itype-has-hidden-recursive normalized) label
61477748 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
61487749 ?: (gth (lent vars) 26) label
61497750 =/ printable=itype (canonical-itype normalized vars)
@@ -6152,8 +7753,8 @@
61527753:: A capital in a written mold is generalized with its enclosing ++.
61537754:: Atom constraints may remain generic; until full rigidity checking
61547755:: is implemented, do not report a type if one became more specific.
6155−:: Whether distinct written capitals may become equal is a doc question;
6156−:: the partial checker leaves such inference unsupported for now.
7756+:: Distinct written capitals cannot be forced equal; use the same
7757+:: capital where a type must be shared (Decisions 2026-10-30).
61577758::
61587759++ cap-id-in
61597760 |= [n=@ud caps=icaps sub=isub]
@@ -6169,6 +7770,35 @@
61697770 ?: =(n u.ident) &
61707771 $(caps t.caps)
61717772::
7773+++ cap-with-id
7774+ |= [n=@ud caps=icaps sub=isub]
7775+ ^- (unit icap)
7776+ ?~ caps ~
7777+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7778+ =/ ident=(unit @ud)
7779+ ?+ -.resolved ~
7780+ %var `id.resolved
7781+ %avar `id.resolved
7782+ ==
7783+ ?~ ident $(caps t.caps)
7784+ ?: =(n u.ident) `i.caps
7785+ $(caps t.caps)
7786+::
7787+++ merged-capitals
7788+ |= [caps=icaps sub=isub]
7789+ ^- (unit [first=icap second=icap])
7790+ ?~ caps ~
7791+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7792+ =/ ident=(unit @ud)
7793+ ?+ -.resolved ~
7794+ %var `id.resolved
7795+ %avar `id.resolved
7796+ ==
7797+ ?~ ident $(caps t.caps)
7798+ =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
7799+ ?^ found `[u.found i.caps]
7800+ $(caps t.caps)
7801+::
61727802++ constrained-capitals
61737803 |= [caps=icaps sub=isub]
61747804 ^- ?
@@ -6207,9 +7837,12 @@
62077837 %atom |
62087838 %any-atom |
62097839 %flag |
7840+ %noun |
62107841 %tag |
62117842 %const |
62127843 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
7844+ %recursive |
7845+ %collection (lien args.t |=(c=itype (has-atom-var n c)))
62137846 %face $(t body.t)
62147847 %fn |($(t sample.t) $(t product.t))
62157848 %cell |($(t hed.t) $(t tal.t))
@@ -6256,9 +7889,9 @@
62567889::
62577890:: Build the supported part of the value environment in dependency order.
62587891:: Each pass adds successful definitions. Forward references become
6259−:: available on a later pass; recursive groups and unsupported syntax do
6260−:: not enter the environment. Generalized definitions are closed, so a
6261−:: use instantiates its variables afresh.
7892+:: available on a later pass; unsupported syntax does not enter the
7893+:: environment. Generalized definitions are closed, so a use instantiates
7894+:: its variables afresh.
62627895::
62637896++ global-value-names
62647897 |= ds=(list def)
@@ -6276,8 +7909,319 @@
62767909 ?~ t.hits &
62777910 |
62787911::
7912+:: A top-level gate may refer to itself through one monomorphic placeholder.
7913+:: Its declared sample is inferred first and preserves its field faces.
7914+:: Unify the completed body with that placeholder before generalization;
7915+:: reporting repeats the same check instead of instantiating the gate's
7916+:: generalized interface inside its own body. Mutual groups stay unsupported.
7917+::
7918+++ direct-self-call
7919+ |= [e=expr name=term]
7920+ ^- ?
7921+ ?: ?=(%group -.e) $(e inner.e)
7922+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7923+ ?. ?=(%call -.e) |
7924+ ?. ?=(%wing -.head.e) |
7925+ =(names.head.e ~[name])
7926+::
7927+++ branch-base-arm
7928+ |= [e=expr name=term]
7929+ ^- (unit expr)
7930+ ?: ?=(%group -.e) $(e inner.e)
7931+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7932+ ?. ?=(%branch -.e) ~
7933+ ?~ arms.e ~
7934+ ?~ t.arms.e ~
7935+ ?^ t.t.arms.e ~
7936+ =/ x=arm i.arms.e
7937+ =/ y=arm i.t.arms.e
7938+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) ~
7939+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) ~
7940+ ?: =(val.lit.pat.x val.lit.pat.y) ~
7941+ =/ first=? (direct-self-call val.x name)
7942+ =/ second=? (direct-self-call val.y name)
7943+ ?: =(first second) ~
7944+ `?:(first val.y val.x)
7945+::
7946+:: Infer the base arm independently, with the self binding removed. Only
7947+:: a closed type whose constraints resolved can seed the recursive result.
7948+:: The regular body inference then checks both arms with shared state.
7949+::
7950+++ recursive-branch-seed
7951+ |= [d=def env=ienv state=istate]
7952+ ^- (unit itype)
7953+ ?. ?=(%value -.d) ~
7954+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) ~
7955+ =/ gate=expr val.d
7956+ =/ body=expr
7957+ ?- -.gate
7958+ %gate body.gate
7959+ %gate-wide body.gate
7960+ * !!
7961+ ==
7962+ =/ base=(unit expr) (branch-base-arm body name.d)
7963+ ?~ base ~
7964+ =/ outer=ienv (skim env |=(entry=[name=term scheme=ischeme] !=(name.entry name.d)))
7965+ =/ sam=isample-result
7966+ ?- -.gate
7967+ %gate (infer-sample sample.gate outer state)
7968+ %gate-wide (infer-sample sample.gate outer state)
7969+ * !!
7970+ ==
7971+ ?: ?=(%| -.sam) ~
7972+ =/ inferred=iresult (infer-fragment u.base env.p.sam state.p.sam)
7973+ ?: ?=(%| -.inferred) ~
7974+ ?: (pending-tags tags.state.p.inferred sub.state.p.inferred) ~
7975+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred) ~
7976+ =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7977+ ?: ?=(^ (itype-vars typ)) ~
7978+ ?: (itype-has-tag typ) ~
7979+ `typ
7980+::
7981+++ infer-recursive-gate
7982+ |= [d=def env=ienv state=istate]
7983+ ^- iresult
7984+ ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
7985+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
7986+ [%| ["recursive definition is not a gate" ~]]
7987+ =/ result=(unit itype) (recursive-branch-seed d env state)
7988+ =/ gate=expr val.d
7989+ =/ sam=isample-result
7990+ ?- -.gate
7991+ %gate (infer-sample sample.gate env state)
7992+ %gate-wide (infer-sample sample.gate env state)
7993+ * !!
7994+ ==
7995+ ?: ?=(%| -.sam)
7996+ =/ diag=(unit idiag)
7997+ ?- -.gate
7998+ %gate (sample-import-invalid sample.gate env state)
7999+ %gate-wide (sample-import-invalid sample.gate env state)
8000+ * ~
8001+ ==
8002+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
8003+ [%| [p.sam ~]]
8004+ =/ id=@ud next.state.p.sam
8005+ =/ product=itype ?~(result [%var id] u.result)
8006+ =/ st=istate state.p.sam(next +(id))
8007+ =/ seed=itype [%fn typ.p.sam product]
8008+ =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
8009+ =/ body=expr
8010+ ?- -.gate
8011+ %gate body.gate
8012+ %gate-wide body.gate
8013+ * !!
8014+ ==
8015+ =/ out=iresult (infer-fragment body seeded st)
8016+ ?: ?=(%| -.out) out
8017+ =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
8018+ ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
8019+ [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
8020+::
8021+++ dependency-root
8022+ |= names=(list term)
8023+ ^- (list term)
8024+ ?~ names ~
8025+ ~[(rear names)]
8026+::
8027+++ dependency-exprs
8028+ |= xs=(list expr)
8029+ ^- (list term)
8030+ ?~ xs ~
8031+ =/ first=(list term) (dependency-expr i.xs)
8032+ (weld first $(xs t.xs))
8033+::
8034+++ dependency-pieces
8035+ |= xs=(list piece)
8036+ ^- (list term)
8037+ ?~ xs ~
8038+ =/ first=(list term)
8039+ ?- -.i.xs
8040+ %expr (dependency-expr p.i.xs)
8041+ %text ~
8042+ ==
8043+ (weld first $(xs t.xs))
8044+::
8045+++ dependency-qsegs
8046+ |= xs=(list qseg)
8047+ ^- (list term)
8048+ ?~ xs ~
8049+ =/ first=(list term)
8050+ ?- -.i.xs
8051+ %expr (dependency-expr p.i.xs)
8052+ %knot ~
8053+ ==
8054+ (weld first $(xs t.xs))
8055+::
8056+++ dependency-items
8057+ |= xs=(list item)
8058+ ^- (list term)
8059+ ?~ xs ~
8060+ =/ first=(list term) (dependency-expr val.i.xs)
8061+ (weld first $(xs t.xs))
8062+::
8063+++ dependency-edits
8064+ |= xs=(list edit)
8065+ ^- (list term)
8066+ ?~ xs ~
8067+ =/ first=(list term) (dependency-expr val.i.xs)
8068+ (weld first $(xs t.xs))
8069+::
8070+++ dependency-arms
8071+ |= xs=(list arm)
8072+ ^- (list term)
8073+ ?~ xs ~
8074+ =/ first=(list term) (dependency-expr val.i.xs)
8075+ (weld first $(xs t.xs))
8076+::
8077+++ dependency-defs
8078+ |= xs=(list def)
8079+ ^- (list term)
8080+ ?~ xs ~
8081+ =/ first=(list term)
8082+ ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
8083+ ~
8084+ (weld first $(xs t.xs))
8085+::
8086+++ dependency-expr
8087+ |= e=expr
8088+ ^- (list term)
8089+ ?- -.e
8090+ %str (dependency-pieces pieces.e)
8091+ %qath (dependency-qsegs segs.e)
8092+ %wing (dependency-root names.e)
8093+ %change
8094+ =/ first=(list term) (dependency-root target.e)
8095+ =/ last=(list term) (dependency-edits edits.e)
8096+ (weld first last)
8097+ %pair (dependency-expr val.e)
8098+ %unit (dependency-expr val.e)
8099+ %group (dependency-expr inner.e)
8100+ %list (dependency-exprs items.e)
8101+ %tuple (dependency-items items.e)
8102+ %gate (dependency-expr body.e)
8103+ %gate-wide (dependency-expr body.e)
8104+ %call
8105+ =/ first=(list term) (dependency-expr head.e)
8106+ =/ last=(list term) (dependency-exprs args.e)
8107+ (weld first last)
8108+ %cast (dependency-expr val.e)
8109+ %trace
8110+ =/ first=(list term) (dependency-expr val.e)
8111+ =/ last=(list term) (dependency-expr then.e)
8112+ (weld first last)
8113+ %branch
8114+ =/ first=(list term) (dependency-expr subject.e)
8115+ =/ last=(list term) (dependency-arms arms.e)
8116+ (weld first last)
8117+ %body
8118+ =/ first=(list term) (dependency-defs defs.e)
8119+ =/ last=(list term) (dependency-expr final.e)
8120+ (weld first last)
8121+ * ~
8122+ ==
8123+::
8124+:: Infer a cyclic component with one monomorphic seed per gate. All members
8125+:: must succeed before any scheme is available; pending constraints and
8126+:: unresolved branch joins remain partial.
8127++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
8128++$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
8129+++ seed-gate-group
8130+ |= [ds=(list def) env=ienv state=istate]
8131+ ^- igate-seeds
8132+ ?~ ds [%& [~ state]]
8133+ =/ d=def i.ds
8134+ ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
8135+ =/ gate=expr val.d
8136+ ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
8137+ [%| ["recursive group contains a non-gate" ~]]
8138+ =/ initial=istate (reserve-def-caps gate state)
8139+ =/ sam=isample-result
8140+ ?- -.gate
8141+ %gate (infer-sample sample.gate env initial)
8142+ %gate-wide (infer-sample sample.gate env initial)
8143+ * !!
8144+ ==
8145+ ?: ?=(%| -.sam) [%| [p.sam ~]]
8146+ =/ body=expr
8147+ ?- -.gate
8148+ %gate body.gate
8149+ %gate-wide body.gate
8150+ * !!
8151+ ==
8152+ =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
8153+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
8154+ =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
8155+ =/ rest=igate-seeds $(ds t.ds, state after)
8156+ ?: ?=(%| -.rest) rest
8157+ [%& [[entry entries.p.rest] state.p.rest]]
8158+::
8159+++ group-seed-env
8160+ |= [entries=(list igate-entry) env=ienv]
8161+ ^- ienv
8162+ ?~ entries env
8163+ [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
8164+::
8165+++ infer-gate-group-bodies
8166+ |= [entries=(list igate-entry) seeds=ienv state=istate]
8167+ ^- igate-seeds
8168+ ?~ entries [%& [~ state]]
8169+ =/ entry=igate-entry i.entries
8170+ ?> ?=(%fn -.typ.entry)
8171+ =/ scope=ienv (weld seeds env.entry)
8172+ =/ out=iresult (infer-fragment body.entry scope state(caps caps.entry))
8173+ ?: ?=(%| -.out) out
8174+ =/ uni=(unit isub) (itype-unify product.typ.entry typ.p.out sub.state.p.out)
8175+ ?~ uni [%| ["recursive group constraint is not supported by partial inference" ~]]
8176+ =. caps.entry caps.state.p.out
8177+ =/ after=istate state.p.out(sub u.uni, caps caps.state)
8178+ =/ rest=igate-seeds $(entries t.entries, state after)
8179+ ?: ?=(%| -.rest) rest
8180+ [%& [[entry entries.p.rest] state.p.rest]]
8181+::
8182+++ group-schemes
8183+ |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
8184+ ^- (each ienv idiag)
8185+ ?~ entries [%& ~]
8186+ =/ entry=igate-entry i.entries
8187+ =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
8188+ ?^ merged
8189+ [%| ["distinct type variables must not be forced equal" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
8190+ ?: (constrained-capitals caps.entry sub.state)
8191+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
8192+ =/ typ=itype (itype-normalize typ.entry sub.state)
8193+ ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
8194+ [%| ["recursive group needs unsupported inference" ~]]
8195+ =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
8196+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8197+ =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
8198+ ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
8199+ =/ rest=(each ienv idiag) $(entries t.entries)
8200+ ?: ?=(%| -.rest) rest
8201+ [%& [[name.entry [typ vars]] p.rest]]
8202+::
8203+++ infer-gate-group
8204+ |= [ds=(list def) env=ienv state=istate]
8205+ ^- ilocal-result
8206+ =/ names=(list term) (global-value-names ds)
8207+ ?. (levy names |=(n=term (unique-value-name n names)))
8208+ [%| ["recursive group contains duplicate names" ~]]
8209+ ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
8210+ [%| ["recursive group shadows a name" ~]]
8211+ =/ scoped=istate state(globals (weld names globals.state))
8212+ =/ seeded=igate-seeds (seed-gate-group ds env scoped)
8213+ ?: ?=(%| -.seeded) seeded
8214+ =/ seeds=ienv (group-seed-env entries.p.seeded ~)
8215+ =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
8216+ ?: ?=(%| -.body) body
8217+ ?: (pending-tags tags.state.p.body sub.state.p.body)
8218+ [%| ["recursive group has unresolved literal constraints" ~]]
8219+ =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
8220+ ?: ?=(%| -.schemes) schemes
8221+ [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
8222+::
62798223++ add-supported-defs
6280− |= [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]
8224+ |= [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)]
62818225 ^- ienv
62828226 ?~ ds env
62838227 =/ d=def i.ds
@@ -6285,7 +8229,10 @@
62858229 ?. (unique-value-name name.d globals) $(ds t.ds)
62868230 ?^ (ienv-lookup name.d env) $(ds t.ds)
62878231 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6288− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top])
8232+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8233+ =. initial (reserve-def-caps val.d initial)
8234+ =/ result=iresult (infer-fragment val.d env initial)
8235+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
62898236 ?: ?=(%| -.result) $(ds t.ds)
62908237 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
62918238 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
@@ -6295,14 +8242,254 @@
62958242 ?: (gth (lent vars) 26) $(ds t.ds)
62968243 $(ds t.ds, env [[name.d [typ vars]] env])
62978244::
8245++$ iresolved [env=ienv grouped=(list term)]
8246++$ iadj (map term (list term))
8247++$ ivisited (map term ?)
8248++$ iwork (list [name=term done=?])
8249++$ iwresult [seen=ivisited order=(list term)]
8250++$ icresult [seen=ivisited component=(list term)]
8251++$ icomponents (list (list term))
8252+++ graph-nameset
8253+ |= [names=(list term) seen=ivisited]
8254+ ^- ivisited
8255+ ?~ names seen
8256+ $(names t.names, seen (~(put by seen) i.names &))
8257+::
8258+++ graph-edges
8259+ |= [name=term graph=iadj]
8260+ ^- (list term)
8261+ =/ found=(unit (list term)) (~(get by graph) name)
8262+ ?~ found ~
8263+ u.found
8264+::
8265+++ graph-make-forward
8266+ |= [ds=(list def) names=ivisited graph=iadj]
8267+ ^- iadj
8268+ ?~ ds graph
8269+ ?. ?=(%value -.i.ds) $(ds t.ds)
8270+ =/ deps=(list term) (dependency-expr val.i.ds)
8271+ =. deps (skim deps |=(n=term ?=(^ (~(get by names) n))))
8272+ $(ds t.ds, graph (~(put by graph) name.i.ds deps))
8273+::
8274+++ graph-add-reverse
8275+ |= [name=term edges=(list term) reverse=iadj]
8276+ ^- iadj
8277+ ?~ edges reverse
8278+ =/ prior=(list term) (graph-edges i.edges reverse)
8279+ $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
8280+::
8281+++ graph-reverse
8282+ |= [names=(list term) graph=iadj reverse=iadj]
8283+ ^- iadj
8284+ ?~ names reverse
8285+ =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
8286+ $(names t.names)
8287+::
8288+++ graph-order
8289+ |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
8290+ ^- iwresult
8291+ ?~ todo [seen order]
8292+ =/ event=[name=term done=?] i.todo
8293+ ?: done.event $(todo t.todo, order [name.event order])
8294+ ?: ?=(^ (~(get by seen) name.event)) $(todo t.todo)
8295+ =. seen (~(put by seen) name.event &)
8296+ =/ children=iwork (turn (graph-edges name.event graph) |=(n=term [n |]))
8297+ $(todo (weld children [[name.event &] t.todo]))
8298+::
8299+++ graph-collect
8300+ |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
8301+ ^- icresult
8302+ ?~ todo [seen component]
8303+ ?: ?=(^ (~(get by seen) i.todo)) $(todo t.todo)
8304+ =. seen (~(put by seen) i.todo &)
8305+ $(todo (weld (graph-edges i.todo graph) t.todo), component [i.todo component])
8306+::
8307+++ graph-collect-all
8308+ |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
8309+ ^- icomponents
8310+ ?~ order comps
8311+ ?: ?=(^ (~(get by seen) i.order)) $(order t.order)
8312+ =/ found=icresult (graph-collect ~[i.order] seen ~ graph)
8313+ $(order t.order, seen seen.found, comps [component.found comps])
8314+::
8315+:: Two depth-first passes find components before group inference. Maps
8316+:: preserve the graph identity; duplicate global names fail closed.
8317+++ graph-components
8318+ |= [ds=(list def) names=(list term)]
8319+ ^- icomponents
8320+ =/ nameset=ivisited ~
8321+ =/ pending=(list term) names
8322+ |-
8323+ ?^ pending
8324+ ?: ?=(^ (~(get by nameset) i.pending)) ~
8325+ $(pending t.pending, nameset (~(put by nameset) i.pending &))
8326+ =/ graph=iadj (graph-make-forward ds nameset ~)
8327+ =/ reverse=iadj (graph-reverse names graph ~)
8328+ =/ order=iwresult (graph-order (turn names |=(n=term [n |])) ~ ~ graph)
8329+ (graph-collect-all order.order ~ reverse ~)
8330+::
8331+++ graph-cycle
8332+ |= [component=(list term) graph=iadj]
8333+ ^- ?
8334+ ?~ component |
8335+ ?^ t.component &
8336+ (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
8337+::
8338+++ add-groups
8339+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) state=istate]
8340+ ^- iresolved
8341+ ?~ components [env grouped]
8342+ =/ component=(list term) i.components
8343+ ?. (graph-cycle component graph) $(components t.components)
8344+ ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
8345+ =/ members=(list def)
8346+ %+ skim ds
8347+ |= d=def
8348+ &(?=(%value -.d) (lien component |=(n=term =(n name.d))))
8349+ ?. =((lent members) (lent component)) $(components t.components)
8350+ ?. (levy component |=(n=term (unique-value-name n globals.state))) $(components t.components)
8351+ =/ result=ilocal-result (infer-gate-group members env state)
8352+ ?: ?=(%| -.result) $(components t.components)
8353+ $(components t.components, env env.p.result, grouped (weld component grouped))
8354+::
8355+++ resolve-groups
8356+ |= [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)]
8357+ ^- iresolved
8358+ =/ env=ienv ~
8359+ =/ grouped=(list term) ~
8360+ =/ names=(list term) (global-value-names ds)
8361+ =/ nameset=ivisited (graph-nameset names ~)
8362+ =/ graph=iadj (graph-make-forward ds nameset ~)
8363+ =/ components=icomponents (graph-components ds names)
8364+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8365+ |-
8366+ =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
8367+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8368+ =/ out=iresolved (add-groups ds components graph next grouped initial)
8369+ ?: =(env env.out) out
8370+ $(env env.out, grouped grouped.out)
8371+::
62988372++ resolve-supported-defs
6299− |= [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]
8373+ |= [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)]
63008374 ^- ienv
6301− =/ env=ienv ~
8375+ env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
8376+::
8377+:: A diagnostic-only proof for a narrow syntactic value cycle. Every
8378+:: edge is an unqualified wing in a supported expression, and samples
8379+:: may not shadow global bindings. Unknown forms yield no conclusion.
8380++$ icyclesite [name=term at=span]
8381++$ icycle [name=term first=span next=span]
8382+++ cycle-sites-list
8383+ |= [xs=(list expr) globals=(list term) locals=(list term)]
8384+ ^- (unit (list icyclesite))
8385+ ?~ xs `~
8386+ =/ first=(unit (list icyclesite)) (cycle-sites i.xs globals locals)
8387+ ?~ first ~
8388+ =/ tail=(unit (list icyclesite)) $(xs t.xs)
8389+ ?~ tail ~
8390+ `(weld u.first u.tail)
8391+::
8392+++ cycle-sample-name
8393+ |= [sam=sample globals=(list term) locals=(list term)]
8394+ ^- (unit (unit term))
8395+ ?- -.sam
8396+ %bind
8397+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
8398+ ``name.sam
8399+ %face
8400+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
8401+ ``name.sam
8402+ %bare `~
8403+ * ~
8404+ ==
8405+::
8406+++ cycle-sites
8407+ |= [e=expr globals=(list term) locals=(list term)]
8408+ ^- (unit (list icyclesite))
8409+ ?- -.e
8410+ %wing
8411+ ?. ?=([@ ~] names.e) ~
8412+ `~[[i.names.e at.e]]
8413+ %lit `~
8414+ %str
8415+ ?: (lien pieces.e |=(p=piece ?=(%expr -.p))) ~
8416+ `~
8417+ %group $(e inner.e)
8418+ %body ?~(defs.e $(e final.e) ~)
8419+ %cast $(e val.e)
8420+ %gate
8421+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
8422+ ?~ binder ~
8423+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
8424+ $(e body.e, locals nested)
8425+ %gate-wide
8426+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
8427+ ?~ binder ~
8428+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
8429+ $(e body.e, locals nested)
8430+ %call
8431+ =/ first=(unit (list icyclesite)) $(e head.e)
8432+ ?~ first ~
8433+ =/ tail=(unit (list icyclesite)) (cycle-sites-list args.e globals locals)
8434+ ?~ tail ~
8435+ `(weld u.first u.tail)
8436+ * ~
8437+ ==
8438+::
8439+++ cycle-definitely-atom
8440+ |= e=expr
8441+ ^- ?
8442+ ?: ?=(%group -.e) $(e inner.e)
8443+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8444+ ?. ?=(%cast -.e) |
8445+ |(?=(%aura -.shape.e) ?=(%flag -.shape.e))
8446+::
8447+++ cycle-proof-group
8448+ |= [members=(list def) globals=(list term)]
8449+ ^- ?
8450+ ?~ members &
8451+ ?. ?=(%value -.i.members) |
8452+ ?. (unique-value-name name.i.members globals) |
8453+ ?. ?=(^ (cycle-sites val.i.members globals ~)) |
8454+ $(members t.members)
8455+::
8456+++ cycle-find-site
8457+ |= [sites=(list icyclesite) component=(list term)]
8458+ ^- (unit span)
8459+ ?~ sites ~
8460+ ?: (lien component |=(n=term =(n name.i.sites))) `at.i.sites
8461+ $(sites t.sites)
8462+::
8463+++ cycle-group-errors
8464+ |= [members=(list def) component=(list term) globals=(list term)]
8465+ ^- (list icycle)
8466+ ?~ members ~
8467+ =/ d=def i.members
8468+ ?> ?=(%value -.d)
8469+ =/ tail=(list icycle) $(members t.members)
8470+ ?. (cycle-definitely-atom val.d) tail
8471+ =/ sites=(unit (list icyclesite)) (cycle-sites val.d globals ~)
8472+ ?~ sites tail
8473+ =/ found=(unit span) (cycle-find-site u.sites component)
8474+ ?~ found tail
8475+ [[name.d at.d u.found] tail]
8476+::
8477+++ definite-value-cycles
8478+ |= [ds=(list def) globals=(list term)]
8479+ ^- (list icycle)
8480+ =/ names=(list term) (global-value-names ds)
8481+ =/ graph=iadj (graph-make-forward ds (graph-nameset names ~) ~)
8482+ =/ components=icomponents (graph-components ds names)
8483+ =/ out=(list icycle) ~
63028484 |-
6303− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at)
6304− ?: =(next env) env
6305− $(env next)
8485+ ?~ components out
8486+ =/ component=(list term) i.components
8487+ ?. (graph-cycle component graph) $(components t.components)
8488+ =/ members=(list def)
8489+ (skim ds |=(d=def &(?=(%value -.d) (lien component |=(n=term =(n name.d))))))
8490+ ?. =((lent members) (lent component)) $(components t.components)
8491+ ?. (cycle-proof-group members globals) $(components t.components)
8492+ $(components t.components, out (weld (cycle-group-errors members component globals) out))
63068493::
63078494+| %union-analysis
63088495::
@@ -6525,6 +8712,22 @@
65258712 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
65268713 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
65278714::
8715+:: In an API file or before main's kind is known, a lone `+$ poke`
8716+:: may be a declaration rather than a mold that shadows the prelude. Do not call
8717+:: that one collision definite, and do not hide unrelated scope errors.
8718+++ pending-declared-poke
8719+ |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
8720+ ^- ?
8721+ ?. (lien prelude-molds |=(n=term =(%poke n))) |
8722+ ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
8723+ =/ pokes=(list def)
8724+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
8725+ ?~ pokes |
8726+ ?^ t.pokes |
8727+ =/ remaining=(list def)
8728+ (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
8729+ (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
8730+::
65288731++ module-mold-types
65298732 |= [molds=imolds state=istate]
65308733 ^- (each imold-types @t)
@@ -6538,6 +8741,147 @@
65388741 ?: ?=(%| -.rest) rest
65398742 [%& [[name.m template.u.t] p.rest]]
65408743::
8744+:: Prepare a provisional interface from the trusted vendored source.
8745+:: Every declared name remains reserved, but only molds and values this
8746+:: fragment can infer are usable. Unsupported bodies are not validated.
8747+:: An optional internal source supplies the prelude's one supported import;
8748+:: clients cannot import that path directly. Named unions retain their origin.
8749+::
8750+:: Recognize only the complete standard prelude list shape. Its recursive
8751+:: tail uses the same parameter and the unqualified list name. The reader
8752+:: verifies Hoon's list provenance before producing the same collection type.
8753+:: The prelude source and reader output are trusted caller inputs.
8754+::
8755+++ standard-prelude-list
8756+ |= sh=shape
8757+ ^- ?
8758+ ?. ?=(%generic -.sh) |
8759+ ?~ vars.sh |
8760+ ?^ t.vars.sh |
8761+ =/ var=@t i.vars.sh
8762+ ?. ?=(%union -.body.sh) |
8763+ =/ cs=(list shape) cases.body.sh
8764+ ?~ cs |
8765+ ?~ t.cs |
8766+ ?^ t.t.cs |
8767+ ?. ?=(%const -.i.cs) |
8768+ ?. =(%null form.lit.i.cs) |
8769+ ?. ?=(%cell -.i.t.cs) |
8770+ =/ fs=(list field) fields.i.t.cs
8771+ ?~ fs |
8772+ ?~ t.fs |
8773+ ?^ t.t.fs |
8774+ ?. ?=(%face -.i.fs) |
8775+ ?. =(%i name.i.fs) |
8776+ ?. ?=(%tvar -.shape.i.fs) |
8777+ ?. =(var name.shape.i.fs) |
8778+ ?. ?=(%face -.i.t.fs) |
8779+ ?. =(%t name.i.t.fs) |
8780+ =/ tail=shape shape.i.t.fs
8781+ ?. ?=(%apply -.tail) |
8782+ ?. =(~[%list] ref.tail) |
8783+ ?~ args.tail |
8784+ ?^ t.args.tail |
8785+ ?. ?=(%tvar -.i.args.tail) |
8786+ =(var name.i.args.tail)
8787+::
8788+++ prelude-label
8789+ |= [typ=itype name=term]
8790+ ^- itype
8791+ ?. ?=(%union -.typ) typ
8792+ ?^ args.typ typ
8793+ typ(label `name)
8794+::
8795+++ partial-prelude-molds
8796+ |= [molds=imolds state=istate]
8797+ ^- imold-types
8798+ ?~ molds ~
8799+ =/ m=[name=term body=shape] i.molds
8800+ ?: &(=(at.state /lib/jibb/prelude/jibb) =(%list name.m))
8801+ ?. (standard-prelude-list body.m) $(molds t.molds)
8802+ [[%list [[%collection %list ~[[%var 0]]] ~[0]]] $(molds t.molds)]
8803+ =/ out=(unit [template=ischeme state=istate])
8804+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
8805+ ?~ out $(molds t.molds)
8806+ =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
8807+ =. typ.template.u.out (prelude-label typ.template.u.out name.m)
8808+ [[name.m template.u.out] $(molds t.molds)]
8809+::
8810+++ partial-prelude-interface-with-internal
8811+ |= [src=@t internal-source=(unit @t)]
8812+ ^- (unit ifile)
8813+ ?: =(0 src) ~
8814+ =/ at=path /lib/jibb/prelude/jibb
8815+ =/ parsed (parse at src)
8816+ ?: ?=(%| -.parsed) ~
8817+ =/ private=(unit ijimports)
8818+ ?~ imports.p.parsed `~
8819+ ?. ?=([[%jibb *] ~] imports.p.parsed) ~
8820+ ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
8821+ ?~ internal-source ~
8822+ =/ built=jfile-result
8823+ (infer-jibb-file /lib/jibb/internal/jibb u.internal-source ~ ~ ~ ~[/lib/jibb/internal/jibb] ~ ~ ~ ~)
8824+ ?: ?=(%| -.built) ~
8825+ `~[[face.i.imports.p.parsed iface.p.built]]
8826+ ?~ private ~
8827+ ?~ defs.p.parsed ~
8828+ ?. (module-scope-valid p.parsed ~ ~) ~
8829+ =/ ds=(list def) defs.p.parsed
8830+ =/ molds=imolds (collect-simple-molds ds)
8831+ =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8832+ =/ globals=(list term) (weld (import-binding-names imports.p.parsed) (global-value-names ds))
8833+ :: Remove raw list before inferring any template, so an altered list
8834+ :: cannot leak through an alias. Its name remains reserved either way.
8835+ =/ declared=? (lien names |=(name=term =(%list name)))
8836+ =/ env-molds=imolds molds
8837+ =? env-molds declared
8838+ (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
8839+ =/ reserved=(list term) ?:(declared ~[%list] ~)
8840+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~]
8841+ =/ mt=imold-types (partial-prelude-molds molds state)
8842+ =/ partial=ifile [~ mt at ~]
8843+ :: An explicitly qualified re-export must resolve. Other unsupported
8844+ :: prelude declarations remain reserved but absent from the interface.
8845+ =/ required=imolds
8846+ %+ skim molds
8847+ |= m=[name=term body=shape]
8848+ =/ sh=shape body.m
8849+ ?. ?=(%ref -.sh) |
8850+ ?~ names.sh |
8851+ ?=(^ t.names.sh)
8852+ ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
8853+ =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
8854+ `[env mt at ~]
8855+::
8856+++ partial-prelude-interface
8857+ |= src=@t
8858+ ^- (unit ifile)
8859+ (partial-prelude-interface-with-internal src ~)
8860+::
8861++$ iprelude [iface=ifile values=(list term) molds=(list term)]
8862+::
8863+++ prepare-prelude
8864+ |= src=@t
8865+ ^- (unit iprelude)
8866+ =/ iface=(unit ifile) (partial-prelude-interface src)
8867+ ?~ iface ~
8868+ =/ parsed (parse /lib/jibb/prelude/jibb src)
8869+ ?: ?=(%| -.parsed) ~
8870+ =/ vals=(list term) (global-value-names defs.p.parsed)
8871+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
8872+ `[u.iface vals ms]
8873+::
8874+++ prepare-prelude-with-internal
8875+ |= [src=@t internal-source=@t]
8876+ ^- (unit iprelude)
8877+ =/ iface=(unit ifile) (partial-prelude-interface-with-internal src `internal-source)
8878+ ?~ iface ~
8879+ =/ parsed (parse /lib/jibb/prelude/jibb src)
8880+ ?: ?=(%| -.parsed) ~
8881+ =/ vals=(list term) (global-value-names defs.p.parsed)
8882+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
8883+ `[u.iface vals ms]
8884+::
65418885++ module-values-complete
65428886 |= [ds=(list def) env=ienv]
65438887 ^- ?
@@ -6559,11 +8903,13 @@
65598903 $(cache t.cache)
65608904::
65618905++ resolve-jibb-imports
6562− |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term) cache=jcache]
8906+ |= [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)]
65638907 ^- jimports-result
65648908 ?~ imports [%& [~ cache]]
65658909 ?. ?=(%jibb -.i.imports) $(imports t.imports)
65668910 =/ at=path (weld path.i.imports `path`~[%jibb])
8911+ ?: =(at /lib/jibb/internal/jibb)
8912+ [%| 'the prelude internal module is private']
65678913 ?: (lien active |=(p=path =(p at)))
65688914 [%| (crip "import cycle at {(spud at)}")]
65698915 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -6572,24 +8918,287 @@
65728918 =/ cached=(unit ifile) (find-jibb-cache at cache)
65738919 =/ iface=jfile-result
65748920 ?^ cached [%& [u.cached cache]]
6575− (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache)
8921+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
65768922 ?: ?=(%| -.iface) [%| p.iface]
65778923 =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
65788924 ?: ?=(%| -.rest) rest
65798925 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
65808926::
8927+:: Provisional declaration extraction only; this does not derive asks,
8928+:: validate imported types, or claim that an API module has checked.
8929++$ iapi-path [at=span name=term segments=(list pseg) full=term diffs=(list term) scry=(unit (list pseg))]
8930+++ api-path-mark
8931+ |= [sh=shape marks=(list term)]
8932+ ^- (unit term)
8933+ ?. ?=(%ref -.sh) ~
8934+ ?. ?=([@ ~] names.sh) ~
8935+ ?. (unique-value-name i.names.sh marks) ~
8936+ `i.names.sh
8937+::
8938+++ api-path-diffs
8939+ |= [shapes=(list shape) marks=(list term) used=(list term)]
8940+ ^- (unit (list term))
8941+ ?~ shapes `~
8942+ =/ n=(unit term) (api-path-mark i.shapes marks)
8943+ ?~ n ~
8944+ ?: (lien used |=(x=term =(x u.n))) ~
8945+ =/ rest=(unit (list term)) $(shapes t.shapes, used [u.n used])
8946+ ?~ rest ~
8947+ `[u.n u.rest]
8948+::
8949+++ api-path-payload
8950+ |= [sh=shape marks=(list term)]
8951+ ^- (unit [full=term diffs=(list term)])
8952+ =/ direct=(unit term) (api-path-mark sh marks)
8953+ ?^ direct `[u.direct ~]
8954+ ?. ?=(%apply -.sh) ~
8955+ ?. =(~[%facts] ref.sh) ~
8956+ ?~ args.sh ~
8957+ ?~ t.args.sh ~
8958+ =/ full=(unit term) (api-path-mark i.args.sh marks)
8959+ ?~ full ~
8960+ =/ diffs=(unit (list term)) (api-path-diffs t.args.sh marks ~[u.full])
8961+ ?~ diffs ~
8962+ `[u.full u.diffs]
8963+::
8964++$ iapi-parameter [name=term aura=@ta at=span]
8965+++ api-path-parameters
8966+ |= [segments=(list pseg) seen=(list term)]
8967+ ^- (unit (list iapi-parameter))
8968+ ?~ segments `~
8969+ ?: ?=(%knot -.i.segments) $(segments t.segments)
8970+ =/ seg=pseg i.segments
8971+ ?> ?=(%typed -.seg)
8972+ ?: =(0 aura.seg) ~
8973+ ?: (lien seen |=(n=term =(n name.seg))) ~
8974+ =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
8975+ ?~ rest ~
8976+ `[[name.seg aura.seg at.seg] u.rest]
8977+::
8978+++ api-scry-parameters-compatible
8979+ |= [scry=(list iapi-parameter) watch=(list iapi-parameter)]
8980+ ^- ?
8981+ ?~ scry &
8982+ ?. (lien watch |=(p=iapi-parameter &(=(name.p name.i.scry) =(aura.p aura.i.scry)))) |
8983+ $(scry t.scry)
8984+::
8985+++ api-path-one
8986+ |= [sh=shape marks=(list term)]
8987+ ^- (unit iapi-path)
8988+ ?. ?=(%cell -.sh) ~
8989+ =/ fs=(list field) fields.sh
8990+ ?~ fs ~
8991+ ?~ t.fs ~
8992+ ?~ t.t.fs ~
8993+ ?: (gth (lent fs) 4) ~
8994+ ?. ?=(%bare -.i.fs) ~
8995+ =/ tag=shape shape.i.fs
8996+ ?. ?=(%const -.tag) ~
8997+ ?. =(%term form.lit.tag) ~
8998+ =/ name=term val.lit.tag
8999+ ?. (jibb-face-name name) ~
9000+ ?. ?=(%bare -.i.t.fs) ~
9001+ =/ path-shape=shape shape.i.t.fs
9002+ ?. ?=(%path -.path-shape) ~
9003+ ?. ?=(%bare -.i.t.t.fs) ~
9004+ =/ payload=(unit [full=term diffs=(list term)]) (api-path-payload shape.i.t.t.fs marks)
9005+ ?~ payload ~
9006+ =/ scry=(unit (unit (list pseg)))
9007+ ?~ t.t.t.fs `~
9008+ =/ entry=field i.t.t.t.fs
9009+ ?. ?=(%face -.entry) ~
9010+ ?. =(%scry name.entry) ~
9011+ ?. ?=(%path -.shape.entry) ~
9012+ ``segs.shape.entry
9013+ ?~ scry ~
9014+ =/ params=(unit (list iapi-parameter)) (api-path-parameters segs.path-shape ~)
9015+ ?~ params ~
9016+ ?^ u.scry
9017+ =/ scry-params=(unit (list iapi-parameter)) (api-path-parameters u.u.scry ~)
9018+ ?~ scry-params ~
9019+ ?. (api-scry-parameters-compatible u.scry-params u.params) ~
9020+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
9021+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
9022+::
9023+++ api-path-many
9024+ |= [shapes=(list shape) marks=(list term) seen=(list term)]
9025+ ^- (unit (list iapi-path))
9026+ ?~ shapes `~
9027+ =/ one=(unit iapi-path) (api-path-one i.shapes marks)
9028+ ?~ one ~
9029+ ?: (lien seen |=(n=term =(n name.u.one))) ~
9030+ =/ rest=(unit (list iapi-path)) $(shapes t.shapes, seen [name.u.one seen])
9031+ ?~ rest ~
9032+ `[u.one u.rest]
9033+::
9034+++ api-path-declaration
9035+ |= [sh=shape marks=(list term)]
9036+ ^- (unit (list iapi-path))
9037+ ?: ?=(%union -.sh) (api-path-many cases.sh marks ~)
9038+ (api-path-many ~[sh] marks ~)
9039+::
9040+:: Derived gates share the value namespace. /% marks name molds; /- and
9041+:: /= also introduce faces that cannot be shadowed by a derived value.
9042+++ api-import-faces
9043+ |= imports=(list import)
9044+ ^- (list term)
9045+ ?~ imports ~
9046+ ?- -.i.imports
9047+ %mark $(imports t.imports)
9048+ %sur [name.i.imports $(imports t.imports)]
9049+ %jibb [face.i.imports $(imports t.imports)]
9050+ ==
9051+::
9052+++ api-derived-names-valid
9053+ |= [paths=(list iapi-path) poke-names=(list term) mod=module prelude-values=(list term)]
9054+ ^- ?
9055+ =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
9056+ =/ derived=(list term) (weld path-names poke-names)
9057+ =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
9058+ (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
9059+::
9060+:: Analysis only. Successful external entries must be unchanged results
9061+:: produced for the declared marks; no request interface is produced.
9062++$ iapi-mark-type [name=term typ=itype]
9063++$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
9064+++ api-diff-types
9065+ |= [names=(list term) externals=imark-externals declared=(list term)]
9066+ ^- (unit (list iapi-mark-type))
9067+ ?~ names `~
9068+ =/ typ=(unit itype) (find-imported-mark i.names externals declared)
9069+ ?~ typ ~
9070+ =/ tail=(unit (list iapi-mark-type)) $(names t.names)
9071+ ?~ tail ~
9072+ `[[i.names u.typ] u.tail]
9073+::
9074+++ api-path-types
9075+ |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
9076+ ^- (unit (list iapi-path-typed))
9077+ ?~ paths `~
9078+ =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
9079+ ?~ full ~
9080+ =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
9081+ ?~ diffs ~
9082+ =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
9083+ ?~ tail ~
9084+ `[[i.paths u.full u.diffs] u.tail]
9085+::
9086+++ api-poke-mark-names
9087+ |= [pokes=(list def) declared=(list term)]
9088+ ^- (unit (list term))
9089+ ?~ pokes `~
9090+ ?^ t.pokes ~
9091+ =/ d=def i.pokes
9092+ ?. ?=(%mold -.d) ~
9093+ =/ sh=shape shape.d
9094+ ?: ?=(%union -.sh) (api-path-diffs cases.sh declared ~)
9095+ =/ name=(unit term) (api-path-mark sh declared)
9096+ ?~ name ~
9097+ `~[u.name]
9098+::
9099+++ api-path-analysis
9100+ |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
9101+ ^- (unit (list iapi-path-typed))
9102+ =/ ds=(list def) defs.mod
9103+ =/ declarations=(list def)
9104+ (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
9105+ ?. ?=([* ~] declarations) ~
9106+ =/ pokes=(list def)
9107+ (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
9108+ ?: (gth (lent pokes) 1) ~
9109+ =/ ordinary=(list def)
9110+ (skim ds |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
9111+ ?. (module-scope-valid mod(defs ordinary) prelude-values prelude-molds) ~
9112+ =/ declared=(list term) (collect-mark-imports imports.mod)
9113+ =/ poke-names=(unit (list term)) (api-poke-mark-names pokes declared)
9114+ ?~ poke-names ~
9115+ =/ decl=def i.declarations
9116+ ?> ?=(%mold -.decl)
9117+ =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
9118+ ?~ paths ~
9119+ ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
9120+ (api-path-types u.paths externals declared)
9121+::
9122+:: Source/graph entry for path analysis only. The returned paths retain
9123+:: reader-derived mark types and import resolution has checked reachable
9124+:: Jibb dependencies. This is not an API interface or a module check.
9125+++ api-path-analysis-source
9126+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
9127+ ^- (each (list iapi-path-typed) @t)
9128+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
9129+ ?~ prepared [%| 'API path analysis needs the prepared prelude']
9130+ =/ parsed (parse file src)
9131+ ?: ?=(%| -.parsed) [%| 'API path source does not parse']
9132+ =/ prelude=(unit ifile) `iface.u.prepared
9133+ =/ deps=jimports-result
9134+ (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
9135+ ?: ?=(%| -.deps) [%| p.deps]
9136+ =/ paths=(unit (list iapi-path-typed))
9137+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
9138+ ?~ paths [%| 'API path declaration needs unsupported analysis']
9139+ [%& u.paths]
9140+::
9141+++ api-mark-exports
9142+ |= [marks=(list term) all=(list term) externals=imark-externals]
9143+ ^- imold-types
9144+ ?~ marks ~
9145+ =/ t=(unit itype) (find-imported-mark i.marks externals all)
9146+ ?~ t $(marks t.marks)
9147+ [[i.marks [u.t ~]] $(marks t.marks)]
9148+::
9149+:: Experimental direct poke-only API. Unsupported API declarations fail
9150+:: as a whole; supplied mark reader results retain their existing boundary.
9151+++ api-poke-interface
9152+ |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
9153+ ^- (unit ifile)
9154+ ?. ?=([%ui %api @ %jibb ~] at) ~
9155+ ?~ prelude ~
9156+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
9157+ =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
9158+ ?~ poke ~
9159+ ?. ?=(%union -.typ.u.poke) ~
9160+ ?^ vars.u.poke ~
9161+ =/ compatible=?
9162+ %+ lien cases.typ.u.poke
9163+ |= c=itype
9164+ ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
9165+ ?. compatible ~
9166+ ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
9167+ ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
9168+ =/ marks=(list term) (collect-mark-imports imports.mod)
9169+ ?. ?=([@ ~] marks) ~
9170+ =/ ds=(list def) defs.mod
9171+ ?. ?=([[%mold *] ~] ds) ~
9172+ ?. =(%poke name.i.ds) ~
9173+ =/ sh=shape shape.i.ds
9174+ ?. ?=([%ref *] sh) ~
9175+ ?. ?=([@ ~] names.sh) ~
9176+ =/ n=term i.names.sh
9177+ ?. (unique-value-name n marks) ~
9178+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
9179+ =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
9180+ ?~ mark ~
9181+ =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
9182+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]]]
9183+::
65819184++ infer-jibb-file
6582− |= [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]
9185+ |= [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)]
65839186 ^- jfile-result
6584− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
65859187 =/ parsed (parse at src)
65869188 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
65879189 =/ mod=module p.parsed
6588− ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
9190+ ?: ?=([%ui %api *] at)
9191+ =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
9192+ ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
9193+ [%& [u.iface [[at u.iface] cache]]]
9194+ ?. (module-scope-valid mod prelude-values prelude-molds)
9195+ ?: (pending-declared-poke at mod prelude-values prelude-molds)
9196+ [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
9197+ [%| (crip "module has conflicting names: {(spud at)}")]
65899198 =/ vals=(list term) (global-value-names defs.mod)
65909199 ?: (lien vals |=(n=term =(n %main)))
65919200 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
6592− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache)
9201+ =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
65939202 ?: ?=(%| -.js) [%| p.js]
65949203 =/ molds=imolds (collect-simple-molds defs.mod)
65959204 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
@@ -6597,13 +9206,13 @@
65979206 =/ marks=(list term) (collect-mark-imports imports.mod)
65989207 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
65999208 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6600− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top]
9209+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
66019210 =/ mts=(each imold-types @t) (module-mold-types molds state)
66029211 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
6603− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at)
9212+ =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
66049213 ?. (module-values-complete defs.mod env)
66059214 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
6606− [%& [[env p.mts at] [[at [env p.mts at]] cache.p.js]]]
9215+ [%& [[env p.mts at ~] [[at [env p.mts at ~]] cache.p.js]]]
66079216::
66089217:: +golden-types-with-modules fails closed for imports without prelude
66099218:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -6618,8 +9227,10 @@
66189227 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
66199228 (golden-types-with-marks file src externals mark-externals)
66209229::
6621−:: The caller supplies the actual prelude source. Its current names are
6622−:: reserved, but its incomplete inventory and types are not checked here.
9230+:: The caller supplies the actual prelude source. Its declared names are
9231+:: reserved, and supported inferred types are made available. The inventory
9232+:: and the checker are incomplete, so this never claims a checked module.
9233+:: Hosts may prepare the same trusted source once and reuse its interface.
66239234::
66249235++ golden-types-with-prelude
66259236 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
@@ -6629,29 +9240,64 @@
66299240 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
66309241 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
66319242 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
6632− =/ prelude-values=(list term) (global-value-names defs.p.prelude)
6633− =/ prelude-molds=(list term)
6634− (turn (collect-simple-molds defs.p.prelude) |=(m=[name=term body=shape] name.m))
9243+ =/ prepared=(unit iprelude) (prepare-prelude prelude-source)
9244+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
9245+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
9246+::
9247+++ golden-types-with-prelude-and-internal
9248+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t internal-source=@t]
9249+ ^- @t
9250+ =/ prepared=(unit iprelude) (prepare-prelude-with-internal prelude-source internal-source)
9251+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
9252+::
9253+++ golden-types-with-prepared-prelude
9254+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
9255+ ^- @t
9256+ =/ parsed (parse file src)
9257+ ?: ?=(%| -.parsed) (show-error src p.parsed)
9258+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
9259+ =/ prelude-values=(list term) values.u.prepared
9260+ =/ prelude-molds=(list term) molds.u.prepared
9261+ =/ iface=(unit ifile) `iface.u.prepared
66359262 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
9263+ ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
9264+ 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
66369265 'partial inference; module not checked\0amodule has conflicting names'
66379266 =/ js=jimports-result
6638− (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~)
9267+ (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
66399268 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
66409269 =/ scope-values=(list term)
66419270 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
6642− (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds)
9271+ (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
66439272::
66449273:: +golden-types-with-marks: supply declared mark types separately from /sur
66459274:: entries, as [mark result] with the result from +read-mark:jibb-import.
66469275:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
66479276::
9277+:: Callers pass unchanged structured reader results; graph validation
9278+:: remains in the existing bridge, and failures stay available lazily.
9279+++ reader-result-for-checker
9280+ |= result=*
9281+ ^- *
9282+ ?: ?=([%ok *] result) [%& +.result]
9283+ result
9284+::
9285+++ golden-types-with-reader-diagnostics
9286+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
9287+ ^- @t
9288+ =/ ex=iexternals
9289+ (turn externals |=(e=[module=term name=term result=*] [module.e name.e (reader-result-for-checker result.e)]))
9290+ =/ mx=imark-externals
9291+ (turn mark-externals |=(e=[mark=term result=*] [mark.e (reader-result-for-checker result.e)]))
9292+ (golden-types-with-marks file src ex mx)
9293+::
66489294++ golden-types-with-marks
66499295 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
66509296 ^- @t
6651− (golden-types-in-context file src externals mark-externals ~ ~ ~)
9297+ (golden-types-in-context file src externals mark-externals ~ ~ ~ ~)
66529298::
66539299++ golden-types-in-context
6654− |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term)]
9300+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
66559301 ^- @t
66569302 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
66579303 =/ parsed (parse file src)
@@ -6661,7 +9307,9 @@
66619307 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
66629308 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
66639309 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
6664− =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds file)
9310+ =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
9311+ =/ cycles=(list icycle) (definite-value-cycles ds globals)
9312+ =/ env=ienv env.resolution
66659313 =/ lines=(list @t) ~
66669314 |-
66679315 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -6670,15 +9318,40 @@
66709318 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
66719319 ?. (unique-value-name name.d globals)
66729320 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
9321+ =/ cycle=(list icycle) (skim cycles |=(c=icycle =(name.c name.d)))
9322+ ?^ cycle
9323+ =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
9324+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
9325+ ?: (lien grouped.resolution |=(n=term =(n name.d)))
9326+ =/ found=(unit ischeme) (ienv-lookup name.d env)
9327+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
9328+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
9329+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
9330+ $(ds t.ds, lines [line lines])
66739331 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6674− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top])
9332+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
9333+ =. initial (reserve-def-caps val.d initial)
9334+ =/ result=iresult
9335+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
9336+ (infer-recursive-gate d env initial)
9337+ (infer-fragment val.d env initial)
66759338 ?: ?=(%| -.result)
66769339 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
9340+ =/ merged=(unit [first=icap second=icap])
9341+ (merged-capitals caps.state.p.result sub.state.p.result)
9342+ ?^ merged
9343+ =/ diag=idiag
9344+ ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]
9345+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
66779346 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
66789347 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
66799348 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
9349+ ?: (pending-null tags.state.p.result sub.state.p.result)
9350+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: `~` needs context in partial inference") lines])
66809351 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
66819352 $(ds t.ds, lines [(crip "++ {(trip name.d)}: tag needs context in partial inference") lines])
9353+ ?: (itype-has-hidden-recursive typ)
9354+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
66829355 ?: (itype-has-hidden-generic typ)
66839356 $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
66849357 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)