@@ -874,7 +874,7 @@
874874 %'~[' %'|=(' %'$-(' :: openers
875875 %'%/' %'/' :: paths
876876 %'+' %'`' %'=' :: pair, unit, face
877− %'*' %'?' %'_' :: noun, loobean, type hole
877+ %'*' %'?' :: noun, loobean mold
878878 %'++' %'+$' %'|=' %'|$' :: runes
879879 %'^-' %'~&' %'?-' %'!!' :: runes
880880 %'/-' %'/%' %'/=' :: imports
@@ -1016,7 +1016,6 @@
10161016 [%const at=span =lit] :: ~ %add %.y
10171017 [%ref at=span names=(list term)] :: state item.todo
10181018 [%tvar at=span name=@t] :: M
1019− [%hole at=span ~] :: _
10201019 [%path at=span segs=(list pseg)] :: / /todos /todo/[id=@ud]
10211020 [%apply at=span ref=(list term) args=(list shape)] :: (list @t)
10221021 [%cell at=span fields=(list field)] :: [text=@t done=?]
@@ -1025,9 +1024,9 @@
10251024 [%generic at=span vars=(list @t) body=shape] :: +$ name |$ [M] …
10261025 ==
10271026::
1028−:: +pseg: a path mold's segment, a knot, [name=aura], or [name=_]
1027+:: +pseg: a path mold's segment, a knot or [name=aura]
10291028::
1030−+$ pseg $%([%knot p=@ta] [%typed at=span name=term aura=@ta] [%inferred at=span name=term hole-at=span])
1029++$ pseg $%([%knot p=@ta] [%typed at=span name=term aura=@ta])
10311030::
10321031+| %api
10331032::
@@ -1296,7 +1295,6 @@
12961295 (emit 1 %'=')
12971296 ?: =('`' a) (emit 1 %'`')
12981297 ?: =('*' a) (emit 1 %'*')
1299− ?: =('_' a) (emit 1 %'_')
13001298 ?: =('~' a)
13011299 ?: =('[' b) (emit 2 %'~[')
13021300 ?: =('&' b) (emit 2 %'~&')
@@ -1672,14 +1670,14 @@
16721670:: What may begin each place the parser reads (section 3, Errors):
16731671:: an expression a-z 0-9 " ( [ ~ % / ` | ^ ? !
16741672:: an operand a-z 0-9 " ( [ ~ % / ` | !
1675−:: a mold a-z A-Z @ * ! ? ~ % / ( [ $ _
1673+:: a mold a-z A-Z @ * ! ? ~ % / ( [ $
16761674:: a pattern a-z 0-9 " ~ % * [
16771675:: and what may go tight after an operand: . ( + = after a name, a
16781676:: closer ) ] }, or the : of a comment
16791677::
16801678++ expr-mask 0x57ff.ffff.4800.0000.83ff.8126.0000.0000
16811679++ operand-mask 0x57ff.ffff.0800.0000.03ff.8126.0000.0000
1682−++ mold-mask 0x47ff.fffe.8fff.ffff.8000.8532.0000.0000
1680+++ mold-mask 0x47ff.fffe.0fff.ffff.8000.8532.0000.0000
16831681++ bar-mask 0x1000.0000.0000.0000.0000.0000.0000.0000
16841682++ pattern-mask 0x47ff.fffe.0800.0000.03ff.0424.0000.0000
16851683++ after-mask 0x2000.0000.2000.0000.2400.4b00.0000.0000
@@ -2109,7 +2107,6 @@
21092107 ?- -.s
21102108 %knot (weld "/" (trip p.s))
21112109 %typed "/[{(trip name.s)}=@{(trip aura.s)}]"
2112− %inferred "/[{(trip name.s)}=_]"
21132110 ==
21142111::
21152112++ show-tvars
@@ -2321,7 +2318,6 @@
23212318 %const (nod "const" at.s (show-lit lit.s) ~)
23222319 %ref (nod "ref" at.s (show-names names.s) ~)
23232320 %tvar (nod "tvar" at.s (trip name.s) ~)
2324− %hole (nod "hole" at.s "" ~)
23252321 %path (nod "path" at.s (show-psegs segs.s) ~)
23262322 %apply (nod "apply" at.s (show-names ref.s) (turn args.s sexp-shape))
23272323 %cell (nod "cell" at.s "" (turn fields.s sexp-field))
@@ -3846,7 +3842,6 @@
38463842 %'*' [%& [%noun at.t ~] t.ts]
38473843 %'!!' [%& [%void at.t ~] t.ts]
38483844 %'?' [%& [%flag at.t ~] t.ts]
3849− %'_' [%& [%hole at.t ~] t.ts]
38503845 [%name *] [%& [%ref at.t ~[p.lex.t]] t.ts]
38513846 [%wing *] [%& [%ref at.t p.lex.t] t.ts]
38523847 [%tvar *] [%& [%tvar at.t p.lex.t] t.ts]
@@ -4063,7 +4058,7 @@
40634058 ?: &(?=(^ nex) tight.i.nex) (bad nex "a path segment")
40644059 (bad-space i.after nex "a path segment")
40654060 ::
4066− :: +read-pseg: a path mold's knot, [name=aura], or [name=_] with no
4061+ :: +read-pseg: a path mold's segment, a knot or [name=aura] with no
40674062 :: spaces, and where it ends
40684063 ::
40694064 ++ read-pseg
@@ -4080,16 +4075,13 @@
40804075 ?: |(?=(~ r2) !tight.i.r2) (bad-space i.r1 r2 "`=`")
40814076 ?. ?=([[* * %'='] *] r2) (bad-in r2 "`=`" tis-mask)
40824077 =/ r3=(list token) t.r2
4083− ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura or type hole")
4084− ?. ?=([[* * ?([%aura *] %'_')] *] r3) (bad-in r3 "an aura or type hole" (con pat-mask (bex 95)))
4078+ ?: |(?=(~ r3) !tight.i.r3) (bad-space i.r2 r3 "an aura")
4079+ ?. ?=([[* * [%aura *]] *] r3) (bad-in r3 "an aura" pat-mask)
40854080 =/ r4=(list token) t.r3
40864081 ?: |(?=(~ r4) !tight.i.r4) (bad-space i.r3 r4 "`]`")
40874082 ?. ?=([[* * %']'] *] r4) (bad-in r4 "`]`" ser-mask)
40884083 =/ at=span [beg.at.op end.at.i.r4]
4089− =/ seg=pseg
4090− ?: ?=(%'_' lex.i.r3) [%inferred at p.lex.i.r1 at.i.r3]
4091− [%typed at p.lex.i.r1 p.lex.i.r3]
4092− [%& [seg end.at.i.r4] t.r4]
4084+ [%& [[%typed at p.lex.i.r1 p.lex.i.r3] end.at.i.r4] t.r4]
40934085 --
40944086::
40954087+| %span-check
@@ -4473,7 +4465,6 @@
44734465 %const [%const at.s ~[%lit] %one ~]
44744466 %ref [%ref at.s ~[%name %wing] %one ~]
44754467 %tvar [%tvar at.s ~[%tvar] %one ~]
4476− %hole [%hole at.s ~[%'_'] %one ~]
44774468 %apply [%apply at.s ~[%'('] %shut (turn args.s outline-shape)]
44784469 %cell [%cell at.s ~[%'['] %shut (turn fields.s outline-sample)]
44794470 ::
@@ -4482,11 +4473,8 @@
44824473 %+ murn segs.s
44834474 |= g=pseg
44844475 ^- (unit outline)
4485− ?- -.g
4486− %knot ~
4487− %typed `[%typed at.g ~[%'['] %shut ~]
4488− %inferred `[%typed at.g ~[%'['] %shut ~[[%hole hole-at.g ~[%'_'] %one ~]]]
4489− ==
4476+ ?. ?=(%typed -.g) ~
4477+ `[%typed at.g ~[%'['] %shut ~]
44904478 [%path at.s ~[%'/'] %run ks]
44914479 ::
44924480 %union
@@ -4546,8 +4534,6 @@
45464534 [%path [1 9] [1 9] [1 21]]
45474535 [%face [1 7] [1 7] [1 21]]
45484536 ==
4549− :: an inferred path aura's hole spanning its = as well
4550− ['+$ x /a/[id=_]' ~[[%hole [1 13] [1 12] [1 14]]]]
45514537 :: an import's path cut short
45524538 ['/= c /ui/c' ~[[%jibb [1 1] [1 1] [1 11]]]]
45534539 :: brackets that close with the deeper lines, cut at their line's
@@ -4614,20 +4600,6 @@
46144600:: from their display name. Generic cases must be disjoint for all arguments.
46154601:: Unnamed union printing is informational; it is not Jibb syntax.
46164602::
4617−:: `proj` is a reserved, type-directed operation, not an ordinary gate.
4618−:: The supported fragment selects uniquely faced fields from a known record
4619−:: in source order (reordering is a doc question). It records the original
4620−:: call, source and target types, and source axes with its definition;
4621−:: A single selected field keeps its face and uses one source axis.
4622−:: Checked module interfaces retain that evidence and their source, including
4623−:: the private prelude dependency. A later lowerer must replace the call by
4624−:: an inline gate applied to the operand once; no lowering is implemented yet.
4625−:: Ordinary fits never insert a projection. Unknown or variable-origin record
4626−:: spines, implicit narrowing inside selected fields, and projections in
4627−:: recursive groups remain unsupported. Directional fits bound faced-spine
4628−:: proofs to fewer than 1,024 cells; the projection planner has a separate
4629−:: 4,096-step bound. These are inference limits, not language limits.
4630−::
46314603+$ itype
46324604 $~ [%var 0]
46334605 $% [%var id=@ud]
@@ -4636,12 +4608,10 @@
46364608 [%atom aura=@ta]
46374609 [%any-atom ~]
46384610 [%flag ~]
4639− [%noun ~]
46404611 [%tag id=@ud literal=lit constructor=?]
46414612 [%const literal=lit]
46424613 [%collection name=term args=(list itype)]
46434614 [%recursive module=term name=term label=(unit @t)]
4644− [%jrec at=path name=term label=(unit @t) head=term aura=@ta tail=term]
46454615 [%union cases=(list itype) origin=(unit [at=path name=term]) label=(unit @t) args=(list itype)]
46464616 [%face name=term body=itype]
46474617 [%fn sample=itype product=itype]
@@ -4691,12 +4661,10 @@
46914661 %atom |
46924662 %any-atom |
46934663 %flag |
4694− %noun |
46954664 %tag =(n id.t)
46964665 %const |
46974666 %union |((lien cases.t |=(c=itype (itype-occurs n c sub))) (lien args.t |=(c=itype (itype-occurs n c sub))))
46984667 %recursive |
4699− %jrec |
47004668 %collection (lien args.t |=(c=itype (itype-occurs n c sub)))
47014669 %face $(t body.t)
47024670 %fn |($(t sample.t) $(t product.t))
@@ -4715,8 +4683,6 @@
47154683 =. a (itype-walk a sub)
47164684 =. b (itype-walk b sub)
47174685 ?: =(a b) `sub
4718− ?: &(?=(%jrec -.a) ?=(%jrec -.b))
4719− ?:(&(=(at.a at.b) =(name.a name.b) =(head.a head.b) =(aura.a aura.b) =(tail.a tail.b)) `sub ~)
47204686 ?: &(?=(%recursive -.a) ?=(%recursive -.b))
47214687 ?:(&(=(module.a module.b) =(name.a name.b)) `sub ~)
47224688 ?: &(?=(%union -.a) ?=(%union -.b))
@@ -4791,12 +4757,10 @@
47914757 %atom |
47924758 %any-atom &
47934759 %flag |
4794− %noun |
47954760 %tag |
47964761 %const |
47974762 %union |((lien cases.t |=(c=itype (itype-has-any-atom c sub))) (lien args.t |=(c=itype (itype-has-any-atom c sub))))
47984763 %recursive |
4799− %jrec |
48004764 %collection (lien args.t |=(c=itype (itype-has-any-atom c sub)))
48014765 %face $(t body.t)
48024766 %fn |($(t sample.t) $(t product.t))
@@ -4863,12 +4827,10 @@
48634827 %atom &
48644828 %any-atom &
48654829 %flag &
4866− %noun |
48674830 %tag &
48684831 %const &
48694832 %union |((lien cases.typ |=(c=itype (itype-has-fixed-atom c))) (lien args.typ |=(c=itype (itype-has-fixed-atom c))))
48704833 %recursive |
4871− %jrec |
48724834 %collection (lien args.typ |=(c=itype (itype-has-fixed-atom c)))
48734835 %face $(typ body.typ)
48744836 %fn |($(typ sample.typ) $(typ product.typ))
@@ -4954,8 +4916,6 @@
49544916 %cell &
49554917 %union &
49564918 %recursive &
4957− %jrec &
4958− %noun &
49594919 %collection &
49604920 %face $(t body.t)
49614921 %fn |($(t sample.t) $(t product.t))
@@ -5027,7 +4987,6 @@
50274987 ^- ?
50284988 ?- -.t
50294989 %recursive &
5030− %jrec &
50314990 %collection (lien args.t |=(c=itype (itype-has-recursive c)))
50324991 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-recursive c)))
50334992 %face $(t body.t)
@@ -5041,7 +5000,6 @@
50415000 ^- ?
50425001 ?- -.t
50435002 %recursive ?=(~ label.t)
5044− %jrec ?=(~ label.t)
50455003 %collection (lien args.t |=(c=itype (itype-has-hidden-recursive c)))
50465004 %union (lien (weld args.t cases.t) |=(c=itype (itype-has-hidden-recursive c)))
50475005 %face $(t body.t)
@@ -5092,39 +5050,11 @@
50925050++ itype-fit
50935051 |= [actual=itype expected=itype sub=isub next=@ud]
50945052 ^- ifit
5095− (itype-fit-inner actual expected sub next | |)
5096−++ itype-fit-inner
5097− |= [actual=itype expected=itype sub=isub next=@ud skip-width=? spine-proof=?]
5098− ^- ifit
5099− ?: &(!skip-width ?=(%cell -.actual) ?=(%cell -.expected) |((width-spine-exhausted actual 1.024) (width-spine-exhausted expected 1.024)))
5100− [%unknown ~]
5101− =/ known=(unit [source=iwfields target=iwfields])
5102− ?: skip-width ~
5103− (width-known-shape actual expected sub)
5104− =/ too-wide=? ?~(known | (gth (lent order.source.u.known) (lent order.target.u.known)))
5105− ?: too-wide [%unknown ~]
5106− =/ spine-checked=? |(spine-proof ?=(^ known))
51075053 =/ uncertain=?
51085054 |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual) ?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected))
5109− =/ actual-open=?
5110− |(?=(%var -.actual) ?=(%avar -.actual) ?=(%nvar -.actual))
51115055 =. actual (itype-walk actual sub)
51125056 =. expected (itype-walk expected sub)
51135057 ?: =(actual expected) [%ok sub next]
5114− :: Any value can be used where a noun is expected. An unresolved
5115− :: bare tag is fixed as a constant; a constructor still needs a gate.
5116− ?: ?=(%noun -.expected)
5117− ?: ?=(%tag -.actual)
5118− ?: constructor.actual [%unknown ~]
5119− [%ok [[id.actual expected] sub] next]
5120− [%ok sub next]
5121− :: An arbitrary noun is not known to fit a narrower type.
5122− ?: &(?=(%noun -.actual) !?=(%var -.expected)) [%unknown ~]
5123− ?: &(!uncertain ?=(%jrec -.actual) ?=(%face -.expected)) $(expected body.expected)
5124− ?: &(!uncertain ?=(%face -.actual) ?=(%jrec -.expected)) $(actual body.actual)
5125− ?: &(?=(%jrec -.actual) ?=(%jrec -.expected))
5126− ?:(&(=(at.actual at.expected) =(name.actual name.expected) =(head.actual head.expected) =(aura.actual aura.expected) =(tail.actual tail.expected)) [%ok sub next] [%bad ~])
5127− ?: &(|(?=(%jrec -.actual) ?=(%jrec -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
51285058 ?: &(?=(%recursive -.actual) ?=(%recursive -.expected))
51295059 ?:(&(=(module.actual module.expected) =(name.actual name.expected)) [%ok sub next] [%bad ~])
51305060 ?: &(|(?=(%recursive -.actual) ?=(%recursive -.expected)) !|(?=(%var -.actual) ?=(%var -.expected))) [%unknown ~]
@@ -5136,19 +5066,6 @@
51365066 =/ unified=(unit isub) (itype-unify-args args.actual args.expected sub)
51375067 ?^ unified [%ok u.unified next]
51385068 [%unknown ~]
5139− :: A known union can instantiate an unconstrained sample directly;
5140− :: preserve unknown results for variable-bound union origins.
5141− ?: &(!actual-open ?=(%union -.actual) ?=(%var -.expected))
5142− ?~ origin.actual [%unknown ~]
5143− =/ normalized=itype (itype-normalize actual sub)
5144− ?: |((itype-has-tag normalized) (itype-has-recursive normalized) (itype-has-any-atom actual sub)) [%unknown ~]
5145− =/ unified=(unit isub) (itype-unify actual expected sub)
5146− ?~ unified [%unknown ~]
5147− [%ok u.unified next]
5148− :: A concrete union value in a tuple may acquire the expected field's
5149− :: face. A variable-bound union still needs face propagation support.
5150− ?: &(!uncertain ?=(%union -.actual) ?=(%face -.expected))
5151− $(expected body.expected)
51525069 ?: ?=(%union -.actual) [%unknown ~]
51535070 ?: &(?=(%union -.expected) |(?=(%avar -.actual) ?=(%nvar -.actual))) [%unknown ~]
51545071 ?: &(?=(%union -.expected) !?=(%var -.actual))
@@ -5167,10 +5084,6 @@
51675084 =/ trial=ifit (itype-fit-ctor-cases literal.actual sample.expected cases sub next)
51685085 ?. ?=(%ok -.trial) trial
51695086 [%ok [[id.actual expected] sub.trial] next.trial]
5170− :: Zero may be the empty list. A nested cell fit lacks the context
5171− :: needed to resolve it here, so do not report a definite mismatch.
5172− ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5173− [%unknown ~]
51745087 ?: ?=(%const -.expected)
51755088 ?:(=(val.literal.actual val.literal.expected) [%ok [[id.actual expected] sub] next] [%bad ~])
51765089 ?: ?=(%atom -.expected)
@@ -5188,8 +5101,6 @@
51885101 [%ok u.u next]
51895102 ?: |(?=(%avar -.expected) ?=(%nvar -.expected)) [%unknown ~]
51905103 ?: ?=(%face -.expected) $(expected body.expected)
5191− ?: &(?=(%collection -.expected) =(%list name.expected) =(0 val.literal.actual))
5192− [%unknown ~]
51935104 ?: ?=(%const -.expected)
51945105 ?:(=(val.literal.actual val.literal.expected) [%ok sub next] [%bad ~])
51955106 ?: ?=(%atom -.expected)
@@ -5219,9 +5130,9 @@
52195130 ?: &((aura-prefix aura.actual aura.expected) uncertain) [%unknown ~]
52205131 [%bad ~]
52215132 ?: &(?=(%cell -.actual) ?=(%cell -.expected))
5222− =/ first=ifit $(actual hed.actual, expected hed.expected, skip-width |, spine-proof |)
5133+ =/ first=ifit $(actual hed.actual, expected hed.expected)
52235134 ?. ?=(%ok -.first) first
5224− $(actual tal.actual, expected tal.expected, sub sub.first, next next.first, skip-width spine-checked, spine-proof spine-checked)
5135+ $(actual tal.actual, expected tal.expected, sub sub.first, next next.first)
52255136 :: A field may add a face to an occurrence of the very same type
52265137 :: variable. Binding that variable to a face around itself would fail
52275138 :: the occurs check, but its underlying type has already matched.
@@ -5243,9 +5154,9 @@
52435154 [%ok u.unified next]
52445155 ?: &(?=(%face -.actual) ?=(%face -.expected))
52455156 ?. =(name.actual name.expected) [%bad ~]
5246− $(actual body.actual, expected body.expected, skip-width |, spine-proof |)
5247− ?: ?=(%face -.actual) $(actual body.actual, skip-width |, spine-proof |)
5248− ?: ?=(%face -.expected) $(expected body.expected, skip-width |, spine-proof |)
5157+ $(actual body.actual, expected body.expected)
5158+ ?: ?=(%face -.actual) $(actual body.actual)
5159+ ?: ?=(%face -.expected) $(expected body.expected)
52495160 ?: (itype-face-asym actual expected sub) [%unknown ~]
52505161 ?: |((itype-has-any-atom actual sub) (itype-has-any-atom expected sub))
52515162 [%unknown ~]
@@ -5321,10 +5232,7 @@
53215232+$ ischeme [typ=itype vars=(list @ud)]
53225233+$ ienv (list [name=term scheme=ischeme])
53235234+$ imold-types (list [name=term template=ischeme])
5324−+$ iderived [name=term agent=term mark=term]
5325−+$ iwidth-definition [name=term original=expr typ=itype sub=isub projections=(list iwprojection)]
5326−+$ iwidth-dependency [at=path source=(unit @t) definitions=(list iwidth-definition)]
5327−+$ ifile [values=ienv molds=imold-types at=path derived=(list iderived) elaborations=(list iwidth-definition) dependencies=(list iwidth-dependency) source=(unit @t)]
5235++$ ifile [values=ienv molds=imold-types at=path]
53285236+$ ijimports (list [face=term interface=ifile])
53295237+$ icap [name=@t id=@ud at=span]
53305238+$ icaps (list icap)
@@ -5334,100 +5242,7 @@
53345242:: This core has no Ford dependencies; unrecognized payloads fail closed.
53355243+$ iexternals (list [module=term name=term result=*])
53365244+$ imark-externals (list [mark=term result=*])
5337−:: Hole obligations survive discarded expressions until their owning
5338−:: definition has inferred; their source spans support unresolved reports.
5339−+$ ihole [id=@ud at=span]
5340−:: Recursive-mold unfolding spends fuel in the threaded inference state.
5341−:: Retries can restart from an earlier state, so this bounds an attempt,
5342−:: not all parsing or module-checking work.
5343−:: Experimental: only closed, uniquely faced records have known axes.
5344−+$ iwfield [name=term axis=@ud typ=itype]
5345−+$ iwfields [order=(list iwfield) index=(map term iwfield)]
5346−+$ iwstep [name=term axis=@ud]
5347−+$ iwidth-result [steps=(list iwstep) sub=isub next=@ud]
5348−+$ iwprojection [at=span original=expr source=itype target=itype steps=(list iwstep)]
5349−++ width-scan
5350− |= [typ=itype sub=isub axis=@ud fuel=@ud]
5351− ^- (unit iwfields)
5352− =/ order=(list iwfield) ~
5353− =/ index=(map term iwfield) *(map term iwfield)
5354− |-
5355− ?: =(0 fuel) ~
5356− ?: |(?=(%var -.typ) ?=(%avar -.typ) ?=(%nvar -.typ)) ~
5357− ?: ?=(%face -.typ)
5358− =/ entry=iwfield [name.typ axis body.typ]
5359− ?: ?=(^ (~(get by index) name.entry)) ~
5360− `[(flop [entry order]) (~(put by index) name.entry entry)]
5361− ?. ?=(%cell -.typ) ~
5362− =/ head=itype hed.typ
5363− ?: |(?=(%var -.head) ?=(%avar -.head) ?=(%nvar -.head)) ~
5364− ?. ?=(%face -.head) ~
5365− =/ entry=iwfield [name.head (mul 2 axis) body.head]
5366− ?: ?=(^ (~(get by index) name.entry)) ~
5367− $(typ tal.typ, axis +((mul 2 axis)), fuel (dec fuel), order [entry order], index (~(put by index) name.entry entry))
5368−++ width-in-order
5369− |= [source=(list iwfield) target=(list iwfield)]
5370− ^- ?
5371− ?~ target &
5372− ?~ source |
5373− ?: =(name.i.source name.i.target) $(source t.source, target t.target)
5374− $(source t.source)
5375−++ width-fit-fields
5376− |= [source=(map term iwfield) target=(list iwfield) sub=isub next=@ud]
5377− ^- (unit iwidth-result)
5378− ?~ target `[~ sub next]
5379− =/ found=(unit iwfield) (~(get by source) name.i.target)
5380− ?~ found ~
5381− =/ fit=ifit (itype-fit typ.u.found typ.i.target sub next)
5382− ?. ?=(%ok -.fit) ~
5383− =/ rest=(unit iwidth-result) $(target t.target, sub sub.fit, next next.fit)
5384− ?~ rest ~
5385− `[[[name.i.target axis.u.found] steps.u.rest] sub.u.rest next.u.rest]
5386−++ width-spine-exhausted
5387− |= [t=itype fuel=@ud]
5388− ^- ?
5389− ?: =(0 fuel) &
5390− ?. ?=(%cell -.t) |
5391− ?. ?=(%face -.hed.t) |
5392− $(t tal.t, fuel (dec fuel))
5393−++ width-known-shape
5394− |= [actual=itype expected=itype sub=isub]
5395− ^- (unit [source=iwfields target=iwfields])
5396− ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5397− =/ source=(unit iwfields) (width-scan actual sub 1 1.024)
5398− =/ target=(unit iwfields) (width-scan expected sub 1 1.024)
5399− ?~ source ~
5400− ?~ target ~
5401− `[u.source u.target]
5402−::
5403−++ width-shape
5404− |= [actual=itype expected=itype sub=isub]
5405− ^- (unit [source=iwfields target=iwfields])
5406− ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
5407− =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5408− =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5409− ?~ source ~
5410− ?~ target ~
5411− ?. (gth (lent order.u.source) (lent order.u.target)) ~
5412− `[u.source u.target]
5413−++ width-proj-shape
5414− |= [actual=itype expected=itype sub=isub]
5415− ^- (unit [source=iwfields target=iwfields])
5416− ?. &(|(?=(%cell -.actual) ?=(%face -.actual)) |(?=(%cell -.expected) ?=(%face -.expected))) ~
5417− =/ source=(unit iwfields) (width-scan actual sub 1 4.096)
5418− =/ target=(unit iwfields) (width-scan expected sub 1 4.096)
5419− ?~ source ~
5420− ?~ target ~
5421− ?: (lth (lent order.u.source) (lent order.u.target)) ~
5422− `[u.source u.target]
5423−::
5424−++ width-project
5425− |= [shape=[source=iwfields target=iwfields] sub=isub next=@ud]
5426− ^- (unit iwidth-result)
5427− ?. (width-in-order order.source.shape order.target.shape) ~
5428− (width-fit-fields index.source.shape order.target.shape sub next)
5429−::
5430−+$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile) holes=(list ihole) jrec-fuel=@ud projections=(list iwprojection)]
5245++$ istate [next=@ud sub=isub caps=icaps binders=(list @ud) molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) params=iparams active=(list term) tags=(list ipending) in-mold=? at=path top-molds=(list term) prelude=(unit ifile)]
54315246+$ idiag [msg=tape sites=(list [at=span note=tape])]
54325247+$ iresult (each [typ=itype state=istate] idiag)
54335248+$ isample-result (each [typ=itype env=ienv state=istate] tape)
@@ -5463,8 +5278,6 @@
54635278:: generalize an aura from its sample, which requires constraint analysis
54645279:: beyond this fragment; leave those cases unresolved.
54655280::
5466−:: This helper only controls decimal defaulting in visible types. A noun
5467−:: may contain gates and is not proof of a gate-free value.
54685281++ itype-has-gate
54695282 |= t=itype
54705283 ^- ?
@@ -5472,7 +5285,6 @@
54725285 %fn &
54735286 %cell |($(t hed.t) $(t tal.t))
54745287 %recursive |
5475− %jrec |
54765288 %collection (lien args.t |=(c=itype (itype-has-gate c)))
54775289 %face $(t body.t)
54785290 %union (lien cases.t |=(c=itype (itype-has-gate c)))
@@ -5484,7 +5296,6 @@
54845296 %atom |
54855297 %any-atom |
54865298 %flag |
5487− %noun |
54885299 ==
54895300::
54905301++ default-decimals
@@ -5499,90 +5310,6 @@
54995310 * t
55005311 ==
55015312::
5502−:: A hole is solved only by a fully determined type or a written
5503−:: in-scope type variable. Ordinary fresh variables are not evidence.
5504−:: Compare representatives after substitution, since unification can
5505−:: orient a written capital toward the hole rather than the reverse.
5506−++ hole-variable-id
5507− |= t=itype
5508− ^- (unit @ud)
5509− ?- -.t
5510− %var `id.t
5511− %avar `id.t
5512− %nvar `id.t
5513− %tag `id.t
5514− * ~
5515− ==
5516−++ hole-same-variable
5517− |= [a=itype b=itype]
5518− ^- ?
5519− =/ x=(unit @ud) (hole-variable-id a)
5520− ?~ x |
5521− =/ y=(unit @ud) (hole-variable-id b)
5522− ?~ y |
5523− =(u.x u.y)
5524−++ hole-known
5525− |= [t=itype state=istate]
5526− ^- ?
5527− =. t (itype-walk t sub.state)
5528− ?- -.t
5529− ?(%var %avar %nvar)
5530− ?: (lien caps.state |=(c=icap (hole-same-variable t (itype-walk [%var id.c] sub.state)))) &
5531− (lien params.state |=(p=[name=@t typ=itype] (hole-same-variable t (itype-walk typ.p sub.state))))
5532− %tag |
5533− %any-atom &
5534− %union &((levy cases.t |=(c=itype (hole-known c state))) (levy args.t |=(c=itype (hole-known c state))))
5535− %collection (levy args.t |=(c=itype (hole-known c state)))
5536− %face $(t body.t)
5537− %fn &($(t sample.t) $(t product.t))
5538− %cell &($(t hed.t) $(t tal.t))
5539− * &
5540− ==
5541−++ default-hole-numbers
5542− |= [all=(list ihole) prior=(list ihole) state=istate env=ienv permit=?]
5543− ^- istate
5544− :: Do not default a named capital or a variable captured from env.
5545− ?. permit state
5546− ?: =(all prior) state
5547− ?~ all state
5548− =/ t=itype (itype-walk [%var id.i.all] sub.state)
5549− =/ free=(list @ud) (free-env-vars env sub.state)
5550− =? state &(?=(%nvar -.t) !(hole-known t state) !(lien free |=(id=@ud =(id id.t))))
5551− state(sub [[id.t [%atom %ud]] sub.state])
5552− $(all t.all)
5553−::
5554−:: Only obligations created inside this definition belong to it.
5555−++ holes-created
5556− |= [all=(list ihole) prior=(list ihole)]
5557− ^- (list ihole)
5558− ?: =(all prior) ~
5559− ?~ all ~
5560− [i.all $(all t.all)]
5561−++ hole-uncertain
5562− |= [t=itype state=istate]
5563− ^- ?
5564− =. t (itype-walk t sub.state)
5565− ?- -.t
5566− ?(%tag %nvar %avar) !(hole-known t state)
5567− %union |((lien cases.t |=(c=itype (hole-uncertain c state))) (lien args.t |=(c=itype (hole-uncertain c state))))
5568− %collection (lien args.t |=(c=itype (hole-uncertain c state)))
5569− %face $(t body.t)
5570− %fn |($(t sample.t) $(t product.t))
5571− %cell |($(t hed.t) $(t tal.t))
5572− * |
5573− ==
5574−::
5575−++ unresolved-hole
5576− |= [all=(list ihole) prior=(list ihole) state=istate]
5577− ^- (unit idiag)
5578− =/ work=(list ihole) (flop (holes-created all prior))
5579− |-
5580− ?~ work ~
5581− ?: (hole-known [%var id.i.work] state) $(work t.work)
5582− ?: (hole-uncertain [%var id.i.work] state)
5583− `["type hole needs unsupported inference" ~[[at.i.work "type hole"]]]
5584− `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
5585−::
55865313++ itype-vars
55875314 |= t=itype
55885315 ^- (list @ud)
@@ -5593,12 +5320,10 @@
55935320 %atom ~
55945321 %any-atom ~
55955322 %flag ~
5596− %noun ~
55975323 %tag ~
55985324 %const ~
55995325 %union (zing (turn (weld args.t cases.t) |=(c=itype (itype-vars c))))
56005326 %recursive ~
5601− %jrec ~
56025327 %collection (zing (turn args.t |=(c=itype (itype-vars c))))
56035328 %face $(t body.t)
56045329 %fn (weld $(t sample.t) $(t product.t))
@@ -5633,12 +5358,10 @@
56335358 %atom t
56345359 %any-atom t
56355360 %flag t
5636− %noun t
56375361 %tag t
56385362 %const t
56395363 %union [%union (turn cases.t |=(c=itype (itype-rename c ren))) origin.t label.t (turn args.t |=(c=itype (itype-rename c ren)))]
56405364 %recursive t
5641− %jrec t
56425365 %collection [%collection name.t (turn args.t |=(c=itype (itype-rename c ren)))]
56435366 %face [%face name.t $(t body.t)]
56445367 %fn [%fn $(t sample.t) $(t product.t)]
@@ -5658,12 +5381,10 @@
56585381 %atom |
56595382 %any-atom |
56605383 %flag |
5661− %noun |
56625384 %tag |
56635385 %const |
56645386 %union |((lien cases.t |=(c=itype (itype-var-is-atom n c))) (lien args.t |=(c=itype (itype-var-is-atom n c))))
56655387 %recursive |
5666− %jrec |
56675388 %collection (lien args.t |=(c=itype (itype-var-is-atom n c)))
56685389 %face $(t body.t)
56695390 %fn |($(t sample.t) $(t product.t))
@@ -5766,11 +5487,6 @@
57665487 ?. ?=([%ref @ @] node) ~
57675488 ?. &(=(module +<.node) =(name +>.node)) ~
57685489 `[[%unknown ~] &]
5769− %apply
5770− ?. ?=([%apply %list [* ~]] node) ~
5771− =/ item $(node -.+>.node)
5772− ?~ item ~
5773− `[[%or ~[[%atom `0] [%cell pat.u.item [%unknown ~]]]] has.u.item]
57745490 %face
57755491 ?. ?=([%face @ *] node) ~
57765492 ?. (jibb-face-name +<.node) ~
@@ -5825,10 +5541,6 @@
58255541 %cell ?:(?=([%cell * *] node) (imported-record-faces-valid node ~) |)
58265542 %fork (imported-faces-valid-list +.node)
58275543 %apply ?:(?=([%apply @ *] node) (imported-faces-valid-list +>.node) |)
5828− %named
5829− ?. ?=([%named @ @ *] node) |
5830− =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
5831− (imported-faces-valid body.n)
58325544 ==
58335545::
58345546++ imported-faces-valid-list
@@ -5860,19 +5572,7 @@
58605572 ^- (unit itype)
58615573 ?@ node ~
58625574 ?+ -.node ~
5863− %noun ?:(=(node [%noun ~]) `[%noun ~] ~)
58645575 %atom
5865− :: A Hoon loobean singleton is one of the two Jibb loobeans.
5866− ?: ?=([%atom %f [~ @]] node)
5867− =/ value=@ +>+.node
5868− ?. |(=(value 0) =(value 1)) ~
5869− =/ printed=@t ?:(=(value 0) '%.y' '%.n')
5870− `[%const [%loobean %f value printed]]
5871− :: Hoon's null singleton is the same noun as Jibb's `~` mold.
5872− :: Other non-term singleton atoms remain unsupported here.
5873− ?: ?=([%atom %n [~ @]] node)
5874− ?. =(0 +>+.node) ~
5875− `[%const [%null %n 0 '~']]
58765576 ?: ?=([%atom %tas [~ @]] node)
58775577 =/ value=@ +>+.node
58785578 ?. |(=(value 0) (jibb-face-name value)) ~
@@ -5882,15 +5582,6 @@
58825582 =/ aura=@ta (@ta +<.node)
58835583 ?. |(?=(?(%u %ud %ux %uv %t %ta %tas %p %da %dr) aura) =('tD' aura)) ~
58845584 `[%atom aura]
5885− %named
5886− ?. ?=([%named @ @ *] node) ~
5887− =/ n=[%named module=@ name=@ body=*] ;;([%named module=@ name=@ body=*] node)
5888− ?. &((jibb-face-name module.n) (jibb-face-name name.n)) ~
5889− ?. ?=([%fork *] body.n) ~
5890− =/ proof=(unit irec-pattern) (rec-pattern body.n (@tas module.n) (@tas name.n))
5891− ?~ proof ~
5892− ?. has.u.proof ~
5893− `[%recursive (@tas module.n) (@tas name.n) `(crip "{(trip name.n)}.{(trip module.n)}")]
58945585 %apply
58955586 ?. ?=([%apply @ *] node) ~
58965587 =/ name=term (@tas +<.node)
@@ -5904,15 +5595,10 @@
59045595 ?. =(arity (lent u.args)) ~
59055596 `[%collection name u.args]
59065597 %fork
5907− :: Hoon's ordinary ? mold is the fork of its two %f singletons.
5908− =/ raw=* +.node
5909− ?: |(=(raw ~[[%atom %f `0] [%atom %f `1]]) =(raw ~[[%atom %f `1] [%atom %f `0]]))
5910− `[%flag ~]
5911− =/ cases=(unit (list itype)) (import-to-itypes raw)
5598+ =/ cases=(unit (list itype)) (import-to-itypes +.node)
59125599 ?~ cases ~
59135600 ?~ u.cases ~
59145601 ?~ t.u.cases ~
5915− ?: (import-has-loobean-singleton u.cases) ~
59165602 ?. (import-cases-disjoint u.cases) ~
59175603 `[%union u.cases ~ ~ ~]
59185604 %face
@@ -5931,20 +5617,6 @@
59315617 `[%cell u.left u.right]
59325618 ==
59335619::
5934−++ import-direct-loobean
5935− |= t=itype
5936− ^- ?
5937− ?: ?=(%face -.t) $(t body.t)
5938− ?: ?=(%union -.t) (import-has-loobean-singleton cases.t)
5939− ?=([%const [%loobean *]] t)
5940−::
5941−++ import-has-loobean-singleton
5942− |= cases=(list itype)
5943− ^- ?
5944− ?~ cases |
5945− ?: (import-direct-loobean i.cases) &
5946− $(cases t.cases)
5947−::
59485620++ import-to-itypes
59495621 |= nodes=*
59505622 ^- (unit (list itype))
@@ -5959,9 +5631,7 @@
59595631 |= typ=itype
59605632 ^- upat
59615633 ?- -.typ
5962− %noun [%all ~]
59635634 %atom [%atom ~]
5964− %flag [%or ~[[%atom `0] [%atom `1]]]
59655635 %const [%atom `val.literal.typ]
59665636 %face $(typ body.typ)
59675637 %cell [%cell $(typ hed.typ) $(typ tal.typ)]
@@ -6056,55 +5726,25 @@
60565726 ?:(=(`origin origin.typ.template) `name.i.molds $(molds t.molds))
60575727 $(molds t.molds)
60585728::
6059−:: A public non-generic alias names exactly its origin and arguments.
6060−:: Reusing only an origin could print a different generic instantiation.
6061−++ prelude-union-alias
6062− |= [origin=[at=path name=term] args=(list itype) molds=imold-types]
6063− ^- (unit term)
6064− ?^ args ~
6065− ?~ molds ~
6066− =/ template=ischeme template.i.molds
6067− ?: &(?=(~ vars.template) ?=(%union -.typ.template))
6068− ?:(&(=(`origin origin.typ.template) =(args args.typ.template)) `name.i.molds $(molds t.molds))
6069− $(molds t.molds)
6070−::
6071−:: Names exported by the directly imported module are visible through its
6072−:: face; a matching prelude alias is also visible without a qualifier.
6073−::
6074−++ jrec-alias
6075− |= [origin=path name=term molds=imold-types]
6076− ^- (unit term)
6077− ?~ molds ~
6078− =/ template=ischeme template.i.molds
6079− ?: &(?=(~ vars.template) ?=(%jrec -.typ.template) =(at.typ.template origin) =(name.typ.template name)) `name.i.molds
6080− $(molds t.molds)
5729+:: Only names exported by this directly imported module are visible through
5730+:: its face. Other origins retain identity but print as unnamed unions.
60815731::
60825732++ itype-in-import
6083− |= [t=itype iface=ifile face=term prelude=(unit ifile)]
5733+ |= [t=itype iface=ifile face=term]
60845734 ^- itype
60855735 ?- -.t
60865736 %union
60875737 =/ label=(unit @t)
60885738 ?~ origin.t ~
60895739 ?: =(at.u.origin.t /lib/jibb/prelude/jibb) `name.u.origin.t
6090− =/ public=(unit term)
6091− ?~ prelude ~
6092− (prelude-union-alias u.origin.t args.t molds.u.prelude)
6093− ?^ public `u.public
60945740 =/ alias=(unit term) ~
60955741 =? alias &(=(at.u.origin.t at.iface) ?=(^ (find-jibb-mold name.u.origin.t iface))) `name.u.origin.t
60965742 =? alias ?=(~ alias) (imported-union-alias u.origin.t molds.iface)
60975743 ?~ alias ~
60985744 `(crip "{(trip u.alias)}.{(trip face)}")
6099− [%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)))]
5745+ [%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)))]
61005746 %recursive [%recursive module.t name.t ~]
6101− %jrec
6102− =/ public=(unit term) ?~(prelude ~ (jrec-alias at.t name.t molds.u.prelude))
6103− ?^ public t(label `u.public)
6104− =/ alias=(unit term) (jrec-alias at.t name.t molds.iface)
6105− ?~ alias t(label ~)
6106− t(label `(crip "{(trip u.alias)}.{(trip face)}"))
6107− %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face prelude)))]
5747+ %collection [%collection name.t (turn args.t |=(c=itype (itype-in-import c iface face)))]
61085748 %face [%face name.t $(t body.t)]
61095749 %fn [%fn $(t sample.t) $(t product.t)]
61105750 %cell [%cell $(t hed.t) $(t tal.t)]
@@ -6177,46 +5817,9 @@
61775817 =/ rest=[params=iparams vars=(list @ud) next=@ud] $(names t.names, next +(next))
61785818 [[[i.names [%var next]] params.rest] [next vars.rest] next.rest]
61795819::
6180−:: Recognize a unique top-level source mold with exactly a null case and a
6181−:: faced atom-headed cell whose faced tail names that same mold. Its Jibb
6182−:: path and name provide nominal identity. Other recursive shapes fail closed;
6183−:: construction and matching expose the proven shape one layer at a time.
6184−++ simple-source-recursive
6185− |= [name=term sh=shape state=istate]
6186− ^- (unit itype)
6187− ?. (lien top-molds.state |=(n=term =(n name))) ~
6188− =/ original=(unit shape) (find-simple-mold name molds.state)
6189− ?~ original ~
6190− ?. =(u.original sh) ~
6191− ?. ?=(%union -.sh) ~
6192− =/ cs=(list shape) cases.sh
6193− ?~ cs ~
6194− ?~ t.cs ~
6195− ?^ t.t.cs ~
6196− ?. ?=(%const -.i.cs) ~
6197− ?. =(%null form.lit.i.cs) ~
6198− ?. ?=(%cell -.i.t.cs) ~
6199− =/ fs=(list field) fields.i.t.cs
6200− ?~ fs ~
6201− ?~ t.fs ~
6202− ?^ t.t.fs ~
6203− ?. ?=(%face -.i.fs) ~
6204− ?. ?=(%aura -.shape.i.fs) ~
6205− ?. !=(0 aura.shape.i.fs) ~
6206− ?. ?=(%face -.i.t.fs) ~
6207− ?. !=(name.i.fs name.i.t.fs) ~
6208− =/ tail=shape shape.i.t.fs
6209− ?. ?=(%ref -.tail) ~
6210− ?. =(names.tail ~[name]) ~
6211− `[%jrec at.state name `name name.i.fs aura.shape.i.fs name.i.t.fs]
6212−::
62135820++ infer-mold-template
62145821 |= [sh=shape state=istate]
62155822 ^- (unit [template=ischeme state=istate])
6216− =/ direct=(unit itype)
6217− ?. ?=([@ ~] active.state) ~
6218− (simple-source-recursive i.active.state sh state)
6219− ?^ direct `[[u.direct ~] state]
62205823 ?: ?=(%generic -.sh)
62215824 ?~ vars.sh ~
62225825 ?. (distinct-params vars.sh) ~
@@ -6224,19 +5827,17 @@
62245827 =/ out=(unit [typ=itype state=istate])
62255828 (infer-simple-shape body.sh state(next next.fresh, params params.fresh, in-mold &))
62265829 ?~ out ~
6227− ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
62285830 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.sh) ?=(~ origin.typ.u.out)) ~
62295831 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.sh))
62305832 typ.u.out(args (turn vars.fresh |=(n=@ud `itype`[%var n])))
62315833 =/ used=(list @ud) (itype-vars typ.u.out)
62325834 ?. (levy used |=(n=@ud (lien vars.fresh |=(p=@ud =(p n))))) ~
6233− `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
5835+ `[[typ.u.out vars.fresh] state.u.out(params params.state, in-mold in-mold.state)]
62345836 =/ out=(unit [typ=itype state=istate])
62355837 (infer-simple-shape sh state(params ~, in-mold &))
62365838 ?~ out ~
6237− ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
62385839 ?: ?=(^ (itype-vars typ.u.out)) ~
6239− `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state, holes holes.state)]
5840+ `[[typ.u.out ~] state.u.out(params params.state, in-mold in-mold.state)]
62405841::
62415842:: A direct imported reference may carry definite reader evidence. Only
62425843:: uniquely supplied, declared inputs are used; unsupported data stay generic.
@@ -6339,12 +5940,10 @@
63395940 |= [sh=shape state=istate]
63405941 ^- (unit [typ=itype state=istate])
63415942 ?- -.sh
6342− %hole `[[%var next.state] state(next +(next.state), holes [[next.state at.sh] holes.state])]
63435943 %aura
63445944 ?: =(0 aura.sh) `[[%any-atom ~] state]
63455945 `[[%atom aura.sh] state]
63465946 %flag `[[%flag ~] state]
6347− %noun `[[%noun ~] state]
63485947 %const
63495948 ?. |(=(%term form.lit.sh) =(%null form.lit.sh)) ~
63505949 `[[%const lit.sh] state]
@@ -6371,7 +5970,7 @@
63715970 =/ found=(unit ischeme) (find-jibb-mold n u.iface)
63725971 ?~ found ~
63735972 ?^ vars.u.found ~
6374− `[(itype-in-import typ.u.found u.iface i.t.names.sh prelude.state) state]
5973+ `[(itype-in-import typ.u.found u.iface i.t.names.sh) state]
63755974 =/ found=(unit itype)
63765975 (find-imported-mold i.t.names.sh n externals.state surs.state)
63775976 ?~ found ~
@@ -6390,13 +5989,10 @@
63905989 ?~ prelude-entry ~
63915990 ?^ vars.u.prelude-entry ~
63925991 `[typ.u.prelude-entry state]
6393− =/ direct=(unit itype) (simple-source-recursive n u.found state)
6394− ?^ direct `[u.direct state]
63955992 =/ out=(unit [typ=itype state=istate])
63965993 $(sh u.found, state state(active [n active.state], in-mold &, params ~))
63975994 ?~ out ~
6398− ?^ (unresolved-hole holes.state.u.out holes.state state.u.out) ~
6399− `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state, holes holes.state)]
5995+ `[(label-direct-union typ.u.out u.found n state) state.u.out(active active.state, in-mold in-mold.state, params params.state)]
64005996 %apply
64015997 ?~ ref.sh ~
64025998 =/ args=(unit [types=(list itype) state=istate]) (infer-shape-args args.sh state)
@@ -6411,7 +6007,7 @@
64116007 ?~ vars.u.template ~
64126008 =/ applied=(unit itype) (template-apply u.template types.u.args)
64136009 ?~ applied ~
6414− `[(itype-in-import u.applied u.iface i.t.ref.sh prelude.state.u.args) state.u.args]
6010+ `[(itype-in-import u.applied u.iface i.t.ref.sh) state.u.args]
64156011 ?: (lien active.state.u.args |=(x=term =(x n))) ~
64166012 =/ found=(unit shape) (find-simple-mold n molds.state.u.args)
64176013 ?~ found
@@ -6430,12 +6026,11 @@
64306026 =/ out=(unit [typ=itype state=istate])
64316027 $(sh body.u.found, state state.u.args(active [n active.state.u.args], in-mold &, params u.params))
64326028 ?~ out ~
6433− ?^ (unresolved-hole holes.state.u.out holes.state.u.args state.u.out) ~
64346029 ?: &(?=(%union -.typ.u.out) !?=(%union -.body.u.found) ?=(~ origin.typ.u.out)) ~
64356030 ?: &(?=(%union -.typ.u.out) ?=(%union -.body.u.found) !(lien top-molds.state.u.args |=(x=term =(x n)))) ~
64366031 =? typ.u.out &(?=(%union -.typ.u.out) ?=(%union -.body.u.found))
64376032 (label-direct-union typ.u.out(args types.u.args) u.found n state.u.args)
6438− `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args, holes holes.state.u.args)]
6033+ `[typ.u.out state.u.out(active active.state.u.args, in-mold in-mold.state.u.args, params params.state.u.args)]
64396034 %tvar
64406035 =/ param=(unit itype) (iparam-lookup name.sh params.state)
64416036 ?^ param `[u.param state]
@@ -6475,12 +6070,12 @@
64756070 ^- isample-result
64766071 ?- -.s
64776072 %bind
6478− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6073+ ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
64796074 [%| "sample shadows a name"]
64806075 =/ t=itype [%var next.state]
64816076 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
64826077 %face
6483− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
6078+ ?: |(?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
64846079 [%| "sample shadows a name"]
64856080 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
64866081 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -6518,8 +6113,8 @@
65186113 [%& [%cell ht typ.p.tail] env.p.tail state.p.tail]
65196114::
65206115:: Local definitions generalize only variables outside their enclosing
6521−:: environment and explicit-capital scope. Recursive gate groups use
6522−:: monomorphic placeholders while their bodies are checked.
6116+:: environment and explicit-capital scope. Single self-recursive gates
6117+:: use a monomorphic placeholder; mutually recursive groups stay unsupported.
65236118::
65246119+$ ilocal-result (each [env=ienv state=istate] idiag)
65256120++ free-env-vars
@@ -6548,7 +6143,6 @@
65486143 |-
65496144 ?~ ds &
65506145 ?: ?=(%mold -.i.ds) $(ds t.ds)
6551− ?: =(name.i.ds %proj) |
65526146 ?. (unique-value-name name.i.ds names) |
65536147 ?: ?=(^ (ienv-lookup name.i.ds env)) |
65546148 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -6572,7 +6166,6 @@
65726166 |-
65736167 ?~ locals &
65746168 =/ n=term name.i.locals
6575− ?: =(n %proj) |
65766169 ?. (unique-value-name n names) |
65776170 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
65786171 ?: (lien marks.state |=(m=term =(n m))) |
@@ -6737,13 +6330,7 @@
67376330 |-
67386331 ?~ ds
67396332 ?~ remaining [%& env state]
6740− ?. progressed
6741− =/ pending=(list def) (flop remaining)
6742− =/ groups=icomponents (graph-components pending (global-value-names pending))
6743− =/ grouped=(unit [rest=(list def) env=ienv state=istate])
6744− (try-local-group pending groups env state)
6745− ?~ grouped [%| ["local definitions need unsupported inference" ~]]
6746− $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
6333+ ?. progressed [%| ["local definitions need unsupported inference" ~]]
67476334 $(ds (flop remaining), remaining ~, progressed |)
67486335 =/ d=def i.ds
67496336 ?> ?=(%value -.d)
@@ -6752,9 +6339,6 @@
67526339 =/ retried=? ?=(%| -.inferred)
67536340 =? inferred retried (infer-recursive-gate d env local-state)
67546341 ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
6755− =. state.p.inferred (default-hole-numbers holes.state.p.inferred holes.state state.p.inferred env !(itype-has-gate (itype-normalize typ.p.inferred sub.state.p.inferred)))
6756− =/ hole=(unit idiag) (unresolved-hole holes.state.p.inferred holes.state state.p.inferred)
6757− ?^ hole [%| u.hole]
67586342 =/ merged=(unit [first=icap second=icap])
67596343 (merged-capitals caps.state.p.inferred sub.state.p.inferred)
67606344 ?^ merged
@@ -6770,28 +6354,7 @@
67706354 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
67716355 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
67726356 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
6773− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
6774−::
6775−:: Try complete cyclic local groups after individual definitions stall.
6776−:: Components with non-gates or unresolved constraints stay unavailable.
6777−::
6778−++ try-local-group
6779− |= [ds=(list def) groups=icomponents env=ienv state=istate]
6780− ^- (unit [rest=(list def) env=ienv state=istate])
6781− ?~ groups ~
6782− =/ names=(list term) i.groups
6783− ?. (gth (lent names) 1) $(groups t.groups)
6784− =/ members=(list def)
6785− (skim ds |=(d=def &(?=(%value -.d) (lien names |=(n=term =(n name.d))))))
6786− ?. =((lent members) (lent names)) $(groups t.groups)
6787− =/ result=ilocal-result (infer-gate-group members env state)
6788− ?: ?=(%| -.result) $(groups t.groups)
6789− =/ rest=(list def)
6790− (skim ds |=(d=def !(lien names |=(n=term =(n name.d)))))
6791− =/ more=(unit [rest=(list def) env=ienv state=istate])
6792− $(ds rest, groups t.groups, env env.p.result, state state.p.result)
6793− ?^ more more
6794− `[rest env.p.result state.p.result]
6357+ $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state), progressed &)
67956358::
67966359:: Read only fields of a known record. Unresolved field constraints and
67976360:: ambiguous repeated faces are outside this fragment. Imported record
@@ -6814,29 +6377,17 @@
68146377 ^- iresult
68156378 =/ reverse=(list term) (flop names)
68166379 ?~ reverse [%| ["empty wing" ~]]
6817− =/ iface=(unit ifile) (find-jibb-interface i.reverse jimports.state)
6380+ =/ scheme=(unit ischeme) (ienv-lookup i.reverse env)
6381+ ?~ scheme [%| ["field access is not supported by partial inference" ~]]
6382+ =/ inst=[typ=itype state=istate] (instantiate-scheme u.scheme state)
68186383 =/ fields=(list term) t.reverse
6819− ?~ fields [%| ["field access is not supported by partial inference" ~]]
6820− =/ scheme=(unit ischeme)
6821− ?~ iface
6822− (ienv-lookup i.reverse env)
6823− (ienv-lookup i.fields values.u.iface)
6824− ?~ scheme
6825− ?^ iface [%| ["module member is not available to partial inference" ~]]
6826− [%| ["field access is not supported by partial inference" ~]]
6827− =/ inst=[typ=itype state=istate]
6828− ?~ iface (instantiate-scheme u.scheme state)
6829− =/ imported=ischeme u.scheme
6830− =. typ.imported (itype-in-import typ.imported u.iface i.reverse prelude.state)
6831− (instantiate-scheme imported state)
6832− =/ remaining=(list term) ?~(iface fields t.fields)
68336384 =/ typ=itype typ.inst
68346385 |-
6835− ?~ remaining [%& typ state.inst]
6836− =/ found=(list itype) (record-fields-named i.remaining typ sub.state.inst)
6386+ ?~ fields [%& typ state.inst]
6387+ =/ found=(list itype) (record-fields-named i.fields typ sub.state.inst)
68376388 ?~ found [%| ["field is not available to partial inference" ~]]
68386389 ?^ t.found [%| ["field name is ambiguous in partial inference" ~]]
6839− $(remaining t.remaining, typ i.found)
6390+ $(fields t.fields, typ i.found)
68406391::
68416392:: Propagate a known union or list through supported loobean, unit and list
68426393:: branches. Empty bodies and groups are transparent; bodies with definitions
@@ -6875,9 +6426,6 @@
68756426 [%| ["branch does not cover both loobeans" ~]]
68766427 =/ subject=iresult (infer-fragment subject.e env state)
68776428 ?: ?=(%| -.subject) subject
6878− =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
6879− ?: ?=(%union -.subject-type)
6880− [%| ["contextual union-pattern branch is not supported by partial inference" ~]]
68816429 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
68826430 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
68836431 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -6891,17 +6439,10 @@
68916439 ?: ?=(%unknown -.fit)
68926440 ?: &(?=(%collection -.expected) =(%list name.expected))
68936441 [%| ["branch list constraint is not supported by partial inference" ~]]
6894− ?: ?=(%flag -.expected) [%| ["branch loobean constraint is not supported by partial inference" ~]]
68956442 [%| ["branch union constraint is not supported by partial inference" ~]]
68966443 ?: ?=(%bad -.fit)
6897− =/ missing=(unit idiag) (missing-union-tag e expected sub.state.p.value context)
6898− ?^ missing [%| u.missing]
6899− =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
6900− ?^ nested [%| u.nested]
69016444 ?: &(?=(%collection -.expected) =(%list name.expected))
69026445 [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
6903− ?: ?=(%flag -.expected)
6904− [%| ["branch arm does not fit its expected loobean" ~[[context "expected loobean"] [(span-of e) "branch arm"]]]]
69056446 [%| ["branch arm does not fit its expected union" ~[[context "expected union"] [(span-of e) "branch arm"]]]]
69066447 [%& expected state.p.value(sub sub.fit, next next.fit)]
69076448::
@@ -6966,37 +6507,23 @@
69666507 [%| ["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)]]]]
69676508 [%& target state.p.tail(sub sub.fit, next next.fit)]
69686509::
6969−++ infer-open-list-items
6970− |= [items=(list expr) expected=itype env=ienv state=istate context=span]
6971− ^- iresult
6972− ?~ items [%& expected state]
6973− =/ target=itype (itype-walk expected sub.state)
6974− =/ value=iresult (infer-call-context-arg i.items target env state context)
6975− ?: ?=(%| -.value) value
6976− =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
6977− ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
6978− ?: ?=(%bad -.fit)
6979− ?: |((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))
6980− [%| ["list item widening is not supported by partial inference" ~]]
6981− [%| ["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)]]]]
6982− ?: (itype-has-tag (itype-normalize expected sub.fit))
6983− [%| ["list item needs context in partial inference" ~]]
6984− $(items t.items, state state.p.value(sub sub.fit, next next.fit))
6985−::
69866510++ infer-list-items
69876511 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
69886512 ^- iresult
69896513 ?~ items [%& expected state]
69906514 =/ target=itype (itype-walk expected sub.state)
6991− =/ value=iresult (infer-call-context-arg i.items target env state context)
6515+ =/ value=iresult
6516+ ?: &(?=(%union -.target) (context-union-branch i.items))
6517+ (infer-union-context i.items target env state context)
6518+ ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch i.items))
6519+ (infer-union-context i.items target env state context)
6520+ ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression i.items))
6521+ (infer-list-context i.items target env state context)
6522+ (infer-fragment i.items env state)
69926523 ?: ?=(%| -.value) value
69936524 =/ fit=ifit (itype-fit typ.p.value target sub.state.p.value next.state.p.value)
69946525 ?: ?=(%unknown -.fit) [%| ["list item constraint is not supported by partial inference" ~]]
69956526 ?: ?=(%bad -.fit)
6996− =/ missing=(unit idiag) (missing-union-tag i.items target sub.state.p.value context)
6997− ?^ missing [%| u.missing]
6998− =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
6999− ?^ nested [%| u.nested]
70006527 [%| ["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)]]]]
70016528 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
70026529::
@@ -7089,7 +6616,7 @@
70896616 [%| ["list branch pattern is not supported by partial inference" ~]]
70906617 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
70916618 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
7092− ?: |(=(head.u.binder %proj) =(tail.u.binder %proj) =(head.u.binder tail.u.binder) ?=(^ (ienv-lookup head.u.binder env)) ?=(^ (ienv-lookup tail.u.binder env)) (lien globals.state |=(n=term |(=(n head.u.binder) =(n tail.u.binder)))))
6619+ ?: |(=(head.u.binder tail.u.binder) ?=(^ (ienv-lookup head.u.binder env)) ?=(^ (ienv-lookup tail.u.binder env)) (lien globals.state |=(n=term |(=(n head.u.binder) =(n tail.u.binder)))))
70936620 [%| ["pattern binder shadows a name" ~]]
70946621 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
70956622 =/ left=iresult
@@ -7126,7 +6653,7 @@
71266653 [%| ["unit branch pattern is not supported by partial inference" ~]]
71276654 =/ binder=(unit term) ?:(first-empty second-name first-name)
71286655 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
7129− ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
6656+ ?: |(?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
71306657 [%| ["pattern binder shadows a name" ~]]
71316658 =/ payload=(unit itype) (unit-union-payload typ)
71326659 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -7168,553 +6695,10 @@
71686695 [%| ["a cell in interpolation needs a printer" ~[[(span-of p.i.ps) "cell without a printer"]]]]
71696696 [%| ["interpolation type needs unsupported inference" ~]]
71706697::
7171−:: Whole-case coverage for a known union. When a pattern may cover only
7172−:: part of a case, finite loobean refinements are tried below; other
7173−:: partial coverage stays unsupported until the general pattern matrix.
7174−+$ imatch ?(%full %none %unknown)
7175−++ union-pattern-items
7176− |= [ps=(list pattern) t=itype]
7177− ^- imatch
7178− ?~ ps %unknown
7179− ?~ t.ps (union-pattern i.ps t)
7180− =. t ?:(?=(%face -.t) body.t t)
7181− ?. ?=(%cell -.t)
7182− ?: |(?=(%atom -.t) ?=(%any-atom -.t) ?=(%flag -.t) ?=(%const -.t)) %none
7183− %unknown
7184− =/ a=imatch (union-pattern i.ps hed.t)
7185− =/ b=imatch $(ps t.ps, t tal.t)
7186− ?: |(=(%none a) =(%none b)) %none
7187− ?:(&(=(%full a) =(%full b)) %full %unknown)
7188−::
7189−++ union-pattern
7190− |= [p=pattern t=itype]
7191− ^- imatch
7192− =. t ?:(?=(%face -.t) body.t t)
7193− ?- -.p
7194− %any %full
7195− %bind %full
7196− %lit
7197− ?: ?=(%const -.t) ?:(=(val.literal.t val.lit.p) %full %none)
7198− ?: ?=(%cell -.t) %none
7199− ?: ?=(%flag -.t)
7200− ?:(|(=(0 val.lit.p) =(1 val.lit.p)) %unknown %none)
7201− %unknown
7202− %str ?:(?=(%cell -.t) %none %unknown)
7203− %cell (union-pattern-items items.p t)
7204− ==
7205−::
7206−++ union-pattern-has-bind
7207− |= p=pattern
7208− ^- ?
7209− ?: ?=(%bind -.p) &
7210− ?. ?=(%cell -.p) |
7211− (lien items.p union-pattern-has-bind)
7212−::
7213−++ union-pattern-bind-items
7214− |= [ps=(list pattern) t=itype env=ienv globals=(list term)]
7215− ^- (unit ienv)
7216− ?~ ps ~
7217− ?~ t.ps (union-pattern-bind i.ps t env globals)
7218− =. t ?:(?=(%face -.t) body.t t)
7219− ?. ?=(%cell -.t) ~
7220− =/ first=(unit ienv) (union-pattern-bind i.ps hed.t env globals)
7221− ?~ first ~
7222− $(ps t.ps, t tal.t, env u.first)
7223−::
7224−++ union-pattern-bind
7225− |= [p=pattern t=itype env=ienv globals=(list term)]
7226− ^- (unit ienv)
7227− =. t ?:(?=(%face -.t) body.t t)
7228− ?: ?=(%bind -.p)
7229− ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
7230− `[[name.p [t ~]] env]
7231− ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
7232− `env
7233−::
7234−:: Split loobean fields into finite refinements for partial patterns.
7235−:: Keep original cases for binder types and preserve whole-case matching
7236−:: before trying refinements. Cap products at 64; unknown, empty or opaque
7237−:: shapes stay unsupported rather than implying complete pattern checking.
7238−+$ ifinite [origin=@ud base=itype part=itype]
7239−++ finite-product
7240− |= [hs=(list itype) ts=(list itype) out=(list itype)]
7241− ^- (list itype)
7242− ?~ hs out
7243− =/ rows=(list itype) (turn ts |=(t=itype [%cell i.hs t]))
7244− $(hs t.hs, out (weld rows out))
7245−::
7246−++ finite-type
7247− |= t=itype
7248− ^- (unit (list itype))
7249− ?- -.t
7250− %flag
7251− `~[[%const [%loobean %f 0 '%.y']] [%const [%loobean %f 1 '%.n']]]
7252− %face
7253− =/ body=(unit (list itype)) $(t body.t)
7254− ?~ body ~
7255− `(turn u.body |=(x=itype [%face name.t x]))
7256− %cell
7257− =/ hed=(unit (list itype)) $(t hed.t)
7258− ?~ hed ~
7259− =/ tal=(unit (list itype)) $(t tal.t)
7260− ?~ tal ~
7261− ?: (gth (mul (lent u.hed) (lent u.tal)) 64) ~
7262− `(finite-product u.hed u.tal ~)
7263− * `~[t]
7264− ==
7265−::
7266−++ finite-cases
7267− |= [xs=(list itype) out=(list ifinite) origin=@ud]
7268− ^- (unit (list ifinite))
7269− ?~ xs `out
7270− =/ parts=(unit (list itype)) (finite-type i.xs)
7271− ?~ parts ~
7272− ?: (gth (add (lent out) (lent u.parts)) 64) ~
7273− =/ rows=(list ifinite) (turn u.parts |=(t=itype [origin i.xs t]))
7274− $(xs t.xs, out (weld out rows), origin +(origin))
7275−::
7276−++ infer-known-union-whole
7277− |= [e=expr env=ienv subject=iresult]
7278− ^- (unit iresult)
7279− ?> ?=(%branch -.e)
7280− ?: ?=(%| -.subject) `subject
7281− =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7282− ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7283− =/ cases=(list itype) cases.typ
7284− =/ remaining=(list itype) cases
7285− =/ arms=(list arm) arms.e
7286− =/ st=istate state.p.subject
7287− =/ answer=(unit itype) ~
7288− |-
7289− ?~ arms
7290− ?^ remaining
7291− `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7292− ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7293− `[%& u.answer st]
7294− =/ a=arm i.arms
7295− ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7296− ~
7297− =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
7298− ?~ matching
7299− ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
7300− `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7301− `[%| ["union pattern is not supported by partial inference" ~]]
7302− ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
7303− `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7304− =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7305− ?~ bound `[%| ["pattern binder shadows a name" ~]]
7306− =/ body=iresult (infer-fragment val.a u.bound st)
7307− ?: ?=(%| -.body) `body
7308− =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7309− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7310− ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
7311− $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
7312−::
7313−++ infer-known-union-context-whole
7314− |= [e=expr expected=itype env=ienv subject=iresult context=span]
7315− ^- (unit iresult)
7316− ?> ?=(%branch -.e)
7317− ?: ?=(%| -.subject) `subject
7318− =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7319− ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
7320− =/ cases=(list itype) cases.typ
7321− =/ remaining=(list itype) cases
7322− =/ arms=(list arm) arms.e
7323− =/ st=istate state.p.subject
7324− =/ answer=(unit itype) ~
7325− |-
7326− ?~ arms
7327− ?^ remaining
7328− `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
7329− ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
7330− `[%& expected st]
7331− =/ a=arm i.arms
7332− ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
7333− ~
7334− =/ matching=(list itype) (skim remaining |=(c=itype =(%full (union-pattern pat.a c))))
7335− ?~ matching
7336− ?: (lien cases |=(c=itype =(%full (union-pattern pat.a c))))
7337− `[%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7338− `[%| ["union pattern is not supported by partial inference" ~]]
7339− ?: &(?=(^ t.matching) (union-pattern-has-bind pat.a))
7340− `[%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7341− =/ bound=(unit ienv) (union-pattern-bind pat.a i.matching env globals.st)
7342− ?~ bound `[%| ["pattern binder shadows a name" ~]]
7343− =/ body=iresult (infer-call-context-arg val.a expected u.bound st context)
7344− ?: ?=(%| -.body) `body
7345− =/ fit=ifit (itype-fit typ.p.body expected sub.state.p.body next.state.p.body)
7346− ?: ?=(%unknown -.fit) `[%| ["union branch result constraint is not supported by partial inference" ~]]
7347− ?: ?=(%bad -.fit)
7348− =/ missing=(unit idiag) (missing-union-tag val.a expected sub.state.p.body context)
7349− ?^ missing `[%| u.missing]
7350− =/ nested=(unit idiag) (nested-missing-tag val.a typ.p.body expected sub.state.p.body next.state.p.body context)
7351− ?^ nested `[%| u.nested]
7352− `[%| ["union branch arm does not fit its expected type" ~[[context "expected type"] [(span-of val.a) "branch arm"]]]]
7353− ?: (itype-has-tag (itype-normalize expected sub.fit))
7354− `[%| ["union branch result needs context in partial inference" ~]]
7355− $(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)
7356−::
7357−++ infer-known-union-finite
7358− |= [e=expr env=ienv subject=iresult expected=(unit [typ=itype context=span])]
7359− ^- iresult
7360− ?> ?=(%branch -.e)
7361− ?: ?=(%| -.subject) subject
7362− =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7363− ?. ?=(%union -.typ) [%| ["branch is not supported by partial inference" ~]]
7364− =/ expanded=(unit (list ifinite)) (finite-cases cases.typ ~ 0)
7365− ?~ expanded [%| ["union pattern expansion needs unsupported inference" ~]]
7366− =/ cases=(list ifinite) u.expanded
7367− =/ remaining=(list ifinite) cases
7368− =/ arms=(list arm) arms.e
7369− =/ st=istate state.p.subject
7370− =/ answer=(unit itype) ~
7371− |-
7372− ?~ arms
7373− ?^ remaining
7374− [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
7375− ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
7376− ?~ expected [%& u.answer st]
7377− [%& typ.u.expected st]
7378− =/ a=arm i.arms
7379− ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
7380− [%| ["partial union pattern is not supported by partial inference" ~]]
7381− =/ matching=(list ifinite) (skim remaining |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7382− ?~ matching
7383− ?: (lien cases |=(c=ifinite =(%full (union-pattern pat.a part.c))))
7384− [%| ["branch arm is covered by earlier arms" ~[[at.pat.a "covered arm"]]]]
7385− [%| ["union pattern is not supported by partial inference" ~]]
7386− ?: &((union-pattern-has-bind pat.a) (lien t.matching |=(c=ifinite !=(origin.c origin.i.matching))))
7387− [%| ["a union pattern binding several cases is not supported by partial inference" ~]]
7388− =/ bound=(unit ienv) (union-pattern-bind pat.a base.i.matching env globals.st)
7389− ?~ bound [%| ["pattern binder shadows a name" ~]]
7390− =/ body=iresult
7391− ?~ expected (infer-fragment val.a u.bound st)
7392− (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7393− ?: ?=(%| -.body) body
7394− ?^ expected
7395− =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7396− ?: ?=(%unknown -.fit) [%| ["union branch result constraint is not supported by partial inference" ~]]
7397− ?: ?=(%bad -.fit)
7398− =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7399− ?^ missing [%| u.missing]
7400− =/ 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)
7401− ?^ nested [%| u.nested]
7402− [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7403− ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7404− [%| ["union branch result needs context in partial inference" ~]]
7405− $(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)
7406− =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
7407− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
7408− ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
7409− $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
7410−::
7411−:: Prove a one-arm record pattern covers a known, non-union subject.
7412−:: Variable or partial matches stay unsupported; binding uses the same
7413−:: scope and original payload types as the existing union matcher.
7414−++ single-structured-pattern
7415− |= e=expr
7416− ^- ?
7417− ?. ?=(%branch -.e) |
7418− ?~ arms.e |
7419− ?^ t.arms.e |
7420− =/ p=pattern pat.i.arms.e
7421− ?. ?=(%cell -.p) |
7422− !(levy items.p |=(x=pattern ?=(%bind -.x)))
7423−::
7424−++ infer-single-case-branch
7425− |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
7426− ^- iresult
7427− ?> (single-structured-pattern e)
7428− ?> ?=(%branch -.e)
7429− ?> ?=(^ arms.e)
7430− =/ a=arm i.arms.e
7431− =/ subject=iresult (infer-fragment subject.e env state)
7432− ?: ?=(%| -.subject) subject
7433− =/ st=istate state.p.subject
7434− =/ typ=itype (itype-normalize typ.p.subject sub.st)
7435− ?: ?=(%union -.typ) [%| ["single-case pattern needs unsupported inference" ~]]
7436− ?. =(%full (union-pattern pat.a typ))
7437− [%| ["single-case pattern needs unsupported inference" ~]]
7438− =/ bound=(unit ienv) (union-pattern-bind pat.a typ env globals.st)
7439− ?~ bound [%| ["pattern binder shadows a name" ~]]
7440− ?~ expected (infer-fragment val.a u.bound st)
7441− =/ body=iresult (infer-call-context-arg val.a typ.u.expected u.bound st context.u.expected)
7442− ?: ?=(%| -.body) body
7443− =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
7444− ?: ?=(%unknown -.fit) [%| ["single-case branch result constraint is not supported by partial inference" ~]]
7445− ?: ?=(%bad -.fit)
7446− =/ missing=(unit idiag) (missing-union-tag val.a typ.u.expected sub.state.p.body context.u.expected)
7447− ?^ missing [%| u.missing]
7448− =/ 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)
7449− ?^ nested [%| u.nested]
7450− [%| ["single-case branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
7451− ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
7452− [%| ["single-case branch result needs context in partial inference" ~]]
7453− [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
7454−::
7455−:: This view is used only by pattern analysis, never exported or bound as
7456−:: the subject. Only null plus a two-binder/wildcard cell is supported; its
7457−:: tail keeps the original recursive type. Other patterns fail closed.
7458−++ jrec-match-view
7459− |= [e=expr subject=iresult]
7460− ^- iresult
7461− ?: ?=(%| -.subject) subject
7462− ?. ?=(%branch -.e) subject
7463− =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7464− ?. ?=(%jrec -.typ) subject
7465− ?~ arms.e subject
7466− ?~ t.arms.e subject
7467− ?^ t.t.arms.e subject
7468− =/ x=pattern pat.i.arms.e
7469− =/ y=pattern pat.i.t.arms.e
7470− =/ empty=? &(?=(%lit -.x) =(%null form.lit.x))
7471− =/ full=pattern ?:(empty y x)
7472− ?. |(empty &(?=(%lit -.y) =(%null form.lit.y))) subject
7473− ?. ?=(%cell -.full) subject
7474− ?~ items.full subject
7475− ?~ t.items.full subject
7476− ?^ t.t.items.full subject
7477− ?. |(?=(%bind -.i.items.full) ?=(%any -.i.items.full)) subject
7478− ?. |(?=(%bind -.i.t.items.full) ?=(%any -.i.t.items.full)) subject
7479− ?: =(0 jrec-fuel.state.p.subject)
7480− [%| ["recursive mold unfolding needs unsupported inference" ~]]
7481− =/ nil=itype [%const [%null %n 0 '~']]
7482− =/ cell=itype [%cell [%face head.typ [%atom aura.typ]] [%face tail.typ typ]]
7483− [%& [%union ~[nil cell] ~ ~ ~] state.p.subject(jrec-fuel (dec jrec-fuel.state.p.subject))]
7484−::
7485−++ infer-known-union-branch-subject
7486− |= [e=expr env=ienv subject=iresult]
7487− ^- iresult
7488− =. subject (jrec-match-view e subject)
7489− =/ whole=(unit iresult) (infer-known-union-whole e env subject)
7490− ?~ whole (infer-known-union-finite e env subject ~)
7491− u.whole
7492−::
7493−++ infer-known-union-branch
7494− |= [e=expr env=ienv state=istate]
7495− ^- iresult
7496− ?> ?=(%branch -.e)
7497− (infer-known-union-branch-subject e env (infer-fragment subject.e env state))
7498−::
7499−++ infer-known-union-context-subject
7500− |= [e=expr expected=itype env=ienv subject=iresult context=span]
7501− ^- iresult
7502− =. subject (jrec-match-view e subject)
7503− =/ whole=(unit iresult) (infer-known-union-context-whole e expected env subject context)
7504− ?~ whole (infer-known-union-finite e env subject `[expected context])
7505− u.whole
7506−::
7507−:: Limit speculative subject inference to wings and shallow calls;
7508−:: grouping is peeled linearly and cannot introduce a nested branch.
7509−++ simple-union-subject-arg
7510− |= e=expr
7511− ^- ?
7512− ?- -.e
7513− %wing &
7514− %lit &
7515− %str !(lien pieces.e |=(p=piece ?=(%expr -.p)))
7516− * |
7517− ==
7518−::
7519−++ safe-union-subject
7520− |= e=expr
7521− ^- ?
7522− ?: ?=(%group -.e) $(e inner.e)
7523− ?: ?=(%wing -.e) &
7524− ?. ?=(%call -.e) |
7525− ?. ?=(%wing -.head.e) |
7526− (levy args.e simple-union-subject-arg)
7527−::
7528−++ duplicate-loobean-arms
7529− |= e=expr
7530− ^- ?
7531− ?. ?=(%branch -.e) |
7532− ?~ arms.e |
7533− ?~ t.arms.e |
7534− ?^ t.t.arms.e |
7535− =/ x=pattern pat.i.arms.e
7536− =/ y=pattern pat.i.t.arms.e
7537− ?. &(?=(%lit -.x) ?=(%lit -.y)) |
7538− ?. &(=(%loobean form.lit.x) =(%loobean form.lit.y)) |
7539− =(val.lit.x val.lit.y)
7540−::
7541−++ union-subject-call
7542− |= e=expr
7543− ^- ?
7544− ?: ?=(%group -.e) $(e inner.e)
7545− ?=(%call -.e)
7546−::
7547−++ known-union-subject
7548− |= [e=expr env=ienv state=istate]
7549− ^- (unit iresult)
7550− ?. (safe-union-subject e) ~
7551− =/ subject=iresult (infer-fragment e env state)
7552− ?: ?=(%| -.subject) ?:((union-subject-call e) `subject ~)
7553− =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
7554− ?. |(?=(%union -.typ) ?=(%jrec -.typ)) ~
7555− `subject
7556−::
7557−::
7558−:: Infer changes only against a fully known record spine. Retain the
7559−:: target type; unknown spines and repeated edits remain unsupported.
7560−++ change-spine-known
7561− |= [t=itype sub=isub]
7562− ^- ?
7563− =. t (itype-walk t sub)
7564− ?: ?=(%face -.t) &
7565− ?. ?=(%cell -.t) |
7566− =/ first=itype (itype-walk hed.t sub)
7567− ?. ?=(%face -.first) |
7568− $(t tal.t)
7569−::
7570−++ infer-change-edits
7571− |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
7572− ^- iresult
7573− ?~ edits [%& target state]
7574− =/ entry=edit i.edits
7575− ?: (lien seen |=(name=term =(name name.entry)))
7576− [%| ["repeated change fields are not supported by partial inference" ~]]
7577− ?. (change-spine-known target sub.state)
7578− [%| ["change target needs a known record in partial inference" ~]]
7579− =/ found=(list itype) (record-fields-named name.entry target sub.state)
7580− ?~ found
7581− [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
7582− ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
7583− =/ expected=itype i.found
7584− =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
7585− ?: ?=(%| -.value) value
7586− =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
7587− ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
7588− ?: ?=(%bad -.fit)
7589− [%| ["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)]]]]
7590− $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
7591−::
7592−:: Backtick constructs the canonical prelude unit, after checking its
7593−:: prepared template has the standard null and [~ u=A] cases.
7594−++ standard-unit-template
7595− |= [template=ischeme at=path]
7596− ^- ?
7597− ?. =(at /lib/jibb/prelude/jibb) |
7598− ?~ vars.template |
7599− ?^ t.vars.template |
7600− =/ v=@ud i.vars.template
7601− =/ nil=itype [%const [%null %n 0 '~']]
7602− =/ expected=itype
7603− [%union ~[nil [%cell nil [%face %u [%var v]]]] `[at %unit] `%unit ~[[%var v]]]
7604− =(typ.template expected)
7605−::
7606−:: A named missing-case diagnostic needs more than a failed fit: a case
7607−:: with that tag but the wrong payload is not a missing case. Unknown
7608−:: shapes and atom types that accept terms keep the proof conservative.
7609−+$ itag-presence ?(%yes %no %maybe)
7610−++ tag-presence-cases
7611− |= [cases=(list itype) value=@ sub=isub]
7612− ^- itag-presence
7613− ?~ cases %no
7614− =/ first=itag-presence (tag-presence i.cases value sub)
7615− ?: =(%yes first) %yes
7616− =/ rest=itag-presence $(cases t.cases)
7617− ?: =(%yes rest) %yes
7618− ?: |(=(%maybe first) =(%maybe rest)) %maybe
7619− %no
7620−::
7621−++ tag-presence
7622− |= [t=itype value=@ sub=isub]
7623− ^- itag-presence
7624− =. t (itype-walk t sub)
7625− ?- -.t
7626− %const ?:(=(value val.literal.t) %yes %no)
7627− %flag ?:(|(=(value 0) =(value 1)) %yes %no)
7628− %atom ?:(|(=(%tas aura.t) =(%ta aura.t)) %maybe %no)
7629− %face $(t body.t)
7630− %cell
7631− =/ first=itag-presence $(t hed.t)
7632− ?: =(%yes first) %yes
7633− =/ rest=itag-presence $(t tal.t)
7634− ?: =(%yes rest) %yes
7635− ?: |(=(%maybe first) =(%maybe rest)) %maybe
7636− %no
7637− %union (tag-presence-cases cases.t value sub)
7638− * %maybe
7639− ==
7640−::
7641−++ missing-union-tag
7642− |= [e=expr expected=itype sub=isub context=span]
7643− ^- (unit idiag)
7644− ?. ?=(%lit -.e) ~
7645− ?. =(%term form.lit.e) ~
7646− =. expected (itype-walk expected sub)
7647− |-
7648− ?: ?=(%face -.expected) $(expected (itype-walk body.expected sub))
7649− ?. ?=(%union -.expected) ~
7650− ?. =(%no (tag-presence-cases cases.expected val.lit.e sub)) ~
7651− =/ label=tape
7652− ?~ label.expected "union {(show-itype expected sub)}"
7653− (show-itype expected sub)
7654− `["{label} has no case `{(trip txt.lit.e)}`" ~[[context "expected union"] [(span-of e) "tag"]]]
7655−::
7656−:: Locate a missing tag inside a syntactic tuple only by replaying the
7657−:: directional fit in source order. Uncertain or earlier failures stop
7658−:: the walk, preserving the generic diagnostic rather than guessing.
7659−++ nested-missing-tag
7660− |= [e=expr actual=itype expected=itype sub=isub next=@ud context=span]
7661− ^- (unit idiag)
7662− =/ original=[left=itype right=itype] [actual expected]
7663− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7664− =/ fit=ifit (itype-fit actual expected sub next)
7665− ?. ?=(%bad -.fit) ~
7666− =. actual (itype-walk actual sub)
7667− =. expected (itype-walk expected sub)
7668− ?: &(?=(%face -.actual) ?=(%face -.expected))
7669− ?. =(name.actual name.expected) ~
7670− $(actual body.actual, expected body.expected)
7671− ?: ?=(%face -.actual) $(actual body.actual)
7672− ?: ?=(%face -.expected) $(expected body.expected)
7673− =/ direct=(unit idiag) (missing-union-tag e expected sub context)
7674− ?^ direct direct
7675− ?. ?=(%tuple -.e) ~
7676− (nested-missing-items items.e actual expected sub next context)
7677−::
7678−++ nested-missing-items
7679− |= [items=(list item) actual=itype expected=itype sub=isub next=@ud context=span]
7680− ^- (unit idiag)
7681− ?~ items ~
7682− ?~ t.items (nested-missing-tag val.i.items actual expected sub next context)
7683− =/ original=[left=itype right=itype] [actual expected]
7684− ?: |(?=(%var -.left.original) ?=(%avar -.left.original) ?=(%nvar -.left.original) ?=(%var -.right.original) ?=(%avar -.right.original) ?=(%nvar -.right.original)) ~
7685− =. actual (itype-walk actual sub)
7686− =. expected (itype-walk expected sub)
7687− ?. &(?=(%cell -.actual) ?=(%cell -.expected)) ~
7688− =/ first=ifit (itype-fit hed.actual hed.expected sub next)
7689− ?: ?=(%bad -.first)
7690− (nested-missing-tag val.i.items hed.actual hed.expected sub next context)
7691− ?. ?=(%ok -.first) ~
7692− $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
7693−::
7694−:: A term-headed pair is the same noun as a two-item cell. Preserve the
7695−:: whole pair span for the synthetic head and the value's own span for
7696−:: the payload; unresolved term constraints follow ordinary cell inference.
7697−++ pair-as-cell
7698− |= e=expr
7699− ^- expr
7700− ?> ?=(%pair -.e)
7701− =/ head=expr [%lit at.e [%term %tas tag.e (crip ['%' (trip tag.e)])]]
7702− [%tuple at.e ~[[at.e ~ head] [(span-of val.e) ~ val.e]]]
7703−::
7704−:: A segment costs one shared step; dynamic segments are not handled yet.
7705−++ qath-static-fuel
7706− |= [segs=(list qseg) fuel=@ud]
7707− ^- (unit @ud)
7708− ?~ segs `fuel
7709− ?: =(0 fuel) ~
7710− ?. ?=(%knot -.i.segs) ~
7711− $(segs t.segs, fuel (dec fuel))
7712−::
77136698++ infer-fragment
77146699 |= [e=expr env=ienv state=istate]
77156700 ^- iresult
77166701 ?- -.e
7717− %pair $(e (pair-as-cell e))
77186702 %lit
77196703 ?- form.lit.e
77206704 %number ?: =(%ud aura.lit.e)
@@ -7728,45 +6712,7 @@
77286712 %term [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
77296713 %null [%& [%tag next.state lit.e |] state(next +(next.state), tags [[next.state lit.e] tags.state])]
77306714 ==
7731− %unit
7732− ?~ prelude.state [%| ["unit construction needs the standard prelude in partial inference" ~]]
7733− =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
7734− ?~ standard [%| ["unit construction needs the standard prelude in partial inference" ~]]
7735− ?. (standard-unit-template u.standard at.u.prelude.state)
7736− [%| ["unit construction needs the standard prelude in partial inference" ~]]
7737− =/ value=iresult $(e val.e)
7738− ?: ?=(%| -.value) value
7739− =/ result=(unit itype) (template-apply u.standard ~[typ.p.value])
7740− ?~ result [%| ["unit construction is not supported by partial inference" ~]]
7741− [%& u.result state.p.value]
7742− %list
7743− ?~ prelude.state [%| ["list literal needs the standard prelude in partial inference" ~]]
7744− ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7745− [%| ["list literal needs the standard prelude in partial inference" ~]]
7746− =/ standard=(unit ischeme) (find-jibb-mold %list u.prelude.state)
7747− ?~ standard [%| ["list literal needs the standard prelude in partial inference" ~]]
7748− ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
7749− [%| ["list literal needs the standard prelude in partial inference" ~]]
7750− =/ element=itype [%var next.state]
7751− =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
7752− ?: ?=(%| -.result) result
7753− [%& [%collection %list ~[element]] state.p.result]
77546715 %str (infer-string-pieces pieces.e env state)
7755− %qath
7756− ?~ prelude.state [%| ["application path needs the standard prelude in partial inference" ~]]
7757− ?. =(at.u.prelude.state /lib/jibb/prelude/jibb)
7758− [%| ["application path needs the standard prelude in partial inference" ~]]
7759− =/ standard=(unit ischeme) (find-jibb-mold %qath u.prelude.state)
7760− ?~ standard [%| ["application path needs the standard prelude in partial inference" ~]]
7761− ?. ?=(~ vars.u.standard) [%| ["application path mold needs unsupported inference" ~]]
7762− =/ typ=itype typ.u.standard
7763− ?. ?=(%jrec -.typ) [%| ["application path mold needs unsupported inference" ~]]
7764− ?. &(=(at.typ /lib/jibb/internal/jibb) =(%qath name.typ) =(%i head.typ) =(%ta aura.typ) =(%t tail.typ))
7765− [%| ["application path mold needs unsupported inference" ~]]
7766− ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
7767− =/ remain=(unit @ud) (qath-static-fuel segs.e (dec jrec-fuel.state))
7768− ?~ remain [%| ["application path segments need unsupported inference" ~]]
7769− [%& typ state(jrec-fuel u.remain)]
77706716 %wing
77716717 ?~ names.e [%| ["empty wing" ~]]
77726718 ?^ t.names.e
@@ -7775,7 +6721,7 @@
77756721 ?~ iface (infer-field-wing names.e env state)
77766722 =/ member=(unit ischeme) (ienv-lookup i.names.e values.u.iface)
77776723 ?~ member [%| ["module member is not available to partial inference" ~]]
7778− =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e prelude.state)
6724+ =. typ.u.member (itype-in-import typ.u.member u.iface i.t.names.e)
77796725 =/ instance=[typ=itype state=istate] (instantiate-scheme u.member state)
77806726 [%& typ.instance state.instance]
77816727 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
@@ -7788,11 +6734,6 @@
77886734 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
77896735 [%& typ.instance state.instance]
77906736 %group $(e inner.e)
7791− %change
7792− ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
7793− =/ target=iresult $(e [%wing at.e target.e])
7794− ?: ?=(%| -.target) target
7795− (infer-change-edits edits.e typ.p.target env state.p.target ~)
77966737 %ctor [%& [%tag next.state tag.e &] state(next +(next.state), tags [[next.state tag.e] tags.state])]
77976738 %trace
77986739 =/ traced=iresult $(e val.e)
@@ -7809,9 +6750,6 @@
78096750 [%| ["local molds shadow a name" ~]]
78106751 =/ local-state=istate
78116752 state(globals (weld local-names globals.state), molds (weld local-molds molds.state))
7812− =/ mold-hole=(unit span) (simple-local-mold-hole defs.e)
7813− ?^ mold-hole
7814− [%| ["type hole needs a determined type" ~[[u.mold-hole "unresolved type hole"]]]]
78156753 ?. (local-molds-supported local-molds local-state)
78166754 [%| ["local molds need unsupported inference" ~]]
78176755 =/ values=(list def) (local-value-defs defs.e)
@@ -7822,30 +6760,20 @@
78226760 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
78236761 %branch
78246762 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
7825− ?~ t.arms.e
7826− ?: (single-structured-pattern e) (infer-single-case-branch e env state ~)
7827− (infer-cell-branch e env state ~)
7828− ?^ t.t.arms.e (infer-known-union-branch e env state)
7829− =/ known=(unit iresult) (known-union-subject subject.e env state)
7830− ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
7831− ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
7832− (infer-known-union-branch-subject e env u.known)
6763+ ?~ t.arms.e (infer-cell-branch e env state)
6764+ ?^ t.t.arms.e [%| ["branch is not supported by partial inference" ~]]
78336765 =/ x=arm i.arms.e
78346766 =/ y=arm i.t.arms.e
78356767 ?: |((unit-empty-pattern pat.x) (unit-empty-pattern pat.y))
78366768 (infer-unit-branch e env state ~)
7837− ?. ?=(%lit -.pat.x) (infer-known-union-branch e env state)
7838− ?. ?=(%lit -.pat.y) (infer-known-union-branch e env state)
6769+ ?. ?=(%lit -.pat.x) [%| ["branch pattern is not supported by partial inference" ~]]
6770+ ?. ?=(%lit -.pat.y) [%| ["branch pattern is not supported by partial inference" ~]]
78396771 ?. &(=(%loobean form.lit.pat.x) =(%loobean form.lit.pat.y))
7840− (infer-known-union-branch e env state)
7841− ?: &(?=(^ known) ?=(%& -.u.known)) (infer-known-union-branch-subject e env u.known)
6772+ [%| ["branch pattern is not supported by partial inference" ~]]
78426773 ?: =(val.lit.pat.x val.lit.pat.y)
78436774 [%| ["branch does not cover both loobeans" ~]]
78446775 =/ subject=iresult $(e subject.e)
78456776 ?: ?=(%| -.subject) subject
7846− =/ subject-type=itype (itype-normalize typ.p.subject sub.state.p.subject)
7847− ?: ?=(%union -.subject-type)
7848− [%| ["union-pattern branch subject is not supported by partial inference" ~]]
78496777 =/ su=(unit isub) (itype-unify typ.p.subject [%flag ~] sub.state.p.subject)
78506778 ?~ su [%| ["loobean branch subject does not unify with ?" ~]]
78516779 =/ left=iresult $(e val.x, state state.p.subject(sub u.su))
@@ -7877,18 +6805,17 @@
78776805 ?^ diag [%| u.diag]
78786806 [%| ["cast mold is not supported by partial inference" ~]]
78796807 =/ value=iresult
7880− (infer-call-context-arg val.e typ.u.target env state.u.target at.shape.e)
6808+ ?: &(?=(%union -.typ.u.target) (context-union-branch val.e))
6809+ (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6810+ ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-union-branch val.e))
6811+ (infer-union-context val.e typ.u.target env state.u.target at.shape.e)
6812+ ?: &(?=(%collection -.typ.u.target) =(%list name.typ.u.target) (context-list-expression val.e))
6813+ (infer-list-context val.e typ.u.target env state.u.target at.shape.e)
6814+ $(e val.e, state state.u.target)
78816815 ?: ?=(%| -.value) value
7882− =/ shape=(unit [source=iwfields target=iwfields])
7883− (width-shape typ.p.value typ.u.target sub.state.p.value)
7884− ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
78856816 =/ fit=ifit (itype-fit typ.p.value typ.u.target sub.state.p.value next.state.p.value)
78866817 ?: ?=(%unknown -.fit) [%| ["cast constraint is not supported by partial inference" ~]]
78876818 ?: ?=(%bad -.fit)
7888− =/ missing=(unit idiag) (missing-union-tag val.e typ.u.target sub.state.p.value at.shape.e)
7889− ?^ missing [%| u.missing]
7890− =/ 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)
7891− ?^ nested [%| u.nested]
78926819 [%| ["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)]]]]
78936820 =/ merged=itype (itype-merge-faces typ.p.value typ.u.target sub.fit)
78946821 [%& merged state.p.value(sub sub.fit, next next.fit)]
@@ -7913,9 +6840,43 @@
79136840 [%& [%fn typ.p.sam typ.p.body] state.p.body]
79146841 %call
79156842 ?~ args.e [%| ["call has no argument" ~]]
7916− ?: (explicit-proj-call e env state)
7917− [%| ["proj needs an expected record type" ~]]
7918− (infer-call-with-head e env state (infer-fragment head.e env state))
6843+ =/ head=iresult $(e head.e)
6844+ ?: ?=(%| -.head) head
6845+ =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
6846+ =/ arg=iresult
6847+ ?^ t.args.e
6848+ ?: ?=(%fn -.head-type)
6849+ (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
6850+ (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
6851+ ?: &(?=(%fn -.head-type) ?=(%union -.sample.head-type) (context-union-branch i.args.e))
6852+ (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6853+ ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-union-branch i.args.e))
6854+ (infer-union-context i.args.e sample.head-type env state.p.head (span-of head.e))
6855+ ?: &(?=(%fn -.head-type) ?=(%collection -.sample.head-type) =(%list name.sample.head-type) (context-list-expression i.args.e))
6856+ (infer-list-context i.args.e sample.head-type env state.p.head (span-of head.e))
6857+ $(e i.args.e, state state.p.head)
6858+ ?: ?=(%| -.arg) arg
6859+ =/ st=istate state.p.arg
6860+ =/ ht=itype (itype-walk typ.p.head sub.st)
6861+ ?: ?=(%fn -.ht)
6862+ =/ fit=ifit (itype-fit typ.p.arg sample.ht sub.st next.st)
6863+ ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
6864+ ?: ?=(%bad -.fit)
6865+ =/ bad=(unit [at=span typ=itype])
6866+ ?~(t.args.e ~ (call-error-site args.e typ.p.arg sample.ht sub.st next.st))
6867+ =/ whole-args=span
6868+ ?~(t.args.e (span-of i.args.e) [beg:(span-of i.args.e) end:(span-of (rear args.e))])
6869+ =/ arg-at=span ?~(bad whole-args at.u.bad)
6870+ =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
6871+ [%| ["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)]]]]
6872+ ?: &((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))
6873+ [%| ["call result face propagation is not supported by partial inference" ~]]
6874+ [%& product.ht st(sub sub.fit, next next.fit)]
6875+ =/ result=itype [%var next.st]
6876+ =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
6877+ ?~ uni
6878+ [%| ["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)]]]]
6879+ [%& result st(next +(next.st), sub u.uni)]
79196880 * [%| ["expression is not supported by partial inference" ~]]
79206881 ==
79216882::
@@ -7923,72 +6884,6 @@
79236884:: failed. If an intermediate fit is uncertain, retain the whole argument
79246885:: span rather than assigning blame to a particular argument.
79256886::
7926−:: Check a call using the head already inferred in this state. Keeping
7927−:: this shared avoids evaluating or instantiating a contextual head twice.
7928−++ width-has-projections
7929− |= ps=(list iwprojection)
7930− ^- ?
7931− ?~ ps |
7932− &
7933−::
7934−+$ iwidth-elaboration [original=expr typ=itype sub=isub projections=(list iwprojection)]
7935−++ infer-width-elaboration
7936− |= [e=expr env=ienv state=istate]
7937− ^- (each iwidth-elaboration idiag)
7938− =/ out=iresult (infer-fragment e env state)
7939− ?: ?=(%| -.out) [%| p.out]
7940− [%& [e typ.p.out sub.state.p.out (flop projections.state.p.out)]]
7941−::
7942−++ infer-call-with-head
7943− |= [e=expr env=ienv state=istate head=iresult]
7944− ^- iresult
7945− ?> ?=(%call -.e)
7946− ?~ args.e [%| ["call has no argument" ~]]
7947− ?: ?=(%| -.head) head
7948− =/ head-type=itype (itype-walk typ.p.head sub.state.p.head)
7949− =/ arg=iresult
7950− ?^ t.args.e
7951− ?: ?=(%fn -.head-type)
7952− (infer-call-context-args args.e sample.head-type env state.p.head (span-of head.e))
7953− (infer-simple-items (turn args.e |=(a=expr [(span-of a) ~ a])) env state.p.head)
7954− ?: ?=(%fn -.head-type)
7955− (infer-call-context-arg i.args.e sample.head-type env state.p.head (span-of head.e))
7956− (infer-fragment i.args.e env state.p.head)
7957− ?: ?=(%| -.arg) arg
7958− =/ st=istate state.p.arg
7959− =/ ht=itype (itype-walk typ.p.head sub.st)
7960− ?: ?=(%fn -.ht)
7961− =/ shape=(unit [source=iwfields target=iwfields])
7962− ?^ t.args.e ~
7963− (width-shape typ.p.arg sample.ht sub.st)
7964− ?^ shape [%| ["record width constraint needs unsupported inference" ~]]
7965− =/ fit=ifit
7966− ?^ t.args.e (itype-fit-inner typ.p.arg sample.ht sub.st next.st & |)
7967− (itype-fit typ.p.arg sample.ht sub.st next.st)
7968− ?: ?=(%unknown -.fit) [%| ["call constraint is not supported by partial inference" ~]]
7969− ?: ?=(%bad -.fit)
7970− ?~ t.args.e
7971− =/ missing=(unit idiag) (missing-union-tag i.args.e sample.ht sub.st (span-of head.e))
7972− ?^ missing [%| u.missing]
7973− =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
7974− ?^ nested [%| u.nested]
7975− [%| ["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)]]]]
7976− =/ bad=(unit [at=span typ=itype])
7977− (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
7978− =/ whole-args=span
7979− [beg:(span-of i.args.e) end:(span-of (rear args.e))]
7980− =/ arg-at=span ?~(bad whole-args at.u.bad)
7981− =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
7982− [%| ["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)]]]]
7983− ?: &((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))
7984− [%| ["call result face propagation is not supported by partial inference" ~]]
7985− [%& product.ht st(sub sub.fit, next next.fit)]
7986− =/ result=itype [%var next.st]
7987− =/ uni=(unit isub) (itype-unify ht [%fn typ.p.arg result] sub.st)
7988− ?~ uni
7989− [%| ["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)]]]]
7990− [%& result st(next +(next.st), sub u.uni)]
7991−::
79926887++ call-error-site
79936888 |= [args=(list expr) actual=itype expected=itype sub=isub next=@ud]
79946889 ^- (unit [at=span typ=itype])
@@ -8009,249 +6904,34 @@
80096904 ?: ?=(%unknown -.first) ~
80106905 $(args t.args, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
80116906::
8012−:: Context can help a call argument or cast value while the final fit
8013−:: checks the complete right-nested type, including any written faces.
8014−::
8015−:: Context can resolve the payload of a canonical prelude unit, but an
8016−:: unrelated union with a similar noun shape is not the same mold.
8017−++ infer-unit-context
8018− |= [e=expr expected=itype env=ienv state=istate context=span]
8019− ^- iresult
8020− ?> ?=(%unit -.e)
8021− ?> ?=(%union -.expected)
8022− ?~ prelude.state (infer-fragment e env state)
8023− =/ standard=(unit ischeme) (find-jibb-mold %unit u.prelude.state)
8024− ?~ standard (infer-fragment e env state)
8025− ?. (standard-unit-template u.standard at.u.prelude.state) (infer-fragment e env state)
8026− ?. =(origin.expected `[at.u.prelude.state %unit]) (infer-fragment e env state)
8027− ?~ args.expected (infer-fragment e env state)
8028− ?^ t.args.expected (infer-fragment e env state)
8029− =/ payload=itype i.args.expected
8030− =/ canonical=(unit itype) (template-apply u.standard ~[payload])
8031− ?~ canonical (infer-fragment e env state)
8032− ?> ?=(%union -.u.canonical)
8033− ?. =((itype-normalize expected(label ~) sub.state) (itype-normalize u.canonical(label ~) sub.state))
8034− (infer-fragment e env state)
8035− =/ value=iresult (infer-call-context-arg val.e payload env state context)
8036− ?: ?=(%| -.value) value
8037− =/ fit=ifit (itype-fit typ.p.value payload sub.state.p.value next.state.p.value)
8038− ?: ?=(%unknown -.fit) [%| ["unit payload constraint is not supported by partial inference" ~]]
8039− ?: ?=(%bad -.fit)
8040− =/ missing=(unit idiag) (missing-union-tag val.e payload sub.state.p.value context)
8041− ?^ missing [%| u.missing]
8042− =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
8043− ?^ nested [%| u.nested]
8044− [%| ["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)]]]]
8045− [%& expected state.p.value(sub sub.fit, next next.fit)]
8046−::
8047−:: A known gate whose result is still an inference variable can receive
8048−:: an enclosing target before its argument is inferred. Other products
8049−:: and unresolved calls use the existing directional path unchanged.
8050−++ infer-contextual-call
8051− |= [e=expr expected=itype env=ienv state=istate]
8052− ^- iresult
8053− ?> ?=(%call -.e)
8054− ?~ args.e [%| ["call has no argument" ~]]
8055− =/ head=iresult (infer-fragment head.e env state)
8056− ?: ?=(%| -.head) head
8057− =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
8058− ?. ?=(%fn -.ht) (infer-call-with-head e env state head)
8059− =/ result=itype (itype-walk product.ht sub.state.p.head)
8060− ?. ?=(%var -.result) (infer-call-with-head e env state head)
8061− ?: |(?=(%var -.expected) ?=(%avar -.expected) ?=(%nvar -.expected) (itype-has-tag (itype-normalize expected sub.state.p.head)))
8062− (infer-call-with-head e env state head)
8063− =/ sub=(unit isub) (itype-unify result expected sub.state.p.head)
8064− ?~ sub (infer-call-with-head e env state head)
8065− (infer-call-with-head e env state [%& typ.p.head state.p.head(sub u.sub)])
8066−::
8067−:: An eligible fully faced literal receives context by name, in source order.
8068−++ width-literal-fields
8069− |= [items=(list item) axis=@ud fuel=@ud]
8070− ^- (unit iwfields)
8071− =/ order=(list iwfield) ~
8072− =/ index=(map term iwfield) *(map term iwfield)
8073− |-
8074− ?~ items ~
8075− ?: =(0 fuel) ~
8076− ?~ face.i.items ~
8077− =/ at-axis=@ud ?~(t.items axis (mul 2 axis))
8078− =/ entry=iwfield [u.face.i.items at-axis [%noun ~]]
8079− ?: ?=(^ (~(get by index) name.entry)) ~
8080− =. index (~(put by index) name.entry entry)
8081− =. order [entry order]
8082− ?~ t.items `[(flop order) index]
8083− $(items t.items, axis +((mul 2 axis)), fuel (dec fuel))
8084−++ width-infer-items
8085− |= [items=(list item) expected=(map term iwfield) env=ienv state=istate context=span]
8086− ^- iresult
8087− ?~ items [%| ["empty record is not supported" ~]]
8088− ?~ face.i.items [%| ["record face needs unsupported inference" ~]]
8089− =/ field=(unit iwfield) (~(get by expected) u.face.i.items)
8090− =/ head=iresult
8091− ?~ field (infer-fragment val.i.items env state)
8092− (infer-call-context-arg val.i.items typ.u.field env state context)
8093− ?: ?=(%| -.head) head
8094− =/ typ=itype [%face u.face.i.items typ.p.head]
8095− ?~ t.items [%& typ state.p.head]
8096− =/ tail=iresult $(items t.items, state state.p.head)
8097− ?: ?=(%| -.tail) tail
8098− [%& [%cell typ typ.p.tail] state.p.tail]
8099−++ width-infer-literal
8100− |= [e=expr expected=itype env=ienv state=istate context=span]
8101− ^- (unit iresult)
8102− ?. ?=(%tuple -.e) ~
8103− ?. |(?=(%cell -.expected) ?=(%face -.expected)) ~
8104− =/ source=(unit iwfields) (width-literal-fields items.e 1 4.096)
8105− =/ target=(unit iwfields) (width-scan expected sub.state 1 4.096)
8106− ?~ source ~
8107− ?~ target ~
8108− ?: (lth (lent order.u.source) (lent order.u.target)) ~
8109− ?. (width-in-order order.u.source order.u.target)
8110− `(infer-simple-items items.e env state)
8111− `(width-infer-items items.e index.u.target env state context)
8112−::
8113−:: Recognize only the reserved unqualified, one-argument operation.
8114−++ explicit-proj-call
8115− |= [e=expr env=ienv state=istate]
8116− ^- ?
8117− ?. ?=(%call -.e) |
8118− ?. ?=([* ~] args.e) |
8119− ?. ?=(%wing -.head.e) |
8120− ?. =(names.head.e ~[%proj]) |
8121− ?: ?=(^ (ienv-lookup %proj env)) |
8122− ?: (lien globals.state |=(n=term =(n %proj))) |
8123− ?~ prelude.state &
8124− ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
8125−++ infer-proj-source
8126− |= [e=expr expected=itype env=ienv state=istate context=span]
8127− ^- iresult
8128− ?: ?=(%group -.e) $(e inner.e)
8129− =/ literal=(unit iresult) (width-infer-literal e expected env state context)
8130− ?^ literal u.literal
8131− (infer-fragment e env state)
8132−++ infer-proj-context
8133− |= [e=expr expected=itype env=ienv state=istate context=span]
8134− ^- iresult
8135− ?> ?=(%call -.e)
8136− ?~ args.e [%| ["proj needs one record" ~]]
8137− ?. |(?=(%cell -.expected) ?=(%face -.expected)) [%| ["proj needs an expected record type" ~]]
8138− =/ value=iresult (infer-proj-source i.args.e expected env state context)
8139− ?: ?=(%| -.value) value
8140− =/ shape=(unit [source=iwfields target=iwfields])
8141− (width-proj-shape typ.p.value expected sub.state.p.value)
8142− ?~ shape [%| ["proj needs a known record containing its expected fields" ~]]
8143− =/ project=(unit iwidth-result) (width-project u.shape sub.state.p.value next.state.p.value)
8144− ?~ project [%| ["proj constraint needs unsupported inference" ~]]
8145− =/ st=istate state.p.value(sub sub.u.project, next next.u.project)
8146− [%& expected st(projections [[at.e e typ.p.value expected steps.u.project] projections.st])]
6907+:: Context can help each argument while the final fit still checks the
6908+:: complete right-nested sample, including any faces on its positions.
81476909::
81486910++ infer-call-context-arg
81496911 |= [e=expr expected=itype env=ienv state=istate context=span]
81506912 ^- iresult
8151− ?: ?=(%pair -.e) $(e (pair-as-cell e))
8152− ?: ?=(%group -.e) $(e inner.e)
8153− ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
8154− ?: ?=(%trace -.e)
8155− =/ traced=iresult (infer-fragment val.e env state)
8156− ?: ?=(%| -.traced) traced
8157− $(e then.e, state state.p.traced)
81586913 =/ target=itype (itype-walk expected sub.state)
81596914 |-
81606915 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8161− ?: (explicit-proj-call e env state)
8162− (infer-proj-context e expected env state context)
8163− :: Only the source-proven one-layer cell is exposed. Each recursive
8164− :: descent consumes one written tuple; named values use ordinary fit.
8165− ?: &(?=(%jrec -.target) ?=(%lit -.e) =(%null form.lit.e))
8166− ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8167− [%& target state(jrec-fuel (dec jrec-fuel.state))]
8168− ?: &(?=(%jrec -.target) ?=(%tuple -.e))
8169− ?: =(0 jrec-fuel.state) [%| ["recursive mold unfolding needs unsupported inference" ~]]
8170− =. state state(jrec-fuel (dec jrec-fuel.state))
8171− =/ shape=itype
8172− [%cell [%face head.target [%atom aura.target]] [%face tail.target target]]
8173− =/ value=iresult (infer-call-context-items items.e shape env state context)
8174− ?: ?=(%| -.value) value
8175− =/ fit=ifit (itype-fit typ.p.value shape sub.state.p.value next.state.p.value)
8176− ?: ?=(%unknown -.fit) [%| ["recursive mold cell constraint needs unsupported inference" ~]]
8177− ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
8178− [%& target state.p.value(sub sub.fit, next next.fit)]
8179− ?: ?=(%call -.e) (infer-contextual-call e target env state)
8180− ?: (single-structured-pattern e)
8181− (infer-single-case-branch e env state `[target context])
8182− ?: (cell-binder-pattern e)
8183− (infer-cell-branch e env state `[target context])
8184− :: In a loobean-singleton context retain the written loobean noun;
8185− :: the usual final fit decides whether that value is permitted.
8186− =/ singleton=(unit itype)
8187− ?. ?=(%lit -.e) ~
8188− ?. =(%loobean form.lit.e) ~
8189− ?. ?=(%const -.target) ~
8190− ?. =(%loobean form.literal.target) ~
8191− `[%const lit.e]
8192− ?^ singleton [%& u.singleton state]
8193− =/ known=(unit iresult)
8194− ?: ?=(%branch -.e) (known-union-subject subject.e env state)
8195− ~
8196− ?: &(?=(^ known) ?=(%| -.u.known) !(duplicate-loobean-arms e)) u.known
8197− ?: &(?=(^ known) ?=(%& -.u.known) ?=(~ (unit-union-payload (itype-normalize typ.p.u.known sub.state.p.u.known))))
8198− (infer-known-union-context-subject e target env u.known context)
8199− ?: &(?=(%union -.target) ?=(%unit -.e))
8200− (infer-unit-context e target env state context)
8201− ?: &(?=(%flag -.target) (context-union-branch e))
8202− (infer-union-context e target env state context)
82036916 ?: &(?=(%union -.target) (context-union-branch e))
82046917 (infer-union-context e target env state context)
82056918 ?: &(?=(%collection -.target) =(%list name.target) (context-union-branch e))
82066919 (infer-union-context e target env state context)
82076920 ?: &(?=(%collection -.target) =(%list name.target) (context-list-expression e))
82086921 (infer-list-context e target env state context)
8209− ?: &(?=(%cell -.target) ?=(%tuple -.e))
8210− (infer-call-context-items items.e target env state context)
82116922 (infer-fragment e env state)
82126923::
8213−:: Preserve each written face; the final complete sample fit checks faces.
8214−:: A tuple or positional field face belongs to the enclosing sample,
8215−:: not to the expression at that position. A second face, if present,
8216−:: is part of the value's own expected type.
8217−++ projection-field-target
8218− |= expected=itype
8219− ^- itype
8220− ?:(?=(%face -.expected) body.expected expected)
8221−::
8222−++ infer-call-context-items
8223− |= [items=(list item) expected=itype env=ienv state=istate context=span]
8224− ^- iresult
8225− ?~ items [%| ["empty cell is not supported by partial inference" ~]]
8226− ?~ t.items
8227− =/ last=iresult (infer-call-context-arg val.i.items (projection-field-target expected) env state context)
8228− ?: ?=(%| -.last) last
8229− =/ typ=itype typ.p.last
8230− =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8231− [%& typ state.p.last]
8232− =/ target=itype (itype-walk expected sub.state)
8233− |-
8234− ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
8235− ?. ?=(%cell -.target) (infer-simple-items items env state)
8236− =/ head=iresult (infer-call-context-arg val.i.items (projection-field-target hed.target) env state context)
8237− ?: ?=(%| -.head) head
8238− =/ typ=itype typ.p.head
8239− =. typ ?~(face.i.items typ [%face u.face.i.items typ])
8240− =/ tail=iresult (infer-call-context-items t.items tal.target env state.p.head context)
8241− ?: ?=(%| -.tail) tail
8242− [%& [%cell typ typ.p.tail] state.p.tail]
8243−::
82446924++ infer-call-context-args
82456925 |= [args=(list expr) expected=itype env=ienv state=istate context=span]
82466926 ^- iresult
82476927 ?~ args [%| ["call has no argument" ~]]
8248− ?~ t.args (infer-call-context-arg i.args (projection-field-target expected) env state context)
6928+ ?~ t.args (infer-call-context-arg i.args expected env state context)
82496929 =/ target=itype (itype-walk expected sub.state)
82506930 |-
82516931 ?: ?=(%face -.target) $(target (itype-walk body.target sub.state))
82526932 ?. ?=(%cell -.target)
82536933 (infer-simple-items (turn args |=(a=expr [(span-of a) ~ a])) env state)
8254− =/ head=iresult (infer-call-context-arg i.args (projection-field-target hed.target) env state context)
6934+ =/ head=iresult (infer-call-context-arg i.args hed.target env state context)
82556935 ?: ?=(%| -.head) head
82566936 =/ tail=iresult (infer-call-context-args t.args tal.target env state.p.head context)
82576937 ?: ?=(%| -.tail) tail
@@ -8272,55 +6952,11 @@
82726952 ?: ?=(%| -.tail) tail
82736953 [%& [%cell ht typ.p.tail] state.p.tail]
82746954::
8275−:: A single all-binder cell pattern covers a known cell spine; the final
8276−:: binder captures the remaining noun. Other pattern matrices stay partial.
8277−::
8278−:: Validate binders before reading the subject, preserving shadow-error
8279−:: precedence. The last binder receives the entire remaining tail.
8280−++ cell-pattern-names
8281− |= [pats=(list pattern) env=ienv globals=(list term) seen=(list term)]
8282− ^- (each (list term) @t)
8283− ?~ pats [%& ~]
8284− ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
8285− =/ name=term name.i.pats
8286− ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
8287− [%| 'pattern shadows a name']
8288− =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
8289− ?: ?=(%| -.rest) rest
8290− [%& [name p.rest]]
8291−::
8292−++ cell-pattern-types
8293− |= [names=(list term) env=ienv next=@ud]
8294− ^- [typ=itype env=ienv next=@ud]
8295− ?~ names !!
8296− =/ head=itype [%var next]
8297− =/ scope=ienv [[i.names [head ~]] env]
8298− ?~ t.names [head scope +(next)]
8299− =/ tail=[typ=itype env=ienv next=@ud] $(names t.names, env scope, next +(next))
8300− [[%cell head typ.tail] env.tail next.tail]
8301−::
8302−:: At every position that must be a cell, opaque or sum types may still
8303−:: contain cells. Do not report a definite mismatch without unfolding them.
8304−++ cell-pattern-spine-unknown
8305− |= [typ=itype names=(list term) sub=isub]
8306− ^- ?
8307− ?~ names |
8308− ?~ t.names |
8309− =. typ (itype-walk typ sub)
8310− ?: ?=(%cell -.typ) $(typ tal.typ, names t.names)
8311− |(?=(%union -.typ) ?=(%collection -.typ) ?=(%recursive -.typ) ?=(%jrec -.typ) ?=(%noun -.typ) ?=(%fn -.typ) ?=(%tag -.typ))
8312−::
8313−++ cell-binder-pattern
8314− |= e=expr
8315− ^- ?
8316− ?. ?=(%branch -.e) |
8317− ?~ arms.e |
8318− ?^ t.arms.e |
8319− ?. ?=(%cell -.pat.i.arms.e) |
8320− !(single-structured-pattern e)
6955+:: A single two-binder cell pattern covers every value of a cell type.
6956+:: No other pattern matrix is implemented here.
83216957::
83226958++ infer-cell-branch
8323− |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
6959+ |= [e=expr env=ienv state=istate]
83246960 ^- iresult
83256961 ?> ?=(%branch -.e)
83266962 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -8329,31 +6965,25 @@
83296965 =/ pats=(list pattern) items.pat.arm
83306966 ?~ pats [%| ["branch pattern is not supported by partial inference" ~]]
83316967 ?~ t.pats [%| ["branch pattern is not supported by partial inference" ~]]
8332− =/ names=(each (list term) @t) (cell-pattern-names pats env globals.state ~)
8333− ?: ?=(%| -.names) [%| [(trip p.names) ~]]
6968+ ?^ t.t.pats [%| ["branch pattern is not supported by partial inference" ~]]
6969+ ?. ?=(%bind -.i.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6970+ ?. ?=(%bind -.i.t.pats) [%| ["branch pattern is not supported by partial inference" ~]]
6971+ =/ one=term name.i.pats
6972+ =/ two=term name.i.t.pats
6973+ ?: |(=(one two) ?=(^ (ienv-lookup one env)) ?=(^ (ienv-lookup two env)) (lien globals.state |=(x=term |(=(x one) =(x two)))))
6974+ [%| ["pattern shadows a name" ~]]
83346975 =/ subject=iresult (infer-fragment subject.e env state)
83356976 ?: ?=(%| -.subject) subject
83366977 =/ st=istate state.p.subject
8337− =/ subject-type=itype (itype-normalize typ.p.subject sub.st)
8338− ?: (itype-has-recursive subject-type)
6978+ ?: (itype-has-recursive (itype-normalize typ.p.subject sub.st))
83396979 [%| ["recursive pattern is not supported by partial inference" ~]]
83406980 ?: (itype-has-face typ.p.subject sub.st)
83416981 [%| ["record patterns are not supported by partial inference" ~]]
8342− ?: (cell-pattern-spine-unknown subject-type p.names sub.st)
8343− [%| ["cell pattern subject is not supported by partial inference" ~]]
8344− =/ binders=[typ=itype env=ienv next=@ud] (cell-pattern-types p.names env next.st)
8345− =/ sub=(unit isub) (itype-unify typ.p.subject typ.binders sub.st)
6982+ =/ head=itype [%var next.st]
6983+ =/ tail=itype [%var +(next.st)]
6984+ =/ sub=(unit isub) (itype-unify typ.p.subject [%cell head tail] sub.st)
83466985 ?~ sub [%| ["cell pattern does not match the subject type" ~]]
8347− =. st st(next next.binders, sub u.sub)
8348− ?~ expected (infer-fragment val.arm env.binders st)
8349− =/ body=iresult (infer-call-context-arg val.arm typ.u.expected env.binders st context.u.expected)
8350− ?: ?=(%| -.body) body
8351− =/ fit=ifit (itype-fit typ.p.body typ.u.expected sub.state.p.body next.state.p.body)
8352− ?: ?=(%unknown -.fit) [%| ["cell branch result constraint is not supported by partial inference" ~]]
8353− ?: ?=(%bad -.fit) [%| ["cell branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.arm) "branch arm"]]]]
8354− ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8355− [%| ["cell branch result needs context in partial inference" ~]]
8356− [%& typ.u.expected state.p.body(sub sub.fit, next next.fit)]
6986+ (infer-fragment val.arm [[one [head ~]] [two [tail ~]] env] st(next (add 2 next.st), sub u.sub))
83576987::
83586988++ show-itype
83596989 |= [t=itype sub=isub]
@@ -8372,7 +7002,6 @@
83727002 %atom "@{(trip aura.t)}"
83737003 %any-atom "@"
83747004 %flag "?"
8375− %noun "*"
83767005 %tag (trip txt.literal.t)
83777006 %const (trip txt.literal.t)
83787007 %union
@@ -8380,7 +7009,6 @@
83807009 ?~ args.t (trip u.label.t)
83817010 "({(trip u.label.t)} {(show-itype-cases args.t sub)})"
83827011 %recursive ?~(label.t "recursive mold" (trip u.label.t))
8383− %jrec ?~(label.t "recursive mold" (trip u.label.t))
83847012 %collection "({(trip name.t)} {(show-itype-cases args.t sub)})"
83857013 %face "[{(trip name.t)}={(show-itype-context body.t sub)}]"
83867014 %fn "$-({(show-itype-context sample.t sub)} {(show-itype-context product.t sub)})"
@@ -8421,12 +7049,10 @@
84217049 %atom |
84227050 %any-atom |
84237051 %flag |
8424− %noun |
84257052 %tag |
84267053 %const |
84277054 %union |((lien cases.typ |=(c=itype (itype-has-nvar c))) (lien args.typ |=(c=itype (itype-has-nvar c))))
84287055 %recursive |
8429− %jrec |
84307056 %collection (lien args.typ |=(c=itype (itype-has-nvar c)))
84317057 %face $(typ body.typ)
84327058 %fn |($(typ sample.typ) $(typ product.typ))
@@ -8531,12 +7157,10 @@
85317157 %atom |
85327158 %any-atom |
85337159 %flag |
8534− %noun |
85357160 %tag |
85367161 %const |
85377162 %union |((lien cases.t |=(c=itype (has-atom-var n c))) (lien args.t |=(c=itype (has-atom-var n c))))
85387163 %recursive |
8539− %jrec |
85407164 %collection (lien args.t |=(c=itype (has-atom-var n c)))
85417165 %face $(t body.t)
85427166 %fn |($(t sample.t) $(t product.t))
@@ -8584,9 +7208,9 @@
85847208::
85857209:: Build the supported part of the value environment in dependency order.
85867210:: Each pass adds successful definitions. Forward references become
8587−:: available on a later pass; unsupported syntax does not enter the
8588−:: environment. Generalized definitions are closed, so a use instantiates
8589−:: its variables afresh.
7211+:: available on a later pass; mutually recursive groups and unsupported
7212+:: syntax do not enter the environment. Generalized definitions are closed, so a
7213+:: use instantiates its variables afresh.
85907214::
85917215++ global-value-names
85927216 |= ds=(list def)
@@ -8713,508 +7337,36 @@
87137337 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
87147338 [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
87157339::
8716−++ dependency-root
8717− |= names=(list term)
8718− ^- (list term)
8719− ?~ names ~
8720− ~[(rear names)]
8721−::
8722−++ dependency-exprs
8723− |= xs=(list expr)
8724− ^- (list term)
8725− ?~ xs ~
8726− =/ first=(list term) (dependency-expr i.xs)
8727− (weld first $(xs t.xs))
8728−::
8729−++ dependency-pieces
8730− |= xs=(list piece)
8731− ^- (list term)
8732− ?~ xs ~
8733− =/ first=(list term)
8734− ?- -.i.xs
8735− %expr (dependency-expr p.i.xs)
8736− %text ~
8737− ==
8738− (weld first $(xs t.xs))
8739−::
8740−++ dependency-qsegs
8741− |= xs=(list qseg)
8742− ^- (list term)
8743− ?~ xs ~
8744− =/ first=(list term)
8745− ?- -.i.xs
8746− %expr (dependency-expr p.i.xs)
8747− %knot ~
8748− ==
8749− (weld first $(xs t.xs))
8750−::
8751−++ dependency-items
8752− |= xs=(list item)
8753− ^- (list term)
8754− ?~ xs ~
8755− =/ first=(list term) (dependency-expr val.i.xs)
8756− (weld first $(xs t.xs))
8757−::
8758−++ dependency-edits
8759− |= xs=(list edit)
8760− ^- (list term)
8761− ?~ xs ~
8762− =/ first=(list term) (dependency-expr val.i.xs)
8763− (weld first $(xs t.xs))
8764−::
8765−++ dependency-arms
8766− |= xs=(list arm)
8767− ^- (list term)
8768− ?~ xs ~
8769− =/ first=(list term) (dependency-expr val.i.xs)
8770− (weld first $(xs t.xs))
8771−::
8772−++ dependency-defs
8773− |= xs=(list def)
8774− ^- (list term)
8775− ?~ xs ~
8776− =/ first=(list term)
8777− ?: ?=(%value -.i.xs) (dependency-expr val.i.xs)
8778− ~
8779− (weld first $(xs t.xs))
8780−::
8781−++ dependency-expr
8782− |= e=expr
8783− ^- (list term)
8784− ?- -.e
8785− %str (dependency-pieces pieces.e)
8786− %qath (dependency-qsegs segs.e)
8787− %wing (dependency-root names.e)
8788− %change
8789− =/ first=(list term) (dependency-root target.e)
8790− =/ last=(list term) (dependency-edits edits.e)
8791− (weld first last)
8792− %pair (dependency-expr val.e)
8793− %unit (dependency-expr val.e)
8794− %group (dependency-expr inner.e)
8795− %list (dependency-exprs items.e)
8796− %tuple (dependency-items items.e)
8797− %gate (dependency-expr body.e)
8798− %gate-wide (dependency-expr body.e)
8799− %call
8800− =/ first=(list term) (dependency-expr head.e)
8801− =/ last=(list term) (dependency-exprs args.e)
8802− (weld first last)
8803− %cast (dependency-expr val.e)
8804− %trace
8805− =/ first=(list term) (dependency-expr val.e)
8806− =/ last=(list term) (dependency-expr then.e)
8807− (weld first last)
8808− %branch
8809− =/ first=(list term) (dependency-expr subject.e)
8810− =/ last=(list term) (dependency-arms arms.e)
8811− (weld first last)
8812− %body
8813− =/ first=(list term) (dependency-defs defs.e)
8814− =/ last=(list term) (dependency-expr final.e)
8815− (weld first last)
8816− * ~
8817− ==
8818−::
8819−:: Infer a cyclic component with one monomorphic seed per gate. All members
8820−:: must succeed before any scheme is available; pending constraints and
8821−:: unresolved branch joins remain partial.
8822−+$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
8823−+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
8824−++ seed-gate-group
8825− |= [ds=(list def) env=ienv state=istate]
8826− ^- igate-seeds
8827− ?~ ds [%& [~ state]]
8828− =/ d=def i.ds
8829− ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
8830− =/ gate=expr val.d
8831− ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
8832− [%| ["recursive group contains a non-gate" ~]]
8833− =/ initial=istate (reserve-def-caps gate state)
8834− =/ sam=isample-result
8835− ?- -.gate
8836− %gate (infer-sample sample.gate env initial)
8837− %gate-wide (infer-sample sample.gate env initial)
8838− * !!
8839− ==
8840− ?: ?=(%| -.sam) [%| [p.sam ~]]
8841− =/ body=expr
8842− ?- -.gate
8843− %gate body.gate
8844− %gate-wide body.gate
8845− * !!
8846− ==
8847− =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
8848− =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
8849− =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
8850− =/ rest=igate-seeds $(ds t.ds, state after)
8851− ?: ?=(%| -.rest) rest
8852− [%& [[entry entries.p.rest] state.p.rest]]
8853−::
8854−++ group-seed-env
8855− |= [entries=(list igate-entry) env=ienv]
8856− ^- ienv
8857− ?~ entries env
8858− [[name.i.entries [typ.i.entries ~]] $(entries t.entries)]
8859−::
8860−++ infer-gate-group-bodies
8861− |= [entries=(list igate-entry) seeds=ienv state=istate]
8862− ^- igate-seeds
8863− ?~ entries [%& [~ state]]
8864− =/ entry=igate-entry i.entries
8865− ?> ?=(%fn -.typ.entry)
8866− =/ scope=ienv (weld seeds env.entry)
8867− =/ out=iresult (infer-fragment body.entry scope state(caps caps.entry))
8868− ?: ?=(%| -.out) out
8869− =/ uni=(unit isub) (itype-unify product.typ.entry typ.p.out sub.state.p.out)
8870− ?~ uni [%| ["recursive group constraint is not supported by partial inference" ~]]
8871− =. caps.entry caps.state.p.out
8872− =/ after=istate state.p.out(sub u.uni, caps caps.state)
8873− =/ rest=igate-seeds $(entries t.entries, state after)
8874− ?: ?=(%| -.rest) rest
8875− [%& [[entry entries.p.rest] state.p.rest]]
8876−::
8877−++ group-schemes
8878− |= [entries=(list igate-entry) env=ienv outer=istate state=istate]
8879− ^- (each ienv idiag)
8880− ?~ entries [%& ~]
8881− =/ entry=igate-entry i.entries
8882− =/ merged=(unit [first=icap second=icap]) (merged-capitals caps.entry sub.state)
8883− ?^ merged
8884− [%| ["distinct type variables must not be forced equal" ~[[at.first.u.merged "first type variable"] [at.second.u.merged "second type variable"]]]]
8885− ?: (constrained-capitals caps.entry sub.state)
8886− [%| ["explicit capital constraints are not supported by partial inference" ~]]
8887− =/ typ=itype (itype-normalize typ.entry sub.state)
8888− ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
8889− [%| ["recursive group needs unsupported inference" ~]]
8890− =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
8891− =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
8892− =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
8893− ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
8894− =/ rest=(each ienv idiag) $(entries t.entries)
8895− ?: ?=(%| -.rest) rest
8896− [%& [[name.entry [typ vars]] p.rest]]
8897−::
8898−++ infer-gate-group
8899− |= [ds=(list def) env=ienv state=istate]
8900− ^- ilocal-result
8901− =/ names=(list term) (global-value-names ds)
8902− ?. (levy names |=(n=term (unique-value-name n names)))
8903− [%| ["recursive group contains duplicate names" ~]]
8904− ?: (lien names |=(n=term ?=(^ (ienv-lookup n env))))
8905− [%| ["recursive group shadows a name" ~]]
8906− =/ scoped=istate state(globals (weld names globals.state))
8907− =/ seeded=igate-seeds (seed-gate-group ds env scoped)
8908− ?: ?=(%| -.seeded) seeded
8909− =/ seeds=ienv (group-seed-env entries.p.seeded ~)
8910− =/ body=igate-seeds (infer-gate-group-bodies entries.p.seeded seeds state.p.seeded)
8911− ?: ?=(%| -.body) body
8912− :: Per-member ownership through mutual recursion is not implemented.
8913− ?: !=(projections.state.p.body projections.state)
8914− [%| ["record projection in recursive groups needs unsupported inference" ~]]
8915− ?: !=(holes.state.p.body holes.state)
8916− [%| ["holes in recursive groups need unsupported inference" ~]]
8917− ?: (pending-tags tags.state.p.body sub.state.p.body)
8918− [%| ["recursive group has unresolved literal constraints" ~]]
8919− =/ schemes=(each ienv idiag) (group-schemes entries.p.body env state state.p.body)
8920− ?: ?=(%| -.schemes) schemes
8921− [%& [(weld p.schemes env) state.p.body(globals globals.state)]]
8922−::
8923−++ width-finalize
8924− |= [ps=(list iwprojection) sub=isub visible=(list @ud)]
8925− ^- (unit (list iwprojection))
8926− ?~ ps `~
8927− ?: (lien t.ps |=(p=iwprojection =(at.p at.i.ps))) ~
8928− =/ src=itype (default-decimals (itype-normalize source.i.ps sub))
8929− =/ dst=itype (default-decimals (itype-normalize target.i.ps sub))
8930− ?: |((itype-has-nvar src) (itype-has-nvar dst) (itype-has-tag src) (itype-has-tag dst)) ~
8931− =/ vars=(list @ud) (weld (itype-vars src) (itype-vars dst))
8932− ?. (levy vars |=(n=@ud (lien visible |=(v=@ud =(n v))))) ~
8933− =/ rest=(unit (list iwprojection)) $(ps t.ps)
8934− ?~ rest ~
8935− =/ entry=iwprojection i.ps
8936− =. entry entry(source src, target dst)
8937− `[entry u.rest]
8938−::
89397340++ add-supported-defs
8940− |= [ds=(list def) env=ienv molds=imolds globals=(list term) externals=iexternals surs=(list term) mark-externals=imark-externals marks=(list term) jimports=ijimports reserved-molds=(list term) at=path prelude=(unit ifile) artifacts=(list iwidth-definition)]
8941− ^- [env=ienv artifacts=(list iwidth-definition)]
8942− ?~ ds [env artifacts]
7341+ |= [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)]
7342+ ^- ienv
7343+ ?~ ds env
89437344 =/ d=def i.ds
89447345 ?: ?=(%mold -.d) $(ds t.ds)
89457346 ?. (unique-value-name name.d globals) $(ds t.ds)
89467347 ?^ (ienv-lookup name.d env) $(ds t.ds)
89477348 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
8948− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
7349+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude]
89497350 =. initial (reserve-def-caps val.d initial)
89507351 =/ result=iresult (infer-fragment val.d env initial)
89517352 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
89527353 ?: ?=(%| -.result) $(ds t.ds)
8953− =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
8954− ?^ (unresolved-hole holes.state.p.result holes.initial state.p.result) $(ds t.ds)
89557354 ?: (constrained-capitals caps.state.p.result sub.state.p.result) $(ds t.ds)
89567355 =/ typ=itype (default-decimals (itype-normalize typ.p.result sub.state.p.result))
89577356 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) $(ds t.ds)
89587357 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) $(ds t.ds)
89597358 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
89607359 ?: (gth (lent vars) 26) $(ds t.ds)
8961− =/ finalized=(unit (list iwprojection))
8962− (width-finalize projections.state.p.result sub.state.p.result vars)
8963− ?~ finalized $(ds t.ds)
8964− =? artifacts ?=(^ u.finalized)
8965− [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
89667360 $(ds t.ds, env [[name.d [typ vars]] env])
89677361::
8968−+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
8969−+$ iadj (map term (list term))
8970−+$ ivisited (map term ?)
8971−+$ iwork (list [name=term done=?])
8972−+$ iwresult [seen=ivisited order=(list term)]
8973−+$ icresult [seen=ivisited component=(list term)]
8974−+$ icomponents (list (list term))
8975−++ graph-nameset
8976− |= [names=(list term) seen=ivisited]
8977− ^- ivisited
8978− ?~ names seen
8979− $(names t.names, seen (~(put by seen) i.names &))
8980−::
8981−++ graph-edges
8982− |= [name=term graph=iadj]
8983− ^- (list term)
8984− =/ found=(unit (list term)) (~(get by graph) name)
8985− ?~ found ~
8986− u.found
8987−::
8988−++ graph-make-forward
8989− |= [ds=(list def) names=ivisited graph=iadj]
8990− ^- iadj
8991− ?~ ds graph
8992− ?. ?=(%value -.i.ds) $(ds t.ds)
8993− =/ deps=(list term) (dependency-expr val.i.ds)
8994− =. deps (skim deps |=(n=term ?=(^ (~(get by names) n))))
8995− $(ds t.ds, graph (~(put by graph) name.i.ds deps))
8996−::
8997−++ graph-add-reverse
8998− |= [name=term edges=(list term) reverse=iadj]
8999− ^- iadj
9000− ?~ edges reverse
9001− =/ prior=(list term) (graph-edges i.edges reverse)
9002− $(edges t.edges, reverse (~(put by reverse) i.edges [name prior]))
9003−::
9004−++ graph-reverse
9005− |= [names=(list term) graph=iadj reverse=iadj]
9006− ^- iadj
9007− ?~ names reverse
9008− =. reverse (graph-add-reverse i.names (graph-edges i.names graph) reverse)
9009− $(names t.names)
9010−::
9011−++ graph-order
9012− |= [todo=iwork seen=ivisited order=(list term) graph=iadj]
9013− ^- iwresult
9014− ?~ todo [seen order]
9015− =/ event=[name=term done=?] i.todo
9016− ?: done.event $(todo t.todo, order [name.event order])
9017− ?: ?=(^ (~(get by seen) name.event)) $(todo t.todo)
9018− =. seen (~(put by seen) name.event &)
9019− =/ children=iwork (turn (graph-edges name.event graph) |=(n=term [n |]))
9020− $(todo (weld children [[name.event &] t.todo]))
9021−::
9022−++ graph-collect
9023− |= [todo=(list term) seen=ivisited component=(list term) graph=iadj]
9024− ^- icresult
9025− ?~ todo [seen component]
9026− ?: ?=(^ (~(get by seen) i.todo)) $(todo t.todo)
9027− =. seen (~(put by seen) i.todo &)
9028− $(todo (weld (graph-edges i.todo graph) t.todo), component [i.todo component])
9029−::
9030−++ graph-collect-all
9031− |= [order=(list term) seen=ivisited graph=iadj comps=icomponents]
9032− ^- icomponents
9033− ?~ order comps
9034− ?: ?=(^ (~(get by seen) i.order)) $(order t.order)
9035− =/ found=icresult (graph-collect ~[i.order] seen ~ graph)
9036− $(order t.order, seen seen.found, comps [component.found comps])
9037−::
9038−:: Two depth-first passes find components before group inference. Maps
9039−:: preserve the graph identity; duplicate global names fail closed.
9040−++ graph-components
9041− |= [ds=(list def) names=(list term)]
9042− ^- icomponents
9043− =/ nameset=ivisited ~
9044− =/ pending=(list term) names
9045− |-
9046− ?^ pending
9047− ?: ?=(^ (~(get by nameset) i.pending)) ~
9048− $(pending t.pending, nameset (~(put by nameset) i.pending &))
9049− =/ graph=iadj (graph-make-forward ds nameset ~)
9050− =/ reverse=iadj (graph-reverse names graph ~)
9051− =/ order=iwresult (graph-order (turn names |=(n=term [n |])) ~ ~ graph)
9052− (graph-collect-all order.order ~ reverse ~)
9053−::
9054−++ graph-cycle
9055− |= [component=(list term) graph=iadj]
9056− ^- ?
9057− ?~ component |
9058− ?^ t.component &
9059− (lien (graph-edges i.component graph) |=(x=term =(x i.component)))
9060−::
9061−++ add-groups
9062− |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
9063− ^- iresolved
9064− ?~ components [env grouped artifacts]
9065− =/ component=(list term) i.components
9066− ?. (graph-cycle component graph) $(components t.components)
9067− ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
9068− =/ members=(list def)
9069− %+ skim ds
9070− |= d=def
9071− &(?=(%value -.d) (lien component |=(n=term =(n name.d))))
9072− ?. =((lent members) (lent component)) $(components t.components)
9073− ?. (levy component |=(n=term (unique-value-name n globals.state))) $(components t.components)
9074− =/ result=ilocal-result (infer-gate-group members env state)
9075− ?: ?=(%| -.result) $(components t.components)
9076− $(components t.components, env env.p.result, grouped (weld component grouped))
9077−::
9078−++ resolve-groups
9079− |= [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)]
9080− ^- iresolved
9081− =/ env=ienv ~
9082− =/ grouped=(list term) ~
9083− =/ artifacts=(list iwidth-definition) ~
9084− =/ names=(list term) (global-value-names ds)
9085− =/ nameset=ivisited (graph-nameset names ~)
9086− =/ graph=iadj (graph-make-forward ds nameset ~)
9087− =/ components=icomponents (graph-components ds names)
9088− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9089− |-
9090− =/ next=[env=ienv artifacts=(list iwidth-definition)]
9091− (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts)
9092− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~]
9093− =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
9094− ?: =(env env.out) out
9095− $(env env.out, grouped grouped.out, artifacts artifacts.out)
9096−::
90977362++ resolve-supported-defs
90987363 |= [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)]
90997364 ^- ienv
9100− env:(resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
9101−::
9102−:: A diagnostic-only proof for a narrow syntactic value cycle. Every
9103−:: edge is an unqualified wing in a supported expression, and samples
9104−:: may not shadow global bindings. Unknown forms yield no conclusion.
9105−+$ icyclesite [name=term at=span]
9106−+$ icycle [name=term first=span next=span]
9107−++ cycle-sites-list
9108− |= [xs=(list expr) globals=(list term) locals=(list term)]
9109− ^- (unit (list icyclesite))
9110− ?~ xs `~
9111− =/ first=(unit (list icyclesite)) (cycle-sites i.xs globals locals)
9112− ?~ first ~
9113− =/ tail=(unit (list icyclesite)) $(xs t.xs)
9114− ?~ tail ~
9115− `(weld u.first u.tail)
9116−::
9117−++ cycle-sample-name
9118− |= [sam=sample globals=(list term) locals=(list term)]
9119− ^- (unit (unit term))
9120− ?- -.sam
9121− %bind
9122− ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9123− ``name.sam
9124− %face
9125− ?: (lien (weld globals locals) |=(n=term =(n name.sam))) ~
9126− ``name.sam
9127− %bare `~
9128− * ~
9129− ==
9130−::
9131−++ cycle-sites
9132− |= [e=expr globals=(list term) locals=(list term)]
9133− ^- (unit (list icyclesite))
9134− ?- -.e
9135− %wing
9136− ?. ?=([@ ~] names.e) ~
9137− `~[[i.names.e at.e]]
9138− %lit `~
9139− %str
9140− ?: (lien pieces.e |=(p=piece ?=(%expr -.p))) ~
9141− `~
9142− %group $(e inner.e)
9143− %body ?~(defs.e $(e final.e) ~)
9144− %cast $(e val.e)
9145− %gate
9146− =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9147− ?~ binder ~
9148− =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9149− $(e body.e, locals nested)
9150− %gate-wide
9151− =/ binder=(unit (unit term)) (cycle-sample-name sample.e globals locals)
9152− ?~ binder ~
9153− =/ nested=(list term) ?~(u.binder locals [u.u.binder locals])
9154− $(e body.e, locals nested)
9155− %call
9156− =/ first=(unit (list icyclesite)) $(e head.e)
9157− ?~ first ~
9158− =/ tail=(unit (list icyclesite)) (cycle-sites-list args.e globals locals)
9159− ?~ tail ~
9160− `(weld u.first u.tail)
9161− * ~
9162− ==
9163−::
9164−++ cycle-definitely-atom
9165− |= e=expr
9166− ^- ?
9167− ?: ?=(%group -.e) $(e inner.e)
9168− ?: &(?=(%body -.e) ?=(~ defs.e)) $(e final.e)
9169− ?. ?=(%cast -.e) |
9170− |(?=(%aura -.shape.e) ?=(%flag -.shape.e))
9171−::
9172−++ cycle-proof-group
9173− |= [members=(list def) globals=(list term)]
9174− ^- ?
9175− ?~ members &
9176− ?. ?=(%value -.i.members) |
9177− ?. (unique-value-name name.i.members globals) |
9178− ?. ?=(^ (cycle-sites val.i.members globals ~)) |
9179− $(members t.members)
9180−::
9181−++ cycle-find-site
9182− |= [sites=(list icyclesite) component=(list term)]
9183− ^- (unit span)
9184− ?~ sites ~
9185− ?: (lien component |=(n=term =(n name.i.sites))) `at.i.sites
9186− $(sites t.sites)
9187−::
9188−++ cycle-group-errors
9189− |= [members=(list def) component=(list term) globals=(list term)]
9190− ^- (list icycle)
9191− ?~ members ~
9192− =/ d=def i.members
9193− ?> ?=(%value -.d)
9194− =/ tail=(list icycle) $(members t.members)
9195− ?. (cycle-definitely-atom val.d) tail
9196− =/ sites=(unit (list icyclesite)) (cycle-sites val.d globals ~)
9197− ?~ sites tail
9198− =/ found=(unit span) (cycle-find-site u.sites component)
9199− ?~ found tail
9200− [[name.d at.d u.found] tail]
9201−::
9202−++ definite-value-cycles
9203− |= [ds=(list def) globals=(list term)]
9204− ^- (list icycle)
9205− =/ names=(list term) (global-value-names ds)
9206− =/ graph=iadj (graph-make-forward ds (graph-nameset names ~) ~)
9207− =/ components=icomponents (graph-components ds names)
9208− =/ out=(list icycle) ~
7365+ =/ env=ienv ~
92097366 |-
9210− ?~ components out
9211− =/ component=(list term) i.components
9212− ?. (graph-cycle component graph) $(components t.components)
9213− =/ members=(list def)
9214− (skim ds |=(d=def &(?=(%value -.d) (lien component |=(n=term =(n name.d))))))
9215− ?. =((lent members) (lent component)) $(components t.components)
9216− ?. (cycle-proof-group members globals) $(components t.components)
9217− $(components t.components, out (weld (cycle-group-errors members component globals) out))
7367+ =/ next=ienv (add-supported-defs ds env molds globals externals surs mark-externals marks jimports reserved-molds at prelude)
7368+ ?: =(next env) env
7369+ $(env next)
92187370::
92197371+| %union-analysis
92207372::
@@ -9351,142 +7503,11 @@
93517503 [at.first at.second (union-relate a (project-union-mold second molds ~))]
93527504 (weld pairs $(cases t.cases))
93537505::
9354−:: A closed structural mold supplies no equation to determine a hole.
9355−:: Applications, references, unbound capitals and unions are unproved.
9356−++ simple-mold-hole
9357− |= sh=shape
9358− ^- (unit (unit span))
9359− ?: ?=(%generic -.sh)
9360− ?~ vars.sh ~
9361− ?. (distinct-params vars.sh) ~
9362− (simple-mold-hole-in body.sh vars.sh)
9363− (simple-mold-hole-in sh ~)
9364−++ simple-mold-hole-in
9365− |= [sh=shape vars=(list @t)]
9366− ^- (unit (unit span))
9367− ?- -.sh
9368− %hole ``at.sh
9369− ?(%aura %noun %void %flag %const) `~
9370− %tvar ?:((lien vars |=(v=@t =(v name.sh))) `~ ~)
9371− %cell (simple-mold-field-holes fields.sh vars)
9372− %fn
9373− =/ a=(unit (unit span)) $(sh sample.sh)
9374− ?~ a ~
9375− =/ b=(unit (unit span)) $(sh product.sh)
9376− ?~ b ~
9377− `?~(u.a u.b u.a)
9378− %generic ~
9379− * ~
9380− ==
9381−++ simple-mold-field-holes
9382− |= [fields=(list field) vars=(list @t)]
9383− ^- (unit (unit span))
9384− ?~ fields `~
9385− =/ f=field i.fields
9386− =/ first=(unit (unit span))
9387− ?- -.f
9388− %face (simple-mold-hole-in shape.f vars)
9389− %bare (simple-mold-hole-in shape.f vars)
9390− %pun ~
9391− ==
9392− ?~ first ~
9393− =/ rest=(unit (unit span)) $(fields t.fields)
9394− ?~ rest ~
9395− `?~(u.first u.rest u.first)
9396−++ simple-local-mold-hole
9397− |= defs=(list def)
9398− ^- (unit span)
9399− ?~ defs ~
9400− ?. ?=(%mold -.i.defs) $(defs t.defs)
9401− =/ found=(unit (unit span)) (simple-mold-hole shape.i.defs)
9402− ?~ found $(defs t.defs)
9403− ?^ u.found u.found
9404− $(defs t.defs)
9405−::
9406−:: A partial prelude may omit unsupported declarations, but may not
9407−:: publish an interface while a named mold's hole remains unchecked.
9408−++ shape-has-hole
9409− |= sh=shape
9410− ^- ?
9411− ?- -.sh
9412− %hole &
9413− %path (lien segs.sh |=(s=pseg ?=(%inferred -.s)))
9414− %apply (lien args.sh shape-has-hole)
9415− %union (lien cases.sh shape-has-hole)
9416− %cell (lien fields.sh field-has-hole)
9417− %fn |($(sh sample.sh) $(sh product.sh))
9418− %generic $(sh body.sh)
9419− * |
9420− ==
9421−++ field-has-hole
9422− |= f=field
9423− ^- ?
9424− ?- -.f
9425− %face (shape-has-hole shape.f)
9426− %bare (shape-has-hole shape.f)
9427− %pun |
9428− ==
9429−++ named-mold-has-hole
9430− |= ds=(list def)
9431− ^- ?
9432− ?~ ds |
9433− ?: &(?=(%mold -.i.ds) (shape-has-hole shape.i.ds)) &
9434− $(ds t.ds)
9435−::
9436−++ sample-has-hole
9437− |= sam=sample
9438− ^- ?
9439− ?- -.sam
9440− %face (shape-has-hole shape.sam)
9441− %bare (shape-has-hole shape.sam)
9442− %cell (lien items.sam sample-has-hole)
9443− * |
9444− ==
9445−++ def-has-hole
9446− |= d=def
9447− ^- ?
9448− ?- -.d
9449− %mold (shape-has-hole shape.d)
9450− %value (expr-has-hole val.d)
9451− ==
9452−++ expr-has-hole
9453− |= e=expr
9454− ^- ?
9455− ?- -.e
9456− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9457− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (expr-has-hole p.p) |)))
9458− %change (lien edits.e |=(p=edit (expr-has-hole val.p)))
9459− %pair $(e val.e)
9460− %unit $(e val.e)
9461− %group $(e inner.e)
9462− %list (lien items.e expr-has-hole)
9463− %tuple (lien items.e |=(i=item (expr-has-hole val.i)))
9464− ?(%gate %gate-wide) |((sample-has-hole sample.e) $(e body.e))
9465− %cast |((shape-has-hole shape.e) $(e val.e))
9466− %call |($(e head.e) (lien args.e expr-has-hole))
9467− %trace |($(e val.e) $(e then.e))
9468− %branch |($(e subject.e) (lien arms.e |=(a=arm (expr-has-hole val.a))))
9469− %body |((lien defs.e def-has-hole) $(e final.e))
9470− * |
9471− ==
9472−++ hole-values-present
9473− |= [ds=(list def) env=ienv]
9474− ^- ?
9475− ?~ ds &
9476− ?. ?=(%value -.i.ds) $(ds t.ds)
9477− ?: (expr-has-hole val.i.ds)
9478− ?. ?=(^ (ienv-lookup name.i.ds env)) |
9479− $(ds t.ds)
9480− $(ds t.ds)
94817506++ show-partial-mold
94827507 |= [file=path src=@t d=def molds=imolds]
94837508 ^- @t
94847509 ?> ?=(%mold -.d)
94857510 =/ sh=shape shape.d
9486− =/ hole=(unit (unit span)) (simple-mold-hole sh)
9487− ?: &(?=(^ hole) ?=(^ u.hole))
9488− =/ text=@t (show-error src [file line.beg.u.u.hole col.beg.u.u.hole "unresolved type hole"])
9489− (of-wain:format ~[(crip "+$ {(trip name.d)}: type hole needs a determined type") text])
94907511 =? sh ?=(%generic -.sh) body.sh
94917512 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
94927513 =/ pairs=(list upair) (union-pairs cases.sh molds)
@@ -9513,21 +7534,6 @@
95137534 (show-error src [file line.beg.at.site col.beg.at.site note.site])
95147535 (of-wain:format [summary excerpts])
95157536::
9516−:: Both written field sites are shown in the source that declares them.
9517−++ show-duplicate-fields
9518− |= [file=path src=@t diagnostic=idiag]
9519− ^- @t
9520− =/ excerpts=(list @t)
9521− %+ turn sites.diagnostic
9522− |= site=[at=span note=tape]
9523− (show-error src [file line.beg.at.site col.beg.at.site note.site])
9524− (of-wain:format [(crip msg.diagnostic) excerpts])
9525−::
9526−++ duplicate-fields-report
9527− |= [file=path src=@t diagnostic=idiag]
9528− ^- @t
9529− (of-wain:format ~['partial inference; module not checked' (show-duplicate-fields file src diagnostic)])
9530−::
95317537:: +golden-types: a partial report; it does not claim the module checks
95327538::
95337539++ golden-types
@@ -9557,180 +7563,6 @@
95577563+$ jfile-result (each [iface=ifile cache=jcache] @t)
95587564+$ jimports-result (each [resolved=ijimports cache=jcache] @t)
95597565::
9560−:: Written record fields each have their own lexical record scope.
9561−+$ written-fields (map term span)
9562−++ duplicate-written-field
9563− |= [name=term at=span seen=written-fields]
9564− ^- (unit idiag)
9565− =/ prior=(unit span) (~(get by seen) name)
9566− ?~ prior ~
9567− `["record field `{(trip name)}` is repeated" ~[[u.prior "first field"] [at "repeated field"]]]
9568−++ duplicate-shapes
9569− |= xs=(list shape)
9570− ^- (unit idiag)
9571− ?~ xs ~
9572− =/ first (duplicate-shape i.xs)
9573− ?^ first first
9574− $(xs t.xs)
9575−++ duplicate-fields
9576− |= [fields=(list field) seen=written-fields]
9577− ^- (unit idiag)
9578− ?~ fields ~
9579− =/ f=field i.fields
9580− =/ n=(unit term)
9581− ?- -.f
9582− %face `name.f
9583− %pun `name.f
9584− %bare ~
9585− ==
9586− =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.f seen))
9587− ?^ dup dup
9588− =/ inner=(unit idiag)
9589− ?- -.f
9590− %face (duplicate-shape shape.f)
9591− %pun ~
9592− %bare (duplicate-shape shape.f)
9593− ==
9594− ?^ inner inner
9595− $(fields t.fields, seen ?~(n seen (~(put by seen) u.n at.f)))
9596−++ duplicate-shape
9597− |= s=shape
9598− ^- (unit idiag)
9599− ?- -.s
9600− %cell (duplicate-fields fields.s ~)
9601− %apply (duplicate-shapes args.s)
9602− %union (duplicate-shapes cases.s)
9603− %fn
9604− =/ left (duplicate-shape sample.s)
9605− ?^ left left
9606− (duplicate-shape product.s)
9607− %generic (duplicate-shape body.s)
9608− * ~
9609− ==
9610−++ duplicate-samples
9611− |= [items=(list sample) seen=written-fields]
9612− ^- (unit idiag)
9613− ?~ items ~
9614− =/ a=sample i.items
9615− =/ n=(unit term)
9616− ?- -.a
9617− %bind `name.a
9618− %face `name.a
9619− %pun `name.a
9620− * ~
9621− ==
9622− =/ dup=(unit idiag) ?~(n ~ (duplicate-written-field u.n at.a seen))
9623− ?^ dup dup
9624− =/ inner (duplicate-sample a)
9625− ?^ inner inner
9626− $(items t.items, seen ?~(n seen (~(put by seen) u.n at.a)))
9627−++ duplicate-sample
9628− |= s=sample
9629− ^- (unit idiag)
9630− ?- -.s
9631− %cell (duplicate-samples items.s ~)
9632− %face (duplicate-shape shape.s)
9633− %bare (duplicate-shape shape.s)
9634− * ~
9635− ==
9636−++ duplicate-exprs
9637− |= xs=(list expr)
9638− ^- (unit idiag)
9639− ?~ xs ~
9640− =/ first (duplicate-expr i.xs)
9641− ?^ first first
9642− $(xs t.xs)
9643−++ duplicate-items
9644− |= [items=(list item) seen=written-fields]
9645− ^- (unit idiag)
9646− ?~ items ~
9647− =/ a=item i.items
9648− =/ dup=(unit idiag) ?~(face.a ~ (duplicate-written-field u.face.a at.a seen))
9649− ?^ dup dup
9650− =/ inner (duplicate-expr val.a)
9651− ?^ inner inner
9652− $(items t.items, seen ?~(face.a seen (~(put by seen) u.face.a at.a)))
9653−++ duplicate-pieces
9654− |= pieces=(list piece)
9655− ^- (unit idiag)
9656− ?~ pieces ~
9657− =/ first=(unit idiag) ?:(?=(%expr -.i.pieces) (duplicate-expr p.i.pieces) ~)
9658− ?^ first first
9659− $(pieces t.pieces)
9660−++ duplicate-qsegs
9661− |= segs=(list qseg)
9662− ^- (unit idiag)
9663− ?~ segs ~
9664− =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
9665− ?^ first first
9666− $(segs t.segs)
9667−++ duplicate-edits
9668− |= edits=(list edit)
9669− ^- (unit idiag)
9670− ?~ edits ~
9671− =/ first (duplicate-expr val.i.edits)
9672− ?^ first first
9673− $(edits t.edits)
9674−++ duplicate-arms
9675− |= arms=(list arm)
9676− ^- (unit idiag)
9677− ?~ arms ~
9678− =/ first (duplicate-expr val.i.arms)
9679− ?^ first first
9680− $(arms t.arms)
9681−++ duplicate-defs
9682− |= defs=(list def)
9683− ^- (unit idiag)
9684− ?~ defs ~
9685− =/ first=(unit idiag)
9686− ?- -.i.defs
9687− %mold (duplicate-shape shape.i.defs)
9688− %value (duplicate-expr val.i.defs)
9689− ==
9690− ?^ first first
9691− $(defs t.defs)
9692−++ duplicate-expr
9693− |= e=expr
9694− ^- (unit idiag)
9695− ?- -.e
9696− %str (duplicate-pieces pieces.e)
9697− %qath (duplicate-qsegs segs.e)
9698− %change (duplicate-edits edits.e)
9699− %pair (duplicate-expr val.e)
9700− %unit (duplicate-expr val.e)
9701− %group (duplicate-expr inner.e)
9702− %list (duplicate-exprs items.e)
9703− %tuple (duplicate-items items.e ~)
9704− %gate-wide
9705− =/ first (duplicate-sample sample.e)
9706− ?^ first first
9707− (duplicate-expr body.e)
9708− %gate
9709− =/ first (duplicate-sample sample.e)
9710− ?^ first first
9711− (duplicate-expr body.e)
9712− %cast
9713− =/ first (duplicate-shape shape.e)
9714− ?^ first first
9715− (duplicate-expr val.e)
9716− %call
9717− =/ first (duplicate-expr head.e)
9718− ?^ first first
9719− (duplicate-exprs args.e)
9720− %trace
9721− =/ first (duplicate-expr val.e)
9722− ?^ first first
9723− (duplicate-expr then.e)
9724− %branch
9725− =/ first (duplicate-expr subject.e)
9726− ?^ first first
9727− (duplicate-arms arms.e)
9728− %body
9729− =/ first (duplicate-defs defs.e)
9730− ?^ first first
9731− (duplicate-expr final.e)
9732− * ~
9733− ==
97347566++ import-binding-names
97357567 |= imports=(list import)
97367568 ^- (list term)
@@ -9743,60 +7575,6 @@
97437575 ==
97447576 [n $(imports t.imports)]
97457577::
9746−++ reserved-proj-sample
9747− |= sam=sample
9748− ^- ?
9749− ?- -.sam
9750− %bind =(name.sam %proj)
9751− %face =(name.sam %proj)
9752− %pun =(name.sam %proj)
9753− %cell (lien items.sam reserved-proj-sample)
9754− * |
9755− ==
9756−++ reserved-proj-pattern
9757− |= p=pattern
9758− ^- ?
9759− ?- -.p
9760− %bind =(name.p %proj)
9761− %cell (lien items.p reserved-proj-pattern)
9762− * |
9763− ==
9764−++ reserved-proj-def
9765− |= d=def
9766− ^- ?
9767− ?: =(name.d %proj) &
9768− ?: ?=(%value -.d) (reserved-proj-expr val.d)
9769− |
9770−++ reserved-proj-expr
9771− |= e=expr
9772− ^- ?
9773− ?- -.e
9774− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
9775− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
9776− %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
9777− %pair $(e val.e)
9778− %unit $(e val.e)
9779− %group $(e inner.e)
9780− %list (lien items.e reserved-proj-expr)
9781− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
9782− ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
9783− %cast $(e val.e)
9784− %call |($(e head.e) (lien args.e reserved-proj-expr))
9785− %trace |($(e val.e) $(e then.e))
9786− %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
9787− %body |((lien defs.e reserved-proj-def) $(e final.e))
9788− * |
9789− ==
9790−::
9791−++ module-has-reserved-proj
9792− |= mod=module
9793− ^- ?
9794− =/ imported=(list term) (import-binding-names imports.mod)
9795− =/ vals=(list term) (global-value-names defs.mod)
9796− =/ molds=imolds (collect-simple-molds defs.mod)
9797− =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9798− |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
9799−::
98007578++ module-scope-valid
98017579 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
98027580 ^- ?
@@ -9804,7 +7582,6 @@
98047582 =/ vals=(list term) (global-value-names defs.mod)
98057583 =/ molds=imolds (collect-simple-molds defs.mod)
98067584 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9807− ?: (module-has-reserved-proj mod) |
98087585 ?. %+ levy imported
98097586 |= n=term
98107587 &((unique-value-name n imported) !(lien vals |=(v=term =(n v))) !(lien mold-names |=(m=term =(n m))) !(lien prelude-values |=(v=term =(n v))) !(lien prelude-molds |=(m=term =(n m))))
@@ -9812,22 +7589,6 @@
98127589 ?. (levy vals |=(n=term &((unique-value-name n vals) !(lien prelude-values |=(v=term =(n v)))))) |
98137590 (levy mold-names |=(n=term &((unique-value-name n mold-names) !(lien prelude-molds |=(m=term =(n m))))))
98147591::
9815−:: In an API file or before main's kind is known, a lone `+$ poke`
9816−:: may be a declaration rather than a mold that shadows the prelude. Do not call
9817−:: that one collision definite, and do not hide unrelated scope errors.
9818−++ pending-declared-poke
9819− |= [at=path mod=module prelude-values=(list term) prelude-molds=(list term)]
9820− ^- ?
9821− ?. (lien prelude-molds |=(n=term =(%poke n))) |
9822− ?. |(?=([%ui %api @ %jibb ~] at) (lien defs.mod |=(d=def &(?=(%value -.d) =(%main name.d))))) |
9823− =/ pokes=(list def)
9824− (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
9825− ?~ pokes |
9826− ?^ t.pokes |
9827− =/ remaining=(list def)
9828− (skim defs.mod |=(d=def !&(?=(%mold -.d) =(%poke name.d))))
9829− (module-scope-valid mod(defs remaining) prelude-values prelude-molds)
9830−::
98317592++ module-mold-types
98327593 |= [molds=imolds state=istate]
98337594 ^- (each imold-types @t)
@@ -9843,9 +7604,9 @@
98437604::
98447605:: Prepare a provisional interface from the trusted vendored source.
98457606:: Every declared name remains reserved, but only molds and values this
9846−:: fragment can infer are usable. Unsupported bodies are not validated.
9847−:: An optional internal source supplies the prelude's one supported import;
9848−:: clients cannot import that path directly. Named unions retain their origin.
7607+:: fragment can infer are usable. Unsupported bodies are not validated,
7608+:: and imports into the prelude are not supported yet. The fixed origin
7609+:: gives its named unions the same identity in every importing module.
98497610::
98507611:: Recognize only the complete standard prelude list shape. Its recursive
98517612:: tail uses the same parameter and the unqualified list name. The reader
@@ -9885,14 +7646,6 @@
98857646 ?. ?=(%tvar -.i.args.tail) |
98867647 =(var name.i.args.tail)
98877648::
9888−++ prelude-label
9889− |= [typ=itype name=term]
9890− ^- itype
9891− ?: ?=(%jrec -.typ) typ(label `name)
9892− ?. ?=(%union -.typ) typ
9893− ?^ args.typ typ
9894− typ(label `name)
9895−::
98967649++ partial-prelude-molds
98977650 |= [molds=imolds state=istate]
98987651 ^- imold-types
@@ -9905,72 +7658,22 @@
99057658 (infer-mold-template body.m state(active [name.m active.state], in-mold &))
99067659 ?~ out $(molds t.molds)
99077660 =. typ.template.u.out (label-direct-union typ.template.u.out body.m name.m state)
9908− =. typ.template.u.out (prelude-label typ.template.u.out name.m)
99097661 [[name.m template.u.out] $(molds t.molds)]
99107662::
9911−:: A compiler-owned interface available only to the dedicated
9912−:: internal-prelude preparation path, never the ordinary module resolver.
9913−++ private-primitive-interface
9914− ^- ifile
9915− =/ a=itype [%avar 0]
9916− =/ pair=itype [%cell a a]
9917− =/ greater=ischeme [[%fn pair [%flag ~]] ~[0]]
9918− [~[[%raw-gth greater]] ~ /lib/jibb/primitives/jibb ~ ~ ~ ~]
9919−::
9920−++ infer-private-internal
7663+++ partial-prelude-interface
99217664 |= src=@t
99227665 ^- (unit ifile)
9923− =/ at=path /lib/jibb/internal/jibb
9924− =/ parsed (parse at src)
9925− ?: ?=(%| -.parsed) ~
9926− =/ mod=module p.parsed
9927− ?^ (duplicate-defs defs.mod) ~
9928− ?~ imports.mod
9929− =/ built=jfile-result (infer-jibb-file at src ~ ~ ~ ~[at] ~ ~ ~ ~)
9930− ?: ?=(%| -.built) ~
9931− `iface.p.built
9932− ?. ?=([[%jibb *] ~] imports.mod) ~
9933− ?. =(path.i.imports.mod /lib/jibb/primitives) ~
9934− ?. (module-scope-valid mod ~ ~) ~
9935− =/ vals=(list term) (global-value-names defs.mod)
9936− ?: (lien vals |=(n=term =(n %main))) ~
9937− =/ molds=imolds (collect-simple-molds defs.mod)
9938− =/ globals=(list term) (weld (import-binding-names imports.mod) vals)
9939− =/ js=ijimports ~[[face.i.imports.mod private-primitive-interface]]
9940− =/ reserved=(list term) ~[face.i.imports.mod]
9941− =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9942− =/ state=istate [0 ~ ~ ~ molds globals ~ ~ ~ ~ js reserved ~ ~ ~ | at top ~ ~ 256 ~]
9943− =/ mts=(each imold-types @t) (module-mold-types molds state)
9944− ?: ?=(%| -.mts) ~
9945− =/ resolution=iresolved (resolve-groups defs.mod molds globals ~ ~ ~ ~ js reserved at ~)
9946− =/ env=ienv env.resolution
9947− ?. (module-values-complete defs.mod env) ~
9948− `[env p.mts at ~ artifacts.resolution ~ `src]
9949−::
9950−++ partial-prelude-interface-with-internal
9951− |= [src=@t internal-source=(unit @t)]
9952− ^- (unit ifile)
99537666 ?: =(0 src) ~
99547667 =/ at=path /lib/jibb/prelude/jibb
99557668 =/ parsed (parse at src)
99567669 ?: ?=(%| -.parsed) ~
9957− ?: (named-mold-has-hole defs.p.parsed) ~
9958− ?^ (duplicate-defs defs.p.parsed) ~
9959− =/ private=(unit ijimports)
9960− ?~ imports.p.parsed `~
9961− ?. ?=([[%jibb *] ~] imports.p.parsed) ~
9962− ?. =(path.i.imports.p.parsed /lib/jibb/internal) ~
9963− ?~ internal-source ~
9964− =/ built=(unit ifile) (infer-private-internal u.internal-source)
9965− ?~ built ~
9966− `~[[face.i.imports.p.parsed u.built]]
9967− ?~ private ~
7670+ ?^ imports.p.parsed ~
99687671 ?~ defs.p.parsed ~
99697672 ?. (module-scope-valid p.parsed ~ ~) ~
99707673 =/ ds=(list def) defs.p.parsed
99717674 =/ molds=imolds (collect-simple-molds ds)
99727675 =/ names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
9973− =/ globals=(list term) (weld (import-binding-names imports.p.parsed) (global-value-names ds))
7676+ =/ globals=(list term) (global-value-names ds)
99747677 :: Remove raw list before inferring any template, so an altered list
99757678 :: cannot leak through an alias. Its name remains reserved either way.
99767679 =/ declared=? (lien names |=(name=term =(%list name)))
@@ -9978,38 +7681,11 @@
99787681 =? env-molds declared
99797682 (skim molds |=(m=[name=term body=shape] !=(%list name.m)))
99807683 =/ reserved=(list term) ?:(declared ~[%list] ~)
9981− =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ u.private reserved ~ ~ ~ | at names ~ ~ 256 ~]
9982− :: Other prelude molds may use list only after its source has passed
9983− :: the standard-list check. The raw declaration remains removed.
9984− =/ declared-list=(unit shape) (find-simple-mold %list molds)
9985− =/ mold-prelude=(unit ifile)
9986− ?~ declared-list ~
9987− ?. (standard-prelude-list u.declared-list) ~
9988− `[~ ~[[%list [[%collection %list ~[[%var 0]]] ~[0]]]] at ~ ~ ~ ~]
9989− =/ mt=imold-types (partial-prelude-molds molds state(prelude mold-prelude))
9990− =/ partial=ifile [~ mt at ~ ~ ~ ~]
9991− :: An explicitly qualified re-export must resolve. Other unsupported
9992− :: prelude declarations remain reserved but absent from the interface.
9993− =/ required=imolds
9994− %+ skim molds
9995− |= m=[name=term body=shape]
9996− =/ sh=shape body.m
9997− ?. ?=(%ref -.sh) |
9998− ?~ names.sh |
9999− ?=(^ t.names.sh)
10000− ?. (levy required |=(m=[name=term body=shape] ?=(^ (find-jibb-mold name.m partial)))) ~
10001− =/ resolution=iresolved (resolve-groups ds env-molds globals ~ ~ ~ ~ u.private reserved at `partial)
10002− =/ env=ienv env.resolution
10003− ?. (hole-values-present ds env) ~
10004− =/ deps=(list iwidth-dependency)
10005− ?~ u.private ~
10006− ~[[at.interface.i.u.private source.interface.i.u.private elaborations.interface.i.u.private]]
10007− `[env mt at ~ artifacts.resolution deps `src]
10008−::
10009−++ partial-prelude-interface
10010− |= src=@t
10011− ^- (unit ifile)
10012− (partial-prelude-interface-with-internal src ~)
7684+ =/ state=istate [0 ~ ~ ~ env-molds globals ~ ~ ~ ~ ~ reserved ~ ~ ~ | at names ~]
7685+ =/ mt=imold-types (partial-prelude-molds molds state)
7686+ =/ partial=ifile [~ mt at]
7687+ =/ env=ienv (resolve-supported-defs ds env-molds globals ~ ~ ~ ~ ~ reserved at `partial)
7688+ `[env mt at]
100137689::
100147690+$ iprelude [iface=ifile values=(list term) molds=(list term)]
100157691::
@@ -10024,17 +7700,6 @@
100247700 =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
100257701 `[u.iface vals ms]
100267702::
10027−++ prepare-prelude-with-internal
10028− |= [src=@t internal-source=@t]
10029− ^- (unit iprelude)
10030− =/ iface=(unit ifile) (partial-prelude-interface-with-internal src `internal-source)
10031− ?~ iface ~
10032− =/ parsed (parse /lib/jibb/prelude/jibb src)
10033− ?: ?=(%| -.parsed) ~
10034− =/ vals=(list term) (global-value-names defs.p.parsed)
10035− =/ ms=(list term) (turn (collect-simple-molds defs.p.parsed) |=(m=[name=term body=shape] name.m))
10036− `[u.iface vals ms]
10037−::
100387703++ module-values-complete
100397704 |= [ds=(list def) env=ienv]
100407705 ^- ?
@@ -10061,10 +7726,6 @@
100617726 ?~ imports [%& [~ cache]]
100627727 ?. ?=(%jibb -.i.imports) $(imports t.imports)
100637728 =/ at=path (weld path.i.imports `path`~[%jibb])
10064− ?: =(at /lib/jibb/internal/jibb)
10065− [%| 'the prelude internal module is private']
10066− ?: =(at /lib/jibb/primitives/jibb)
10067− [%| 'the prelude primitive interface is private']
100687729 ?: (lien active |=(p=path =(p at)))
100697730 [%| (crip "import cycle at {(spud at)}")]
100707731 =/ found=jbundle (skim modules |=(m=jsource =(at at.m)))
@@ -10079,287 +7740,14 @@
100797740 ?: ?=(%| -.rest) rest
100807741 [%& [[[face.i.imports iface.p.iface] resolved.p.rest] cache.p.rest]]
100817742::
10082−:: Provisional declaration extraction only; this does not derive asks,
10083−:: validate imported types, or claim that an API module has checked.
10084−+$ iapi-path [at=span name=term segments=(list pseg) full=term diffs=(list term) scry=(unit (list pseg))]
10085−++ api-path-mark
10086− |= [sh=shape marks=(list term)]
10087− ^- (unit term)
10088− ?. ?=(%ref -.sh) ~
10089− ?. ?=([@ ~] names.sh) ~
10090− ?. (unique-value-name i.names.sh marks) ~
10091− `i.names.sh
10092−::
10093−++ api-path-diffs
10094− |= [shapes=(list shape) marks=(list term) used=(list term)]
10095− ^- (unit (list term))
10096− ?~ shapes `~
10097− =/ n=(unit term) (api-path-mark i.shapes marks)
10098− ?~ n ~
10099− ?: (lien used |=(x=term =(x u.n))) ~
10100− =/ rest=(unit (list term)) $(shapes t.shapes, used [u.n used])
10101− ?~ rest ~
10102− `[u.n u.rest]
10103−::
10104−++ api-path-payload
10105− |= [sh=shape marks=(list term)]
10106− ^- (unit [full=term diffs=(list term)])
10107− =/ direct=(unit term) (api-path-mark sh marks)
10108− ?^ direct `[u.direct ~]
10109− ?. ?=(%apply -.sh) ~
10110− ?. =(~[%facts] ref.sh) ~
10111− ?~ args.sh ~
10112− ?~ t.args.sh ~
10113− =/ full=(unit term) (api-path-mark i.args.sh marks)
10114− ?~ full ~
10115− =/ diffs=(unit (list term)) (api-path-diffs t.args.sh marks ~[u.full])
10116− ?~ diffs ~
10117− `[u.full u.diffs]
10118−::
10119−+$ iapi-parameter [name=term aura=@ta at=span]
10120−++ api-path-parameters
10121− |= [segments=(list pseg) seen=(list term)]
10122− ^- (unit (list iapi-parameter))
10123− ?~ segments `~
10124− ?: ?=(%knot -.i.segments) $(segments t.segments)
10125− =/ seg=pseg i.segments
10126− ?. ?=(%typed -.seg) ~
10127− ?: =(0 aura.seg) ~
10128− ?: (lien seen |=(n=term =(n name.seg))) ~
10129− =/ rest=(unit (list iapi-parameter)) $(segments t.segments, seen [name.seg seen])
10130− ?~ rest ~
10131− `[[name.seg aura.seg at.seg] u.rest]
10132−::
10133−++ api-scry-parameters-compatible
10134− |= [scry=(list iapi-parameter) watch=(list iapi-parameter)]
10135− ^- ?
10136− ?~ scry &
10137− ?. (lien watch |=(p=iapi-parameter &(=(name.p name.i.scry) =(aura.p aura.i.scry)))) |
10138− $(scry t.scry)
10139−::
10140−++ api-path-one
10141− |= [sh=shape marks=(list term)]
10142− ^- (unit iapi-path)
10143− ?. ?=(%cell -.sh) ~
10144− =/ fs=(list field) fields.sh
10145− ?~ fs ~
10146− ?~ t.fs ~
10147− ?~ t.t.fs ~
10148− ?: (gth (lent fs) 4) ~
10149− ?. ?=(%bare -.i.fs) ~
10150− =/ tag=shape shape.i.fs
10151− ?. ?=(%const -.tag) ~
10152− ?. =(%term form.lit.tag) ~
10153− =/ name=term val.lit.tag
10154− ?. (jibb-face-name name) ~
10155− ?. ?=(%bare -.i.t.fs) ~
10156− =/ path-shape=shape shape.i.t.fs
10157− ?. ?=(%path -.path-shape) ~
10158− ?. ?=(%bare -.i.t.t.fs) ~
10159− =/ payload=(unit [full=term diffs=(list term)]) (api-path-payload shape.i.t.t.fs marks)
10160− ?~ payload ~
10161− =/ scry=(unit (unit (list pseg)))
10162− ?~ t.t.t.fs `~
10163− =/ entry=field i.t.t.t.fs
10164− ?. ?=(%face -.entry) ~
10165− ?. =(%scry name.entry) ~
10166− ?. ?=(%path -.shape.entry) ~
10167− ``segs.shape.entry
10168− ?~ scry ~
10169− =/ params=(unit (list iapi-parameter)) (api-path-parameters segs.path-shape ~)
10170− ?~ params ~
10171− ?^ u.scry
10172− =/ scry-params=(unit (list iapi-parameter)) (api-path-parameters u.u.scry ~)
10173− ?~ scry-params ~
10174− ?. (api-scry-parameters-compatible u.scry-params u.params) ~
10175− `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
10176− `[at.sh name segs.path-shape full.u.payload diffs.u.payload u.scry]
10177−::
10178−++ api-path-many
10179− |= [shapes=(list shape) marks=(list term) seen=(list term)]
10180− ^- (unit (list iapi-path))
10181− ?~ shapes `~
10182− =/ one=(unit iapi-path) (api-path-one i.shapes marks)
10183− ?~ one ~
10184− ?: (lien seen |=(n=term =(n name.u.one))) ~
10185− =/ rest=(unit (list iapi-path)) $(shapes t.shapes, seen [name.u.one seen])
10186− ?~ rest ~
10187− `[u.one u.rest]
10188−::
10189−++ api-path-declaration
10190− |= [sh=shape marks=(list term)]
10191− ^- (unit (list iapi-path))
10192− ?: ?=(%union -.sh) (api-path-many cases.sh marks ~)
10193− (api-path-many ~[sh] marks ~)
10194−::
10195−:: Derived gates share the value namespace. /% marks name molds; /- and
10196−:: /= also introduce faces that cannot be shadowed by a derived value.
10197−++ api-import-faces
10198− |= imports=(list import)
10199− ^- (list term)
10200− ?~ imports ~
10201− ?- -.i.imports
10202− %mark $(imports t.imports)
10203− %sur [name.i.imports $(imports t.imports)]
10204− %jibb [face.i.imports $(imports t.imports)]
10205− ==
10206−::
10207−++ api-derived-names-valid
10208− |= [paths=(list iapi-path) poke-names=(list term) mod=module prelude-values=(list term)]
10209− ^- ?
10210− =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
10211− =/ derived=(list term) (weld path-names poke-names)
10212− ?: (lien derived |=(n=term =(n %proj))) |
10213− =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
10214− (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
10215−::
10216−:: Analysis only. Successful external entries must be unchanged results
10217−:: produced for the declared marks; no request interface is produced.
10218−+$ iapi-mark-type [name=term typ=itype]
10219−+$ iapi-path-typed [path=iapi-path full=itype diffs=(list iapi-mark-type)]
10220−++ api-diff-types
10221− |= [names=(list term) externals=imark-externals declared=(list term)]
10222− ^- (unit (list iapi-mark-type))
10223− ?~ names `~
10224− =/ typ=(unit itype) (find-imported-mark i.names externals declared)
10225− ?~ typ ~
10226− =/ tail=(unit (list iapi-mark-type)) $(names t.names)
10227− ?~ tail ~
10228− `[[i.names u.typ] u.tail]
10229−::
10230−++ api-path-types
10231− |= [paths=(list iapi-path) externals=imark-externals declared=(list term)]
10232− ^- (unit (list iapi-path-typed))
10233− ?~ paths `~
10234− =/ full=(unit itype) (find-imported-mark full.i.paths externals declared)
10235− ?~ full ~
10236− =/ diffs=(unit (list iapi-mark-type)) (api-diff-types diffs.i.paths externals declared)
10237− ?~ diffs ~
10238− =/ tail=(unit (list iapi-path-typed)) $(paths t.paths)
10239− ?~ tail ~
10240− `[[i.paths u.full u.diffs] u.tail]
10241−::
10242−++ api-poke-mark-names
10243− |= [pokes=(list def) declared=(list term)]
10244− ^- (unit (list term))
10245− ?~ pokes `~
10246− ?^ t.pokes ~
10247− =/ d=def i.pokes
10248− ?. ?=(%mold -.d) ~
10249− =/ sh=shape shape.d
10250− ?: ?=(%union -.sh) (api-path-diffs cases.sh declared ~)
10251− =/ name=(unit term) (api-path-mark sh declared)
10252− ?~ name ~
10253− `~[u.name]
10254−::
10255−++ api-path-analysis
10256− |= [mod=module externals=imark-externals prelude-values=(list term) prelude-molds=(list term)]
10257− ^- (unit (list iapi-path-typed))
10258− ?: (lien defs.mod def-has-hole) ~
10259− ?^ (duplicate-defs defs.mod) ~
10260− =/ ds=(list def) defs.mod
10261− =/ declarations=(list def)
10262− (skim ds |=(d=def &(?=(%mold -.d) =(%paths name.d))))
10263− ?. ?=([* ~] declarations) ~
10264− =/ pokes=(list def)
10265− (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
10266− ?: (gth (lent pokes) 1) ~
10267− =/ ordinary=(list def)
10268− (skim ds |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
10269− ?. (module-scope-valid mod(defs ordinary) prelude-values prelude-molds) ~
10270− =/ declared=(list term) (collect-mark-imports imports.mod)
10271− =/ poke-names=(unit (list term)) (api-poke-mark-names pokes declared)
10272− ?~ poke-names ~
10273− =/ decl=def i.declarations
10274− ?> ?=(%mold -.decl)
10275− =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
10276− ?~ paths ~
10277− ?. (api-derived-names-valid u.paths u.poke-names mod prelude-values) ~
10278− (api-path-types u.paths externals declared)
10279−::
10280−:: Source/graph entry for path analysis only. The returned paths retain
10281−:: reader-derived mark types and import resolution has checked reachable
10282−:: Jibb dependencies. This is not an API interface or a module check.
10283−++ api-path-analysis-source
10284− |= [file=path src=@t externals=iexternals marks=imark-externals modules=jbundle prepared=(unit iprelude)]
10285− ^- (each (list iapi-path-typed) @t)
10286− ?. ?=([%ui %api @ %jibb ~] file) [%| 'API path analysis requires /ui/api/<agent>.jibb']
10287− =/ parsed (parse file src)
10288− ?: ?=(%| -.parsed) [%| 'API path source does not parse']
10289− =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10290− ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
10291− ?~ prepared [%| 'API path analysis needs the prepared prelude']
10292− =/ prelude=(unit ifile) `iface.u.prepared
10293− =/ deps=jimports-result
10294− (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
10295− ?: ?=(%| -.deps) [%| p.deps]
10296− =/ paths=(unit (list iapi-path-typed))
10297− (api-path-analysis p.parsed marks values.u.prepared molds.u.prepared)
10298− ?~ paths [%| 'API path declaration needs unsupported analysis']
10299− [%& u.paths]
10300−::
10301−++ api-mark-exports
10302− |= [marks=(list term) all=(list term) externals=imark-externals]
10303− ^- imold-types
10304− ?~ marks ~
10305− =/ t=(unit itype) (find-imported-mark i.marks externals all)
10306− ?~ t $(marks t.marks)
10307− [[i.marks [u.t ~]] $(marks t.marks)]
10308−::
10309−:: Experimental direct poke-only API. Unsupported API declarations fail
10310−:: as a whole; supplied mark reader results retain their existing boundary.
10311−++ api-poke-interface
10312− |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
10313− ^- (unit ifile)
10314− ?: (lien defs.mod def-has-hole) ~
10315− ?. ?=([%ui %api @ %jibb ~] at) ~
10316− ?^ (duplicate-defs defs.mod) ~
10317− ?~ prelude ~
10318− ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
10319− =/ poke=(unit ischeme) (find-jibb-mold %poke u.prelude)
10320− ?~ poke ~
10321− ?. ?=(%union -.typ.u.poke) ~
10322− ?^ vars.u.poke ~
10323− =/ compatible=?
10324− %+ lien cases.typ.u.poke
10325− |= c=itype
10326− ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
10327− ?. compatible ~
10328− ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
10329− ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
10330− =/ marks=(list term) (collect-mark-imports imports.mod)
10331− ?. ?=([@ ~] marks) ~
10332− =/ ds=(list def) defs.mod
10333− ?. ?=([[%mold *] ~] ds) ~
10334− ?. =(%poke name.i.ds) ~
10335− =/ sh=shape shape.i.ds
10336− ?. ?=([%ref *] sh) ~
10337− ?. ?=([@ ~] names.sh) ~
10338− =/ n=term i.names.sh
10339− ?. (unique-value-name n marks) ~
10340− ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
10341− =/ mark=(unit itype) (find-imported-mark n mark-externals marks)
10342− ?~ mark ~
10343− =/ sc=ischeme [[%fn u.mark typ.u.poke] ~]
10344− `[~[[n sc]] (api-mark-exports marks marks mark-externals) at ~[[n i.t.t.at n]] ~ ~ ~]
10345−::
103467743++ infer-jibb-file
103477744 |= [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)]
103487745 ^- jfile-result
7746+ ?: ?=([%ui %api *] at) [%| (crip "API module needs unsupported inference: {(spud at)}")]
103497747 =/ parsed (parse at src)
103507748 ?: ?=(%| -.parsed) [%| (crip "module source does not parse: {(spud at)}")]
103517749 =/ mod=module p.parsed
10352− =/ duplicate=(unit idiag) (duplicate-defs defs.mod)
10353− ?^ duplicate [%| (show-duplicate-fields at src u.duplicate)]
10354− ?: ?=([%ui %api *] at)
10355− =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
10356− ?~ iface [%| (crip "API module needs unsupported inference: {(spud at)}")]
10357− =/ checked=ifile u.iface(source `src)
10358− [%& [checked [[at checked] cache]]]
10359− ?. (module-scope-valid mod prelude-values prelude-molds)
10360− ?: (pending-declared-poke at mod prelude-values prelude-molds)
10361− [%| (crip "module kind or scope needs unsupported inference: {(spud at)}")]
10362− [%| (crip "module has conflicting names: {(spud at)}")]
7750+ ?. (module-scope-valid mod prelude-values prelude-molds) [%| (crip "module has conflicting names: {(spud at)}")]
103637751 =/ vals=(list term) (global-value-names defs.mod)
103647752 ?: (lien vals |=(n=term =(n %main)))
103657753 [%| (crip "module kind needs unsupported inference: {(spud at)}")]
@@ -10371,15 +7759,13 @@
103717759 =/ marks=(list term) (collect-mark-imports imports.mod)
103727760 =/ reserved=(list term) (weld prelude-molds (turn resolved.p.js |=(j=[face=term interface=ifile] face.j)))
103737761 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10374− =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude ~ 256 ~]
7762+ =/ state=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks resolved.p.js reserved ~ ~ ~ | at top prelude]
103757763 =/ mts=(each imold-types @t) (module-mold-types molds state)
103767764 ?: ?=(%| -.mts) [%| (crip "{(trip p.mts)}: {(spud at)}")]
10377− =/ resolution=iresolved (resolve-groups defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
10378− =/ env=ienv env.resolution
7765+ =/ env=ienv (resolve-supported-defs defs.mod molds globals externals surs mark-externals marks resolved.p.js reserved at prelude)
103797766 ?. (module-values-complete defs.mod env)
103807767 [%| (crip "module definitions need unsupported inference: {(spud at)}")]
10381− =/ iface=ifile [env p.mts at ~ artifacts.resolution ~ `src]
10382− [%& [iface [[at iface] cache.p.js]]]
7768+ [%& [[env p.mts at] [[at [env p.mts at]] cache.p.js]]]
103837769::
103847770:: +golden-types-with-modules fails closed for imports without prelude
103857771:: scope. +golden-types-with-prelude resolves supported library graphs;
@@ -10390,8 +7776,6 @@
103907776 ^- @t
103917777 =/ parsed (parse file src)
103927778 ?: ?=(%| -.parsed) (show-error src p.parsed)
10393− =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10394− ?^ duplicate (duplicate-fields-report file src u.duplicate)
103957779 ?: (lien imports.p.parsed |=(i=import ?=(%jibb -.i)))
103967780 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
103977781 (golden-types-with-marks file src externals mark-externals)
@@ -10406,8 +7790,6 @@
104067790 ^- @t
104077791 =/ parsed (parse file src)
104087792 ?: ?=(%| -.parsed) (show-error src p.parsed)
10409− =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10410− ?^ duplicate (duplicate-fields-report file src u.duplicate)
104117793 ?: =(0 prelude-source) 'partial inference; module not checked\0aprelude source missing; module import inference unsupported'
104127794 =/ prelude (parse /lib/jibb/prelude/jibb prelude-source)
104137795 ?: ?=(%| -.prelude) 'partial inference; module not checked\0aprelude source does not parse; module import inference unsupported'
@@ -10415,26 +7797,16 @@
104157797 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
104167798 (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
104177799::
10418−++ golden-types-with-prelude-and-internal
10419− |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prelude-source=@t internal-source=@t]
10420− ^- @t
10421− =/ prepared=(unit iprelude) (prepare-prelude-with-internal prelude-source internal-source)
10422− (golden-types-with-prepared-prelude file src externals mark-externals modules prepared)
10423−::
104247800++ golden-types-with-prepared-prelude
104257801 |= [file=path src=@t externals=iexternals mark-externals=imark-externals modules=jbundle prepared=(unit iprelude)]
104267802 ^- @t
104277803 =/ parsed (parse file src)
104287804 ?: ?=(%| -.parsed) (show-error src p.parsed)
10429− =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10430− ?^ duplicate (duplicate-fields-report file src u.duplicate)
104317805 ?~ prepared 'partial inference; module not checked\0aprelude interface is not supported'
104327806 =/ prelude-values=(list term) values.u.prepared
104337807 =/ prelude-molds=(list term) molds.u.prepared
104347808 =/ iface=(unit ifile) `iface.u.prepared
104357809 ?. (module-scope-valid p.parsed prelude-values prelude-molds)
10436− ?: (pending-declared-poke file p.parsed prelude-values prelude-molds)
10437− 'partial inference; module not checked\0amodule kind or scope needs unsupported inference'
104387810 'partial inference; module not checked\0amodule has conflicting names'
104397811 =/ js=jimports-result
104407812 (resolve-jibb-imports imports.p.parsed externals mark-externals modules ~[file] prelude-values prelude-molds ~ iface)
@@ -10475,18 +7847,12 @@
104757847 =. reserved-molds (weld reserved-molds (turn jimports |=(j=[face=term interface=ifile] face.j)))
104767848 =/ parsed (parse file src)
104777849 ?: ?=(%| -.parsed) (show-error src p.parsed)
10478− =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
10479− ?^ duplicate (duplicate-fields-report file src u.duplicate)
10480− ?: (module-has-reserved-proj p.parsed)
10481− 'module has reserved proj name'
104827850 =/ ds=(list def) defs.p.parsed
104837851 =/ molds=imolds (collect-simple-molds ds)
104847852 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
104857853 =/ surs=(list term) (collect-sur-imports imports.p.parsed)
104867854 =/ marks=(list term) (collect-mark-imports imports.p.parsed)
10487− =/ resolution=iresolved (resolve-groups ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
10488− =/ cycles=(list icycle) (definite-value-cycles ds globals)
10489− =/ env=ienv env.resolution
7855+ =/ env=ienv (resolve-supported-defs ds molds globals externals surs mark-externals marks jimports reserved-molds file prelude)
104907856 =/ lines=(list @t) ~
104917857 |-
104927858 ?~ ds (of-wain:format ['partial inference; module not checked' (flop lines)])
@@ -10495,18 +7861,8 @@
104957861 $(ds t.ds, lines [(show-partial-mold file src d molds) lines])
104967862 ?. (unique-value-name name.d globals)
104977863 $(ds t.ds, lines [(crip "++ {(trip name.d)}: name already in scope") lines])
10498− =/ cycle=(list icycle) (skim cycles |=(c=icycle =(name.c name.d)))
10499− ?^ cycle
10500− =/ diag=idiag ["non-gate value depends on itself through a cycle" ~[[first.i.cycle "value in cycle"] [next.i.cycle "dependency in cycle"]]]
10501− $(ds t.ds, lines [(show-inference-diagnostic file src name.d diag) lines])
10502− ?: (lien grouped.resolution |=(n=term =(n name.d)))
10503− =/ found=(unit ischeme) (ienv-lookup name.d env)
10504− ?~ found $(ds t.ds, lines [(crip "++ {(trip name.d)}: recursive group unavailable") lines])
10505− =/ typ=itype (canonical-itype typ.u.found vars.u.found)
10506− =/ line=@t (crip "++ {(trip name.d)}: {(show-itype typ ~)}{(show-atom-constraint typ)}")
10507− $(ds t.ds, lines [line lines])
105087864 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10509− =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude ~ 256 ~]
7865+ =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | file top prelude]
105107866 =. initial (reserve-def-caps val.d initial)
105117867 =/ result=iresult
105127868 ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
@@ -10514,10 +7870,6 @@
105147870 (infer-fragment val.d env initial)
105157871 ?: ?=(%| -.result)
105167872 $(ds t.ds, lines [(show-inference-diagnostic file src name.d p.result) lines])
10517− =. state.p.result (default-hole-numbers holes.state.p.result holes.initial state.p.result env !(itype-has-gate (itype-normalize typ.p.result sub.state.p.result)))
10518− =/ hole=(unit idiag) (unresolved-hole holes.state.p.result holes.initial state.p.result)
10519− ?^ hole
10520− $(ds t.ds, lines [(show-inference-diagnostic file src name.d u.hole) lines])
105217873 =/ merged=(unit [first=icap second=icap])
105227874 (merged-capitals caps.state.p.result sub.state.p.result)
105237875 ?^ merged
@@ -10540,8 +7892,6 @@
105407892 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
105417893 ?: (gth (lent vars) 26)
105427894 $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
10543− ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
10544− $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
105457895 =/ printable=itype (canonical-itype typ vars)
105467896 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
105477897 $(ds t.ds, lines [line lines])