@@ -4595,8 +4595,10 @@
45954595:: their defaulting and inferred generalization are implemented.
45964596:: Bare @ is a separate unrestricted atom type. A directional fit check
45974597:: permits concrete atoms to widen to it, never the reverse. A fit that
4598−:: needs a not-yet-implemented constraint remains unsupported. Only
4599−:: unfaced cells are represented here.
4598+:: needs a not-yet-implemented constraint remains unsupported. Named unions
4599+:: retain origin and ordered arguments, including phantom arguments, apart
4600+:: from their display name. Generic cases must be disjoint for all arguments.
4601+:: Unnamed union printing is informational; it is not Jibb syntax.
46004602::
46014603+$ itype
46024604 $~ [%var 0]
@@ -4606,11 +4608,19 @@
46064608 [%atom aura=@ta]
46074609 [%any-atom ~]
46084610 [%flag ~]
4611+ [%noun ~]
4612+ [%tag id=@ud literal=lit constructor=?]
4613+ [%const literal=lit]
4614+ [%collection name=term args=(list itype)]
4615+ [%recursive module=term name=term label=(unit @t)]
4616+ [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4617+ [%face name=term body=itype]
46094618 [%fn sample=itype product=itype]
46104619 [%cell hed=itype tal=itype]
46114620 ==
46124621+$ ibinding [id=@ud val=itype]
46134622+$ isub (list ibinding)
4623++$ ipending [id=@ud literal=lit]
46144624::
46154625++ itype-lookup
46164626 |= [n=@ud sub=isub]
@@ -4635,6 +4645,10 @@
46354645 =/ found=(unit itype) (itype-lookup id.t sub)
46364646 ?~ found t
46374647 $(t u.found)
4648+ %tag
4649+ =/ found=(unit itype) (itype-lookup id.t sub)
4650+ ?~ found t
4651+ $(t u.found)
46384652 ==
46394653::
46404654++ itype-occurs
@@ -4648,6 +4662,13 @@
46484662 %atom |
46494663 %any-atom |
46504664 %flag |
4665+ %noun |
4666+ %tag =(n id.t)
4667+ %const |
4668+ %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)))
4671+ %face $(t body.t)
46514672 %fn |($(t sample.t) $(t product.t))
46524673 %cell |($(t hed.t) $(t tal.t))
46534674 ==
@@ -4664,6 +4685,16 @@
46644685 =. a (itype-walk a sub)
46654686 =. b (itype-walk b sub)
46664687 ?: =(a b) `sub
4688+ ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4689+ ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
4690+ ?: &(?=(%union -.a) ?=(%union -.b))
4691+ ?. =(origin.a origin.b) ~
4692+ ?: &(?=(~ args.a) ?=(~ args.b)) ?:(=(cases.a cases.b) `sub ~)
4693+ ?~ origin.a ~
4694+ (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)
46674698 ?: ?=(%var -.a)
46684699 ?: (itype-occurs id.a b sub) ~
46694700 `[[id.a b] sub]
@@ -4686,7 +4717,12 @@
46864717 ?: ?=(%avar -.b)
46874718 ?. |(?=(%atom -.a) ?=(%any-atom -.a) ?=(%flag -.a)) ~
46884719 `[[id.b a] sub]
4720+ ?: &(?=(%const -.a) ?=(%const -.b))
4721+ ?:(=(val.literal.a val.literal.b) `sub ~)
46894722 ?: &(?=(%atom -.a) ?=(%atom -.b)) ~
4723+ ?: &(?=(%face -.a) ?=(%face -.b))
4724+ ?. =(name.a name.b) ~
4725+ $(a body.a, b body.b)
46904726 ?: &(?=(%fn -.a) ?=(%fn -.b))
46914727 =/ first=(unit isub) $(a sample.a, b sample.b)
46924728 ?~ first ~
@@ -4697,6 +4733,15 @@
46974733 $(a tal.a, b tal.b, sub u.first)
46984734 ~
46994735::
4736+++ itype-unify-args
4737+ |= [as=(list itype) bs=(list itype) sub=isub]
4738+ ^- (unit isub)
4739+ ?~ as ?~(bs `sub ~)
4740+ ?~ bs ~
4741+ =/ next=(unit isub) (itype-unify i.as i.bs sub)
4742+ ?~ next ~
4743+ $(as t.as, bs t.bs, sub u.next)
4744+::
47004745:: +itype-fit: one-way widening from an actual type to an expected type
47014746::
47024747:: An unknown variable used where @ is expected gains a fresh atom
@@ -4714,6 +4759,13 @@
47144759 %atom |
47154760 %any-atom &
47164761 %flag |
4762+ %noun |
4763+ %tag |
4764+ %const |
4765+ %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4766+ %recursive |
4767+ %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4768+ %face $(t body.t)
47174769 %fn |($(t sample.t) $(t product.t))
47184770 %cell |($(t hed.t) $(t tal.t))
47194771 ==
@@ -4736,6 +4788,14 @@
47364788:: Related auras in a structural unification need a common-type rule;
47374789:: until that rule is implemented, report an unknown rather than error.
47384790::
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+::
47394799++ itype-family-related
47404800 |= [a=itype b=itype sub=isub]
47414801 ^- ?
@@ -4744,6 +4804,12 @@
47444804 ?: &(?=(%atom -.a) ?=(%atom -.b))
47454805 ?. !=(aura.a aura.b) |
47464806 |((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)
4810+ ?: &(?=(%face -.a) ?=(%face -.b))
4811+ ?. =(name.a name.b) |
4812+ $(a body.a, b body.b)
47474813 ?: &(?=(%cell -.a) ?=(%cell -.b))
47484814 |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
47494815 ?: &(?=(%fn -.a) ?=(%fn -.b))
@@ -4764,6 +4830,13 @@
47644830 %atom &
47654831 %any-atom &
47664832 %flag &
4833+ %noun |
4834+ %tag &
4835+ %const &
4836+ %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)))
4839+ %face $(typ body.typ)
47674840 %fn |($(typ sample.typ) $(typ product.typ))
47684841 %cell |($(typ hed.typ) $(typ tal.typ))
47694842 ==
@@ -4781,6 +4854,204 @@
47814854 ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b
47824855 ~
47834856::
4857+:: Unifying an already-bound tuple with a faced position would need to
4858+:: update the bound type. Until substitutions can retain that information,
4859+:: variable-dependent face merges stay unresolved.
4860+::
4861+++ itype-has-face
4862+ |= [t=itype sub=isub]
4863+ ^- ?
4864+ =. t (itype-walk t sub)
4865+ ?- -.t
4866+ %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4867+ %face &
4868+ %cell |($(t hed.t) $(t tal.t))
4869+ %fn |($(t sample.t) $(t product.t))
4870+ * |
4871+ ==
4872+::
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+::
4881+++ itype-face-asym
4882+ |= [a=itype b=itype sub=isub]
4883+ ^- ?
4884+ =. a (itype-walk a sub)
4885+ =. 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)
4889+ ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4890+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4891+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
4892+ ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4893+ ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
4894+ |
4895+::
4896+:: A successful cast keeps any explicit faces from either side while
4897+:: retaining the target's aura choices. Both faces have already matched.
4898+::
4899+++ itype-merge-faces
4900+ |= [actual=itype expected=itype sub=isub]
4901+ ^- itype
4902+ =. actual (itype-walk actual sub)
4903+ =. expected (itype-walk expected sub)
4904+ ?: &(?=(%face -.actual) ?=(%face -.expected))
4905+ [%face name.expected $(actual body.actual, expected body.expected)]
4906+ ?: ?=(%face -.actual)
4907+ [%face name.actual $(actual body.actual)]
4908+ ?: ?=(%face -.expected)
4909+ [%face name.expected $(expected body.expected)]
4910+ ?: &(?=(%cell -.actual) ?=(%cell -.expected))
4911+ [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
4912+ expected
4913+::
4914+++ itype-output-may-be-cell
4915+ |= [t=itype sub=isub]
4916+ ^- ?
4917+ =. t (itype-walk t sub)
4918+ ?- -.t
4919+ %var &
4920+ %cell &
4921+ %union &
4922+ %recursive &
4923+ %noun &
4924+ %collection &
4925+ %face $(t body.t)
4926+ %fn |($(t sample.t) $(t product.t))
4927+ * |
4928+ ==
4929+::
4930+++ pending-tags
4931+ |= [tags=(list ipending) sub=isub]
4932+ ^- ?
4933+ ?~ tags |
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))) &
4942+ $(tags t.tags)
4943+::
4944+:: Tags remain constrained until a mold selects a case or permitted atom
4945+:: type. Never generalize an unresolved tag through aliases or cells.
4946+::
4947+++ itype-has-tag
4948+ |= t=itype
4949+ ^- ?
4950+ ?- -.t
4951+ %tag &
4952+ %collection (lien args.t |=(c=itype (itype-has-tag c)))
4953+ %face $(t body.t)
4954+ %fn |($(t sample.t) $(t product.t))
4955+ %cell |($(t hed.t) $(t tal.t))
4956+ %union |((lien cases.t |=(c=itype (itype-has-tag c))) (lien args.t |=(c=itype (itype-has-tag c))))
4957+ * |
4958+ ==
4959+::
4960+++ itype-has-union
4961+ |= t=itype
4962+ ^- ?
4963+ ?- -.t
4964+ %union &
4965+ %collection (lien args.t |=(c=itype (itype-has-union c)))
4966+ %face $(t body.t)
4967+ %fn |($(t sample.t) $(t product.t))
4968+ %cell |($(t hed.t) $(t tal.t))
4969+ * |
4970+ ==
4971+::
4972+:: Until a visible generic alias can be selected, expanding a named
4973+:: generic union would hide phantom arguments and its origin. This is a
4974+:: limitation of partial inference, not the unnamed-union print notation.
4975+::
4976+++ itype-has-hidden-generic
4977+ |= t=itype
4978+ ^- ?
4979+ ?- -.t
4980+ %union
4981+ ?: &(?=(~ label.t) ?=(^ args.t)) &
4982+ (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)))
4984+ %face $(t body.t)
4985+ %fn |($(t sample.t) $(t product.t))
4986+ %cell |($(t hed.t) $(t tal.t))
4987+ * |
4988+ ==
4989+::
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+::
5016+++ itype-fit-cases
5017+ |= [actual=itype cases=(list itype) sub=isub next=@ud]
5018+ ^- ifit
5019+ =/ good=(unit ifit) ~
5020+ =/ pending=? |
5021+ |-
5022+ ?~ cases
5023+ ?: pending [%unknown ~]
5024+ ?~ good [%bad ~]
5025+ u.good
5026+ =/ trial=ifit (itype-fit actual i.cases sub next)
5027+ ?- -.trial
5028+ %unknown $(cases t.cases, pending &)
5029+ %bad $(cases t.cases)
5030+ %ok
5031+ ?^ good [%unknown ~]
5032+ $(cases t.cases, good `trial)
5033+ ==
5034+::
5035+:: A constructor needs a case with its tag at the head and a payload
5036+:: compatible with the expected gate sample. Other case forms do not
5037+:: identify a constructor.
5038+::
5039+++ itype-fit-ctor-cases
5040+ |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
5041+ ^- ifit
5042+ =/ found=(unit ifit) ~
5043+ |-
5044+ ?~ cases ?~(found [%bad ~] u.found)
5045+ =/ c=itype (itype-walk i.cases sub)
5046+ ?. ?=(%cell -.c) $(cases t.cases)
5047+ =/ head=itype (itype-walk hed.c sub)
5048+ ?. ?=(%const -.head) $(cases t.cases)
5049+ ?. =(%term form.literal.head) $(cases t.cases)
5050+ ?. =(val.literal.head val.tag) $(cases t.cases)
5051+ ?^ found [%unknown ~]
5052+ =/ trial=ifit (itype-fit sample tal.c sub next)
5053+ $(cases t.cases, found `trial)
5054+::
47845055++ itype-fit
47855056 |= [actual=itype expected=itype sub=isub next=@ud]
47865057 ^- ifit
@@ -4789,6 +5060,81 @@
47895060 =. actual (itype-walk actual sub)
47905061 =. expected (itype-walk expected sub)
47915062 ?: =(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 ~]
5075+ ?: &(?=(%union -.actual) ?=(%union -.expected))
5076+ ?. =(origin.actual origin.expected) [%unknown ~]
5077+ ?: &(?=(~ args.actual) ?=(~ args.expected))
5078+ ?:(=(cases.actual cases.expected) [%ok sub next] [%unknown ~])
5079+ ?~ origin.actual [%unknown ~]
5080+ =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
5081+ ?^ unified [%ok u.unified next]
5082+ [%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)
5087+ ?: ?=(%union -.actual) [%unknown ~]
5088+ ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
5089+ ?: &(?=(%union -.expected) !?=(%var -.actual))
5090+ (itype-fit-cases actual cases.expected sub next)
5091+ ?: ?=(%tag -.actual)
5092+ ?: ?=(%var -.expected)
5093+ =/ u=(unit isub) (itype-unify actual expected sub)
5094+ ?~ u [%bad ~]
5095+ [%ok u.u next]
5096+ ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5097+ ?: ?=(%face -.expected) $(expected body.expected)
5098+ ?: constructor.actual
5099+ ?. ?=(%fn -.expected) [%bad ~]
5100+ =/ product=itype (itype-walk product.expected sub)
5101+ =/ cases=(list itype) ?:(?=(%union -.product) cases.product ~[product])
5102+ =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
5103+ ?. ?=(%ok -.trial) trial
5104+ [%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 ~]
5109+ ?: ?=(%const -.expected)
5110+ ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
5111+ ?: ?=(%atom -.expected)
5112+ ?: |(=(%tas aura.expected) =(%ta aura.expected))
5113+ [%ok [[id.actual expected] sub] next]
5114+ [%bad ~]
5115+ ?: ?=(%flag -.expected)
5116+ ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok [[id.actual expected] sub] next] [%bad ~])
5117+ ?: ?=(%any-atom -.expected) [%ok [[id.actual expected] sub] next]
5118+ [%bad ~]
5119+ ?: ?=(%const -.actual)
5120+ ?: ?=(%var -.expected)
5121+ =/ u=(unit isub) (itype-unify actual expected sub)
5122+ ?~ u [%bad ~]
5123+ [%ok u.u next]
5124+ ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5125+ ?: ?=(%face -.expected) $(expected body.expected)
5126+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5127+ [%unknown ~]
5128+ ?: ?=(%const -.expected)
5129+ ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
5130+ ?: ?=(%atom -.expected)
5131+ ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
5132+ [%bad ~]
5133+ ?: ?=(%flag -.expected)
5134+ ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok sub next] [%bad ~])
5135+ ?: ?=(%any-atom -.expected) [%ok sub next]
5136+ [%bad ~]
5137+ ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
47925138 ?: ?=(%any-atom -.expected)
47935139 ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
47945140 ?: ?=(%var -.actual)
@@ -4811,18 +5157,37 @@
48115157 =/ first=ifit $(actual hed.actual, expected hed.expected)
48125158 ?. ?=(%ok -.first) first
48135159 $(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 ~]
48145169 ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
48155170 [%unknown ~]
48165171 ?: |(?=(%var -.actual) ?=(%var -.expected))
48175172 =/ unified=(unit isub) (itype-unify actual expected sub)
48185173 ?~ unified
5174+ ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5175+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
48195176 ?: (itype-family-related actual expected sub) [%unknown ~]
48205177 [%bad ~]
48215178 [%ok u.unified next]
5179+ ?: &(?=(%face -.actual) ?=(%face -.expected))
5180+ ?. =(name.actual name.expected) [%bad ~]
5181+ $(actual body.actual, expected body.expected)
5182+ ?: ?=(%face -.actual) $(actual body.actual)
5183+ ?: ?=(%face -.expected) $(expected body.expected)
5184+ ?: (itype-face-asym actual expected sub) [%unknown ~]
48225185 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
48235186 [%unknown ~]
48245187 =/ unified=(unit isub) (itype-unify actual expected sub)
48255188 ?~ unified
5189+ ?: |((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 ~]
48265191 ?: (itype-family-related actual expected sub) [%unknown ~]
48275192 [%bad ~]
48285193 [%ok u.unified next]
@@ -4851,24 +5216,58 @@
48515216 ["a shared type variable should reject incompatible arguments" problems]
48525217 =? problems ?=(~ (itype-unify same fine ~))
48535218 ["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]
48545250 problems
48555251::
48565252:: The expression inference below is deliberately a fragment: bindings,
4857−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5253+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
48585254:: result for unsupported syntax is a diagnostic, never a checked module.
48595255::
48605256+$ ischeme [typ=itype vars=(list @ud)]
48615257+$ ienv (list [name=term scheme=ischeme])
4862−+$ imold-types (list [name=term typ=itype])
4863−+$ ifile [values=ienv molds=imold-types]
5258++$ imold-types (list [name=term template=ischeme])
5259++$ iderived [name=term agent=term mark=term]
5260++$ ifile [values=ienv molds=imold-types at=path derived=(list iderived)]
48645261+$ ijimports (list [face=term interface=ifile])
4865−+$ icaps (list [name=@t id=@ud])
5262++$ icap [name=@t id=@ud at=span]
5263++$ icaps (list icap)
5264++$ iparams (list [name=@t typ=itype])
48665265+$ imolds (list [name=term body=shape])
48675266:: A caller supplies the exact noun returned by +read-mold:jibb-import.
48685267:: This core has no Ford dependencies; unrecognized payloads fail closed.
48695268+$ iexternals (list [module=term name=term result=*])
48705269+$ imark-externals (list [mark=term result=*])
4871−+$ 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) active=(list term) in-mold=?]
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)]
48725271+$ idiag [msg=tape sites=(list [at=span note=tape])]
48735272+$ iresult (each [typ=itype state=istate] idiag)
48745273+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -4888,6 +5287,11 @@
48885287 |= [t=itype sub=isub]
48895288 ^- itype
48905289 =. t (itype-walk t sub)
5290+ ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5291+ ?: ?=(%union -.t)
5292+ [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5293+ ?: ?=(%face -.t)
5294+ [%face name.t $(t body.t)]
48915295 ?: ?=(%fn -.t)
48925296 [%fn $(t sample.t) $(t product.t)]
48935297 ?: ?=(%cell -.t)
@@ -4899,18 +5303,27 @@
48995303:: generalize an aura from its sample, which requires constraint analysis
49005304:: beyond this fragment; leave those cases unresolved.
49015305::
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.
49025308++ itype-has-gate
49035309 |= t=itype
49045310 ^- ?
49055311 ?- -.t
49065312 %fn &
49075313 %cell |($(t hed.t) $(t tal.t))
5314+ %recursive |
5315+ %collection (lien args.t |=(c=itype (itype-has-gate c)))
5316+ %face $(t body.t)
5317+ %union (lien cases.t |=(c=itype (itype-has-gate c)))
5318+ %tag |
5319+ %const |
49085320 %var |
49095321 %avar |
49105322 %nvar |
49115323 %atom |
49125324 %any-atom |
49135325 %flag |
5326+ %noun |
49145327 ==
49155328::
49165329++ default-decimals
@@ -4919,6 +5332,8 @@
49195332 ?: (itype-has-gate t) t
49205333 ?- -.t
49215334 %nvar [%atom %ud]
5335+ %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5336+ %face [%face name.t $(t body.t)]
49225337 %cell [%cell $(t hed.t) $(t tal.t)]
49235338 * t
49245339 ==
@@ -4933,6 +5348,13 @@
49335348 %atom ~
49345349 %any-atom ~
49355350 %flag ~
5351+ %noun ~
5352+ %tag ~
5353+ %const ~
5354+ %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))))
5357+ %face $(t body.t)
49365358 %fn (weld $(t sample.t) $(t product.t))
49375359 %cell (weld $(t hed.t) $(t tal.t))
49385360 ==
@@ -4965,6 +5387,13 @@
49655387 %atom t
49665388 %any-atom t
49675389 %flag t
5390+ %noun t
5391+ %tag t
5392+ %const t
5393+ %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)))]
5396+ %face [%face name.t $(t body.t)]
49685397 %fn [%fn $(t sample.t) $(t product.t)]
49695398 %cell [%cell $(t hed.t) $(t tal.t)]
49705399 ==
@@ -4982,6 +5411,13 @@
49825411 %atom |
49835412 %any-atom |
49845413 %flag |
5414+ %noun |
5415+ %tag |
5416+ %const |
5417+ %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)))
5420+ %face $(t body.t)
49855421 %fn |($(t sample.t) $(t product.t))
49865422 %cell |($(t hed.t) $(t tal.t))
49875423 ==
@@ -5042,20 +5478,184 @@
50425478 $(ds t.ds)
50435479::
50445480::
5045−:: The importer owns its algebra. Only successful %atom and %cell nouns
5046−:: in the supported subset are decoded here. In particular a singleton,
5047−:: face, union, collection or recursive reference must not be 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.
5487+::
5488+++ jibb-face-name
5489+ |= name=@
5490+ ^- ?
5491+ =/ chars=tape (trip (@t name))
5492+ ?~ chars |
5493+ ?. (is-lower i.chars) |
5494+ (levy t.chars |=(c=@tD (in c name-mask)))
5495+::
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)
50485600::
50495601++ import-to-itype
50505602 |= node=*
50515603 ^- (unit itype)
50525604 ?@ node ~
50535605 ?+ -.node ~
5606+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
50545607 %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]]
50555624 ?. ?=([%atom @ ~] node) ~
50565625 =/ aura=@ta (@ta +<.node)
50575626 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
50585627 `[%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 ~ ~ ~]
5652+ %face
5653+ ?. ?=([%face @ *] node) ~
5654+ =/ name=@ +<.node
5655+ ?. (jibb-face-name name) ~
5656+ =/ body=(unit itype) $(node +>.node)
5657+ ?~ body ~
5658+ `[%face (@tas name) u.body]
50595659 %cell
50605660 ?. ?=([%cell * *] node) ~
50615661 =/ left=(unit itype) $(node +<.node)
@@ -5065,6 +5665,52 @@
50655665 `[%cell u.left u.right]
50665666 ==
50675667::
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+::
50685714++ find-imported-mold
50695715 |= [module=term name=term externals=iexternals surs=(list term)]
50705716 ^- (unit itype)
@@ -5076,7 +5722,15 @@
50765722 =/ result=* result.i.found
50775723 ?@ result ~
50785724 ?. ?=(%& -.result) ~
5079− (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+
50805734::
50815735++ collect-sur-imports
50825736 |= imports=(list import)
@@ -5105,6 +5759,7 @@
51055759 =/ result=* result.i.found
51065760 ?@ result ~
51075761 ?. ?=(%& -.result) ~
5762+ ?. (imported-faces-valid +.result) ~
51085763 (import-to-itype +.result)
51095764::
51105765++ find-jibb-interface
@@ -5116,13 +5771,251 @@
51165771::
51175772++ find-jibb-mold
51185773 |= [name=term iface=ifile]
5119− ^- (unit itype)
5774+ ^- (unit ischeme)
51205775 =/ ms=imold-types molds.iface
51215776 |-
51225777 ?~ ms ~
5123− ?: =(name name.i.ms) `typ.i.ms
5778+ ?: =(name name.i.ms) `template.i.ms
51245779 $(ms t.ms)
51255780::
5781+:: An exported alias may name a union from another module. Only a
5782+:: nongeneric alias of the same origin is usable through this import face.
5783+::
5784+++ imported-union-alias
5785+ |= [origin=[at=path name=term] molds=imold-types]
5786+ ^- (unit term)
5787+ ?~ molds ~
5788+ =/ template=ischeme template.i.molds
5789+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
5790+ ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
5791+ $(molds t.molds)
5792+::
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.
5807+::
5808+++ itype-in-import
5809+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
5810+ ^- itype
5811+ ?- -.t
5812+ %union
5813+ =/ label=(unit @t)
5814+ ?~ 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
5820+ =/ alias=(unit term) ~
5821+ =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
5822+ =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
5823+ ?~ alias ~
5824+ `(crip "{(trip u.alias)}.{(trip 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)))]
5828+ %face [%face name.t $(t body.t)]
5829+ %fn [%fn $(t sample.t) $(t product.t)]
5830+ %cell [%cell $(t hed.t) $(t tal.t)]
5831+ * t
5832+ ==
5833+::
5834+++ label-direct-union
5835+ |= [typ=itype body=shape name=term state=istate]
5836+ ^- itype
5837+ ?. ?=(%union -.typ) typ
5838+ =/ direct=? ?=(%union -.body)
5839+ =? direct ?=(%generic -.body) ?=(%union -.body.body)
5840+ ?. direct typ
5841+ ?. (lien top-molds.state |=(n=term =(n name))) typ
5842+ [%union cases.typ `[at.state name] `name args.typ]
5843+::
5844+:: Generic mold parameters are lexical and distinct from the enclosing
5845+:: value's capital variables. Arguments are substituted only once, so
5846+:: 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.
5849+::
5850+++ iparam-lookup
5851+ |= [name=@t params=iparams]
5852+ ^- (unit itype)
5853+ ?~ params ~
5854+ ?: =(name name.i.params) `typ.i.params
5855+ $(params t.params)
5856+::
5857+++ distinct-params
5858+ |= names=(list @t)
5859+ ^- ?
5860+ ?~ names &
5861+ ?: (lien t.names |=(n=@t =(n i.names))) |
5862+ $(names t.names)
5863+::
5864+++ bind-params
5865+ |= [names=(list @t) args=(list itype)]
5866+ ^- (unit iparams)
5867+ ?~ names ?~(args `~ ~)
5868+ ?~ args ~
5869+ =/ rest=(unit iparams) $(names t.names, args t.args)
5870+ ?~ rest ~
5871+ `[[i.names i.args] u.rest]
5872+::
5873+++ template-apply
5874+ |= [template=ischeme args=(list itype)]
5875+ ^- (unit itype)
5876+ =/ vars=(list @ud) vars.template
5877+ =/ ren=isub ~
5878+ |-
5879+ ?~ vars ?~(args `(itype-rename typ.template ren) ~)
5880+ ?~ args ~
5881+ $(vars t.vars, args t.args, ren [[i.vars i.args] ren])
5882+::
5883+++ infer-shape-args
5884+ |= [args=(list shape) state=istate]
5885+ ^- (unit [types=(list itype) state=istate])
5886+ ?~ args `[~ state]
5887+ =/ head=(unit [typ=itype state=istate]) (infer-simple-shape i.args state)
5888+ ?~ head ~
5889+ =/ tail=(unit [types=(list itype) state=istate]) $(args t.args, state state.u.head)
5890+ ?~ tail ~
5891+ `[[typ.u.head types.u.tail] state.u.tail]
5892+::
5893+++ fresh-mold-params
5894+ |= [names=(list @t) next=@ud]
5895+ ^- [params=iparams vars=(list @ud) next=@ud]
5896+ ?~ names [~ ~ next]
5897+ =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
5898+ [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
5899+::
5900+++ infer-mold-template
5901+ |= [sh=shape state=istate]
5902+ ^- (unit [template=ischeme state=istate])
5903+ ?: ?=(%generic -.sh)
5904+ ?~ vars.sh ~
5905+ ?. (distinct-params vars.sh) ~
5906+ =/ fresh=[params=iparams vars=(list @ud) next=@ud] (fresh-mold-params vars.sh next.state)
5907+ =/ out=(unit [typ=itype state=istate])
5908+ (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
5909+ ?~ out ~
5910+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
5911+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
5912+ typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
5913+ =/ used=(list @ud) (itype-vars typ.u.out)
5914+ ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5915+ `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state)]
5916+ =/ out=(unit [typ=itype state=istate])
5917+ (infer-simple-shape sh state(params ~, in-mold &))
5918+ ?~ out ~
5919+ ?: ?=(^ (itype-vars typ.u.out)) ~
5920+ `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
5921+::
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+::
51266019++ infer-simple-shape
51276020 |= [sh=shape state=istate]
51286021 ^- (unit [typ=itype state=istate])
@@ -5131,6 +6024,16 @@
51316024 ?: =(0 aura.sh) `[[%any-atom ~] state]
51326025 `[[%atom aura.sh] state]
51336026 %flag `[[%flag ~] state]
6027+ %noun `[[%noun ~] state]
6028+ %const
6029+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
6030+ `[[%const lit.sh] state]
6031+ %union
6032+ =/ pairs=(list upair) (union-pairs cases.sh molds.state)
6033+ ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
6034+ =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
6035+ ?~ cs ~
6036+ `[[%union types.u.cs ~ ~ ~] state.u.cs]
51346037 %cell (infer-simple-fields fields.sh state)
51356038 %fn
51366039 =/ arg=(unit [typ=itype state=istate]) $(sh sample.sh)
@@ -5145,9 +6048,10 @@
51456048 ?^ t.t.names.sh ~
51466049 =/ iface=(unit ifile) (find-jibb-interface i.t.names.sh jimports.state)
51476050 ?^ iface
5148− =/ found=(unit itype) (find-jibb-mold n u.iface)
6051+ =/ found=(unit ischeme) (find-jibb-mold n u.iface)
51496052 ?~ found ~
5150− `[u.found state]
6053+ ?^ vars.u.found ~
6054+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
51516055 =/ found=(unit itype)
51526056 (find-imported-mold i.t.names.sh n externals.state surs.state)
51536057 ?~ found ~
@@ -5159,16 +6063,62 @@
51596063 `[u.imported state]
51606064 ?: (lien active.state |=(x=term =(x n))) ~
51616065 =/ found=(unit shape) (find-simple-mold n molds.state)
5162− ?~ 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]
51636073 =/ out=(unit [typ=itype state=istate])
5164− $(sh u.found, state state(active [n active.state], in-mold &))
6074+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
51656075 ?~ out ~
5166− `[typ.u.out state.u.out(active active.state, in-mold in-mold.state)]
6076+ `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state)]
6077+ %apply
6078+ ?~ ref.sh ~
6079+ =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
6080+ ?~ args ~
6081+ =/ n=term i.ref.sh
6082+ ?^ t.ref.sh
6083+ ?^ t.t.ref.sh ~
6084+ =/ iface=(unit ifile) (find-jibb-interface i.t.ref.sh jimports.state.u.args)
6085+ ?~ iface ~
6086+ =/ template=(unit ischeme) (find-jibb-mold n u.iface)
6087+ ?~ template ~
6088+ ?~ vars.u.template ~
6089+ =/ applied=(unit itype) (template-apply u.template types.u.args)
6090+ ?~ applied ~
6091+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
6092+ ?: (lien active.state.u.args |=(x=term =(x n))) ~
6093+ =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
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]
6103+ ?. ?=(%generic -.u.found) ~
6104+ ?. (distinct-params vars.u.found) ~
6105+ =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6106+ ?~ params ~
6107+ =/ out=(unit [typ=itype state=istate])
6108+ $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
6109+ ?~ 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))
6113+ (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6114+ `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
51676115 %tvar
6116+ =/ param=(unit itype) (iparam-lookup name.sh params.state)
6117+ ?^ param `[u.param state]
51686118 ?: in-mold.state ~
51696119 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
51706120 ?^ n `[[%var u.n] state]
5171− `[[%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])]
51726122 * ~
51736123 ==
51746124::
@@ -5176,13 +6126,25 @@
51766126 |= [fields=(list field) state=istate]
51776127 ^- (unit [typ=itype state=istate])
51786128 ?~ fields ~
5179− ?. ?=(%bare -.i.fields) ~
5180− =/ head=(unit [typ=itype state=istate]) (infer-simple-shape shape.i.fields state)
6129+ =/ field-shape=shape
6130+ ?- -.i.fields
6131+ %bare shape.i.fields
6132+ %face shape.i.fields
6133+ %pun [%ref at.i.fields ~[name.i.fields]]
6134+ ==
6135+ =/ head=(unit [typ=itype state=istate]) (infer-simple-shape field-shape state)
51816136 ?~ head ~
5182− ?~ t.fields head
6137+ =/ t=itype typ.u.head
6138+ =. t
6139+ ?- -.i.fields
6140+ %bare t
6141+ %face [%face name.i.fields t]
6142+ %pun [%face name.i.fields t]
6143+ ==
6144+ ?~ t.fields `[t state.u.head]
51836145 =/ tail=(unit [typ=itype state=istate]) $(fields t.fields, state state.u.head)
51846146 ?~ tail ~
5185− `[[%cell typ.u.head typ.u.tail] state.u.tail]
6147+ `[[%cell t typ.u.tail] state.u.tail]
51866148::
51876149++ infer-sample
51886150 |= [s=sample env=ienv state=istate]
@@ -5203,12 +6165,37 @@
52036165 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
52046166 ?~ t [%| "sample mold is not supported by partial inference"]
52056167 [%& typ.u.t env state.u.t]
5206− * [%| "sample is not supported by partial inference"]
6168+ %pun
6169+ $(s [%face at.s name.s [%ref at.s ~[name.s]]])
6170+ %cell
6171+ (infer-sample-items items.s env state)
52076172 ==
52086173::
6174+:: Cell-sample binders are faces on their positions; at the top of a
6175+:: sample a binder only supplies a name for the whole sample.
6176+::
6177+++ infer-sample-items
6178+ |= [items=(list sample) env=ienv state=istate]
6179+ ^- isample-result
6180+ ?~ items [%| "empty sample is not supported by partial inference"]
6181+ =/ head=isample-result (infer-sample i.items env state)
6182+ ?: ?=(%| -.head) head
6183+ =/ ht=itype typ.p.head
6184+ =. ht
6185+ ?- -.i.items
6186+ %bind [%face name.i.items ht]
6187+ %face [%face name.i.items ht]
6188+ %pun [%face name.i.items ht]
6189+ * ht
6190+ ==
6191+ ?~ t.items [%& ht env.p.head state.p.head]
6192+ =/ tail=isample-result $(items t.items, env env.p.head, state state.p.head)
6193+ ?: ?=(%| -.tail) tail
6194+ [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
6195+::
52096196:: Local definitions generalize only variables outside their enclosing
5210−:: environment and explicit-capital scope. Unresolved groups stay
5211−:: 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.
52126199::
52136200+$ ilocal-result (each [env=ienv state=istate] idiag)
52146201++ free-env-vars
@@ -5272,11 +6259,150 @@
52726259 ^- ?
52736260 ?~ locals &
52746261 =/ m=[name=term body=shape] i.locals
5275− =/ inferred=(unit [typ=itype state=istate])
5276− (infer-simple-shape body.m state(active [name.m active.state], in-mold &))
6262+ =/ inferred=(unit [template=ischeme state=istate])
6263+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
52776264 ?~ inferred |
52786265 $(locals t.locals)
52796266::
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+::
52806406++ infer-local-defs
52816407 |= [ds=(list def) env=ienv state=istate]
52826408 ^- ilocal-result
@@ -5285,56 +6411,890 @@
52856411 |-
52866412 ?~ ds
52876413 ?~ remaining [%& env state]
5288− ?. 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 |)
52896421 $(ds (flop remaining), remaining ~, progressed |)
52906422 =/ d=def i.ds
52916423 ?> ?=(%value -.d)
5292− =/ 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)
52936428 ?: ?=(%| -.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" ~]]
52946435 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
6436+ ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
6437+ $(ds t.ds, remaining [d remaining])
52956438 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
52966439 $(ds t.ds, remaining [d remaining])
52976440 =/ free=(list @ud)
5298− (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))
52996442 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
53006443 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
5301− $(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]
6466+::
6467+:: Read only fields of a known record. Unresolved field constraints and
6468+:: ambiguous repeated faces are outside this fragment. Imported record
6469+:: spines with repeated names are unavailable when used.
6470+::
6471+++ record-fields-named
6472+ |= [name=term t=itype sub=isub]
6473+ ^- (list itype)
6474+ =. t (itype-walk t sub)
6475+ ?: ?=(%face -.t)
6476+ ?:(=(name name.t) ~[body.t] ~)
6477+ ?. ?=(%cell -.t) ~
6478+ =/ first=(list itype) ~
6479+ =/ head=itype (itype-walk hed.t sub)
6480+ =? first ?=(%face -.head) ?:(=(name name.head) ~[body.head] ~)
6481+ (weld first $(t tal.t))
6482+::
6483+++ infer-field-wing
6484+ |= [names=(list term) env=ienv state=istate]
6485+ ^- iresult
6486+ =/ reverse=(list term) (flop names)
6487+ ?~ reverse [%| ["empty wing" ~]]
6488+ =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6489+ ?~ scheme [%| ["field access is not supported by partial inference" ~]]
6490+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
6491+ =/ fields=(list term) t.reverse
6492+ =/ typ=itype typ.inst
6493+ |-
6494+ ?~ fields [%& typ state.inst]
6495+ =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
6496+ ?~ found [%| ["field is not available to partial inference" ~]]
6497+ ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6498+ $(fields t.fields, typ i.found)
53026499::
5303−++ infer-fragment
5304− |= [e=expr env=ienv state=istate]
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.
6503+::
6504+++ context-union-branch
6505+ |= e=expr
6506+ ^- ?
6507+ ?- -.e
6508+ %branch &
6509+ %group $(e inner.e)
6510+ %body ?~(defs.e $(e final.e) |)
6511+ * |
6512+ ==
6513+::
6514+++ infer-union-context
6515+ |= [e=expr expected=itype env=ienv state=istate context=span]
53056516 ^- iresult
6517+ ?: ?=(%group -.e) $(e inner.e)
6518+ ?: &(?=(%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)
6521+ ?: ?=(%branch -.e)
6522+ ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
6523+ ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
6524+ ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
6525+ =/ x=arm i.arms.e
6526+ =/ 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])
6529+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y))
6530+ [%| ["branch pattern is not supported by partial inference" ~]]
6531+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6532+ [%| ["branch pattern is not supported by partial inference" ~]]
6533+ ?: =(val.lit.pat.x val.lit.pat.y)
6534+ [%| ["branch does not cover both loobeans" ~]]
6535+ =/ subject=iresult (infer-fragment subject.e env state)
6536+ ?: ?=(%| -.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" ~]]
6540+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
6541+ ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
6542+ =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
6543+ ?: ?=(%| -.left) left
6544+ =/ right=iresult $(e val.y, state state.p.left)
6545+ ?: ?=(%| -.right) right
6546+ [%& expected state.p.right]
6547+ =/ value=iresult (infer-fragment e env state)
6548+ ?: ?=(%| -.value) value
6549+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
6550+ ?: ?=(%unknown -.fit)
6551+ ?: &(?=(%collection -.expected) =(%list name.expected))
6552+ [%| ["branch list constraint is not supported by partial inference" ~]]
6553+ [%| ["branch union constraint is not supported by partial inference" ~]]
6554+ ?: ?=(%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"]]]]
6561+ [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
6562+ [%& expected state.p.value(sub sub.fit, next next.fit)]
6563+::
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+ ^- ?
53066571 ?- -.e
5307− %lit
5308− ?- form.lit.e
5309− %number ?: =(%ud aura.lit.e)
5310− [%& [%nvar next.state] state(next +(next.state))]
5311− [%& [%atom aura.lit.e] state]
5312− %ship [%& [%atom %p] state]
5313− %date [%& [%atom %da] state]
5314− %duration [%& [%atom %dr] state]
5315− %knot [%& [%atom %ta] state]
5316− %loobean [%& [%flag ~] state]
5317− * [%| ["literal needs contextual inference" ~]]
5318− ==
5319− %str
5320− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
5321− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
5322− [%& [%atom %t] state]
5323− %wing
5324− ?~ names.e [%| ["empty wing" ~]]
5325− ?^ t.names.e
5326− ?^ t.t.names.e [%| ["field access is not supported by partial inference" ~]]
5327− =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
5328− ?~ iface [%| ["field access is not supported by partial inference" ~]]
5329− =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
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+::
7230+++ infer-fragment
7231+ |= [e=expr env=ienv state=istate]
7232+ ^- iresult
7233+ ?- -.e
7234+ %lit
7235+ ?- form.lit.e
7236+ %number ?: =(%ud aura.lit.e)
7237+ [%& [%nvar next.state] state(next +(next.state))]
7238+ [%& [%atom aura.lit.e] state]
7239+ %ship [%& [%atom %p] state]
7240+ %date [%& [%atom %da] state]
7241+ %duration [%& [%atom %dr] state]
7242+ %knot [%& [%atom %ta] state]
7243+ %loobean [%& [%flag ~] state]
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])]
7246+ ==
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)
7271+ %wing
7272+ ?~ names.e [%| ["empty wing" ~]]
7273+ ?^ t.names.e
7274+ ?^ t.t.names.e (infer-field-wing names.e env state)
7275+ =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
7276+ ?~ iface (infer-field-wing names.e env state)
7277+ =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
53307278 ?~ member [%| ["module member is not available to partial inference" ~]]
7279+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
53317280 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
53327281 [%& typ.instance state.instance]
53337282 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
5334− ?~ 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]
53357289 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
53367290 [%& typ.instance state.instance]
53377291 %group $(e inner.e)
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])]
53387298 %trace
53397299 =/ traced=iresult $(e val.e)
53407300 ?: ?=(%| -.traced) traced
@@ -5361,17 +7321,26 @@
53617321 %branch
53627322 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
53637323 ?~ t.arms.e (infer-cell-branch e env state)
5364− ?^ 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)
53657328 =/ x=arm i.arms.e
53667329 =/ y=arm i.t.arms.e
5367− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
5368− ?. ?=(%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)
53697334 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
5370− [%| ["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)
53717337 ?: =(val.lit.pat.x val.lit.pat.y)
53727338 [%| ["branch does not cover both loobeans" ~]]
53737339 =/ subject=iresult $(e subject.e)
53747340 ?: ?=(%| -.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" ~]]
53757344 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
53767345 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
53777346 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -5384,41 +7353,69 @@
53847353 [%| ["branch widening is not supported by partial inference" ~]]
53857354 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
53867355 ?~ joined
7356+ ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
7357+ [%| ["recursive branch matching is not supported by partial inference" ~]]
7358+ ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
7359+ [%| ["branch tag or union context is not supported by partial inference" ~]]
53877360 =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
53887361 ?^ common [%& u.common state.p.right]
7362+ ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))
7363+ [%| ["record branch matching is not supported by partial inference" ~]]
53897364 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
53907365 [%| ["branch widening is not supported by partial inference" ~]]
53917366 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
53927367 [%& typ.p.left state.p.right(sub u.joined)]
53937368 %cast
53947369 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
5395− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
5396− =/ value=iresult $(e val.e, state state.u.target)
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" ~]]
7374+ =/ value=iresult
7375+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
53977376 ?: ?=(%| -.value) value
53987377 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
53997378 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
54007379 ?: ?=(%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]
54017384 [%| ["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)]]]]
5402− [%& typ.u.target state.p.value(sub sub.fit, next next.fit)]
7385+ =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
7386+ [%& merged state.p.value(sub sub.fit, next next.fit)]
54037387 %crash [%& [%var next.state] state(next +(next.state))]
54047388 %gate
54057389 =/ sam=isample-result (infer-sample sample.e env state)
5406− ?: ?=(%| -.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 ~]]
54077394 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
54087395 ?: ?=(%| -.body) body
54097396 [%& [%fn typ.p.sam typ.p.body] state.p.body]
54107397 %gate-wide
54117398 =/ sam=isample-result (infer-sample sample.e env state)
5412− ?: ?=(%| -.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 ~]]
54137403 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
54147404 ?: ?=(%| -.body) body
54157405 [%& [%fn typ.p.sam typ.p.body] state.p.body]
54167406 %call
54177407 ?~ args.e [%| ["call has no argument" ~]]
5418− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
54197408 =/ head=iresult $(e head.e)
54207409 ?: ?=(%| -.head) head
5421− =/ arg=iresult $(e i.args.e, state state.p.head)
7410+ =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
7411+ =/ arg=iresult
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))
7418+ $(e i.args.e, state state.p.head)
54227419 ?: ?=(%| -.arg) arg
54237420 =/ st=istate state.p.arg
54247421 =/ ht=itype (itype-walk typ.p.head sub.st)
@@ -5426,7 +7423,21 @@
54267423 =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
54277424 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
54287425 ?: ?=(%bad -.fit)
5429− [%| ["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)]]]]
7439+ ?: &((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))
7440+ [%| ["call result face propagation is not supported by partial inference" ~]]
54307441 [%& product.ht st(sub sub.fit, next next.fit)]
54317442 =/ result=itype [%var next.st]
54327443 =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
@@ -5436,23 +7447,194 @@
54367447 * [%| ["expression is not supported by partial inference" ~]]
54377448 ==
54387449::
5439−:: Unfaced tuple expressions are the one supported cell construction.
5440−:: Faced cells wait for the representation to preserve record faces.
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+::
7586+:: Tuple and record expressions preserve their explicitly written faces.
54417587::
54427588++ infer-simple-items
54437589 |= [items=(list item) env=ienv state=istate]
54447590 ^- iresult
54457591 ?~ items [%| ["empty cell is not supported by partial inference" ~]]
5446− ?^ face.i.items [%| ["record faces are not supported by partial inference" ~]]
54477592 =/ head=iresult (infer-fragment val.i.items env state)
54487593 ?: ?=(%| -.head) head
5449− ?~ t.items head
7594+ =/ ht=itype typ.p.head
7595+ =. ht ?~(face.i.items ht [%face u.face.i.items ht])
7596+ ?~ t.items [%& ht state.p.head]
54507597 =/ tail=iresult $(items t.items, state state.p.head)
54517598 ?: ?=(%| -.tail) tail
5452− [%& [%cell typ.p.head typ.p.tail] state.p.tail]
5453−::
5454−:: A single two-binder cell pattern covers every value of a cell type.
5455−:: No other pattern matrix is implemented here.
7599+ [%& [%cell ht typ.p.tail] state.p.tail]
7600+::
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))
54567638::
54577639++ infer-cell-branch
54587640 |= [e=expr env=ienv state=istate]
@@ -5464,21 +7646,22 @@
54647646 =/ pats=(list pattern) items.pat.arm
54657647 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
54667648 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
5467− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
5468− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
5469− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
5470− =/ one=term name.i.pats
5471− =/ two=term name.i.t.pats
5472− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
5473− [%| ["pattern shadows a name" ~]]
7649+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
7650+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
54747651 =/ subject=iresult (infer-fragment subject.e env state)
54757652 ?: ?=(%| -.subject) subject
54767653 =/ st=istate state.p.subject
5477− =/ head=itype [%var next.st]
5478− =/ tail=itype [%var +(next.st)]
5479− =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
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" ~]]
7657+ ?: (itype-has-face typ.p.subject sub.st)
7658+ [%| ["record patterns are not supported by partial inference" ~]]
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)
54807663 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
5481− (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))
54827665::
54837666++ show-itype
54847667 |= [t=itype sub=isub]
@@ -5497,10 +7680,41 @@
54977680 %atom "@{(trip aura.t)}"
54987681 %any-atom "@"
54997682 %flag "?"
5500− %fn "$-({$(t sample.t)} {$(t product.t)})"
5501− %cell "[{$(t hed.t)} {$(t tal.t)}]"
7683+ %noun "*"
7684+ %tag (trip txt.literal.t)
7685+ %const (trip txt.literal.t)
7686+ %union
7687+ ?~ label.t (show-itype-cases cases.t sub)
7688+ ?~ args.t (trip u.label.t)
7689+ "({(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)})"
7692+ %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
7693+ %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
7694+ %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
55027695 ==
55037696::
7697+++ show-itype-item
7698+ |= [t=itype sub=isub]
7699+ ^- tape
7700+ =. t (itype-walk t sub)
7701+ ?: ?=(%face -.t) "{(trip name.t)}={(show-itype-context body.t sub)}"
7702+ (show-itype-context t sub)
7703+::
7704+++ show-itype-context
7705+ |= [t=itype sub=isub]
7706+ ^- tape
7707+ =. t (itype-walk t sub)
7708+ ?: &(?=(%union -.t) ?=(~ label.t)) "({(show-itype t sub)})"
7709+ (show-itype t sub)
7710+::
7711+++ show-itype-cases
7712+ |= [cases=(list itype) sub=isub]
7713+ ^- tape
7714+ ?~ cases ""
7715+ ?~ t.cases (show-itype-context i.cases sub)
7716+ "{(show-itype-context i.cases sub)} {$(cases t.cases)}"
7717+::
55047718:: Include the type at a conflicting site where it can be printed.
55057719:: A lone unresolved variable or decimal variable keeps the neutral label.
55067720::
@@ -5514,6 +7728,13 @@
55147728 %atom |
55157729 %any-atom |
55167730 %flag |
7731+ %noun |
7732+ %tag |
7733+ %const |
7734+ %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)))
7737+ %face $(typ body.typ)
55177738 %fn |($(typ sample.typ) $(typ product.typ))
55187739 %cell |($(typ hed.typ) $(typ tal.typ))
55197740 ==
@@ -5522,7 +7743,8 @@
55227743 |= [label=tape typ=itype sub=isub]
55237744 ^- tape
55247745 =/ normalized=itype (itype-normalize typ sub)
5525− ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized)) label
7746+ ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
7747+ ?: (itype-has-hidden-recursive normalized) label
55267748 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
55277749 ?: (gth (lent vars) 26) label
55287750 =/ printable=itype (canonical-itype normalized vars)
@@ -5531,13 +7753,64 @@
55317753:: A capital in a written mold is generalized with its enclosing ++.
55327754:: Atom constraints may remain generic; until full rigidity checking
55337755:: is implemented, do not report a type if one became more specific.
7756+:: Distinct written capitals cannot be forced equal; use the same
7757+:: capital where a type must be shared (Decisions 2026-10-30).
7758+::
7759+++ cap-id-in
7760+ |= [n=@ud caps=icaps sub=isub]
7761+ ^- ?
7762+ ?~ caps |
7763+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7764+ =/ ident=(unit @ud)
7765+ ?+ -.resolved ~
7766+ %var `id.resolved
7767+ %avar `id.resolved
7768+ ==
7769+ ?~ ident $(caps t.caps)
7770+ ?: =(n u.ident) &
7771+ $(caps t.caps)
7772+::
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)
55347801::
55357802++ constrained-capitals
55367803 |= [caps=icaps sub=isub]
55377804 ^- ?
55387805 ?~ caps |
55397806 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
5540− ?. |(?=(%var -.resolved) ?=(%avar -.resolved)) &
7807+ =/ ident=(unit @ud)
7808+ ?+ -.resolved ~
7809+ %var `id.resolved
7810+ %avar `id.resolved
7811+ ==
7812+ ?~ ident &
7813+ ?: (cap-id-in u.ident t.caps sub) &
55417814 $(caps t.caps)
55427815::
55437816:: An atom variable may be generalized when an explicit capital, sample
@@ -5564,6 +7837,13 @@
55647837 %atom |
55657838 %any-atom |
55667839 %flag |
7840+ %noun |
7841+ %tag |
7842+ %const |
7843+ %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)))
7846+ %face $(t body.t)
55677847 %fn |($(t sample.t) $(t product.t))
55687848 %cell |($(t hed.t) $(t tal.t))
55697849 ==
@@ -5609,9 +7889,9 @@
56097889::
56107890:: Build the supported part of the value environment in dependency order.
56117891:: Each pass adds successful definitions. Forward references become
5612−:: available on a later pass; recursive groups and unsupported syntax do
5613−:: not enter the environment. Generalized definitions are closed, so a
5614−:: 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.
56157895::
56167896++ global-value-names
56177897 |= ds=(list def)
@@ -5629,31 +7909,587 @@
56297909 ?~ t.hits &
56307910 |
56317911::
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+::
56328223++ add-supported-defs
5633− |= [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)]
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)]
56348225 ^- ienv
56358226 ?~ ds env
56368227 =/ d=def i.ds
56378228 ?: ?=(%mold -.d) $(ds t.ds)
56388229 ?. (unique-value-name name.d globals) $(ds t.ds)
56398230 ?^ (ienv-lookup name.d env) $(ds t.ds)
5640− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ |])
8231+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
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)
56418236 ?: ?=(%| -.result) $(ds t.ds)
56428237 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
56438238 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
8239+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
56448240 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
56458241 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
56468242 ?: (gth (lent vars) 26) $(ds t.ds)
56478243 $(ds t.ds, env [[name.d [typ vars]] env])
56488244::
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+::
56498372++ resolve-supported-defs
5650− |= [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)]
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)]
56518374 ^- ienv
5652− =/ 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) ~
56538484 |-
5654− =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds)
5655− ?: =(next env) env
5656− $(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))
56578493::
56588494+| %union-analysis
56598495::
@@ -5846,8 +8682,9 @@
58468682::
58478683+$ jsource [at=path source=@t]
58488684+$ jbundle (list jsource)
5849−+$ jfile-result (each ifile @t)
5850−+$ jimports-result (each ijimports @t)
8685++$ jcache (list [at=path iface=ifile])
8686++$ jfile-result (each [iface=ifile cache=jcache] @t)
8687++$ jimports-result (each [resolved=ijimports cache=jcache] @t)
58518688::
58528689++ import-binding-names
58538690 |= imports=(list import)
@@ -5875,18 +8712,175 @@
58758712 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
58768713 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
58778714::
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+::
58788731++ module-mold-types
58798732 |= [molds=imolds state=istate]
58808733 ^- (each imold-types @t)
58818734 ?~ molds [%& ~]
58828735 =/ m=[name=term body=shape] i.molds
5883− =/ t=(unit [typ=itype state=istate])
5884− (infer-simple-shape body.m state(active [name.m active.state], in-mold &))
8736+ =/ t=(unit [template=ischeme state=istate])
8737+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
58858738 ?~ t [%| 'module mold needs unsupported inference']
5886− ?: ?=(^ (itype-vars typ.u.t)) [%| 'module mold has unsupported variables']
8739+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
58878740 =/ rest=(each imold-types @t) $(molds t.molds)
58888741 ?: ?=(%| -.rest) rest
5889− [%& [[name.m typ.u.t] p.rest]]
8742+ [%& [[name.m template.u.t] p.rest]]
8743+::
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]
58908884::
58918885++ module-values-complete
58928886 |= [ds=(list def) env=ienv]
@@ -5896,48 +8890,329 @@
58968890 ?~ (ienv-lookup name.i.ds env) |
58978891 $(ds t.ds)
58988892::
8893+:: Cache only completed interfaces for this invocation. The source bundle,
8894+:: imported Hoon types and prelude are fixed for the whole graph. Check the
8895+:: active path and duplicate sources before consulting it, so a cache hit
8896+:: cannot hide a cycle or ambiguous source.
8897+::
8898+++ find-jibb-cache
8899+ |= [at=path cache=jcache]
8900+ ^- (unit ifile)
8901+ ?~ cache ~
8902+ ?: =(at at.i.cache) `iface.i.cache
8903+ $(cache t.cache)
8904+::
58998905++ resolve-jibb-imports
5900− |= [imports=(list import) externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term)]
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)]
59018907 ^- jimports-result
5902− ?~ imports [%& ~]
8908+ ?~ imports [%& [~ cache]]
59038909 ?. ?=(%jibb -.i.imports) $(imports t.imports)
59048910 =/ at=path (weld path.i.imports `path`~[%jibb])
8911+ ?: =(at /lib/jibb/internal/jibb)
8912+ [%| 'the prelude internal module is private']
59058913 ?: (lien active |=(p=path =(p at)))
59068914 [%| (crip "import cycle at {(spud at)}")]
59078915 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
59088916 ?~ found [%| (crip "module source missing: {(spud at)}")]
59098917 ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
5910− =/ iface=jfile-result (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds)
8918+ =/ cached=(unit ifile) (find-jibb-cache at cache)
8919+ =/ iface=jfile-result
8920+ ?^ cached [%& [u.cached cache]]
8921+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
59118922 ?: ?=(%| -.iface) [%| p.iface]
5912− =/ rest=jimports-result $(imports t.imports)
8923+ =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
59138924 ?: ?=(%| -.rest) rest
5914− [%& [[face.i.imports p.iface] p.rest]]
8925+ [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
8926+::
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]]]
59159183::
59169184++ infer-jibb-file
5917− |= [at=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle active=(list path) prelude-values=(list term) prelude-molds=(list term)]
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)]
59189186 ^- jfile-result
5919− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
59209187 =/ parsed (parse at src)
59219188 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
59229189 =/ mod=module p.parsed
5923− ?. (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)}")]
59249198 =/ vals=(list term) (global-value-names defs.mod)
59259199 ?: (lien vals |=(n=term =(n %main)))
59269200 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
5927− =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds)
9201+ =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
59289202 ?: ?=(%| -.js) [%| p.js]
59299203 =/ molds=imolds (collect-simple-molds defs.mod)
59309204 =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
59319205 =/ surs=(list term) (collect-sur-imports imports.mod)
59329206 =/ marks=(list term) (collect-mark-imports imports.mod)
5933− =/ reserved=(list term) (weld prelude-molds (turn p.js |=(j=[face=term interface=ifile] face.j)))
5934− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks p.js reserved ~ |]
9207+ =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
9208+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9209+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
59359210 =/ mts=(each imold-types @t) (module-mold-types molds state)
59369211 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
5937− =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks p.js reserved)
9212+ =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
59389213 ?. (module-values-complete defs.mod env)
59399214 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
5940− [%& [env p.mts]]
9215+ [%& [[env p.mts at ~] [[at [env p.mts at ~]] cache.p.js]]]
59419216::
59429217:: +golden-types-with-modules fails closed for imports without prelude
59439218:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -5952,8 +9227,10 @@
59529227 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
59539228 (golden-types-with-marks file src externals mark-externals)
59549229::
5955−:: The caller supplies the actual prelude source. Its current names are
5956−:: 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.
59579234::
59589235++ golden-types-with-prelude
59599236 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
@@ -5963,29 +9240,64 @@
59639240 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
59649241 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
59659242 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
5966− =/ prelude-values=(list term) (global-value-names defs.p.prelude)
5967− =/ prelude-molds=(list term)
5968− (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
59699262 ?. (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'
59709265 'partial inference; module not checked\0amodule has conflicting names'
59719266 =/ js=jimports-result
5972− (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)
59739268 ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
59749269 =/ scope-values=(list term)
59759270 (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
5976− (golden-types-in-context file src externals mark-externals p.js scope-values prelude-molds)
9271+ (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
59779272::
59789273:: +golden-types-with-marks: supply declared mark types separately from /sur
59799274:: entries, as [mark result] with the result from +read-mark:jibb-import.
59809275:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
59819276::
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+::
59829294++ golden-types-with-marks
59839295 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
59849296 ^- @t
5985− (golden-types-in-context file src externals mark-externals ~ ~ ~)
9297+ (golden-types-in-context file src externals mark-externals ~ ~ ~ ~)
59869298::
59879299++ golden-types-in-context
5988− |= [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)]
59899301 ^- @t
59909302 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
59919303 =/ parsed (parse file src)
@@ -5995,7 +9307,9 @@
59959307 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
59969308 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
59979309 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
5998− =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds)
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
59999313 =/ lines=(list @t) ~
60009314 |-
60019315 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -6004,12 +9318,42 @@
60049318 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
60059319 ?. (unique-value-name name.d globals)
60069320 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
6007− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ |])
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])
9331+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
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)
60089338 ?: ?=(%| -.result)
60099339 $(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])
60109346 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
60119347 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
60129348 =/ 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])
9351+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
9352+ $(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])
9355+ ?: (itype-has-hidden-generic typ)
9356+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
60139357 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
60149358 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
60159359 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))