@@ -4608,6 +4608,7 @@
46084608 [%atom aura=@ta]
46094609 [%any-atom ~]
46104610 [%flag ~]
4611+ [%noun ~]
46114612 [%tag id=@ud literal=lit constructor=?]
46124613 [%const literal=lit]
46134614 [%collection name=term args=(list itype)]
@@ -4661,6 +4662,7 @@
46614662 %atom |
46624663 %any-atom |
46634664 %flag |
4665+ %noun |
46644666 %tag =(n id.t)
46654667 %const |
46664668 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
@@ -4757,6 +4759,7 @@
47574759 %atom |
47584760 %any-atom &
47594761 %flag |
4762+ %noun |
47604763 %tag |
47614764 %const |
47624765 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
@@ -4827,6 +4830,7 @@
48274830 %atom &
48284831 %any-atom &
48294832 %flag &
4833+ %noun |
48304834 %tag &
48314835 %const &
48324836 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
@@ -4916,6 +4920,7 @@
49164920 %cell &
49174921 %union &
49184922 %recursive &
4923+ %noun &
49194924 %collection &
49204925 %face $(t body.t)
49214926 %fn |($(t sample.t) $(t product.t))
@@ -5055,6 +5060,15 @@
50555060 =. actual (itype-walk actual sub)
50565061 =. expected (itype-walk expected sub)
50575062 ?: =(actual expected) [%ok sub next]
5063+ :: Any value can be used where a noun is expected. An unresolved
5064+ :: bare tag is fixed as a constant; a constructor still needs a gate.
5065+ ?: ?=(%noun -.expected)
5066+ ?: ?=(%tag -.actual)
5067+ ?: constructor.actual [%unknown ~]
5068+ [%ok [[id.actual expected] sub] next]
5069+ [%ok sub next]
5070+ :: An arbitrary noun is not known to fit a narrower type.
5071+ ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
50585072 ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
50595073 ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
50605074 ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
@@ -5066,6 +5080,10 @@
50665080 =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
50675081 ?^ unified [%ok u.unified next]
50685082 [%unknown ~]
5083+ :: A concrete union value in a tuple may acquire the expected field's
5084+ :: face. A variable-bound union still needs face propagation support.
5085+ ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5086+ $(expected body.expected)
50695087 ?: ?=(%union -.actual) [%unknown ~]
50705088 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
50715089 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -5084,6 +5102,10 @@
50845102 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
50855103 ?. ?=(%ok -.trial) trial
50865104 [%ok [[id.actual expected] sub.trial] next.trial]
5105+ :: Zero may be the empty list. A nested cell fit lacks the context
5106+ :: needed to resolve it here, so do not report a definite mismatch.
5107+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5108+ [%unknown ~]
50875109 ?: ?=(%const -.expected)
50885110 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
50895111 ?: ?=(%atom -.expected)
@@ -5101,6 +5123,8 @@
51015123 [%ok u.u next]
51025124 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
51035125 ?: ?=(%face -.expected) $(expected body.expected)
5126+ ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5127+ [%unknown ~]
51045128 ?: ?=(%const -.expected)
51055129 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
51065130 ?: ?=(%atom -.expected)
@@ -5226,15 +5250,17 @@
52265250 problems
52275251::
52285252:: The expression inference below is deliberately a fragment: bindings,
5229−:: simple gates, unary calls, fixed-aura literals, and plain strings. The
5253+:: simple gates, calls, fixed-aura literals, and some interpolated strings. The
52305254:: result for unsupported syntax is a diagnostic, never a checked module.
52315255::
52325256+$ ischeme [typ=itype vars=(list @ud)]
52335257+$ ienv (list [name=term scheme=ischeme])
52345258+$ imold-types (list [name=term template=ischeme])
5235−+$ ifile [values=ienv molds=imold-types at=path]
5259++$ iderived [name=term agent=term mark=term]
5260++$ ifile [values=ienv molds=imold-types at=path derived=(list iderived)]
52365261+$ ijimports (list [face=term interface=ifile])
5237−+$ icaps (list [name=@t id=@ud])
5262++$ icap [name=@t id=@ud at=span]
5263++$ icaps (list icap)
52385264+$ iparams (list [name=@t typ=itype])
52395265+$ imolds (list [name=term body=shape])
52405266:: A caller supplies the exact noun returned by +read-mold:jibb-import.
@@ -5277,6 +5303,8 @@
52775303:: generalize an aura from its sample, which requires constraint analysis
52785304:: beyond this fragment; leave those cases unresolved.
52795305::
5306+:: This helper only controls decimal defaulting in visible types. A noun
5307+:: may contain gates and is not proof of a gate-free value.
52805308++ itype-has-gate
52815309 |= t=itype
52825310 ^- ?
@@ -5295,6 +5323,7 @@
52955323 %atom |
52965324 %any-atom |
52975325 %flag |
5326+ %noun |
52985327 ==
52995328::
53005329++ default-decimals
@@ -5319,6 +5348,7 @@
53195348 %atom ~
53205349 %any-atom ~
53215350 %flag ~
5351+ %noun ~
53225352 %tag ~
53235353 %const ~
53245354 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
@@ -5357,6 +5387,7 @@
53575387 %atom t
53585388 %any-atom t
53595389 %flag t
5390+ %noun t
53605391 %tag t
53615392 %const t
53625393 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
@@ -5380,6 +5411,7 @@
53805411 %atom |
53815412 %any-atom |
53825413 %flag |
5414+ %noun |
53835415 %tag |
53845416 %const |
53855417 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
@@ -5524,12 +5556,66 @@
55245556 $(pats t.pats)
55255557::
55265558::
5559+::
5560+:: Repeated faces along an imported record spine fail closed. Hoon's type
5561+:: graph can erase unfaced nested-cell boundaries, so that alone does not
5562+:: prove the original source repeated a name within one record. A faced
5563+:: body and each union alternative have separate scopes. Check recursive
5564+:: roots before making them opaque; unused molds are never inspected.
5565+::
5566+++ imported-faces-valid
5567+ |= node=*
5568+ ^- ?
5569+ ?@ node &
5570+ ?+ -.node &
5571+ %face ?:(?=([%face @ *] node) $(node +>.node) |)
5572+ %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
5573+ %fork (imported-faces-valid-list +.node)
5574+ %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
5575+ ==
5576+::
5577+++ imported-faces-valid-list
5578+ |= nodes=*
5579+ ^- ?
5580+ ?@ nodes =(nodes 0)
5581+ ?. (imported-faces-valid -.nodes) |
5582+ $(nodes +.nodes)
5583+::
5584+++ imported-record-faces-valid
5585+ |= [node=* names=(list @)]
5586+ ^- ?
5587+ ?: ?=([%cell * *] node)
5588+ =/ head=* +<.node
5589+ =/ rest=* +>.node
5590+ ?: ?=([%face @ *] head)
5591+ ?: (lien names |=(n=@ =(n +<.head))) |
5592+ ?. (imported-faces-valid +>.head) |
5593+ $(node rest, names [+<.head names])
5594+ ?. (imported-faces-valid head) |
5595+ $(node rest)
5596+ ?: ?=([%face @ *] node)
5597+ ?: (lien names |=(n=@ =(n +<.node))) |
5598+ (imported-faces-valid +>.node)
5599+ (imported-faces-valid node)
5600+::
55275601++ import-to-itype
55285602 |= node=*
55295603 ^- (unit itype)
55305604 ?@ node ~
55315605 ?+ -.node ~
5606+ %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
55325607 %atom
5608+ :: A Hoon loobean singleton is one of the two Jibb loobeans.
5609+ ?: ?=([%atom %f [~ @]] node)
5610+ =/ value=@ +>+.node
5611+ ?. |(=(value 0) =(value 1)) ~
5612+ =/ printed=@t ?:(=(value 0) '%.y' '%.n')
5613+ `[%const [%loobean %f value printed]]
5614+ :: Hoon's null singleton is the same noun as Jibb's `~` mold.
5615+ :: Other non-term singleton atoms remain unsupported here.
5616+ ?: ?=([%atom %n [~ @]] node)
5617+ ?. =(0 +>+.node) ~
5618+ `[%const [%null %n 0 '~']]
55335619 ?: ?=([%atom %tas [~ @]] node)
55345620 =/ value=@ +>+.node
55355621 ?. |(=(value 0) (jibb-face-name value)) ~
@@ -5552,10 +5638,15 @@
55525638 ?. =(arity (lent u.args)) ~
55535639 `[%collection name u.args]
55545640 %fork
5555− =/ cases=(unit (list itype)) (import-to-itypes +.node)
5641+ :: Hoon's ordinary ? mold is the fork of its two %f singletons.
5642+ =/ raw=* +.node
5643+ ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
5644+ `[%flag ~]
5645+ =/ cases=(unit (list itype)) (import-to-itypes raw)
55565646 ?~ cases ~
55575647 ?~ u.cases ~
55585648 ?~ t.u.cases ~
5649+ ?: (import-has-loobean-singleton u.cases) ~
55595650 ?. (import-cases-disjoint u.cases) ~
55605651 `[%union u.cases ~ ~ ~]
55615652 %face
@@ -5574,6 +5665,20 @@
55745665 `[%cell u.left u.right]
55755666 ==
55765667::
5668+++ import-direct-loobean
5669+ |= t=itype
5670+ ^- ?
5671+ ?: ?=(%face -.t) $(t body.t)
5672+ ?: ?=(%union -.t) (import-has-loobean-singleton cases.t)
5673+ ?=([%const [%loobean *]] t)
5674+::
5675+++ import-has-loobean-singleton
5676+ |= cases=(list itype)
5677+ ^- ?
5678+ ?~ cases |
5679+ ?: (import-direct-loobean i.cases) &
5680+ $(cases t.cases)
5681+::
55775682++ import-to-itypes
55785683 |= nodes=*
55795684 ^- (unit (list itype))
@@ -5588,7 +5693,9 @@
55885693 |= typ=itype
55895694 ^- upat
55905695 ?- -.typ
5696+ %noun [%all ~]
55915697 %atom [%atom ~]
5698+ %flag [%or ~[[%atom `0] [%atom `1]]]
55925699 %const [%atom `val.literal.typ]
55935700 %face $(typ body.typ)
55945701 %cell [%cell $(typ hed.typ) $(typ tal.typ)]
@@ -5616,6 +5723,7 @@
56165723 ?@ result ~
56175724 ?. ?=(%& -.result) ~
56185725 =/ node=* +.result
5726+ ?. (imported-faces-valid node) ~
56195727 ?@ node (import-to-itype node)
56205728 ?: ?=(%ref -.node) (import-to-itype node)
56215729 =/ pattern=(unit irec-pattern) (rec-pattern node module name)
@@ -5651,6 +5759,7 @@
56515759 =/ result=* result.i.found
56525760 ?@ result ~
56535761 ?. ?=(%& -.result) ~
5762+ ?. (imported-faces-valid +.result) ~
56545763 (import-to-itype +.result)
56555764::
56565765++ find-jibb-interface
@@ -5681,25 +5790,41 @@
56815790 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
56825791 $(molds t.molds)
56835792::
5684−:: Only names exported by this directly imported module are visible through
5685−:: its face. Other origins retain identity but print as unnamed unions.
5793+:: A public non-generic alias names exactly its origin and arguments.
5794+:: Reusing only an origin could print a different generic instantiation.
5795+++ prelude-union-alias
5796+ |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
5797+ ^- (unit term)
5798+ ?^ args ~
5799+ ?~ molds ~
5800+ =/ template=ischeme template.i.molds
5801+ ?: &(?=(~ vars.template) ?=(%union -.typ.template))
5802+ ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
5803+ $(molds t.molds)
5804+::
5805+:: Names exported by the directly imported module are visible through its
5806+:: face; a matching prelude alias is also visible without a qualifier.
56865807::
56875808++ itype-in-import
5688− |= [t=itype iface=ifile face=term]
5809+ |= [t=itype iface=ifile face=term prelude=(unit ifile)]
56895810 ^- itype
56905811 ?- -.t
56915812 %union
56925813 =/ label=(unit @t)
56935814 ?~ origin.t ~
56945815 ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
5816+ =/ public=(unit term)
5817+ ?~ prelude ~
5818+ (prelude-union-alias u.origin.t args.t molds.u.prelude)
5819+ ?^ public `u.public
56955820 =/ alias=(unit term) ~
56965821 =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
56975822 =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
56985823 ?~ alias ~
56995824 `(crip "{(trip u.alias)}.{(trip face)}")
5700− [%union (turn cases.t |=(c=itype (itype-in-import c iface face))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face)))]
5825+ [%union (turn cases.t |=(c=itype (itype-in-import c iface face prelude))) origin.t label (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
57015826 %recursive [%recursive module.t name.t ~]
5702− %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face)))]
5827+ %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
57035828 %face [%face name.t $(t body.t)]
57045829 %fn [%fn $(t sample.t) $(t product.t)]
57055830 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -5794,6 +5919,103 @@
57945919 ?: ?=(^ (itype-vars typ.u.out)) ~
57955920 `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
57965921::
5922+:: A direct imported reference may carry definite reader evidence. Only
5923+:: uniquely supplied, declared inputs are used; unsupported data stay generic.
5924+++ direct-import-invalid
5925+ |= [sh=shape state=istate]
5926+ ^- (unit idiag)
5927+ ?. ?=(%ref -.sh) ~
5928+ ?~ names.sh ~
5929+ =/ n=term i.names.sh
5930+ =/ raw=*
5931+ ?~ t.names.sh
5932+ ?. (unique-value-name n marks.state) ~
5933+ ?: (lien surs.state |=(x=term =(x n))) ~
5934+ ?: ?=(^ (find-jibb-interface n jimports.state)) ~
5935+ ?: (lien globals.state |=(x=term =(x n))) ~
5936+ ?: (lien reserved-molds.state |=(x=term =(x n))) ~
5937+ ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) ~
5938+ =/ found=imark-externals (skim mark-externals.state |=(e=[mark=term result=*] =(mark.e n)))
5939+ ?~ found ~
5940+ ?^ t.found ~
5941+ result.i.found
5942+ ?^ t.t.names.sh ~
5943+ =/ mod=term i.t.names.sh
5944+ ?: ?=(^ (find-jibb-interface mod jimports.state)) ~
5945+ ?. (unique-value-name mod surs.state) ~
5946+ ?: (lien marks.state |=(x=term =(x mod))) ~
5947+ ?: (lien globals.state |=(x=term =(x mod))) ~
5948+ ?: (lien reserved-molds.state |=(x=term =(x mod))) ~
5949+ ?: (lien molds.state |=(m=[name=term body=shape] =(mod name.m))) ~
5950+ =/ found=iexternals (skim externals.state |=(e=[module=term name=term result=*] &(=(module.e mod) =(name.e n))))
5951+ ?~ found ~
5952+ ?^ t.found ~
5953+ result.i.found
5954+ ?. ?=([%invalid ?(%aura %core) @] raw) ~
5955+ `["{(trip +>.raw)}" ~[[at.sh "invalid imported mold"]]]
5956+::
5957+:: Replay only the shape branches whose evaluation order we can prove.
5958+:: Successful prefixes must be checked before descending to a failure.
5959+++ nested-import-invalid
5960+ |= [sh=shape state=istate]
5961+ ^- (unit idiag)
5962+ ?: ?=(^ (infer-simple-shape sh state)) ~
5963+ ?- -.sh
5964+ %ref
5965+ =/ direct=(unit idiag) (direct-import-invalid sh state)
5966+ ?^ direct direct
5967+ ?~ names.sh ~
5968+ ?^ t.names.sh ~
5969+ =/ n=term i.names.sh
5970+ ?: (lien marks.state |=(x=term =(x n))) ~
5971+ ?: (lien active.state |=(x=term =(x n))) ~
5972+ =/ found=(unit shape) (find-simple-mold n molds.state)
5973+ ?~ found ~
5974+ $(sh u.found, state state(active [n active.state], in-mold &, params ~))
5975+ %fn
5976+ =/ first=(unit [typ=itype state=istate]) (infer-simple-shape sample.sh state)
5977+ ?~ first $(sh sample.sh)
5978+ $(sh product.sh, state state.u.first)
5979+ %cell (nested-field-invalid fields.sh state)
5980+ * ~
5981+ ==
5982+::
5983+++ nested-field-invalid
5984+ |= [fields=(list field) state=istate]
5985+ ^- (unit idiag)
5986+ ?~ fields ~
5987+ =/ sh=shape
5988+ ?- -.i.fields
5989+ %bare shape.i.fields
5990+ %face shape.i.fields
5991+ %pun [%ref at.i.fields ~[name.i.fields]]
5992+ ==
5993+ =/ out=(unit [typ=itype state=istate]) (infer-simple-shape sh state)
5994+ ?~ out (nested-import-invalid sh state)
5995+ $(fields t.fields, state state.u.out)
5996+::
5997+++ sample-import-invalid
5998+ |= [s=sample env=ienv state=istate]
5999+ ^- (unit idiag)
6000+ =/ result=isample-result (infer-sample s env state)
6001+ ?: ?=(%& -.result) ~
6002+ ?. =(p.result "sample mold is not supported by partial inference") ~
6003+ ?- s
6004+ [%face *] (nested-import-invalid shape.s state)
6005+ [%bare *] (nested-import-invalid shape.s state)
6006+ [%pun *] (nested-import-invalid [%ref at.s ~[name.s]] state)
6007+ [%cell *] (nested-samples-invalid items.s env state)
6008+ * ~
6009+ ==
6010+::
6011+++ nested-samples-invalid
6012+ |= [items=(list sample) env=ienv state=istate]
6013+ ^- (unit idiag)
6014+ ?~ items ~
6015+ =/ head=isample-result (infer-sample i.items env state)
6016+ ?: ?=(%| -.head) (sample-import-invalid i.items env state)
6017+ $(items t.items, env env.p.head, state state.p.head)
6018+::
57976019++ infer-simple-shape
57986020 |= [sh=shape state=istate]
57996021 ^- (unit [typ=itype state=istate])
@@ -5802,6 +6024,7 @@
58026024 ?: =(0 aura.sh) `[[%any-atom ~] state]
58036025 `[[%atom aura.sh] state]
58046026 %flag `[[%flag ~] state]
6027+ %noun `[[%noun ~] state]
58056028 %const
58066029 ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
58076030 `[[%const lit.sh] state]
@@ -5828,7 +6051,7 @@
58286051 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
58296052 ?~ found ~
58306053 ?^ vars.u.found ~
5831− `[(itype-in-import typ.u.found u.iface i.t.names.sh) state]
6054+ `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
58326055 =/ found=(unit itype)
58336056 (find-imported-mold i.t.names.sh n externals.state surs.state)
58346057 ?~ found ~
@@ -5865,7 +6088,7 @@
58656088 ?~ vars.u.template ~
58666089 =/ applied=(unit itype) (template-apply u.template types.u.args)
58676090 ?~ applied ~
5868− `[(itype-in-import u.applied u.iface i.t.ref.sh) state.u.args]
6091+ `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
58696092 ?: (lien active.state.u.args |=(x=term =(x n))) ~
58706093 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
58716094 ?~ found
@@ -5895,7 +6118,7 @@
58956118 ?: in-mold.state ~
58966119 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
58976120 ?^ n `[[%var u.n] state]
5898− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state] caps.state])]
6121+ `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
58996122 * ~
59006123 ==
59016124::
@@ -5971,8 +6194,8 @@
59716194 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
59726195::
59736196:: Local definitions generalize only variables outside their enclosing
5974−:: environment and explicit-capital scope. Unresolved groups stay
5975−:: unsupported: this fragment does not infer recursive definitions.
6197+:: environment and explicit-capital scope. Recursive gate groups use
6198+:: monomorphic placeholders while their bodies are checked.
59766199::
59776200+$ ilocal-result (each [env=ienv state=istate] idiag)
59786201++ free-env-vars
@@ -6041,6 +6264,145 @@
60416264 ?~ inferred |
60426265 $(locals t.locals)
60436266::
6267+:: Gather written capitals belonging to one ++. Nested local definitions
6268+:: establish their own scopes; inline gates remain in the enclosing scope.
6269++$ icap-site [name=@t at=span]
6270+++ scope-shape
6271+ |= s=shape
6272+ ^- (list icap-site)
6273+ ?- -.s
6274+ %tvar ~[[name.s at.s]]
6275+ %apply (zing (turn args.s scope-shape))
6276+ %cell (zing (turn fields.s scope-field))
6277+ %union (zing (turn cases.s scope-shape))
6278+ %fn (weld (scope-shape sample.s) (scope-shape product.s))
6279+ %generic
6280+ =/ inside=(list icap-site) (scope-shape body.s)
6281+ (skim inside |=(site=icap-site !(lien vars.s |=(v=@t =(v name.site)))))
6282+ * ~
6283+ ==
6284+::
6285+++ scope-field
6286+ |= f=field
6287+ ^- (list icap-site)
6288+ ?- -.f
6289+ %face (scope-shape shape.f)
6290+ %bare (scope-shape shape.f)
6291+ %pun ~
6292+ ==
6293+::
6294+++ scope-sample
6295+ |= s=sample
6296+ ^- (list icap-site)
6297+ ?- -.s
6298+ %face (scope-shape shape.s)
6299+ %bare (scope-shape shape.s)
6300+ %cell (zing (turn items.s scope-sample))
6301+ * ~
6302+ ==
6303+::
6304+++ scope-pieces
6305+ |= ps=(list piece)
6306+ ^- (list icap-site)
6307+ ?~ ps ~
6308+ =/ first=(list icap-site)
6309+ ?- -.i.ps
6310+ %expr (scope-expr p.i.ps)
6311+ %text ~
6312+ ==
6313+ (weld first $(ps t.ps))
6314+::
6315+++ scope-qsegs
6316+ |= ps=(list qseg)
6317+ ^- (list icap-site)
6318+ ?~ ps ~
6319+ =/ first=(list icap-site)
6320+ ?- -.i.ps
6321+ %expr (scope-expr p.i.ps)
6322+ %knot ~
6323+ ==
6324+ (weld first $(ps t.ps))
6325+::
6326+++ scope-edits
6327+ |= xs=(list edit)
6328+ ^- (list icap-site)
6329+ ?~ xs ~
6330+ =/ first=(list icap-site) (scope-expr val.i.xs)
6331+ (weld first $(xs t.xs))
6332+::
6333+++ scope-items
6334+ |= xs=(list item)
6335+ ^- (list icap-site)
6336+ ?~ xs ~
6337+ =/ first=(list icap-site) (scope-expr val.i.xs)
6338+ (weld first $(xs t.xs))
6339+::
6340+++ scope-arms
6341+ |= xs=(list arm)
6342+ ^- (list icap-site)
6343+ ?~ xs ~
6344+ =/ first=(list icap-site) (scope-expr val.i.xs)
6345+ (weld first $(xs t.xs))
6346+::
6347+++ scope-exprs
6348+ |= xs=(list expr)
6349+ ^- (list icap-site)
6350+ ?~ xs ~
6351+ =/ first=(list icap-site) (scope-expr i.xs)
6352+ (weld first $(xs t.xs))
6353+::
6354+++ scope-expr
6355+ |= e=expr
6356+ ^- (list icap-site)
6357+ ?- -.e
6358+ %str (scope-pieces pieces.e)
6359+ %qath (scope-qsegs segs.e)
6360+ %change (scope-edits edits.e)
6361+ %pair (scope-expr val.e)
6362+ %unit (scope-expr val.e)
6363+ %group (scope-expr inner.e)
6364+ %list (scope-exprs items.e)
6365+ %tuple (scope-items items.e)
6366+ %gate
6367+ =/ first=(list icap-site) (scope-sample sample.e)
6368+ =/ last=(list icap-site) (scope-expr body.e)
6369+ (weld first last)
6370+ %gate-wide
6371+ =/ first=(list icap-site) (scope-sample sample.e)
6372+ =/ last=(list icap-site) (scope-expr body.e)
6373+ (weld first last)
6374+ %call
6375+ =/ first=(list icap-site) (scope-expr head.e)
6376+ =/ last=(list icap-site) (scope-exprs args.e)
6377+ (weld first last)
6378+ %cast
6379+ =/ first=(list icap-site) (scope-shape shape.e)
6380+ =/ last=(list icap-site) (scope-expr val.e)
6381+ (weld first last)
6382+ %trace
6383+ =/ first=(list icap-site) (scope-expr val.e)
6384+ =/ last=(list icap-site) (scope-expr then.e)
6385+ (weld first last)
6386+ %branch
6387+ =/ first=(list icap-site) (scope-expr subject.e)
6388+ =/ last=(list icap-site) (scope-arms arms.e)
6389+ (weld first last)
6390+ %body (scope-expr final.e)
6391+ * ~
6392+ ==
6393+::
6394+++ reserve-cap-sites
6395+ |= [sites=(list icap-site) state=istate]
6396+ ^- istate
6397+ ?~ sites state
6398+ ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
6399+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
6400+::
6401+++ reserve-def-caps
6402+ |= [e=expr state=istate]
6403+ ^- istate
6404+ (reserve-cap-sites (scope-expr e) state)
6405+::
60446406++ infer-local-defs
60456407 |= [ds=(list def) env=ienv state=istate]
60466408 ^- ilocal-result
@@ -6049,26 +6411,62 @@
60496411 |-
60506412 ?~ ds
60516413 ?~ remaining [%& env state]
6052− ?. progressed [%| ["local definitions need unsupported inference" ~]]
6414+ ?. progressed
6415+ =/ pending=(list def) (flop remaining)
6416+ =/ groups=icomponents (graph-components pending (global-value-names pending))
6417+ =/ grouped=(unit [rest=(list def) env=ienv state=istate])
6418+ (try-local-group pending groups env state)
6419+ ?~ grouped [%| ["local definitions need unsupported inference" ~]]
6420+ $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
60536421 $(ds (flop remaining), remaining ~, progressed |)
60546422 =/ d=def i.ds
60556423 ?> ?=(%value -.d)
6056− =/ inferred=iresult (infer-fragment val.d env state)
6424+ =/ local-state=istate (reserve-def-caps val.d state)
6425+ =/ inferred=iresult (infer-fragment val.d env local-state)
6426+ =/ retried=? ?=(%| -.inferred)
6427+ =? inferred retried (infer-recursive-gate d env local-state)
60576428 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6429+ =/ merged=(unit [first=icap second=icap])
6430+ (merged-capitals caps.state.p.inferred sub.state.p.inferred)
6431+ ?^ merged
6432+ [%| ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
6433+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred)
6434+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
60586435 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
60596436 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
60606437 $(ds t.ds, remaining [d remaining])
60616438 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
60626439 $(ds t.ds, remaining [d remaining])
60636440 =/ free=(list @ud)
6064− (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state.p.inferred sub.state.p.inferred))
6441+ (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
60656442 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
60666443 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6067− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred, progressed &)
6444+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
6445+::
6446+:: Try complete cyclic local groups after individual definitions stall.
6447+:: Components with non-gates or unresolved constraints stay unavailable.
6448+::
6449+++ try-local-group
6450+ |= [ds=(list def) groups=icomponents env=ienv state=istate]
6451+ ^- (unit [rest=(list def) env=ienv state=istate])
6452+ ?~ groups ~
6453+ =/ names=(list term) i.groups
6454+ ?. (gth (lent names) 1) $(groups t.groups)
6455+ =/ members=(list def)
6456+ (skim ds |=(d=def &(?=(%value -.d) (lien names |=(n=term =(n name.d))))))
6457+ ?. =((lent members) (lent names)) $(groups t.groups)
6458+ =/ result=ilocal-result (infer-gate-group members env state)
6459+ ?: ?=(%| -.result) $(groups t.groups)
6460+ =/ rest=(list def)
6461+ (skim ds |=(d=def !(lien names |=(n=term =(n name.d)))))
6462+ =/ more=(unit [rest=(list def) env=ienv state=istate])
6463+ $(ds rest, groups t.groups, env env.p.result, state state.p.result)
6464+ ?^ more more
6465+ `[rest env.p.result state.p.result]
60686466::
60696467:: Read only fields of a known record. Unresolved field constraints and
6070−:: ambiguous repeated faces are outside this fragment (doc question:
6071−:: whether duplicate imported Hoon faces are valid or select a field).
6468+:: ambiguous repeated faces are outside this fragment. Imported record
6469+:: spines with repeated names are unavailable when used.
60726470::
60736471++ record-fields-named
60746472 |= [name=term t=itype sub=isub]
@@ -6099,9 +6497,9 @@
60996497 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
61006498 $(fields t.fields, typ i.found)
61016499::
6102−:: Propagate a known union through supported loobean and unit branches. Empty bodies
6103−:: and groups are transparent; bodies with definitions keep their normal
6104−:: scoping and wait for general bidirectional inference.
6500+:: Propagate a known union or list through supported loobean, unit and list
6501+:: branches. Empty bodies and groups are transparent; bodies with definitions
6502+:: keep their normal scoping and wait for general bidirectional inference.
61056503::
61066504++ context-union-branch
61076505 |= e=expr
@@ -6118,6 +6516,8 @@
61186516 ^- iresult
61196517 ?: ?=(%group -.e) $(e inner.e)
61206518 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6519+ ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
6520+ (infer-list-context e expected env state context)
61216521 ?: ?=(%branch -.e)
61226522 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
61236523 ?~ t.arms.e [%| ["branch pattern is not supported by partial inference" ~]]
@@ -6134,6 +6534,9 @@
61346534 [%| ["branch does not cover both loobeans" ~]]
61356535 =/ subject=iresult (infer-fragment subject.e env state)
61366536 ?: ?=(%| -.subject) subject
6537+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
6538+ ?: ?=(%union -.subject-type)
6539+ [%| ["contextual union-pattern branch is not supported by partial inference" ~]]
61376540 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
61386541 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
61396542 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6145,20 +6548,30 @@
61456548 ?: ?=(%| -.value) value
61466549 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
61476550 ?: ?=(%unknown -.fit)
6551+ ?: &(?=(%collection -.expected) =(%list name.expected))
6552+ [%| ["branch list constraint is not supported by partial inference" ~]]
61486553 [%| ["branch union constraint is not supported by partial inference" ~]]
61496554 ?: ?=(%bad -.fit)
6555+ =/ missing=(unit idiag) (missing-union-tag e expected sub.state.p.value context)
6556+ ?^ missing [%| u.missing]
6557+ =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
6558+ ?^ nested [%| u.nested]
6559+ ?: &(?=(%collection -.expected) =(%list name.expected))
6560+ [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
61506561 [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
61516562 [%& expected state.p.value(sub sub.fit, next next.fit)]
61526563::
6153−:: A list literal needs a known list target and the validated prelude list.
6154−:: Its items receive that target one by one; pending constraints elsewhere
6155−:: stay in the threaded state. Other list syntax remains unsupported.
6564+:: A list expression needs a known list target and the validated prelude list.
6565+:: Literal items and unfaced two-item cons cells receive that target one by
6566+:: one; pending constraints elsewhere stay in the threaded state.
61566567::
6157−++ context-list-literal
6568+++ context-list-expression
61586569 |= e=expr
61596570 ^- ?
61606571 ?- -.e
61616572 %list &
6573+ %tuple &
6574+ %lit |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
61626575 %group $(e inner.e)
61636576 %body ?~(defs.e $(e final.e) |)
61646577 * |
@@ -6169,7 +6582,6 @@
61696582 ^- iresult
61706583 ?: ?=(%group -.e) $(e inner.e)
61716584 ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
6172− ?> ?=(%list -.e)
61736585 ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
61746586 ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
61756587 [%| ["list literal needs the standard prelude in partial inference" ~]]
@@ -6182,25 +6594,65 @@
61826594 ?. =(%list name.target) [%| ["list context is not supported by partial inference" ~]]
61836595 ?~ args.target [%| ["list context is not supported by partial inference" ~]]
61846596 ?^ t.args.target [%| ["list context is not supported by partial inference" ~]]
6185− =/ result=iresult (infer-list-items items.e i.args.target env state context)
6186− ?: ?=(%| -.result) result
6187− [%& target state.p.result]
6597+ ?: ?=(%lit -.e)
6598+ ?. |(=(%null form.lit.e) &(=(%term form.lit.e) =(0 val.lit.e)))
6599+ [%| ["list expression is not supported by partial inference" ~]]
6600+ [%& target state]
6601+ ?: ?=(%list -.e)
6602+ =/ result=iresult (infer-list-items items.e i.args.target env state context)
6603+ ?: ?=(%| -.result) result
6604+ [%& target state.p.result]
6605+ ?. ?=(%tuple -.e) [%| ["list expression is not supported by partial inference" ~]]
6606+ ?~ items.e [%| ["cons shape is not supported by partial inference" ~]]
6607+ ?~ t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6608+ ?^ t.t.items.e [%| ["cons shape is not supported by partial inference" ~]]
6609+ ?^ face.i.items.e [%| ["faced cons is not supported by partial inference" ~]]
6610+ ?^ face.i.t.items.e [%| ["faced cons is not supported by partial inference" ~]]
6611+ =/ head=iresult (infer-list-items ~[val.i.items.e] i.args.target env state context)
6612+ ?: ?=(%| -.head) head
6613+ =/ target=itype (itype-walk target sub.state.p.head)
6614+ =/ tail=iresult
6615+ ?: (context-list-expression val.i.t.items.e)
6616+ (infer-list-context val.i.t.items.e target env state.p.head context)
6617+ (infer-fragment val.i.t.items.e env state.p.head)
6618+ ?: ?=(%| -.tail) tail
6619+ =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
6620+ ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
6621+ ?: ?=(%bad -.fit)
6622+ [%| ["list tail does not fit its expected type" ~[[context (site-type-note "expected list" target sub.state.p.tail)] [(span-of val.i.t.items.e) (site-type-note "list tail" typ.p.tail sub.state.p.tail)]]]]
6623+ [%& target state.p.tail(sub sub.fit, next next.fit)]
6624+::
6625+++ infer-open-list-items
6626+ |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6627+ ^- iresult
6628+ ?~ items [%& expected state]
6629+ =/ target=itype (itype-walk expected sub.state)
6630+ =/ value=iresult (infer-call-context-arg i.items target env state context)
6631+ ?: ?=(%| -.value) value
6632+ =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6633+ ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6634+ ?: ?=(%bad -.fit)
6635+ ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
6636+ [%| ["list item widening is not supported by partial inference" ~]]
6637+ [%| ["list items do not have compatible types" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
6638+ ?: (itype-has-tag (itype-normalize expected sub.fit))
6639+ [%| ["list item needs context in partial inference" ~]]
6640+ $(items t.items, state state.p.value(sub sub.fit, next next.fit))
61886641::
61896642++ infer-list-items
61906643 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
61916644 ^- iresult
61926645 ?~ items [%& expected state]
61936646 =/ target=itype (itype-walk expected sub.state)
6194− =/ value=iresult
6195− ?: &(?=(%union -.target) (context-union-branch i.items))
6196− (infer-union-context i.items target env state context)
6197− ?: &(?=(%collection -.target) =(%list name.target) (context-list-literal i.items))
6198− (infer-list-context i.items target env state context)
6199− (infer-fragment i.items env state)
6647+ =/ value=iresult (infer-call-context-arg i.items target env state context)
62006648 ?: ?=(%| -.value) value
62016649 =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
62026650 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
62036651 ?: ?=(%bad -.fit)
6652+ =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
6653+ ?^ missing [%| u.missing]
6654+ =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
6655+ ?^ nested [%| u.nested]
62046656 [%| ["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)]]]]
62056657 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
62066658::
@@ -6348,6 +6800,433 @@
63486800 ?~ joined [%| ["unit branch results need unsupported inference" ~]]
63496801 [%& typ.p.left state.p.right(sub u.joined)]
63506802::
6803+:: Infer pieces in order, retaining their substitutions and pending tags.
6804+:: A bare decimal literal has no outside type constraint, so it takes its
6805+:: normal @ud default here. Other open numeric and aura variables wait for
6806+:: deferred constraints, which this fragment does not implement yet.
6807+++ infer-string-pieces
6808+ |= [ps=(list piece) env=ienv state=istate]
6809+ ^- iresult
6810+ ?~ ps [%& [%atom %t] state]
6811+ ?: ?=(%text -.i.ps) $(ps t.ps)
6812+ =/ item=iresult (infer-fragment p.i.ps env state)
6813+ ?: ?=(%| -.item) item
6814+ =/ t=itype (itype-normalize typ.p.item sub.state.p.item)
6815+ ?: |(?=(%atom -.t) ?=(%any-atom -.t))
6816+ $(ps t.ps, state state.p.item)
6817+ ?: &(?=(%nvar -.t) ?=(%lit -.p.i.ps) =(%number form.lit.p.i.ps))
6818+ $(ps t.ps, state state.p.item)
6819+ ?: &(?=(%collection -.t) =(%list name.t) =(~[[%atom 'tD']] args.t))
6820+ $(ps t.ps, state state.p.item)
6821+ ?: &(?=(%avar -.t) (atom-var-from-cap id.t caps.state.p.item sub.state.p.item))
6822+ [%| ["a generic atom in interpolation needs an aura" ~[[(span-of p.i.ps) "atom with a generic aura"]]]]
6823+ ?: ?=(%cell -.t)
6824+ [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
6825+ [%| ["interpolation type needs unsupported inference" ~]]
6826+::
6827+:: Whole-case coverage for a known union. When a pattern may cover only
6828+:: part of a case, finite loobean refinements are tried below; other
6829+:: partial coverage stays unsupported until the general pattern matrix.
6830++$ imatch ?(%full %none %unknown)
6831+++ union-pattern-items
6832+ |= [ps=(list pattern) t=itype]
6833+ ^- imatch
6834+ ?~ ps %unknown
6835+ ?~ t.ps (union-pattern i.ps t)
6836+ =. t ?:(?=(%face -.t) body.t t)
6837+ ?. ?=(%cell -.t)
6838+ ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
6839+ %unknown
6840+ =/ a=imatch (union-pattern i.ps hed.t)
6841+ =/ b=imatch $(ps t.ps, t tal.t)
6842+ ?: |(=(%none a) =(%none b)) %none
6843+ ?:(&(=(%full a) =(%full b)) %full %unknown)
6844+::
6845+++ union-pattern
6846+ |= [p=pattern t=itype]
6847+ ^- imatch
6848+ =. t ?:(?=(%face -.t) body.t t)
6849+ ?- -.p
6850+ %any %full
6851+ %bind %full
6852+ %lit
6853+ ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
6854+ ?: ?=(%cell -.t) %none
6855+ ?: ?=(%flag -.t)
6856+ ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
6857+ %unknown
6858+ %str ?:(?=(%cell -.t) %none %unknown)
6859+ %cell (union-pattern-items items.p t)
6860+ ==
6861+::
6862+++ union-pattern-has-bind
6863+ |= p=pattern
6864+ ^- ?
6865+ ?: ?=(%bind -.p) &
6866+ ?. ?=(%cell -.p) |
6867+ (lien items.p union-pattern-has-bind)
6868+::
6869+++ union-pattern-bind-items
6870+ |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
6871+ ^- (unit ienv)
6872+ ?~ ps ~
6873+ ?~ t.ps (union-pattern-bind i.ps t env globals)
6874+ =. t ?:(?=(%face -.t) body.t t)
6875+ ?. ?=(%cell -.t) ~
6876+ =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
6877+ ?~ first ~
6878+ $(ps t.ps, t tal.t, env u.first)
6879+::
6880+++ union-pattern-bind
6881+ |= [p=pattern t=itype env=ienv globals=(list term)]
6882+ ^- (unit ienv)
6883+ =. t ?:(?=(%face -.t) body.t t)
6884+ ?: ?=(%bind -.p)
6885+ ?: |(?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
6886+ `[[name.p [t ~]] env]
6887+ ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
6888+ `env
6889+::
6890+:: Split loobean fields into finite refinements for partial patterns.
6891+:: Keep original cases for binder types and preserve whole-case matching
6892+:: before trying refinements. Cap products at 64; unknown, empty or opaque
6893+:: shapes stay unsupported rather than implying complete pattern checking.
6894++$ ifinite [origin=@ud base=itype part=itype]
6895+++ finite-product
6896+ |= [hs=(list itype) ts=(list itype) out=(list itype)]
6897+ ^- (list itype)
6898+ ?~ hs out
6899+ =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
6900+ $(hs t.hs, out (weld rows out))
6901+::
6902+++ finite-type
6903+ |= t=itype
6904+ ^- (unit (list itype))
6905+ ?- -.t
6906+ %flag
6907+ `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
6908+ %face
6909+ =/ body=(unit (list itype)) $(t body.t)
6910+ ?~ body ~
6911+ `(turn u.body |=(x=itype [%face name.t x]))
6912+ %cell
6913+ =/ hed=(unit (list itype)) $(t hed.t)
6914+ ?~ hed ~
6915+ =/ tal=(unit (list itype)) $(t tal.t)
6916+ ?~ tal ~
6917+ ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
6918+ `(finite-product u.hed u.tal ~)
6919+ * `~[t]
6920+ ==
6921+::
6922+++ finite-cases
6923+ |= [xs=(list itype) out=(list ifinite) origin=@ud]
6924+ ^- (unit (list ifinite))
6925+ ?~ xs `out
6926+ =/ parts=(unit (list itype)) (finite-type i.xs)
6927+ ?~ parts ~
6928+ ?: (gth (add (lent out) (lent u.parts)) 64) ~
6929+ =/ rows=(list ifinite) (turn u.parts |=(t=itype [origin i.xs t]))
6930+ $(xs t.xs, out (weld out rows), origin +(origin))
6931+::
6932+++ infer-known-union-whole
6933+ |= [e=expr env=ienv state=istate]
6934+ ^- (unit iresult)
6935+ ?> ?=(%branch -.e)
6936+ =/ subject=iresult (infer-fragment subject.e env state)
6937+ ?: ?=(%| -.subject) `subject
6938+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6939+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
6940+ =/ cases=(list itype) cases.typ
6941+ =/ remaining=(list itype) cases
6942+ =/ arms=(list arm) arms.e
6943+ =/ st=istate state.p.subject
6944+ =/ answer=(unit itype) ~
6945+ |-
6946+ ?~ arms
6947+ ?^ remaining
6948+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
6949+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
6950+ `[%& u.answer st]
6951+ =/ a=arm i.arms
6952+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
6953+ ~
6954+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
6955+ ?~ matching
6956+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
6957+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6958+ `[%| ["union pattern is not supported by partial inference" ~]]
6959+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
6960+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6961+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
6962+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
6963+ =/ body=iresult (infer-fragment val.a u.bound st)
6964+ ?: ?=(%| -.body) `body
6965+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
6966+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
6967+ ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
6968+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
6969+::
6970+++ infer-known-union-context-whole
6971+ |= [e=expr expected=itype env=ienv state=istate context=span]
6972+ ^- (unit iresult)
6973+ ?> ?=(%branch -.e)
6974+ =/ subject=iresult (infer-fragment subject.e env state)
6975+ ?: ?=(%| -.subject) `subject
6976+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
6977+ ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
6978+ =/ cases=(list itype) cases.typ
6979+ =/ remaining=(list itype) cases
6980+ =/ arms=(list arm) arms.e
6981+ =/ st=istate state.p.subject
6982+ =/ answer=(unit itype) ~
6983+ |-
6984+ ?~ arms
6985+ ?^ remaining
6986+ `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
6987+ ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
6988+ `[%& expected st]
6989+ =/ a=arm i.arms
6990+ ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
6991+ ~
6992+ =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
6993+ ?~ matching
6994+ ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
6995+ `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
6996+ `[%| ["union pattern is not supported by partial inference" ~]]
6997+ ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
6998+ `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
6999+ =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7000+ ?~ bound `[%| ["pattern binder shadows a name" ~]]
7001+ =/ body=iresult (infer-call-context-arg val.a expected u.bound st context)
7002+ ?: ?=(%| -.body) `body
7003+ =/ fit=ifit (itype-fit typ.p.body expected sub.state.p.body next.state.p.body)
7004+ ?: ?=(%unknown -.fit) `[%| ["union branch result constraint is not supported by partial inference" ~]]
7005+ ?: ?=(%bad -.fit)
7006+ =/ missing=(unit idiag) (missing-union-tag val.a expected sub.state.p.body context)
7007+ ?^ missing `[%| u.missing]
7008+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body expected sub.state.p.body next.state.p.body context)
7009+ ?^ nested `[%| u.nested]
7010+ `[%| ["union branch arm does not fit its expected type" ~[[context "expected type"] [(span-of val.a) "branch arm"]]]]
7011+ ?: (itype-has-tag (itype-normalize expected sub.fit))
7012+ `[%| ["union branch result needs context in partial inference" ~]]
7013+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body(sub sub.fit, next next.fit), answer `expected)
7014+::
7015+++ infer-known-union-finite
7016+ |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7017+ ^- iresult
7018+ ?> ?=(%branch -.e)
7019+ =/ subject=iresult (infer-fragment subject.e env state)
7020+ ?: ?=(%| -.subject) subject
7021+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7022+ ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7023+ =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7024+ ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7025+ =/ cases=(list ifinite) u.expanded
7026+ =/ remaining=(list ifinite) cases
7027+ =/ arms=(list arm) arms.e
7028+ =/ st=istate state.p.subject
7029+ =/ answer=(unit itype) ~
7030+ |-
7031+ ?~ arms
7032+ ?^ remaining
7033+ [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
7034+ ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
7035+ ?~ expected [%& u.answer st]
7036+ [%& typ.u.expected st]
7037+ =/ a=arm i.arms
7038+ ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
7039+ [%| ["partial union pattern is not supported by partial inference" ~]]
7040+ =/ matching=(list ifinite) (skim remaining |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7041+ ?~ matching
7042+ ?: (lien cases |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7043+ [%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7044+ [%| ["union pattern is not supported by partial inference" ~]]
7045+ ?: &((union-pattern-has-bind pat.a) (lien t.matching |=(c=ifinite !=(origin.c origin.i.matching))))
7046+ [%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7047+ =/ bound=(unit ienv) (union-pattern-bind pat.a base.i.matching env globals.st)
7048+ ?~ bound [%| ["pattern binder shadows a name" ~]]
7049+ =/ body=iresult
7050+ ?~ expected (infer-fragment val.a u.bound st)
7051+ (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7052+ ?: ?=(%| -.body) body
7053+ ?^ expected
7054+ =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7055+ ?: ?=(%unknown -.fit) [%| ["union branch result constraint is not supported by partial inference" ~]]
7056+ ?: ?=(%bad -.fit)
7057+ =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7058+ ?^ missing [%| u.missing]
7059+ =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body typ.u.expected sub.state.p.body next.state.p.body context.u.expected)
7060+ ?^ nested [%| u.nested]
7061+ [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7062+ ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7063+ [%| ["union branch result needs context in partial inference" ~]]
7064+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body(sub sub.fit, next next.fit), answer `typ.u.expected)
7065+ =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7066+ =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7067+ ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
7068+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
7069+::
7070+++ infer-known-union-branch
7071+ |= [e=expr env=ienv state=istate]
7072+ ^- iresult
7073+ =/ whole=(unit iresult) (infer-known-union-whole e env state)
7074+ ?~ whole (infer-known-union-finite e env state ~)
7075+ u.whole
7076+::
7077+++ infer-known-union-context
7078+ |= [e=expr expected=itype env=ienv state=istate context=span]
7079+ ^- iresult
7080+ =/ whole=(unit iresult) (infer-known-union-context-whole e expected env state context)
7081+ ?~ whole (infer-known-union-finite e env state `[expected context])
7082+ u.whole
7083+::
7084+++ known-union-subject
7085+ |= [e=expr env=ienv state=istate]
7086+ ^- (unit itype)
7087+ ?. ?=(%wing -.e) ~
7088+ =/ subject=iresult (infer-fragment e env state)
7089+ ?: ?=(%| -.subject) ~
7090+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7091+ ?. ?=(%union -.typ) ~
7092+ `typ
7093+::
7094+:: Infer changes only against a fully known record spine. Retain the
7095+:: target type; unknown spines and repeated edits remain unsupported.
7096+++ change-spine-known
7097+ |= [t=itype sub=isub]
7098+ ^- ?
7099+ =. t (itype-walk t sub)
7100+ ?: ?=(%face -.t) &
7101+ ?. ?=(%cell -.t) |
7102+ =/ first=itype (itype-walk hed.t sub)
7103+ ?. ?=(%face -.first) |
7104+ $(t tal.t)
7105+::
7106+++ infer-change-edits
7107+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
7108+ ^- iresult
7109+ ?~ edits [%& target state]
7110+ =/ entry=edit i.edits
7111+ ?: (lien seen |=(name=term =(name name.entry)))
7112+ [%| ["repeated change fields are not supported by partial inference" ~]]
7113+ ?. (change-spine-known target sub.state)
7114+ [%| ["change target needs a known record in partial inference" ~]]
7115+ =/ found=(list itype) (record-fields-named name.entry target sub.state)
7116+ ?~ found
7117+ [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
7118+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
7119+ =/ expected=itype i.found
7120+ =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
7121+ ?: ?=(%| -.value) value
7122+ =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
7123+ ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
7124+ ?: ?=(%bad -.fit)
7125+ [%| ["change field and replacement do not unify" ~[[at.entry (site-type-note "expected replacement" expected sub.state.p.value)] [(span-of val.entry) (site-type-note "replacement" typ.p.value sub.state.p.value)]]]]
7126+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
7127+::
7128+:: Backtick constructs the canonical prelude unit, after checking its
7129+:: prepared template has the standard null and [~ u=A] cases.
7130+++ standard-unit-template
7131+ |= [template=ischeme at=path]
7132+ ^- ?
7133+ ?. =(at /lib/jibb/prelude/jibb) |
7134+ ?~ vars.template |
7135+ ?^ t.vars.template |
7136+ =/ v=@ud i.vars.template
7137+ =/ nil=itype [%const [%null %n 0 '~']]
7138+ =/ expected=itype
7139+ [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
7140+ =(typ.template expected)
7141+::
7142+:: A named missing-case diagnostic needs more than a failed fit: a case
7143+:: with that tag but the wrong payload is not a missing case. Unknown
7144+:: shapes and atom types that accept terms keep the proof conservative.
7145++$ itag-presence ?(%yes %no %maybe)
7146+++ tag-presence-cases
7147+ |= [cases=(list itype) value=@ sub=isub]
7148+ ^- itag-presence
7149+ ?~ cases %no
7150+ =/ first=itag-presence (tag-presence i.cases value sub)
7151+ ?: =(%yes first) %yes
7152+ =/ rest=itag-presence $(cases t.cases)
7153+ ?: =(%yes rest) %yes
7154+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7155+ %no
7156+::
7157+++ tag-presence
7158+ |= [t=itype value=@ sub=isub]
7159+ ^- itag-presence
7160+ =. t (itype-walk t sub)
7161+ ?- -.t
7162+ %const ?:(=(value val.literal.t) %yes %no)
7163+ %flag ?:(|(=(value 0) =(value 1)) %yes %no)
7164+ %atom ?:(|(=(%tas aura.t) =(%ta aura.t)) %maybe %no)
7165+ %face $(t body.t)
7166+ %cell
7167+ =/ first=itag-presence $(t hed.t)
7168+ ?: =(%yes first) %yes
7169+ =/ rest=itag-presence $(t tal.t)
7170+ ?: =(%yes rest) %yes
7171+ ?: |(=(%maybe first) =(%maybe rest)) %maybe
7172+ %no
7173+ %union (tag-presence-cases cases.t value sub)
7174+ * %maybe
7175+ ==
7176+::
7177+++ missing-union-tag
7178+ |= [e=expr expected=itype sub=isub context=span]
7179+ ^- (unit idiag)
7180+ ?. ?=(%lit -.e) ~
7181+ ?. =(%term form.lit.e) ~
7182+ =. expected (itype-walk expected sub)
7183+ |-
7184+ ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
7185+ ?. ?=(%union -.expected) ~
7186+ ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
7187+ =/ label=tape
7188+ ?~ label.expected "union {(show-itype expected sub)}"
7189+ (show-itype expected sub)
7190+ `["{label} has no case `{(trip txt.lit.e)}`" ~[[context "expected union"] [(span-of e) "tag"]]]
7191+::
7192+:: Locate a missing tag inside a syntactic tuple only by replaying the
7193+:: directional fit in source order. Uncertain or earlier failures stop
7194+:: the walk, preserving the generic diagnostic rather than guessing.
7195+++ nested-missing-tag
7196+ |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7197+ ^- (unit idiag)
7198+ =/ original=[left=itype right=itype] [actual expected]
7199+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7200+ =/ fit=ifit (itype-fit actual expected sub next)
7201+ ?. ?=(%bad -.fit) ~
7202+ =. actual (itype-walk actual sub)
7203+ =. expected (itype-walk expected sub)
7204+ ?: &(?=(%face -.actual) ?=(%face -.expected))
7205+ ?. =(name.actual name.expected) ~
7206+ $(actual body.actual, expected body.expected)
7207+ ?: ?=(%face -.actual) $(actual body.actual)
7208+ ?: ?=(%face -.expected) $(expected body.expected)
7209+ =/ direct=(unit idiag) (missing-union-tag e expected sub context)
7210+ ?^ direct direct
7211+ ?. ?=(%tuple -.e) ~
7212+ (nested-missing-items items.e actual expected sub next context)
7213+::
7214+++ nested-missing-items
7215+ |= [items=(list item) actual=itype expected=itype sub=isub next=@ud context=span]
7216+ ^- (unit idiag)
7217+ ?~ items ~
7218+ ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
7219+ =/ original=[left=itype right=itype] [actual expected]
7220+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7221+ =. actual (itype-walk actual sub)
7222+ =. expected (itype-walk expected sub)
7223+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7224+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7225+ ?: ?=(%bad -.first)
7226+ (nested-missing-tag val.i.items hed.actual hed.expected sub next context)
7227+ ?. ?=(%ok -.first) ~
7228+ $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7229+::
63517230++ infer-fragment
63527231 |= [e=expr env=ienv state=istate]
63537232 ^- iresult
@@ -6365,10 +7244,30 @@
63657244 %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
63667245 %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
63677246 ==
6368− %str
6369− =/ interpolated=? (lien pieces.e |=(p=piece ?=(%expr -.p)))
6370− ?: interpolated [%| ["interpolation is not supported by partial inference" ~]]
6371− [%& [%atom %t] state]
7247+ %unit
7248+ ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
7249+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7250+ ?~ standard [%| ["unit construction needs the standard prelude in partial inference" ~]]
7251+ ?. (standard-unit-template u.standard at.u.prelude.state)
7252+ [%| ["unit construction needs the standard prelude in partial inference" ~]]
7253+ =/ value=iresult $(e val.e)
7254+ ?: ?=(%| -.value) value
7255+ =/ result=(unit itype) (template-apply u.standard ~[typ.p.value])
7256+ ?~ result [%| ["unit construction is not supported by partial inference" ~]]
7257+ [%& u.result state.p.value]
7258+ %list
7259+ ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
7260+ ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7261+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7262+ =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
7263+ ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
7264+ ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
7265+ [%| ["list literal needs the standard prelude in partial inference" ~]]
7266+ =/ element=itype [%var next.state]
7267+ =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
7268+ ?: ?=(%| -.result) result
7269+ [%& [%collection %list ~[element]] state.p.result]
7270+ %str (infer-string-pieces pieces.e env state)
63727271 %wing
63737272 ?~ names.e [%| ["empty wing" ~]]
63747273 ?^ t.names.e
@@ -6377,7 +7276,7 @@
63777276 ?~ iface (infer-field-wing names.e env state)
63787277 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
63797278 ?~ member [%| ["module member is not available to partial inference" ~]]
6380− =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e)
7279+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
63817280 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
63827281 [%& typ.instance state.instance]
63837282 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
@@ -6390,6 +7289,11 @@
63907289 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
63917290 [%& typ.instance state.instance]
63927291 %group $(e inner.e)
7292+ %change
7293+ ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
7294+ =/ target=iresult $(e [%wing at.e target.e])
7295+ ?: ?=(%| -.target) target
7296+ (infer-change-edits edits.e typ.p.target env state.p.target ~)
63937297 %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
63947298 %trace
63957299 =/ traced=iresult $(e val.e)
@@ -6417,19 +7321,26 @@
64177321 %branch
64187322 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
64197323 ?~ t.arms.e (infer-cell-branch e env state)
6420− ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
7324+ ?^ t.t.arms.e (infer-known-union-branch e env state)
7325+ =/ known=(unit itype) (known-union-subject subject.e env state)
7326+ ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
7327+ (infer-known-union-branch e env state)
64217328 =/ x=arm i.arms.e
64227329 =/ y=arm i.t.arms.e
64237330 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
64247331 (infer-unit-branch e env state ~)
6425− ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
6426− ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
7332+ ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7333+ ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
64277334 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
6428− [%| ["branch pattern is not supported by partial inference" ~]]
7335+ (infer-known-union-branch e env state)
7336+ ?^ known (infer-known-union-branch e env state)
64297337 ?: =(val.lit.pat.x val.lit.pat.y)
64307338 [%| ["branch does not cover both loobeans" ~]]
64317339 =/ subject=iresult $(e subject.e)
64327340 ?: ?=(%| -.subject) subject
7341+ =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
7342+ ?: ?=(%union -.subject-type)
7343+ [%| ["union-pattern branch subject is not supported by partial inference" ~]]
64337344 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
64347345 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
64357346 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6456,44 +7367,54 @@
64567367 [%& typ.p.left state.p.right(sub u.joined)]
64577368 %cast
64587369 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
6459− ?~ target [%| ["cast mold is not supported by partial inference" ~]]
7370+ ?~ target
7371+ =/ diag=(unit idiag) (nested-import-invalid shape.e state)
7372+ ?^ diag [%| u.diag]
7373+ [%| ["cast mold is not supported by partial inference" ~]]
64607374 =/ value=iresult
6461− ?: &(?=(%union -.typ.u.target) (context-union-branch val.e))
6462− (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6463− ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-list-literal val.e))
6464− (infer-list-context val.e typ.u.target env state.u.target at.shape.e)
6465− $(e val.e, state state.u.target)
7375+ (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
64667376 ?: ?=(%| -.value) value
64677377 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
64687378 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
64697379 ?: ?=(%bad -.fit)
7380+ =/ missing=(unit idiag) (missing-union-tag val.e typ.u.target sub.state.p.value at.shape.e)
7381+ ?^ missing [%| u.missing]
7382+ =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value at.shape.e)
7383+ ?^ nested [%| u.nested]
64707384 [%| ["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)]]]]
64717385 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
64727386 [%& merged state.p.value(sub sub.fit, next next.fit)]
64737387 %crash [%& [%var next.state] state(next +(next.state))]
64747388 %gate
64757389 =/ sam=isample-result (infer-sample sample.e env state)
6476− ?: ?=(%| -.sam) [%| [p.sam ~]]
7390+ ?: ?=(%| -.sam)
7391+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7392+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7393+ [%| [p.sam ~]]
64777394 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
64787395 ?: ?=(%| -.body) body
64797396 [%& [%fn typ.p.sam typ.p.body] state.p.body]
64807397 %gate-wide
64817398 =/ sam=isample-result (infer-sample sample.e env state)
6482− ?: ?=(%| -.sam) [%| [p.sam ~]]
7399+ ?: ?=(%| -.sam)
7400+ =/ diag=(unit idiag) (sample-import-invalid sample.e env state)
7401+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
7402+ [%| [p.sam ~]]
64837403 =/ body=iresult $(e body.e, env env.p.sam, state state.p.sam)
64847404 ?: ?=(%| -.body) body
64857405 [%& [%fn typ.p.sam typ.p.body] state.p.body]
64867406 %call
64877407 ?~ args.e [%| ["call has no argument" ~]]
6488− ?^ t.args.e [%| ["multiple arguments are not supported by partial inference" ~]]
64897408 =/ head=iresult $(e head.e)
64907409 ?: ?=(%| -.head) head
64917410 =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
64927411 =/ arg=iresult
6493− ?: &(?=(%fn -.head-type) ?=(%union -.sample.head-type) (context-union-branch i.args.e))
6494− (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6495− ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-list-literal i.args.e))
6496− (infer-list-context i.args.e sample.head-type env state.p.head (span-of head.e))
7412+ ?^ t.args.e
7413+ ?: ?=(%fn -.head-type)
7414+ (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
7415+ (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
7416+ ?: ?=(%fn -.head-type)
7417+ (infer-call-context-arg i.args.e sample.head-type env state.p.head (span-of head.e))
64977418 $(e i.args.e, state state.p.head)
64987419 ?: ?=(%| -.arg) arg
64997420 =/ st=istate state.p.arg
@@ -6502,7 +7423,19 @@
65027423 =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
65037424 ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
65047425 ?: ?=(%bad -.fit)
6505− [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7426+ ?~ t.args.e
7427+ =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
7428+ ?^ missing [%| u.missing]
7429+ =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
7430+ ?^ nested [%| u.nested]
7431+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
7432+ =/ bad=(unit [at=span typ=itype])
7433+ (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
7434+ =/ whole-args=span
7435+ [beg:(span-of i.args.e) end:(span-of (rear args.e))]
7436+ =/ arg-at=span ?~(bad whole-args at.u.bad)
7437+ =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7438+ [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]
65067439 ?: &((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))
65077440 [%| ["call result face propagation is not supported by partial inference" ~]]
65087441 [%& product.ht st(sub sub.fit, next next.fit)]
@@ -6514,6 +7447,142 @@
65147447 * [%| ["expression is not supported by partial inference" ~]]
65157448 ==
65167449::
7450+:: Locate a definite failing argument after the complete sample fit has
7451+:: failed. If an intermediate fit is uncertain, retain the whole argument
7452+:: span rather than assigning blame to a particular argument.
7453+::
7454+++ call-error-site
7455+ |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
7456+ ^- (unit [at=span typ=itype])
7457+ ?~ args ~
7458+ =/ original=[left=itype right=itype] [actual expected]
7459+ ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7460+ =. actual (itype-walk actual sub)
7461+ =. expected (itype-walk expected sub)
7462+ ?: &(?=(%face -.expected) !?=(%face -.actual))
7463+ $(expected body.expected)
7464+ ?~ t.args
7465+ =/ fit=ifit (itype-fit actual expected sub next)
7466+ ?. ?=(%bad -.fit) ~
7467+ `[(span-of i.args) (itype-normalize actual sub)]
7468+ ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7469+ =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7470+ ?: ?=(%bad -.first) `[(span-of i.args) (itype-normalize hed.actual sub)]
7471+ ?: ?=(%unknown -.first) ~
7472+ $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7473+::
7474+:: Context can help a call argument or cast value while the final fit
7475+:: checks the complete right-nested type, including any written faces.
7476+::
7477+:: Context can resolve the payload of a canonical prelude unit, but an
7478+:: unrelated union with a similar noun shape is not the same mold.
7479+++ infer-unit-context
7480+ |= [e=expr expected=itype env=ienv state=istate context=span]
7481+ ^- iresult
7482+ ?> ?=(%unit -.e)
7483+ ?> ?=(%union -.expected)
7484+ ?~ prelude.state (infer-fragment e env state)
7485+ =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7486+ ?~ standard (infer-fragment e env state)
7487+ ?. (standard-unit-template u.standard at.u.prelude.state) (infer-fragment e env state)
7488+ ?. =(origin.expected `[at.u.prelude.state %unit]) (infer-fragment e env state)
7489+ ?~ args.expected (infer-fragment e env state)
7490+ ?^ t.args.expected (infer-fragment e env state)
7491+ =/ payload=itype i.args.expected
7492+ =/ canonical=(unit itype) (template-apply u.standard ~[payload])
7493+ ?~ canonical (infer-fragment e env state)
7494+ ?> ?=(%union -.u.canonical)
7495+ ?. =((itype-normalize expected(label ~) sub.state) (itype-normalize u.canonical(label ~) sub.state))
7496+ (infer-fragment e env state)
7497+ =/ value=iresult (infer-call-context-arg val.e payload env state context)
7498+ ?: ?=(%| -.value) value
7499+ =/ fit=ifit (itype-fit typ.p.value payload sub.state.p.value next.state.p.value)
7500+ ?: ?=(%unknown -.fit) [%| ["unit payload constraint is not supported by partial inference" ~]]
7501+ ?: ?=(%bad -.fit)
7502+ =/ missing=(unit idiag) (missing-union-tag val.e payload sub.state.p.value context)
7503+ ?^ missing [%| u.missing]
7504+ =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
7505+ ?^ nested [%| u.nested]
7506+ [%| ["unit payload does not fit its expected type" ~[[context (site-type-note "expected unit payload" payload sub.state.p.value)] [(span-of val.e) (site-type-note "payload" typ.p.value sub.state.p.value)]]]]
7507+ [%& expected state.p.value(sub sub.fit, next next.fit)]
7508+::
7509+++ infer-call-context-arg
7510+ |= [e=expr expected=itype env=ienv state=istate context=span]
7511+ ^- iresult
7512+ ?: ?=(%group -.e) $(e inner.e)
7513+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7514+ ?: ?=(%trace -.e)
7515+ =/ traced=iresult (infer-fragment val.e env state)
7516+ ?: ?=(%| -.traced) traced
7517+ $(e then.e, state state.p.traced)
7518+ =/ target=itype (itype-walk expected sub.state)
7519+ |-
7520+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7521+ :: In a loobean-singleton context retain the written loobean noun;
7522+ :: the usual final fit decides whether that value is permitted.
7523+ =/ singleton=(unit itype)
7524+ ?. ?=(%lit -.e) ~
7525+ ?. =(%loobean form.lit.e) ~
7526+ ?. ?=(%const -.target) ~
7527+ ?. =(%loobean form.literal.target) ~
7528+ `[%const lit.e]
7529+ ?^ singleton [%& u.singleton state]
7530+ =/ known=(unit itype)
7531+ ?: ?=(%branch -.e) (known-union-subject subject.e env state)
7532+ ~
7533+ ?: &(?=(^ known) ?=(~ (unit-union-payload u.known)))
7534+ (infer-known-union-context e target env state context)
7535+ ?: &(?=(%union -.target) ?=(%unit -.e))
7536+ (infer-unit-context e target env state context)
7537+ ?: &(?=(%union -.target) (context-union-branch e))
7538+ (infer-union-context e target env state context)
7539+ ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
7540+ (infer-union-context e target env state context)
7541+ ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
7542+ (infer-list-context e target env state context)
7543+ ?: &(?=(%cell -.target) ?=(%tuple -.e))
7544+ (infer-call-context-items items.e target env state context)
7545+ (infer-fragment e env state)
7546+::
7547+:: Preserve each written face; the final complete sample fit checks faces.
7548+++ infer-call-context-items
7549+ |= [items=(list item) expected=itype env=ienv state=istate context=span]
7550+ ^- iresult
7551+ ?~ items [%| ["empty cell is not supported by partial inference" ~]]
7552+ ?~ t.items
7553+ =/ last=iresult (infer-call-context-arg val.i.items expected env state context)
7554+ ?: ?=(%| -.last) last
7555+ =/ typ=itype typ.p.last
7556+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7557+ [%& typ state.p.last]
7558+ =/ target=itype (itype-walk expected sub.state)
7559+ |-
7560+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7561+ ?. ?=(%cell -.target) (infer-simple-items items env state)
7562+ =/ head=iresult (infer-call-context-arg val.i.items hed.target env state context)
7563+ ?: ?=(%| -.head) head
7564+ =/ typ=itype typ.p.head
7565+ =. typ ?~(face.i.items typ [%face u.face.i.items typ])
7566+ =/ tail=iresult (infer-call-context-items t.items tal.target env state.p.head context)
7567+ ?: ?=(%| -.tail) tail
7568+ [%& [%cell typ typ.p.tail] state.p.tail]
7569+::
7570+++ infer-call-context-args
7571+ |= [args=(list expr) expected=itype env=ienv state=istate context=span]
7572+ ^- iresult
7573+ ?~ args [%| ["call has no argument" ~]]
7574+ ?~ t.args (infer-call-context-arg i.args expected env state context)
7575+ =/ target=itype (itype-walk expected sub.state)
7576+ |-
7577+ ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
7578+ ?. ?=(%cell -.target)
7579+ (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
7580+ =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
7581+ ?: ?=(%| -.head) head
7582+ =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
7583+ ?: ?=(%| -.tail) tail
7584+ [%& [%cell typ.p.head typ.p.tail] state.p.tail]
7585+::
65177586:: Tuple and record expressions preserve their explicitly written faces.
65187587::
65197588++ infer-simple-items
@@ -6529,8 +7598,43 @@
65297598 ?: ?=(%| -.tail) tail
65307599 [%& [%cell ht typ.p.tail] state.p.tail]
65317600::
6532−:: A single two-binder cell pattern covers every value of a cell type.
6533−:: No other pattern matrix is implemented here.
7601+:: A single all-binder cell pattern covers a known cell spine; the final
7602+:: binder captures the remaining noun. Other pattern matrices stay partial.
7603+::
7604+:: Validate binders before reading the subject, preserving shadow-error
7605+:: precedence. The last binder receives the entire remaining tail.
7606+++ cell-pattern-names
7607+ |= [pats=(list pattern) env=ienv globals=(list term) seen=(list term)]
7608+ ^- (each (list term) @t)
7609+ ?~ pats [%& ~]
7610+ ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
7611+ =/ name=term name.i.pats
7612+ ?: |(?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
7613+ [%| 'pattern shadows a name']
7614+ =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
7615+ ?: ?=(%| -.rest) rest
7616+ [%& [name p.rest]]
7617+::
7618+++ cell-pattern-types
7619+ |= [names=(list term) env=ienv next=@ud]
7620+ ^- [typ=itype env=ienv next=@ud]
7621+ ?~ names !!
7622+ =/ head=itype [%var next]
7623+ =/ scope=ienv [[i.names [head ~]] env]
7624+ ?~ t.names [head scope +(next)]
7625+ =/ tail=[typ=itype env=ienv next=@ud] $(names t.names, env scope, next +(next))
7626+ [[%cell head typ.tail] env.tail next.tail]
7627+::
7628+:: At every position that must be a cell, opaque or sum types may still
7629+:: contain cells. Do not report a definite mismatch without unfolding them.
7630+++ cell-pattern-spine-unknown
7631+ |= [typ=itype names=(list term) sub=isub]
7632+ ^- ?
7633+ ?~ names |
7634+ ?~ t.names |
7635+ =. typ (itype-walk typ sub)
7636+ ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
7637+ |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
65347638::
65357639++ infer-cell-branch
65367640 |= [e=expr env=ienv state=istate]
@@ -6542,25 +7646,22 @@
65427646 =/ pats=(list pattern) items.pat.arm
65437647 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
65447648 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6545− ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6546− ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6547− ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6548− =/ one=term name.i.pats
6549− =/ two=term name.i.t.pats
6550− ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
6551− [%| ["pattern shadows a name" ~]]
7649+ =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
7650+ ?: ?=(%| -.names) [%| [(trip p.names) ~]]
65527651 =/ subject=iresult (infer-fragment subject.e env state)
65537652 ?: ?=(%| -.subject) subject
65547653 =/ st=istate state.p.subject
6555− ?: (itype-has-recursive (itype-normalize typ.p.subject sub.st))
7654+ =/ subject-type=itype (itype-normalize typ.p.subject sub.st)
7655+ ?: (itype-has-recursive subject-type)
65567656 [%| ["recursive pattern is not supported by partial inference" ~]]
65577657 ?: (itype-has-face typ.p.subject sub.st)
65587658 [%| ["record patterns are not supported by partial inference" ~]]
6559− =/ head=itype [%var next.st]
6560− =/ tail=itype [%var +(next.st)]
6561− =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
7659+ ?: (cell-pattern-spine-unknown subject-type p.names sub.st)
7660+ [%| ["cell pattern subject is not supported by partial inference" ~]]
7661+ =/ binders=[typ=itype env=ienv next=@ud] (cell-pattern-types p.names env next.st)
7662+ =/ sub=(unit isub) (itype-unify typ.p.subject typ.binders sub.st)
65627663 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
6563− (infer-fragment val.arm [[one [head ~]] [two [tail ~]] env] st(next (add 2 next.st), sub u.sub))
7664+ (infer-fragment val.arm env.binders st(next next.binders, sub u.sub))
65647665::
65657666++ show-itype
65667667 |= [t=itype sub=isub]
@@ -6579,6 +7680,7 @@
65797680 %atom "@{(trip aura.t)}"
65807681 %any-atom "@"
65817682 %flag "?"
7683+ %noun "*"
65827684 %tag (trip txt.literal.t)
65837685 %const (trip txt.literal.t)
65847686 %union
@@ -6626,6 +7728,7 @@
66267728 %atom |
66277729 %any-atom |
66287730 %flag |
7731+ %noun |
66297732 %tag |
66307733 %const |
66317734 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
@@ -6650,8 +7753,8 @@
66507753:: A capital in a written mold is generalized with its enclosing ++.
66517754:: Atom constraints may remain generic; until full rigidity checking
66527755:: is implemented, do not report a type if one became more specific.
6653−:: Whether distinct written capitals may become equal is a doc question;
6654−:: the partial checker leaves such inference unsupported for now.
7756+:: Distinct written capitals cannot be forced equal; use the same
7757+:: capital where a type must be shared (Decisions 2026-10-30).
66557758::
66567759++ cap-id-in
66577760 |= [n=@ud caps=icaps sub=isub]
@@ -6667,6 +7770,35 @@
66677770 ?: =(n u.ident) &
66687771 $(caps t.caps)
66697772::
7773+++ cap-with-id
7774+ |= [n=@ud caps=icaps sub=isub]
7775+ ^- (unit icap)
7776+ ?~ caps ~
7777+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7778+ =/ ident=(unit @ud)
7779+ ?+ -.resolved ~
7780+ %var `id.resolved
7781+ %avar `id.resolved
7782+ ==
7783+ ?~ ident $(caps t.caps)
7784+ ?: =(n u.ident) `i.caps
7785+ $(caps t.caps)
7786+::
7787+++ merged-capitals
7788+ |= [caps=icaps sub=isub]
7789+ ^- (unit [first=icap second=icap])
7790+ ?~ caps ~
7791+ =/ resolved=itype (itype-walk [%var id.i.caps] sub)
7792+ =/ ident=(unit @ud)
7793+ ?+ -.resolved ~
7794+ %var `id.resolved
7795+ %avar `id.resolved
7796+ ==
7797+ ?~ ident $(caps t.caps)
7798+ =/ found=(unit icap) (cap-with-id u.ident t.caps sub)
7799+ ?^ found `[u.found i.caps]
7800+ $(caps t.caps)
7801+::
66707802++ constrained-capitals
66717803 |= [caps=icaps sub=isub]
66727804 ^- ?
@@ -6705,6 +7837,7 @@
67057837 %atom |
67067838 %any-atom |
67077839 %flag |
7840+ %noun |
67087841 %tag |
67097842 %const |
67107843 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
@@ -6756,9 +7889,9 @@
67567889::
67577890:: Build the supported part of the value environment in dependency order.
67587891:: Each pass adds successful definitions. Forward references become
6759−:: available on a later pass; recursive groups and unsupported syntax do
6760−:: not enter the environment. Generalized definitions are closed, so a
6761−:: use instantiates its variables afresh.
7892+:: available on a later pass; unsupported syntax does not enter the
7893+:: environment. Generalized definitions are closed, so a use instantiates
7894+:: its variables afresh.
67627895::
67637896++ global-value-names
67647897 |= ds=(list def)
@@ -6776,6 +7909,317 @@
67767909 ?~ t.hits &
67777910 |
67787911::
7912+:: A top-level gate may refer to itself through one monomorphic placeholder.
7913+:: Its declared sample is inferred first and preserves its field faces.
7914+:: Unify the completed body with that placeholder before generalization;
7915+:: reporting repeats the same check instead of instantiating the gate's
7916+:: generalized interface inside its own body. Mutual groups stay unsupported.
7917+::
7918+++ direct-self-call
7919+ |= [e=expr name=term]
7920+ ^- ?
7921+ ?: ?=(%group -.e) $(e inner.e)
7922+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7923+ ?. ?=(%call -.e) |
7924+ ?. ?=(%wing -.head.e) |
7925+ =(names.head.e ~[name])
7926+::
7927+++ branch-base-arm
7928+ |= [e=expr name=term]
7929+ ^- (unit expr)
7930+ ?: ?=(%group -.e) $(e inner.e)
7931+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
7932+ ?. ?=(%branch -.e) ~
7933+ ?~ arms.e ~
7934+ ?~ t.arms.e ~
7935+ ?^ t.t.arms.e ~
7936+ =/ x=arm i.arms.e
7937+ =/ y=arm i.t.arms.e
7938+ ?. &(?=(%lit -.pat.x) ?=(%lit -.pat.y)) ~
7939+ ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y)) ~
7940+ ?: =(val.lit.pat.x val.lit.pat.y) ~
7941+ =/ first=? (direct-self-call val.x name)
7942+ =/ second=? (direct-self-call val.y name)
7943+ ?: =(first second) ~
7944+ `?:(first val.y val.x)
7945+::
7946+:: Infer the base arm independently, with the self binding removed. Only
7947+:: a closed type whose constraints resolved can seed the recursive result.
7948+:: The regular body inference then checks both arms with shared state.
7949+::
7950+++ recursive-branch-seed
7951+ |= [d=def env=ienv state=istate]
7952+ ^- (unit itype)
7953+ ?. ?=(%value -.d) ~
7954+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) ~
7955+ =/ gate=expr val.d
7956+ =/ body=expr
7957+ ?- -.gate
7958+ %gate body.gate
7959+ %gate-wide body.gate
7960+ * !!
7961+ ==
7962+ =/ base=(unit expr) (branch-base-arm body name.d)
7963+ ?~ base ~
7964+ =/ outer=ienv (skim env |=(entry=[name=term scheme=ischeme] !=(name.entry name.d)))
7965+ =/ sam=isample-result
7966+ ?- -.gate
7967+ %gate (infer-sample sample.gate outer state)
7968+ %gate-wide (infer-sample sample.gate outer state)
7969+ * !!
7970+ ==
7971+ ?: ?=(%| -.sam) ~
7972+ =/ inferred=iresult (infer-fragment u.base env.p.sam state.p.sam)
7973+ ?: ?=(%| -.inferred) ~
7974+ ?: (pending-tags tags.state.p.inferred sub.state.p.inferred) ~
7975+ ?: (constrained-capitals caps.state.p.inferred sub.state.p.inferred) ~
7976+ =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7977+ ?: ?=(^ (itype-vars typ)) ~
7978+ ?: (itype-has-tag typ) ~
7979+ `typ
7980+::
7981+++ infer-recursive-gate
7982+ |= [d=def env=ienv state=istate]
7983+ ^- iresult
7984+ ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
7985+ ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
7986+ [%| ["recursive definition is not a gate" ~]]
7987+ =/ result=(unit itype) (recursive-branch-seed d env state)
7988+ =/ gate=expr val.d
7989+ =/ sam=isample-result
7990+ ?- -.gate
7991+ %gate (infer-sample sample.gate env state)
7992+ %gate-wide (infer-sample sample.gate env state)
7993+ * !!
7994+ ==
7995+ ?: ?=(%| -.sam)
7996+ =/ diag=(unit idiag)
7997+ ?- -.gate
7998+ %gate (sample-import-invalid sample.gate env state)
7999+ %gate-wide (sample-import-invalid sample.gate env state)
8000+ * ~
8001+ ==
8002+ ?: &(=(p.sam "sample mold is not supported by partial inference") ?=(^ diag)) [%| u.diag]
8003+ [%| [p.sam ~]]
8004+ =/ id=@ud next.state.p.sam
8005+ =/ product=itype ?~(result [%var id] u.result)
8006+ =/ st=istate state.p.sam(next +(id))
8007+ =/ seed=itype [%fn typ.p.sam product]
8008+ =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
8009+ =/ body=expr
8010+ ?- -.gate
8011+ %gate body.gate
8012+ %gate-wide body.gate
8013+ * !!
8014+ ==
8015+ =/ out=iresult (infer-fragment body seeded st)
8016+ ?: ?=(%| -.out) out
8017+ =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
8018+ ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
8019+ [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
8020+::
8021+++ dependency-root
8022+ |= names=(list term)
8023+ ^- (list term)
8024+ ?~ names ~
8025+ ~[(rear names)]
8026+::
8027+++ dependency-exprs
8028+ |= xs=(list expr)
8029+ ^- (list term)
8030+ ?~ xs ~
8031+ =/ first=(list term) (dependency-expr i.xs)
8032+ (weld first $(xs t.xs))
8033+::
8034+++ dependency-pieces
8035+ |= xs=(list piece)
8036+ ^- (list term)
8037+ ?~ xs ~
8038+ =/ first=(list term)
8039+ ?- -.i.xs
8040+ %expr (dependency-expr p.i.xs)
8041+ %text ~
8042+ ==
8043+ (weld first $(xs t.xs))
8044+::
8045+++ dependency-qsegs
8046+ |= xs=(list qseg)
8047+ ^- (list term)
8048+ ?~ xs ~
8049+ =/ first=(list term)
8050+ ?- -.i.xs
8051+ %expr (dependency-expr p.i.xs)
8052+ %knot ~
8053+ ==
8054+ (weld first $(xs t.xs))
8055+::
8056+++ dependency-items
8057+ |= xs=(list item)
8058+ ^- (list term)
8059+ ?~ xs ~
8060+ =/ first=(list term) (dependency-expr val.i.xs)
8061+ (weld first $(xs t.xs))
8062+::
8063+++ dependency-edits
8064+ |= xs=(list edit)
8065+ ^- (list term)
8066+ ?~ xs ~
8067+ =/ first=(list term) (dependency-expr val.i.xs)
8068+ (weld first $(xs t.xs))
8069+::
8070+++ dependency-arms
8071+ |= xs=(list arm)
8072+ ^- (list term)
8073+ ?~ xs ~
8074+ =/ first=(list term) (dependency-expr val.i.xs)
8075+ (weld first $(xs t.xs))
8076+::
8077+++ dependency-defs
8078+ |= xs=(list def)
8079+ ^- (list term)
8080+ ?~ xs ~
8081+ =/ first=(list term)
8082+ ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
8083+ ~
8084+ (weld first $(xs t.xs))
8085+::
8086+++ dependency-expr
8087+ |= e=expr
8088+ ^- (list term)
8089+ ?- -.e
8090+ %str (dependency-pieces pieces.e)
8091+ %qath (dependency-qsegs segs.e)
8092+ %wing (dependency-root names.e)
8093+ %change
8094+ =/ first=(list term) (dependency-root target.e)
8095+ =/ last=(list term) (dependency-edits edits.e)
8096+ (weld first last)
8097+ %pair (dependency-expr val.e)
8098+ %unit (dependency-expr val.e)
8099+ %group (dependency-expr inner.e)
8100+ %list (dependency-exprs items.e)
8101+ %tuple (dependency-items items.e)
8102+ %gate (dependency-expr body.e)
8103+ %gate-wide (dependency-expr body.e)
8104+ %call
8105+ =/ first=(list term) (dependency-expr head.e)
8106+ =/ last=(list term) (dependency-exprs args.e)
8107+ (weld first last)
8108+ %cast (dependency-expr val.e)
8109+ %trace
8110+ =/ first=(list term) (dependency-expr val.e)
8111+ =/ last=(list term) (dependency-expr then.e)
8112+ (weld first last)
8113+ %branch
8114+ =/ first=(list term) (dependency-expr subject.e)
8115+ =/ last=(list term) (dependency-arms arms.e)
8116+ (weld first last)
8117+ %body
8118+ =/ first=(list term) (dependency-defs defs.e)
8119+ =/ last=(list term) (dependency-expr final.e)
8120+ (weld first last)
8121+ * ~
8122+ ==
8123+::
8124+:: Infer a cyclic component with one monomorphic seed per gate. All members
8125+:: must succeed before any scheme is available; pending constraints and
8126+:: unresolved branch joins remain partial.
8127++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
8128++$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
8129+++ seed-gate-group
8130+ |= [ds=(list def) env=ienv state=istate]
8131+ ^- igate-seeds
8132+ ?~ ds [%& [~ state]]
8133+ =/ d=def i.ds
8134+ ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
8135+ =/ gate=expr val.d
8136+ ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
8137+ [%| ["recursive group contains a non-gate" ~]]
8138+ =/ initial=istate (reserve-def-caps gate state)
8139+ =/ sam=isample-result
8140+ ?- -.gate
8141+ %gate (infer-sample sample.gate env initial)
8142+ %gate-wide (infer-sample sample.gate env initial)
8143+ * !!
8144+ ==
8145+ ?: ?=(%| -.sam) [%| [p.sam ~]]
8146+ =/ body=expr
8147+ ?- -.gate
8148+ %gate body.gate
8149+ %gate-wide body.gate
8150+ * !!
8151+ ==
8152+ =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
8153+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
8154+ =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
8155+ =/ rest=igate-seeds $(ds t.ds, state after)
8156+ ?: ?=(%| -.rest) rest
8157+ [%& [[entry entries.p.rest] state.p.rest]]
8158+::
8159+++ group-seed-env
8160+ |= [entries=(list igate-entry) env=ienv]
8161+ ^- ienv
8162+ ?~ entries env
8163+ [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
8164+::
8165+++ infer-gate-group-bodies
8166+ |= [entries=(list igate-entry) seeds=ienv state=istate]
8167+ ^- igate-seeds
8168+ ?~ entries [%& [~ state]]
8169+ =/ entry=igate-entry i.entries
8170+ ?> ?=(%fn -.typ.entry)
8171+ =/ scope=ienv (weld seeds env.entry)
8172+ =/ out=iresult (infer-fragment body.entry scope state(caps caps.entry))
8173+ ?: ?=(%| -.out) out
8174+ =/ uni=(unit isub) (itype-unify product.typ.entry typ.p.out sub.state.p.out)
8175+ ?~ uni [%| ["recursive group constraint is not supported by partial inference" ~]]
8176+ =. caps.entry caps.state.p.out
8177+ =/ after=istate state.p.out(sub u.uni, caps caps.state)
8178+ =/ rest=igate-seeds $(entries t.entries, state after)
8179+ ?: ?=(%| -.rest) rest
8180+ [%& [[entry entries.p.rest] state.p.rest]]
8181+::
8182+++ group-schemes
8183+ |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
8184+ ^- (each ienv idiag)
8185+ ?~ entries [%& ~]
8186+ =/ entry=igate-entry i.entries
8187+ =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
8188+ ?^ merged
8189+ [%| ["distinct type variables must not be forced equal" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
8190+ ?: (constrained-capitals caps.entry sub.state)
8191+ [%| ["explicit capital constraints are not supported by partial inference" ~]]
8192+ =/ typ=itype (itype-normalize typ.entry sub.state)
8193+ ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
8194+ [%| ["recursive group needs unsupported inference" ~]]
8195+ =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
8196+ =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8197+ =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
8198+ ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
8199+ =/ rest=(each ienv idiag) $(entries t.entries)
8200+ ?: ?=(%| -.rest) rest
8201+ [%& [[name.entry [typ vars]] p.rest]]
8202+::
8203+++ infer-gate-group
8204+ |= [ds=(list def) env=ienv state=istate]
8205+ ^- ilocal-result
8206+ =/ names=(list term) (global-value-names ds)
8207+ ?. (levy names |=(n=term (unique-value-name n names)))
8208+ [%| ["recursive group contains duplicate names" ~]]
8209+ ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
8210+ [%| ["recursive group shadows a name" ~]]
8211+ =/ scoped=istate state(globals (weld names globals.state))
8212+ =/ seeded=igate-seeds (seed-gate-group ds env scoped)
8213+ ?: ?=(%| -.seeded) seeded
8214+ =/ seeds=ienv (group-seed-env entries.p.seeded ~)
8215+ =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
8216+ ?: ?=(%| -.body) body
8217+ ?: (pending-tags tags.state.p.body sub.state.p.body)
8218+ [%| ["recursive group has unresolved literal constraints" ~]]
8219+ =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
8220+ ?: ?=(%| -.schemes) schemes
8221+ [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
8222+::
67798223++ add-supported-defs
67808224 |= [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)]
67818225 ^- ienv
@@ -6785,7 +8229,10 @@
67858229 ?. (unique-value-name name.d globals) $(ds t.ds)
67868230 ?^ (ienv-lookup name.d env) $(ds t.ds)
67878231 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
6788− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude])
8232+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8233+ =. initial (reserve-def-caps val.d initial)
8234+ =/ result=iresult (infer-fragment val.d env initial)
8235+ =? result ?=(%| -.result) (infer-recursive-gate d env initial)
67898236 ?: ?=(%| -.result) $(ds t.ds)
67908237 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
67918238 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
@@ -6795,14 +8242,254 @@
67958242 ?: (gth (lent vars) 26) $(ds t.ds)
67968243 $(ds t.ds, env [[name.d [typ vars]] env])
67978244::
6798−++ resolve-supported-defs
8245++$ iresolved [env=ienv grouped=(list term)]
8246++$ iadj (map term (list term))
8247++$ ivisited (map term ?)
8248++$ iwork (list [name=term done=?])
8249++$ iwresult [seen=ivisited order=(list term)]
8250++$ icresult [seen=ivisited component=(list term)]
8251++$ icomponents (list (list term))
8252+++ graph-nameset
8253+ |= [names=(list term) seen=ivisited]
8254+ ^- ivisited
8255+ ?~ names seen
8256+ $(names t.names, seen (~(put by seen) i.names &))
8257+::
8258+++ graph-edges
8259+ |= [name=term graph=iadj]
8260+ ^- (list term)
8261+ =/ found=(unit (list term)) (~(get by graph) name)
8262+ ?~ found ~
8263+ u.found
8264+::
8265+++ graph-make-forward
8266+ |= [ds=(list def) names=ivisited graph=iadj]
8267+ ^- iadj
8268+ ?~ ds graph
8269+ ?. ?=(%value -.i.ds) $(ds t.ds)
8270+ =/ deps=(list term) (dependency-expr val.i.ds)
8271+ =. deps (skim deps |=(n=term ?=(^ (~(get by names) n))))
8272+ $(ds t.ds, graph (~(put by graph) name.i.ds deps))
8273+::
8274+++ graph-add-reverse
8275+ |= [name=term edges=(list term) reverse=iadj]
8276+ ^- iadj
8277+ ?~ edges reverse
8278+ =/ prior=(list term) (graph-edges i.edges reverse)
8279+ $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
8280+::
8281+++ graph-reverse
8282+ |= [names=(list term) graph=iadj reverse=iadj]
8283+ ^- iadj
8284+ ?~ names reverse
8285+ =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
8286+ $(names t.names)
8287+::
8288+++ graph-order
8289+ |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
8290+ ^- iwresult
8291+ ?~ todo [seen order]
8292+ =/ event=[name=term done=?] i.todo
8293+ ?: done.event $(todo t.todo, order [name.event order])
8294+ ?: ?=(^ (~(get by seen) name.event)) $(todo t.todo)
8295+ =. seen (~(put by seen) name.event &)
8296+ =/ children=iwork (turn (graph-edges name.event graph) |=(n=term [n |]))
8297+ $(todo (weld children [[name.event &] t.todo]))
8298+::
8299+++ graph-collect
8300+ |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
8301+ ^- icresult
8302+ ?~ todo [seen component]
8303+ ?: ?=(^ (~(get by seen) i.todo)) $(todo t.todo)
8304+ =. seen (~(put by seen) i.todo &)
8305+ $(todo (weld (graph-edges i.todo graph) t.todo), component [i.todo component])
8306+::
8307+++ graph-collect-all
8308+ |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
8309+ ^- icomponents
8310+ ?~ order comps
8311+ ?: ?=(^ (~(get by seen) i.order)) $(order t.order)
8312+ =/ found=icresult (graph-collect ~[i.order] seen ~ graph)
8313+ $(order t.order, seen seen.found, comps [component.found comps])
8314+::
8315+:: Two depth-first passes find components before group inference. Maps
8316+:: preserve the graph identity; duplicate global names fail closed.
8317+++ graph-components
8318+ |= [ds=(list def) names=(list term)]
8319+ ^- icomponents
8320+ =/ nameset=ivisited ~
8321+ =/ pending=(list term) names
8322+ |-
8323+ ?^ pending
8324+ ?: ?=(^ (~(get by nameset) i.pending)) ~
8325+ $(pending t.pending, nameset (~(put by nameset) i.pending &))
8326+ =/ graph=iadj (graph-make-forward ds nameset ~)
8327+ =/ reverse=iadj (graph-reverse names graph ~)
8328+ =/ order=iwresult (graph-order (turn names |=(n=term [n |])) ~ ~ graph)
8329+ (graph-collect-all order.order ~ reverse ~)
8330+::
8331+++ graph-cycle
8332+ |= [component=(list term) graph=iadj]
8333+ ^- ?
8334+ ?~ component |
8335+ ?^ t.component &
8336+ (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
8337+::
8338+++ add-groups
8339+ |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) state=istate]
8340+ ^- iresolved
8341+ ?~ components [env grouped]
8342+ =/ component=(list term) i.components
8343+ ?. (graph-cycle component graph) $(components t.components)
8344+ ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
8345+ =/ members=(list def)
8346+ %+ skim ds
8347+ |= d=def
8348+ &(?=(%value -.d) (lien component |=(n=term =(n name.d))))
8349+ ?. =((lent members) (lent component)) $(components t.components)
8350+ ?. (levy component |=(n=term (unique-value-name n globals.state))) $(components t.components)
8351+ =/ result=ilocal-result (infer-gate-group members env state)
8352+ ?: ?=(%| -.result) $(components t.components)
8353+ $(components t.components, env env.p.result, grouped (weld component grouped))
8354+::
8355+++ resolve-groups
67998356 |= [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)]
6800− ^- ienv
8357+ ^- iresolved
68018358 =/ env=ienv ~
8359+ =/ grouped=(list term) ~
8360+ =/ names=(list term) (global-value-names ds)
8361+ =/ nameset=ivisited (graph-nameset names ~)
8362+ =/ graph=iadj (graph-make-forward ds nameset ~)
8363+ =/ components=icomponents (graph-components ds names)
8364+ =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
68028365 |-
68038366 =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
6804− ?: =(next env) env
6805− $(env next)
8367+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
8368+ =/ out=iresolved (add-groups ds components graph next grouped initial)
8369+ ?: =(env env.out) out
8370+ $(env env.out, grouped grouped.out)
8371+::
8372+++ resolve-supported-defs
8373+ |= [ds=(list def) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile)]
8374+ ^- ienv
8375+ env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
8376+::
8377+:: A diagnostic-only proof for a narrow syntactic value cycle. Every
8378+:: edge is an unqualified wing in a supported expression, and samples
8379+:: may not shadow global bindings. Unknown forms yield no conclusion.
8380++$ icyclesite [name=term at=span]
8381++$ icycle [name=term first=span next=span]
8382+++ cycle-sites-list
8383+ |= [xs=(list expr) globals=(list term) locals=(list term)]
8384+ ^- (unit (list icyclesite))
8385+ ?~ xs `~
8386+ =/ first=(unit (list icyclesite)) (cycle-sites i.xs globals locals)
8387+ ?~ first ~
8388+ =/ tail=(unit (list icyclesite)) $(xs t.xs)
8389+ ?~ tail ~
8390+ `(weld u.first u.tail)
8391+::
8392+++ cycle-sample-name
8393+ |= [sam=sample globals=(list term) locals=(list term)]
8394+ ^- (unit (unit term))
8395+ ?- -.sam
8396+ %bind
8397+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
8398+ ``name.sam
8399+ %face
8400+ ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
8401+ ``name.sam
8402+ %bare `~
8403+ * ~
8404+ ==
8405+::
8406+++ cycle-sites
8407+ |= [e=expr globals=(list term) locals=(list term)]
8408+ ^- (unit (list icyclesite))
8409+ ?- -.e
8410+ %wing
8411+ ?. ?=([@ ~] names.e) ~
8412+ `~[[i.names.e at.e]]
8413+ %lit `~
8414+ %str
8415+ ?: (lien pieces.e |=(p=piece ?=(%expr -.p))) ~
8416+ `~
8417+ %group $(e inner.e)
8418+ %body ?~(defs.e $(e final.e) ~)
8419+ %cast $(e val.e)
8420+ %gate
8421+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
8422+ ?~ binder ~
8423+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
8424+ $(e body.e, locals nested)
8425+ %gate-wide
8426+ =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
8427+ ?~ binder ~
8428+ =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
8429+ $(e body.e, locals nested)
8430+ %call
8431+ =/ first=(unit (list icyclesite)) $(e head.e)
8432+ ?~ first ~
8433+ =/ tail=(unit (list icyclesite)) (cycle-sites-list args.e globals locals)
8434+ ?~ tail ~
8435+ `(weld u.first u.tail)
8436+ * ~
8437+ ==
8438+::
8439+++ cycle-definitely-atom
8440+ |= e=expr
8441+ ^- ?
8442+ ?: ?=(%group -.e) $(e inner.e)
8443+ ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8444+ ?. ?=(%cast -.e) |
8445+ |(?=(%aura -.shape.e) ?=(%flag -.shape.e))
8446+::
8447+++ cycle-proof-group
8448+ |= [members=(list def) globals=(list term)]
8449+ ^- ?
8450+ ?~ members &
8451+ ?. ?=(%value -.i.members) |
8452+ ?. (unique-value-name name.i.members globals) |
8453+ ?. ?=(^ (cycle-sites val.i.members globals ~)) |
8454+ $(members t.members)
8455+::
8456+++ cycle-find-site
8457+ |= [sites=(list icyclesite) component=(list term)]
8458+ ^- (unit span)
8459+ ?~ sites ~
8460+ ?: (lien component |=(n=term =(n name.i.sites))) `at.i.sites
8461+ $(sites t.sites)
8462+::
8463+++ cycle-group-errors
8464+ |= [members=(list def) component=(list term) globals=(list term)]
8465+ ^- (list icycle)
8466+ ?~ members ~
8467+ =/ d=def i.members
8468+ ?> ?=(%value -.d)
8469+ =/ tail=(list icycle) $(members t.members)
8470+ ?. (cycle-definitely-atom val.d) tail
8471+ =/ sites=(unit (list icyclesite)) (cycle-sites val.d globals ~)
8472+ ?~ sites tail
8473+ =/ found=(unit span) (cycle-find-site u.sites component)
8474+ ?~ found tail
8475+ [[name.d at.d u.found] tail]
8476+::
8477+++ definite-value-cycles
8478+ |= [ds=(list def) globals=(list term)]
8479+ ^- (list icycle)
8480+ =/ names=(list term) (global-value-names ds)
8481+ =/ graph=iadj (graph-make-forward ds (graph-nameset names ~) ~)
8482+ =/ components=icomponents (graph-components ds names)
8483+ =/ out=(list icycle) ~
8484+ |-
8485+ ?~ components out
8486+ =/ component=(list term) i.components
8487+ ?. (graph-cycle component graph) $(components t.components)
8488+ =/ members=(list def)
8489+ (skim ds |=(d=def &(?=(%value -.d) (lien component |=(n=term =(n name.d))))))
8490+ ?. =((lent members) (lent component)) $(components t.components)
8491+ ?. (cycle-proof-group members globals) $(components t.components)
8492+ $(components t.components, out (weld (cycle-group-errors members component globals) out))
68068493::
68078494+| %union-analysis
68088495::
@@ -7025,6 +8712,22 @@
70258712 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
70268713 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
70278714::
8715+:: In an API file or before main's kind is known, a lone `+$ poke`
8716+:: may be a declaration rather than a mold that shadows the prelude. Do not call
8717+:: that one collision definite, and do not hide unrelated scope errors.
8718+++ pending-declared-poke
8719+ |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
8720+ ^- ?
8721+ ?. (lien prelude-molds |=(n=term =(%poke n))) |
8722+ ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
8723+ =/ pokes=(list def)
8724+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
8725+ ?~ pokes |
8726+ ?^ t.pokes |
8727+ =/ remaining=(list def)
8728+ (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
8729+ (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
8730+::
70288731++ module-mold-types
70298732 |= [molds=imolds state=istate]
70308733 ^- (each imold-types @t)
@@ -7040,9 +8743,9 @@
70408743::
70418744:: Prepare a provisional interface from the trusted vendored source.
70428745:: Every declared name remains reserved, but only molds and values this
7043−:: fragment can infer are usable. Unsupported bodies are not validated,
7044−:: and imports into the prelude are not supported yet. The fixed origin
7045−:: gives its named unions the same identity in every importing module.
8746+:: fragment can infer are usable. Unsupported bodies are not validated.
8747+:: An optional internal source supplies the prelude's one supported import;
8748+:: clients cannot import that path directly. Named unions retain their origin.
70468749::
70478750:: Recognize only the complete standard prelude list shape. Its recursive
70488751:: tail uses the same parameter and the unqualified list name. The reader
@@ -7082,6 +8785,13 @@
70828785 ?. ?=(%tvar -.i.args.tail) |
70838786 =(var name.i.args.tail)
70848787::
8788+++ prelude-label
8789+ |= [typ=itype name=term]
8790+ ^- itype
8791+ ?. ?=(%union -.typ) typ
8792+ ?^ args.typ typ
8793+ typ(label `name)
8794+::
70858795++ partial-prelude-molds
70868796 |= [molds=imolds state=istate]
70878797 ^- imold-types
@@ -7094,26 +8804,59 @@
70948804 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
70958805 ?~ out $(molds t.molds)
70968806 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
8807+ =. typ.template.u.out (prelude-label typ.template.u.out name.m)
70978808 [[name.m template.u.out] $(molds t.molds)]
70988809::
7099−++ partial-prelude-interface
7100− |= src=@t
8810+++ partial-prelude-interface-with-internal
8811+ |= [src=@t internal-source=(unit @t)]
71018812 ^- (unit ifile)
71028813 ?: =(0 src) ~
71038814 =/ at=path /lib/jibb/prelude/jibb
71048815 =/ parsed (parse at src)
71058816 ?: ?=(%| -.parsed) ~
7106− ?^ imports.p.parsed ~
8817+ =/ private=(unit ijimports)
8818+ ?~ imports.p.parsed `~
8819+ ?. ?=([[%jibb *] ~] imports.p.parsed) ~
8820+ ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
8821+ ?~ internal-source ~
8822+ =/ built=jfile-result
8823+ (infer-jibb-file /lib/jibb/internal/jibb u.internal-source ~ ~ ~ ~[/lib/jibb/internal/jibb] ~ ~ ~ ~)
8824+ ?: ?=(%| -.built) ~
8825+ `~[[face.i.imports.p.parsed iface.p.built]]
8826+ ?~ private ~
71078827 ?~ defs.p.parsed ~
71088828 ?. (module-scope-valid p.parsed ~ ~) ~
71098829 =/ ds=(list def) defs.p.parsed
71108830 =/ molds=imolds (collect-simple-molds ds)
71118831 =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7112− =/ globals=(list term) (global-value-names ds)
7113− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ ~ ~ ~ ~ ~ | at names ~]
8832+ =/ globals=(list term) (weld (import-binding-names imports.p.parsed) (global-value-names ds))
8833+ :: Remove raw list before inferring any template, so an altered list
8834+ :: cannot leak through an alias. Its name remains reserved either way.
8835+ =/ declared=? (lien names |=(name=term =(%list name)))
8836+ =/ env-molds=imolds molds
8837+ =? env-molds declared
8838+ (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
8839+ =/ reserved=(list term) ?:(declared ~[%list] ~)
8840+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~]
71148841 =/ mt=imold-types (partial-prelude-molds molds state)
7115− =/ env=ienv (resolve-supported-defs ds molds globals ~ ~ ~ ~ ~ ~ at ~)
7116− `[env mt at]
8842+ =/ partial=ifile [~ mt at ~]
8843+ :: An explicitly qualified re-export must resolve. Other unsupported
8844+ :: prelude declarations remain reserved but absent from the interface.
8845+ =/ required=imolds
8846+ %+ skim molds
8847+ |= m=[name=term body=shape]
8848+ =/ sh=shape body.m
8849+ ?. ?=(%ref -.sh) |
8850+ ?~ names.sh |
8851+ ?=(^ t.names.sh)
8852+ ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
8853+ =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
8854+ `[env mt at ~]
8855+::
8856+++ partial-prelude-interface
8857+ |= src=@t
8858+ ^- (unit ifile)
8859+ (partial-prelude-interface-with-internal src ~)
71178860::
71188861+$ iprelude [iface=ifile values=(list term) molds=(list term)]
71198862::
@@ -7128,6 +8871,17 @@
71288871 =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
71298872 `[u.iface vals ms]
71308873::
8874+++ prepare-prelude-with-internal
8875+ |= [src=@t internal-source=@t]
8876+ ^- (unit iprelude)
8877+ =/ iface=(unit ifile) (partial-prelude-interface-with-internal src `internal-source)
8878+ ?~ iface ~
8879+ =/ parsed (parse /lib/jibb/prelude/jibb src)
8880+ ?: ?=(%| -.parsed) ~
8881+ =/ vals=(list term) (global-value-names defs.p.parsed)
8882+ =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
8883+ `[u.iface vals ms]
8884+::
71318885++ module-values-complete
71328886 |= [ds=(list def) env=ienv]
71338887 ^- ?
@@ -7154,6 +8908,8 @@
71548908 ?~ imports [%& [~ cache]]
71558909 ?. ?=(%jibb -.i.imports) $(imports t.imports)
71568910 =/ at=path (weld path.i.imports `path`~[%jibb])
8911+ ?: =(at /lib/jibb/internal/jibb)
8912+ [%| 'the prelude internal module is private']
71578913 ?: (lien active |=(p=path =(p at)))
71588914 [%| (crip "import cycle at {(spud at)}")]
71598915 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -7168,14 +8924,277 @@
71688924 ?: ?=(%| -.rest) rest
71698925 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
71708926::
8927+:: Provisional declaration extraction only; this does not derive asks,
8928+:: validate imported types, or claim that an API module has checked.
8929++$ iapi-path [at=span name=term segments=(list pseg) full=term diffs=(list term) scry=(unit (list pseg))]
8930+++ api-path-mark
8931+ |= [sh=shape marks=(list term)]
8932+ ^- (unit term)
8933+ ?. ?=(%ref -.sh) ~
8934+ ?. ?=([@ ~] names.sh) ~
8935+ ?. (unique-value-name i.names.sh marks) ~
8936+ `i.names.sh
8937+::
8938+++ api-path-diffs
8939+ |= [shapes=(list shape) marks=(list term) used=(list term)]
8940+ ^- (unit (list term))
8941+ ?~ shapes `~
8942+ =/ n=(unit term) (api-path-mark i.shapes marks)
8943+ ?~ n ~
8944+ ?: (lien used |=(x=term =(x u.n))) ~
8945+ =/ rest=(unit (list term)) $(shapes t.shapes, used [u.n used])
8946+ ?~ rest ~
8947+ `[u.n u.rest]
8948+::
8949+++ api-path-payload
8950+ |= [sh=shape marks=(list term)]
8951+ ^- (unit [full=term diffs=(list term)])
8952+ =/ direct=(unit term) (api-path-mark sh marks)
8953+ ?^ direct `[u.direct ~]
8954+ ?. ?=(%apply -.sh) ~
8955+ ?. =(~[%facts] ref.sh) ~
8956+ ?~ args.sh ~
8957+ ?~ t.args.sh ~
8958+ =/ full=(unit term) (api-path-mark i.args.sh marks)
8959+ ?~ full ~
8960+ =/ diffs=(unit (list term)) (api-path-diffs t.args.sh marks ~[u.full])
8961+ ?~ diffs ~
8962+ `[u.full u.diffs]
8963+::
8964++$ iapi-parameter [name=term aura=@ta at=span]
8965+++ api-path-parameters
8966+ |= [segments=(list pseg) seen=(list term)]
8967+ ^- (unit (list iapi-parameter))
8968+ ?~ segments `~
8969+ ?: ?=(%knot -.i.segments) $(segments t.segments)
8970+ =/ seg=pseg i.segments
8971+ ?> ?=(%typed -.seg)
8972+ ?: =(0 aura.seg) ~
8973+ ?: (lien seen |=(n=term =(n name.seg))) ~
8974+ =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
8975+ ?~ rest ~
8976+ `[[name.seg aura.seg at.seg] u.rest]
8977+::
8978+++ api-scry-parameters-compatible
8979+ |= [scry=(list iapi-parameter) watch=(list iapi-parameter)]
8980+ ^- ?
8981+ ?~ scry &
8982+ ?. (lien watch |=(p=iapi-parameter &(=(name.p name.i.scry) =(aura.p aura.i.scry)))) |
8983+ $(scry t.scry)
8984+::
8985+++ api-path-one
8986+ |= [sh=shape marks=(list term)]
8987+ ^- (unit iapi-path)
8988+ ?. ?=(%cell -.sh) ~
8989+ =/ fs=(list field) fields.sh
8990+ ?~ fs ~
8991+ ?~ t.fs ~
8992+ ?~ t.t.fs ~
8993+ ?: (gth (lent fs) 4) ~
8994+ ?. ?=(%bare -.i.fs) ~
8995+ =/ tag=shape shape.i.fs
8996+ ?. ?=(%const -.tag) ~
8997+ ?. =(%term form.lit.tag) ~
8998+ =/ name=term val.lit.tag
8999+ ?. (jibb-face-name name) ~
9000+ ?. ?=(%bare -.i.t.fs) ~
9001+ =/ path-shape=shape shape.i.t.fs
9002+ ?. ?=(%path -.path-shape) ~
9003+ ?. ?=(%bare -.i.t.t.fs) ~
9004+ =/ payload=(unit [full=term diffs=(list term)]) (api-path-payload shape.i.t.t.fs marks)
9005+ ?~ payload ~
9006+ =/ scry=(unit (unit (list pseg)))
9007+ ?~ t.t.t.fs `~
9008+ =/ entry=field i.t.t.t.fs
9009+ ?. ?=(%face -.entry) ~
9010+ ?. =(%scry name.entry) ~
9011+ ?. ?=(%path -.shape.entry) ~
9012+ ``segs.shape.entry
9013+ ?~ scry ~
9014+ =/ params=(unit (list iapi-parameter)) (api-path-parameters segs.path-shape ~)
9015+ ?~ params ~
9016+ ?^ u.scry
9017+ =/ scry-params=(unit (list iapi-parameter)) (api-path-parameters u.u.scry ~)
9018+ ?~ scry-params ~
9019+ ?. (api-scry-parameters-compatible u.scry-params u.params) ~
9020+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
9021+ `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
9022+::
9023+++ api-path-many
9024+ |= [shapes=(list shape) marks=(list term) seen=(list term)]
9025+ ^- (unit (list iapi-path))
9026+ ?~ shapes `~
9027+ =/ one=(unit iapi-path) (api-path-one i.shapes marks)
9028+ ?~ one ~
9029+ ?: (lien seen |=(n=term =(n name.u.one))) ~
9030+ =/ rest=(unit (list iapi-path)) $(shapes t.shapes, seen [name.u.one seen])
9031+ ?~ rest ~
9032+ `[u.one u.rest]
9033+::
9034+++ api-path-declaration
9035+ |= [sh=shape marks=(list term)]
9036+ ^- (unit (list iapi-path))
9037+ ?: ?=(%union -.sh) (api-path-many cases.sh marks ~)
9038+ (api-path-many ~[sh] marks ~)
9039+::
9040+:: Derived gates share the value namespace. /% marks name molds; /- and
9041+:: /= also introduce faces that cannot be shadowed by a derived value.
9042+++ api-import-faces
9043+ |= imports=(list import)
9044+ ^- (list term)
9045+ ?~ imports ~
9046+ ?- -.i.imports
9047+ %mark $(imports t.imports)
9048+ %sur [name.i.imports $(imports t.imports)]
9049+ %jibb [face.i.imports $(imports t.imports)]
9050+ ==
9051+::
9052+++ api-derived-names-valid
9053+ |= [paths=(list iapi-path) poke-names=(list term) mod=module prelude-values=(list term)]
9054+ ^- ?
9055+ =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
9056+ =/ derived=(list term) (weld path-names poke-names)
9057+ =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
9058+ (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
9059+::
9060+:: Analysis only. Successful external entries must be unchanged results
9061+:: produced for the declared marks; no request interface is produced.
9062++$ iapi-mark-type [name=term typ=itype]
9063++$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
9064+++ api-diff-types
9065+ |= [names=(list term) externals=imark-externals declared=(list term)]
9066+ ^- (unit (list iapi-mark-type))
9067+ ?~ names `~
9068+ =/ typ=(unit itype) (find-imported-mark i.names externals declared)
9069+ ?~ typ ~
9070+ =/ tail=(unit (list iapi-mark-type)) $(names t.names)
9071+ ?~ tail ~
9072+ `[[i.names u.typ] u.tail]
9073+::
9074+++ api-path-types
9075+ |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
9076+ ^- (unit (list iapi-path-typed))
9077+ ?~ paths `~
9078+ =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
9079+ ?~ full ~
9080+ =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
9081+ ?~ diffs ~
9082+ =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
9083+ ?~ tail ~
9084+ `[[i.paths u.full u.diffs] u.tail]
9085+::
9086+++ api-poke-mark-names
9087+ |= [pokes=(list def) declared=(list term)]
9088+ ^- (unit (list term))
9089+ ?~ pokes `~
9090+ ?^ t.pokes ~
9091+ =/ d=def i.pokes
9092+ ?. ?=(%mold -.d) ~
9093+ =/ sh=shape shape.d
9094+ ?: ?=(%union -.sh) (api-path-diffs cases.sh declared ~)
9095+ =/ name=(unit term) (api-path-mark sh declared)
9096+ ?~ name ~
9097+ `~[u.name]
9098+::
9099+++ api-path-analysis
9100+ |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
9101+ ^- (unit (list iapi-path-typed))
9102+ =/ ds=(list def) defs.mod
9103+ =/ declarations=(list def)
9104+ (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
9105+ ?. ?=([* ~] declarations) ~
9106+ =/ pokes=(list def)
9107+ (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
9108+ ?: (gth (lent pokes) 1) ~
9109+ =/ ordinary=(list def)
9110+ (skim ds |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
9111+ ?. (module-scope-valid mod(defs ordinary) prelude-values prelude-molds) ~
9112+ =/ declared=(list term) (collect-mark-imports imports.mod)
9113+ =/ poke-names=(unit (list term)) (api-poke-mark-names pokes declared)
9114+ ?~ poke-names ~
9115+ =/ decl=def i.declarations
9116+ ?> ?=(%mold -.decl)
9117+ =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
9118+ ?~ paths ~
9119+ ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
9120+ (api-path-types u.paths externals declared)
9121+::
9122+:: Source/graph entry for path analysis only. The returned paths retain
9123+:: reader-derived mark types and import resolution has checked reachable
9124+:: Jibb dependencies. This is not an API interface or a module check.
9125+++ api-path-analysis-source
9126+ |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
9127+ ^- (each (list iapi-path-typed) @t)
9128+ ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
9129+ ?~ prepared [%| 'API path analysis needs the prepared prelude']
9130+ =/ parsed (parse file src)
9131+ ?: ?=(%| -.parsed) [%| 'API path source does not parse']
9132+ =/ prelude=(unit ifile) `iface.u.prepared
9133+ =/ deps=jimports-result
9134+ (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
9135+ ?: ?=(%| -.deps) [%| p.deps]
9136+ =/ paths=(unit (list iapi-path-typed))
9137+ (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
9138+ ?~ paths [%| 'API path declaration needs unsupported analysis']
9139+ [%& u.paths]
9140+::
9141+++ api-mark-exports
9142+ |= [marks=(list term) all=(list term) externals=imark-externals]
9143+ ^- imold-types
9144+ ?~ marks ~
9145+ =/ t=(unit itype) (find-imported-mark i.marks externals all)
9146+ ?~ t $(marks t.marks)
9147+ [[i.marks [u.t ~]] $(marks t.marks)]
9148+::
9149+:: Experimental direct poke-only API. Unsupported API declarations fail
9150+:: as a whole; supplied mark reader results retain their existing boundary.
9151+++ api-poke-interface
9152+ |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
9153+ ^- (unit ifile)
9154+ ?. ?=([%ui %api @ %jibb ~] at) ~
9155+ ?~ prelude ~
9156+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
9157+ =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
9158+ ?~ poke ~
9159+ ?. ?=(%union -.typ.u.poke) ~
9160+ ?^ vars.u.poke ~
9161+ =/ compatible=?
9162+ %+ lien cases.typ.u.poke
9163+ |= c=itype
9164+ ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
9165+ ?. compatible ~
9166+ ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
9167+ ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
9168+ =/ marks=(list term) (collect-mark-imports imports.mod)
9169+ ?. ?=([@ ~] marks) ~
9170+ =/ ds=(list def) defs.mod
9171+ ?. ?=([[%mold *] ~] ds) ~
9172+ ?. =(%poke name.i.ds) ~
9173+ =/ sh=shape shape.i.ds
9174+ ?. ?=([%ref *] sh) ~
9175+ ?. ?=([@ ~] names.sh) ~
9176+ =/ n=term i.names.sh
9177+ ?. (unique-value-name n marks) ~
9178+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
9179+ =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
9180+ ?~ mark ~
9181+ =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
9182+ `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]]]
9183+::
71719184++ infer-jibb-file
71729185 |= [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)]
71739186 ^- jfile-result
7174− ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
71759187 =/ parsed (parse at src)
71769188 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
71779189 =/ mod=module p.parsed
7178− ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
9190+ ?: ?=([%ui %api *] at)
9191+ =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
9192+ ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
9193+ [%& [u.iface [[at u.iface] cache]]]
9194+ ?. (module-scope-valid mod prelude-values prelude-molds)
9195+ ?: (pending-declared-poke at mod prelude-values prelude-molds)
9196+ [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
9197+ [%| (crip "module has conflicting names: {(spud at)}")]
71799198 =/ vals=(list term) (global-value-names defs.mod)
71809199 ?: (lien vals |=(n=term =(n %main)))
71819200 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
@@ -7193,7 +9212,7 @@
71939212 =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
71949213 ?. (module-values-complete defs.mod env)
71959214 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
7196− [%& [[env p.mts at] [[at [env p.mts at]] cache.p.js]]]
9215+ [%& [[env p.mts at ~] [[at [env p.mts at ~]] cache.p.js]]]
71979216::
71989217:: +golden-types-with-modules fails closed for imports without prelude
71999218:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -7225,6 +9244,12 @@
72259244 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
72269245 (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
72279246::
9247+++ golden-types-with-prelude-and-internal
9248+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t internal-source=@t]
9249+ ^- @t
9250+ =/ prepared=(unit iprelude) (prepare-prelude-with-internal prelude-source internal-source)
9251+ (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
9252+::
72289253++ golden-types-with-prepared-prelude
72299254 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
72309255 ^- @t
@@ -7235,6 +9260,8 @@
72359260 =/ prelude-molds=(list term) molds.u.prepared
72369261 =/ iface=(unit ifile) `iface.u.prepared
72379262 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
9263+ ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
9264+ 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
72389265 'partial inference; module not checked\0amodule has conflicting names'
72399266 =/ js=jimports-result
72409267 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
@@ -7247,6 +9274,23 @@
72479274:: entries, as [mark result] with the result from +read-mark:jibb-import.
72489275:: Unknown, duplicated, failed and undeclared entries never resolve a mold.
72499276::
9277+:: Callers pass unchanged structured reader results; graph validation
9278+:: remains in the existing bridge, and failures stay available lazily.
9279+++ reader-result-for-checker
9280+ |= result=*
9281+ ^- *
9282+ ?: ?=([%ok *] result) [%& +.result]
9283+ result
9284+::
9285+++ golden-types-with-reader-diagnostics
9286+ |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
9287+ ^- @t
9288+ =/ ex=iexternals
9289+ (turn externals |=(e=[module=term name=term result=*] [module.e name.e (reader-result-for-checker result.e)]))
9290+ =/ mx=imark-externals
9291+ (turn mark-externals |=(e=[mark=term result=*] [mark.e (reader-result-for-checker result.e)]))
9292+ (golden-types-with-marks file src ex mx)
9293+::
72509294++ golden-types-with-marks
72519295 |= [file=path src=@t externals=iexternals mark-externals=imark-externals]
72529296 ^- @t
@@ -7263,7 +9307,9 @@
72639307 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
72649308 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
72659309 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
7266− =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
9310+ =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
9311+ =/ cycles=(list icycle) (definite-value-cycles ds globals)
9312+ =/ env=ienv env.resolution
72679313 =/ lines=(list @t) ~
72689314 |-
72699315 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -7272,10 +9318,31 @@
72729318 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
72739319 ?. (unique-value-name name.d globals)
72749320 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
9321+ =/ cycle=(list icycle) (skim cycles |=(c=icycle =(name.c name.d)))
9322+ ?^ cycle
9323+ =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
9324+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
9325+ ?: (lien grouped.resolution |=(n=term =(n name.d)))
9326+ =/ found=(unit ischeme) (ienv-lookup name.d env)
9327+ ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
9328+ =/ typ=itype (canonical-itype typ.u.found vars.u.found)
9329+ =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
9330+ $(ds t.ds, lines [line lines])
72759331 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
7276− =/ result=iresult (infer-fragment val.d env [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude])
9332+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
9333+ =. initial (reserve-def-caps val.d initial)
9334+ =/ result=iresult
9335+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
9336+ (infer-recursive-gate d env initial)
9337+ (infer-fragment val.d env initial)
72779338 ?: ?=(%| -.result)
72789339 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
9340+ =/ merged=(unit [first=icap second=icap])
9341+ (merged-capitals caps.state.p.result sub.state.p.result)
9342+ ?^ merged
9343+ =/ diag=idiag
9344+ ["distinct type variables `{(trip name.first.u.merged)}` and `{(trip name.second.u.merged)}` must not be forced equal; use the same capital for a shared type" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]
9345+ $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
72799346 ?: (constrained-capitals caps.state.p.result sub.state.p.result)
72809347 $(ds t.ds, lines [(crip "++ {(trip name.d)}: explicit capital constraints are not supported by partial inference") lines])
72819348 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))