@@ -4590,22 +4590,36 @@
45904590:: Each top-level inferred definition generalizes its free variables, and
45914591:: a use instantiates them afresh. Binders inside a gate stay monomorphic;
45924592:: capital variables in molds share one allocation within the definition.
4593−:: Decimal literals have atom-only variables; until their constraints
4594−:: can be printed and generalized, an unresolved one is unsupported.
4595−:: Bare @ is unsupported until its unrestricted-atom rule is implemented.
4596−:: Only unfaced cells are represented here.
4593+:: Atom constraints tied to an explicit capital or an inferred sample
4594+:: are generalized and printed. Other aura variables remain unsupported until
4595+:: their defaulting and inferred generalization are implemented.
4596+:: Bare @ is a separate unrestricted atom type. A directional fit check
4597+:: permits concrete atoms to widen to it, never the reverse. A fit that
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.
45974602::
45984603+$ itype
45994604 $~ [%var 0]
46004605 $% [%var id=@ud]
46014606 [%avar id=@ud]
4607+ [%nvar id=@ud]
46024608 [%atom aura=@ta]
4609+ [%any-atom ~]
46034610 [%flag ~]
4611+ [%tag id=@ud literal=lit constructor=?]
4612+ [%const literal=lit]
4613+ [%collection name=term args=(list itype)]
4614+ [%recursive module=term name=term label=(unit @t)]
4615+ [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
4616+ [%face name=term body=itype]
46044617 [%fn sample=itype product=itype]
46054618 [%cell hed=itype tal=itype]
46064619 ==
46074620+$ ibinding [id=@ud val=itype]
46084621+$ isub (list ibinding)
4622++$ ipending [id=@ud literal=lit]
46094623::
46104624++ itype-lookup
46114625 |= [n=@ud sub=isub]
@@ -4626,6 +4640,14 @@
46264640 =/ found=(unit itype) (itype-lookup id.t sub)
46274641 ?~ found t
46284642 $(t u.found)
4643+ %nvar
4644+ =/ found=(unit itype) (itype-lookup id.t sub)
4645+ ?~ found t
4646+ $(t u.found)
4647+ %tag
4648+ =/ found=(unit itype) (itype-lookup id.t sub)
4649+ ?~ found t
4650+ $(t u.found)
46294651 ==
46304652::
46314653++ itype-occurs
@@ -4635,8 +4657,16 @@
46354657 ?- -.t
46364658 %var =(n id.t)
46374659 %avar =(n id.t)
4660+ %nvar =(n id.t)
46384661 %atom |
4662+ %any-atom |
46394663 %flag |
4664+ %tag =(n id.t)
4665+ %const |
4666+ %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
4667+ %recursive |
4668+ %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
4669+ %face $(t body.t)
46404670 %fn |($(t sample.t) $(t product.t))
46414671 %cell |($(t hed.t) $(t tal.t))
46424672 ==
@@ -4653,19 +4683,44 @@
46534683 =. a (itype-walk a sub)
46544684 =. b (itype-walk b sub)
46554685 ?: =(a b) `sub
4686+ ?: &(?=(%recursive -.a) ?=(%recursive -.b))
4687+ ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
4688+ ?: &(?=(%union -.a) ?=(%union -.b))
4689+ ?. =(origin.a origin.b) ~
4690+ ?: &(?=(~ args.a) ?=(~ args.b)) ?:(=(cases.a cases.b) `sub ~)
4691+ ?~ origin.a ~
4692+ (itype-unify-args args.a args.b sub)
4693+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4694+ ?. =(name.a name.b) ~
4695+ (itype-unify-args args.a args.b sub)
46564696 ?: ?=(%var -.a)
46574697 ?: (itype-occurs id.a b sub) ~
46584698 `[[id.a b] sub]
46594699 ?: ?=(%var -.b)
46604700 ?: (itype-occurs id.b a sub) ~
46614701 `[[id.b a] sub]
4702+ :: The narrower decimal constraint survives a match with an atom
4703+ :: variable; decimal syntax alone does not make it a loobean.
4704+ ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4705+ ?: &(?=(%avar -.a) ?=(%nvar -.b)) `[[id.a b] sub]
4706+ ?: ?=(%nvar -.a)
4707+ ?. |(?=(%nvar -.b) ?=(%atom -.b)) ~
4708+ `[[id.a b] sub]
4709+ ?: ?=(%nvar -.b)
4710+ ?. ?=(%atom -.a) ~
4711+ `[[id.b a] sub]
46624712 ?: ?=(%avar -.a)
4663− ?. |(?=(%avar -.b) ?=(%atom -.b)) ~
4713+ ?. |(?=(%avar -.b) ?=(%atom -.b) ?=(%any-atom -.b) ?=(%flag -.b)) ~
46644714 `[[id.a b] sub]
46654715 ?: ?=(%avar -.b)
4666− ?. ?=(%atom -.a) ~
4716+ ?. |(?=(%atom -.a) ?=(%any-atom -.a) ?=(%flag -.a)) ~
46674717 `[[id.b a] sub]
4718+ ?: &(?=(%const -.a) ?=(%const -.b))
4719+ ?:(=(val.literal.a val.literal.b) `sub ~)
46684720 ?: &(?=(%atom -.a) ?=(%atom -.b)) ~
4721+ ?: &(?=(%face -.a) ?=(%face -.b))
4722+ ?. =(name.a name.b) ~
4723+ $(a body.a, b body.b)
46694724 ?: &(?=(%fn -.a) ?=(%fn -.b))
46704725 =/ first=(unit isub) $(a sample.a, b sample.b)
46714726 ?~ first ~
@@ -4676,6 +4731,453 @@
46764731 $(a tal.a, b tal.b, sub u.first)
46774732 ~
46784733::
4734+++ itype-unify-args
4735+ |= [as=(list itype) bs=(list itype) sub=isub]
4736+ ^- (unit isub)
4737+ ?~ as ?~(bs `sub ~)
4738+ ?~ bs ~
4739+ =/ next=(unit isub) (itype-unify i.as i.bs sub)
4740+ ?~ next ~
4741+ $(as t.as, bs t.bs, sub u.next)
4742+::
4743+:: +itype-fit: one-way widening from an actual type to an expected type
4744+::
4745+:: An unknown variable used where @ is expected gains a fresh atom
4746+:: constraint. Function compatibility involving @ remains unknown.
4747+::
4748++$ ifit $%([%ok sub=isub next=@ud] [%bad ~] [%unknown ~])
4749+++ itype-has-any-atom
4750+ |= [t=itype sub=isub]
4751+ ^- ?
4752+ =. t (itype-walk t sub)
4753+ ?- -.t
4754+ %var |
4755+ %avar |
4756+ %nvar |
4757+ %atom |
4758+ %any-atom &
4759+ %flag |
4760+ %tag |
4761+ %const |
4762+ %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
4763+ %recursive |
4764+ %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
4765+ %face $(t body.t)
4766+ %fn |($(t sample.t) $(t product.t))
4767+ %cell |($(t hed.t) $(t tal.t))
4768+ ==
4769+::
4770+::
4771+:: Hoon aura families are textual prefixes: @tD is in @t, and @uvJ
4772+:: is in @uv and @u. Jibb permits widening toward the prefix only.
4773+::
4774+++ aura-prefix
4775+ |= [parent=@ta child=@ta]
4776+ ^- ?
4777+ =/ a=tape (trip parent)
4778+ =/ b=tape (trip child)
4779+ |-
4780+ ?~ a &
4781+ ?~ b |
4782+ ?. =(i.a i.b) |
4783+ $(a t.a, b t.b)
4784+::
4785+:: Related auras in a structural unification need a common-type rule;
4786+:: until that rule is implemented, report an unknown rather than error.
4787+::
4788+++ itype-family-related-collection-args
4789+ |= [as=(list itype) bs=(list itype) sub=isub]
4790+ ^- ?
4791+ ?~ as |
4792+ ?~ bs |
4793+ ?: (itype-family-related i.as i.bs sub) &
4794+ $(as t.as, bs t.bs)
4795+::
4796+++ itype-family-related
4797+ |= [a=itype b=itype sub=isub]
4798+ ^- ?
4799+ =. a (itype-walk a sub)
4800+ =. b (itype-walk b sub)
4801+ ?: &(?=(%atom -.a) ?=(%atom -.b))
4802+ ?. !=(aura.a aura.b) |
4803+ |((aura-prefix aura.a aura.b) (aura-prefix aura.b aura.a))
4804+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4805+ ?. =(name.a name.b) |
4806+ (itype-family-related-collection-args args.a args.b sub)
4807+ ?: &(?=(%face -.a) ?=(%face -.b))
4808+ ?. =(name.a name.b) |
4809+ $(a body.a, b body.b)
4810+ ?: &(?=(%cell -.a) ?=(%cell -.b))
4811+ |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4812+ ?: &(?=(%fn -.a) ?=(%fn -.b))
4813+ |($(a sample.a, b sample.b) $(a product.a, b product.b))
4814+ |
4815+::
4816+:: A branch whose two result types are already concrete can use an
4817+:: explicitly present parent aura (or @) as its result. This does not
4818+:: guess a parent for sibling auras or solve variable-dependent joins.
4819+::
4820+++ itype-has-fixed-atom
4821+ |= typ=itype
4822+ ^- ?
4823+ ?- -.typ
4824+ %var |
4825+ %avar |
4826+ %nvar |
4827+ %atom &
4828+ %any-atom &
4829+ %flag &
4830+ %tag &
4831+ %const &
4832+ %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
4833+ %recursive |
4834+ %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
4835+ %face $(typ body.typ)
4836+ %fn |($(typ sample.typ) $(typ product.typ))
4837+ %cell |($(typ hed.typ) $(typ tal.typ))
4838+ ==
4839+::
4840+++ itype-concrete-join
4841+ |= [a=itype b=itype sub=isub]
4842+ ^- (unit itype)
4843+ =. a (itype-walk a sub)
4844+ =. b (itype-walk b sub)
4845+ ?: &(?=(%atom -.a) ?=(%atom -.b))
4846+ ?: (aura-prefix aura.a aura.b) `a
4847+ ?: (aura-prefix aura.b aura.a) `b
4848+ ~
4849+ ?: &(?=(%any-atom -.a) |(?=(%atom -.b) ?=(%flag -.b))) `a
4850+ ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b
4851+ ~
4852+::
4853+:: Unifying an already-bound tuple with a faced position would need to
4854+:: update the bound type. Until substitutions can retain that information,
4855+:: variable-dependent face merges stay unresolved.
4856+::
4857+++ itype-has-face
4858+ |= [t=itype sub=isub]
4859+ ^- ?
4860+ =. t (itype-walk t sub)
4861+ ?- -.t
4862+ %collection (lien args.t |=(c=itype (itype-has-face c sub)))
4863+ %face &
4864+ %cell |($(t hed.t) $(t tal.t))
4865+ %fn |($(t sample.t) $(t product.t))
4866+ * |
4867+ ==
4868+::
4869+++ itype-face-asym-collection-args
4870+ |= [as=(list itype) bs=(list itype) sub=isub]
4871+ ^- ?
4872+ ?~ as |
4873+ ?~ bs |
4874+ ?: (itype-face-asym i.as i.bs sub) &
4875+ $(as t.as, bs t.bs)
4876+::
4877+++ itype-face-asym
4878+ |= [a=itype b=itype sub=isub]
4879+ ^- ?
4880+ =. a (itype-walk a sub)
4881+ =. b (itype-walk b sub)
4882+ ?: &(?=(%collection -.a) ?=(%collection -.b))
4883+ ?. =(name.a name.b) |
4884+ (itype-face-asym-collection-args args.a args.b sub)
4885+ ?: &(?=(%face -.a) ?=(%face -.b)) $(a body.a, b body.b)
4886+ ?: ?=(%face -.a) !|(?=(%var -.b) ?=(%avar -.b) ?=(%nvar -.b))
4887+ ?: ?=(%face -.b) !|(?=(%var -.a) ?=(%avar -.a) ?=(%nvar -.a))
4888+ ?: &(?=(%cell -.a) ?=(%cell -.b)) |($(a hed.a, b hed.b) $(a tal.a, b tal.b))
4889+ ?: &(?=(%fn -.a) ?=(%fn -.b)) |($(a sample.a, b sample.b) $(a product.a, b product.b))
4890+ |
4891+::
4892+:: A successful cast keeps any explicit faces from either side while
4893+:: retaining the target's aura choices. Both faces have already matched.
4894+::
4895+++ itype-merge-faces
4896+ |= [actual=itype expected=itype sub=isub]
4897+ ^- itype
4898+ =. actual (itype-walk actual sub)
4899+ =. expected (itype-walk expected sub)
4900+ ?: &(?=(%face -.actual) ?=(%face -.expected))
4901+ [%face name.expected $(actual body.actual, expected body.expected)]
4902+ ?: ?=(%face -.actual)
4903+ [%face name.actual $(actual body.actual)]
4904+ ?: ?=(%face -.expected)
4905+ [%face name.expected $(expected body.expected)]
4906+ ?: &(?=(%cell -.actual) ?=(%cell -.expected))
4907+ [%cell $(actual hed.actual, expected hed.expected) $(actual tal.actual, expected tal.expected)]
4908+ expected
4909+::
4910+++ itype-output-may-be-cell
4911+ |= [t=itype sub=isub]
4912+ ^- ?
4913+ =. t (itype-walk t sub)
4914+ ?- -.t
4915+ %var &
4916+ %cell &
4917+ %union &
4918+ %recursive &
4919+ %collection &
4920+ %face $(t body.t)
4921+ %fn |($(t sample.t) $(t product.t))
4922+ * |
4923+ ==
4924+::
4925+++ pending-tags
4926+ |= [tags=(list ipending) sub=isub]
4927+ ^- ?
4928+ ?~ tags |
4929+ ?~ (itype-lookup id.i.tags sub) &
4930+ $(tags t.tags)
4931+::
4932+++ pending-null
4933+ |= [tags=(list ipending) sub=isub]
4934+ ^- ?
4935+ ?~ tags |
4936+ ?: &(?=(%null form.literal.i.tags) ?=(~ (itype-lookup id.i.tags sub))) &
4937+ $(tags t.tags)
4938+::
4939+:: Tags remain constrained until a mold selects a case or permitted atom
4940+:: type. Never generalize an unresolved tag through aliases or cells.
4941+::
4942+++ itype-has-tag
4943+ |= t=itype
4944+ ^- ?
4945+ ?- -.t
4946+ %tag &
4947+ %collection (lien args.t |=(c=itype (itype-has-tag c)))
4948+ %face $(t body.t)
4949+ %fn |($(t sample.t) $(t product.t))
4950+ %cell |($(t hed.t) $(t tal.t))
4951+ %union |((lien cases.t |=(c=itype (itype-has-tag c))) (lien args.t |=(c=itype (itype-has-tag c))))
4952+ * |
4953+ ==
4954+::
4955+++ itype-has-union
4956+ |= t=itype
4957+ ^- ?
4958+ ?- -.t
4959+ %union &
4960+ %collection (lien args.t |=(c=itype (itype-has-union c)))
4961+ %face $(t body.t)
4962+ %fn |($(t sample.t) $(t product.t))
4963+ %cell |($(t hed.t) $(t tal.t))
4964+ * |
4965+ ==
4966+::
4967+:: Until a visible generic alias can be selected, expanding a named
4968+:: generic union would hide phantom arguments and its origin. This is a
4969+:: limitation of partial inference, not the unnamed-union print notation.
4970+::
4971+++ itype-has-hidden-generic
4972+ |= t=itype
4973+ ^- ?
4974+ ?- -.t
4975+ %union
4976+ ?: &(?=(~ label.t) ?=(^ args.t)) &
4977+ (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-generic c)))
4978+ %collection (lien args.t |=(c=itype (itype-has-hidden-generic c)))
4979+ %face $(t body.t)
4980+ %fn |($(t sample.t) $(t product.t))
4981+ %cell |($(t hed.t) $(t tal.t))
4982+ * |
4983+ ==
4984+::
4985+++ itype-has-recursive
4986+ |= t=itype
4987+ ^- ?
4988+ ?- -.t
4989+ %recursive &
4990+ %collection (lien args.t |=(c=itype (itype-has-recursive c)))
4991+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
4992+ %face $(t body.t)
4993+ %cell |($(t hed.t) $(t tal.t))
4994+ %fn |($(t sample.t) $(t product.t))
4995+ * |
4996+ ==
4997+::
4998+++ itype-has-hidden-recursive
4999+ |= t=itype
5000+ ^- ?
5001+ ?- -.t
5002+ %recursive ?=(~ label.t)
5003+ %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
5004+ %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
5005+ %face $(t body.t)
5006+ %cell |($(t hed.t) $(t tal.t))
5007+ %fn |($(t sample.t) $(t product.t))
5008+ * |
5009+ ==
5010+::
5011+++ itype-fit-cases
5012+ |= [actual=itype cases=(list itype) sub=isub next=@ud]
5013+ ^- ifit
5014+ =/ good=(unit ifit) ~
5015+ =/ pending=? |
5016+ |-
5017+ ?~ cases
5018+ ?: pending [%unknown ~]
5019+ ?~ good [%bad ~]
5020+ u.good
5021+ =/ trial=ifit (itype-fit actual i.cases sub next)
5022+ ?- -.trial
5023+ %unknown $(cases t.cases, pending &)
5024+ %bad $(cases t.cases)
5025+ %ok
5026+ ?^ good [%unknown ~]
5027+ $(cases t.cases, good `trial)
5028+ ==
5029+::
5030+:: A constructor needs a case with its tag at the head and a payload
5031+:: compatible with the expected gate sample. Other case forms do not
5032+:: identify a constructor.
5033+::
5034+++ itype-fit-ctor-cases
5035+ |= [tag=lit sample=itype cases=(list itype) sub=isub next=@ud]
5036+ ^- ifit
5037+ =/ found=(unit ifit) ~
5038+ |-
5039+ ?~ cases ?~(found [%bad ~] u.found)
5040+ =/ c=itype (itype-walk i.cases sub)
5041+ ?. ?=(%cell -.c) $(cases t.cases)
5042+ =/ head=itype (itype-walk hed.c sub)
5043+ ?. ?=(%const -.head) $(cases t.cases)
5044+ ?. =(%term form.literal.head) $(cases t.cases)
5045+ ?. =(val.literal.head val.tag) $(cases t.cases)
5046+ ?^ found [%unknown ~]
5047+ =/ trial=ifit (itype-fit sample tal.c sub next)
5048+ $(cases t.cases, found `trial)
5049+::
5050+++ itype-fit
5051+ |= [actual=itype expected=itype sub=isub next=@ud]
5052+ ^- ifit
5053+ =/ uncertain=?
5054+ |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5055+ =. actual (itype-walk actual sub)
5056+ =. expected (itype-walk expected sub)
5057+ ?: =(actual expected) [%ok sub next]
5058+ ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
5059+ ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
5060+ ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
5061+ ?: &(?=(%union -.actual) ?=(%union -.expected))
5062+ ?. =(origin.actual origin.expected) [%unknown ~]
5063+ ?: &(?=(~ args.actual) ?=(~ args.expected))
5064+ ?:(=(cases.actual cases.expected) [%ok sub next] [%unknown ~])
5065+ ?~ origin.actual [%unknown ~]
5066+ =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
5067+ ?^ unified [%ok u.unified next]
5068+ [%unknown ~]
5069+ :: A concrete union value in a tuple may acquire the expected field's
5070+ :: face. A variable-bound union still needs face propagation support.
5071+ ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5072+ $(expected body.expected)
5073+ ?: ?=(%union -.actual) [%unknown ~]
5074+ ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
5075+ ?: &(?=(%union -.expected) !?=(%var -.actual))
5076+ (itype-fit-cases actual cases.expected sub next)
5077+ ?: ?=(%tag -.actual)
5078+ ?: ?=(%var -.expected)
5079+ =/ u=(unit isub) (itype-unify actual expected sub)
5080+ ?~ u [%bad ~]
5081+ [%ok u.u next]
5082+ ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5083+ ?: ?=(%face -.expected) $(expected body.expected)
5084+ ?: constructor.actual
5085+ ?. ?=(%fn -.expected) [%bad ~]
5086+ =/ product=itype (itype-walk product.expected sub)
5087+ =/ cases=(list itype) ?:(?=(%union -.product) cases.product ~[product])
5088+ =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
5089+ ?. ?=(%ok -.trial) trial
5090+ [%ok [[id.actual expected] sub.trial] next.trial]
5091+ :: Zero may be the empty list. A nested cell fit lacks the context
5092+ :: needed to resolve it here, so do not report a definite mismatch.
5093+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5094+ [%unknown ~]
5095+ ?: ?=(%const -.expected)
5096+ ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
5097+ ?: ?=(%atom -.expected)
5098+ ?: |(=(%tas aura.expected) =(%ta aura.expected))
5099+ [%ok [[id.actual expected] sub] next]
5100+ [%bad ~]
5101+ ?: ?=(%flag -.expected)
5102+ ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok [[id.actual expected] sub] next] [%bad ~])
5103+ ?: ?=(%any-atom -.expected) [%ok [[id.actual expected] sub] next]
5104+ [%bad ~]
5105+ ?: ?=(%const -.actual)
5106+ ?: ?=(%var -.expected)
5107+ =/ u=(unit isub) (itype-unify actual expected sub)
5108+ ?~ u [%bad ~]
5109+ [%ok u.u next]
5110+ ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5111+ ?: ?=(%face -.expected) $(expected body.expected)
5112+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5113+ [%unknown ~]
5114+ ?: ?=(%const -.expected)
5115+ ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
5116+ ?: ?=(%atom -.expected)
5117+ ?: |(=(%tas aura.expected) =(%ta aura.expected)) [%ok sub next]
5118+ [%bad ~]
5119+ ?: ?=(%flag -.expected)
5120+ ?:(|(=(0 val.literal.actual) =(1 val.literal.actual)) [%ok sub next] [%bad ~])
5121+ ?: ?=(%any-atom -.expected) [%ok sub next]
5122+ [%bad ~]
5123+ ?: &(uncertain (itype-face-asym actual expected sub)) [%unknown ~]
5124+ ?: ?=(%any-atom -.expected)
5125+ ?: |(?=(%atom -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%flag -.actual)) [%ok sub next]
5126+ ?: ?=(%var -.actual)
5127+ =/ unified=(unit isub) (itype-unify actual [%avar next] sub)
5128+ ?~ unified [%bad ~]
5129+ [%ok u.unified +(next)]
5130+ [%bad ~]
5131+ ?: ?=(%any-atom -.actual)
5132+ ?: ?=(%var -.expected)
5133+ =/ unified=(unit isub) (itype-unify actual expected sub)
5134+ ?~ unified [%bad ~]
5135+ [%ok u.unified next]
5136+ ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
5137+ [%bad ~]
5138+ ?: &(?=(%atom -.actual) ?=(%atom -.expected))
5139+ ?: (aura-prefix aura.expected aura.actual) [%ok sub next]
5140+ ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
5141+ [%bad ~]
5142+ ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5143+ =/ first=ifit $(actual hed.actual, expected hed.expected)
5144+ ?. ?=(%ok -.first) first
5145+ $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
5146+ :: A field may add a face to an occurrence of the very same type
5147+ :: variable. Binding that variable to a face around itself would fail
5148+ :: the occurs check, but its underlying type has already matched.
5149+ ?: &(?=(%var -.actual) ?=(%face -.expected) =(actual (itype-walk body.expected sub)))
5150+ [%ok sub next]
5151+ :: Differing variables and faces need propagation that is not yet
5152+ :: represented. Binding one to the face can create a false mismatch.
5153+ ?: &(?=(%var -.actual) ?=(%face -.expected)) [%unknown ~]
5154+ ?: &(?=(%face -.actual) ?=(%var -.expected)) [%unknown ~]
5155+ ?: &(?=(%var -.actual) (itype-has-any-atom expected sub))
5156+ [%unknown ~]
5157+ ?: |(?=(%var -.actual) ?=(%var -.expected))
5158+ =/ unified=(unit isub) (itype-unify actual expected sub)
5159+ ?~ unified
5160+ ?: |(?=(%face -.actual) ?=(%face -.expected)) [%unknown ~]
5161+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
5162+ ?: (itype-family-related actual expected sub) [%unknown ~]
5163+ [%bad ~]
5164+ [%ok u.unified next]
5165+ ?: &(?=(%face -.actual) ?=(%face -.expected))
5166+ ?. =(name.actual name.expected) [%bad ~]
5167+ $(actual body.actual, expected body.expected)
5168+ ?: ?=(%face -.actual) $(actual body.actual)
5169+ ?: ?=(%face -.expected) $(expected body.expected)
5170+ ?: (itype-face-asym actual expected sub) [%unknown ~]
5171+ ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
5172+ [%unknown ~]
5173+ =/ unified=(unit isub) (itype-unify actual expected sub)
5174+ ?~ unified
5175+ ?: |((itype-has-union (itype-normalize actual sub)) (itype-has-union (itype-normalize expected sub))) [%unknown ~]
5176+ ?: |((itype-has-recursive (itype-normalize actual sub)) (itype-has-recursive (itype-normalize expected sub))) [%unknown ~]
5177+ ?: (itype-family-related actual expected sub) [%unknown ~]
5178+ [%bad ~]
5179+ [%ok u.unified next]
5180+::
46795181++ itype-unify-test
46805182 ^- (list tape)
46815183 =/ a=itype [%var 0]
@@ -4700,21 +5202,59 @@
47005202 ["a shared type variable should reject incompatible arguments" problems]
47015203 =? problems ?=(~ (itype-unify same fine ~))
47025204 ["a shared type variable should accept equal arguments" problems]
5205+ =/ list-a=itype [%collection %list ~[a]]
5206+ =/ list-t=itype [%collection %list ~[txt]]
5207+ =/ list-n=itype [%collection %list ~[num]]
5208+ =? problems ?=(^ (itype-unify a list-a ~))
5209+ ["occurs check should look through collection arguments" problems]
5210+ =? problems !=((itype-vars list-a) ~[0])
5211+ ["generalization should see collection argument variables" problems]
5212+ =? problems !=((itype-rename list-a ~[[0 num]]) list-n)
5213+ ["instantiation should rename collection argument variables" problems]
5214+ =? problems ?=(^ (itype-unify list-t list-n ~))
5215+ ["collection arguments with different auras should conflict" problems]
5216+ =? problems ?=(^ (itype-unify list-t [%collection %unit ~[txt]] ~))
5217+ ["different collection names should conflict" problems]
5218+ =? problems !(itype-family-related list-t [%collection %list ~[[%atom 'tD']]] ~)
5219+ ["collection arguments should preserve aura-family uncertainty" problems]
5220+ =? problems !(itype-face-asym [%collection %list ~[[%face %x txt]]] list-t ~)
5221+ ["collection arguments should preserve face uncertainty" problems]
5222+ =/ recursive=itype [%recursive %fixture %chain `'chain.fixture']
5223+ =/ same-recursive=itype [%recursive %fixture %chain ~]
5224+ =/ other-recursive=itype [%recursive %other %chain `'chain.other']
5225+ =? problems ?=(~ (itype-unify recursive same-recursive ~))
5226+ ["recursive identity should not depend on its visible name" problems]
5227+ =? problems ?=(^ (itype-unify recursive other-recursive ~))
5228+ ["recursive identity should include the source module" problems]
5229+ =/ recursive-fit=ifit (itype-fit recursive txt ~ 0)
5230+ =? problems !?=(%unknown -.recursive-fit)
5231+ ["opaque recursive types should not be unfolded by a fit" problems]
5232+ =/ nested-fit=ifit
5233+ (itype-fit [%collection %list ~[a]] list-t ~[[0 recursive]] 1)
5234+ =? problems !?=(%unknown -.nested-fit)
5235+ ["recursive types behind substitutions should remain uncertain" problems]
47035236 problems
47045237::
47055238:: The expression inference below is deliberately a fragment: bindings,
4706−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5239+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
47075240:: result for unsupported syntax is a diagnostic, never a checked module.
47085241::
47095242+$ ischeme [typ=itype vars=(list @ud)]
47105243+$ ienv (list [name=term scheme=ischeme])
4711−+$ icaps (list [name=@t id=@ud])
5244++$ imold-types (list [name=term template=ischeme])
5245++$ ifile [values=ienv molds=imold-types at=path]
5246++$ ijimports (list [face=term interface=ifile])
5247++$ icap [name=@t id=@ud at=span]
5248++$ icaps (list icap)
5249++$ iparams (list [name=@t typ=itype])
47125250+$ imolds (list [name=term body=shape])
47135251:: A caller supplies the exact noun returned by +read-mold:jibb-import.
47145252:: This core has no Ford dependencies; unrecognized payloads fail closed.
47155253+$ iexternals (list [module=term name=term result=*])
4716−+$ istate [next=@ud sub=isub caps=icaps molds=imolds globals=(list term) externals=iexternals surs=(list term) active=(list term) in-mold=?]
4717−+$ iresult (each [typ=itype state=istate] tape)
5254++$ imark-externals (list [mark=term result=*])
5255++$ 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)]
5256++$ idiag [msg=tape sites=(list [at=span note=tape])]
5257++$ iresult (each [typ=itype state=istate] idiag)
47185258+$ isample-result (each [typ=itype env=ienv state=istate] tape)
47195259::
47205260++ ienv-lookup
@@ -4732,20 +5272,70 @@
47325272 |= [t=itype sub=isub]
47335273 ^- itype
47345274 =. t (itype-walk t sub)
5275+ ?: ?=(%collection -.t) [%collection name.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5276+ ?: ?=(%union -.t)
5277+ [%union (turn cases.t |=(c=itype (itype-normalize c sub))) origin.t label.t (turn args.t |=(c=itype (itype-normalize c sub)))]
5278+ ?: ?=(%face -.t)
5279+ [%face name.t $(t body.t)]
47355280 ?: ?=(%fn -.t)
47365281 [%fn $(t sample.t) $(t product.t)]
47375282 ?: ?=(%cell -.t)
47385283 [%cell $(t hed.t) $(t tal.t)]
47395284 t
47405285::
5286+::
5287+:: Default decimal variables only in types with no gates. A gate can
5288+:: generalize an aura from its sample, which requires constraint analysis
5289+:: beyond this fragment; leave those cases unresolved.
5290+::
5291+++ itype-has-gate
5292+ |= t=itype
5293+ ^- ?
5294+ ?- -.t
5295+ %fn &
5296+ %cell |($(t hed.t) $(t tal.t))
5297+ %recursive |
5298+ %collection (lien args.t |=(c=itype (itype-has-gate c)))
5299+ %face $(t body.t)
5300+ %union (lien cases.t |=(c=itype (itype-has-gate c)))
5301+ %tag |
5302+ %const |
5303+ %var |
5304+ %avar |
5305+ %nvar |
5306+ %atom |
5307+ %any-atom |
5308+ %flag |
5309+ ==
5310+::
5311+++ default-decimals
5312+ |= t=itype
5313+ ^- itype
5314+ ?: (itype-has-gate t) t
5315+ ?- -.t
5316+ %nvar [%atom %ud]
5317+ %collection [%collection name.t (turn args.t |=(c=itype (default-decimals c)))]
5318+ %face [%face name.t $(t body.t)]
5319+ %cell [%cell $(t hed.t) $(t tal.t)]
5320+ * t
5321+ ==
5322+::
47415323++ itype-vars
47425324 |= t=itype
47435325 ^- (list @ud)
47445326 ?- -.t
47455327 %var ~[id.t]
47465328 %avar ~[id.t]
5329+ %nvar ~[id.t]
47475330 %atom ~
5331+ %any-atom ~
47485332 %flag ~
5333+ %tag ~
5334+ %const ~
5335+ %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
5336+ %recursive ~
5337+ %collection (zing (turn args.t |=(c=itype (itype-vars c))))
5338+ %face $(t body.t)
47495339 %fn (weld $(t sample.t) $(t product.t))
47505340 %cell (weld $(t hed.t) $(t tal.t))
47515341 ==
@@ -4767,13 +5357,50 @@
47675357 =/ found=(unit itype) (itype-lookup id.t ren)
47685358 ?~ found t
47695359 u.found
4770− %avar t
5360+ %avar
5361+ =/ found=(unit itype) (itype-lookup id.t ren)
5362+ ?~ found t
5363+ u.found
5364+ %nvar
5365+ =/ found=(unit itype) (itype-lookup id.t ren)
5366+ ?~ found t
5367+ u.found
47715368 %atom t
5369+ %any-atom t
47725370 %flag t
5371+ %tag t
5372+ %const t
5373+ %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
5374+ %recursive t
5375+ %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
5376+ %face [%face name.t $(t body.t)]
47735377 %fn [%fn $(t sample.t) $(t product.t)]
47745378 %cell [%cell $(t hed.t) $(t tal.t)]
47755379 ==
47765380::
5381+:: Variable IDs are unique across the two kinds. Inspecting the
5382+:: normalized type preserves the atom constraint when renaming.
5383+::
5384+++ itype-var-is-atom
5385+ |= [n=@ud t=itype]
5386+ ^- ?
5387+ ?- -.t
5388+ %var |
5389+ %avar =(n id.t)
5390+ %nvar =(n id.t)
5391+ %atom |
5392+ %any-atom |
5393+ %flag |
5394+ %tag |
5395+ %const |
5396+ %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
5397+ %recursive |
5398+ %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
5399+ %face $(t body.t)
5400+ %fn |($(t sample.t) $(t product.t))
5401+ %cell |($(t hed.t) $(t tal.t))
5402+ ==
5403+::
47775404:: Canonical numbering makes printed variables independent of the order
47785405:: the unifier happened to allocate intermediates.
47795406::
@@ -4784,7 +5411,8 @@
47845411 =/ n=@ud 0
47855412 |-
47865413 ?~ vars (itype-rename t ren)
4787− $(vars t.vars, ren [[i.vars [%var n]] ren], n +(n))
5414+ =/ replacement=itype ?:((itype-var-is-atom i.vars t) [%avar n] [%var n])
5415+ $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
47885416::
47895417++ instantiate-scheme
47905418 |= [scheme=ischeme state=istate]
@@ -4793,7 +5421,13 @@
47935421 =/ vars=(list @ud) vars.scheme
47945422 |-
47955423 ?~ vars [(itype-rename typ.scheme ren) state]
4796− $(vars t.vars, ren [[i.vars [%var next.state]] ren], state state(next +(next.state)))
5424+ =/ replacement=itype
5425+ ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] [%var next.state])
5426+ :: A generalized atom variable is a valid origin for re-generalizing
5427+ :: an alias, just as a sample binder is.
5428+ =/ st=istate state(next +(next.state))
5429+ =? binders.st ?=(%avar -.replacement) [next.state binders.state]
5430+ $(vars t.vars, ren [[i.vars replacement] ren], state st)
47975431::
47985432++ icap-lookup
47995433 |= [n=@t caps=icaps]
@@ -4823,9 +5457,125 @@
48235457 $(ds t.ds)
48245458::
48255459::
4826−:: The importer owns its algebra. Only successful %atom and %cell nouns
4827−:: in the supported subset are decoded here. In particular a singleton,
4828−:: face, union, collection or recursive reference must not be widened.
5460+:: The caller supplies unchanged results from the source-aware importer.
5461+:: That boundary is trusted for source provenance: a fork alone cannot
5462+:: reveal cases Hoon collapsed before it was constructed. Validate the
5463+:: supplied graph independently, including pairwise disjointness. Fixed
5464+:: atoms, term singletons, cells, faces and proven forks are decoded;
5465+:: unsupported singletons, collections and recursive references fail.
5466+::
5467+++ jibb-face-name
5468+ |= name=@
5469+ ^- ?
5470+ =/ chars=tape (trip (@t name))
5471+ ?~ chars |
5472+ ?. (is-lower i.chars) |
5473+ (levy t.chars |=(c=@tD (in c name-mask)))
5474+::
5475+:: A source-aware reader result is trusted for origin. Validate every
5476+:: supplied branch and keep the recursive mold opaque: unfolding its
5477+:: root while naming only its tail would change its type identity.
5478++$ irec-pattern [pat=upat has=?]
5479+++ rec-pattern
5480+ |= [node=* module=term name=term]
5481+ ^- (unit irec-pattern)
5482+ ?@ node ~
5483+ ?+ -.node ~
5484+ %atom
5485+ ?: ?=([%atom %n [~ @]] node)
5486+ ?. =(0 +>+.node) ~
5487+ `[[%atom `0] |]
5488+ ?: ?=([%atom %tas [~ @]] node)
5489+ =/ value=@ +>+.node
5490+ ?. |(=(value 0) (jibb-face-name value)) ~
5491+ `[[%atom `value] |]
5492+ ?. ?=([%atom @ ~] node) ~
5493+ =/ aura=@ta (@ta +<.node)
5494+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
5495+ `[[%atom ~] |]
5496+ %ref
5497+ ?. ?=([%ref @ @] node) ~
5498+ ?. &(=(module +<.node) =(name +>.node)) ~
5499+ `[[%unknown ~] &]
5500+ %face
5501+ ?. ?=([%face @ *] node) ~
5502+ ?. (jibb-face-name +<.node) ~
5503+ $(node +>.node)
5504+ %cell
5505+ ?. ?=([%cell * *] node) ~
5506+ =/ left $(node +<.node)
5507+ ?~ left ~
5508+ =/ right $(node +>.node)
5509+ ?~ right ~
5510+ `[[%cell pat.u.left pat.u.right] |(has.u.left has.u.right)]
5511+ %fork
5512+ =/ cases (rec-patterns +.node module name)
5513+ ?~ cases ~
5514+ ?~ pats.u.cases ~
5515+ ?~ t.pats.u.cases ~
5516+ ?. (rec-patterns-disjoint pats.u.cases) ~
5517+ `[[%or pats.u.cases] has.u.cases]
5518+ ==
5519+::
5520+++ rec-patterns
5521+ |= [nodes=* module=term name=term]
5522+ ^- (unit [pats=(list upat) has=?])
5523+ ?@ nodes ?:(=(nodes 0) `[~ |] ~)
5524+ =/ first (rec-pattern -.nodes module name)
5525+ ?~ first ~
5526+ =/ rest $(nodes +.nodes)
5527+ ?~ rest ~
5528+ `[[pat.u.first pats.u.rest] |(has.u.first has.u.rest)]
5529+::
5530+++ rec-patterns-disjoint
5531+ |= pats=(list upat)
5532+ ^- ?
5533+ ?~ pats &
5534+ ?. (levy t.pats |=(p=upat =(%disjoint (union-relate i.pats p)))) |
5535+ $(pats t.pats)
5536+::
5537+::
5538+::
5539+:: Repeated faces along an imported record spine fail closed. Hoon's type
5540+:: graph can erase unfaced nested-cell boundaries, so that alone does not
5541+:: prove the original source repeated a name within one record. A faced
5542+:: body and each union alternative have separate scopes. Check recursive
5543+:: roots before making them opaque; unused molds are never inspected.
5544+::
5545+++ imported-faces-valid
5546+ |= node=*
5547+ ^- ?
5548+ ?@ node &
5549+ ?+ -.node &
5550+ %face ?:(?=([%face @ *] node) $(node +>.node) |)
5551+ %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
5552+ %fork (imported-faces-valid-list +.node)
5553+ %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
5554+ ==
5555+::
5556+++ imported-faces-valid-list
5557+ |= nodes=*
5558+ ^- ?
5559+ ?@ nodes =(nodes 0)
5560+ ?. (imported-faces-valid -.nodes) |
5561+ $(nodes +.nodes)
5562+::
5563+++ imported-record-faces-valid
5564+ |= [node=* names=(list @)]
5565+ ^- ?
5566+ ?: ?=([%cell * *] node)
5567+ =/ head=* +<.node
5568+ =/ rest=* +>.node
5569+ ?: ?=([%face @ *] head)
5570+ ?: (lien names |=(n=@ =(n +<.head))) |
5571+ ?. (imported-faces-valid +>.head) |
5572+ $(node rest, names [+<.head names])
5573+ ?. (imported-faces-valid head) |
5574+ $(node rest)
5575+ ?: ?=([%face @ *] node)
5576+ ?: (lien names |=(n=@ =(n +<.node))) |
5577+ (imported-faces-valid +>.node)
5578+ (imported-faces-valid node)
48295579::
48305580++ import-to-itype
48315581 |= node=*
@@ -4833,10 +5583,41 @@
48335583 ?@ node ~
48345584 ?+ -.node ~
48355585 %atom
5586+ ?: ?=([%atom %tas [~ @]] node)
5587+ =/ value=@ +>+.node
5588+ ?. |(=(value 0) (jibb-face-name value)) ~
5589+ =/ printed=@t ?:(=(value 0) '%$' (cat 3 '%' value))
5590+ `[%const [%term %tas value printed]]
48365591 ?. ?=([%atom @ ~] node) ~
48375592 =/ aura=@ta (@ta +<.node)
4838− ?. ?=(?(%ud %ux %uv %t %ta %tas %p %da %dr) aura) ~
5593+ ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
48395594 `[%atom aura]
5595+ %apply
5596+ ?. ?=([%apply @ *] node) ~
5597+ =/ name=term (@tas +<.node)
5598+ =/ arity=@ud
5599+ ?: |(=(%list name) =(%unit name) =(%set name) =(%qeu name)) 1
5600+ ?: |(=(%map name) =(%mop name) =(%jar name) =(%jug name)) 2
5601+ 0
5602+ ?: =(arity 0) ~
5603+ =/ args=(unit (list itype)) (import-to-itypes +>.node)
5604+ ?~ args ~
5605+ ?. =(arity (lent u.args)) ~
5606+ `[%collection name u.args]
5607+ %fork
5608+ =/ cases=(unit (list itype)) (import-to-itypes +.node)
5609+ ?~ cases ~
5610+ ?~ u.cases ~
5611+ ?~ t.u.cases ~
5612+ ?. (import-cases-disjoint u.cases) ~
5613+ `[%union u.cases ~ ~ ~]
5614+ %face
5615+ ?. ?=([%face @ *] node) ~
5616+ =/ name=@ +<.node
5617+ ?. (jibb-face-name name) ~
5618+ =/ body=(unit itype) $(node +>.node)
5619+ ?~ body ~
5620+ `[%face (@tas name) u.body]
48405621 %cell
48415622 ?. ?=([%cell * *] node) ~
48425623 =/ left=(unit itype) $(node +<.node)
@@ -4846,6 +5627,36 @@
48465627 `[%cell u.left u.right]
48475628 ==
48485629::
5630+++ import-to-itypes
5631+ |= nodes=*
5632+ ^- (unit (list itype))
5633+ ?@ nodes ?:(=(nodes 0) `~ ~)
5634+ =/ first (import-to-itype -.nodes)
5635+ ?~ first ~
5636+ =/ rest $(nodes +.nodes)
5637+ ?~ rest ~
5638+ `[u.first u.rest]
5639+::
5640+++ import-type-pattern
5641+ |= typ=itype
5642+ ^- upat
5643+ ?- -.typ
5644+ %atom [%atom ~]
5645+ %const [%atom `val.literal.typ]
5646+ %face $(typ body.typ)
5647+ %cell [%cell $(typ hed.typ) $(typ tal.typ)]
5648+ %union [%or (turn cases.typ |=(t=itype (import-type-pattern t)))]
5649+ * [%unknown ~]
5650+ ==
5651+::
5652+++ import-cases-disjoint
5653+ |= cases=(list itype)
5654+ ^- ?
5655+ ?~ cases &
5656+ =/ first=upat (import-type-pattern i.cases)
5657+ ?. (levy t.cases |=(t=itype =(%disjoint (union-relate first (import-type-pattern t))))) |
5658+ $(cases t.cases)
5659+::
48495660++ find-imported-mold
48505661 |= [module=term name=term externals=iexternals surs=(list term)]
48515662 ^- (unit itype)
@@ -4857,7 +5668,15 @@
48575668 =/ result=* result.i.found
48585669 ?@ result ~
48595670 ?. ?=(%& -.result) ~
4860− (import-to-itype +.result)
5671+ =/ node=* +.result
5672+ ?. (imported-faces-valid node) ~
5673+ ?@ node (import-to-itype node)
5674+ ?: ?=(%ref -.node) (import-to-itype node)
5675+ =/ pattern=(unit irec-pattern) (rec-pattern node module name)
5676+ ?~ pattern (import-to-itype node)
5677+ ?. has.u.pattern (import-to-itype node)
5678+ `[%recursive module name `(crip "{(trip name)}.{(trip module)}")]
5679+
48615680::
48625681++ collect-sur-imports
48635682 |= imports=(list import)
@@ -4867,14 +5686,283 @@
48675686 [name.i.imports $(imports t.imports)]
48685687 $(imports t.imports)
48695688::
5689+++ collect-mark-imports
5690+ |= imports=(list import)
5691+ ^- (list term)
5692+ ?~ imports ~
5693+ ?: ?=(%mark -.i.imports)
5694+ [mark.i.imports $(imports t.imports)]
5695+ $(imports t.imports)
5696+::
5697+++ find-imported-mark
5698+ |= [name=term externals=imark-externals marks=(list term)]
5699+ ^- (unit itype)
5700+ ?. (unique-value-name name marks) ~
5701+ =/ found=imark-externals
5702+ (skim externals |=(e=[mark=term result=*] =(name mark.e)))
5703+ ?~ found ~
5704+ ?^ t.found ~
5705+ =/ result=* result.i.found
5706+ ?@ result ~
5707+ ?. ?=(%& -.result) ~
5708+ ?. (imported-faces-valid +.result) ~
5709+ (import-to-itype +.result)
5710+::
5711+++ find-jibb-interface
5712+ |= [face=term imports=ijimports]
5713+ ^- (unit ifile)
5714+ ?~ imports ~
5715+ ?: =(face face.i.imports) `interface.i.imports
5716+ $(imports t.imports)
5717+::
5718+++ find-jibb-mold
5719+ |= [name=term iface=ifile]
5720+ ^- (unit ischeme)
5721+ =/ ms=imold-types molds.iface
5722+ |-
5723+ ?~ ms ~
5724+ ?: =(name name.i.ms) `template.i.ms
5725+ $(ms t.ms)
5726+::
5727+:: An exported alias may name a union from another module. Only a
5728+:: nongeneric alias of the same origin is usable through this import face.
5729+::
5730+++ imported-union-alias
5731+ |= [origin=[at=path name=term] molds=imold-types]
5732+ ^- (unit term)
5733+ ?~ molds ~
5734+ =/ template=ischeme template.i.molds
5735+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
5736+ ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
5737+ $(molds t.molds)
5738+::
5739+:: Only names exported by this directly imported module are visible through
5740+:: its face. Other origins retain identity but print as unnamed unions.
5741+::
5742+++ itype-in-import
5743+ |= [t=itype iface=ifile face=term]
5744+ ^- itype
5745+ ?- -.t
5746+ %union
5747+ =/ label=(unit @t)
5748+ ?~ origin.t ~
5749+ ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
5750+ =/ alias=(unit term) ~
5751+ =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
5752+ =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
5753+ ?~ alias ~
5754+ `(crip "{(trip u.alias)}.{(trip face)}")
5755+ [%union (turn cases.t |=(c=itype (itype-in-import c iface face))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face)))]
5756+ %recursive [%recursive module.t name.t ~]
5757+ %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face)))]
5758+ %face [%face name.t $(t body.t)]
5759+ %fn [%fn $(t sample.t) $(t product.t)]
5760+ %cell [%cell $(t hed.t) $(t tal.t)]
5761+ * t
5762+ ==
5763+::
5764+++ label-direct-union
5765+ |= [typ=itype body=shape name=term state=istate]
5766+ ^- itype
5767+ ?. ?=(%union -.typ) typ
5768+ =/ direct=? ?=(%union -.body)
5769+ =? direct ?=(%generic -.body) ?=(%union -.body.body)
5770+ ?. direct typ
5771+ ?. (lien top-molds.state |=(n=term =(n name))) typ
5772+ [%union cases.typ `[at.state name] `name args.typ]
5773+::
5774+:: Generic mold parameters are lexical and distinct from the enclosing
5775+:: value's capital variables. Arguments are substituted only once, so
5776+:: an argument's variable ID cannot be captured by a template ID.
5777+:: A generic alias of a named union keeps the underlying union's origin
5778+:: and substituted argument order; an originless union stays unsupported.
5779+::
5780+++ iparam-lookup
5781+ |= [name=@t params=iparams]
5782+ ^- (unit itype)
5783+ ?~ params ~
5784+ ?: =(name name.i.params) `typ.i.params
5785+ $(params t.params)
5786+::
5787+++ distinct-params
5788+ |= names=(list @t)
5789+ ^- ?
5790+ ?~ names &
5791+ ?: (lien t.names |=(n=@t =(n i.names))) |
5792+ $(names t.names)
5793+::
5794+++ bind-params
5795+ |= [names=(list @t) args=(list itype)]
5796+ ^- (unit iparams)
5797+ ?~ names ?~(args `~ ~)
5798+ ?~ args ~
5799+ =/ rest=(unit iparams) $(names t.names, args t.args)
5800+ ?~ rest ~
5801+ `[[i.names i.args] u.rest]
5802+::
5803+++ template-apply
5804+ |= [template=ischeme args=(list itype)]
5805+ ^- (unit itype)
5806+ =/ vars=(list @ud) vars.template
5807+ =/ ren=isub ~
5808+ |-
5809+ ?~ vars ?~(args `(itype-rename typ.template ren) ~)
5810+ ?~ args ~
5811+ $(vars t.vars, args t.args, ren [[i.vars i.args] ren])
5812+::
5813+++ infer-shape-args
5814+ |= [args=(list shape) state=istate]
5815+ ^- (unit [types=(list itype) state=istate])
5816+ ?~ args `[~ state]
5817+ =/ head=(unit [typ=itype state=istate]) (infer-simple-shape i.args state)
5818+ ?~ head ~
5819+ =/ tail=(unit [types=(list itype) state=istate]) $(args t.args, state state.u.head)
5820+ ?~ tail ~
5821+ `[[typ.u.head types.u.tail] state.u.tail]
5822+::
5823+++ fresh-mold-params
5824+ |= [names=(list @t) next=@ud]
5825+ ^- [params=iparams vars=(list @ud) next=@ud]
5826+ ?~ names [~ ~ next]
5827+ =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
5828+ [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
5829+::
5830+++ infer-mold-template
5831+ |= [sh=shape state=istate]
5832+ ^- (unit [template=ischeme state=istate])
5833+ ?: ?=(%generic -.sh)
5834+ ?~ vars.sh ~
5835+ ?. (distinct-params vars.sh) ~
5836+ =/ fresh=[params=iparams vars=(list @ud) next=@ud] (fresh-mold-params vars.sh next.state)
5837+ =/ out=(unit [typ=itype state=istate])
5838+ (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
5839+ ?~ out ~
5840+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
5841+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
5842+ typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
5843+ =/ used=(list @ud) (itype-vars typ.u.out)
5844+ ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
5845+ `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state)]
5846+ =/ out=(unit [typ=itype state=istate])
5847+ (infer-simple-shape sh state(params ~, in-mold &))
5848+ ?~ out ~
5849+ ?: ?=(^ (itype-vars typ.u.out)) ~
5850+ `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
5851+::
5852+:: A direct imported reference may carry definite reader evidence. Only
5853+:: uniquely supplied, declared inputs are used; unsupported data stay generic.
5854+++ direct-import-invalid
5855+ |= [sh=shape state=istate]
5856+ ^- (unit idiag)
5857+ ?. ?=(%ref -.sh) ~
5858+ ?~ names.sh ~
5859+ =/ n=term i.names.sh
5860+ =/ raw=*
5861+ ?~ t.names.sh
5862+ ?. (unique-value-name n marks.state) ~
5863+ ?: (lien surs.state |=(x=term =(x n))) ~
5864+ ?: ?=(^ (find-jibb-interface n jimports.state)) ~
5865+ ?: (lien globals.state |=(x=term =(x n))) ~
5866+ ?: (lien reserved-molds.state |=(x=term =(x n))) ~
5867+ ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) ~
5868+ =/ found=imark-externals (skim mark-externals.state |=(e=[mark=term result=*] =(mark.e n)))
5869+ ?~ found ~
5870+ ?^ t.found ~
5871+ result.i.found
5872+ ?^ t.t.names.sh ~
5873+ =/ mod=term i.t.names.sh
5874+ ?: ?=(^ (find-jibb-interface mod jimports.state)) ~
5875+ ?. (unique-value-name mod surs.state) ~
5876+ ?: (lien marks.state |=(x=term =(x mod))) ~
5877+ ?: (lien globals.state |=(x=term =(x mod))) ~
5878+ ?: (lien reserved-molds.state |=(x=term =(x mod))) ~
5879+ ?: (lien molds.state |=(m=[name=term body=shape] =(mod name.m))) ~
5880+ =/ found=iexternals (skim externals.state |=(e=[module=term name=term result=*] &(=(module.e mod) =(name.e n))))
5881+ ?~ found ~
5882+ ?^ t.found ~
5883+ result.i.found
5884+ ?. ?=([%invalid ?(%aura %core) @] raw) ~
5885+ `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
5886+::
5887+:: Replay only the shape branches whose evaluation order we can prove.
5888+:: Successful prefixes must be checked before descending to a failure.
5889+++ nested-import-invalid
5890+ |= [sh=shape state=istate]
5891+ ^- (unit idiag)
5892+ ?: ?=(^ (infer-simple-shape sh state)) ~
5893+ ?- -.sh
5894+ %ref
5895+ =/ direct=(unit idiag) (direct-import-invalid sh state)
5896+ ?^ direct direct
5897+ ?~ names.sh ~
5898+ ?^ t.names.sh ~
5899+ =/ n=term i.names.sh
5900+ ?: (lien marks.state |=(x=term =(x n))) ~
5901+ ?: (lien active.state |=(x=term =(x n))) ~
5902+ =/ found=(unit shape) (find-simple-mold n molds.state)
5903+ ?~ found ~
5904+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
5905+ %fn
5906+ =/ first=(unit [typ=itype state=istate]) (infer-simple-shape sample.sh state)
5907+ ?~ first $(sh sample.sh)
5908+ $(sh product.sh, state state.u.first)
5909+ %cell (nested-field-invalid fields.sh state)
5910+ * ~
5911+ ==
5912+::
5913+++ nested-field-invalid
5914+ |= [fields=(list field) state=istate]
5915+ ^- (unit idiag)
5916+ ?~ fields ~
5917+ =/ sh=shape
5918+ ?- -.i.fields
5919+ %bare shape.i.fields
5920+ %face shape.i.fields
5921+ %pun [%ref at.i.fields ~[name.i.fields]]
5922+ ==
5923+ =/ out=(unit [typ=itype state=istate]) (infer-simple-shape sh state)
5924+ ?~ out (nested-import-invalid sh state)
5925+ $(fields t.fields, state state.u.out)
5926+::
5927+++ sample-import-invalid
5928+ |= [s=sample env=ienv state=istate]
5929+ ^- (unit idiag)
5930+ =/ result=isample-result (infer-sample s env state)
5931+ ?: ?=(%& -.result) ~
5932+ ?. =(p.result "sample mold is not supported by partial inference") ~
5933+ ?- s
5934+ [%face *] (nested-import-invalid shape.s state)
5935+ [%bare *] (nested-import-invalid shape.s state)
5936+ [%pun *] (nested-import-invalid [%ref at.s ~[name.s]] state)
5937+ [%cell *] (nested-samples-invalid items.s env state)
5938+ * ~
5939+ ==
5940+::
5941+++ nested-samples-invalid
5942+ |= [items=(list sample) env=ienv state=istate]
5943+ ^- (unit idiag)
5944+ ?~ items ~
5945+ =/ head=isample-result (infer-sample i.items env state)
5946+ ?: ?=(%| -.head) (sample-import-invalid i.items env state)
5947+ $(items t.items, env env.p.head, state state.p.head)
5948+::
48705949++ infer-simple-shape
48715950 |= [sh=shape state=istate]
48725951 ^- (unit [typ=itype state=istate])
48735952 ?- -.sh
48745953 %aura
4875− ?: =(0 aura.sh) ~
5954+ ?: =(0 aura.sh) `[[%any-atom ~] state]
48765955 `[[%atom aura.sh] state]
48775956 %flag `[[%flag ~] state]
5957+ %const
5958+ ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
5959+ `[[%const lit.sh] state]
5960+ %union
5961+ =/ pairs=(list upair) (union-pairs cases.sh molds.state)
5962+ ?. (levy pairs |=(p=upair =(%disjoint relation.p))) ~
5963+ =/ cs=(unit [types=(list itype) state=istate]) (infer-shape-args cases.sh state)
5964+ ?~ cs ~
5965+ `[[%union types.u.cs ~ ~ ~] state.u.cs]
48785966 %cell (infer-simple-fields fields.sh state)
48795967 %fn
48805968 =/ arg=(unit [typ=itype state=istate]) $(sh sample.sh)
@@ -4887,59 +5975,1034 @@
48875975 =/ n=term i.names.sh
48885976 ?^ t.names.sh
48895977 ?^ t.t.names.sh ~
5978+ =/ iface=(unit ifile) (find-jibb-interface i.t.names.sh jimports.state)
5979+ ?^ iface
5980+ =/ found=(unit ischeme) (find-jibb-mold n u.iface)
5981+ ?~ found ~
5982+ ?^ vars.u.found ~
5983+ `[(itype-in-import typ.u.found u.iface i.t.names.sh) state]
48905984 =/ found=(unit itype)
48915985 (find-imported-mold i.t.names.sh n externals.state surs.state)
48925986 ?~ found ~
48935987 `[u.found state]
5988+ ?: (lien marks.state |=(x=term =(x n)))
5989+ ?^ (find-simple-mold n molds.state) ~
5990+ =/ imported=(unit itype) (find-imported-mark n mark-externals.state marks.state)
5991+ ?~ imported ~
5992+ `[u.imported state]
48945993 ?: (lien active.state |=(x=term =(x n))) ~
48955994 =/ found=(unit shape) (find-simple-mold n molds.state)
4896− ?~ found ~
5995+ ?~ found
5996+ ?: (lien molds.state |=(m=[name=term body=shape] =(name.m n))) ~
5997+ ?~ prelude.state ~
5998+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state)
5999+ ?~ prelude-entry ~
6000+ ?^ vars.u.prelude-entry ~
6001+ `[typ.u.prelude-entry state]
6002+ =/ out=(unit [typ=itype state=istate])
6003+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
6004+ ?~ out ~
6005+ `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state)]
6006+ %apply
6007+ ?~ ref.sh ~
6008+ =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
6009+ ?~ args ~
6010+ =/ n=term i.ref.sh
6011+ ?^ t.ref.sh
6012+ ?^ t.t.ref.sh ~
6013+ =/ iface=(unit ifile) (find-jibb-interface i.t.ref.sh jimports.state.u.args)
6014+ ?~ iface ~
6015+ =/ template=(unit ischeme) (find-jibb-mold n u.iface)
6016+ ?~ template ~
6017+ ?~ vars.u.template ~
6018+ =/ applied=(unit itype) (template-apply u.template types.u.args)
6019+ ?~ applied ~
6020+ `[(itype-in-import u.applied u.iface i.t.ref.sh) state.u.args]
6021+ ?: (lien active.state.u.args |=(x=term =(x n))) ~
6022+ =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
6023+ ?~ found
6024+ ?: (lien molds.state.u.args |=(m=[name=term body=shape] =(name.m n))) ~
6025+ ?~ prelude.state.u.args ~
6026+ =/ prelude-entry=(unit ischeme) (find-jibb-mold n u.prelude.state.u.args)
6027+ ?~ prelude-entry ~
6028+ ?~ vars.u.prelude-entry ~
6029+ =/ applied=(unit itype) (template-apply u.prelude-entry types.u.args)
6030+ ?~ applied ~
6031+ `[u.applied state.u.args]
6032+ ?. ?=(%generic -.u.found) ~
6033+ ?. (distinct-params vars.u.found) ~
6034+ =/ params=(unit iparams) (bind-params vars.u.found types.u.args)
6035+ ?~ params ~
48976036 =/ out=(unit [typ=itype state=istate])
4898− $(sh u.found, state state(active [n active.state], in-mold &))
6037+ $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
48996038 ?~ out ~
4900− `[typ.u.out state.u.out(active active.state, in-mold in-mold.state)]
6039+ ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
6040+ ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
6041+ =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
6042+ (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6043+ `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
49016044 %tvar
6045+ =/ param=(unit itype) (iparam-lookup name.sh params.state)
6046+ ?^ param `[u.param state]
49026047 ?: in-mold.state ~
49036048 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
49046049 ?^ n `[[%var u.n] state]
4905− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state] caps.state])]
6050+ `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
49066051 * ~
49076052 ==
49086053::
4909−++ infer-simple-fields
4910− |= [fields=(list field) state=istate]
4911− ^- (unit [typ=itype state=istate])
4912− ?~ fields ~
4913− ?. ?=(%bare -.i.fields) ~
4914− =/ head=(unit [typ=itype state=istate]) (infer-simple-shape shape.i.fields state)
4915− ?~ head ~
4916− ?~ t.fields head
4917− =/ tail=(unit [typ=itype state=istate]) $(fields t.fields, state state.u.head)
4918− ?~ tail ~
4919− `[[%cell typ.u.head typ.u.tail] state.u.tail]
6054+++ infer-simple-fields
6055+ |= [fields=(list field) state=istate]
6056+ ^- (unit [typ=itype state=istate])
6057+ ?~ fields ~
6058+ =/ field-shape=shape
6059+ ?- -.i.fields
6060+ %bare shape.i.fields
6061+ %face shape.i.fields
6062+ %pun [%ref at.i.fields ~[name.i.fields]]
6063+ ==
6064+ =/ head=(unit [typ=itype state=istate]) (infer-simple-shape field-shape state)
6065+ ?~ head ~
6066+ =/ t=itype typ.u.head
6067+ =. t
6068+ ?- -.i.fields
6069+ %bare t
6070+ %face [%face name.i.fields t]
6071+ %pun [%face name.i.fields t]
6072+ ==
6073+ ?~ t.fields `[t state.u.head]
6074+ =/ tail=(unit [typ=itype state=istate]) $(fields t.fields, state state.u.head)
6075+ ?~ tail ~
6076+ `[[%cell t typ.u.tail] state.u.tail]
6077+::
6078+++ infer-sample
6079+ |= [s=sample env=ienv state=istate]
6080+ ^- isample-result
6081+ ?- -.s
6082+ %bind
6083+ ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6084+ [%| "sample shadows a name"]
6085+ =/ t=itype [%var next.state]
6086+ [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
6087+ %face
6088+ ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6089+ [%| "sample shadows a name"]
6090+ =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
6091+ ?~ t [%| "sample mold is not supported by partial inference"]
6092+ [%& typ.u.t [[name.s [typ.u.t ~]] env] state.u.t]
6093+ %bare
6094+ =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
6095+ ?~ t [%| "sample mold is not supported by partial inference"]
6096+ [%& typ.u.t env state.u.t]
6097+ %pun
6098+ $(s [%face at.s name.s [%ref at.s ~[name.s]]])
6099+ %cell
6100+ (infer-sample-items items.s env state)
6101+ ==
6102+::
6103+:: Cell-sample binders are faces on their positions; at the top of a
6104+:: sample a binder only supplies a name for the whole sample.
6105+::
6106+++ infer-sample-items
6107+ |= [items=(list sample) env=ienv state=istate]
6108+ ^- isample-result
6109+ ?~ items [%| "empty sample is not supported by partial inference"]
6110+ =/ head=isample-result (infer-sample i.items env state)
6111+ ?: ?=(%| -.head) head
6112+ =/ ht=itype typ.p.head
6113+ =. ht
6114+ ?- -.i.items
6115+ %bind [%face name.i.items ht]
6116+ %face [%face name.i.items ht]
6117+ %pun [%face name.i.items ht]
6118+ * ht
6119+ ==
6120+ ?~ t.items [%& ht env.p.head state.p.head]
6121+ =/ tail=isample-result $(items t.items, env env.p.head, state state.p.head)
6122+ ?: ?=(%| -.tail) tail
6123+ [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
6124+::
6125+:: Local definitions generalize only variables outside their enclosing
6126+:: environment and explicit-capital scope. Single self-recursive gates
6127+:: use a monomorphic placeholder; mutually recursive groups stay unsupported.
6128+::
6129++$ ilocal-result (each [env=ienv state=istate] idiag)
6130+++ free-env-vars
6131+ |= [env=ienv sub=isub]
6132+ ^- (list @ud)
6133+ ?~ env ~
6134+ =/ sc=ischeme scheme.i.env
6135+ =/ ids=(list @ud) (unique-type-vars (itype-vars typ.sc))
6136+ =/ free=(list @ud) ~
6137+ |-
6138+ ?~ ids (weld free (free-env-vars t.env sub))
6139+ ?: (lien vars.sc |=(n=@ud =(n i.ids))) $(ids t.ids)
6140+ =/ resolved=itype (itype-normalize [%var i.ids] sub)
6141+ $(ids t.ids, free (weld (itype-vars resolved) free))
6142+::
6143+++ free-cap-vars
6144+ |= [caps=icaps sub=isub]
6145+ ^- (list @ud)
6146+ ?~ caps ~
6147+ (weld (itype-vars (itype-normalize [%var id.i.caps] sub)) $(caps t.caps))
6148+::
6149+++ local-names-valid
6150+ |= [ds=(list def) env=ienv state=istate]
6151+ ^- ?
6152+ =/ names=(list term) (global-value-names ds)
6153+ |-
6154+ ?~ ds &
6155+ ?: ?=(%mold -.i.ds) $(ds t.ds)
6156+ ?. (unique-value-name name.i.ds names) |
6157+ ?: ?=(^ (ienv-lookup name.i.ds env)) |
6158+ ?: (lien globals.state |=(n=term =(n name.i.ds))) |
6159+ $(ds t.ds)
6160+::
6161+:: The supported local molds are nonrecursive simple aliases. Validate
6162+:: all of them, including unused ones, before checking any local values.
6163+:: The enclosing gate sample was checked before this scope was entered.
6164+::
6165+++ local-value-defs
6166+ |= ds=(list def)
6167+ ^- (list def)
6168+ ?~ ds ~
6169+ ?: ?=(%mold -.i.ds) $(ds t.ds)
6170+ [i.ds $(ds t.ds)]
6171+::
6172+++ local-mold-names-valid
6173+ |= [locals=imolds state=istate]
6174+ ^- ?
6175+ =/ names=(list term) (turn locals |=(m=[name=term body=shape] name.m))
6176+ |-
6177+ ?~ locals &
6178+ =/ n=term name.i.locals
6179+ ?. (unique-value-name n names) |
6180+ ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
6181+ ?: (lien marks.state |=(m=term =(n m))) |
6182+ ?: (lien reserved-molds.state |=(m=term =(n m))) |
6183+ ?: (lien surs.state |=(m=term =(n m))) |
6184+ $(locals t.locals)
6185+::
6186+++ local-molds-supported
6187+ |= [locals=imolds state=istate]
6188+ ^- ?
6189+ ?~ locals &
6190+ =/ m=[name=term body=shape] i.locals
6191+ =/ inferred=(unit [template=ischeme state=istate])
6192+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
6193+ ?~ inferred |
6194+ $(locals t.locals)
6195+::
6196+:: Gather written capitals belonging to one ++. Nested local definitions
6197+:: establish their own scopes; inline gates remain in the enclosing scope.
6198++$ icap-site [name=@t at=span]
6199+++ scope-shape
6200+ |= s=shape
6201+ ^- (list icap-site)
6202+ ?- -.s
6203+ %tvar ~[[name.s at.s]]
6204+ %apply (zing (turn args.s scope-shape))
6205+ %cell (zing (turn fields.s scope-field))
6206+ %union (zing (turn cases.s scope-shape))
6207+ %fn (weld (scope-shape sample.s) (scope-shape product.s))
6208+ %generic
6209+ =/ inside=(list icap-site) (scope-shape body.s)
6210+ (skim inside |=(site=icap-site !(lien vars.s |=(v=@t =(v name.site)))))
6211+ * ~
6212+ ==
6213+::
6214+++ scope-field
6215+ |= f=field
6216+ ^- (list icap-site)
6217+ ?- -.f
6218+ %face (scope-shape shape.f)
6219+ %bare (scope-shape shape.f)
6220+ %pun ~
6221+ ==
6222+::
6223+++ scope-sample
6224+ |= s=sample
6225+ ^- (list icap-site)
6226+ ?- -.s
6227+ %face (scope-shape shape.s)
6228+ %bare (scope-shape shape.s)
6229+ %cell (zing (turn items.s scope-sample))
6230+ * ~
6231+ ==
6232+::
6233+++ scope-pieces
6234+ |= ps=(list piece)
6235+ ^- (list icap-site)
6236+ ?~ ps ~
6237+ =/ first=(list icap-site)
6238+ ?- -.i.ps
6239+ %expr (scope-expr p.i.ps)
6240+ %text ~
6241+ ==
6242+ (weld first $(ps t.ps))
6243+::
6244+++ scope-qsegs
6245+ |= ps=(list qseg)
6246+ ^- (list icap-site)
6247+ ?~ ps ~
6248+ =/ first=(list icap-site)
6249+ ?- -.i.ps
6250+ %expr (scope-expr p.i.ps)
6251+ %knot ~
6252+ ==
6253+ (weld first $(ps t.ps))
6254+::
6255+++ scope-edits
6256+ |= xs=(list edit)
6257+ ^- (list icap-site)
6258+ ?~ xs ~
6259+ =/ first=(list icap-site) (scope-expr val.i.xs)
6260+ (weld first $(xs t.xs))
6261+::
6262+++ scope-items
6263+ |= xs=(list item)
6264+ ^- (list icap-site)
6265+ ?~ xs ~
6266+ =/ first=(list icap-site) (scope-expr val.i.xs)
6267+ (weld first $(xs t.xs))
6268+::
6269+++ scope-arms
6270+ |= xs=(list arm)
6271+ ^- (list icap-site)
6272+ ?~ xs ~
6273+ =/ first=(list icap-site) (scope-expr val.i.xs)
6274+ (weld first $(xs t.xs))
6275+::
6276+++ scope-exprs
6277+ |= xs=(list expr)
6278+ ^- (list icap-site)
6279+ ?~ xs ~
6280+ =/ first=(list icap-site) (scope-expr i.xs)
6281+ (weld first $(xs t.xs))
6282+::
6283+++ scope-expr
6284+ |= e=expr
6285+ ^- (list icap-site)
6286+ ?- -.e
6287+ %str (scope-pieces pieces.e)
6288+ %qath (scope-qsegs segs.e)
6289+ %change (scope-edits edits.e)
6290+ %pair (scope-expr val.e)
6291+ %unit (scope-expr val.e)
6292+ %group (scope-expr inner.e)
6293+ %list (scope-exprs items.e)
6294+ %tuple (scope-items items.e)
6295+ %gate
6296+ =/ first=(list icap-site) (scope-sample sample.e)
6297+ =/ last=(list icap-site) (scope-expr body.e)
6298+ (weld first last)
6299+ %gate-wide
6300+ =/ first=(list icap-site) (scope-sample sample.e)
6301+ =/ last=(list icap-site) (scope-expr body.e)
6302+ (weld first last)
6303+ %call
6304+ =/ first=(list icap-site) (scope-expr head.e)
6305+ =/ last=(list icap-site) (scope-exprs args.e)
6306+ (weld first last)
6307+ %cast
6308+ =/ first=(list icap-site) (scope-shape shape.e)
6309+ =/ last=(list icap-site) (scope-expr val.e)
6310+ (weld first last)
6311+ %trace
6312+ =/ first=(list icap-site) (scope-expr val.e)
6313+ =/ last=(list icap-site) (scope-expr then.e)
6314+ (weld first last)
6315+ %branch
6316+ =/ first=(list icap-site) (scope-expr subject.e)
6317+ =/ last=(list icap-site) (scope-arms arms.e)
6318+ (weld first last)
6319+ %body (scope-expr final.e)
6320+ * ~
6321+ ==
6322+::
6323+++ reserve-cap-sites
6324+ |= [sites=(list icap-site) state=istate]
6325+ ^- istate
6326+ ?~ sites state
6327+ ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
6328+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
6329+::
6330+++ reserve-def-caps
6331+ |= [e=expr state=istate]
6332+ ^- istate
6333+ (reserve-cap-sites (scope-expr e) state)
6334+::
6335+++ infer-local-defs
6336+ |= [ds=(list def) env=ienv state=istate]
6337+ ^- ilocal-result
6338+ =/ remaining=(list def) ~
6339+ =/ progressed=? |
6340+ |-
6341+ ?~ ds
6342+ ?~ remaining [%& env state]
6343+ ?. progressed [%| ["local definitions need unsupported inference" ~]]
6344+ $(ds (flop remaining), remaining ~, progressed |)
6345+ =/ d=def i.ds
6346+ ?> ?=(%value -.d)
6347+ =/ local-state=istate (reserve-def-caps val.d state)
6348+ =/ inferred=iresult (infer-fragment val.d env local-state)
6349+ =/ retried=? ?=(%| -.inferred)
6350+ =? inferred retried (infer-recursive-gate d env local-state)
6351+ ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6352+ =/ merged=(unit [first=icap second=icap])
6353+ (merged-capitals caps.state.p.inferred sub.state.p.inferred)
6354+ ?^ merged
6355+ [%| ["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"]]]]
6356+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred)
6357+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
6358+ =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
6359+ ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
6360+ $(ds t.ds, remaining [d remaining])
6361+ ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
6362+ $(ds t.ds, remaining [d remaining])
6363+ =/ free=(list @ud)
6364+ (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
6365+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
6366+ =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6367+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
6368+::
6369+:: Read only fields of a known record. Unresolved field constraints and
6370+:: ambiguous repeated faces are outside this fragment. Imported record
6371+:: spines with repeated names are unavailable when used.
6372+::
6373+++ record-fields-named
6374+ |= [name=term t=itype sub=isub]
6375+ ^- (list itype)
6376+ =. t (itype-walk t sub)
6377+ ?: ?=(%face -.t)
6378+ ?:(=(name name.t) ~[body.t] ~)
6379+ ?. ?=(%cell -.t) ~
6380+ =/ first=(list itype) ~
6381+ =/ head=itype (itype-walk hed.t sub)
6382+ =? first ?=(%face -.head) ?:(=(name name.head) ~[body.head] ~)
6383+ (weld first $(t tal.t))
6384+::
6385+++ infer-field-wing
6386+ |= [names=(list term) env=ienv state=istate]
6387+ ^- iresult
6388+ =/ reverse=(list term) (flop names)
6389+ ?~ reverse [%| ["empty wing" ~]]
6390+ =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6391+ ?~ scheme [%| ["field access is not supported by partial inference" ~]]
6392+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
6393+ =/ fields=(list term) t.reverse
6394+ =/ typ=itype typ.inst
6395+ |-
6396+ ?~ fields [%& typ state.inst]
6397+ =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
6398+ ?~ found [%| ["field is not available to partial inference" ~]]
6399+ ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6400+ $(fields t.fields, typ i.found)
6401+::
6402+:: Propagate a known union or list through supported loobean, unit and list
6403+:: branches. Empty bodies and groups are transparent; bodies with definitions
6404+:: keep their normal scoping and wait for general bidirectional inference.
6405+::
6406+++ context-union-branch
6407+ |= e=expr
6408+ ^- ?
6409+ ?- -.e
6410+ %branch &
6411+ %group $(e inner.e)
6412+ %body ?~(defs.e $(e final.e) |)
6413+ * |
6414+ ==
6415+::
6416+++ infer-union-context
6417+ |= [e=expr expected=itype env=ienv state=istate context=span]
6418+ ^- iresult
6419+ ?: ?=(%group -.e) $(e inner.e)
6420+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6421+ ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
6422+ (infer-list-context e expected env state context)
6423+ ?: ?=(%branch -.e)
6424+ ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
6425+ ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
6426+ ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
6427+ =/ x=arm i.arms.e
6428+ =/ y=arm i.t.arms.e
6429+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
6430+ (infer-unit-branch e env state `[expected context])
6431+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y))
6432+ [%| ["branch pattern is not supported by partial inference" ~]]
6433+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6434+ [%| ["branch pattern is not supported by partial inference" ~]]
6435+ ?: =(val.lit.pat.x val.lit.pat.y)
6436+ [%| ["branch does not cover both loobeans" ~]]
6437+ =/ subject=iresult (infer-fragment subject.e env state)
6438+ ?: ?=(%| -.subject) subject
6439+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
6440+ ?: ?=(%union -.subject-type)
6441+ [%| ["contextual union-pattern branch is not supported by partial inference" ~]]
6442+ =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
6443+ ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
6444+ =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
6445+ ?: ?=(%| -.left) left
6446+ =/ right=iresult $(e val.y, state state.p.left)
6447+ ?: ?=(%| -.right) right
6448+ [%& expected state.p.right]
6449+ =/ value=iresult (infer-fragment e env state)
6450+ ?: ?=(%| -.value) value
6451+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
6452+ ?: ?=(%unknown -.fit)
6453+ ?: &(?=(%collection -.expected) =(%list name.expected))
6454+ [%| ["branch list constraint is not supported by partial inference" ~]]
6455+ [%| ["branch union constraint is not supported by partial inference" ~]]
6456+ ?: ?=(%bad -.fit)
6457+ =/ missing=(unit idiag) (missing-union-tag e expected sub.state.p.value context)
6458+ ?^ missing [%| u.missing]
6459+ ?: &(?=(%collection -.expected) =(%list name.expected))
6460+ [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
6461+ [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
6462+ [%& expected state.p.value(sub sub.fit, next next.fit)]
6463+::
6464+:: A list expression needs a known list target and the validated prelude list.
6465+:: Literal items and unfaced two-item cons cells receive that target one by
6466+:: one; pending constraints elsewhere stay in the threaded state.
6467+::
6468+++ context-list-expression
6469+ |= e=expr
6470+ ^- ?
6471+ ?- -.e
6472+ %list &
6473+ %tuple &
6474+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6475+ %group $(e inner.e)
6476+ %body ?~(defs.e $(e final.e) |)
6477+ * |
6478+ ==
6479+::
6480+++ infer-list-context
6481+ |= [e=expr expected=itype env=ienv state=istate context=span]
6482+ ^- iresult
6483+ ?: ?=(%group -.e) $(e inner.e)
6484+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6485+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
6486+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
6487+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6488+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
6489+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
6490+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
6491+ [%| ["list literal needs the standard prelude in partial inference" ~]]
6492+ =/ target=itype (itype-walk expected sub.state)
6493+ ?. ?=(%collection -.target) [%| ["list context is not supported by partial inference" ~]]
6494+ ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
6495+ ?~ args.target [%| ["list context is not supported by partial inference" ~]]
6496+ ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
6497+ ?: ?=(%lit -.e)
6498+ ?. |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6499+ [%| ["list expression is not supported by partial inference" ~]]
6500+ [%& target state]
6501+ ?: ?=(%list -.e)
6502+ =/ result=iresult (infer-list-items items.e i.args.target env state context)
6503+ ?: ?=(%| -.result) result
6504+ [%& target state.p.result]
6505+ ?. ?=(%tuple -.e) [%| ["list expression is not supported by partial inference" ~]]
6506+ ?~ items.e [%| ["cons shape is not supported by partial inference" ~]]
6507+ ?~ t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6508+ ?^ t.t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6509+ ?^ face.i.items.e [%| ["faced cons is not supported by partial inference" ~]]
6510+ ?^ face.i.t.items.e [%| ["faced cons is not supported by partial inference" ~]]
6511+ =/ head=iresult (infer-list-items ~[val.i.items.e] i.args.target env state context)
6512+ ?: ?=(%| -.head) head
6513+ =/ target=itype (itype-walk target sub.state.p.head)
6514+ =/ tail=iresult
6515+ ?: (context-list-expression val.i.t.items.e)
6516+ (infer-list-context val.i.t.items.e target env state.p.head context)
6517+ (infer-fragment val.i.t.items.e env state.p.head)
6518+ ?: ?=(%| -.tail) tail
6519+ =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
6520+ ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
6521+ ?: ?=(%bad -.fit)
6522+ [%| ["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)]]]]
6523+ [%& target state.p.tail(sub sub.fit, next next.fit)]
6524+::
6525+++ infer-list-items
6526+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6527+ ^- iresult
6528+ ?~ items [%& expected state]
6529+ =/ target=itype (itype-walk expected sub.state)
6530+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6531+ ?: ?=(%| -.value) value
6532+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6533+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6534+ ?: ?=(%bad -.fit)
6535+ =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
6536+ ?^ missing [%| u.missing]
6537+ [%| ["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)]]]]
6538+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
6539+::
6540+:: The supported unit pattern covers exactly an atom zero and a cell
6541+:: headed by zero, with a single binder for its payload. Unresolved
6542+:: subjects and all other pattern matrices stay outside this fragment.
6543+::
6544+++ unit-empty-pattern
6545+ |= p=pattern
6546+ ^- ?
6547+ ?. ?=(%lit -.p) |
6548+ =(%null form.lit.p)
49206549::
4921−++ infer-sample
4922− |= [s=sample env=ienv state=istate]
4923− ^- isample-result
4924− ?- -.s
4925− %bind
4926− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
4927− [%| "sample shadows a name"]
4928− =/ t=itype [%var next.state]
4929− [%& t [[name.s [t ~]] env] state(next +(next.state))]
6550+++ unit-payload-pattern
6551+ |= p=pattern
6552+ ^- (unit term)
6553+ ?. ?=(%cell -.p) ~
6554+ ?~ items.p ~
6555+ ?~ t.items.p ~
6556+ ?^ t.t.items.p ~
6557+ ?. (unit-empty-pattern i.items.p) ~
6558+ ?. ?=(%bind -.i.t.items.p) ~
6559+ `name.i.t.items.p
6560+::
6561+++ unit-empty-case
6562+ |= t=itype
6563+ ^- ?
6564+ ?. ?=(%const -.t) |
6565+ =(0 val.literal.t)
6566+::
6567+++ unit-payload-case
6568+ |= t=itype
6569+ ^- (unit itype)
6570+ ?. ?=(%cell -.t) ~
6571+ ?. (unit-empty-case hed.t) ~
6572+ =/ payload=itype tal.t
6573+ =? payload ?=(%face -.payload) body.payload
6574+ `payload
6575+::
6576+++ unit-union-payload
6577+ |= t=itype
6578+ ^- (unit itype)
6579+ ?. ?=(%union -.t) ~
6580+ ?~ cases.t ~
6581+ ?~ t.cases.t ~
6582+ ?^ t.t.cases.t ~
6583+ ?: (unit-empty-case i.cases.t) (unit-payload-case i.t.cases.t)
6584+ ?: (unit-empty-case i.t.cases.t) (unit-payload-case i.cases.t)
6585+ ~
6586+::
6587+:: List matching currently covers exactly null and a cell of two binders.
6588+:: The head has the element type and the tail has the whole list type.
6589+:: Other patterns and lists whose element mold is empty remain unsupported.
6590+::
6591+++ list-payload-pattern
6592+ |= p=pattern
6593+ ^- (unit [head=term tail=term])
6594+ ?. ?=(%cell -.p) ~
6595+ ?~ items.p ~
6596+ ?~ t.items.p ~
6597+ ?^ t.t.items.p ~
6598+ ?. ?=(%bind -.i.items.p) ~
6599+ ?. ?=(%bind -.i.t.items.p) ~
6600+ `[name.i.items.p name.i.t.items.p]
6601+::
6602+++ infer-list-branch
6603+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span]) typ=itype]
6604+ ^- iresult
6605+ ?> ?=(%branch -.e)
6606+ ?> ?=(%collection -.typ)
6607+ ?. =(%list name.typ) [%| ["list pattern is not supported by partial inference" ~]]
6608+ ?~ prelude.state [%| ["list pattern needs the standard prelude in partial inference" ~]]
6609+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
6610+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
6611+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
6612+ ?~ standard [%| ["list pattern needs the standard prelude in partial inference" ~]]
6613+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
6614+ [%| ["list pattern needs the standard prelude in partial inference" ~]]
6615+ ?~ args.typ [%| ["list pattern is not supported by partial inference" ~]]
6616+ ?^ t.args.typ [%| ["list pattern is not supported by partial inference" ~]]
6617+ ?~ arms.e [%| ["list branch is not supported by partial inference" ~]]
6618+ ?~ t.arms.e [%| ["list branch is not supported by partial inference" ~]]
6619+ ?^ t.t.arms.e [%| ["list branch is not supported by partial inference" ~]]
6620+ =/ x=arm i.arms.e
6621+ =/ y=arm i.t.arms.e
6622+ =/ first-empty=? (unit-empty-pattern pat.x)
6623+ =/ first-name=(unit [head=term tail=term]) (list-payload-pattern pat.x)
6624+ =/ second-name=(unit [head=term tail=term]) (list-payload-pattern pat.y)
6625+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
6626+ [%| ["list branch pattern is not supported by partial inference" ~]]
6627+ =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
6628+ ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
6629+ ?: |(=(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)))))
6630+ [%| ["pattern binder shadows a name" ~]]
6631+ =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
6632+ =/ left=iresult
6633+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state)
6634+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state context.u.expected)
6635+ ?: ?=(%| -.left) left
6636+ =/ right=iresult
6637+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6638+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
6639+ ?: ?=(%| -.right) right
6640+ ?^ expected [%& typ.u.expected state.p.right]
6641+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
6642+ ?~ joined [%| ["list branch results need unsupported inference" ~]]
6643+ [%& typ.p.left state.p.right(sub u.joined)]
6644+::
6645+++ infer-unit-branch
6646+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
6647+ ^- iresult
6648+ ?> ?=(%branch -.e)
6649+ ?~ arms.e [%| ["unit branch is not supported by partial inference" ~]]
6650+ ?~ t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
6651+ ?^ t.t.arms.e [%| ["unit branch is not supported by partial inference" ~]]
6652+ =/ subject=iresult (infer-fragment subject.e env state)
6653+ ?: ?=(%| -.subject) subject
6654+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6655+ ?: &(?=(%collection -.typ) =(%list name.typ))
6656+ (infer-list-branch e env state.p.subject expected typ)
6657+ =/ x=arm i.arms.e
6658+ =/ y=arm i.t.arms.e
6659+ =/ first-empty=? (unit-empty-pattern pat.x)
6660+ =/ first-name=(unit term) (unit-payload-pattern pat.x)
6661+ =/ second-name=(unit term) (unit-payload-pattern pat.y)
6662+ ?. |(&(first-empty ?=(^ second-name)) &((unit-empty-pattern pat.y) ?=(^ first-name)))
6663+ [%| ["unit branch pattern is not supported by partial inference" ~]]
6664+ =/ binder=(unit term) ?:(first-empty second-name first-name)
6665+ ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
6666+ ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
6667+ [%| ["pattern binder shadows a name" ~]]
6668+ =/ payload=(unit itype) (unit-union-payload typ)
6669+ ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
6670+ =/ extended=ienv [[u.binder [u.payload ~]] env]
6671+ =/ left=iresult
6672+ ?~ expected (infer-fragment val.x ?:(first-empty env extended) state.p.subject)
6673+ (infer-union-context val.x typ.u.expected ?:(first-empty env extended) state.p.subject context.u.expected)
6674+ ?: ?=(%| -.left) left
6675+ =/ right=iresult
6676+ ?~ expected (infer-fragment val.y ?:(first-empty extended env) state.p.left)
6677+ (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
6678+ ?: ?=(%| -.right) right
6679+ ?^ expected [%& typ.u.expected state.p.right]
6680+ =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
6681+ ?~ joined [%| ["unit branch results need unsupported inference" ~]]
6682+ [%& typ.p.left state.p.right(sub u.joined)]
6683+::
6684+:: Infer pieces in order, retaining their substitutions and pending tags.
6685+:: A bare decimal literal has no outside type constraint, so it takes its
6686+:: normal @ud default here. Other open numeric and aura variables wait for
6687+:: deferred constraints, which this fragment does not implement yet.
6688+++ infer-string-pieces
6689+ |= [ps=(list piece) env=ienv state=istate]
6690+ ^- iresult
6691+ ?~ ps [%& [%atom %t] state]
6692+ ?: ?=(%text -.i.ps) $(ps t.ps)
6693+ =/ item=iresult (infer-fragment p.i.ps env state)
6694+ ?: ?=(%| -.item) item
6695+ =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
6696+ ?: |(?=(%atom -.t) ?=(%any-atom -.t))
6697+ $(ps t.ps, state state.p.item)
6698+ ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
6699+ $(ps t.ps, state state.p.item)
6700+ ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
6701+ $(ps t.ps, state state.p.item)
6702+ ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
6703+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
6704+ ?: ?=(%cell -.t)
6705+ [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
6706+ [%| ["interpolation type needs unsupported inference" ~]]
6707+::
6708+:: Whole-case coverage for a known union. When a pattern may cover only
6709+:: part of a case, finite loobean refinements are tried below; other
6710+:: partial coverage stays unsupported until the general pattern matrix.
6711++$ imatch ?(%full %none %unknown)
6712+++ union-pattern-items
6713+ |= [ps=(list pattern) t=itype]
6714+ ^- imatch
6715+ ?~ ps %unknown
6716+ ?~ t.ps (union-pattern i.ps t)
6717+ =. t ?:(?=(%face -.t) body.t t)
6718+ ?. ?=(%cell -.t)
6719+ ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
6720+ %unknown
6721+ =/ a=imatch (union-pattern i.ps hed.t)
6722+ =/ b=imatch $(ps t.ps, t tal.t)
6723+ ?: |(=(%none a) =(%none b)) %none
6724+ ?:(&(=(%full a) =(%full b)) %full %unknown)
6725+::
6726+++ union-pattern
6727+ |= [p=pattern t=itype]
6728+ ^- imatch
6729+ =. t ?:(?=(%face -.t) body.t t)
6730+ ?- -.p
6731+ %any %full
6732+ %bind %full
6733+ %lit
6734+ ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
6735+ ?: ?=(%cell -.t) %none
6736+ ?: ?=(%flag -.t)
6737+ ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
6738+ %unknown
6739+ %str ?:(?=(%cell -.t) %none %unknown)
6740+ %cell (union-pattern-items items.p t)
6741+ ==
6742+::
6743+++ union-pattern-has-bind
6744+ |= p=pattern
6745+ ^- ?
6746+ ?: ?=(%bind -.p) &
6747+ ?. ?=(%cell -.p) |
6748+ (lien items.p union-pattern-has-bind)
6749+::
6750+++ union-pattern-bind-items
6751+ |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
6752+ ^- (unit ienv)
6753+ ?~ ps ~
6754+ ?~ t.ps (union-pattern-bind i.ps t env globals)
6755+ =. t ?:(?=(%face -.t) body.t t)
6756+ ?. ?=(%cell -.t) ~
6757+ =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
6758+ ?~ first ~
6759+ $(ps t.ps, t tal.t, env u.first)
6760+::
6761+++ union-pattern-bind
6762+ |= [p=pattern t=itype env=ienv globals=(list term)]
6763+ ^- (unit ienv)
6764+ =. t ?:(?=(%face -.t) body.t t)
6765+ ?: ?=(%bind -.p)
6766+ ?: |(?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
6767+ `[[name.p [t ~]] env]
6768+ ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
6769+ `env
6770+::
6771+:: Split loobean fields into finite refinements for partial patterns.
6772+:: Keep original cases for binder types and preserve whole-case matching
6773+:: before trying refinements. Cap products at 64; unknown, empty or opaque
6774+:: shapes stay unsupported rather than implying complete pattern checking.
6775++$ ifinite [origin=@ud base=itype part=itype]
6776+++ finite-product
6777+ |= [hs=(list itype) ts=(list itype) out=(list itype)]
6778+ ^- (list itype)
6779+ ?~ hs out
6780+ =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
6781+ $(hs t.hs, out (weld rows out))
6782+::
6783+++ finite-type
6784+ |= t=itype
6785+ ^- (unit (list itype))
6786+ ?- -.t
6787+ %flag
6788+ `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
49306789 %face
4931− ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
4932− [%| "sample shadows a name"]
4933− =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
4934− ?~ t [%| "sample mold is not supported by partial inference"]
4935− [%& typ.u.t [[name.s [typ.u.t ~]] env] state.u.t]
4936− %bare
4937− =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
4938− ?~ t [%| "sample mold is not supported by partial inference"]
4939− [%& typ.u.t env state.u.t]
4940− * [%| "sample is not supported by partial inference"]
6790+ =/ body=(unit (list itype)) $(t body.t)
6791+ ?~ body ~
6792+ `(turn u.body |=(x=itype [%face name.t x]))
6793+ %cell
6794+ =/ hed=(unit (list itype)) $(t hed.t)
6795+ ?~ hed ~
6796+ =/ tal=(unit (list itype)) $(t tal.t)
6797+ ?~ tal ~
6798+ ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
6799+ `(finite-product u.hed u.tal ~)
6800+ * `~[t]
6801+ ==
6802+::
6803+++ finite-cases
6804+ |= [xs=(list itype) out=(list ifinite) origin=@ud]
6805+ ^- (unit (list ifinite))
6806+ ?~ xs `out
6807+ =/ parts=(unit (list itype)) (finite-type i.xs)
6808+ ?~ parts ~
6809+ ?: (gth (add (lent out) (lent u.parts)) 64) ~
6810+ =/ rows=(list ifinite) (turn u.parts |=(t=itype [origin i.xs t]))
6811+ $(xs t.xs, out (weld out rows), origin +(origin))
6812+::
6813+++ infer-known-union-whole
6814+ |= [e=expr env=ienv state=istate]
6815+ ^- (unit iresult)
6816+ ?> ?=(%branch -.e)
6817+ =/ subject=iresult (infer-fragment subject.e env state)
6818+ ?: ?=(%| -.subject) `subject
6819+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6820+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
6821+ =/ cases=(list itype) cases.typ
6822+ =/ remaining=(list itype) cases
6823+ =/ arms=(list arm) arms.e
6824+ =/ st=istate state.p.subject
6825+ =/ answer=(unit itype) ~
6826+ |-
6827+ ?~ arms
6828+ ?^ remaining
6829+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
6830+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
6831+ `[%& u.answer st]
6832+ =/ a=arm i.arms
6833+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
6834+ ~
6835+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
6836+ ?~ matching
6837+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
6838+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6839+ `[%| ["union pattern is not supported by partial inference" ~]]
6840+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
6841+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6842+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
6843+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
6844+ =/ body=iresult (infer-fragment val.a u.bound st)
6845+ ?: ?=(%| -.body) `body
6846+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
6847+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
6848+ ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
6849+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
6850+::
6851+++ infer-known-union-finite
6852+ |= [e=expr env=ienv state=istate]
6853+ ^- iresult
6854+ ?> ?=(%branch -.e)
6855+ =/ subject=iresult (infer-fragment subject.e env state)
6856+ ?: ?=(%| -.subject) subject
6857+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6858+ ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
6859+ =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
6860+ ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
6861+ =/ cases=(list ifinite) u.expanded
6862+ =/ remaining=(list ifinite) cases
6863+ =/ arms=(list arm) arms.e
6864+ =/ st=istate state.p.subject
6865+ =/ answer=(unit itype) ~
6866+ |-
6867+ ?~ arms
6868+ ?^ remaining
6869+ [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
6870+ ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
6871+ [%& u.answer st]
6872+ =/ a=arm i.arms
6873+ ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
6874+ [%| ["partial union pattern is not supported by partial inference" ~]]
6875+ =/ matching=(list ifinite) (skim remaining |=(c=ifinite =(%full (union-pattern pat.a part.c))))
6876+ ?~ matching
6877+ ?: (lien cases |=(c=ifinite =(%full (union-pattern pat.a part.c))))
6878+ [%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6879+ [%| ["union pattern is not supported by partial inference" ~]]
6880+ ?: &((union-pattern-has-bind pat.a) (lien t.matching |=(c=ifinite !=(origin.c origin.i.matching))))
6881+ [%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6882+ =/ bound=(unit ienv) (union-pattern-bind pat.a base.i.matching env globals.st)
6883+ ?~ bound [%| ["pattern binder shadows a name" ~]]
6884+ =/ body=iresult (infer-fragment val.a u.bound st)
6885+ ?: ?=(%| -.body) body
6886+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
6887+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
6888+ ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
6889+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
6890+::
6891+++ infer-known-union-branch
6892+ |= [e=expr env=ienv state=istate]
6893+ ^- iresult
6894+ =/ whole=(unit iresult) (infer-known-union-whole e env state)
6895+ ?~ whole (infer-known-union-finite e env state)
6896+ u.whole
6897+::
6898+++ known-union-subject
6899+ |= [e=expr env=ienv state=istate]
6900+ ^- (unit itype)
6901+ ?. ?=(%wing -.e) ~
6902+ =/ subject=iresult (infer-fragment e env state)
6903+ ?: ?=(%| -.subject) ~
6904+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6905+ ?. ?=(%union -.typ) ~
6906+ `typ
6907+::
6908+:: Infer changes only against a fully known record spine. Retain the
6909+:: target type; unknown spines and repeated edits remain unsupported.
6910+++ change-spine-known
6911+ |= [t=itype sub=isub]
6912+ ^- ?
6913+ =. t (itype-walk t sub)
6914+ ?: ?=(%face -.t) &
6915+ ?. ?=(%cell -.t) |
6916+ =/ first=itype (itype-walk hed.t sub)
6917+ ?. ?=(%face -.first) |
6918+ $(t tal.t)
6919+::
6920+++ infer-change-edits
6921+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
6922+ ^- iresult
6923+ ?~ edits [%& target state]
6924+ =/ entry=edit i.edits
6925+ ?: (lien seen |=(name=term =(name name.entry)))
6926+ [%| ["repeated change fields are not supported by partial inference" ~]]
6927+ ?. (change-spine-known target sub.state)
6928+ [%| ["change target needs a known record in partial inference" ~]]
6929+ =/ found=(list itype) (record-fields-named name.entry target sub.state)
6930+ ?~ found
6931+ [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
6932+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
6933+ =/ expected=itype i.found
6934+ =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
6935+ ?: ?=(%| -.value) value
6936+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
6937+ ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
6938+ ?: ?=(%bad -.fit)
6939+ [%| ["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)]]]]
6940+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
6941+::
6942+:: Backtick constructs the canonical prelude unit, after checking its
6943+:: prepared template has the standard null and [~ u=A] cases.
6944+++ standard-unit-template
6945+ |= [template=ischeme at=path]
6946+ ^- ?
6947+ ?. =(at /lib/jibb/prelude/jibb) |
6948+ ?~ vars.template |
6949+ ?^ t.vars.template |
6950+ =/ v=@ud i.vars.template
6951+ =/ nil=itype [%const [%null %n 0 '~']]
6952+ =/ expected=itype
6953+ [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
6954+ =(typ.template expected)
6955+::
6956+:: A named missing-case diagnostic needs more than a failed fit: a case
6957+:: with that tag but the wrong payload is not a missing case. Unknown
6958+:: shapes and atom types that accept terms keep the proof conservative.
6959++$ itag-presence ?(%yes %no %maybe)
6960+++ tag-presence-cases
6961+ |= [cases=(list itype) value=@ sub=isub]
6962+ ^- itag-presence
6963+ ?~ cases %no
6964+ =/ first=itag-presence (tag-presence i.cases value sub)
6965+ ?: =(%yes first) %yes
6966+ =/ rest=itag-presence $(cases t.cases)
6967+ ?: =(%yes rest) %yes
6968+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
6969+ %no
6970+::
6971+++ tag-presence
6972+ |= [t=itype value=@ sub=isub]
6973+ ^- itag-presence
6974+ =. t (itype-walk t sub)
6975+ ?- -.t
6976+ %const ?:(=(value val.literal.t) %yes %no)
6977+ %flag ?:(|(=(value 0) =(value 1)) %yes %no)
6978+ %atom ?:(|(=(%tas aura.t) =(%ta aura.t)) %maybe %no)
6979+ %face $(t body.t)
6980+ %cell
6981+ =/ first=itag-presence $(t hed.t)
6982+ ?: =(%yes first) %yes
6983+ =/ rest=itag-presence $(t tal.t)
6984+ ?: =(%yes rest) %yes
6985+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
6986+ %no
6987+ %union (tag-presence-cases cases.t value sub)
6988+ * %maybe
49416989 ==
49426990::
6991+++ missing-union-tag
6992+ |= [e=expr expected=itype sub=isub context=span]
6993+ ^- (unit idiag)
6994+ ?. ?=(%lit -.e) ~
6995+ ?. =(%term form.lit.e) ~
6996+ =. expected (itype-walk expected sub)
6997+ |-
6998+ ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
6999+ ?. ?=(%union -.expected) ~
7000+ ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
7001+ =/ label=tape
7002+ ?~ label.expected "union {(show-itype expected sub)}"
7003+ (show-itype expected sub)
7004+ `["{label} has no case `{(trip txt.lit.e)}`" ~[[context "expected union"] [(span-of e) "tag"]]]
7005+::
49437006++ infer-fragment
49447007 |= [e=expr env=ienv state=istate]
49457008 ^- iresult
@@ -4947,105 +7010,331 @@
49477010 %lit
49487011 ?- form.lit.e
49497012 %number ?: =(%ud aura.lit.e)
4950− [%& [%avar next.state] state(next +(next.state))]
7013+ [%& [%nvar next.state] state(next +(next.state))]
49517014 [%& [%atom aura.lit.e] state]
49527015 %ship [%& [%atom %p] state]
49537016 %date [%& [%atom %da] state]
49547017 %duration [%& [%atom %dr] state]
49557018 %knot [%& [%atom %ta] state]
49567019 %loobean [%& [%flag ~] state]
4957− * [%| "literal needs contextual inference"]
7020+ %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
7021+ %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
49587022 ==
4959− %str
4960− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
4961− ?: interpolated [%| "interpolation is not supported by partial inference"]
4962− [%& [%atom %t] state]
7023+ %unit
7024+ ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
7025+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7026+ ?~ standard [%| ["unit construction needs the standard prelude in partial inference" ~]]
7027+ ?. (standard-unit-template u.standard at.u.prelude.state)
7028+ [%| ["unit construction needs the standard prelude in partial inference" ~]]
7029+ =/ value=iresult $(e val.e)
7030+ ?: ?=(%| -.value) value
7031+ =/ result=(unit itype) (template-apply u.standard ~[typ.p.value])
7032+ ?~ result [%| ["unit construction is not supported by partial inference" ~]]
7033+ [%& u.result state.p.value]
7034+ %str (infer-string-pieces pieces.e env state)
49637035 %wing
4964− ?~ names.e [%| "empty wing"]
4965− ?^ t.names.e [%| "field access is not supported by partial inference"]
7036+ ?~ names.e [%| ["empty wing" ~]]
7037+ ?^ t.names.e
7038+ ?^ t.t.names.e (infer-field-wing names.e env state)
7039+ =/ iface=(unit ifile) (find-jibb-interface i.t.names.e jimports.state)
7040+ ?~ iface (infer-field-wing names.e env state)
7041+ =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
7042+ ?~ member [%| ["module member is not available to partial inference" ~]]
7043+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e)
7044+ =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
7045+ [%& typ.instance state.instance]
49667046 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
4967− ?~ scheme [%| "name is not available to partial inference"]
7047+ ?~ scheme
7048+ ?~ prelude.state [%| ["name is not available to partial inference" ~]]
7049+ =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
7050+ ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
7051+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.prelude-entry state)
7052+ [%& typ.inst state.inst]
49687053 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
49697054 [%& typ.instance state.instance]
49707055 %group $(e inner.e)
7056+ %change
7057+ ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
7058+ =/ target=iresult $(e [%wing at.e target.e])
7059+ ?: ?=(%| -.target) target
7060+ (infer-change-edits edits.e typ.p.target env state.p.target ~)
7061+ %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
7062+ %trace
7063+ =/ traced=iresult $(e val.e)
7064+ ?: ?=(%| -.traced) traced
7065+ $(e then.e, state state.p.traced)
49717066 %tuple (infer-simple-items items.e env state)
49727067 %body
4973− ?^ defs.e [%| "local definitions are not supported by partial inference"]
4974− $(e final.e)
7068+ ?~ defs.e $(e final.e)
7069+ =/ local-names=(list term) (global-value-names defs.e)
7070+ ?. (local-names-valid defs.e env state)
7071+ [%| ["local definitions shadow a name" ~]]
7072+ =/ local-molds=imolds (collect-simple-molds defs.e)
7073+ ?. (local-mold-names-valid local-molds state)
7074+ [%| ["local molds shadow a name" ~]]
7075+ =/ local-state=istate
7076+ state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
7077+ ?. (local-molds-supported local-molds local-state)
7078+ [%| ["local molds need unsupported inference" ~]]
7079+ =/ values=(list def) (local-value-defs defs.e)
7080+ =/ locals=ilocal-result (infer-local-defs values env local-state)
7081+ ?: ?=(%| -.locals) locals
7082+ =/ result=iresult $(e final.e, env env.p.locals, state state.p.locals)
7083+ ?: ?=(%| -.result) result
7084+ [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
49757085 %branch
4976− ?~ arms.e [%| "branch is not supported by partial inference"]
7086+ ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
49777087 ?~ t.arms.e (infer-cell-branch e env state)
4978− ?^ t.t.arms.e [%| "branch is not supported by partial inference"]
7088+ ?^ t.t.arms.e (infer-known-union-branch e env state)
7089+ =/ known=(unit itype) (known-union-subject subject.e env state)
7090+ ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
7091+ (infer-known-union-branch e env state)
49797092 =/ x=arm i.arms.e
49807093 =/ y=arm i.t.arms.e
4981− ?. ?=(%lit -.pat.x) [%| "branch pattern is not supported by partial inference"]
4982− ?. ?=(%lit -.pat.y) [%| "branch pattern is not supported by partial inference"]
7094+ ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
7095+ (infer-unit-branch e env state ~)
7096+ ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7097+ ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
49837098 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
4984− [%| "branch pattern is not supported by partial inference"]
7099+ (infer-known-union-branch e env state)
7100+ ?^ known (infer-known-union-branch e env state)
49857101 ?: =(val.lit.pat.x val.lit.pat.y)
4986− [%| "branch does not cover both loobeans"]
7102+ [%| ["branch does not cover both loobeans" ~]]
49877103 =/ subject=iresult $(e subject.e)
49887104 ?: ?=(%| -.subject) subject
7105+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
7106+ ?: ?=(%union -.subject-type)
7107+ [%| ["union-pattern branch subject is not supported by partial inference" ~]]
49897108 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
4990− ?~ su [%| "loobean branch subject does not unify with ?"]
7109+ ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
49917110 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
49927111 ?: ?=(%| -.left) left
49937112 =/ right=iresult $(e val.y, state state.p.left)
49947113 ?: ?=(%| -.right) right
7114+ =/ ltype=itype (itype-normalize typ.p.left sub.state.p.right)
7115+ =/ rtype=itype (itype-normalize typ.p.right sub.state.p.right)
7116+ ?: &(!=(ltype rtype) |(?=(^ (itype-vars ltype)) ?=(^ (itype-vars rtype))) |((itype-has-fixed-atom ltype) (itype-has-fixed-atom rtype)))
7117+ [%| ["branch widening is not supported by partial inference" ~]]
49957118 =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
4996− ?~ joined [%| "branch arms have incompatible types"]
7119+ ?~ joined
7120+ ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
7121+ [%| ["recursive branch matching is not supported by partial inference" ~]]
7122+ ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
7123+ [%| ["branch tag or union context is not supported by partial inference" ~]]
7124+ =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
7125+ ?^ common [%& u.common state.p.right]
7126+ ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))
7127+ [%| ["record branch matching is not supported by partial inference" ~]]
7128+ ?: |((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))
7129+ [%| ["branch widening is not supported by partial inference" ~]]
7130+ [%| ["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)]]]]
49977131 [%& typ.p.left state.p.right(sub u.joined)]
49987132 %cast
49997133 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
5000− ?~ target [%| "cast mold is not supported by partial inference"]
5001− =/ value=iresult $(e val.e, state state.u.target)
7134+ ?~ target
7135+ =/ diag=(unit idiag) (nested-import-invalid shape.e state)
7136+ ?^ diag [%| u.diag]
7137+ [%| ["cast mold is not supported by partial inference" ~]]
7138+ =/ value=iresult
7139+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
50027140 ?: ?=(%| -.value) value
5003− =/ uni=(unit isub) (itype-unify typ.u.target typ.p.value sub.state.p.value)
5004− ?~ uni [%| "cast mold and expression type do not unify"]
5005− [%& typ.u.target state.p.value(sub u.uni)]
7141+ =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
7142+ ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
7143+ ?: ?=(%bad -.fit)
7144+ =/ missing=(unit idiag) (missing-union-tag val.e typ.u.target sub.state.p.value at.shape.e)
7145+ ?^ missing [%| u.missing]
7146+ [%| ["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)]]]]
7147+ =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
7148+ [%& merged state.p.value(sub sub.fit, next next.fit)]
50067149 %crash [%& [%var next.state] state(next +(next.state))]
50077150 %gate
50087151 =/ sam=isample-result (infer-sample sample.e env state)
5009− ?: ?=(%| -.sam) [%| p.sam]
7152+ ?: ?=(%| -.sam)
7153+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7154+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7155+ [%| [p.sam ~]]
50107156 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
50117157 ?: ?=(%| -.body) body
50127158 [%& [%fn typ.p.sam typ.p.body] state.p.body]
50137159 %gate-wide
50147160 =/ sam=isample-result (infer-sample sample.e env state)
5015− ?: ?=(%| -.sam) [%| p.sam]
7161+ ?: ?=(%| -.sam)
7162+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7163+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7164+ [%| [p.sam ~]]
50167165 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
50177166 ?: ?=(%| -.body) body
50187167 [%& [%fn typ.p.sam typ.p.body] state.p.body]
50197168 %call
5020− ?~ args.e [%| "call has no argument"]
5021− ?^ t.args.e [%| "multiple arguments are not supported by partial inference"]
7169+ ?~ args.e [%| ["call has no argument" ~]]
50227170 =/ head=iresult $(e head.e)
50237171 ?: ?=(%| -.head) head
5024− =/ arg=iresult $(e i.args.e, state state.p.head)
7172+ =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
7173+ =/ arg=iresult
7174+ ?^ t.args.e
7175+ ?: ?=(%fn -.head-type)
7176+ (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
7177+ (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
7178+ ?: ?=(%fn -.head-type)
7179+ (infer-call-context-arg i.args.e sample.head-type env state.p.head (span-of head.e))
7180+ $(e i.args.e, state state.p.head)
50257181 ?: ?=(%| -.arg) arg
50267182 =/ st=istate state.p.arg
7183+ =/ ht=itype (itype-walk typ.p.head sub.st)
7184+ ?: ?=(%fn -.ht)
7185+ =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
7186+ ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
7187+ ?: ?=(%bad -.fit)
7188+ ?~ t.args.e
7189+ =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
7190+ ?^ missing [%| u.missing]
7191+ [%| ["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)]]]]
7192+ =/ bad=(unit [at=span typ=itype])
7193+ (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
7194+ =/ whole-args=span
7195+ [beg:(span-of i.args.e) end:(span-of (rear args.e))]
7196+ =/ arg-at=span ?~(bad whole-args at.u.bad)
7197+ =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7198+ [%| ["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)]]]]
7199+ ?: &((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))
7200+ [%| ["call result face propagation is not supported by partial inference" ~]]
7201+ [%& product.ht st(sub sub.fit, next next.fit)]
50277202 =/ result=itype [%var next.st]
5028− =/ uni=(unit isub)
5029− (itype-unify typ.p.head [%fn typ.p.arg result] sub.st)
5030− ?~ uni [%| "call's sample and argument types do not unify"]
7203+ =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
7204+ ?~ uni
7205+ [%| ["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)]]]]
50317206 [%& result st(next +(next.st), sub u.uni)]
5032− * [%| "expression is not supported by partial inference"]
7207+ * [%| ["expression is not supported by partial inference" ~]]
50337208 ==
50347209::
5035−:: Unfaced tuple expressions are the one supported cell construction.
5036−:: Faced cells wait for the representation to preserve record faces.
7210+:: Locate a definite failing argument after the complete sample fit has
7211+:: failed. If an intermediate fit is uncertain, retain the whole argument
7212+:: span rather than assigning blame to a particular argument.
7213+::
7214+++ call-error-site
7215+ |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
7216+ ^- (unit [at=span typ=itype])
7217+ ?~ args ~
7218+ =/ original=[left=itype right=itype] [actual expected]
7219+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7220+ =. actual (itype-walk actual sub)
7221+ =. expected (itype-walk expected sub)
7222+ ?: &(?=(%face -.expected) !?=(%face -.actual))
7223+ $(expected body.expected)
7224+ ?~ t.args
7225+ =/ fit=ifit (itype-fit actual expected sub next)
7226+ ?. ?=(%bad -.fit) ~
7227+ `[(span-of i.args) (itype-normalize actual sub)]
7228+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7229+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7230+ ?: ?=(%bad -.first) `[(span-of i.args) (itype-normalize hed.actual sub)]
7231+ ?: ?=(%unknown -.first) ~
7232+ $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7233+::
7234+:: Context can help a call argument or cast value while the final fit
7235+:: checks the complete right-nested type, including any written faces.
7236+::
7237+:: Context can resolve the payload of a canonical prelude unit, but an
7238+:: unrelated union with a similar noun shape is not the same mold.
7239+++ infer-unit-context
7240+ |= [e=expr expected=itype env=ienv state=istate context=span]
7241+ ^- iresult
7242+ ?> ?=(%unit -.e)
7243+ ?> ?=(%union -.expected)
7244+ ?~ prelude.state (infer-fragment e env state)
7245+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7246+ ?~ standard (infer-fragment e env state)
7247+ ?. (standard-unit-template u.standard at.u.prelude.state) (infer-fragment e env state)
7248+ ?. =(origin.expected `[at.u.prelude.state %unit]) (infer-fragment e env state)
7249+ ?~ args.expected (infer-fragment e env state)
7250+ ?^ t.args.expected (infer-fragment e env state)
7251+ =/ payload=itype i.args.expected
7252+ =/ canonical=(unit itype) (template-apply u.standard ~[payload])
7253+ ?~ canonical (infer-fragment e env state)
7254+ ?> ?=(%union -.u.canonical)
7255+ ?. =((itype-normalize expected(label ~) sub.state) (itype-normalize u.canonical(label ~) sub.state))
7256+ (infer-fragment e env state)
7257+ =/ value=iresult (infer-call-context-arg val.e payload env state context)
7258+ ?: ?=(%| -.value) value
7259+ =/ fit=ifit (itype-fit typ.p.value payload sub.state.p.value next.state.p.value)
7260+ ?: ?=(%unknown -.fit) [%| ["unit payload constraint is not supported by partial inference" ~]]
7261+ ?: ?=(%bad -.fit)
7262+ =/ missing=(unit idiag) (missing-union-tag val.e payload sub.state.p.value context)
7263+ ?^ missing [%| u.missing]
7264+ [%| ["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)]]]]
7265+ [%& expected state.p.value(sub sub.fit, next next.fit)]
7266+::
7267+++ infer-call-context-arg
7268+ |= [e=expr expected=itype env=ienv state=istate context=span]
7269+ ^- iresult
7270+ =/ target=itype (itype-walk expected sub.state)
7271+ |-
7272+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7273+ ?: &(?=(%union -.target) ?=(%unit -.e))
7274+ (infer-unit-context e target env state context)
7275+ ?: &(?=(%union -.target) (context-union-branch e))
7276+ (infer-union-context e target env state context)
7277+ ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
7278+ (infer-union-context e target env state context)
7279+ ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
7280+ (infer-list-context e target env state context)
7281+ ?: &(?=(%cell -.target) ?=(%tuple -.e))
7282+ (infer-call-context-items items.e target env state context)
7283+ (infer-fragment e env state)
7284+::
7285+:: Preserve each written face; the final complete sample fit checks faces.
7286+++ infer-call-context-items
7287+ |= [items=(list item) expected=itype env=ienv state=istate context=span]
7288+ ^- iresult
7289+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
7290+ ?~ t.items
7291+ =/ last=iresult (infer-call-context-arg val.i.items expected env state context)
7292+ ?: ?=(%| -.last) last
7293+ =/ typ=itype typ.p.last
7294+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7295+ [%& typ state.p.last]
7296+ =/ target=itype (itype-walk expected sub.state)
7297+ |-
7298+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7299+ ?. ?=(%cell -.target) (infer-simple-items items env state)
7300+ =/ head=iresult (infer-call-context-arg val.i.items hed.target env state context)
7301+ ?: ?=(%| -.head) head
7302+ =/ typ=itype typ.p.head
7303+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7304+ =/ tail=iresult (infer-call-context-items t.items tal.target env state.p.head context)
7305+ ?: ?=(%| -.tail) tail
7306+ [%& [%cell typ typ.p.tail] state.p.tail]
7307+::
7308+++ infer-call-context-args
7309+ |= [args=(list expr) expected=itype env=ienv state=istate context=span]
7310+ ^- iresult
7311+ ?~ args [%| ["call has no argument" ~]]
7312+ ?~ t.args (infer-call-context-arg i.args expected env state context)
7313+ =/ target=itype (itype-walk expected sub.state)
7314+ |-
7315+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7316+ ?. ?=(%cell -.target)
7317+ (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
7318+ =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
7319+ ?: ?=(%| -.head) head
7320+ =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
7321+ ?: ?=(%| -.tail) tail
7322+ [%& [%cell typ.p.head typ.p.tail] state.p.tail]
7323+::
7324+:: Tuple and record expressions preserve their explicitly written faces.
50377325::
50387326++ infer-simple-items
50397327 |= [items=(list item) env=ienv state=istate]
50407328 ^- iresult
5041− ?~ items [%| "empty cell is not supported by partial inference"]
5042− ?^ face.i.items [%| "record faces are not supported by partial inference"]
7329+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
50437330 =/ head=iresult (infer-fragment val.i.items env state)
50447331 ?: ?=(%| -.head) head
5045− ?~ t.items head
7332+ =/ ht=itype typ.p.head
7333+ =. ht ?~(face.i.items ht [%face u.face.i.items ht])
7334+ ?~ t.items [%& ht state.p.head]
50467335 =/ tail=iresult $(items t.items, state state.p.head)
50477336 ?: ?=(%| -.tail) tail
5048− [%& [%cell typ.p.head typ.p.tail] state.p.tail]
7337+ [%& [%cell ht typ.p.tail] state.p.tail]
50497338::
50507339:: A single two-binder cell pattern covers every value of a cell type.
50517340:: No other pattern matrix is implemented here.
@@ -5054,26 +7343,30 @@
50547343 |= [e=expr env=ienv state=istate]
50557344 ^- iresult
50567345 ?> ?=(%branch -.e)
5057− ?~ arms.e [%| "branch is not supported by partial inference"]
7346+ ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
50587347 =/ arm=arm i.arms.e
5059− ?. ?=(%cell -.pat.arm) [%| "branch pattern is not supported by partial inference"]
7348+ ?. ?=(%cell -.pat.arm) [%| ["branch pattern is not supported by partial inference" ~]]
50607349 =/ pats=(list pattern) items.pat.arm
5061− ?~ pats [%| "branch pattern is not supported by partial inference"]
5062− ?~ t.pats [%| "branch pattern is not supported by partial inference"]
5063− ?^ t.t.pats [%| "branch pattern is not supported by partial inference"]
5064− ?. ?=(%bind -.i.pats) [%| "branch pattern is not supported by partial inference"]
5065− ?. ?=(%bind -.i.t.pats) [%| "branch pattern is not supported by partial inference"]
7350+ ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
7351+ ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
7352+ ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
7353+ ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
7354+ ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
50667355 =/ one=term name.i.pats
50677356 =/ two=term name.i.t.pats
50687357 ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
5069− [%| "pattern shadows a name"]
7358+ [%| ["pattern shadows a name" ~]]
50707359 =/ subject=iresult (infer-fragment subject.e env state)
50717360 ?: ?=(%| -.subject) subject
50727361 =/ st=istate state.p.subject
7362+ ?: (itype-has-recursive (itype-normalize typ.p.subject sub.st))
7363+ [%| ["recursive pattern is not supported by partial inference" ~]]
7364+ ?: (itype-has-face typ.p.subject sub.st)
7365+ [%| ["record patterns are not supported by partial inference" ~]]
50737366 =/ head=itype [%var next.st]
50747367 =/ tail=itype [%var +(next.st)]
50757368 =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
5076− ?~ sub [%| "cell pattern does not match the subject type"]
7369+ ?~ sub [%| ["cell pattern does not match the subject type" ~]]
50777370 (infer-fragment val.arm [[one [head ~]] [two [tail ~]] env] st(next (add 2 next.st), sub u.sub))
50787371::
50797372++ show-itype
@@ -5084,44 +7377,223 @@
50847377 %var
50857378 ?: (lth id.t 26) [(add 65 id.t) ~]
50867379 "T{<id.t>}"
5087− %avar "@"
7380+ %avar
7381+ ?: (lth id.t 26) [(add 65 id.t) ~]
7382+ "T{<id.t>}"
7383+ %nvar
7384+ ?: (lth id.t 26) [(add 65 id.t) ~]
7385+ "T{<id.t>}"
50887386 %atom "@{(trip aura.t)}"
7387+ %any-atom "@"
50897388 %flag "?"
5090− %fn "$-({$(t sample.t)} {$(t product.t)})"
5091− %cell "[{$(t hed.t)} {$(t tal.t)}]"
7389+ %tag (trip txt.literal.t)
7390+ %const (trip txt.literal.t)
7391+ %union
7392+ ?~ label.t (show-itype-cases cases.t sub)
7393+ ?~ args.t (trip u.label.t)
7394+ "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
7395+ %recursive ?~(label.t "recursive mold" (trip u.label.t))
7396+ %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
7397+ %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
7398+ %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
7399+ %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
50927400 ==
50937401::
5094−:: Unfixed aura variables are withheld from the output until inference
5095−:: can generalize them and the printer represents their constraints.
7402+++ show-itype-item
7403+ |= [t=itype sub=isub]
7404+ ^- tape
7405+ =. t (itype-walk t sub)
7406+ ?: ?=(%face -.t) "{(trip name.t)}={(show-itype-context body.t sub)}"
7407+ (show-itype-context t sub)
7408+::
7409+++ show-itype-context
7410+ |= [t=itype sub=isub]
7411+ ^- tape
7412+ =. t (itype-walk t sub)
7413+ ?: &(?=(%union -.t) ?=(~ label.t)) "({(show-itype t sub)})"
7414+ (show-itype t sub)
7415+::
7416+++ show-itype-cases
7417+ |= [cases=(list itype) sub=isub]
7418+ ^- tape
7419+ ?~ cases ""
7420+ ?~ t.cases (show-itype-context i.cases sub)
7421+ "{(show-itype-context i.cases sub)} {$(cases t.cases)}"
7422+::
7423+:: Include the type at a conflicting site where it can be printed.
7424+:: A lone unresolved variable or decimal variable keeps the neutral label.
50967425::
5097−++ itype-has-avar
5098− |= t=itype
7426+++ itype-has-nvar
7427+ |= typ=itype
50997428 ^- ?
5100− ?- -.t
5101− %avar &
5102− %var |
5103− %atom |
5104− %flag |
5105− %fn |($(t sample.t) $(t product.t))
5106− %cell |($(t hed.t) $(t tal.t))
7429+ ?- -.typ
7430+ %nvar &
7431+ %var |
7432+ %avar |
7433+ %atom |
7434+ %any-atom |
7435+ %flag |
7436+ %tag |
7437+ %const |
7438+ %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
7439+ %recursive |
7440+ %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
7441+ %face $(typ body.typ)
7442+ %fn |($(typ sample.typ) $(typ product.typ))
7443+ %cell |($(typ hed.typ) $(typ tal.typ))
51077444 ==
51087445::
7446+++ site-type-note
7447+ |= [label=tape typ=itype sub=isub]
7448+ ^- tape
7449+ =/ normalized=itype (itype-normalize typ sub)
7450+ ?: |(?=(%var -.normalized) ?=(%avar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
7451+ ?: (itype-has-hidden-recursive normalized) label
7452+ =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
7453+ ?: (gth (lent vars) 26) label
7454+ =/ printable=itype (canonical-itype normalized vars)
7455+ "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
7456+::
51097457:: A capital in a written mold is generalized with its enclosing ++.
5110−:: Until its rigidity and aura constraints are represented, do not
5111−:: report a type when unification made one more specific.
7458+:: Atom constraints may remain generic; until full rigidity checking
7459+:: is implemented, do not report a type if one became more specific.
7460+:: Distinct written capitals cannot be forced equal; use the same
7461+:: capital where a type must be shared (Decisions 2026-10-30).
7462+::
7463+++ cap-id-in
7464+ |= [n=@ud caps=icaps sub=isub]
7465+ ^- ?
7466+ ?~ caps |
7467+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7468+ =/ ident=(unit @ud)
7469+ ?+ -.resolved ~
7470+ %var `id.resolved
7471+ %avar `id.resolved
7472+ ==
7473+ ?~ ident $(caps t.caps)
7474+ ?: =(n u.ident) &
7475+ $(caps t.caps)
7476+::
7477+++ cap-with-id
7478+ |= [n=@ud caps=icaps sub=isub]
7479+ ^- (unit icap)
7480+ ?~ caps ~
7481+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7482+ =/ ident=(unit @ud)
7483+ ?+ -.resolved ~
7484+ %var `id.resolved
7485+ %avar `id.resolved
7486+ ==
7487+ ?~ ident $(caps t.caps)
7488+ ?: =(n u.ident) `i.caps
7489+ $(caps t.caps)
7490+::
7491+++ merged-capitals
7492+ |= [caps=icaps sub=isub]
7493+ ^- (unit [first=icap second=icap])
7494+ ?~ caps ~
7495+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7496+ =/ ident=(unit @ud)
7497+ ?+ -.resolved ~
7498+ %var `id.resolved
7499+ %avar `id.resolved
7500+ ==
7501+ ?~ ident $(caps t.caps)
7502+ =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
7503+ ?^ found `[u.found i.caps]
7504+ $(caps t.caps)
51127505::
51137506++ constrained-capitals
51147507 |= [caps=icaps sub=isub]
51157508 ^- ?
51167509 ?~ caps |
51177510 =/ resolved=itype (itype-walk [%var id.i.caps] sub)
5118− ?. ?=(%var -.resolved) &
7511+ =/ ident=(unit @ud)
7512+ ?+ -.resolved ~
7513+ %var `id.resolved
7514+ %avar `id.resolved
7515+ ==
7516+ ?~ ident &
7517+ ?: (cap-id-in u.ident t.caps sub) &
7518+ $(caps t.caps)
7519+::
7520+:: An atom variable may be generalized when an explicit capital, sample
7521+:: binder or instantiated constraint resolves to it. Decimal variables need
7522+:: defaulting and must not be generalized as arbitrary atom types.
7523+::
7524+++ atom-var-from-cap
7525+ |= [n=@ud caps=icaps sub=isub]
7526+ ^- ?
7527+ ?~ caps |
7528+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7529+ ?: ?=(%avar -.resolved)
7530+ ?: =(n id.resolved) &
7531+ $(caps t.caps)
51197532 $(caps t.caps)
51207533::
7534+++ has-atom-var
7535+ |= [n=@ud t=itype]
7536+ ^- ?
7537+ ?- -.t
7538+ %var |
7539+ %avar =(n id.t)
7540+ %nvar |
7541+ %atom |
7542+ %any-atom |
7543+ %flag |
7544+ %tag |
7545+ %const |
7546+ %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
7547+ %recursive |
7548+ %collection (lien args.t |=(c=itype (has-atom-var n c)))
7549+ %face $(t body.t)
7550+ %fn |($(t sample.t) $(t product.t))
7551+ %cell |($(t hed.t) $(t tal.t))
7552+ ==
7553+::
7554+++ atom-var-from-binder
7555+ |= [n=@ud binders=(list @ud) sub=isub]
7556+ ^- ?
7557+ ?~ binders |
7558+ =/ resolved=itype (itype-normalize [%var i.binders] sub)
7559+ :: An instantiated atom variable is not itself a substitution, so
7560+ :: its origin still walks as an unbound variable of the same ID.
7561+ ?: ?=(%var -.resolved)
7562+ ?: =(n id.resolved) &
7563+ $(binders t.binders)
7564+ ?: (has-atom-var n resolved) &
7565+ $(binders t.binders)
7566+::
7567+++ unsupported-atom-vars
7568+ |= [t=itype caps=icaps binders=(list @ud) sub=isub]
7569+ ^- ?
7570+ =/ vars=(list @ud) (unique-type-vars (itype-vars t))
7571+ |-
7572+ ?~ vars |
7573+ ?: (itype-var-is-atom i.vars t)
7574+ ?. (has-atom-var i.vars t) &
7575+ ?. |((atom-var-from-cap i.vars caps sub) (atom-var-from-binder i.vars binders sub)) &
7576+ $(vars t.vars)
7577+ $(vars t.vars)
7578+::
7579+++ show-atom-constraint
7580+ |= t=itype
7581+ ^- tape
7582+ =/ vars=(list @ud) (unique-type-vars (itype-vars t))
7583+ =/ printed=? |
7584+ =/ out=tape ""
7585+ |-
7586+ ?~ vars out
7587+ ?: (itype-var-is-atom i.vars t)
7588+ =/ sep=tape ?:(printed ", " " where ")
7589+ =/ clause=tape "{sep}{(show-itype [%avar i.vars] ~)} is an atom"
7590+ $(vars t.vars, printed &, out (weld out clause))
7591+ $(vars t.vars)
7592+::
51217593:: Build the supported part of the value environment in dependency order.
51227594:: Each pass adds successful definitions. Forward references become
5123−:: available on a later pass; recursive groups and unsupported syntax do
5124−:: not enter the environment. Generalized definitions are closed, so a
7595+:: available on a later pass; mutually recursive groups and unsupported
7596+:: syntax do not enter the environment. Generalized definitions are closed, so a
51257597:: use instantiates its variables afresh.
51267598::
51277599++ global-value-names
@@ -5140,31 +7612,470 @@
51407612 ?~ t.hits &
51417613 |
51427614::
7615+:: A top-level gate may refer to itself through one monomorphic placeholder.
7616+:: Its declared sample is inferred first and preserves its field faces.
7617+:: Unify the completed body with that placeholder before generalization;
7618+:: reporting repeats the same check instead of instantiating the gate's
7619+:: generalized interface inside its own body. Mutual groups stay unsupported.
7620+::
7621+++ direct-self-call
7622+ |= [e=expr name=term]
7623+ ^- ?
7624+ ?: ?=(%group -.e) $(e inner.e)
7625+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7626+ ?. ?=(%call -.e) |
7627+ ?. ?=(%wing -.head.e) |
7628+ =(names.head.e ~[name])
7629+::
7630+++ branch-base-arm
7631+ |= [e=expr name=term]
7632+ ^- (unit expr)
7633+ ?: ?=(%group -.e) $(e inner.e)
7634+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7635+ ?. ?=(%branch -.e) ~
7636+ ?~ arms.e ~
7637+ ?~ t.arms.e ~
7638+ ?^ t.t.arms.e ~
7639+ =/ x=arm i.arms.e
7640+ =/ y=arm i.t.arms.e
7641+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) ~
7642+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) ~
7643+ ?: =(val.lit.pat.x val.lit.pat.y) ~
7644+ =/ first=? (direct-self-call val.x name)
7645+ =/ second=? (direct-self-call val.y name)
7646+ ?: =(first second) ~
7647+ `?:(first val.y val.x)
7648+::
7649+:: Infer the base arm independently, with the self binding removed. Only
7650+:: a closed type whose constraints resolved can seed the recursive result.
7651+:: The regular body inference then checks both arms with shared state.
7652+::
7653+++ recursive-branch-seed
7654+ |= [d=def env=ienv state=istate]
7655+ ^- (unit itype)
7656+ ?. ?=(%value -.d) ~
7657+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) ~
7658+ =/ gate=expr val.d
7659+ =/ body=expr
7660+ ?- -.gate
7661+ %gate body.gate
7662+ %gate-wide body.gate
7663+ * !!
7664+ ==
7665+ =/ base=(unit expr) (branch-base-arm body name.d)
7666+ ?~ base ~
7667+ =/ outer=ienv (skim env |=(entry=[name=term scheme=ischeme] !=(name.entry name.d)))
7668+ =/ sam=isample-result
7669+ ?- -.gate
7670+ %gate (infer-sample sample.gate outer state)
7671+ %gate-wide (infer-sample sample.gate outer state)
7672+ * !!
7673+ ==
7674+ ?: ?=(%| -.sam) ~
7675+ =/ inferred=iresult (infer-fragment u.base env.p.sam state.p.sam)
7676+ ?: ?=(%| -.inferred) ~
7677+ ?: (pending-tags tags.state.p.inferred sub.state.p.inferred) ~
7678+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred) ~
7679+ =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7680+ ?: ?=(^ (itype-vars typ)) ~
7681+ ?: (itype-has-tag typ) ~
7682+ `typ
7683+::
7684+++ infer-recursive-gate
7685+ |= [d=def env=ienv state=istate]
7686+ ^- iresult
7687+ ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
7688+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
7689+ [%| ["recursive definition is not a gate" ~]]
7690+ =/ result=(unit itype) (recursive-branch-seed d env state)
7691+ =/ gate=expr val.d
7692+ =/ sam=isample-result
7693+ ?- -.gate
7694+ %gate (infer-sample sample.gate env state)
7695+ %gate-wide (infer-sample sample.gate env state)
7696+ * !!
7697+ ==
7698+ ?: ?=(%| -.sam)
7699+ =/ diag=(unit idiag)
7700+ ?- -.gate
7701+ %gate (sample-import-invalid sample.gate env state)
7702+ %gate-wide (sample-import-invalid sample.gate env state)
7703+ * ~
7704+ ==
7705+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7706+ [%| [p.sam ~]]
7707+ =/ id=@ud next.state.p.sam
7708+ =/ product=itype ?~(result [%var id] u.result)
7709+ =/ st=istate state.p.sam(next +(id))
7710+ =/ seed=itype [%fn typ.p.sam product]
7711+ =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
7712+ =/ body=expr
7713+ ?- -.gate
7714+ %gate body.gate
7715+ %gate-wide body.gate
7716+ * !!
7717+ ==
7718+ =/ out=iresult (infer-fragment body seeded st)
7719+ ?: ?=(%| -.out) out
7720+ =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
7721+ ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
7722+ [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
7723+::
7724+++ dependency-root
7725+ |= names=(list term)
7726+ ^- (list term)
7727+ ?~ names ~
7728+ ~[(rear names)]
7729+::
7730+++ dependency-exprs
7731+ |= xs=(list expr)
7732+ ^- (list term)
7733+ ?~ xs ~
7734+ =/ first=(list term) (dependency-expr i.xs)
7735+ (weld first $(xs t.xs))
7736+::
7737+++ dependency-pieces
7738+ |= xs=(list piece)
7739+ ^- (list term)
7740+ ?~ xs ~
7741+ =/ first=(list term)
7742+ ?- -.i.xs
7743+ %expr (dependency-expr p.i.xs)
7744+ %text ~
7745+ ==
7746+ (weld first $(xs t.xs))
7747+::
7748+++ dependency-qsegs
7749+ |= xs=(list qseg)
7750+ ^- (list term)
7751+ ?~ xs ~
7752+ =/ first=(list term)
7753+ ?- -.i.xs
7754+ %expr (dependency-expr p.i.xs)
7755+ %knot ~
7756+ ==
7757+ (weld first $(xs t.xs))
7758+::
7759+++ dependency-items
7760+ |= xs=(list item)
7761+ ^- (list term)
7762+ ?~ xs ~
7763+ =/ first=(list term) (dependency-expr val.i.xs)
7764+ (weld first $(xs t.xs))
7765+::
7766+++ dependency-edits
7767+ |= xs=(list edit)
7768+ ^- (list term)
7769+ ?~ xs ~
7770+ =/ first=(list term) (dependency-expr val.i.xs)
7771+ (weld first $(xs t.xs))
7772+::
7773+++ dependency-arms
7774+ |= xs=(list arm)
7775+ ^- (list term)
7776+ ?~ xs ~
7777+ =/ first=(list term) (dependency-expr val.i.xs)
7778+ (weld first $(xs t.xs))
7779+::
7780+++ dependency-defs
7781+ |= xs=(list def)
7782+ ^- (list term)
7783+ ?~ xs ~
7784+ =/ first=(list term)
7785+ ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
7786+ ~
7787+ (weld first $(xs t.xs))
7788+::
7789+++ dependency-expr
7790+ |= e=expr
7791+ ^- (list term)
7792+ ?- -.e
7793+ %str (dependency-pieces pieces.e)
7794+ %qath (dependency-qsegs segs.e)
7795+ %wing (dependency-root names.e)
7796+ %change
7797+ =/ first=(list term) (dependency-root target.e)
7798+ =/ last=(list term) (dependency-edits edits.e)
7799+ (weld first last)
7800+ %pair (dependency-expr val.e)
7801+ %unit (dependency-expr val.e)
7802+ %group (dependency-expr inner.e)
7803+ %list (dependency-exprs items.e)
7804+ %tuple (dependency-items items.e)
7805+ %gate (dependency-expr body.e)
7806+ %gate-wide (dependency-expr body.e)
7807+ %call
7808+ =/ first=(list term) (dependency-expr head.e)
7809+ =/ last=(list term) (dependency-exprs args.e)
7810+ (weld first last)
7811+ %cast (dependency-expr val.e)
7812+ %trace
7813+ =/ first=(list term) (dependency-expr val.e)
7814+ =/ last=(list term) (dependency-expr then.e)
7815+ (weld first last)
7816+ %branch
7817+ =/ first=(list term) (dependency-expr subject.e)
7818+ =/ last=(list term) (dependency-arms arms.e)
7819+ (weld first last)
7820+ %body
7821+ =/ first=(list term) (dependency-defs defs.e)
7822+ =/ last=(list term) (dependency-expr final.e)
7823+ (weld first last)
7824+ * ~
7825+ ==
7826+::
7827+:: Infer a cyclic top-level component with one monomorphic seed per gate.
7828+:: All members must succeed before any scheme is available; local cyclic
7829+:: groups, pending constraints and unresolved branch joins remain partial.
7830++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
7831++$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
7832+++ seed-gate-group
7833+ |= [ds=(list def) env=ienv state=istate]
7834+ ^- igate-seeds
7835+ ?~ ds [%& [~ state]]
7836+ =/ d=def i.ds
7837+ ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
7838+ =/ gate=expr val.d
7839+ ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
7840+ [%| ["recursive group contains a non-gate" ~]]
7841+ =/ initial=istate (reserve-def-caps gate state)
7842+ =/ sam=isample-result
7843+ ?- -.gate
7844+ %gate (infer-sample sample.gate env initial)
7845+ %gate-wide (infer-sample sample.gate env initial)
7846+ * !!
7847+ ==
7848+ ?: ?=(%| -.sam) [%| [p.sam ~]]
7849+ =/ body=expr
7850+ ?- -.gate
7851+ %gate body.gate
7852+ %gate-wide body.gate
7853+ * !!
7854+ ==
7855+ =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
7856+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
7857+ =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
7858+ =/ rest=igate-seeds $(ds t.ds, state after)
7859+ ?: ?=(%| -.rest) rest
7860+ [%& [[entry entries.p.rest] state.p.rest]]
7861+::
7862+++ group-seed-env
7863+ |= [entries=(list igate-entry) env=ienv]
7864+ ^- ienv
7865+ ?~ entries env
7866+ [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
7867+::
7868+++ infer-gate-group-bodies
7869+ |= [entries=(list igate-entry) seeds=ienv state=istate]
7870+ ^- igate-seeds
7871+ ?~ entries [%& [~ state]]
7872+ =/ entry=igate-entry i.entries
7873+ ?> ?=(%fn -.typ.entry)
7874+ =/ scope=ienv (weld seeds env.entry)
7875+ =/ out=iresult (infer-fragment body.entry scope state(caps caps.entry))
7876+ ?: ?=(%| -.out) out
7877+ =/ uni=(unit isub) (itype-unify product.typ.entry typ.p.out sub.state.p.out)
7878+ ?~ uni [%| ["recursive group constraint is not supported by partial inference" ~]]
7879+ =. caps.entry caps.state.p.out
7880+ =/ after=istate state.p.out(sub u.uni, caps caps.state)
7881+ =/ rest=igate-seeds $(entries t.entries, state after)
7882+ ?: ?=(%| -.rest) rest
7883+ [%& [[entry entries.p.rest] state.p.rest]]
7884+::
7885+++ group-schemes
7886+ |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
7887+ ^- (each ienv idiag)
7888+ ?~ entries [%& ~]
7889+ =/ entry=igate-entry i.entries
7890+ =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
7891+ ?^ merged
7892+ [%| ["distinct type variables must not be forced equal" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
7893+ ?: (constrained-capitals caps.entry sub.state)
7894+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
7895+ =/ typ=itype (itype-normalize typ.entry sub.state)
7896+ ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
7897+ [%| ["recursive group needs unsupported inference" ~]]
7898+ =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
7899+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7900+ =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7901+ ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
7902+ =/ rest=(each ienv idiag) $(entries t.entries)
7903+ ?: ?=(%| -.rest) rest
7904+ [%& [[name.entry [typ vars]] p.rest]]
7905+::
7906+++ infer-gate-group
7907+ |= [ds=(list def) env=ienv state=istate]
7908+ ^- ilocal-result
7909+ =/ names=(list term) (global-value-names ds)
7910+ ?. (levy names |=(n=term (unique-value-name n names)))
7911+ [%| ["recursive group contains duplicate names" ~]]
7912+ ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
7913+ [%| ["recursive group shadows a name" ~]]
7914+ =/ scoped=istate state(globals (weld names globals.state))
7915+ =/ seeded=igate-seeds (seed-gate-group ds env scoped)
7916+ ?: ?=(%| -.seeded) seeded
7917+ =/ seeds=ienv (group-seed-env entries.p.seeded ~)
7918+ =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
7919+ ?: ?=(%| -.body) body
7920+ ?: (pending-tags tags.state.p.body sub.state.p.body)
7921+ [%| ["recursive group has unresolved literal constraints" ~]]
7922+ =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
7923+ ?: ?=(%| -.schemes) schemes
7924+ [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
7925+::
51437926++ add-supported-defs
5144− |= [ds=(list def) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term)]
7927+ |= [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)]
51457928 ^- ienv
51467929 ?~ ds env
51477930 =/ d=def i.ds
51487931 ?: ?=(%mold -.d) $(ds t.ds)
51497932 ?. (unique-value-name name.d globals) $(ds t.ds)
51507933 ?^ (ienv-lookup name.d env) $(ds t.ds)
5151− =/ result=iresult (infer-fragment val.d env [0 ~ ~ molds globals externals surs ~ |])
7934+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7935+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
7936+ =. initial (reserve-def-caps val.d initial)
7937+ =/ result=iresult (infer-fragment val.d env initial)
7938+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
51527939 ?: ?=(%| -.result) $(ds t.ds)
51537940 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
5154− =/ typ=itype (itype-normalize typ.p.result sub.state.p.result)
5155− ?: (itype-has-avar typ) $(ds t.ds)
7941+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
7942+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
7943+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
51567944 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
51577945 ?: (gth (lent vars) 26) $(ds t.ds)
51587946 $(ds t.ds, env [[name.d [typ vars]] env])
51597947::
5160−++ resolve-supported-defs
5161− |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term)]
5162− ^- ienv
7948++$ iresolved [env=ienv grouped=(list term)]
7949++$ iadj (map term (list term))
7950++$ ivisited (map term ?)
7951++$ iwork (list [name=term done=?])
7952++$ iwresult [seen=ivisited order=(list term)]
7953++$ icresult [seen=ivisited component=(list term)]
7954++$ icomponents (list (list term))
7955+++ graph-nameset
7956+ |= [names=(list term) seen=ivisited]
7957+ ^- ivisited
7958+ ?~ names seen
7959+ $(names t.names, seen (~(put by seen) i.names &))
7960+::
7961+++ graph-edges
7962+ |= [name=term graph=iadj]
7963+ ^- (list term)
7964+ =/ found=(unit (list term)) (~(get by graph) name)
7965+ ?~ found ~
7966+ u.found
7967+::
7968+++ graph-make-forward
7969+ |= [ds=(list def) names=ivisited graph=iadj]
7970+ ^- iadj
7971+ ?~ ds graph
7972+ ?. ?=(%value -.i.ds) $(ds t.ds)
7973+ =/ deps=(list term) (dependency-expr val.i.ds)
7974+ =. deps (skim deps |=(n=term ?=(^ (~(get by names) n))))
7975+ $(ds t.ds, graph (~(put by graph) name.i.ds deps))
7976+::
7977+++ graph-add-reverse
7978+ |= [name=term edges=(list term) reverse=iadj]
7979+ ^- iadj
7980+ ?~ edges reverse
7981+ =/ prior=(list term) (graph-edges i.edges reverse)
7982+ $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
7983+::
7984+++ graph-reverse
7985+ |= [names=(list term) graph=iadj reverse=iadj]
7986+ ^- iadj
7987+ ?~ names reverse
7988+ =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
7989+ $(names t.names)
7990+::
7991+++ graph-order
7992+ |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
7993+ ^- iwresult
7994+ ?~ todo [seen order]
7995+ =/ event=[name=term done=?] i.todo
7996+ ?: done.event $(todo t.todo, order [name.event order])
7997+ ?: ?=(^ (~(get by seen) name.event)) $(todo t.todo)
7998+ =. seen (~(put by seen) name.event &)
7999+ =/ children=iwork (turn (graph-edges name.event graph) |=(n=term [n |]))
8000+ $(todo (weld children [[name.event &] t.todo]))
8001+::
8002+++ graph-collect
8003+ |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
8004+ ^- icresult
8005+ ?~ todo [seen component]
8006+ ?: ?=(^ (~(get by seen) i.todo)) $(todo t.todo)
8007+ =. seen (~(put by seen) i.todo &)
8008+ $(todo (weld (graph-edges i.todo graph) t.todo), component [i.todo component])
8009+::
8010+++ graph-collect-all
8011+ |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
8012+ ^- icomponents
8013+ ?~ order comps
8014+ ?: ?=(^ (~(get by seen) i.order)) $(order t.order)
8015+ =/ found=icresult (graph-collect ~[i.order] seen ~ graph)
8016+ $(order t.order, seen seen.found, comps [component.found comps])
8017+::
8018+:: Two depth-first passes find components before group inference. Maps
8019+:: preserve the graph identity; duplicate global names fail closed.
8020+++ graph-components
8021+ |= [ds=(list def) names=(list term)]
8022+ ^- icomponents
8023+ =/ nameset=ivisited ~
8024+ =/ pending=(list term) names
8025+ |-
8026+ ?^ pending
8027+ ?: ?=(^ (~(get by nameset) i.pending)) ~
8028+ $(pending t.pending, nameset (~(put by nameset) i.pending &))
8029+ =/ graph=iadj (graph-make-forward ds nameset ~)
8030+ =/ reverse=iadj (graph-reverse names graph ~)
8031+ =/ order=iwresult (graph-order (turn names |=(n=term [n |])) ~ ~ graph)
8032+ (graph-collect-all order.order ~ reverse ~)
8033+::
8034+++ graph-cycle
8035+ |= [component=(list term) graph=iadj]
8036+ ^- ?
8037+ ?~ component |
8038+ ?^ t.component &
8039+ (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
8040+::
8041+++ add-groups
8042+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) state=istate]
8043+ ^- iresolved
8044+ ?~ components [env grouped]
8045+ =/ component=(list term) i.components
8046+ ?. (graph-cycle component graph) $(components t.components)
8047+ ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
8048+ =/ members=(list def)
8049+ %+ skim ds
8050+ |= d=def
8051+ &(?=(%value -.d) (lien component |=(n=term =(n name.d))))
8052+ ?. =((lent members) (lent component)) $(components t.components)
8053+ ?. (levy component |=(n=term (unique-value-name n globals.state))) $(components t.components)
8054+ =/ result=ilocal-result (infer-gate-group members env state)
8055+ ?: ?=(%| -.result) $(components t.components)
8056+ $(components t.components, env env.p.result, grouped (weld component grouped))
8057+::
8058+++ resolve-groups
8059+ |= [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)]
8060+ ^- iresolved
51638061 =/ env=ienv ~
8062+ =/ grouped=(list term) ~
8063+ =/ names=(list term) (global-value-names ds)
8064+ =/ nameset=ivisited (graph-nameset names ~)
8065+ =/ graph=iadj (graph-make-forward ds nameset ~)
8066+ =/ components=icomponents (graph-components ds names)
8067+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
51648068 |-
5165− =/ next=ienv (add-supported-defs ds env molds globals externals surs)
5166− ?: =(next env) env
5167− $(env next)
8069+ =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
8070+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8071+ =/ out=iresolved (add-groups ds components graph next grouped initial)
8072+ ?: =(env env.out) out
8073+ $(env env.out, grouped grouped.out)
8074+::
8075+++ resolve-supported-defs
8076+ |= [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)]
8077+ ^- ienv
8078+ env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
51688079::
51698080+| %union-analysis
51708081::
@@ -5302,7 +8213,7 @@
53028213 (weld pairs $(cases t.cases))
53038214::
53048215++ show-partial-mold
5305− |= [d=def molds=imolds]
8216+ |= [file=path src=@t d=def molds=imolds]
53068217 ^- @t
53078218 ?> ?=(%mold -.d)
53088219 =/ sh=shape shape.d
@@ -5312,11 +8223,26 @@
53128223 =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
53138224 ?^ overlapping
53148225 =/ p=upair i.overlapping
5315− (crip "+$ {(trip name.d)}: overlapping cases at {(show-loc beg.first.p)} and {(show-loc beg.second.p)}; mold not checked")
8226+ =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
8227+ =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
8228+ =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
8229+ (of-wain:format ~[summary first second])
53168230 ?: (lien pairs |=(p=upair =(%unknown relation.p)))
53178231 (crip "+$ {(trip name.d)}: case disjointness unresolved; mold not checked")
53188232 (crip "+$ {(trip name.d)}: cases proven disjoint; mold not checked")
53198233::
8234+:: +show-inference-diagnostic: a partial report with both source sites
8235+::
8236+++ show-inference-diagnostic
8237+ |= [file=path src=@t name=term diagnostic=idiag]
8238+ ^- @t
8239+ =/ summary=@t (crip "++ {(trip name)}: {msg.diagnostic}")
8240+ =/ excerpts=(list @t)
8241+ %+ turn sites.diagnostic
8242+ |= site=[at=span note=tape]
8243+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
8244+ (of-wain:format [summary excerpts])
8245+::
53208246:: +golden-types: a partial report; it does not claim the module checks
53218247::
53228248++ golden-types
@@ -5333,33 +8259,356 @@
53338259++ golden-types-imports
53348260 |= [file=path src=@t externals=iexternals]
53358261 ^- @t
8262+ (golden-types-with-marks file src externals ~)
8263+::
8264+:: A supplied module is addressed by its logical /ui/.../name/jibb path.
8265+:: Interfaces are closed inference schemes, never raw source shapes.
8266+:: Recursive modules, APIs, derived gates and unsupported definitions do
8267+:: not yield an interface. The reachable graph is checked before the root.
8268+::
8269++$ jsource [at=path source=@t]
8270++$ jbundle (list jsource)
8271++$ jcache (list [at=path iface=ifile])
8272++$ jfile-result (each [iface=ifile cache=jcache] @t)
8273++$ jimports-result (each [resolved=ijimports cache=jcache] @t)
8274+::
8275+++ import-binding-names
8276+ |= imports=(list import)
8277+ ^- (list term)
8278+ ?~ imports ~
8279+ =/ n=term
8280+ ?- -.i.imports
8281+ %jibb face.i.imports
8282+ %sur name.i.imports
8283+ %mark mark.i.imports
8284+ ==
8285+ [n $(imports t.imports)]
8286+::
8287+++ module-scope-valid
8288+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
8289+ ^- ?
8290+ =/ imported=(list term) (import-binding-names imports.mod)
8291+ =/ vals=(list term) (global-value-names defs.mod)
8292+ =/ molds=imolds (collect-simple-molds defs.mod)
8293+ =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8294+ ?. %+ levy imported
8295+ |= n=term
8296+ &((unique-value-name n imported) !(lien vals |=(v=term =(n v))) !(lien mold-names |=(m=term =(n m))) !(lien prelude-values |=(v=term =(n v))) !(lien prelude-molds |=(m=term =(n m))))
8297+ |
8298+ ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
8299+ (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
8300+::
8301+++ module-mold-types
8302+ |= [molds=imolds state=istate]
8303+ ^- (each imold-types @t)
8304+ ?~ molds [%& ~]
8305+ =/ m=[name=term body=shape] i.molds
8306+ =/ t=(unit [template=ischeme state=istate])
8307+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
8308+ ?~ t [%| 'module mold needs unsupported inference']
8309+ =. typ.template.u.t (label-direct-union typ.template.u.t body.m name.m state)
8310+ =/ rest=(each imold-types @t) $(molds t.molds)
8311+ ?: ?=(%| -.rest) rest
8312+ [%& [[name.m template.u.t] p.rest]]
8313+::
8314+:: Prepare a provisional interface from the trusted vendored source.
8315+:: Every declared name remains reserved, but only molds and values this
8316+:: fragment can infer are usable. Unsupported bodies are not validated,
8317+:: and imports into the prelude are not supported yet. The fixed origin
8318+:: gives its named unions the same identity in every importing module.
8319+::
8320+:: Recognize only the complete standard prelude list shape. Its recursive
8321+:: tail uses the same parameter and the unqualified list name. The reader
8322+:: verifies Hoon's list provenance before producing the same collection type.
8323+:: The prelude source and reader output are trusted caller inputs.
8324+::
8325+++ standard-prelude-list
8326+ |= sh=shape
8327+ ^- ?
8328+ ?. ?=(%generic -.sh) |
8329+ ?~ vars.sh |
8330+ ?^ t.vars.sh |
8331+ =/ var=@t i.vars.sh
8332+ ?. ?=(%union -.body.sh) |
8333+ =/ cs=(list shape) cases.body.sh
8334+ ?~ cs |
8335+ ?~ t.cs |
8336+ ?^ t.t.cs |
8337+ ?. ?=(%const -.i.cs) |
8338+ ?. =(%null form.lit.i.cs) |
8339+ ?. ?=(%cell -.i.t.cs) |
8340+ =/ fs=(list field) fields.i.t.cs
8341+ ?~ fs |
8342+ ?~ t.fs |
8343+ ?^ t.t.fs |
8344+ ?. ?=(%face -.i.fs) |
8345+ ?. =(%i name.i.fs) |
8346+ ?. ?=(%tvar -.shape.i.fs) |
8347+ ?. =(var name.shape.i.fs) |
8348+ ?. ?=(%face -.i.t.fs) |
8349+ ?. =(%t name.i.t.fs) |
8350+ =/ tail=shape shape.i.t.fs
8351+ ?. ?=(%apply -.tail) |
8352+ ?. =(~[%list] ref.tail) |
8353+ ?~ args.tail |
8354+ ?^ t.args.tail |
8355+ ?. ?=(%tvar -.i.args.tail) |
8356+ =(var name.i.args.tail)
8357+::
8358+++ partial-prelude-molds
8359+ |= [molds=imolds state=istate]
8360+ ^- imold-types
8361+ ?~ molds ~
8362+ =/ m=[name=term body=shape] i.molds
8363+ ?: &(=(at.state /lib/jibb/prelude/jibb) =(%list name.m))
8364+ ?. (standard-prelude-list body.m) $(molds t.molds)
8365+ [[%list [[%collection %list ~[[%var 0]]] ~[0]]] $(molds t.molds)]
8366+ =/ out=(unit [template=ischeme state=istate])
8367+ (infer-mold-template body.m state(active [name.m active.state], in-mold &))
8368+ ?~ out $(molds t.molds)
8369+ =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
8370+ [[name.m template.u.out] $(molds t.molds)]
8371+::
8372+++ partial-prelude-interface
8373+ |= src=@t
8374+ ^- (unit ifile)
8375+ ?: =(0 src) ~
8376+ =/ at=path /lib/jibb/prelude/jibb
8377+ =/ parsed (parse at src)
8378+ ?: ?=(%| -.parsed) ~
8379+ ?^ imports.p.parsed ~
8380+ ?~ defs.p.parsed ~
8381+ ?. (module-scope-valid p.parsed ~ ~) ~
8382+ =/ ds=(list def) defs.p.parsed
8383+ =/ molds=imolds (collect-simple-molds ds)
8384+ =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8385+ =/ globals=(list term) (global-value-names ds)
8386+ :: Remove raw list before inferring any template, so an altered list
8387+ :: cannot leak through an alias. Its name remains reserved either way.
8388+ =/ declared=? (lien names |=(name=term =(%list name)))
8389+ =/ env-molds=imolds molds
8390+ =? env-molds declared
8391+ (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
8392+ =/ reserved=(list term) ?:(declared ~[%list] ~)
8393+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ ~ reserved ~ ~ ~ | at names ~]
8394+ =/ mt=imold-types (partial-prelude-molds molds state)
8395+ =/ partial=ifile [~ mt at]
8396+ =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ ~ reserved at `partial)
8397+ `[env mt at]
8398+::
8399++$ iprelude [iface=ifile values=(list term) molds=(list term)]
8400+::
8401+++ prepare-prelude
8402+ |= src=@t
8403+ ^- (unit iprelude)
8404+ =/ iface=(unit ifile) (partial-prelude-interface src)
8405+ ?~ iface ~
8406+ =/ parsed (parse /lib/jibb/prelude/jibb src)
8407+ ?: ?=(%| -.parsed) ~
8408+ =/ vals=(list term) (global-value-names defs.p.parsed)
8409+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
8410+ `[u.iface vals ms]
8411+::
8412+++ module-values-complete
8413+ |= [ds=(list def) env=ienv]
8414+ ^- ?
8415+ ?~ ds &
8416+ ?: ?=(%mold -.i.ds) $(ds t.ds)
8417+ ?~ (ienv-lookup name.i.ds env) |
8418+ $(ds t.ds)
8419+::
8420+:: Cache only completed interfaces for this invocation. The source bundle,
8421+:: imported Hoon types and prelude are fixed for the whole graph. Check the
8422+:: active path and duplicate sources before consulting it, so a cache hit
8423+:: cannot hide a cycle or ambiguous source.
8424+::
8425+++ find-jibb-cache
8426+ |= [at=path cache=jcache]
8427+ ^- (unit ifile)
8428+ ?~ cache ~
8429+ ?: =(at at.i.cache) `iface.i.cache
8430+ $(cache t.cache)
8431+::
8432+++ resolve-jibb-imports
8433+ |= [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)]
8434+ ^- jimports-result
8435+ ?~ imports [%& [~ cache]]
8436+ ?. ?=(%jibb -.i.imports) $(imports t.imports)
8437+ =/ at=path (weld path.i.imports `path`~[%jibb])
8438+ ?: (lien active |=(p=path =(p at)))
8439+ [%| (crip "import cycle at {(spud at)}")]
8440+ =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
8441+ ?~ found [%| (crip "module source missing: {(spud at)}")]
8442+ ?^ t.found [%| (crip "duplicate module sources: {(spud at)}")]
8443+ =/ cached=(unit ifile) (find-jibb-cache at cache)
8444+ =/ iface=jfile-result
8445+ ?^ cached [%& [u.cached cache]]
8446+ (infer-jibb-file at source.i.found externals mark-externals modules [at active] prelude-values prelude-molds cache prelude)
8447+ ?: ?=(%| -.iface) [%| p.iface]
8448+ =/ rest=jimports-result $(imports t.imports, cache cache.p.iface)
8449+ ?: ?=(%| -.rest) rest
8450+ [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
8451+::
8452+++ infer-jibb-file
8453+ |= [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)]
8454+ ^- jfile-result
8455+ ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
8456+ =/ parsed (parse at src)
8457+ ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
8458+ =/ mod=module p.parsed
8459+ ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
8460+ =/ vals=(list term) (global-value-names defs.mod)
8461+ ?: (lien vals |=(n=term =(n %main)))
8462+ [%| (crip "module kind needs unsupported inference: {(spud at)}")]
8463+ =/ js=jimports-result (resolve-jibb-imports imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
8464+ ?: ?=(%| -.js) [%| p.js]
8465+ =/ molds=imolds (collect-simple-molds defs.mod)
8466+ =/ globals=(list term) (weld prelude-values (weld (import-binding-names imports.mod) vals))
8467+ =/ surs=(list term) (collect-sur-imports imports.mod)
8468+ =/ marks=(list term) (collect-mark-imports imports.mod)
8469+ =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
8470+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8471+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
8472+ =/ mts=(each imold-types @t) (module-mold-types molds state)
8473+ ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
8474+ =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
8475+ ?. (module-values-complete defs.mod env)
8476+ [%| (crip "module definitions need unsupported inference: {(spud at)}")]
8477+ [%& [[env p.mts at] [[at [env p.mts at]] cache.p.js]]]
8478+::
8479+:: +golden-types-with-modules fails closed for imports without prelude
8480+:: scope. +golden-types-with-prelude resolves supported library graphs;
8481+:: its report remains partial and unreachable sources are not examined.
8482+::
8483+++ golden-types-with-modules
8484+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle]
8485+ ^- @t
8486+ =/ parsed (parse file src)
8487+ ?: ?=(%| -.parsed) (show-error src p.parsed)
8488+ ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
8489+ 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
8490+ (golden-types-with-marks file src externals mark-externals)
8491+::
8492+:: The caller supplies the actual prelude source. Its declared names are
8493+:: reserved, and supported inferred types are made available. The inventory
8494+:: and the checker are incomplete, so this never claims a checked module.
8495+:: Hosts may prepare the same trusted source once and reuse its interface.
8496+::
8497+++ golden-types-with-prelude
8498+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t]
8499+ ^- @t
8500+ =/ parsed (parse file src)
8501+ ?: ?=(%| -.parsed) (show-error src p.parsed)
8502+ ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
8503+ =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
8504+ ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
8505+ =/ prepared=(unit iprelude) (prepare-prelude prelude-source)
8506+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
8507+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
8508+::
8509+++ golden-types-with-prepared-prelude
8510+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
8511+ ^- @t
8512+ =/ parsed (parse file src)
8513+ ?: ?=(%| -.parsed) (show-error src p.parsed)
8514+ ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
8515+ =/ prelude-values=(list term) values.u.prepared
8516+ =/ prelude-molds=(list term) molds.u.prepared
8517+ =/ iface=(unit ifile) `iface.u.prepared
8518+ ?. (module-scope-valid p.parsed prelude-values prelude-molds)
8519+ 'partial inference; module not checked\0amodule has conflicting names'
8520+ =/ js=jimports-result
8521+ (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
8522+ ?: ?=(%| -.js) (of-wain:format ~['partial inference; module not checked' p.js])
8523+ =/ scope-values=(list term)
8524+ (weld prelude-values (weld (collect-sur-imports imports.p.parsed) (collect-mark-imports imports.p.parsed)))
8525+ (golden-types-in-context file src externals mark-externals resolved.p.js scope-values prelude-molds iface)
8526+::
8527+:: +golden-types-with-marks: supply declared mark types separately from /sur
8528+:: entries, as [mark result] with the result from +read-mark:jibb-import.
8529+:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
8530+::
8531+:: Callers pass unchanged structured reader results; graph validation
8532+:: remains in the existing bridge, and failures stay available lazily.
8533+++ reader-result-for-checker
8534+ |= result=*
8535+ ^- *
8536+ ?: ?=([%ok *] result) [%& +.result]
8537+ result
8538+::
8539+++ golden-types-with-reader-diagnostics
8540+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
8541+ ^- @t
8542+ =/ ex=iexternals
8543+ (turn externals |=(e=[module=term name=term result=*] [module.e name.e (reader-result-for-checker result.e)]))
8544+ =/ mx=imark-externals
8545+ (turn mark-externals |=(e=[mark=term result=*] [mark.e (reader-result-for-checker result.e)]))
8546+ (golden-types-with-marks file src ex mx)
8547+::
8548+++ golden-types-with-marks
8549+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
8550+ ^- @t
8551+ (golden-types-in-context file src externals mark-externals ~ ~ ~ ~)
8552+::
8553+++ golden-types-in-context
8554+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals jimports=ijimports prelude-values=(list term) reserved-molds=(list term) prelude=(unit ifile)]
8555+ ^- @t
8556+ =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
53368557 =/ parsed (parse file src)
53378558 ?: ?=(%| -.parsed) (show-error src p.parsed)
53388559 =/ ds=(list def) defs.p.parsed
53398560 =/ molds=imolds (collect-simple-molds ds)
5340− =/ globals=(list term) (global-value-names ds)
8561+ =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
53418562 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
5342− =/ env=ienv (resolve-supported-defs ds molds globals externals surs)
8563+ =/ marks=(list term) (collect-mark-imports imports.p.parsed)
8564+ =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
8565+ =/ env=ienv env.resolution
53438566 =/ lines=(list @t) ~
53448567 |-
53458568 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
53468569 =/ d=def i.ds
53478570 ?: ?=(%mold -.d)
5348− $(ds t.ds, lines [(show-partial-mold d molds) lines])
8571+ $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
53498572 ?. (unique-value-name name.d globals)
53508573 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
5351− =/ result=iresult (infer-fragment val.d env [0 ~ ~ molds globals externals surs ~ |])
8574+ ?: (lien grouped.resolution |=(n=term =(n name.d)))
8575+ =/ found=(unit ischeme) (ienv-lookup name.d env)
8576+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
8577+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
8578+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
8579+ $(ds t.ds, lines [line lines])
8580+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8581+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
8582+ =. initial (reserve-def-caps val.d initial)
8583+ =/ result=iresult
8584+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
8585+ (infer-recursive-gate d env initial)
8586+ (infer-fragment val.d env initial)
53528587 ?: ?=(%| -.result)
5353− $(ds t.ds, lines [(crip "++ {(trip name.d)}: {p.result}") lines])
8588+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
8589+ =/ merged=(unit [first=icap second=icap])
8590+ (merged-capitals caps.state.p.result sub.state.p.result)
8591+ ?^ merged
8592+ =/ diag=idiag
8593+ ["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"]]]
8594+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
53548595 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
53558596 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
5356− =/ typ=itype (itype-normalize typ.p.result sub.state.p.result)
5357− ?: (itype-has-avar typ)
8597+ =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
8598+ ?: (pending-null tags.state.p.result sub.state.p.result)
8599+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: `~` needs context in partial inference") lines])
8600+ ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ))
8601+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: tag needs context in partial inference") lines])
8602+ ?: (itype-has-hidden-recursive typ)
8603+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive mold name is not available in this scope") lines])
8604+ ?: (itype-has-hidden-generic typ)
8605+ $(ds t.ds, lines [(crip "++ {(trip name.d)}: generic union name is not available in this scope") lines])
8606+ ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
53588607 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
53598608 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
53608609 ?: (gth (lent vars) 26)
53618610 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
53628611 =/ printable=itype (canonical-itype typ vars)
5363− =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}")
8612+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
53648613 $(ds t.ds, lines [line lines])
53658614--