@@ -63,8 +63,8 @@
63:: finds each node's end from the tokens alone, matching each opener
63:: finds each node's end from the tokens alone, matching each opener
64:: with its closer on the line, so a node that stops at a child where
64:: with its closer on the line, so a node that stops at a child where
65:: its closer follows fails it, and +check-spans-test plants such
65:: its closer follows fails it, and +check-spans-test plants such
66−:: wrong ends to show that it does (tools/hoon check-spans-test prints
66+:: wrong ends to show that it does (the jibb-check-spans test suite
67−:: the empty list, <<>>, when it passes).
67+:: runs it).
69:: ===================================================================
69:: ===================================================================
70:: 2. The layout pass (+layout)
70:: 2. The layout pass (+layout)
@@ -206,9 +206,11 @@
206:: token holds the text after @. An aura starting @s or
206:: token holds the text after @. An aura starting @s or
207:: @r is an error at 2nd: "signed and floating-point
207:: @r is an error at 2nd: "signed and floating-point
208:: auras are left out of Jibb"
208:: auras are left out of Jibb"
209−:: A-Z type variable: one capital. A letter or digit right
209+:: A-Z type variable [A-Z][a-z0-9]*: a capital, then
210+:: lowercase letters and digits, as M, Msg or T2. Right
211+:: after it, which is emitted first, a capital, _ or -
210−:: after it is an error there, "a type variable is one
212+:: is an error there, "a type variable is a capital,
211−:: capital letter", after the type variable's token
213+:: then lowercase letters and digits"
212:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names
214:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names
213:: joined by dots. Right after the name or wing, which
215:: joined by dots. Right after the name or wing, which
214:: is emitted first, a capital or _ is an error there,
216:: is emitted first, a capital or _ is an error there,
@@ -405,6 +407,7 @@
405:: Why: after the layout pass the grammar is LL(2). Each choice is made by
407:: Why: after the layout pass the grammar is LL(2). Each choice is made by
406:: the next token, at most with the one after it and whether it is tight:
408:: the next token, at most with the one after it and whether it is tight:
407:: name, then = tight a face (items, lines, fields, samples)
409:: name, then = tight a face (items, lines, fields, samples)
410+:: wing, then = tight a change's item or line, wing=value
408:: name, then + tight a pair
411:: name, then + tight a pair
409:: name or wing, then ( tight a change
412:: name or wing, then ( tight a change
410:: |=, then a term tight a constructor; else, where an
413:: |=, then a term tight a constructor; else, where an
@@ -412,6 +415,9 @@
412:: ++ or +$ a definition; else a body's final expr
415:: ++ or +$ a definition; else a body's final expr
413:: INDENT a body, an open bracket's lines, arms
416:: INDENT a body, an open bracket's lines, arms
414:: or cases; else the expression goes on
417:: or cases; else the expression goes on
418+:: NEWLINE, after a rune's head the rest of the body, on a body's
419+:: or ?-'s subject final line (The rest of a body);
415:: So the parser never backtracks, its first failure is its furthest, and
421:: So the parser never backtracks, its first failure is its furthest, and
416:: "expected X, found Y" falls out of each arm without tracking failures
422:: "expected X, found Y" falls out of each arm without tracking failures
417:: across alternatives. Hoon's combinators read tapes of characters and
423:: across alternatives. Hoon's combinators read tapes of characters and
@@ -455,7 +461,9 @@
455:: cases below -> %mold; one case is that mold, several
461:: cases below -> %mold; one case is that mold, several
456:: are %union. The optional generic wraps either in %generic.
462:: are %union. The optional generic wraps either in %generic.
457:: ++ name expr or body -> %value (a body becomes a %body expr)
463:: ++ name expr or body -> %value (a body becomes a %body expr)
458−:: body INDENT { definition NEWLINE } expr DEDENT -> %body
464+:: body INDENT rest DEDENT; rest is { definition NEWLINE } last
465+:: -> %body, and last is expr, or the rest of a body that
466+:: a rune on its final line took (The rest of a body)
459:: call one operand is that operand; more -> %call head args
467:: call one operand is that operand; more -> %call head args
460:: operand literal -> %lit or %str; pathlit -> %path, as a path
468:: operand literal -> %lit or %str; pathlit -> %path, as a path
461:: literal is an expression (Decisions); !! -> %crash, as
469:: literal is an expression (Decisions); !! -> %crash, as
@@ -472,7 +480,9 @@
472:: that line, as () is no group. A ( followed by a rune is
480:: that line, as () is no group. A ( followed by a rune is
473:: the closed form. Lines of an open group or list take no
481:: the closed form. Lines of an open group or list take no
474:: name= (doc question)
482:: name= (doc question)
475−:: change every item and line has name= (the EBNF's "items named")
483+:: change every item and line has name= or wing=, as open.cart=
484+:: (the EBNF's edit) -> %change of edits, each with its
485+:: names as written; a tuple's item takes no wing=
476:: rune |= -> %gate; ^- -> %cast; ~& -> %trace; ?- -> %branch.
486:: rune |= -> %gate; ^- -> %cast; ~& -> %trace; ?- -> %branch.
477:: !! is an operand, not a rune (Decisions): alone where an
487:: !! is an operand, not a rune (Decisions): alone where an
478:: expression goes it is a call of one operand, and !! a
488:: expression goes it is a call of one operand, and !! a
@@ -553,7 +563,23 @@
553:: - Local definitions: at the start of any body, a gate's, an arm's,
563:: - Local definitions: at the start of any body, a gate's, an arm's,
554:: a ^-'s, a ~&'s or a ++'s, as the EBNF's body takes them
564:: a ^-'s, a ~&'s or a ++'s, as the EBNF's body takes them
555:: (Decisions); +$ as well as ++, as the Runes prose's "likewise"
565:: (Decisions); +$ as well as ++, as the Runes prose's "likewise"
556−:: says.
566+:: says. The rest of a body is a body too, so it takes them.
567+:: - The rest of a body (decided 2026-11-03, syntax review S2): a
568+:: body's final line is read with a flag, fin (+read-last), that
569+:: passes down the chain of runes on the line, as ^- @ud ~& x, while
570+:: nothing on the line is left open. A rune whose last child would
571+:: go next, and finds NEWLINE there, takes the lines after it at its
572+:: depth as that child, a body of its own (+read-rest); a ?- that
573+:: begins the line takes them as its arms (+read-branch). The flag
574+:: is off everywhere else: in a bracket, on an arm's line, for a
575+:: definition's own expression, and for a ?- after a rune on the
576+:: line, so ^- @ud ?- x keeps its arms deeper. A line nothing takes
577+:: is an error as before. A rest ends at its body's DEDENT, which
578+:: +read-rest leaves for whatever opened the body, so one DEDENT
579+:: ends every rest nested on that body's lines. Each rest is a level
580+:: of nesting, so the stack grows with them, as with brackets: a
581+:: body of 20.000 ~& x lines at one depth parses, and one of 40.000
582+:: runs out of memory, where 40.000 nested parentheses don't.
557:: - Where errors point: the doc says only "line, column and an
583:: - Where errors point: the doc says only "line, column and an
558:: excerpt"; 2.0 and Errors below say where.
584:: excerpt"; 2.0 and Errors below say where.
@@ -604,11 +630,12 @@
604:: found the end of the line" (+fail-space). No later line can give
630:: found the end of the line" (+fail-space). No later line can give
605:: a tight form its next token. A wing and a ( after a space are no
631:: a tight form its next token. A wing and a ( after a space are no
606:: error: that is a call; nor is / or %/ alone, a whole path. A
632:: error: that is a call; nor is / or %/ alone, a whole path. A
607−:: change's item is name=, so a name there with no = right after it
633+:: change's item is name= or wing=, so a name or a wing there with
608−:: fails just past the name, whatever follows: `m(b c)` at the
634+:: no = right after it fails just past it, whatever follows: `m(b c)`
609−:: space, `m(b)` at the ), `m(a"x)` at the " with the layout pass's
635+:: and `m(a.b 1)` at the space, `m(b)` at the ), `m(a"x)` at the "
610−:: message after the parser's (+unnamed, +moved). `m(a==1)` has its
636+:: with the layout pass's message after the parser's (+unnamed,
611−:: =, and fails at the second, where the layout pass does.
637+:: +moved). `m(a==1)` has its =, and fails at the second, where the
612:: - Where the place needs text on its own line and the line ends,
639:: - Where the place needs text on its own line and the line ends,
613:: whatever line comes next: at the end of that line, just past its
640:: whatever line comes next: at the end of that line, just past its
614:: last token, "found the end of the line" (+fail-line), as no later
641:: last token, "found the end of the line" (+fail-line), as no later
@@ -786,7 +813,9 @@
786:: (value 8:1 init
813:: (value 8:1 init
787:: (cast 8:9
814:: (cast 8:9
788:: (ref 8:12 state)
815:: (ref 8:12 state)
789−:: (tuple 8:18 (lit 8:19 ~) (lit 8:21 %.n))))
816+:: (tuple 8:18
817+:: (face 8:19 items (lit 8:25 ~))
818+:: (face 8:27 open (lit 8:32 %.n)))))
790:: (value 9:1 update
819:: (value 9:1 update
791:: (gate 9:11
820:: (gate 9:11
792:: (cell 9:14
821:: (cell 9:14
@@ -795,17 +824,17 @@
795:: (body 10:3
824:: (body 10:3
796:: (branch 10:3
825:: (branch 10:3
797:: (wing 10:6 a)
826:: (wing 10:6 a)
798−:: (arm 11:5
827+:: (arm 11:3
799−:: (cell 11:5 (lit 11:6 %add) (bind 11:11 item))
828+:: (cell 11:3 (lit 11:4 %add) (bind 11:9 item))
800−:: (change 11:18 s
829+:: (change 11:16 s
801−:: (edit 11:20 items
830+:: (edit 11:18 items
802−:: (tuple 11:26 (wing 11:27 item) (wing 11:32 items.s)))))
831+:: (tuple 11:24 (wing 11:25 item) (wing 11:30 items.s)))))
803−:: (arm 12:5
832+:: (arm 12:3
804−:: (lit 12:5 %toggle)
833+:: (lit 12:3 %toggle)
805−:: (change 12:18 s
834+:: (change 12:16 s
806−:: (edit 12:20 open
835+:: (edit 12:18 open
807−:: (group 12:25
836+:: (group 12:23
808−:: (call 12:26 (wing 12:26 not) (wing 12:30 open.s)))))))))))
837+:: (call 12:24 (wing 12:24 not) (wing 12:28 open.s)))))))))))
810:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
839:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
811:: source line, then a caret under the column (col - 1 spaces, then ^).
840:: source line, then a caret under the column (col - 1 spaces, then ^).
@@ -816,9 +845,9 @@
816:: prints as a space, so the caret stays under its column and golden
845:: prints as a space, so the caret stays under its column and golden
817:: files hold no raw control bytes.
846:: files hold no raw control bytes.
819−:: /ui/basket.jibb:22:5: msg has no case %submitt
848+:: /ui/basket.jibb:22:3: msg has no case %submitt
820−:: %submitt [m(note="") ~]
849+:: %submitt [m(note="") ~]
824+| %positions
853+| %positions
@@ -964,9 +993,10 @@
965+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
994+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
967−:: +edit: a change's item or line, name=value
996+:: +edit: a change's item or line, name=value or wing=value; names
997+:: as written, as a %wing's: open.cart is ~[%open %cart]
969−+$ edit $~([*span %$ *expr] [at=span name=term val=expr])
999++$ edit $~([*span ~ *expr] [at=span names=(list term) val=expr])
971:: +arm: a ?- arm, a pattern and an expression or body
1001:: +arm: a ?- arm, a pattern and an expression or body
@@ -1355,10 +1385,10 @@
1355 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
1385 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
1356 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
1386 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
1357 ?: (is-upper a)
1387 ?: (is-upper a)
1388+ =/ n=@ud (run-len t.cs tvar-mask)
1358− => (emit 1 [%tvar a])
1389+ => (emit +(n) [%tvar (crip [a (scag n t.cs)])])
1359− ?. &(?=(^ cs) |((is-lower i.cs) (is-upper i.cs) (is-digit i.cs)))
1390+ ?. &(?=(^ cs) |((is-upper i.cs) =('_' i.cs) =('-' i.cs))) cor
1361− (err col "a type variable is one capital letter")
1391+ (err col "a type variable is a capital, then lowercase letters and digits")
1362 ?: =(':' a)
1392 ?: =(':' a)
1363 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
1393 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
1364 ?: =(':' b) comment
1394 ?: =(':' b) comment
@@ -1662,6 +1692,7 @@
1662++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
1692++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
1663++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f
1693++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f
1664++ name-mask 0x7ff.fffe.0000.0000.03ff.2000.0000.0000 :: a-z 0-9 -
1694++ name-mask 0x7ff.fffe.0000.0000.03ff.2000.0000.0000 :: a-z 0-9 -
1695+++ tvar-mask 0x7ff.fffe.0000.0000.03ff.0000.0000.0000 :: a-z 0-9
1665++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _
1696++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _
1666++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .
1697++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .
1667++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2
1698++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2
@@ -2280,7 +2311,7 @@
2280++ sexp-edit
2311++ sexp-edit
2281 |= e=edit
2312 |= e=edit
2283− (nod "edit" at.e (trip name.e) ~[(sexp-expr val.e)])
2314+ (nod "edit" at.e (show-names names.e) ~[(sexp-expr val.e)])
2285++ sexp-arm
2316++ sexp-arm
2286 |= a=arm
2317 |= a=arm
@@ -2689,24 +2720,32 @@
2689 ?~ t.els i.els
2720 ?~ t.els i.els
2690 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
2721 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
2723+:: +slot: a bracket's item or line as read, before +bracket-node
2724+:: makes it an item or an edit: its name=, or a change's wing=, else ~
2726++$ slot [at=span face=(list term) val=expr]
2692:: +bracket-node: a tuple, list or change from its items, ending at fin
2728:: +bracket-node: a tuple, list or change from its items, ending at fin
2694++ bracket-node
2730++ bracket-node
2695 |= $: kind=?(%tuple %list %change)
2731 |= $: kind=?(%tuple %list %change)
2696 op=token
2732 op=token
2697 target=(unit [t=token names=(list term)])
2733 target=(unit [t=token names=(list term)])
2698− its=(list item)
2734+ its=(list slot)
2703− %tuple [%tuple [beg.at.op fin] its]
2740+ :+ %tuple [beg.at.op fin]
2704− %list [%list [beg.at.op fin] (turn its |=(i=item val.i))]
2741+ (turn its |=(i=slot ^-(item [at.i ?~(face.i ~ `i.face.i) val.i])))
2743+ %list [%list [beg.at.op fin] (turn its |=(i=slot val.i))]
2707 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
2746 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
2708 :^ %change [beg fin] ?~(target ~ names.u.target)
2747 :^ %change [beg fin] ?~(target ~ names.u.target)
2709− (turn its |=(i=item ^-(edit [at.i ?~(face.i %$ u.face.i) val.i])))
2748+ (turn its |=(i=slot ^-(edit [at.i face.i val.i])))
2712+| %parser
2751+| %parser
@@ -2927,23 +2966,22 @@
2928 :: +unnamed: a change's item or line without its name=
2967 :: +unnamed: a change's item or line without its name=
2930− :: A name could still begin one, so the error is just past it, as
2969+ :: A name or a wing could still begin one, so the error is just
2931− :: a tight form's is (+fail-space): `m(b c)` at the space, `m(b)`
2970+ :: past it, as a tight form's is (+fail-space): `m(b c)` and
2932− :: at the ). So is an error token's text there, unless it begins
2971+ :: `m(a.b 1)` at the space, `m(b)` at the ). So is an error token's
2933− :: with the =: `m(a"x)` at the ", with the layout pass's message
2972+ :: text there, unless it begins with the =: `m(a"x)` at the ", with
2934− :: after the parser's (+moved), but `m(a==1)` at the lexer's error,
2973+ :: the layout pass's message after the parser's (+moved), but
2935− :: the second =. So is a wing's first name: `m(a.b=1)` fails at the
2974+ :: `m(a==1)` at the lexer's error, the second =. At an error token
2936− :: dot (+fail-in). At an error token whose text can't begin a name,
2937− :: at that text, as `m( @sd` at the @ (+fail-in).
2975+ :: whose text can't begin a name, at that text, as `m( @sd` at the
2939 ++ unnamed
2978 ++ unnamed
2940 |= ts=(list token)
2979 |= ts=(list token)
2941 ^- [%| p=error]
2980 ^- [%| p=error]
2942 =/ why=tape "a change's items are named, as in m(done=%.y)"
2981 =/ why=tape "a change's items are named, as in m(done=%.y)"
2943 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
2982 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
2944− ?: ?=([[* * [%wing *]] *] ts)
2983+ ?. ?=([[* * ?([%name *] [%wing *])] *] ts)
2945− (bad-in-why ts "a named item" lower-mask why)
2946− ?. ?=([[* * [%name *]] *] ts) (bad-why ts "a named item" why)
2984+ (bad-why ts "a named item" why)
2947 =/ want=tape "`=` right after {(show-found i.ts)}"
2985 =/ want=tape "`=` right after {(show-found i.ts)}"
2948 ?: ?& ?=([* [* * [%error *]] *] ts)
2986 ?: ?& ?=([* [* * [%error *]] *] ts)
2949 =(end.at.i.ts from.lex.i.t.ts)
2987 =(end.at.i.ts from.lex.i.t.ts)
@@ -2961,9 +2999,10 @@
2961 :: closes on its line (2.9). A bracket that needs none of these
2999 :: closes on its line (2.9). A bracket that needs none of these
2962 :: closes with the deeper lines instead (+shut). No later line can
3000 :: closes with the deeper lines instead (+shut). No later line can
2963 :: give it that, so the error is at the end of the line that took
3001 :: give it that, so the error is at the end of the line that took
2964− :: them (section 3, Errors). want is what it needs. Only an error path
3002+ :: them (section 3, Errors). want is what it needs. It looks only when
2965− :: calls this, and it looks only when after begins with NEWLINE or
2966− :: DEDENT, so it costs nothing on the way to a tree.
3003+ :: after begins with NEWLINE or DEDENT, so it costs nothing on the way
3004+ :: to a tree, except where a rune takes the rest of a body (+read-last):
3005+ :: a look at that rune's line.
2968 ++ doomed
3007 ++ doomed
2969 |= [ts=(list token) after=(list token) want=tape]
3008 |= [ts=(list token) after=(list token) want=tape]
@@ -3120,7 +3159,7 @@
3120 ?: =(%'++' lex.rune)
3159 ?: =(%'++' lex.rune)
3121 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
3160 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
3122 ;< [e=expr more=(list token)] then
3161 ;< [e=expr more=(list token)] then
3123− (read-expr-or-body "the name" after)
3162+ (read-expr-or-body | "the name" after)
3124 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
3163 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
3125 ?: (is-closer rune)
3164 ?: (is-closer rune)
3126 %^ bad-why ts "a definition"
3165 %^ bad-why ts "a definition"
@@ -3200,20 +3239,36 @@
3200 [%& p.lex.i.ts t.ts]
3239 [%& p.lex.i.ts t.ts]
3202 :: +read-expr-or-body: a space and an expression on the line, or a
3241 :: +read-expr-or-body: a space and an expression on the line, or a
3203− :: body on deeper lines; what names what comes before, for errors
3242+ :: body on deeper lines; what names what comes before, for errors.
3243+ :: On a body's final line (fin, +read-last), a line at the same depth
3244+ :: is the rest of the body instead, and the expression on the line
3245+ :: goes on with fin, except a ?-, which keeps its arms deeper
3205 ++ read-expr-or-body
3247 ++ read-expr-or-body
3206− |= [what=tape ts=(list token)]
3248+ |= [fin=? what=tape ts=(list token)]
3207 ^- (pare expr)
3249 ^- (pare expr)
3208 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3250 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3251+ ?: &(fin ?=([[* * %newline] *] ts)) (read-rest t.ts)
3209 ?: ?=([[* * ?(%newline %dedent)] *] ts)
3252 ?: ?=([[* * ?(%newline %dedent)] *] ts)
3210 (bad ts "an expression, or a body on deeper lines")
3253 (bad ts "an expression, or a body on deeper lines")
3211 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3254 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3212− (read-expr ts)
3255+ (read-last &(fin !?=([[* * %'?-'] *] ts)) ts)
3214− :: +read-body: after its INDENT, { definition NEWLINE } expr DEDENT
3257+ :: +read-body: after its INDENT, the rest of a body, then its DEDENT
3216 ++ read-body
3259 ++ read-body
3262+ ;< [e=expr after=(list token)] then (read-rest ts)
3263+ ?> ?=([[* * %dedent] *] after)
3266+ :: +read-rest: { definition NEWLINE } last, up to the DEDENT that ends
3267+ :: a body, which it leaves for whatever opened the body: its INDENT's
3268+ :: reader, or the rune on the final line that took the rest of it
3217 |= ts=(list token)
3272 |= ts=(list token)
3218 ^- (pare expr)
3273 ^- (pare expr)
3219 =| defs=(list def)
3274 =| defs=(list def)
@@ -3227,12 +3282,15 @@
3227 %: bad-in-why ts "a definition or an expression" plus-mask
3282 %: bad-in-why ts "a definition or an expression" plus-mask
3228 "`+` begins `++` or `+$`"
3283 "`+` begins `++` or `+$`"
3230− ;< [e=expr after=(list token)] then (read-expr ts)
3285+ ;< [e=expr after=(list token)] then (read-last & ts)
3231 ?: ?=([[* * %dedent] *] after)
3286 ?: ?=([[* * %dedent] *] after)
3232 =/ ds=(list def) (flop defs)
3287 =/ ds=(list def) (flop defs)
3233 =/ beg=loc ?~(ds beg:(span-of e) beg:(span-of i.ds))
3288 =/ beg=loc ?~(ds beg:(span-of e) beg:(span-of i.ds))
3234− [%& [%body [beg end:(span-of e)] ds e] t.after]
3289+ [%& [%body [beg end:(span-of e)] ds e] after]
3235 ?. ?=([[* * %newline] *] after) (bad-end-in after (tail-can e))
3290 ?. ?=([[* * %newline] *] after) (bad-end-in after (tail-can e))
3291+ ?: &(?=(%branch -.e) !?=([* [* * ?(%'++' %'+$')] *] after))
3292+ %^ bad-why after "the end of the body"
3293+ "this `?-`'s arms are on deeper lines, so this one goes there too"
3236 %^ bad-why after "the end of the body"
3294 %^ bad-why after "the end of the body"
3237 "a body's final expression is its last line"
3295 "a body's final expression is its last line"
@@ -3241,13 +3299,24 @@
3241 ++ read-expr
3299 ++ read-expr
3242 |= ts=(list token)
3300 |= ts=(list token)
3243 ^- (pare expr)
3301 ^- (pare expr)
3304+ :: +read-last: +read-expr, where fin says the expression is a body's
3305+ :: final line or goes on one, with no bracket open before it: then
3306+ :: the rune that ends the line may take the rest of the body at the
3307+ :: same depth as its last child, and a ?- that begins the line its
3308+ :: arms (section 3, The rest of a body)
3311+ |= [fin=? ts=(list token)]
3244 ?~ ts (bad ts "an expression")
3313 ?~ ts (bad ts "an expression")
3245 =* t i.ts
3314 =* t i.ts
3246 ?+ lex.t (read-call ts)
3315 ?+ lex.t (read-call ts)
3247− %'|=' ?:((is-ctor ts) (read-call ts) (read-gate t t.ts))
3316+ %'|=' ?:((is-ctor ts) (read-call ts) (read-gate fin t t.ts))
3248− %'^-' (read-cast t t.ts)
3317+ %'^-' (read-cast fin t t.ts)
3249− %'~&' (read-trace t t.ts)
3318+ %'~&' (read-trace fin t t.ts)
3250− %'?-' (read-branch t t.ts)
3319+ %'?-' (read-branch fin t t.ts)
3253 :: +read-call: operand { operand }; one operand alone is itself
3322 :: +read-call: operand { operand }; one operand alone is itself
@@ -3462,9 +3531,9 @@
3462 (unclosed par ")" after)
3531 (unclosed par ")" after)
3463 ;< [els=(list expr) after=(list token)] then (read-operands ts)
3532 ;< [els=(list expr) after=(list token)] then (read-operands ts)
3464 ?: ?=([[* * %indent] *] after)
3533 ?: ?=([[* * %indent] *] after)
3465− ;< [ls=(list item) more=(list token)] then
3534+ ;< [ls=(list slot) more=(list token)] then
3466 (read-lines %group t.after)
3535 (read-lines %group t.after)
3467− =/ inner=expr (call-of (weld els (turn ls |=(i=item val.i))))
3536+ =/ inner=expr (call-of (weld els (turn ls |=(i=slot val.i))))
3468 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
3537 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
3470 ?: ?=([[* * ?(%newline %dedent)] *] after)
3539 ?: ?=([[* * ?(%newline %dedent)] *] after)
@@ -3489,7 +3558,7 @@
3490 ^- (pare expr)
3559 ^- (pare expr)
3491 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3560 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3492− =| its=(list item)
3561+ =| its=(list slot)
3493 |- ^- (pare expr)
3562 |- ^- (pare expr)
3494 ?~ ts (bad ts "an item")
3563 ?~ ts (bad ts "an item")
3495 =* t i.ts
3564 =* t i.ts
@@ -3497,8 +3566,8 @@
3497 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
3566 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
3498 ?: (is-closer t) (unclosed op (trip close) ts)
3567 ?: (is-closer t) (unclosed op (trip close) ts)
3499 ?: ?=(%indent lex.t)
3568 ?: ?=(%indent lex.t)
3500− ;< [ls=(list item) more=(list token)] then (read-lines kind t.ts)
3569+ ;< [ls=(list slot) more=(list token)] then (read-lines kind t.ts)
3501− =/ every=(list item) (weld (flop its) ls)
3570+ =/ every=(list slot) (weld (flop its) ls)
3502 =/ fin=loc ?~(every end.at.op end.at:(rear every))
3571 =/ fin=loc ?~(every end.at.op end.at:(rear every))
3503 [%& (bracket-node kind op target every fin) more]
3572 [%& (bracket-node kind op target every fin) more]
3504 ?: &(?=(^ its) (shut op `at.i.its ts))
3573 ?: &(?=(^ its) (shut op `at.i.its ts))
@@ -3506,21 +3575,21 @@
3506 ?: ?=(?(%newline %dedent) lex.t)
3575 ?: ?=(?(%newline %dedent) lex.t)
3507 (unclosed-open op (trip close) "an item" ts)
3576 (unclosed-open op (trip close) "an item" ts)
3508 ?: &(tight.t ?=(^ its)) (no-space ts)
3577 ?: &(tight.t ?=(^ its)) (no-space ts)
3509− ;< [i=item more=(list token)] then (read-item kind ts)
3578+ ;< [i=slot more=(list token)] then (read-item kind ts)
3510 $(its [i its], ts more)
3579 $(its [i its], ts more)
3512 :: +read-item: [ name= ] operand; a tuple's item may be named, a
3581 :: +read-item: [ name= ] operand; a tuple's item may be named, a
3513− :: change's must be, a list's is not
3582+ :: change's must be, by a name or a wing, a list's is not
3515 ++ read-item
3584 ++ read-item
3516 |= [kind=?(%tuple %list %change) ts=(list token)]
3585 |= [kind=?(%tuple %list %change) ts=(list token)]
3517− ^- (pare item)
3586+ ^- (pare slot)
3518− ?: &(!?=(%list kind) ?=([[* * [%name *]] [* %& %'='] *] ts))
3587+ ?: &(?=([* * *] ts) (named-item kind ts))
3519 =* nam i.ts
3588 =* nam i.ts
3520 =/ rest=(list token) t.t.ts
3589 =/ rest=(list token) t.t.ts
3521 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3590 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3522 ;< [v=expr after=(list token)] then (read-operand rest)
3591 ;< [v=expr after=(list token)] then (read-operand rest)
3523− [%& [[beg.at.nam end:(span-of v)] `p.lex.nam v] after]
3592+ [%& [[beg.at.nam end:(span-of v)] (names-of lex.nam) v] after]
3524 ?: ?=(%change kind) (unnamed ts)
3593 ?: ?=(%change kind) (unnamed ts)
3525 ?: &(?=(^ ts) (is-rune i.ts))
3594 ?: &(?=(^ ts) (is-rune i.ts))
3526 %: bad-in-why ts "an expression" operand-mask
3595 %: bad-in-why ts "an expression" operand-mask
@@ -3529,15 +3598,25 @@
3529 ;< [v=expr after=(list token)] then (read-operand ts)
3598 ;< [v=expr after=(list token)] then (read-operand ts)
3530 [%& [(span-of v) ~ v] after]
3599 [%& [(span-of v) ~ v] after]
3601+ :: +named-item: whether ts begins an item's or a line's name=: a
3602+ :: tuple's or a change's name, or a change's wing, then = tight
3605+ |= [kind=?(%tuple %list %change %group) ts=(list token)]
3607+ ?. ?=([* [* %& %'='] *] ts) |
3608+ ?: ?=([[* * [%name *]] *] ts) ?=(?(%tuple %change) kind)
3609+ &(?=(%change kind) ?=([[* * [%wing *]] *] ts))
3532 :: +read-lines: after an open bracket's INDENT, its lines, an item
3611 :: +read-lines: after an open bracket's INDENT, its lines, an item
3533 :: each, to its DEDENT
3612 :: each, to its DEDENT
3535 ++ read-lines
3614 ++ read-lines
3536 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3615 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3537− ^- (pare (list item))
3616+ ^- (pare (list slot))
3538− =| ls=(list item)
3617+ =| ls=(list slot)
3539− |- ^- (pare (list item))
3618+ |- ^- (pare (list slot))
3540− ;< [l=item after=(list token)] then (read-line kind ts)
3619+ ;< [l=slot after=(list token)] then (read-line kind ts)
3541 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
3620 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
3542 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
3621 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
3543 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
3622 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
@@ -3564,22 +3643,20 @@
3564 "its items end at the first line that isn't deeper"
3643 "its items end at the first line that isn't deeper"
3566 :: +read-line: an open bracket's line, [ name= ] expr; a tuple's may
3645 :: +read-line: an open bracket's line, [ name= ] expr; a tuple's may
3567− :: be named, a change's must be, a list's and a group's are not
3646+ :: be named, a change's must be, by a name or a wing, a list's and a
3568− :: (doc question)
3647+ :: group's are not (doc question)
3570 ++ read-line
3649 ++ read-line
3571 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3650 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3572− ^- (pare item)
3651+ ^- (pare slot)
3573 =/ cf (closer-first ts "an item")
3652 =/ cf (closer-first ts "an item")
3574 ?^ cf u.cf
3653 ?^ cf u.cf
3575− ?: ?& ?=(?(%tuple %change) kind)
3654+ ?: &(?=([* * *] ts) (named-item kind ts))
3576− ?=([[* * [%name *]] [* %& %'='] *] ts)
3578 =* nam i.ts
3655 =* nam i.ts
3579 =/ rest=(list token) t.t.ts
3656 =/ rest=(list token) t.t.ts
3580 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3657 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3581 ;< [v=expr after=(list token)] then (read-expr rest)
3658 ;< [v=expr after=(list token)] then (read-expr rest)
3582− [%& [[beg.at.nam end:(span-of v)] `p.lex.nam v] after]
3659+ [%& [[beg.at.nam end:(span-of v)] (names-of lex.nam) v] after]
3583 ?: ?=(%change kind) (unnamed ts)
3660 ?: ?=(%change kind) (unnamed ts)
3584 ;< [v=expr after=(list token)] then (read-expr ts)
3661 ;< [v=expr after=(list token)] then (read-expr ts)
3585 [%& [(span-of v) ~ v] after]
3662 [%& [(span-of v) ~ v] after]
@@ -3616,10 +3693,11 @@
3616 %^ bad-why more (closing op ")")
3693 %^ bad-why more (closing op ")")
3617 "the wide gate's body is one operand, so a call goes in parentheses"
3694 "the wide gate's body is one operand, so a call goes in parentheses"
3619− :: +read-gate: |= sample, then an expression or a body
3696+ :: +read-gate: |= sample, then an expression or a body; fin as for
3621 ++ read-gate
3699 ++ read-gate
3622− |= [bar=token ts=(list token)]
3700+ |= [fin=? bar=token ts=(list token)]
3623 ^- (pare expr)
3701 ^- (pare expr)
3624 ?: &(?=(^ ts) tight.i.ts)
3702 ?: &(?=(^ ts) tight.i.ts)
3625 :: a % could begin a constructor's term, as |=%got
3703 :: a % could begin a constructor's term, as |=%got
@@ -3631,13 +3709,14 @@
3631 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3709 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3632 ?^ dm u.dm
3710 ?^ dm u.dm
3633 ;< [e=expr more=(list token)] then
3711 ;< [e=expr more=(list token)] then
3634− (read-expr-or-body "the sample" after)
3712+ (read-expr-or-body fin "the sample" after)
3635 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
3713 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
3637− :: +read-cast: ^- mold, then an expression or a body
3715+ :: +read-cast: ^- mold, then an expression or a body; fin as for
3639 ++ read-cast
3718 ++ read-cast
3640− |= [ket=token ts=(list token)]
3719+ |= [fin=? ket=token ts=(list token)]
3641 ^- (pare expr)
3720 ^- (pare expr)
3642 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
3721 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
3643 ;< [s=shape after=(list token)] then (read-mold ts)
3722 ;< [s=shape after=(list token)] then (read-mold ts)
@@ -3646,41 +3725,65 @@
3646 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3725 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3647 ?^ dm u.dm
3726 ?^ dm u.dm
3648 ;< [e=expr more=(list token)] then
3727 ;< [e=expr more=(list token)] then
3649− (read-expr-or-body "the mold" after)
3728+ (read-expr-or-body fin "the mold" after)
3650 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
3729 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
3652− :: +read-trace: ~& expr, then its body below
3731+ :: +read-trace: ~& expr, then its body below, or, on a body's final
3732+ :: line (fin, +read-last), the rest of the body
3654 ++ read-trace
3734 ++ read-trace
3655− |= [sig=token ts=(list token)]
3735+ |= [fin=? sig=token ts=(list token)]
3656 ^- (pare expr)
3736 ^- (pare expr)
3657 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
3737 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
3658 ;< [v=expr after=(list token)] then (read-expr ts)
3738 ;< [v=expr after=(list token)] then (read-expr ts)
3659− ?. ?=([[* * %indent] *] after)
3660− =/ dm (doomed ts after "`~&`'s body on deeper lines")
3739+ =/ dm (doomed ts after "`~&`'s body on deeper lines")
3661− ?^ dm u.dm
3740+ ?^ dm u.dm
3741+ ;< [b=expr more=(list token)] then
3742+ ?: ?=([[* * %indent] *] after) (read-body t.after)
3743+ ?: &(fin ?=([[* * %newline] *] after)) (read-rest t.after)
3662 (bad after "`~&`'s body on deeper lines")
3744 (bad after "`~&`'s body on deeper lines")
3663− ;< [b=expr more=(list token)] then (read-body t.after)
3664 [%& [%trace [beg.at.sig end:(span-of b)] v b] more]
3745 [%& [%trace [beg.at.sig end:(span-of b)] v b] more]
3666− :: +read-branch: ?- expr, then its arms below, one per line
3747+ :: +read-branch: ?- expr, then its arms below, one per line; or, when
3748+ :: it begins a body's final line (fin, +read-last), at its own depth
3749+ :: to the end of the body, whose DEDENT it leaves (+read-rest)
3668 ++ read-branch
3751 ++ read-branch
3669− |= [wut=token ts=(list token)]
3752+ |= [fin=? wut=token ts=(list token)]
3670 ^- (pare expr)
3753 ^- (pare expr)
3671 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
3754 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
3672 ;< [s=expr after=(list token)] then (read-expr ts)
3755 ;< [s=expr after=(list token)] then (read-expr ts)
3673− ?. ?=([[* * %indent] *] after)
3674− =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3756+ =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3675− ?^ dm u.dm
3757+ ?^ dm u.dm
3758+ ?. ?=([[* * ?(%indent %newline)] *] after)
3676 (bad after "`?-`'s arms on deeper lines")
3759 (bad after "`?-`'s arms on deeper lines")
3760+ =/ flat=? ?=(%newline lex.i.after)
3761+ ?: &(flat !fin) (bad after "`?-`'s arms on deeper lines")
3677 =| arms=(list arm)
3762 =| arms=(list arm)
3678 =/ rest=(list token) t.after
3763 =/ rest=(list token) t.after
3679 |- ^- (pare expr)
3764 |- ^- (pare expr)
3680− ;< [a=arm more=(list token)] then (read-arm rest)
3765+ ;< [a=arm more=(list token)] then
3766+ ?:(flat (read-flat-arm rest) (read-arm rest))
3681 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
3767 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
3682 ?. ?=([[* * %dedent] *] more) (bad-end-in more (tail-can val.a))
3768 ?. ?=([[* * %dedent] *] more) (bad-end-in more (tail-can val.a))
3683− [%& [%branch [beg.at.wut end.at.a] s (flop [a arms])] t.more]
3769+ =/ at=span [beg.at.wut end.at.a]
3770+ [%& [%branch at s (flop [a arms])] ?:(flat more t.more)]
3772+ :: +read-flat-arm: +read-arm at its ?-'s depth, where a line that
3773+ :: could begin the body's other lines gets a hint
3778+ ?: ?=([[* * ?(%'++' %'+$')] *] ts)
3779+ %: bad-in-why ts "a pattern" pattern-mask
3780+ "a body's local definitions come before its final expression"
3782+ ?: ?=([[* * ?(%'~&' %'^-')] *] ts)
3783+ %: bad-in-why ts "a pattern" pattern-mask
3784+ "a trace or cast goes in the arm's body"
3685 :: +read-arm: a pattern, then an expression or a body
3788 :: +read-arm: a pattern, then an expression or a body
@@ -3695,7 +3798,7 @@
3695 %^ bad-why after "a space after the pattern"
3798 %^ bad-why after "a space after the pattern"
3696 "patterns take no `name=`: a bare name binds, as [a b]"
3799 "patterns take no `name=`: a bare name binds, as [a b]"
3697 ;< [e=expr more=(list token)] then
3800 ;< [e=expr more=(list token)] then
3698− (read-expr-or-body "the pattern" after)
3801+ (read-expr-or-body | "the pattern" after)
3699 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
3802 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
3701 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
3804 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
@@ -4437,7 +4540,7 @@
4437++ outline-edit
4540++ outline-edit
4438 |= e=edit
4541 |= e=edit
4439 ^- outline
4542 ^- outline
4440− [%edit at.e ~[%name] %kid ~[(outline-expr val.e)]]
4543+ [%edit at.e ~[%name %wing] %kid ~[(outline-expr val.e)]]
4442++ outline-arm
4545++ outline-arm
4443 |= a=arm
4546 |= a=arm
@@ -4510,9 +4613,9 @@
4511:: Each case parses a source, checks that its spans pass, then moves
4614:: Each case parses a source, checks that its spans pass, then moves
4512:: the span of every node of a kind that starts at a place, as a
4615:: the span of every node of a kind that starts at a place, as a
4513−:: parser bug would, and checks that +check-spans says so. Run it as
4616+:: parser bug would, and checks that +check-spans says so.
4514−:: tools/hoon check-spans-test, which prints <<>> when every case
4617+:: tests/lib/jibb-check-spans.hoon runs it, under eval with
4515−:: passes.
4618+:: tools/test-arms and on the ship.
4517++ check-spans-test
4620++ check-spans-test
4518 ^- (list tape)
4621 ^- (list tape)
@@ -4614,7 +4717,10 @@
4614:: Restricted-number promotion considers written capitals only; if there
4717:: Restricted-number promotion considers written capitals only; if there
4615:: are none, it skips the otherwise unnecessary environment traversal.
4718:: are none, it skips the otherwise unnecessary environment traversal.
4616:: Bare @ is a separate unrestricted atom type. A directional fit check
4719:: Bare @ is a separate unrestricted atom type. A directional fit check
4617−:: permits concrete atoms to widen to it, never the reverse. A fit that
4720+:: permits concrete atoms to widen to it, never the reverse. A bare
4721+:: decimal is a @ud: its variable binds only @ud or @u, it fits @ and *,
4722+:: and +decimal-misfit names it where it meets another aura (S4); a
4723+:: ++ generic over its aura generalizes it to any aura. A fit that
4618:: needs a not-yet-implemented constraint remains unsupported. Named unions
4724:: needs a not-yet-implemented constraint remains unsupported. Named unions
4619:: retain origin and ordered arguments, including phantom arguments, apart
4725:: retain origin and ordered arguments, including phantom arguments, apart
4620:: from their display name. Generic cases must be disjoint for all arguments.
4726:: from their display name. Generic cases must be disjoint for all arguments.
@@ -4634,6 +4740,14 @@
4634:: proofs to fewer than 1,024 cells; the projection planner has a separate
4740:: proofs to fewer than 1,024 cells; the projection planner has a separate
4635:: 4,096-step bound. These are inference limits, not language limits.
4741:: 4,096-step bound. These are inference limits, not language limits.
4743+:: `unface` is reserved with proj (+reserved-name) and is also handled by
4744+:: type: (unface e) has e's type with every face removed, through cells,
4745+:: gates and collection arguments, keeping unions and recursive molds
4746+:: whole (+itype-unface). It is not a value, it takes one argument, and
4747+:: a bare type variable is unsupported, as field access on one is. A ++
4748+:: whose body is (unface |= …) is a gate for recursion (+unfaced-gate).
4749+:: It lowers to its argument; no lowering is implemented yet.
4637:: Supported API imports derive request-gate types atomically for multiple
4751:: Supported API imports derive request-gate types atomically for multiple
4638:: paths, including one typed segment or one diff fold per case. Their checked
4752:: paths, including one typed segment or one diff fold per case. Their checked
4639:: ordinary definitions, mark molds and supported poke constructor are also
4753:: ordinary definitions, mark molds and supported poke constructor are also
@@ -4845,7 +4959,8 @@
4845:: +itype-unify: consistent substitutions, or ~ for a mismatch
4959:: +itype-unify: consistent substitutions, or ~ for a mismatch
4847:: Different concrete auras conflict. A variable may become an atom or
4961:: Different concrete auras conflict. A variable may become an atom or
4848−:: a function, but cannot contain itself. Aura-only variables and faces
4962+:: a function, but cannot contain itself. A decimal's variable binds
4963+:: only @ud or @u (+decimal-aura). Aura-only variables and faces
4849:: require further distinctions before this supports general Jibb.
4964:: require further distinctions before this supports general Jibb.
4851++ itype-unify
4966++ itype-unify
@@ -4894,10 +5009,10 @@
4894 ?: &(?=(%rnvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
5009 ?: &(?=(%rnvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4895 ?: &(?=(%avar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
5010 ?: &(?=(%avar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
4896 ?: ?=(%rnvar -.a)
5011 ?: ?=(%rnvar -.a)
4897− ?. |(?=(%rnvar -.b) ?=(%atom -.b)) ~
5012+ ?. |(?=(%rnvar -.b) &(?=(%atom -.b) (decimal-aura aura.b))) ~
4898 `[[id.a b] sub]
5013 `[[id.a b] sub]
4899 ?: ?=(%rnvar -.b)
5014 ?: ?=(%rnvar -.b)
4900− ?. ?=(%atom -.a) ~
5015+ ?. &(?=(%atom -.a) (decimal-aura aura.a)) ~
4901 `[[id.b a] sub]
5016 `[[id.b a] sub]
4902 ?: &(?=(%avar -.a) ?=(%rvar -.b)) `[[id.a b] sub]
5017 ?: &(?=(%avar -.a) ?=(%rvar -.b)) `[[id.a b] sub]
4903 ?: &(?=(%rvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
5018 ?: &(?=(%rvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
@@ -4908,14 +5023,15 @@
4908 ?. ?=(%atom -.a) ~
5023 ?. ?=(%atom -.a) ~
4909 `[[id.b a] sub]
5024 `[[id.b a] sub]
4910 :: The narrower decimal constraint survives a match with an atom
5025 :: The narrower decimal constraint survives a match with an atom
4911− :: variable; decimal syntax alone does not make it a loobean.
5026+ :: variable; decimal syntax alone does not make it a loobean. A
5027+ :: concrete aura takes a decimal only if it is @ud or @u.
4912 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
5028 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
4913 ?: &(?=(%avar -.a) ?=(%nvar -.b)) `[[id.a b] sub]
5029 ?: &(?=(%avar -.a) ?=(%nvar -.b)) `[[id.a b] sub]
4914 ?: ?=(%nvar -.a)
5030 ?: ?=(%nvar -.a)
4915− ?. |(?=(%nvar -.b) ?=(%atom -.b)) ~
5031+ ?. |(?=(%nvar -.b) &(?=(%atom -.b) (decimal-aura aura.b))) ~
4916 `[[id.a b] sub]
5032 `[[id.a b] sub]
4917 ?: ?=(%nvar -.b)
5033 ?: ?=(%nvar -.b)
4918− ?. ?=(%atom -.a) ~
5034+ ?. &(?=(%atom -.a) (decimal-aura aura.a)) ~
4919 `[[id.b a] sub]
5035 `[[id.b a] sub]
4920 ?: ?=(%avar -.a)
5036 ?: ?=(%avar -.a)
4921 ?. |(?=(%avar -.b) ?=(%atom -.b) ?=(%any-atom -.b) ?=(%flag -.b)) ~
5037 ?. |(?=(%avar -.b) ?=(%atom -.b) ?=(%any-atom -.b) ?=(%flag -.b)) ~
@@ -4939,6 +5055,35 @@
4939 $(a tal.a, b tal.b, sub u.first)
5055 $(a tal.a, b tal.b, sub u.first)
5058+:: +itype-unface: t with every face removed, for (unface e)
5060+:: It strips through cells, through a gate's sample and product and
5061+:: through a built-in collection's arguments, the prelude's unit
5062+:: included, walking bound variables. Other unions and recursive
5063+:: molds are compared by name or by their exact cases, so stripping
5064+:: inside them would stop them from fitting their own name: they are
5065+:: kept whole. An unbound variable stays, so faces it is bound to
5066+:: later are kept. The unit keeps its own u=, as a list keeps i= and
5070+ |= [t=itype sub=isub]
5072+ =. t (itype-walk t sub)
5075+ %cell [%cell $(t hed.t) $(t tal.t)]
5076+ %fn [%fn $(t sample.t) $(t product.t)]
5077+ %collection [%collection name.t (turn args.t |=(a=itype ^$(t a)))]
5079+ ?. =(origin.t `[/lib/jibb/prelude/jibb %unit]) t
5080+ ?. ?=([* ~] args.t) t
5081+ =/ nil=itype [%const [%null %n 0 '~']]
5082+ ?. =(cases.t ~[nil [%cell nil [%face %u i.args.t]]]) t
5083+ =/ arg=itype $(t i.args.t)
5084+ t(cases ~[nil [%cell nil [%face %u arg]]], args ~[arg])
4942+$ igf-form [typ=itype sub=isub left=@ud]
5087+$ igf-form [typ=itype sub=isub left=@ud]
4943+$ igf-forms [types=(list itype) sub=isub left=@ud]
5088+$ igf-forms [types=(list itype) sub=isub left=@ud]
4944++ itype-gate-free-forms
5089++ itype-gate-free-forms
@@ -5060,6 +5205,16 @@
5060 ?. =(i.a i.b) |
5205 ?. =(i.a i.b) |
5061 $(a t.a, b t.b)
5206 $(a t.a, b t.b)
5208+:: +decimal-aura: whether a bare decimal fits an atom of this aura
5210+:: A decimal is a @ud, so as in Hoon it fits @ud and its ancestors
5211+:: @u and @; every other aura takes its own literal (S4).
5216+ (aura-prefix aura %ud)
5063:: Related auras in a structural unification need a common-type rule;
5218:: Related auras in a structural unification need a common-type rule;
5064:: until that rule is implemented, report an unknown rather than error.
5219:: until that rule is implemented, report an unknown rather than error.
@@ -5131,10 +5286,84 @@
5131 ?: (aura-prefix aura.a aura.b) `a
5286 ?: (aura-prefix aura.a aura.b) `a
5132 ?: (aura-prefix aura.b aura.a) `b
5287 ?: (aura-prefix aura.b aura.a) `b
5134− ?: &(?=(%any-atom -.a) |(?=(%atom -.b) ?=(%flag -.b))) `a
5289+ ?: &(?=(%any-atom -.a) |(?=(%atom -.b) ?=(%flag -.b) ?=(%const -.b) ?=(%avar -.b) ?=(%rvar -.b) ?=(%nvar -.b) ?=(%rnvar -.b))) `a
5135− ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a))) `b
5290+ ?: &(?=(%any-atom -.b) |(?=(%atom -.a) ?=(%flag -.a) ?=(%const -.a) ?=(%avar -.a) ?=(%rvar -.a) ?=(%nvar -.a) ?=(%rnvar -.a))) `b
5293+++ itype-branch-join
5294+ |= [a=itype b=itype sub=isub]
5295+ ^- (unit [typ=itype sub=isub])
5296+ =/ unified=(unit isub) (itype-unify a b sub)
5297+ ?^ unified `[(itype-normalize a u.unified) u.unified]
5298+ =/ common=(unit itype) (itype-concrete-join a b sub)
5302+++ itype-branch-join-with
5303+ |= [candidate=itype types=(list itype) sub=isub]
5304+ ^- (unit [typ=itype sub=isub])
5305+ ?~ types `[(itype-normalize candidate sub) sub]
5306+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join candidate i.types sub)
5308+ $(candidate typ.u.joined, types t.types, sub sub.u.joined)
5310+++ itype-branch-unify-list
5311+ |= [types=(list itype) sub=isub]
5312+ ^- (unit [typ=itype sub=isub])
5314+ =/ candidate=itype i.types
5315+ =/ rest=(list itype) t.types
5317+ ?~ rest `[(itype-normalize candidate sub) sub]
5318+ =/ unified=(unit isub) (itype-unify candidate i.rest sub)
5320+ $(candidate (itype-normalize candidate u.unified), rest t.rest, sub u.unified)
5322+++ itype-branch-any-atom
5323+ |= [types=(list itype) sub=isub]
5326+ =/ typ=itype (itype-walk i.types sub)
5327+ ?: ?=(%any-atom -.typ) `typ
5330+++ itype-branch-atom-parent
5331+ |= [candidate=itype types=(list itype) sub=isub]
5333+ ?~ types `candidate
5334+ =/ typ=itype (itype-walk i.types sub)
5335+ ?. ?=(%atom -.typ) $(types t.types)
5336+ =/ joined=(unit itype) (itype-concrete-join candidate typ sub)
5338+ $(candidate u.joined, types t.types)
5340+++ itype-branch-atom-candidates
5341+ |= [candidates=(list itype) types=(list itype) sub=isub]
5344+ =/ candidate=itype (itype-walk i.candidates sub)
5345+ ?. ?=(%atom -.candidate) $(candidates t.candidates)
5346+ =/ parent=(unit itype) (itype-branch-atom-parent candidate types sub)
5348+ $(candidates t.candidates)
5350+++ itype-branch-parent
5351+ |= [types=(list itype) sub=isub]
5353+ =/ unrestricted=(unit itype) (itype-branch-any-atom types sub)
5354+ ?^ unrestricted unrestricted
5355+ (itype-branch-atom-candidates types types sub)
5357+++ itype-branch-join-list
5358+ |= [types=(list itype) sub=isub]
5359+ ^- (unit [typ=itype sub=isub])
5361+ =/ unified=(unit [typ=itype sub=isub]) (itype-branch-unify-list types sub)
5363+ =/ parent=(unit itype) (itype-branch-parent types sub)
5365+ (itype-branch-join-with u.parent types sub)
5138:: Unifying an already-bound tuple with a faced position would need to
5367:: Unifying an already-bound tuple with a faced position would need to
5139:: update the bound type. Until substitutions can retain that information,
5368:: update the bound type. Until substitutions can retain that information,
5140:: variable-dependent face merges stay unresolved.
5369:: variable-dependent face merges stay unresolved.
@@ -5721,6 +5950,24 @@
5721 ["canonicalization should retain gate-free variables" problems]
5950 ["canonicalization should retain gate-free variables" problems]
5722 =? problems !=((show-atom-constraint canonical-free) " where A contains no gates")
5951 =? problems !=((show-atom-constraint canonical-free) " where A contains no gates")
5723 ["the printer should show gate-free constraints" problems]
5952 ["the printer should show gate-free constraints" problems]
5953+ =/ decimal=itype [%nvar 50]
5954+ =? problems ?=(~ (itype-unify decimal num ~))
5955+ ["a decimal should unify with @ud" problems]
5956+ =? problems ?=(~ (itype-unify [%atom %u] decimal ~))
5957+ ["a decimal should unify with @u" problems]
5958+ =? problems ?=(^ (itype-unify decimal [%atom %dr] ~))
5959+ ["a decimal should not unify with @dr" problems]
5960+ =? problems ?=(^ (itype-unify [%atom %ux] decimal ~))
5961+ ["a decimal should not unify with @ux" problems]
5962+ =/ restricted=(unit isub) (itype-unify decimal [%rvar 51] ~)
5963+ =? problems |(?=(~ restricted) ?=(^ (itype-unify [%rvar 51] [%atom %p] u.restricted)))
5964+ ["arithmetic should keep a decimal's aura rule" problems]
5965+ =/ decimal-any=ifit (itype-fit decimal [%any-atom ~] ~ 52)
5966+ =? problems !?=(%ok -.decimal-any)
5967+ ["a decimal should fit @" problems]
5968+ =/ decimal-noun=ifit (itype-fit decimal [%noun ~] ~ 52)
5969+ =? problems !?=(%ok -.decimal-noun)
5970+ ["a decimal should fit a noun" problems]
5724 problems
5971 problems
5726:: The expression inference below is deliberately a fragment: bindings,
5973:: The expression inference below is deliberately a fragment: bindings,
@@ -6099,9 +6346,13 @@
6099 ?~ work ~
6346 ?~ work ~
6100 ?: (hole-known [%var id.i.work] state) $(work t.work)
6347 ?: (hole-known [%var id.i.work] state) $(work t.work)
6101 ?: (hole-uncertain [%var id.i.work] state)
6348 ?: (hole-uncertain [%var id.i.work] state)
6102− `["type hole needs unsupported inference" ~[[at.i.work "type hole"]]]
6349+ `[uncertain-hole-msg ~[[at.i.work "type hole"]]]
6103 `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
6350 `["type hole needs a determined type" ~[[at.i.work "unresolved type hole"]]]
6352+:: +uncertain-hole-msg: unsupported, though it names the hole's site
6354+++ uncertain-hole-msg "type hole needs unsupported inference"
6105++ itype-vars
6356++ itype-vars
6106 |= t=itype
6357 |= t=itype
6107 ^- (list @ud)
6358 ^- (list @ud)
@@ -6264,15 +6515,67 @@
6265 (itype-var-is-gate-free-fuel n t 256)
6516 (itype-var-is-gate-free-fuel n t 256)
6518+:: +named-var: the ID of the nth type variable, written as name
6520+:: An ID counts in its low 64 bits. The name a variable was written
6521+:: with, as Msg, sits above them, or 0 for none, so the name travels
6522+:: with the variable through substitution, generalization and
6523+:: instantiation, and the printer can show it (+show-var). No two
6524+:: IDs share a count, so a name never makes two variables one.
6529+ (add (lsh 6 name) (end 6 n))
6531+:: +var-name: the name in a type variable's ID, or 0 for none
6538+:: +var-count: a type variable's ID without its name
6545+:: +canonical-itype: t with the variables in vars renumbered to print
6547+:: A variable keeps its name unless one before it in vars has the same
6548+:: name. The others take numbers from 0, skipping any whose letter
6549+:: (+show-var) is a name in vars, so a printed type never shows one
6550+:: name for two variables.
6267++ canonical-itype
6552++ canonical-itype
6268 |= [t=itype vars=(list @ud)]
6553 |= [t=itype vars=(list @ud)]
6269 ^- itype
6554 ^- itype
6555+ =/ names=(list @t) (turn vars var-name)
6556+ =/ used=(list @t) ~
6270 =/ ren=isub ~
6557 =/ ren=isub ~
6271 =/ n=@ud 0
6558 =/ n=@ud 0
6273 ?~ vars (itype-rename t ren)
6560 ?~ vars (itype-rename t ren)
6561+ =/ name=@t (var-name i.vars)
6562+ =/ own=? &(!=(0 name) !(lien used |=(u=@t =(u name))))
6563+ =? n !own (letter-free n names)
6564+ =/ id=@ud ?:(own (named-var name 0) n)
6274− =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] ?:((itype-var-is-gate-free i.vars t) [%fvar n] [%var n])))
6565+ =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar id] ?:((itype-var-is-atom i.vars t) [%avar id] ?:((itype-var-is-gate-free i.vars t) [%fvar id] [%var id])))
6275− $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
6566+ $(vars t.vars, ren [[i.vars replacement] ren], n ?:(own n +(n)), used ?:(own [name used] used))
6568+:: +letter-free: the first number from n whose letter is none of names
6571+ |= [n=@ud names=(list @t)]
6573+ ?. (lien names |=(m=@t =(m (crip (show-var n))))) n
6576+:: +instantiate-scheme: a scheme's type with fresh quantified variables
6578+:: Each fresh variable keeps the name of the one it replaces.
6277++ instantiate-scheme
6580++ instantiate-scheme
6278 |= [scheme=ischeme state=istate]
6581 |= [scheme=ischeme state=istate]
@@ -6281,12 +6584,13 @@
6281 =/ vars=(list @ud) vars.scheme
6584 =/ vars=(list @ud) vars.scheme
6283 ?~ vars [(itype-rename typ.scheme ren) state]
6586 ?~ vars [(itype-rename typ.scheme ren) state]
6587+ =/ fresh=@ud (named-var (var-name i.vars) next.state)
6284 =/ replacement=itype
6588 =/ replacement=itype
6285− ?:((itype-var-is-restricted i.vars typ.scheme) [%rvar next.state] ?:((itype-var-is-atom i.vars typ.scheme) [%avar next.state] ?:((itype-var-is-gate-free i.vars typ.scheme) [%fvar next.state] [%var next.state])))
6589+ ?:((itype-var-is-restricted i.vars typ.scheme) [%rvar fresh] ?:((itype-var-is-atom i.vars typ.scheme) [%avar fresh] ?:((itype-var-is-gate-free i.vars typ.scheme) [%fvar fresh] [%var fresh])))
6286 :: A generalized atom variable is a valid origin for re-generalizing
6590 :: A generalized atom variable is a valid origin for re-generalizing
6287 :: an alias, just as a sample binder is.
6591 :: an alias, just as a sample binder is.
6288 =/ st=istate state(next +(next.state))
6592 =/ st=istate state(next +(next.state))
6289− =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
6593+ =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [fresh binders.state]
6290 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6594 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6292++ icap-lookup
6596++ icap-lookup
@@ -7146,7 +7450,8 @@
7146 ?: in-mold.state ~
7450 ?: in-mold.state ~
7147 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
7451 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
7148 ?^ n `[[%var u.n] state]
7452 ?^ n `[[%var u.n] state]
7453+ =/ id=@ud (named-var name.sh next.state)
7149− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
7454+ `[[%var id] state(next +(next.state), caps [[name.sh id at.sh] caps.state])]
@@ -7179,12 +7484,12 @@
7179 ^- isample-result
7484 ^- isample-result
7182− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7487+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7183 [%| "sample shadows a name"]
7488 [%| "sample shadows a name"]
7184 =/ t=itype [%var next.state]
7489 =/ t=itype [%var next.state]
7185 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
7490 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
7187− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7492+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7188 [%| "sample shadows a name"]
7493 [%| "sample shadows a name"]
7189 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
7494 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
7190 ?~ t [%| "sample mold is not supported by partial inference"]
7495 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -7252,7 +7557,7 @@
7254 ?: ?=(%mold -.i.ds) $(ds t.ds)
7559 ?: ?=(%mold -.i.ds) $(ds t.ds)
7255− ?: =(name.i.ds %proj) |
7560+ ?: (reserved-name name.i.ds) |
7256 ?. (unique-value-name name.i.ds names) |
7561 ?. (unique-value-name name.i.ds names) |
7257 ?: ?=(^ (ienv-lookup name.i.ds env)) |
7562 ?: ?=(^ (ienv-lookup name.i.ds env)) |
7258 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
7563 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -7276,7 +7581,7 @@
7277 ?~ locals &
7582 ?~ locals &
7278 =/ n=term name.i.locals
7583 =/ n=term name.i.locals
7279− ?: =(n %proj) |
7584+ ?: (reserved-name n) |
7280 ?. (unique-value-name n names) |
7585 ?. (unique-value-name n names) |
7281 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
7586 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
7282 ?: (lien marks.state |=(m=term =(n m))) |
7587 ?: (lien marks.state |=(m=term =(n m))) |
@@ -7426,17 +7731,123 @@
7426 ^- istate
7731 ^- istate
7427 ?~ sites state
7732 ?~ sites state
7428 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7733 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7734+ =/ id=@ud (named-var name.i.sites next.state)
7429− $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
7735+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites id at.i.sites] caps.state]))
7431++ reserve-def-caps
7737++ reserve-def-caps
7432 |= [e=expr state=istate]
7738 |= [e=expr state=istate]
7433 ^- istate
7739 ^- istate
7434 (reserve-cap-sites (scope-expr e) state)
7740 (reserve-cap-sites (scope-expr e) state)
7742+:: +definite-diag: whether a failure is an error in the program itself
7744+:: A definite error names the sites that conflict. A form partial
7745+:: inference does not support names none, and neither does a name
7746+:: that is not inferred yet, such as a sibling that waits for a later
7747+:: pass. An uncertain hole is the one unsupported result with a site.
7753+ !=(msg.diag uncertain-hole-msg)
7755+:: +shared-types: what a body's shared variables resolve to
7757+:: The variables free in env or in the enclosing capitals, such as an
7758+:: enclosing gate's untyped sample, are shared by all of the body's
7759+:: locals. A local keeps monomorphic only the variables that these
7760+:: resolve to; it generalizes the rest, which each use renames.
7763+ |= [env=ienv caps=icaps sub=isub]
7764+ ^- (list [id=@ud typ=itype])
7766+ (unique-type-vars (weld (free-env-vars env sub) (free-cap-vars caps sub)))
7767+ |=(id=@ud [id (itype-normalize [%var id] sub)])
7769+:: +shared-moved: whether a sibling bound or refined a shared variable
7771+:: A sibling that infers can constrain a shared variable and so turn
7772+:: another local's failure into a success: +itype-fit accepts any type
7773+:: it can prove empty, so after `^- !! x` every cast of x fits. Such a
7774+:: failure can depend on the order siblings are tried in. A variable
7775+:: that a sibling keeps monomorphic occurs in what a shared variable
7776+:: resolves to, so constraining it moves a shared variable too. A
7777+:: substitution only grows, so when none moved, every sibling inferred
7778+:: so far, and the local, ran against the entry state and generalized
7782+ |= [shared=(list [id=@ud typ=itype]) sub=isub]
7784+ (lien shared |=([id=@ud typ=itype] !=(typ (itype-normalize [%var id] sub))))
7786+:: +closed-local: whether a local cannot see any shared variable
7788+:: A local that names no sibling, itself included, no name whose type
7789+:: had a free variable when the body was entered, and no enclosing
7790+:: capital that did, is inferred from generalized schemes and known
7791+:: types alone. What its siblings do cannot change its result, so its
7792+:: error is its own in any order. +sub is the substitution on entry,
7793+:: since a sibling may since have bound such a variable. The names are
7794+:: syntactic and ignore binders, so this errs closed.
7797+ |= [d=def siblings=(list term) env=ienv caps=icaps sub=isub]
7799+ ?. ?=(%value -.d) |
7800+ =/ deps=(list term) (dependency-expr val.d)
7801+ ?: (lien deps |=(n=term |(=(n name.d) (lien siblings |=(s=term =(s n)))))) |
7804+ =/ sc=(unit ischeme) (ienv-lookup n env)
7806+ ?=(^ (free-env-vars ~[[n u.sc]] sub))
7808+ %+ levy (scope-expr val.d)
7810+ =/ id=(unit @ud) (icap-lookup name.site caps)
7812+ ?=(~ (itype-vars (itype-normalize [%var u.id] sub)))
7814+:: +infer-local-defs: infer a body's local values in dependency order
7816+:: A definition that fails, or whose type is still pending, waits for
7817+:: the next pass, since it may refer to a sibling inferred later. When
7818+:: a pass makes no progress and no cyclic group applies, report the
7819+:: definite error of the earliest waiting definition, if no order of
7820+:: the siblings could change it; otherwise the message stays generic.
7822+:: A failure counts only if it names its sites. The failure of a
7823+:: local that sees no shared variable (+closed-local) is its own. Any
7824+:: other failure counts only if no shared variable had moved when it
7825+:: was tried, and, when the body has shared variables, every other
7826+:: waiting definition also failed with sites: one that waits without
7827+:: them, on a checker limit, a pending tag or its own nested stall,
7828+:: might in another order, or once supported, constrain a shared
7829+:: variable and so let the failing local pass. When all of them failed
7830+:: with sites and none moved a shared variable, the state is the same
7831+:: in every order. With no shared variables, each local is inferred
7832+:: from generalized schemes alone.
7834+:: A cyclic group's own errors are not kept. A definition that infers
7835+:: but is then unsupported reports that at once: a failure recorded
7836+:: earlier in the pass may still pass on a retry, once a sibling has
7837+:: constrained a shared variable.
7436++ infer-local-defs
7839++ infer-local-defs
7437 |= [ds=(list def) env=ienv state=istate]
7840 |= [ds=(list def) env=ienv state=istate]
7438 ^- ilocal-result
7841 ^- ilocal-result
7842+ =/ shared=(list [id=@ud typ=itype]) (shared-types env caps.state sub.state)
7439 =/ remaining=(list def) ~
7843 =/ remaining=(list def) ~
7844+ =/ siblings=(list term) (global-value-names ds)
7845+ =/ entry=isub sub.state
7846+ :: this pass's failures with sites that are closed or were tried before
7847+ :: any shared variable moved, newest first; and whether a definition
7848+ :: waits without sites
7849+ =/ failures=(list [diag=idiag closed=?]) ~
7440 =/ progressed=? |
7851 =/ progressed=? |
@@ -7446,16 +7857,35 @@
7446 =/ groups=icomponents (graph-components pending (global-value-names pending))
7857 =/ groups=icomponents (graph-components pending (global-value-names pending))
7447 =/ grouped=(unit [rest=(list def) env=ienv state=istate])
7858 =/ grouped=(unit [rest=(list def) env=ienv state=istate])
7448 (try-local-group pending groups env state)
7859 (try-local-group pending groups env state)
7861+ =/ sure=(list [diag=idiag closed=?])
7862+ ?: |(?=(~ shared) !blocked) failures
7863+ (skim failures |=([diag=idiag closed=?] closed))
7864+ ?^ sure [%| diag:(rear sure)]
7449− ?~ grouped [%| ["local definitions need unsupported inference" ~]]
7865+ [%| ["local definitions need unsupported inference" ~]]
7450− $(ds rest.u.grouped, remaining ~, env env.u.grouped, state state.u.grouped, progressed |)
7866+ $(ds rest.u.grouped, remaining ~, failures ~, blocked |, env env.u.grouped, state state.u.grouped, progressed |)
7451− $(ds (flop remaining), remaining ~, progressed |)
7867+ $(ds (flop remaining), remaining ~, failures ~, blocked |, progressed |)
7452 =/ d=def i.ds
7868 =/ d=def i.ds
7453 ?> ?=(%value -.d)
7869 ?> ?=(%value -.d)
7454 =/ local-state=istate (reserve-def-caps val.d state)
7870 =/ local-state=istate (reserve-def-caps val.d state)
7455− =/ inferred=iresult (infer-fragment val.d env local-state)
7871+ =/ plain=iresult (infer-fragment val.d env local-state)
7456− =/ retried=? ?=(%| -.inferred)
7872+ =/ inferred=iresult
7873+ ?: ?=(%& -.plain) plain
7457− =? inferred retried (infer-recursive-gate d env local-state)
7874+ (infer-recursive-gate d env local-state)
7875+ ?: ?=(%| -.inferred)
7876+ :: For a value that is not a gate the retry only says so; keep the
7877+ :: first failure unless the retry found a definite error.
7879+ ?: ?=(%& -.plain) p.inferred
7880+ ?: (definite-diag p.inferred) p.inferred
7882+ ?. (definite-diag failure) $(ds t.ds, remaining [d remaining], blocked &)
7883+ =/ closed=? (closed-local d siblings env caps.state entry)
7884+ =? failures |(closed !(shared-moved shared sub.state))
7885+ [[failure closed] failures]
7458− ?: ?=(%| -.inferred) $(ds t.ds, remaining [d remaining])
7886+ $(ds t.ds, remaining [d remaining])
7887+ :: Only the deferred transaction adds obligations, and it keeps no
7888+ :: failure reason. Obligations from a local are a checker limit.
7459 ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7889 ?: !=(obligations.state.p.inferred obligations.state) [%| ["deferred local definition needs unsupported inference" ~]]
7460 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7890 =. state.p.inferred (promote-restricted-numbers state.p.inferred env)
7461 =. 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)))
7891 =. 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)))
@@ -7469,14 +7899,15 @@
7469 [%| ["explicit capital constraints are not supported by partial inference" ~]]
7899 [%| ["explicit capital constraints are not supported by partial inference" ~]]
7470 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7900 =/ typ=itype (itype-normalize typ.p.inferred sub.state.p.inferred)
7471 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
7901 ?: |((pending-tags tags.state.p.inferred sub.state.p.inferred) (itype-has-tag typ))
7472− $(ds t.ds, remaining [d remaining])
7902+ $(ds t.ds, remaining [d remaining], blocked &)
7473 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
7903 ?: (unsupported-atom-vars typ caps.state.p.inferred binders.state.p.inferred sub.state.p.inferred)
7474− $(ds t.ds, remaining [d remaining])
7904+ $(ds t.ds, remaining [d remaining], blocked &)
7475 =/ free=(list @ud)
7905 =/ free=(list @ud)
7476 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7906 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7477 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7907 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7478 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7908 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7909+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.inferred sub.state.p.inferred)
7479− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
7910+ $(ds t.ds, env [[name.d named] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
7481:: Try complete cyclic local groups after individual definitions stall.
7912:: Try complete cyclic local groups after individual definitions stall.
7482:: Components with non-gates or unresolved constraints stay unavailable.
7913:: Components with non-gates or unresolved constraints stay unavailable.
@@ -7566,6 +7997,8 @@
7566 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
7997 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
7567 (infer-list-context e expected env state context)
7998 (infer-list-context e expected env state context)
7568 ?: ?=(%branch -.e)
7999 ?: ?=(%branch -.e)
8000+ =/ named=(unit idiag) (branch-tag-name e env state)
8001+ ?^ named [%| u.named]
7569 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
8002 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
7570 ?^ empty-list u.empty-list
8003 ?^ empty-list u.empty-list
7571 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
8004 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -7606,6 +8039,8 @@
7606 ?^ missing [%| u.missing]
8039 ?^ missing [%| u.missing]
7607 =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
8040 =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
7608 ?^ nested [%| u.nested]
8041 ?^ nested [%| u.nested]
8042+ =/ decimal=(unit idiag) (decimal-misfit e typ.p.value expected sub.state.p.value next.state.p.value)
8043+ ?^ decimal [%| u.decimal]
7609 ?: &(?=(%collection -.expected) =(%list name.expected))
8044 ?: &(?=(%collection -.expected) =(%list name.expected))
7610 [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
8045 [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
7611 ?: ?=(%flag -.expected)
8046 ?: ?=(%flag -.expected)
@@ -7671,11 +8106,15 @@
7671 =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
8106 =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
7672 ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
8107 ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
7673 ?: ?=(%bad -.fit)
8108 ?: ?=(%bad -.fit)
8109+ =/ decimal=(unit idiag) (decimal-misfit val.i.t.items.e typ.p.tail target sub.state.p.tail next.state.p.tail)
8110+ ?^ decimal [%| u.decimal]
7674 [%| ["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)]]]]
8111 [%| ["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)]]]]
7675 [%& target state.p.tail(sub sub.fit, next next.fit)]
8112 [%& target state.p.tail(sub sub.fit, next next.fit)]
8114+:: done holds the items already checked, the last first, so that a
8115+:: decimal among them can be blamed when a later item fixes its aura.
7677++ infer-open-list-items
8116++ infer-open-list-items
7678− |= [items=(list expr) expected=itype env=ienv state=istate context=span]
8117+ |= [items=(list expr) expected=itype env=ienv state=istate context=span done=(list expr)]
7679 ^- iresult
8118 ^- iresult
7680 ?~ items [%& expected state]
8119 ?~ items [%& expected state]
7681 =/ target=itype (itype-walk expected sub.state)
8120 =/ target=itype (itype-walk expected sub.state)
@@ -7691,10 +8130,18 @@
7691 ?: ?=(%bad -.fit)
8130 ?: ?=(%bad -.fit)
7692 ?: |((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))
8131 ?: |((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))
7693 [%| ["list item widening is not supported by partial inference" ~]]
8132 [%| ["list item widening is not supported by partial inference" ~]]
8133+ =/ decimal=(unit idiag) (decimal-misfit i.items typ.p.value target sub.state.p.value next.state.p.value)
8134+ ?^ decimal [%| u.decimal]
8135+ =/ earlier=(list expr) (flop done)
8138+ =/ found=(unit idiag) (decimal-misfit-at i.earlier typ.p.value sub.state.p.value)
8139+ ?^ found [%| u.found]
8140+ $(earlier t.earlier)
7694 [%| ["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)]]]]
8141 [%| ["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)]]]]
7695 ?: (itype-has-tag (itype-normalize expected sub.fit))
8142 ?: (itype-has-tag (itype-normalize expected sub.fit))
7696 [%| ["list item needs context in partial inference" ~]]
8143 [%| ["list item needs context in partial inference" ~]]
7697− $(items t.items, state state.p.value(sub sub.fit, next next.fit))
8144+ $(items t.items, state state.p.value(sub sub.fit, next next.fit), done [i.items done])
7699++ infer-list-items
8146++ infer-list-items
7700 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
8147 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
@@ -7715,6 +8162,8 @@
7715 ?^ missing [%| u.missing]
8162 ?^ missing [%| u.missing]
7716 =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
8163 =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
7717 ?^ nested [%| u.nested]
8164 ?^ nested [%| u.nested]
8165+ =/ decimal=(unit idiag) (decimal-misfit i.items typ.p.value target sub.state.p.value next.state.p.value)
8166+ ?^ decimal [%| u.decimal]
7718 [%| ["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)]]]]
8167 [%| ["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)]]]]
7719 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
8168 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
@@ -7812,7 +8261,7 @@
7812 [%| ["list branch pattern is not supported by partial inference" ~]]
8261 [%| ["list branch pattern is not supported by partial inference" ~]]
7813 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
8262 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
7814 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
8263 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
7815− ?: |(=(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)))))
8264+ ?: |((reserved-name head.u.binder) (reserved-name tail.u.binder) =(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)))))
7816 [%| ["pattern binder shadows a name" ~]]
8265 [%| ["pattern binder shadows a name" ~]]
7817 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
8266 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
7818 =/ left=iresult
8267 =/ left=iresult
@@ -7824,9 +8273,9 @@
7824 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
8273 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
7825 ?: ?=(%| -.right) right
8274 ?: ?=(%| -.right) right
7826 ?^ expected [%& typ.u.expected state.p.right]
8275 ?^ expected [%& typ.u.expected state.p.right]
7827− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
8276+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)
7828 ?~ joined [%| ["list branch results need unsupported inference" ~]]
8277 ?~ joined [%| ["list branch results need unsupported inference" ~]]
7829− [%& typ.p.left state.p.right(sub u.joined)]
8278+ [%& typ.u.joined state.p.right(sub sub.u.joined)]
7831++ infer-unit-branch
8280++ infer-unit-branch
7832 |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
8281 |= [e=expr env=ienv state=istate expected=(unit [typ=itype context=span])]
@@ -7849,7 +8298,7 @@
7849 [%| ["unit branch pattern is not supported by partial inference" ~]]
8298 [%| ["unit branch pattern is not supported by partial inference" ~]]
7850 =/ binder=(unit term) ?:(first-empty second-name first-name)
8299 =/ binder=(unit term) ?:(first-empty second-name first-name)
7851 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
8300 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
7852− ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
8301+ ?: |((reserved-name u.binder) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
7853 [%| ["pattern binder shadows a name" ~]]
8302 [%| ["pattern binder shadows a name" ~]]
7854 =/ payload=(unit itype) (unit-union-payload typ)
8303 =/ payload=(unit itype) (unit-union-payload typ)
7855 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
8304 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -7868,9 +8317,9 @@
7868 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
8317 (infer-union-context val.y typ.u.expected ?:(first-empty extended env) state.p.left context.u.expected)
7869 ?: ?=(%| -.right) right
8318 ?: ?=(%| -.right) right
7870 ?^ expected [%& typ.u.expected state.p.right]
8319 ?^ expected [%& typ.u.expected state.p.right]
7871− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
8320+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)
7872 ?~ joined [%| ["unit branch results need unsupported inference" ~]]
8321 ?~ joined [%| ["unit branch results need unsupported inference" ~]]
7873− [%& typ.p.left state.p.right(sub u.joined)]
8322+ [%& typ.u.joined state.p.right(sub sub.u.joined)]
7875:: Infer pieces in order, retaining their substitutions and pending tags.
8324:: Infer pieces in order, retaining their substitutions and pending tags.
7876:: A bare decimal literal has no outside type constraint, so it takes its
8325:: A bare decimal literal has no outside type constraint, so it takes its
@@ -7956,11 +8405,83 @@
7956 ^- (unit ienv)
8405 ^- (unit ienv)
7957 =. t ?:(?=(%face -.t) body.t t)
8406 =. t ?:(?=(%face -.t) body.t t)
7958 ?: ?=(%bind -.p)
8407 ?: ?=(%bind -.p)
7959− ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
8408+ ?: |((reserved-name name.p) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
7960 `[[name.p [t ~]] env]
8409 `[[name.p [t ~]] env]
7961 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
8410 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
8413+:: +branch-tag-name: a ?- pattern name that spells one of the subject's tags
8415+:: A name in a pattern binds, so `stop` written for `%stop` would
8416+:: catch every case left. Where the subject's type at a name's
8417+:: position is a union, or a one-case mold, with a case whose constant
8418+:: there is the term the name spells, the name is an error (Grammar,
8419+:: Patterns). Every path that checks a ?- asks this first, so they
8420+:: agree; it infers the subject apart and drops the state it leaves.
8421+:: A subject that fails, or whose type isn't known yet, is left to the
8422+:: path. Samples aren't patterns: every sample name binds.
8424+ |= [e=expr env=ienv state=istate]
8426+ ?. ?=(%branch -.e) ~
8427+ ?. (lien arms.e |=(a=arm (union-pattern-has-bind pat.a))) ~
8428+ =/ subject=iresult (infer-fragment subject.e env state)
8429+ ?: ?=(%| -.subject) ~
8430+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8431+ =/ arms=(list arm) arms.e
8434+ =/ found=(unit [at=span name=term]) (tag-name-pattern pat.i.arms typ ~)
8435+ ?~ found $(arms t.arms)
8436+ =/ name=tape (trip name.u.found)
8438+ :- "`{name}` binds a name, but the subject's type has `%{name}` here; write %{name}, or * for a catch-all"
8439+ ~[[(span-of subject.e) "subject"] [at.u.found "pattern name"]]
8441+:: +tag-name-pattern: the first name in p that t types by a tag
8443+:: The walk enters faces, cells and unions, and of a union only the
8444+:: cases a cell pattern can match, so `[t %draft]` reads t at @t. It
8445+:: stops at atoms, `*`, variables, collections and recursive molds,
8446+:: and at a generic union's argument positions, which a type variable
8447+:: types in its mold, as u in `[~ u=A]`.
8449+ |= [p=pattern t=itype args=(list itype)]
8450+ ^- (unit [at=span name=term])
8451+ ?. ?=(?(%bind %cell) -.p) ~
8452+ ?: ?=(%face -.t) $(t body.t)
8453+ ?: (lien args |=(a=itype =(a t))) ~
8455+ =/ inner=(list itype) (weld args.t args)
8456+ =/ cases=(list itype) cases.t
8459+ ?: &(?=(%cell -.p) =(%none (union-pattern p i.cases))) $(cases t.cases)
8460+ =/ found=(unit [at=span name=term]) (tag-name-pattern p i.cases inner)
8463+ ?: ?=(%cell -.p) (tag-name-items items.p t args)
8464+ ?. ?=(%const -.t) ~
8465+ ?. &(=(%term form.literal.t) =(%tas aura.literal.t) =(name.p val.literal.t)) ~
8468+:: +tag-name-items: +tag-name-pattern along a cell pattern's items
8470+:: As in +union-pattern-items, the last item takes the rest of the
8471+:: spine. A union mid-spine is read as the rest of the pattern.
8473+ |= [ps=(list pattern) t=itype args=(list itype)]
8474+ ^- (unit [at=span name=term])
8476+ ?~ t.ps (tag-name-pattern i.ps t args)
8477+ ?: ?=(%face -.t) $(t body.t)
8478+ ?: (lien args |=(a=itype =(a t))) ~
8479+ ?: ?=(%union -.t) (tag-name-pattern [%cell at.i.ps ps] t args)
8481+ =/ head=(unit [at=span name=term]) (tag-name-pattern i.ps hed.t args)
8483+ $(ps t.ps, t tal.t)
7964:: Split loobean fields into finite refinements for partial patterns.
8485:: Split loobean fields into finite refinements for partial patterns.
7965:: Keep original cases for binder types and preserve whole-case matching
8486:: Keep original cases for binder types and preserve whole-case matching
7966:: before trying refinements. Cap products at 64; unknown, empty or opaque
8487:: before trying refinements. Cap products at 64; unknown, empty or opaque
@@ -8008,6 +8529,8 @@
8008 ^- (unit iresult)
8529 ^- (unit iresult)
8009 ?> ?=(%branch -.e)
8530 ?> ?=(%branch -.e)
8010 ?: ?=(%| -.subject) `subject
8531 ?: ?=(%| -.subject) `subject
8532+ =/ decimal=(unit idiag) (decimal-arms-misfit arms.e typ.p.subject sub.state.p.subject)
8533+ ?^ decimal `[%| u.decimal]
8011 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8534 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8012 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
8535 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
8013 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
8536 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
@@ -8016,13 +8539,14 @@
8016 =/ remaining=(list itype) cases
8539 =/ remaining=(list itype) cases
8017 =/ arms=(list arm) arms.e
8540 =/ arms=(list arm) arms.e
8018 =/ st=istate state.p.subject
8541 =/ st=istate state.p.subject
8019− =/ answer=(unit itype) ~
8542+ =/ results=(list itype) ~
8022 ?^ remaining
8545 ?^ remaining
8023 `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
8546 `[%| ["missing union case {(show-itype i.remaining sub.st)}" ~]]
8024− ?~ answer `[%| ["empty union branch is not supported by partial inference" ~]]
8547+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join-list (flop results) sub.st)
8025− `[%& u.answer st]
8548+ ?~ joined `[%| ["union branch result matching needs unsupported inference" ~]]
8549+ `[%& typ.u.joined st(sub sub.u.joined)]
8026 =/ a=arm i.arms
8550 =/ a=arm i.arms
8027 ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
8551 ?: (lien remaining |=(c=itype =(%unknown (union-pattern pat.a c))))
@@ -8038,15 +8562,15 @@
8038 =/ body=iresult (infer-fragment val.a u.bound st)
8562 =/ body=iresult (infer-fragment val.a u.bound st)
8039 ?: ?=(%| -.body) `body
8563 ?: ?=(%| -.body) `body
8040 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
8564 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
8041− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
8042− ?: mismatch `[%| ["union branch result matching needs unsupported inference" ~]]
8043− $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, answer `result)
8565+ $(arms t.arms, remaining (skim remaining |=(c=itype !=(%full (union-pattern pat.a c)))), st state.p.body, results [result results])
8045++ infer-known-union-context-whole
8567++ infer-known-union-context-whole
8046 |= [e=expr expected=itype env=ienv subject=iresult context=span]
8568 |= [e=expr expected=itype env=ienv subject=iresult context=span]
8047 ^- (unit iresult)
8569 ^- (unit iresult)
8048 ?> ?=(%branch -.e)
8570 ?> ?=(%branch -.e)
8049 ?: ?=(%| -.subject) `subject
8571 ?: ?=(%| -.subject) `subject
8572+ =/ decimal=(unit idiag) (decimal-arms-misfit arms.e typ.p.subject sub.state.p.subject)
8573+ ?^ decimal `[%| u.decimal]
8050 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8574 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8051 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
8575 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
8052 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
8576 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
@@ -8103,14 +8627,16 @@
8103 =/ remaining=(list ifinite) cases
8627 =/ remaining=(list ifinite) cases
8104 =/ arms=(list arm) arms.e
8628 =/ arms=(list arm) arms.e
8105 =/ st=istate state.p.subject
8629 =/ st=istate state.p.subject
8106− =/ answer=(unit itype) ~
8630+ =/ results=(list itype) ~
8109 ?^ remaining
8633 ?^ remaining
8110 [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
8634 [%| ["missing union case {(show-itype part.i.remaining sub.st)}" ~]]
8111− ?~ answer [%| ["empty union branch is not supported by partial inference" ~]]
8635+ ?~ results [%| ["empty union branch is not supported by partial inference" ~]]
8112− ?~ expected [%& u.answer st]
8636+ ?^ expected [%& typ.u.expected st]
8113− [%& typ.u.expected st]
8637+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join-list (flop results) sub.st)
8638+ ?~ joined [%| ["union branch result matching needs unsupported inference" ~]]
8639+ [%& typ.u.joined st(sub sub.u.joined)]
8114 =/ a=arm i.arms
8640 =/ a=arm i.arms
8115 ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
8641 ?: (lien remaining |=(c=ifinite =(%unknown (union-pattern pat.a part.c))))
8116 [%| ["partial union pattern is not supported by partial inference" ~]]
8642 [%| ["partial union pattern is not supported by partial inference" ~]]
@@ -8138,11 +8664,9 @@
8138 [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
8664 [%| ["union branch arm does not fit its expected type" ~[[context.u.expected "expected type"] [(span-of val.a) "branch arm"]]]]
8139 ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8665 ?: (itype-has-tag (itype-normalize typ.u.expected sub.fit))
8140 [%| ["union branch result needs context in partial inference" ~]]
8666 [%| ["union branch result needs context in partial inference" ~]]
8141− $(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)
8667+ $(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), results [typ.p.body results])
8142 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
8668 =/ result=itype (itype-normalize typ.p.body sub.state.p.body)
8143− =/ mismatch=? ?~(answer | !=((itype-normalize u.answer sub.state.p.body) result))
8144− ?: mismatch [%| ["union branch result matching needs unsupported inference" ~]]
8145− $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, answer `result)
8669+ $(arms t.arms, remaining (skim remaining |=(c=ifinite !=(%full (union-pattern pat.a part.c)))), st state.p.body, results [result results])
8147:: Prove a one-arm record pattern covers a known, non-union subject.
8671:: Prove a one-arm record pattern covers a known, non-union subject.
8148:: Variable or partial matches stay unsupported; binding uses the same
8672:: Variable or partial matches stay unsupported; binding uses the same
@@ -8407,7 +8931,9 @@
8407 `subject
8931 `subject
8409:: Infer changes only against a fully known record spine. Retain the
8933:: Infer changes only against a fully known record spine. Retain the
8410−:: target type; unknown spines and repeated edits remain unsupported.
8934+:: target type; unknown spines and overlapping edits remain unsupported.
8935+:: An edit's wing, as open.cart, reads through record fields only,
8936+:: outermost first, and its value fits the field it names.
8411++ change-spine-known
8937++ change-spine-known
8412 |= [t=itype sub=isub]
8938 |= [t=itype sub=isub]
@@ -8419,26 +8945,87 @@
8419 $(t tal.t)
8945 $(t tal.t)
8421++ infer-change-edits
8947++ infer-change-edits
8422− |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
8948+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list (list term))]
8423 ^- iresult
8949 ^- iresult
8424 ?~ edits [%& target state]
8950 ?~ edits [%& target state]
8425 =/ entry=edit i.edits
8951 =/ entry=edit i.edits
8426− ?: (lien seen |=(name=term =(name name.entry)))
8952+ =/ outer=(list term) (flop names.entry)
8953+ ?: (lien seen |=(prior=(list term) (wing-overlap prior outer)))
8427 [%| ["repeated change fields are not supported by partial inference" ~]]
8954 [%| ["repeated change fields are not supported by partial inference" ~]]
8428 ?. (change-spine-known target sub.state)
8955 ?. (change-spine-known target sub.state)
8429 [%| ["change target needs a known record in partial inference" ~]]
8956 [%| ["change target needs a known record in partial inference" ~]]
8430− =/ found=(list itype) (record-fields-named name.entry target sub.state)
8957+ =/ field=(each itype idiag) (change-wing-field entry target sub.state)
8431− ?~ found
8958+ ?: ?=(%| -.field) [%| p.field]
8432− [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
8433− ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
8434− =/ expected=itype i.found
8959+ =/ expected=itype p.field
8435 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
8960 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
8436 ?: ?=(%| -.value) value
8961 ?: ?=(%| -.value) value
8437 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
8962 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
8438 ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
8963 ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
8439 ?: ?=(%bad -.fit)
8964 ?: ?=(%bad -.fit)
8965+ =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
8966+ ?^ decimal [%| u.decimal]
8440 [%| ["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)]]]]
8967 [%| ["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)]]]]
8441− $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
8968+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [outer seen])
8970+:: +change-wing-field: the type of the field an edit's wing names in
8971+:: a known record target, read through record fields, outermost first
8973+++ change-wing-field
8974+ |= [entry=edit target=itype sub=isub]
8975+ ^- (each itype idiag)
8976+ =/ outer=(list term) (flop names.entry)
8977+ =/ k=@ud (lent names.entry)
8978+ =/ typ=itype target
8979+ =| through=(unit [name=term at=span])
8980+ |- ^- (each itype idiag)
8982+ =/ here=span (edit-name-at entry (dec k))
8983+ ?: &(?=(^ through) !(change-spine-known typ sub))
8984+ ?. (itype-not-record typ sub)
8985+ [%| ["change wing needs a known record in partial inference" ~]]
8986+ =/ label=tape "field `{(trip name.u.through)}`"
8988+ :- "change wing `{(show-names names.entry)}` goes through `{(trip name.u.through)}`, which is not a record"
8989+ ~[[at.u.through (site-type-note label typ sub)]]
8990+ =/ found=(list itype) (record-fields-named i.outer typ sub)
8992+ [%| ["record has no field `{(trip i.outer)}`" ~[[here "unknown field"]]]]
8993+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
8994+ $(outer t.outer, k (dec k), typ i.found, through `[i.outer here])
8996+:: +edit-name-at: where the kth name of an edit's wing is written,
8997+:: counting from 0: its names are joined by dots from the edit's start
9002+ =/ col=@ud col.beg.at.e
9003+ =/ ns=(list term) names.e
9006+ =/ len=@ud (met 3 i.ns)
9007+ ?: =(0 k) [[line.beg.at.e col] [line.beg.at.e (add col len)]]
9008+ $(ns t.ns, k (dec k), col +((add col len)))
9010+:: +itype-not-record: whether a type is surely no record: an atom, a
9011+:: loobean, a list or other collection, a gate, a union or a noun
9014+ |= [t=itype sub=isub]
9016+ =. t (itype-walk t sub)
9017+ ?=(?(%atom %any-atom %flag %const %tag %collection %fn %union %noun %empty) -.t)
9019+:: +wing-overlap: whether two edits' wings, outermost first, name the
9020+:: same field or one a field inside the other's
9023+ |= [a=(list term) b=(list term)]
8443:: Backtick constructs the canonical prelude unit, after checking its
9030:: Backtick constructs the canonical prelude unit, after checking its
8444:: prepared template has the standard null and [~ u=A] cases.
9031:: prepared template has the standard null and [~ u=A] cases.
@@ -8542,6 +9129,183 @@
8542 ?. ?=(%ok -.first) ~
9129 ?. ?=(%ok -.first) ~
8543 $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
9130 $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
9132+:: +decimal-misfit: a decimal's error where another aura is expected
9134+:: A bare decimal is a @ud and fits only @ud, @u, @ and * (S4). After
9135+:: a value fails to fit, refit it with each decimal's variable widened
9136+:: to any aura (+decimal-relax), so that a gate's shared capital learns
9137+:: its aura from the other arguments, then walk the value's syntax
9138+:: beside the type it should fit. The first decimal whose place is an
9139+:: atom of another aura gets the error; otherwise ~, and the caller's
9140+:: own error stands.
9143+ |= [e=expr actual=itype expected=itype sub=isub next=@ud]
9145+ =/ loose=isub (turn sub |=(b=ibinding b(val (decimal-relax val.b))))
9146+ =/ fit=ifit (itype-fit (decimal-relax actual) (decimal-relax expected) loose next)
9147+ (decimal-misfit-at e (decimal-relax expected) ?:(?=(%ok -.fit) sub.fit loose))
9149+:: +decimal-relax: a type with each decimal's variable taking any aura
9156+ %rnvar [%rvar id.t]
9157+ %collection t(args (turn args.t |=(c=itype (decimal-relax c))))
9158+ %grec t(args (turn args.t |=(c=itype (decimal-relax c))))
9159+ %union t(cases (turn cases.t |=(c=itype (decimal-relax c))), args (turn args.t |=(c=itype (decimal-relax c))))
9160+ %face t(body $(t body.t))
9161+ %fn [%fn $(t sample.t) $(t product.t)]
9162+ %cell [%cell $(t hed.t) $(t tal.t)]
9165+:: +decimal-misfit-at: walk a value beside the type it should fit
9167+:: Through groups, faces, tuples and term-headed pairs, the union case
9168+:: a tuple's head tag picks, units and list literals.
9170+++ decimal-misfit-at
9171+ |= [e=expr expected=itype sub=isub]
9173+ =. expected (itype-walk expected sub)
9174+ ?: ?=(%face -.expected) $(expected body.expected)
9176+ %lit (decimal-lit-misfit at.e lit.e expected |)
9177+ %group $(e inner.e)
9178+ %pair $(e (pair-as-cell e))
9179+ %tuple (decimal-misfit-items items.e expected sub)
9181+ ?. ?=(%collection -.expected) ~
9182+ ?. &(=(%unit name.expected) ?=([* ~] args.expected)) ~
9183+ $(e val.e, expected i.args.expected)
9185+ ?. ?=(%collection -.expected) ~
9186+ ?. &(=(%list name.expected) ?=([* ~] args.expected)) ~
9187+ =/ items=(list expr) items.e
9190+ =/ found=(unit idiag) ^$(e i.items, expected i.args.expected)
9195+:: +decimal-misfit-items: a tuple's items beside a cell, the last its tail
9197+++ decimal-misfit-items
9198+ |= [items=(list item) expected=itype sub=isub]
9201+ ?~ t.items (decimal-misfit-at val.i.items expected sub)
9202+ =. expected (itype-walk expected sub)
9203+ ?: ?=(%face -.expected) $(expected body.expected)
9204+ ?: ?=(%union -.expected)
9205+ =/ head=expr val.i.items
9206+ ?. ?=(%lit -.head) ~
9207+ =/ case=(unit itype) (decimal-case val.lit.head cases.expected sub)
9210+ ?. ?=(%cell -.expected) ~
9211+ =/ found=(unit idiag) (decimal-misfit-at val.i.items hed.expected sub)
9213+ $(items t.items, expected tal.expected)
9215+:: +decimal-pattern-misfit: a decimal pattern where another aura is matched
9217+:: The subject's type is known, so no refit is needed. A cell pattern
9218+:: picks its union case by its head, as a tuple does.
9220+++ decimal-pattern-misfit
9221+ |= [p=pattern expected=itype sub=isub]
9223+ =. expected (itype-walk expected sub)
9224+ ?: ?=(%face -.expected) $(expected body.expected)
9225+ ?: ?=(%lit -.p) (decimal-lit-misfit at.p lit.p expected &)
9227+ (decimal-pattern-items items.p expected sub)
9229+:: +decimal-pattern-items: a cell pattern's items, as +decimal-misfit-items
9231+++ decimal-pattern-items
9232+ |= [items=(list pattern) expected=itype sub=isub]
9235+ ?~ t.items (decimal-pattern-misfit i.items expected sub)
9236+ =. expected (itype-walk expected sub)
9237+ ?: ?=(%face -.expected) $(expected body.expected)
9238+ ?: ?=(%union -.expected)
9239+ ?. ?=(%lit -.i.items) ~
9240+ =/ case=(unit itype) (decimal-case val.lit.i.items cases.expected sub)
9243+ ?. ?=(%cell -.expected) ~
9244+ =/ found=(unit idiag) (decimal-pattern-misfit i.items hed.expected sub)
9246+ $(items t.items, expected tal.expected)
9248+:: +decimal-arms-misfit: the first arm whose pattern has a misplaced decimal
9250+++ decimal-arms-misfit
9251+ |= [arms=(list arm) subject=itype sub=isub]
9254+ =/ found=(unit idiag) (decimal-pattern-misfit pat.i.arms subject sub)
9258+:: +decimal-case: the one union case whose head is the constant value
9261+ |= [value=@ cases=(list itype) sub=isub]
9263+ =/ hits=(list itype)
9266+ =. c (itype-walk c sub)
9268+ =/ head=itype (itype-walk hed.c sub)
9269+ =? head ?=(%face -.head) (itype-walk body.head sub)
9270+ &(?=(%const -.head) =(value val.literal.head))
9271+ ?. ?=([* ~] hits) ~
9274+:: +decimal-lit-misfit: the error for a decimal at a place of known type
9276+++ decimal-lit-misfit
9277+ |= [at=span l=lit expected=itype pattern=?]
9279+ ?. &(=(%number form.l) =(%ud aura.l)) ~
9280+ ?. ?=(%atom -.expected) ~
9281+ ?: (decimal-aura aura.expected) ~
9282+ `[(decimal-misfit-msg l aura.expected pattern) ~[[at "decimal"]]]
9284+:: +decimal-misfit-msg: "`30` is a @ud, not a @dr; write ~s30"
9286+:: The hint writes the value in the expected aura's own literal where
9287+:: that reads naturally: 30 seconds, the text "30", the ship ~syd; a
9288+:: date gets an example. Patterns take no dates, durations or knots,
9289+:: so in a pattern those auras get no hint.
9291+++ decimal-misfit-msg
9292+ |= [l=lit aura=@ta pattern=?]
9294+ =/ what=tape "`{(trip txt.l)}` is a @ud, not a @{(trip aura)}"
9296+ ?: &(pattern ?=(?(%da %dr %ta) aura)) ""
9298+ %da "a date, as ~2026.1.1"
9299+ %dr (trip (scot %dr (mul val.l ~s1)))
9300+ %p (trip (scot %p val.l))
9301+ %t (show-quoted txt.l)
9302+ %ta "~.{(trip txt.l)}"
9303+ %ux (trip (scot %ux val.l))
9304+ %uv (trip (scot %uv val.l))
9307+ "{what}; write {hint}"
8545:: A term-headed pair is the same noun as a two-item cell. Preserve the
9309:: A term-headed pair is the same noun as a two-item cell. Preserve the
8546:: whole pair span for the synthetic head and the value's own span for
9310:: whole pair span for the synthetic head and the value's own span for
8547:: the payload; unresolved term constraints follow ordinary cell inference.
9311:: the payload; unresolved term constraints follow ordinary cell inference.
@@ -8599,7 +9363,7 @@
8599 ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
9363 ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
8600 [%| ["list literal needs the standard prelude in partial inference" ~]]
9364 [%| ["list literal needs the standard prelude in partial inference" ~]]
8601 =/ element=itype [%var next.state]
9365 =/ element=itype [%var next.state]
8602− =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
9366+ =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e ~)
8603 ?: ?=(%| -.result) result
9367 ?: ?=(%| -.result) result
8604 [%& [%collection %list ~[element]] state.p.result]
9368 [%& [%collection %list ~[element]] state.p.result]
8605 %str (infer-string-pieces pieces.e env state)
9369 %str (infer-string-pieces pieces.e env state)
@@ -8631,6 +9395,7 @@
8631 [%& typ.instance state.instance]
9395 [%& typ.instance state.instance]
8632 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
9396 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
8633 ?~ scheme
9397 ?~ scheme
9398+ ?: =(i.names.e %unface) [%| (unface-value at.e)]
8634 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
9399 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
8635 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
9400 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
8636 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
9401 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
@@ -8638,7 +9403,10 @@
8638 [%& typ.inst state.inst]
9403 [%& typ.inst state.inst]
8639 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
9404 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
8640 [%& typ.instance state.instance]
9405 [%& typ.instance state.instance]
9407+ ?: &(?=(%wing -.inner.e) =(names.inner.e ~[%unface]) ?=(~ (ienv-lookup %unface env)))
9408+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
8641− %group $(e inner.e)
9409+ $(e inner.e)
8643 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
9411 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
8644 =/ target=iresult $(e [%wing at.e target.e])
9412 =/ target=iresult $(e [%wing at.e target.e])
@@ -8675,6 +9443,8 @@
8675 ?: ?=(%| -.result) result
9443 ?: ?=(%| -.result) result
8676 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
9444 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
9446+ =/ named=(unit idiag) (branch-tag-name e env state)
9447+ ?^ named [%| u.named]
8678 ?^ defer.state (dg-boolean-branch e env state)
9448 ?^ defer.state (dg-boolean-branch e env state)
8679 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
9449 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
8680 ?~ t.arms.e
9450 ?~ t.arms.e
@@ -8715,22 +9485,22 @@
8715 ?: ?=(%| -.right) right
9485 ?: ?=(%| -.right) right
8716 =/ ltype=itype (itype-normalize typ.p.left sub.state.p.right)
9486 =/ ltype=itype (itype-normalize typ.p.left sub.state.p.right)
8717 =/ rtype=itype (itype-normalize typ.p.right sub.state.p.right)
9487 =/ rtype=itype (itype-normalize typ.p.right sub.state.p.right)
8718− ?: &(!=(ltype rtype) |(?=(^ (itype-vars ltype)) ?=(^ (itype-vars rtype))) |((itype-has-fixed-atom ltype) (itype-has-fixed-atom rtype)))
8719− [%| ["branch widening is not supported by partial inference" ~]]
8720− =/ joined=(unit isub) (itype-unify typ.p.left typ.p.right sub.state.p.right)
9488+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)
8721 ?~ joined
9489 ?~ joined
8722 ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
9490 ?: |((itype-has-recursive ltype) (itype-has-recursive rtype))
8723 [%| ["recursive branch matching is not supported by partial inference" ~]]
9491 [%| ["recursive branch matching is not supported by partial inference" ~]]
8724 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
9492 ?: |((itype-has-tag ltype) (itype-has-tag rtype) (itype-has-union ltype) (itype-has-union rtype))
8725 [%| ["branch tag or union context is not supported by partial inference" ~]]
9493 [%| ["branch tag or union context is not supported by partial inference" ~]]
8726− =/ common=(unit itype) (itype-concrete-join typ.p.left typ.p.right sub.state.p.right)
8727− ?^ common [%& u.common state.p.right]
8728 ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))
9494 ?: |((itype-has-face typ.p.left sub.state.p.right) (itype-has-face typ.p.right sub.state.p.right))
8729 [%| ["record branch matching is not supported by partial inference" ~]]
9495 [%| ["record branch matching is not supported by partial inference" ~]]
8730 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
9496 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
8731 [%| ["branch widening is not supported by partial inference" ~]]
9497 [%| ["branch widening is not supported by partial inference" ~]]
9498+ =/ decimal-x=(unit idiag) (decimal-misfit val.x typ.p.left typ.p.right sub.state.p.right next.state.p.right)
9499+ ?^ decimal-x [%| u.decimal-x]
9500+ =/ decimal-y=(unit idiag) (decimal-misfit val.y typ.p.right typ.p.left sub.state.p.right next.state.p.right)
9501+ ?^ decimal-y [%| u.decimal-y]
8732 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
9502 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
8733− [%& typ.p.left state.p.right(sub u.joined)]
9503+ [%& typ.u.joined state.p.right(sub sub.u.joined)]
8735 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
9505 =/ target=(unit [typ=itype state=istate]) (infer-simple-shape shape.e state)
8736 ?~ target
9506 ?~ target
@@ -8750,6 +9520,8 @@
8750 ?^ missing [%| u.missing]
9520 ?^ missing [%| u.missing]
8751 =/ 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)
9521 =/ 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)
8752 ?^ nested [%| u.nested]
9522 ?^ nested [%| u.nested]
9523+ =/ decimal=(unit idiag) (decimal-misfit val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value)
9524+ ?^ decimal [%| u.decimal]
8753 [%| ["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)]]]]
9525 [%| ["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)]]]]
8754 ?: &(?=(^ defer.state.p.value) !(dg-stable-fit typ.p.value typ.u.target sub.fit))
9526 ?: &(?=(^ defer.state.p.value) !(dg-stable-fit typ.p.value typ.u.target sub.fit))
8755 [%| ["deferred cast fit needs stable inference" ~]]
9527 [%| ["deferred cast fit needs stable inference" ~]]
@@ -8778,6 +9550,7 @@
8778 ?~ args.e [%| ["call has no argument" ~]]
9550 ?~ args.e [%| ["call has no argument" ~]]
8779 ?: (explicit-proj-call e env state)
9551 ?: (explicit-proj-call e env state)
8780 [%| ["proj needs an expected record type" ~]]
9552 [%| ["proj needs an expected record type" ~]]
9553+ ?: (reserved-call %unface e env state) (infer-unface e env state)
8781 (infer-call-with-head e env state (infer-fragment head.e env state))
9554 (infer-call-with-head e env state (infer-fragment head.e env state))
8782 * [%| ["expression is not supported by partial inference" ~]]
9555 * [%| ["expression is not supported by partial inference" ~]]
@@ -9073,11 +9846,17 @@
9073 ?^ missing [%| u.missing]
9846 ?^ missing [%| u.missing]
9074 =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
9847 =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
9075 ?^ nested [%| u.nested]
9848 ?^ nested [%| u.nested]
9849+ =/ decimal=(unit idiag) (decimal-misfit i.args.e typ.p.arg sample.ht sub.st next.st)
9850+ ?^ decimal [%| u.decimal]
9076 [%| ["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)]]]]
9851 [%| ["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)]]]]
9077 =/ bad=(unit [at=span typ=itype])
9852 =/ bad=(unit [at=span typ=itype])
9078 (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
9853 (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
9079 =/ whole-args=span
9854 =/ whole-args=span
9080 [beg:(span-of i.args.e) end:(span-of (rear args.e))]
9855 [beg:(span-of i.args.e) end:(span-of (rear args.e))]
9856+ =/ decimal=(unit idiag)
9857+ =/ items=(list item) (turn args.e |=(a=expr [(span-of a) ~ a]))
9858+ (decimal-misfit [%tuple whole-args items] typ.p.arg sample.ht sub.st next.st)
9859+ ?^ decimal [%| u.decimal]
9081 =/ arg-at=span ?~(bad whole-args at.u.bad)
9860 =/ arg-at=span ?~(bad whole-args at.u.bad)
9082 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
9861 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
9083 [%| ["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)]]]]
9862 [%| ["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)]]]]
@@ -9148,6 +9927,8 @@
9148 ?^ missing [%| u.missing]
9927 ?^ missing [%| u.missing]
9149 =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
9928 =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
9150 ?^ nested [%| u.nested]
9929 ?^ nested [%| u.nested]
9930+ =/ decimal=(unit idiag) (decimal-misfit val.e typ.p.value payload sub.state.p.value next.state.p.value)
9931+ ?^ decimal [%| u.decimal]
9151 [%| ["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)]]]]
9932 [%| ["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)]]]]
9152 [%& expected state.p.value(sub sub.fit, next next.fit)]
9933 [%& expected state.p.value(sub sub.fit, next next.fit)]
@@ -9160,6 +9941,7 @@
9160 ^- iresult
9941 ^- iresult
9161 ?> ?=(%call -.e)
9942 ?> ?=(%call -.e)
9162 ?~ args.e [%| ["call has no argument" ~]]
9943 ?~ args.e [%| ["call has no argument" ~]]
9944+ ?: (reserved-call %unface e env state) (infer-unface e env state)
9163 =/ head=iresult (infer-fragment head.e env state)
9945 =/ head=iresult (infer-fragment head.e env state)
9164 ?: ?=(%| -.head) head
9946 ?: ?=(%| -.head) head
9165 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
9947 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
@@ -9242,18 +10024,70 @@
9242 `(infer-simple-items items.e env state)
10024 `(infer-simple-items items.e env state)
9243 `(width-infer-items items.e index.u.target env state context)
10025 `(width-infer-items items.e index.u.target env state context)
10027+:: +reserved-call: whether e calls the reserved operation n
9245−:: Experimental intrinsic recognition; real bindings retain normal calls.
10029+:: Experimental intrinsic recognition; real bindings retain normal calls.
10031+ |= [n=term e=expr env=ienv state=istate]
10033+ ?. ?=(%call -.e) |
10034+ ?. ?=(%wing -.head.e) |
10035+ ?. =(names.head.e ~[n]) |
10036+ ?: ?=(^ (ienv-lookup n env)) |
10037+ ?: (lien globals.state |=(x=term =(x n))) |
10038+ ?~ prelude.state &
10039+ ?:(?=(^ (ienv-lookup n values.u.prelude.state)) | &)
9246++ explicit-proj-call
10040++ explicit-proj-call
9247 |= [e=expr env=ienv state=istate]
10041 |= [e=expr env=ienv state=istate]
9249 ?. ?=(%call -.e) |
10043 ?. ?=(%call -.e) |
9250 ?. ?=([* ~] args.e) |
10044 ?. ?=([* ~] args.e) |
9251− ?. ?=(%wing -.head.e) |
10045+ (reserved-call %proj e env state)
9252− ?. =(names.head.e ~[%proj]) |
10046+::
9253− ?: ?=(^ (ienv-lookup %proj env)) |
10047+:: +infer-unface: (unface e), e's type with every face removed
9254− ?: (lien globals.state |=(n=term =(n %proj))) |
10048+::
9255− ?~ prelude.state &
10049+:: A reserved operation handled by type, like proj. Any number of
9256− ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
10050+:: arguments is taken here so that a wrong count is an error. A type
10051+:: not yet known would wait, as wing access does; the partial checker
10052+:: has no such wait and reports it as unsupported, as it does field
10053+:: access on such a type.
10055+ |= [e=expr env=ienv state=istate]
10058+ ?. ?=([* ~] args.e)
10059+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
10060+ ?^ defer.state [%| ["deferred unface needs unsupported inference" ~]]
10061+ =/ value=iresult (infer-fragment i.args.e env state)
10062+ ?: ?=(%| -.value) value
10063+ =/ typ=itype (itype-walk typ.p.value sub.state.p.value)
10064+ ?: ?=(?(%var %fvar) -.typ)
10065+ [%| ["unface on a type not yet known is not supported by partial inference" ~]]
10066+ [%& (itype-unface typ sub.state.p.value) state.p.value]
10068+:: +unface-value: the error for unface written where a value goes
10073+ ["unface is not a value; write |=(g (unface g))" ~[[at "unface used as a value"]]]
10075+:: +unfaced-gate: the gate under a ++'s (unface |= …), or ~
10077+:: Such a ++ is a gate for recursion: its own name has the unfaced
10078+:: type, and its body may call it.
10080+ |= [e=expr env=ienv state=istate]
10082+ ?: ?=(%group -.e) $(e inner.e)
10083+ ?. (reserved-call %unface e env state) ~
10085+ ?. ?=([* ~] args.e) ~
10086+ =/ gate=expr i.args.e
10088+ ?: ?=(%group -.gate) $(gate inner.gate)
10089+ ?. ?=(?(%gate %gate-wide) -.gate) ~
9257++ infer-proj-source
10091++ infer-proj-source
9258 |= [e=expr expected=itype env=ienv state=istate context=span]
10092 |= [e=expr expected=itype env=ienv state=istate context=span]
9259 ^- iresult
10093 ^- iresult
@@ -9516,6 +10350,8 @@
9516 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
10350 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
9517 [%& target state.p.value(sub sub.fit, next next.fit)]
10351 [%& target state.p.value(sub sub.fit, next next.fit)]
9518 ?: ?=(%call -.e) (infer-contextual-call e target env state)
10352 ?: ?=(%call -.e) (infer-contextual-call e target env state)
10353+ =/ named=(unit idiag) (branch-tag-name e env state)
10354+ ?^ named [%| u.named]
9519 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[target context])
10355 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[target context])
9520 ?^ empty-list u.empty-list
10356 ?^ empty-list u.empty-list
9521 ?: (single-structured-pattern e)
10357 ?: (single-structured-pattern e)
@@ -9658,7 +10494,7 @@
9658 ?~ pats [%& ~]
10494 ?~ pats [%& ~]
9659 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
10495 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
9660 =/ name=term name.i.pats
10496 =/ name=term name.i.pats
9661− ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
10497+ ?: |((reserved-name name) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
9662 [%| 'pattern shadows a name']
10498 [%| 'pattern shadows a name']
9663 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
10499 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
9664 ?: ?=(%| -.rest) rest
10500 ?: ?=(%| -.rest) rest
@@ -9735,24 +10571,12 @@
9735 ^- tape
10571 ^- tape
9736 =. t (itype-walk t sub)
10572 =. t (itype-walk t sub)
9738− %var
10574+ %var (show-var id.t)
9739− ?: (lth id.t 26) [(add 65 id.t) ~]
9741− %fvar
10575+ %fvar (show-var id.t)
9742− ?: (lth id.t 26) [(add 65 id.t) ~]
9744− %avar
10576+ %avar (show-var id.t)
9745− ?: (lth id.t 26) [(add 65 id.t) ~]
9747− %rvar
10577+ %rvar (show-var id.t)
9748− ?: (lth id.t 26) [(add 65 id.t) ~]
9750− %nvar
10578+ %nvar (show-var id.t)
9751− ?: (lth id.t 26) [(add 65 id.t) ~]
9753− %rnvar
10579+ %rnvar (show-var id.t)
9754− ?: (lth id.t 26) [(add 65 id.t) ~]
9756 %atom "@{(trip aura.t)}"
10580 %atom "@{(trip aura.t)}"
9757 %any-atom "@"
10581 %any-atom "@"
9758 %flag "?"
10582 %flag "?"
@@ -9773,6 +10597,17 @@
9773 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
10597 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
10600+:: +show-var: a type variable as printed: its name if it has one, else
10601+:: a letter for its number, A to Z, then T26, T27 and on
10606+ =/ name=@t (var-name id)
10607+ ?. =(0 name) (trip name)
10608+ ?: (lth id 26) [(add 65 id) ~]
9776++ show-itype-item
10611++ show-itype-item
9777 |= [t=itype sub=isub]
10612 |= [t=itype sub=isub]
9778 ^- tape
10613 ^- tape
@@ -9831,8 +10666,7 @@
9831 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
10666 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
9832 ?: (itype-has-hidden-recursive normalized) label
10667 ?: (itype-has-hidden-recursive normalized) label
9833 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
10668 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
9834− ?: (gth (lent vars) 26) label
9835− =/ printable=itype (canonical-itype normalized vars)
10669+ =/ printable=itype (canonical-itype (cap-names normalized vars ~ sub))
9836 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
10670 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
9838:: A capital in a written mold is generalized with its enclosing ++.
10672:: A capital in a written mold is generalized with its enclosing ++.
@@ -9873,6 +10707,116 @@
9873 ?: =(n u.ident) `i.caps
10707 ?: =(n u.ident) `i.caps
9874 $(caps t.caps)
10708 $(caps t.caps)
10710+:: +cap-names: give each variable in vars the name it was written with
10712+:: Unification joins variables, and the one an ID resolves to may not
10713+:: carry the name its definition wrote, as when a capital meets a
10714+:: called gate's variable or an atom variable. Each variable in vars
10715+:: takes the name of the first capital in caps that resolves to it;
10716+:: failing that, of the earliest made of the named variables that
10717+:: resolve to it, itself included (+joined-names). Only the name part
10718+:: of an ID changes, not its count, so IDs stay distinct.
10721+ |= [typ=itype vars=(list @ud) caps=icaps sub=isub]
10722+ ^- [typ=itype vars=(list @ud)]
10723+ =/ written=icaps (flop caps)
10724+ =/ joined=(map @ud @ud) (joined-names sub)
10725+ =/ ren=(map @ud @ud) ~
10726+ =/ out=(list @ud) ~
10728+ ?~ vars [?~(ren typ (itype-reid typ ren)) (flop out)]
10729+ =/ cap=(unit icap) (cap-with-id i.vars written sub)
10730+ =/ first=(unit @ud) (~(get by joined) i.vars)
10733+ ?~ first (var-name i.vars)
10734+ ?: =(0 (var-name i.vars)) (var-name u.first)
10735+ ?: (lth (var-count u.first) (var-count i.vars)) (var-name u.first)
10737+ =/ to=@ud (named-var name i.vars)
10738+ ?: =(to i.vars) $(vars t.vars, out [i.vars out])
10739+ $(vars t.vars, out [to out], ren (~(put by ren) i.vars to))
10741+:: +joined-names: for each variable that named ones resolve to, the
10742+:: earliest made of those, by count
10744+:: One pass over sub keeps each ID's newest binding, as +itype-lookup
10745+:: would find it: the variable it is bound to, or ~ for another type.
10746+:: Each named ID then follows those bindings to the variable it
10747+:: resolves to, if any.
10752+ =/ edges=(map @ud (unit @ud))
10753+ %+ roll (flop sub)
10754+ |= [b=ibinding m=(map @ud (unit @ud))]
10755+ (~(put by m) id.b (var-of val.b))
10756+ =/ named=(list @ud)
10757+ (murn ~(tap by edges) |=([k=@ud *] ?:(=(0 (var-name k)) ~ `k)))
10758+ =/ fuel=@ud ~(wyt by edges)
10759+ =/ out=(map @ud @ud) ~
10762+ =/ root=(unit @ud) (follow-var i.named edges fuel)
10763+ ?~ root $(named t.named)
10764+ ?: =(u.root i.named) $(named t.named)
10765+ =/ best=(unit @ud) (~(get by out) u.root)
10766+ ?: &(?=(^ best) (lth (var-count u.best) (var-count i.named)))
10768+ $(named t.named, out (~(put by out) u.root i.named))
10770+:: +follow-var: the variable that id resolves to through edges, or ~ if
10771+:: it resolves to another type; fuel bounds the steps
10774+ |= [id=@ud edges=(map @ud (unit @ud)) fuel=@ud]
10778+ =/ edge=(unit (unit @ud)) (~(get by edges) id)
10781+ ?: =(u.u.edge id) `id
10782+ $(id u.u.edge, fuel (dec fuel))
10784+:: +var-of: the ID of a type variable node, or ~ for another type
10798+:: +itype-reid: t with the variable IDs in ids replaced, each node
10799+:: keeping its kind
10802+ |= [t=itype ids=(map @ud @ud)]
10805+ %var t(id (fall (~(get by ids) id.t) id.t))
10806+ %fvar t(id (fall (~(get by ids) id.t) id.t))
10807+ %avar t(id (fall (~(get by ids) id.t) id.t))
10808+ %rvar t(id (fall (~(get by ids) id.t) id.t))
10809+ %nvar t(id (fall (~(get by ids) id.t) id.t))
10810+ %rnvar t(id (fall (~(get by ids) id.t) id.t))
10811+ ?(%atom %any-atom %flag %noun %empty %tag %const %recursive %jrec) t
10812+ %union t(cases (turn cases.t |=(c=itype ^$(t c))), args (turn args.t |=(c=itype ^$(t c))))
10813+ %grec t(args (turn args.t |=(c=itype ^$(t c))))
10814+ %collection t(args (turn args.t |=(c=itype ^$(t c))))
10815+ %face t(body $(t body.t))
10816+ %fn t(sample $(t sample.t), product $(t product.t))
10817+ %cell t(hed $(t hed.t), tal $(t tal.t))
9876++ merged-capitals
10820++ merged-capitals
9877 |= [caps=icaps sub=isub]
10821 |= [caps=icaps sub=isub]
9878 ^- (unit [first=icap second=icap])
10822 ^- (unit [first=icap second=icap])
@@ -9995,9 +10939,10 @@
9995 $(vars t.vars)
10939 $(vars t.vars)
9997:: Build the supported part of the value environment in dependency order.
10941:: Build the supported part of the value environment in dependency order.
9998−:: Each pass adds successful definitions. Forward references become
10942+:: Each pass adds successful definitions, visiting them dependencies first
9999−:: available on a later pass; unsupported syntax does not enter the
10943+:: (+dependency-order), so a forward reference usually resolves in the
10944+:: first pass; any that do not are retried on a later pass. Unsupported
10000−:: environment. Generalized definitions are closed, so a use instantiates
10945+:: syntax does not enter the environment. Generalized definitions are closed, so a use instantiates
10001:: its variables afresh.
10946:: its variables afresh.
10003++ global-value-names
10948++ global-value-names
@@ -10091,6 +11036,9 @@
10091 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
11036 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
10092 =. gate-defs.state ~
11037 =. gate-defs.state ~
10093 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
11038 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
11039+ :: A ++ whose body is (unface |= …) is a gate too, unfaced
11040+ =/ peeled=(unit expr) (unfaced-gate val.d env state)
11041+ =? val.d ?=(^ peeled) u.peeled
10094 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
11042 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
10095 [%| ["recursive definition is not a gate" ~]]
11043 [%| ["recursive definition is not a gate" ~]]
10096 =/ result=(unit itype) (recursive-branch-seed d env state)
11044 =/ result=(unit itype) (recursive-branch-seed d env state)
@@ -10114,6 +11062,7 @@
10114 =/ product=itype ?~(result [%var id] u.result)
11062 =/ product=itype ?~(result [%var id] u.result)
10115 =/ st=istate state.p.sam(next +(id))
11063 =/ st=istate state.p.sam(next +(id))
10116 =/ seed=itype [%fn typ.p.sam product]
11064 =/ seed=itype [%fn typ.p.sam product]
11065+ =? seed ?=(^ peeled) (itype-unface seed sub.st)
10117 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
11066 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
10118 =/ body=expr
11067 =/ body=expr
10119 ?- -.gate
11068 ?- -.gate
@@ -10125,7 +11074,9 @@
10125 ?: ?=(%| -.out) out
11074 ?: ?=(%| -.out) out
10126 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
11075 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
10127 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
11076 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
11077+ =/ typ=itype [%fn typ.p.sam typ.p.out]
11078+ =? typ ?=(^ peeled) (itype-unface typ u.uni)
10128− [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
11079+ [%& typ state.p.out(sub u.uni)]
10130++ dependency-root
11081++ dependency-root
10131 |= names=(list term)
11082 |= names=(list term)
@@ -10233,7 +11184,7 @@
10233:: Infer a cyclic component with one monomorphic seed per gate. All members
11184:: Infer a cyclic component with one monomorphic seed per gate. All members
10234:: must succeed before any scheme is available; pending constraints and
11185:: must succeed before any scheme is available; pending constraints and
10235:: unresolved branch joins remain partial.
11186:: unresolved branch joins remain partial.
10236−+$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
11187++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps unfaced=?]
10237+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
11188+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
10238++ seed-gate-group
11189++ seed-gate-group
10239 |= [ds=(list def) env=ienv state=istate]
11190 |= [ds=(list def) env=ienv state=istate]
@@ -10241,7 +11192,9 @@
10241 ?~ ds [%& [~ state]]
11192 ?~ ds [%& [~ state]]
10242 =/ d=def i.ds
11193 =/ d=def i.ds
10243 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
11194 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
11195+ :: A ++ whose body is (unface |= …) is a gate too, unfaced
11196+ =/ peeled=(unit expr) (unfaced-gate val.d env state)
10244− =/ gate=expr val.d
11197+ =/ gate=expr ?~(peeled val.d u.peeled)
10245 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
11198 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
10246 [%| ["recursive group contains a non-gate" ~]]
11199 [%| ["recursive group contains a non-gate" ~]]
10247 =/ initial=istate (reserve-def-caps gate state)
11200 =/ initial=istate (reserve-def-caps gate state)
@@ -10259,7 +11212,8 @@
10261 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
11214 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
11215+ =? seed ?=(^ peeled) (itype-unface seed sub.state.p.sam)
10262− =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
11216+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam ?=(^ peeled)]
10263 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
11217 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
10264 =/ rest=igate-seeds $(ds t.ds, state after)
11218 =/ rest=igate-seeds $(ds t.ds, state after)
10265 ?: ?=(%| -.rest) rest
11219 ?: ?=(%| -.rest) rest
@@ -10299,16 +11253,16 @@
10299 ?: (constrained-capitals caps.entry sub.state)
11253 ?: (constrained-capitals caps.entry sub.state)
10300 [%| ["explicit capital constraints are not supported by partial inference" ~]]
11254 [%| ["explicit capital constraints are not supported by partial inference" ~]]
10301 =/ typ=itype (itype-normalize typ.entry sub.state)
11255 =/ typ=itype (itype-normalize typ.entry sub.state)
11256+ =? typ unfaced.entry (itype-unface typ ~)
10302 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
11257 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
10303 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
11258 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
10304 [%| ["recursive group needs unsupported inference" ~]]
11259 [%| ["recursive group needs unsupported inference" ~]]
10305 =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
11260 =/ free=(list @ud) (weld (free-env-vars env sub.state) (free-cap-vars caps.outer sub.state))
10306 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
11261 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10307 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
11262 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
10308− ?: (gth (lent vars) 26) [%| ["recursive group needs too many type variables" ~]]
10309 =/ rest=(each ienv idiag) $(entries t.entries)
11263 =/ rest=(each ienv idiag) $(entries t.entries)
10310 ?: ?=(%| -.rest) rest
11264 ?: ?=(%| -.rest) rest
10311− [%& [[name.entry [typ vars]] p.rest]]
11265+ [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]
10313++ infer-gate-group
11267++ infer-gate-group
10314 |= [ds=(list def) env=ienv state=istate]
11268 |= [ds=(list def) env=ienv state=istate]
@@ -10484,14 +11438,13 @@
10484 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) ~
11438 ?: |((pending-tags tags.state.p.result sub.state.p.result) (itype-has-tag typ)) ~
10485 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) ~
11439 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result) ~
10486 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
11440 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
10487− ?: (gth (lent vars) 26) ~
10488 =/ finalized=(unit (list iwprojection))
11441 =/ finalized=(unit (list iwprojection))
10489 (width-finalize projections.state.p.result sub.state.p.result vars)
11442 (width-finalize projections.state.p.result sub.state.p.result vars)
10490 ?~ finalized ~
11443 ?~ finalized ~
10491 =? artifacts ?=(^ u.finalized)
11444 =? artifacts ?=(^ u.finalized)
10492 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
11445 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
10493 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
11446 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10494− `[[[name.d [typ vars]] env] checked artifacts]
11447+ `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]
10495++ add-supported-defs-core
11448++ add-supported-defs-core
10496 |= [ds=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) 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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
11449 |= [ds=(list def) checked=(map term def) heads=(unit igate-prelude-evidence) 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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
10497 ^- [env=ienv artifacts=(list iwidth-definition)]
11450 ^- [env=ienv artifacts=(list iwidth-definition)]
@@ -10550,15 +11503,38 @@
10550 =/ components=icomponents (graph-components ds names)
11503 =/ components=icomponents (graph-components ds names)
10551 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11504 =/ top=(list term) (turn molds |=(m=[name=term body=shape] name.m))
10552 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11505 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11506+ =/ ordered=(list def) (dependency-order ds components)
10554 =/ next=[env=ienv artifacts=(list iwidth-definition)]
11508 =/ next=[env=ienv artifacts=(list iwidth-definition)]
10555− (add-supported-defs-core ds (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
11509+ (add-supported-defs-core ordered (direct-checked-gates ds env) heads env molds globals externals surs mark-externals marks jimports reserved-molds at prelude artifacts index)
10556 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
11510 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
10557 =. grec-index.initial index
11511 =. grec-index.initial index
10558 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11512 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
10559 ?: =(env env.out) out
11513 ?: =(env env.out) out
10560 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11514 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11516+:: +dependency-order: the value definitions, dependencies first
11518+:: +graph-components lists the components dependencies first, so one
11519+:: pass of +add-supported-defs-core in this order resolves a forward
11520+:: chain that would otherwise take a pass per link; the fixpoint above
11521+:: stays as the fallback (review question 12). Members of a component
11522+:: keep their source order. Definitions in no component (molds, and
11523+:: every value when duplicate names leave no components) follow in
11526+++ dependency-order
11527+ |= [ds=(list def) components=icomponents]
11529+ =/ ranked=(list def)
11531+ %+ turn components
11532+ |= component=(list term)
11533+ (skim ds |=(d=def &(?=(%value -.d) (lien component |=(n=term =(n name.d))))))
11534+ =/ members=(list term) (zing components)
11535+ =/ named=ivisited (graph-nameset members ~)
11536+ (weld ranked (skip ds |=(d=def &(?=(%value -.d) (~(has by named) name.d)))))
10562++ resolve-supported-defs
11538++ resolve-supported-defs
10563 |= [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)]
11539 |= [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)]
10564 ^- ienv
11540 ^- ienv
@@ -11067,6 +12043,22 @@
11067 [at.first at.second (union-relate a (project-union-mold second molds ~))]
12043 [at.first at.second (union-relate a (project-union-mold second molds ~))]
11068 (weld pairs $(cases t.cases))
12044 (weld pairs $(cases t.cases))
12046+:: The partial report and the full module check share one overlap proof,
12047+:: so for the same union both name the same pair. The caller passes the
12048+:: projected .pairs, which the partial report reads again. The projection
12049+:: proves atoms, flags and nested literal cells, and its first overlap is
12050+:: named even when the source slice would prove an earlier pair. The
12051+:: source slice is tried only when some pair is unknown, for its one-hop
12052+:: generic applications. A missing witness does not mean the cases are
12054+++ mold-overlap-witness
12055+ |= [cases=(list shape) pairs=(list upair) molds=imolds]
12057+ =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
12058+ ?^ overlapping `i.overlapping
12059+ ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
12060+ (union-source-overlap cases molds 256)
11070:: A closed structural mold supplies no equation to determine a hole.
12062:: A closed structural mold supplies no equation to determine a hole.
11071:: Applications, references, unbound capitals and unions are unproved.
12063:: Applications, references, unbound capitals and unions are unproved.
11072++ simple-mold-hole
12064++ simple-mold-hole
@@ -11206,14 +12198,9 @@
11206 =? sh ?=(%generic -.sh) body.sh
12198 =? sh ?=(%generic -.sh) body.sh
11207 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
12199 ?. ?=(%union -.sh) (crip "+$ {(trip name.d)}: not checked")
11208 =/ pairs=(list upair) (union-pairs cases.sh molds)
12200 =/ pairs=(list upair) (union-pairs cases.sh molds)
11209− =/ overlapping=(list upair) (skim pairs |=(p=upair =(%overlap relation.p)))
11211− ?^ overlapping overlapping
11212− ?. (lien pairs |=(p=upair =(%unknown relation.p))) ~
11213− =/ witness=(unit upair) (union-source-overlap cases.sh molds 256)
12201+ =/ witness=(unit upair) (mold-overlap-witness cases.sh pairs molds)
11214− ?~(witness ~ ~[u.witness])
12202+ ?^ witness
11215− ?^ overlapping
12203+ =/ p=upair u.witness
11216− =/ p=upair i.overlapping
11217 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
12204 =/ summary=@t (crip "+$ {(trip name.d)}: overlapping cases; mold not checked")
11218 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
12205 =/ first=@t (show-error src [file line.beg.first.p col.beg.first.p "first union case"])
11219 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
12206 =/ second=@t (show-error src [file line.beg.second.p col.beg.second.p "overlapping case"])
@@ -11237,6 +12224,7 @@
11237 (of-wain:format [summary excerpts])
12224 (of-wain:format [summary excerpts])
11239:: Both written field sites are shown in the source that declares them.
12226:: Both written field sites are shown in the source that declares them.
12227+:: A store's derived-name clash shows its two sites the same way.
11240++ show-duplicate-fields
12228++ show-duplicate-fields
11241 |= [file=path src=@t diagnostic=idiag]
12229 |= [file=path src=@t diagnostic=idiag]
@@ -11394,13 +12382,29 @@
11394 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
12382 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
11395 ?^ first first
12383 ?^ first first
11396 $(segs t.segs)
12384 $(segs t.segs)
12385+:: A change's items each set a field once: two that name the same field,
12386+:: or one a field inside the other's, as cart and open.cart, overlap.
11397++ duplicate-edits
12387++ duplicate-edits
11398 |= edits=(list edit)
12388 |= edits=(list edit)
11399 ^- (unit idiag)
12389 ^- (unit idiag)
12390+ =| seen=(list edit)
12391+ |- ^- (unit idiag)
11400 ?~ edits ~
12392 ?~ edits ~
12394+ =/ prior=(list edit)
12395+ (skim seen |=(p=edit (wing-overlap (flop names.p) (flop names.e))))
12397+ =/ same=? =(names.i.prior names.e)
12398+ =/ sites=(list [at=span note=tape])
12399+ :~ [at.i.prior "first field"]
12400+ [at.e ?:(same "repeated field" "overlapping field")]
12402+ ?: same `["change field `{(show-names names.e)}` is repeated" sites]
12403+ =/ a=tape (show-names names.i.prior)
12404+ `["change fields `{a}` and `{(show-names names.e)}` overlap" sites]
11401− =/ first (duplicate-expr val.i.edits)
12405+ =/ first (duplicate-expr val.e)
11402 ?^ first first
12406 ?^ first first
11403− $(edits t.edits)
12407+ $(edits t.edits, seen [e seen])
11404++ duplicate-arms
12408++ duplicate-arms
11405 |= arms=(list arm)
12409 |= arms=(list arm)
11406 ^- (unit idiag)
12410 ^- (unit idiag)
@@ -11473,59 +12477,68 @@
11474 [n $(imports t.imports)]
12478 [n $(imports t.imports)]
12480+:: +reserved-name: whether n names a reserved operation
12482+:: proj and unface are handled by the checker by type, not bound, so
12483+:: no module may define, import or bind either name, as a value or
12484+:: as a mold. A field, tag or path segment may still be spelled so.
11476−++ reserved-proj-sample
12485+++ reserved-name
12488+ |(=(n %proj) =(n %unface))
11477 |= sam=sample
12490 |= sam=sample
11479 ?- -.sam
12492 ?- -.sam
11480− %bind =(name.sam %proj)
12493+ %bind (reserved-name name.sam)
11481− %face =(name.sam %proj)
12494+ %face (reserved-name name.sam)
11482− %pun =(name.sam %proj)
12495+ %pun (reserved-name name.sam)
11483− %cell (lien items.sam reserved-proj-sample)
12496+ %cell (lien items.sam reserved-sample)
11486−++ reserved-proj-pattern
12499+++ reserved-pattern
11487 |= p=pattern
12500 |= p=pattern
11490− %bind =(name.p %proj)
12503+ %bind (reserved-name name.p)
11491− %cell (lien items.p reserved-proj-pattern)
12504+ %cell (lien items.p reserved-pattern)
11494−++ reserved-proj-def
12507+++ reserved-def
11495 |= d=def
12508 |= d=def
11497− ?: =(name.d %proj) &
12510+ ?: (reserved-name name.d) &
11498− ?: ?=(%value -.d) (reserved-proj-expr val.d)
12511+ ?: ?=(%value -.d) (reserved-expr val.d)
11500−++ reserved-proj-expr
12513+++ reserved-expr
11501 |= e=expr
12514 |= e=expr
11504− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12517+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-expr p.p) |)))
11505− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12518+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-expr p.p) |)))
11506− %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
12519+ %change (lien edits.e |=(p=edit (reserved-expr val.p)))
11507 %pair $(e val.e)
12520 %pair $(e val.e)
11508 %unit $(e val.e)
12521 %unit $(e val.e)
11509 %group $(e inner.e)
12522 %group $(e inner.e)
11510− %list (lien items.e reserved-proj-expr)
12523+ %list (lien items.e reserved-expr)
11511− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
12524+ %tuple (lien items.e |=(i=item (reserved-expr val.i)))
11512− ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
12525+ ?(%gate %gate-wide) |((reserved-sample sample.e) $(e body.e))
11513 %cast $(e val.e)
12526 %cast $(e val.e)
11514− %call |($(e head.e) (lien args.e reserved-proj-expr))
12527+ %call |($(e head.e) (lien args.e reserved-expr))
11515 %trace |($(e val.e) $(e then.e))
12528 %trace |($(e val.e) $(e then.e))
11516− %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
12529+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-pattern pat.a) (reserved-expr val.a)))))
11517− %body |((lien defs.e reserved-proj-def) $(e final.e))
12530+ %body |((lien defs.e reserved-def) $(e final.e))
11521−++ module-has-reserved-proj
12534+++ module-has-reserved
11522 |= mod=module
12535 |= mod=module
11524 =/ imported=(list term) (import-binding-names imports.mod)
12537 =/ imported=(list term) (import-binding-names imports.mod)
11525 =/ vals=(list term) (global-value-names defs.mod)
12538 =/ vals=(list term) (global-value-names defs.mod)
11526 =/ molds=imolds (collect-simple-molds defs.mod)
12539 =/ molds=imolds (collect-simple-molds defs.mod)
11527 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12540 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11528− |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
12541+ |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))
11530++ module-scope-valid
12543++ module-scope-valid
11531 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12544 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -11534,7 +12547,7 @@
11534 =/ vals=(list term) (global-value-names defs.mod)
12547 =/ vals=(list term) (global-value-names defs.mod)
11535 =/ molds=imolds (collect-simple-molds defs.mod)
12548 =/ molds=imolds (collect-simple-molds defs.mod)
11536 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12549 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11537− ?: (module-has-reserved-proj mod) |
12550+ ?: (module-has-reserved mod) |
11538 ?. %+ levy imported
12551 ?. %+ levy imported
11539 |= n=term
12552 |= n=term
11540 &((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))))
12553 &((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))))
@@ -11564,7 +12577,8 @@
11564 ?. valid ~
12577 ?. valid ~
11565 =? sh ?=(%generic -.sh) body.sh
12578 =? sh ?=(%generic -.sh) body.sh
11566 ?. ?=(%union -.sh) ~
12579 ?. ?=(%union -.sh) ~
12580+ :: A failed inference keeps no projection, so it is computed once more.
11567− (union-source-overlap cases.sh molds 256)
12581+ (mold-overlap-witness cases.sh (union-pairs cases.sh molds) molds)
11568++ module-mold-types-detail
12582++ module-mold-types-detail
11569 |= [molds=imolds state=istate]
12583 |= [molds=imolds state=istate]
11570 ^- (each imold-types imold-failure)
12584 ^- (each imold-types imold-failure)
@@ -11888,6 +12902,74 @@
11888 ?~ (ienv-lookup name.i.ds env) |
12902 ?~ (ienv-lookup name.i.ds env) |
11889 $(ds t.ds)
12903 $(ds t.ds)
12905+:: Names the value a failed full check stops at, for its message only. A
12906+:: value whose module dependencies all resolved failed on its own, so the
12907+:: first such missing value is named. Otherwise every missing value waits
12908+:: on another, so following the first one each waits on, from the first
12909+:: missing value, reaches a value twice, which is named. The walk is over
12910+:: the syntactic dependency graph: dependency-expr ignores binders, so a
12911+:: sample or other local binder with a top-level value's name reads as a
12912+:: dependency on it. The named value is on a cycle of that graph, but may
12913+:: only call into the value that failed, as when a binder in that value
12914+:: shadows the named one. It claims no error in the named value.
12915+++ module-missing-value
12916+ |= [ds=(list def) env=ienv]
12918+ =/ missing=(list term)
12921+ ?. ?=(%value -.d) ~
12922+ ?^ (ienv-lookup name.d env) ~
12925+ =/ pending=ivisited (graph-nameset missing ~)
12926+ =/ roots=(list term)
12929+ ?. ?=(%value -.d) ~
12930+ ?~ (~(get by pending) name.d) ~
12931+ =/ deps=(list term) (dependency-expr val.d)
12932+ ?. (levy deps |=(n=term |(=(n name.d) ?=(~ (~(get by pending) n))))) ~
12935+ =/ seen=ivisited ~
12936+ =/ here=term i.missing
12938+ ?^ (~(get by seen) here) `here
12939+ =/ next=(list term)
12943+ ?. ?=(%value -.d) ~
12944+ ?. =(here name.d) ~
12945+ (skim (dependency-expr val.d) |=(n=term &(!=(n here) ?=(^ (~(get by pending) n)))))
12947+ $(seen (~(put by seen) here &), here i.next)
12949+:: Finds the first missing value that is a gate whose own sample has the
12950+:: name of a value in scope. Partial inference rejects that sample ("sample
12951+:: shadows a name"), and it is an error (grammar, Modules). Mark names name
12952+:: molds and are left out, as are cell samples and binders deeper in the
12954+++ module-sample-shadow
12955+ |= [ds=(list def) env=ienv values=(list term)]
12956+ ^- (unit [name=term at=span])
12958+ ?. ?=(%value -.i.ds) $(ds t.ds)
12959+ ?^ (ienv-lookup name.i.ds env) $(ds t.ds)
12960+ =/ e=expr val.i.ds
12961+ ?. ?=(?(%gate %gate-wide) -.e) $(ds t.ds)
12962+ =/ s=sample sample.e
12963+ =/ name=(unit term)
12969+ ?~ name $(ds t.ds)
12970+ ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
11891:: Cache only completed interfaces for this invocation. The source bundle,
12973:: Cache only completed interfaces for this invocation. The source bundle,
11892:: imported Hoon types and prelude are fixed for the whole graph. Check the
12974:: imported Hoon types and prelude are fixed for the whole graph. Check the
11893:: active path and duplicate sources before consulting it, so a cache hit
12975:: active path and duplicate sources before consulting it, so a cache hit
@@ -12154,10 +13236,49 @@
12155 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
13237 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
12156 =/ derived=(list term) (weld path-names poke-names)
13238 =/ derived=(list term) (weld path-names poke-names)
12157− ?: (lien derived |=(n=term =(n %proj))) |
13239+ ?: (lien derived reserved-name) |
12158 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
13240 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
12159 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
13241 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
13243+:: The definite error behind some failures of the check above. An API
13244+:: exports `poke` when it declares `+$ poke`, and a request per case of a
13245+:: `+$ paths` that reads as path cases; these names surely exist, so a clash
13246+:: among them or with the module's scope is an error (grammar, Modules). A
13247+:: reserved `proj` stays unsupported, as in the check above.
13248+++ api-derived-clash
13249+ |= [mod=module prelude-values=(list term)]
13251+ =/ declared=(list term) (collect-mark-imports imports.mod)
13252+ =/ declarations=(list def)
13253+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%paths name.d))))
13254+ =/ cases=(list [name=term at=span note=tape])
13255+ ?. ?=([* ~] declarations) ~
13256+ =/ decl=def i.declarations
13257+ ?> ?=(%mold -.decl)
13258+ =/ paths=(unit (list iapi-path)) (api-path-declaration shape.decl declared)
13260+ (turn u.paths |=(p=iapi-path [name.p at.p "`{(trip name.p)}` is derived from this path case"]))
13261+ =/ pokes=(list def)
13262+ (skim defs.mod |=(d=def &(?=(%mold -.d) =(%poke name.d))))
13263+ =/ derived=(list [name=term at=span note=tape])
13264+ ?. ?=([* ~] pokes) cases
13265+ (snoc cases [%poke at.i.pokes "`poke` is derived from this mold"])
13266+ =/ names=(list term) (turn derived |=(x=[name=term at=span note=tape] name.x))
13267+ =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
13268+ =/ clashes=(list term)
13271+ ?| (reserved-name n)
13272+ &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
13275+ =/ sites=(list [at=span note=tape])
13277+ |= x=[name=term at=span note=tape]
13278+ ?. =(i.clashes name.x) ~
13280+ `(derived-name-clash "API" i.clashes sites mod)
12161:: Analysis only. Successful external entries must be unchanged results
13282:: Analysis only. Successful external entries must be unchanged results
12162:: produced for the declared marks; no request interface is produced.
13283:: produced for the declared marks; no request interface is produced.
12163+$ iapi-mark-type [name=term typ=itype]
13284+$ iapi-mark-type [name=term typ=itype]
@@ -12236,6 +13357,9 @@
12236 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
13357 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12237 ?~ prepared [%| 'API path analysis needs the prepared prelude']
13358 ?~ prepared [%| 'API path analysis needs the prepared prelude']
12238 =/ public=ifile iface.u.prepared
13359 =/ public=ifile iface.u.prepared
13360+ :: The analysis below would call a derived-name clash unsupported.
13361+ =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
13362+ ?^ clash [%| (show-duplicate-fields file src u.clash)]
12239 =/ prelude=(unit ifile) `iface.u.prepared
13363 =/ prelude=(unit ifile) `iface.u.prepared
12240 =/ deps=jimports-result
13364 =/ deps=jimports-result
12241 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
13365 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ prelude)
@@ -12261,6 +13385,9 @@
12261 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
13385 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12262 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
13386 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12263 ?~ prepared [%| 'API path evidence needs the prepared prelude']
13387 ?~ prepared [%| 'API path evidence needs the prepared prelude']
13388+ :: The analysis below would call a derived-name clash unsupported.
13389+ =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
13390+ ?^ clash [%| (show-duplicate-fields file src u.clash)]
12264 =/ public=ifile iface.u.prepared
13391 =/ public=ifile iface.u.prepared
12265 =/ deps=jimports-result
13392 =/ deps=jimports-result
12266 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
13393 (resolve-jibb-imports imports.p.parsed externals marks modules ~[file] values.u.prepared molds.u.prepared ~ `public)
@@ -12282,6 +13409,9 @@
12282 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
13409 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
12283 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
13410 ?^ duplicate [%| (show-duplicate-fields file src u.duplicate)]
12284 ?~ prepared [%| 'API path evidence needs the prepared prelude']
13411 ?~ prepared [%| 'API path evidence needs the prepared prelude']
13412+ :: The analysis below would call a derived-name clash unsupported.
13413+ =/ clash=(unit idiag) (api-derived-clash p.parsed values.u.prepared)
13414+ ?^ clash [%| (show-duplicate-fields file src u.clash)]
12285 =/ public=ifile iface.u.prepared
13415 =/ public=ifile iface.u.prepared
12286 =/ deps=jimports-result
13416 =/ deps=jimports-result
12287 (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
13417 (resolve-jibb-imports imports.p.parsed externals marks modules active values.u.prepared molds.u.prepared cache `public)
@@ -12621,38 +13751,54 @@
12621++ api-poke-interface
13751++ api-poke-interface
12622 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
13752 |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
12623 ^- (unit ifile)
13753 ^- (unit ifile)
13754+ =/ out=(each ifile @t)
13755+ (api-poke-interface-result at mod mark-externals prelude-values prelude-molds prelude)
13756+ ?:(?=(%& -.out) `p.out ~)
13758+:: The same check, naming the part that stopped it. Each reason says which
13759+:: part is outside this fragment and claims no error in the module, except
13760+:: duplicate definitions, an error the full check reports first, as for
13762+++ api-poke-interface-result
13763+ |= [at=path mod=module mark-externals=imark-externals prelude-values=(list term) prelude-molds=(list term) prelude=(unit ifile)]
13764+ ^- (each ifile @t)
12624− ?: (lien defs.mod def-has-hole) ~
13765+ ?: (lien defs.mod def-has-hole) [%| 'API holes need unsupported inference']
12625− ?. ?=([%ui %api @ %jibb ~] at) ~
13766+ ?. ?=([%ui %api @ %jibb ~] at) [%| 'API path evidence requires /ui/api/<agent>.jibb']
12626− ?^ (duplicate-defs defs.mod) ~
13767+ ?^ (duplicate-defs defs.mod) [%| 'API has duplicate definitions']
12627− ?~ prelude ~
13768+ ?~ prelude [%| 'API poke prelude needs unsupported inference']
12628− ?. =(at.u.prelude /lib/jibb/prelude/jibb) ~
13769+ ?. =(at.u.prelude /lib/jibb/prelude/jibb) [%| 'API poke prelude needs unsupported inference']
12629 =/ poke=(unit ischeme) (find-jibb-mold %raw-poke u.prelude)
13770 =/ poke=(unit ischeme) (find-jibb-mold %raw-poke u.prelude)
12630− ?~ poke ~
13771+ ?~ poke [%| 'API poke prelude needs unsupported inference']
12631− ?. ?=(%union -.typ.u.poke) ~
13772+ ?. ?=(%union -.typ.u.poke) [%| 'API poke prelude needs unsupported inference']
12632− ?^ vars.u.poke ~
13773+ ?^ vars.u.poke [%| 'API poke prelude needs unsupported inference']
12633 =/ compatible=?
13774 =/ compatible=?
12634 %+ lien cases.typ.u.poke
13775 %+ lien cases.typ.u.poke
12635 |= c=itype
13776 |= c=itype
12636 ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
13777 ?=([%cell [%const [%term %tas %agent *]] [%cell [%face %agent [%atom %tas]] [%cell [%face %mark [%atom %tas]] [%face %payload [%noun ~]]]]] c)
12637− ?. compatible ~
13778+ ?. compatible [%| 'API poke prelude needs unsupported inference']
12638− ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) ~
13779+ :: Definitions come before imports so that a module with more than a
12639− ?. (levy imports.mod |=(i=import ?=(%mark -.i))) ~
13780+ :: `+$ poke` is not described by its imports.
12640− =/ marks=(list term) (collect-mark-imports imports.mod)
12641− ?. ?=([@ ~] marks) ~
12642 =/ ds=(list def) defs.mod
13781 =/ ds=(list def) defs.mod
12643− ?. ?=([[%mold *] ~] ds) ~
13782+ ?. ?=([[%mold *] ~] ds) [%| 'poke-only API definitions need unsupported inference']
12644− ?. =(%poke name.i.ds) ~
13783+ ?. =(%poke name.i.ds) [%| 'poke-only API definitions need unsupported inference']
13784+ ?. (module-scope-valid mod(defs ~) prelude-values prelude-molds) [%| 'API import scope needs unsupported inference']
13785+ ?. (levy imports.mod |=(i=import ?=(%mark -.i))) [%| 'poke-only API imports need unsupported inference']
13786+ =/ marks=(list term) (collect-mark-imports imports.mod)
13787+ ?. ?=([@ ~] marks) [%| 'poke-only API mark imports need unsupported inference']
12645 =/ sh=shape shape.i.ds
13788 =/ sh=shape shape.i.ds
12646− ?. ?=([%ref *] sh) ~
13789+ ?. ?=([%ref *] sh) [%| 'API poke mold needs unsupported inference']
12647− ?. ?=([@ ~] names.sh) ~
13790+ ?. ?=([@ ~] names.sh) [%| 'API poke mold needs unsupported inference']
12648 =/ n=term i.names.sh
13791 =/ n=term i.names.sh
12649− ?. (unique-value-name n marks) ~
13792+ ?. (unique-value-name n marks) [%| 'API poke mold needs unsupported inference']
12650− ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) ~
13793+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x)))) [%| 'API poke mold needs unsupported inference']
13794+ =/ results=@ud (lent (skim mark-externals |=(e=[mark=term result=*] =(n mark.e))))
13795+ ?: =(0 results) [%| (crip "API poke mark %{(trip n)} has no reader result")]
13796+ ?. =(1 results) [%| (crip "API poke mark %{(trip n)} has duplicate reader results")]
12651 =/ mark=(unit itype) (find-imported-mark-prelude n mark-externals marks u.prelude)
13797 =/ mark=(unit itype) (find-imported-mark-prelude n mark-externals marks u.prelude)
12652− ?~ mark ~
13798+ ?~ mark [%| 'API poke mark reader result needs unsupported inference']
12653 =/ sc=(unit ischeme) (derived-poke-command-scheme u.prelude u.mark)
13799 =/ sc=(unit ischeme) (derived-poke-command-scheme u.prelude u.mark)
12654− ?~ sc ~
13800+ ?~ sc [%| 'API poke command needs unsupported inference']
12655− `[~[[%poke u.sc]] (api-mark-exports marks marks mark-externals u.prelude) at ~[[n i.t.t.at n]] ~ ~ ~ ~]
13801+ [%& [~[[%poke u.sc]] (api-mark-exports marks marks mark-externals u.prelude) at ~[[n i.t.t.at n]] ~ ~ ~ ~]]
12657:: Source-proven ordinary helpers validate each selected /sur dependency.
13803:: Source-proven ordinary helpers validate each selected /sur dependency.
12658:: Unused or less direct cores remain unsupported by this first interface.
13804:: Unused or less direct cores remain unsupported by this first interface.
@@ -12877,30 +14023,73 @@
12877 `[u.init u.update]
14023 `[u.init u.update]
12879+$ istore-declaration [action=term defs=(list def)]
14025+$ istore-declaration [action=term defs=(list def)]
14026+:: A failure carries a diagnostic only when it is a definite error of the
14027+:: source; every other failure is unsupported and carries none.
12880++ store-declaration
14028++ store-declaration
12881 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
14029 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12882− ^- (unit istore-declaration)
14030+ ^- (each istore-declaration (unit idiag))
12883 =/ ds=(list def) defs.mod
14031 =/ ds=(list def) defs.mod
12884 =/ pokes=(list def)
14032 =/ pokes=(list def)
12885 (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
14033 (skim ds |=(d=def &(?=(%mold -.d) =(%poke name.d))))
12886− ?. ?=([* ~] pokes) ~
14034+ ?. ?=([* ~] pokes) [%| ~]
12887 =/ states=(list def)
14035 =/ states=(list def)
12888 (skim ds |=(d=def &(?=(%mold -.d) =(%state name.d))))
14036 (skim ds |=(d=def &(?=(%mold -.d) =(%state name.d))))
12889− ?. ?=([* ~] states) ~
14037+ ?. ?=([* ~] states) [%| ~]
12890 =/ poke=def i.pokes
14038 =/ poke=def i.pokes
12891 =/ state=def i.states
14039 =/ state=def i.states
12892 ?> &(?=(%mold -.poke) ?=(%mold -.state))
14040 ?> &(?=(%mold -.poke) ?=(%mold -.state))
12893− ?: ?=(%generic -.shape.state) ~
14041+ ?: ?=(%generic -.shape.state) [%| ~]
12894− ?: ?=(%generic -.shape.poke) ~
14042+ ?: ?=(%generic -.shape.poke) [%| ~]
12895 =/ action=term %poke
14043 =/ action=term %poke
12896 =/ ordinary=(list def) ds
14044 =/ ordinary=(list def) ds
12897− ?. (module-scope-valid mod prelude-values prelude-molds) ~
12898 =/ derived=(list term) ~[%state action]
14045 =/ derived=(list term) ~[%state action]
12899− ?: (lien derived |=(n=term =(n %proj))) ~
14046+ ?: (lien derived reserved-name) [%| ~]
12900 =/ outer=(list term)
14047 =/ outer=(list term)
12901 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
14048 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
14049+ =/ clashes=(list term)
12902− ?. (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x)))))) ~
14050+ (skip derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
14051+ :: main's `store` is the prelude's builder when the prelude declares it and
14052+ :: nothing local takes the name. Only then do the derived names surely
14053+ :: exist, and then a clash is an error even where the scope also fails, as
14054+ :: for an import face that clashes with both a derived name and its mold.
14056+ ?& (lien prelude-values |=(x=term =(x %store)))
14057+ !(lien (global-value-names ds) |=(x=term =(x %store)))
14058+ !(lien (import-binding-names imports.mod) |=(x=term =(x %store)))
14060+ ?: &(?=(^ clashes) builder (lien outer |=(x=term =(x i.clashes))))
14061+ =/ from=span ?:(=(%state i.clashes) at.state at.poke)
14062+ =/ derived=[at=span note=tape] [from "`{(trip i.clashes)}` is derived from this mold"]
14063+ [%| `(derived-name-clash "store" i.clashes ~[derived] mod)]
14064+ ?. (module-scope-valid mod prelude-values prelude-molds) [%| ~]
12903− `[action ordinary]
14066+ [%& [action ordinary]]
14068+:: A store or API exports names derived from its declarations, and a
14069+:: clashing derived name is an error (grammar, Modules). Show where the name
14070+:: is derived and the definition, import face or other derived name it
14071+:: clashes with; a prelude name has no site in the module.
14072+++ derived-name-clash
14073+ |= [kind=tape n=term derived=(list [at=span note=tape]) mod=module]
14075+ =/ values=(list span)
14076+ (murn defs.mod |=(d=def ?.(&(?=(%value -.d) =(n name.d)) ~ `at.d)))
14077+ =/ faces=(list span)
14078+ %+ murn imports.mod
14082+ %sur ?.(=(n name.i) ~ `at.i)
14083+ %jibb ?.(=(n face.i) ~ `at.i)
14085+ =/ head=tape "{kind} derived name `{(trip n)}` clashes with"
14087+ ["{head} a definition" (weld derived ~[[i.values "clashing definition"]])]
14089+ ["{head} an import face" (weld derived ~[[i.faces "clashing import face"]])]
14090+ ?: ?=([* * *] derived)
14091+ ["{head} another derived name" derived]
14092+ ["{head} a prelude name" derived]
12905++ program-empty-null
14094++ program-empty-null
12906 |= e=expr
14095 |= e=expr
@@ -12932,21 +14121,6 @@
12932 %body ?~(defs.e $(e final.e) e)
14121 %body ?~(defs.e $(e final.e) e)
12935−++ program-init-tuple-null
12938− ?. ?=(%value -.d) |
12939− ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) |
12943− %gate-wide body.val.d
12946− =. body (program-transparent body)
12947− ?. ?=(%tuple -.body) |
12949− (program-empty-null val:(rear items.body))
12951:: Recover only the update of an already recognized direct program main.
14125:: Recover only the update of an already recognized direct program main.
12952:: Its written sample determines the message/model relationship; the canonical
14126:: Its written sample determines the message/model relationship; the canonical
@@ -12986,10 +14160,10 @@
12986 (~(put by (direct-checked-gates ds env)) update.parts update-def)
14160 (~(put by (direct-checked-gates ds env)) update.parts update-def)
12987 =/ templates=ienv
14161 =/ templates=ienv
12988 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14162 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
12989− =/ scanned=(unit dgscan)
14163+ =/ fresh=(unit @ud)
12990− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14164+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
12991− ?~ scanned ~
14165+ ?~ fresh ~
12992− =. next.initial (dg-next-id ids.u.scanned 0)
14166+ =. next.initial u.fresh
12993 =/ update-state=istate (reserve-def-caps val.update-def initial)
14167 =/ update-state=istate (reserve-def-caps val.update-def initial)
12994 =/ sam=isample-result (infer-sample u.written-update env update-state)
14168 =/ sam=isample-result (infer-sample u.written-update env update-state)
12995 ?: ?=(%| -.sam) ~
14169 ?: ?=(%| -.sam) ~
@@ -13148,10 +14322,10 @@
13148 =/ checked=(map term def) (direct-checked-gates ds env)
14322 =/ checked=(map term def) (direct-checked-gates ds env)
13149 =/ templates=ienv
14323 =/ templates=ienv
13150 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14324 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13151− =/ scanned=(unit dgscan)
14325+ =/ fresh=(unit @ud)
13152− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14326+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
13153− ?~ scanned ~
14327+ ?~ fresh ~
13154− =. next.initial (dg-next-id ids.u.scanned 0)
14328+ =. next.initial u.fresh
13155 =/ subs-state=istate (reserve-def-caps val.subs-def initial)
14329 =/ subs-state=istate (reserve-def-caps val.subs-def initial)
13156 =/ sam=isample-result (infer-sample u.written-subs env subs-state)
14330 =/ sam=isample-result (infer-sample u.written-subs env subs-state)
13157 ?: ?=(%| -.sam) ~
14331 ?: ?=(%| -.sam) ~
@@ -13499,10 +14673,10 @@
13499 =/ checked=(map term def) (direct-checked-gates ds env)
14673 =/ checked=(map term def) (direct-checked-gates ds env)
13500 =/ templates=ienv
14674 =/ templates=ienv
13501 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14675 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13502− =/ scanned=(unit dgscan)
14676+ =/ fresh=(unit @ud)
13503− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14677+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
13504− ?~ scanned ~
14678+ ?~ fresh ~
13505− =. next.initial (dg-next-id ids.u.scanned 0)
14679+ =. next.initial u.fresh
13506 =/ view-state=istate (reserve-def-caps val.view-def initial)
14680 =/ view-state=istate (reserve-def-caps val.view-def initial)
13507 =/ sam=isample-result (infer-sample u.written-view env view-state)
14681 =/ sam=isample-result (infer-sample u.written-view env view-state)
13508 ?: ?=(%| -.sam) ~
14682 ?: ?=(%| -.sam) ~
@@ -13613,10 +14787,10 @@
13613 =/ checked=(map term def) (direct-checked-gates ds env)
14787 =/ checked=(map term def) (direct-checked-gates ds env)
13614 =/ templates=ienv
14788 =/ templates=ienv
13615 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
14789 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13616− =/ scanned=(unit dgscan)
14790+ =/ fresh=(unit @ud)
13617− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
14791+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
13618− ?~ scanned ~
14792+ ?~ fresh ~
13619− =. next.initial (dg-next-id ids.u.scanned 0)
14793+ =. next.initial u.fresh
13620 =/ view-state=istate (reserve-def-caps val.view-def initial)
14794 =/ view-state=istate (reserve-def-caps val.view-def initial)
13621 =/ sam=isample-result (infer-sample u.written-view env view-state)
14795 =/ sam=isample-result (infer-sample u.written-view env view-state)
13622 ?: ?=(%| -.sam) ~
14796 ?: ?=(%| -.sam) ~
@@ -13763,21 +14937,89 @@
13763 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14937 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13764 `[env.u.added grouped.resolution artifacts.u.added]
14938 `[env.u.added grouped.resolution artifacts.u.added]
13766−++ program-init-null-sample
14940+:: The model a direct program's initializer must produce. Update's written
13767− |= d=def
14941+:: two-item sample gives it when it can be read. Otherwise main's own program
13768− ^- ?
14942+:: fit does: update, view and subs are fitted together against the prelude
13769− =/ written=(unit sample) (direct-gate-sample d)
14943+:: program's sample, as main's call will fit them, with the initializer an
13770− ?~ written |
14944+:: open variable. Only the initializer's data may stay open, a replay of the
13771− ?. ?=(%bare -.u.written) |
14945+:: fit must not move, and the model must come out closed and tag-free.
13772− =/ sh=shape shape.u.written
14946+++ program-init-model
13773− ?. ?=(%const -.sh) |
14947+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) env=ienv program=ischeme program-def=def initial=istate]
13774− =(%null form.lit.sh)
14948+ ^- (unit itype)
13775−::
14949+ =/ relation=(unit [message=itype model=itype])
13776−:: The tuple-ending-null initializer retry above intentionally keeps its own
14950+ (program-update-relation update.parts ds env)
13777−:: boundary. A direct null-sample initializer can instead receive the closed
14951+ ?^ relation `model.u.relation
13778−:: model already established by update, view and subscriptions.
14952+ =/ args=(unit (list expr)) (program-main-args main)
14954+ =/ written=(unit sample) (direct-gate-sample program-def)
14956+ ?. ?=(%cell -.u.written) ~
14957+ ?~ items.u.written ~
14958+ =/ update=(unit ischeme) (ienv-lookup update.parts env)
14959+ =/ view=(unit ischeme) (ienv-lookup view.parts env)
14960+ =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
14964+ =/ instance=[typ=itype state=istate] (instantiate-scheme program initial)
14965+ ?. ?=(%fn -.typ.instance) ~
14966+ ?. ?=(%cell -.sample.typ.instance) ~
14967+ =/ expected-init=(unit itype)
14968+ (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written))
14969+ ?~ expected-init ~
14970+ ?. ?=(%fn -.u.expected-init) ~
14971+ ?. ?=(%var -.sample.u.expected-init) ~
14972+ =/ data=@ud id.sample.u.expected-init
14973+ =/ init-var=itype [%var next.state.instance]
14974+ =/ up=[typ=itype state=istate]
14975+ (instantiate-scheme u.update state.instance(next +(next.state.instance)))
14976+ =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
14977+ =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
14978+ =/ st=istate state.sb
14979+ =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
14981+ (direct-positional-fit u.args items.u.written actual sample.typ.instance env st sub.st next.st)
14982+ ?. ?=(%ok -.fit) ~
14983+ =/ actual-final=itype (itype-normalize actual sub.fit)
14984+ =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
14985+ =/ open=(list @ud)
14986+ (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
14987+ ?. (levy open |=(n=@ud =(data n))) ~
14988+ ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
14990+ (direct-positional-fit u.args items.u.written actual sample.typ.instance env st sub.fit next.fit)
14991+ ?. ?=(%ok -.replay) ~
14992+ ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
14993+ =/ expected=itype (itype-normalize u.expected-init sub.fit)
14994+ ?. ?=(%fn -.expected) ~
14995+ ?^ (itype-vars product.expected) ~
14998+:: The product of an initializer inferred ordinarily, as a whole gate with no
14999+:: expected type, for a body that context inference cannot take, such as a
15000+:: branch over a nested call's union. Its sample must fit the written one.
15001+++ program-init-ordinary
15002+ |= [init-def=def env=ienv sample=itype state=istate]
15004+ ?> ?=(%value -.init-def)
15005+ =/ gate=iresult (infer-fragment val.init-def env state)
15006+ =? gate ?=(%| -.gate) (infer-recursive-gate init-def env state)
15007+ ?: ?=(%| -.gate) gate
15008+ ?. ?=(%fn -.typ.p.gate) [%| ["initializer is not a gate" ~]]
15010+ (itype-fit sample.typ.p.gate sample sub.state.p.gate next.state.p.gate)
15011+ ?. ?=(%ok -.fit) [%| ["initializer sample differs" ~]]
15012+ [%& product.typ.p.gate state.p.gate(sub sub.fit, next next.fit)]
15014+:: Recover a direct program's initializer once update, view and
15015+:: subscriptions are resolved: its body is inferred against their closed
15016+:: model (+program-init-model), under its own closed written sample. This one
15017+:: path replaced a separate retry for bodies ending in null and a gate that
15018+:: took only a null sample, so any body and any closed sample check the same
15019+:: way (review question 8). The fresh ordinary main inference afterwards
15020+:: checks that all four components agree.
13779++ program-plain-init-context
15021++ program-plain-init-context
13780− |= [parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
15022+ |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13781 ^- (unit iresolved)
15023 ^- (unit iresolved)
13782 =/ env=ienv env.resolution
15024 =/ env=ienv env.resolution
13783 ?^ (ienv-lookup %main env) ~
15025 ?^ (ienv-lookup %main env) ~
@@ -13785,15 +15027,11 @@
13785 ?~ (ienv-lookup update.parts env) ~
15027 ?~ (ienv-lookup update.parts env) ~
13786 ?~ (ienv-lookup view.parts env) ~
15028 ?~ (ienv-lookup view.parts env) ~
13787 ?~ (ienv-lookup subs.parts env) ~
15029 ?~ (ienv-lookup subs.parts env) ~
13788− =/ relation=(unit [message=itype model=itype])
13789− (program-update-relation update.parts ds env)
13791 =/ inits=(list def)
15030 =/ inits=(list def)
13792 (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
15031 (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13793 ?. ?=([* ~] inits) ~
15032 ?. ?=([* ~] inits) ~
13794 =/ init-def=def i.inits
15033 =/ init-def=def i.inits
13795 ?> ?=(%value -.init-def)
15034 ?> ?=(%value -.init-def)
13796− ?. (program-init-null-sample init-def) ~
13797 =/ written=(unit sample) (direct-gate-sample init-def)
15035 =/ written=(unit sample) (direct-gate-sample init-def)
13798 ?~ written ~
15036 ?~ written ~
13799 =/ body=expr
15037 =/ body=expr
@@ -13803,141 +15041,44 @@
13805 ?~ prelude.initial ~
15043 ?~ prelude.initial ~
13806− ?~ (ienv-lookup %program values.u.prelude.initial) ~
15044+ =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13807 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
15046 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13808 ?~ heads ~
15047 ?~ heads ~
13809− ?~ (~(get by gates.u.heads) %program) ~
15048+ =/ program-def=(unit def) (~(get by gates.u.heads) %program)
13810 =/ checked=(map term def) (direct-checked-gates ds env)
15050 =/ checked=(map term def) (direct-checked-gates ds env)
13811 =/ templates=ienv
15051 =/ templates=ienv
13812 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
15052 (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13813− =/ scanned=(unit dgscan)
15053+ =/ fresh=(unit @ud)
13814− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
15054+ (ienv-fresh-id (weld env (weld values.u.prelude.initial templates)))
13815− ?~ scanned ~
15055+ ?~ fresh ~
13816− =. next.initial (dg-next-id ids.u.scanned 0)
15056+ =. next.initial u.fresh
15057+ =/ model=(unit itype)
15058+ %: program-init-model
15059+ main parts ds env u.program u.program-def
15060+ initial(gate-defs checked, head-evidence heads)
13817 =/ init-state=istate (reserve-def-caps val.init-def initial)
15063 =/ init-state=istate (reserve-def-caps val.init-def initial)
13818 =/ sam=isample-result (infer-sample u.written env init-state)
15064 =/ sam=isample-result (infer-sample u.written env init-state)
13819 ?: ?=(%| -.sam) ~
15065 ?: ?=(%| -.sam) ~
13820 ?. ?=(~ (itype-vars typ.p.sam)) ~
15066 ?. ?=(~ (itype-vars typ.p.sam)) ~
13821 ?: (itype-has-tag typ.p.sam) ~
15067 ?: (itype-has-tag typ.p.sam) ~
13822 =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
15068 =/ st=istate state.p.sam(gate-defs checked, head-evidence heads)
15069+ =/ contextual=iresult
15070+ (infer-call-context-arg body u.model env.p.sam st (span-of body))
13823 =/ inferred=iresult
15071 =/ inferred=iresult
13824− (infer-call-context-arg body model.u.relation env.p.sam st (span-of body))
15072+ ?: ?=(%& -.contextual) contextual
15073+ (program-init-ordinary init-def env typ.p.sam init-state(gate-defs checked, head-evidence heads))
13825 ?: ?=(%| -.inferred) ~
15074 ?: ?=(%| -.inferred) ~
13826 =/ product-fit=ifit
15075 =/ product-fit=ifit
13827− (itype-fit typ.p.inferred model.u.relation sub.state.p.inferred next.state.p.inferred)
15076+ (itype-fit typ.p.inferred u.model sub.state.p.inferred next.state.p.inferred)
13828 ?. ?=(%ok -.product-fit) ~
15077 ?. ?=(%ok -.product-fit) ~
13829 =/ merged-product=itype
15078 =/ merged-product=itype
13830− (itype-merge-faces typ.p.inferred model.u.relation sub.product-fit)
15079+ (itype-merge-faces typ.p.inferred u.model sub.product-fit)
13831 =/ actual-cast=itype [%fn typ.p.sam merged-product]
15080 =/ actual-cast=itype [%fn typ.p.sam merged-product]
13832− =/ closed=itype [%fn typ.p.sam model.u.relation]
15081+ =/ closed=itype [%fn typ.p.sam u.model]
13834− (itype-fit actual-cast closed sub.product-fit next.product-fit)
13835− ?. ?=(%ok -.cast) ~
13836− =/ merged=itype (itype-merge-faces actual-cast closed sub.cast)
13837− =/ adjusted=iresult
13838− [%& merged state.p.inferred(sub sub.cast, next next.cast)]
13839− =/ added=(unit iadded-definition)
13840− (add-supported-result init-def adjusted init-state env checked artifacts.resolution)
13842− =/ recovered=(unit ischeme) (ienv-lookup init.parts env.u.added)
13844− ?. ?=(~ vars.u.recovered) ~
13845− ?. ?=(~ (itype-vars typ.u.recovered)) ~
13846− `[env.u.added grouped.resolution artifacts.u.added]
13848−:: Recover only the initializer of an already recognized direct program main.
13849−:: The derived call is evidence for an ordinary init/main retry, never an
13850−:: interface to publish on its own. Any failure returns the original resolution.
13851−++ program-init-context
13852− |= [main=def parts=[init=term update=term view=term subs=term] ds=(list def) resolution=iresolved initial=istate]
13853− ^- (unit iresolved)
13854− =/ env=ienv env.resolution
13855− ?^ (ienv-lookup %main env) ~
13856− ?^ (ienv-lookup init.parts env) ~
13857− =/ update=(unit ischeme) (ienv-lookup update.parts env)
13858− =/ view=(unit ischeme) (ienv-lookup view.parts env)
13859− =/ subs=(unit ischeme) (ienv-lookup subs.parts env)
13863− =/ inits=(list def)
13864− (skim ds |=(d=def &(?=(%value -.d) =(init.parts name.d))))
13865− ?. ?=([* ~] inits) ~
13866− =/ init-def=def i.inits
13867− ?> ?=(%value -.init-def)
13868− ?. (program-init-tuple-null init-def) ~
13869− =/ args=(unit (list expr)) (program-main-args main)
13871− ?~ prelude.initial ~
13872− =/ program=(unit ischeme) (ienv-lookup %program values.u.prelude.initial)
13874− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.initial)
13876− =/ written=(unit def) (~(get by gates.u.heads) %program)
13878− =/ written-sample=(unit sample) (direct-gate-sample u.written)
13879− ?~ written-sample ~
13880− ?. ?=(%cell -.u.written-sample) ~
13881− ?~ items.u.written-sample ~
13882− =/ checked=(map term def) (direct-checked-gates ds env)
13884− (turn molds.u.prelude.initial |=(x=[name=term template=ischeme] [name.x template.x]))
13885− =/ scanned=(unit dgscan)
13886− (dg-all-env-ids (weld env (weld values.u.prelude.initial templates)) 32.768 ~)
13888− =. next.initial (dg-next-id ids.u.scanned 0)
13889− =/ instance=[typ=itype state=istate] (instantiate-scheme u.program initial)
13890− ?. ?=(%fn -.typ.instance) ~
13891− ?. ?=(%cell -.sample.typ.instance) ~
13892− =/ expected-init=(unit itype)
13893− (direct-slot-body hed.sample.typ.instance (direct-sample-name i.items.u.written-sample))
13894− ?~ expected-init ~
13895− ?. ?=(%fn -.u.expected-init) ~
13896− ?. ?=(%var -.sample.u.expected-init) ~
13897− =/ data=@ud id.sample.u.expected-init
13898− =/ init-var=itype [%var next.state.instance]
13899− =/ st=istate state.instance(next +(next.state.instance))
13900− =/ up=[typ=itype state=istate] (instantiate-scheme u.update st)
13901− =/ vw=[typ=itype state=istate] (instantiate-scheme u.view state.up)
13902− =/ sb=[typ=itype state=istate] (instantiate-scheme u.subs state.vw)
13903− =. st state.sb(gate-defs checked, head-evidence heads)
13904− =/ actual=itype [%cell init-var [%cell typ.up [%cell typ.vw typ.sb]]]
13906− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.st next.st)
13907− ?. ?=(%ok -.fit) ~
13908− =/ actual-final=itype (itype-normalize actual sub.fit)
13909− =/ expected-final=itype (itype-normalize sample.typ.instance sub.fit)
13910− =/ open=(list @ud)
13911− (unique-type-vars (weld (itype-vars actual-final) (itype-vars expected-final)))
13912− ?. (levy open |=(n=@ud =(data n))) ~
13913− ?: |((itype-has-tag actual-final) (itype-has-tag expected-final)) ~
13915− (direct-positional-fit u.args items.u.written-sample actual sample.typ.instance env st sub.fit next.fit)
13916− ?. ?=(%ok -.replay) ~
13917− ?. &(=(sub.fit sub.replay) =(next.fit next.replay)) ~
13918− =/ expected=itype (itype-normalize u.expected-init sub.fit)
13919− ?. ?=(%fn -.expected) ~
13920− =. st st(sub sub.fit, next next.fit)
13921− =/ init-state=istate (reserve-def-caps val.init-def st)
13922− =/ inferred=iresult (infer-fragment val.init-def env init-state)
13923− =? inferred ?=(%| -.inferred) (infer-recursive-gate init-def env init-state)
13924− ?: ?=(%| -.inferred) ~
13925− ?. ?=(%fn -.typ.p.inferred) ~
13926− ?^ (itype-vars sample.typ.p.inferred) ~
13928− (itype-fit sample.typ.p.inferred sample.expected sub.state.p.inferred next.state.p.inferred)
13929− ?. ?=(%ok -.data-fit) ~
13930− =/ closed=itype (itype-normalize expected sub.data-fit)
13931− ?. ?=(%fn -.closed) ~
13932− :: Resolve the ordinary tuple cast first, then check the complete gate.
13933− :: General function fit remains unchanged; only this recovered candidate
13934− :: receives the derived result context before its whole-type cast fit.
13935− =/ product-fit=ifit
13936− (itype-fit product.typ.p.inferred product.closed sub.data-fit next.data-fit)
13937− ?. ?=(%ok -.product-fit) ~
13939− (itype-merge-faces product.typ.p.inferred product.closed sub.product-fit)
13940− =/ actual-cast=itype [%fn sample.typ.p.inferred product]
13941 =/ cast=ifit
15082 =/ cast=ifit
13942 (itype-fit actual-cast closed sub.product-fit next.product-fit)
15083 (itype-fit actual-cast closed sub.product-fit next.product-fit)
13943 ?. ?=(%ok -.cast) ~
15084 ?. ?=(%ok -.cast) ~
@@ -14308,12 +15449,48 @@
14308 ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
15449 ?: &(?=([%ui %api *] at) ?=(^ (program-main-def defs.mod)))
14309 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
15450 [%| [(crip "module kind needs unsupported inference: {(spud at)}") ~]]
14310 ?: ?=([%ui %api *] at)
15451 ?: ?=([%ui %api *] at)
15452+ =/ poke=(each ifile @t)
14311− =/ iface=(unit ifile) (api-poke-interface at mod mark-externals prelude-values prelude-molds prelude)
15453+ (api-poke-interface-result at mod mark-externals prelude-values prelude-molds prelude)
14312− ?^ iface
15455+ =/ iface=ifile p.poke
14313− =/ checked=ifile u.iface(source `src, graph `[(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals])
15456+ =/ checked=ifile iface(source `src, graph `[(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals])
14314 [%& [checked [[at checked] cache]]]
15457 [%& [checked [[at checked] cache]]]
15458+ :: A clashing derived name is an error wherever the checks below stop.
15459+ =/ clash=(unit idiag)
15460+ ?. ?=([%ui %api @ %jibb ~] at) ~
15461+ (api-derived-clash mod prelude-values)
15462+ ?^ clash [%| [(show-duplicate-fields at src u.clash) ~]]
15463+ :: So is a name conflict in its scope, reported as for other modules.
15464+ :: `+$ paths` and `+$ poke` are declarations, not molds (overview), and
15465+ :: a `/%` mark names a mold, so it conflicts only with another mark or
15466+ :: mold: `/% %todos` beside the request `todos` is the usual API.
15467+ =/ ordinary=(list def)
15468+ (skim defs.mod |=(d=def !&(?=(%mold -.d) |(=(%paths name.d) =(%poke name.d)))))
15469+ =/ marks=(list term) (collect-mark-imports imports.mod)
15470+ =/ mold-names=(list term)
15471+ (turn (collect-simple-molds ordinary) |=(m=[name=term body=shape] name.m))
15472+ =/ faces=(list import) (skip imports.mod |=(i=import ?=(%mark -.i)))
15473+ ?. ?& (module-scope-valid mod(defs ordinary, imports faces) prelude-values prelude-molds)
15476+ ?& (unique-value-name n marks)
15477+ !(lien mold-names |=(m=term =(m n)))
15478+ !(lien prelude-molds |=(m=term =(m n)))
15481+ [%| [(crip "module has conflicting names: {(spud at)}") ~]]
14315 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15482 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
14316 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
15483 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
15484+ :: A failing Jibb import gives its own error, which may be definite, as
15485+ :: it does for other modules; the constructors below would only wrap it.
15486+ :: They resolve the same imports again, from the interfaces cached here.
15487+ =/ js=jimports-detailed-result
15488+ (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
15489+ ?: ?=(%| -.js) [%| p.js]
15490+ :: Without `+$ paths` only the poke-only interface applies; keep its reason.
15491+ ?. (lien defs.mod |=(d=def &(?=(%mold -.d) =(%paths name.d))))
15492+ [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.poke)}") ~]]
15493+ :: Each constructor names the part that stopped it; keep that reason.
14317 =/ narrow=?
15494 =/ narrow=?
14318 ?. ?=([[%mark *] ~] imports.mod) |
15495 ?. ?=([[%mark *] ~] imports.mod) |
14319 ?. ?=([[%mold *] ~] defs.mod) |
15496 ?. ?=([[%mold *] ~] defs.mod) |
@@ -14321,13 +15498,13 @@
14321 !?=(%union -.shape.i.defs.mod)
15498 !?=(%union -.shape.i.defs.mod)
14322 ?: narrow
15499 ?: narrow
14323 =/ request=(each ione-request-interface @t)
15500 =/ request=(each ione-request-interface @t)
14324− (one-request-interface-graph at src externals mark-externals modules active cache `prepared)
15501+ (one-request-interface-graph at src externals mark-externals modules active cache.p.js `prepared)
14325− ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15502+ ?: ?=(%| -.request) [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.request)}") ~]]
14326 =/ checked=ifile iface.p.request
15503 =/ checked=ifile iface.p.request
14327 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
15504 [%& [checked [[at checked] dependencies.paths.support.p.request]]]
14328 =/ multi=(each [iface=ifile cache=jcache] @t)
15505 =/ multi=(each [iface=ifile cache=jcache] @t)
14329− (multi-request-interface-graph at src externals mark-externals modules active cache `prepared)
15506+ (multi-request-interface-graph at src externals mark-externals modules active cache.p.js `prepared)
14330− ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15507+ ?: ?=(%| -.multi) [%| [(crip "API module needs unsupported inference: {(spud at)}: {(trip p.multi)}") ~]]
14331 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
15508 [%& [iface.p.multi [[at iface.p.multi] cache.p.multi]]]
14332 =/ main=(unit def) (program-main-def defs.mod)
15509 =/ main=(unit def) (program-main-def defs.mod)
14333 =/ main-parts=(unit [init=term update=term view=term subs=term])
15510 =/ main-parts=(unit [init=term update=term view=term subs=term])
@@ -14336,8 +15513,12 @@
14336 ?~(main ~ (page-main-parts u.main))
15513 ?~(main ~ (page-main-parts u.main))
14337 =/ store-parts=(unit [init=term update=term])
15514 =/ store-parts=(unit [init=term update=term])
14338 ?~(main ~ (store-main-parts u.main))
15515 ?~(main ~ (store-main-parts u.main))
15516+ =/ declaration=(each istore-declaration (unit idiag))
15517+ ?~(store-parts [%| ~] (store-declaration mod prelude-values prelude-molds))
15518+ =/ clash=(unit idiag) ?:(?=(%| -.declaration) p.declaration ~)
15519+ ?^ clash [%| [(show-duplicate-fields at src u.clash) ~]]
14339 =/ declared=(unit istore-declaration)
15520 =/ declared=(unit istore-declaration)
14340− ?~(store-parts ~ (store-declaration mod prelude-values prelude-molds))
15521+ ?:(?=(%| -.declaration) ~ `p.declaration)
14341 ?: &(?=(^ store-parts) ?=(~ declared))
15522 ?: &(?=(^ store-parts) ?=(~ declared))
14342 [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
15523 [%| [(crip "module kind or scope needs unsupported inference: {(spud at)}") ~]]
14343 ?: &(?=([%ui %stores *] at) ?=(^ main) ?=(~ store-parts))
15524 ?: &(?=([%ui %stores *] at) ?=(^ main) ?=(~ store-parts))
@@ -14401,11 +15582,8 @@
14401 ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
15582 ?^(viewed ~ (program-plain-view-context u.main-parts ds with-keyed-view state))
14402 =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
15583 =/ with-view=iresolved ?~(plain-view with-keyed-view u.plain-view)
14403 =/ initialized=(unit iresolved)
15584 =/ initialized=(unit iresolved)
14404− (program-init-context u.main u.main-parts ds with-view state)
15585+ (program-plain-init-context u.main u.main-parts ds with-view state)
14405− =/ with-initialized=iresolved ?~(initialized with-view u.initialized)
14406− =/ plain-init=(unit iresolved)
14407− ?^(initialized ~ (program-plain-init-context u.main-parts ds with-initialized state))
14408− =/ components=iresolved ?~(plain-init with-initialized u.plain-init)
15586+ =/ components=iresolved ?~(initialized with-view u.initialized)
14409 (program-main-context u.main ds components state)
15587 (program-main-context u.main ds components state)
14410 =. env env.recovered
15588 =. env env.recovered
14411 =. artifacts.resolution artifacts.recovered
15589 =. artifacts.resolution artifacts.recovered
@@ -14426,7 +15604,15 @@
14426 =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15604 =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
14427 ?^ pending
15605 ?^ pending
14428 [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15606 [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15607+ :: A shadowing sample is an error, so it comes before any named value.
15608+ =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15609+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
15611+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15612+ [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
15613+ =/ missing=(unit term) (module-missing-value required env)
15614+ =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
14429− [%| [(crip "module definitions need unsupported inference: {(spud at)}") ~]]
15615+ [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
14430 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals]
15616 =/ initial=irequest-graph [(silt `(list path)`~[at]) ~ ~ modules prelude prelude-values prelude-molds externals mark-externals]
14431 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
15617 =/ graph=(unit irequest-graph) (request-graph-merge resolved.p.js initial (add 1 (lent resolved.p.js)))
14432 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
15618 ?~ graph [%| ['module request evidence needs unsupported inference' ~]]
@@ -14627,8 +15813,8 @@
14627 ?: ?=(%| -.parsed) (show-error src p.parsed)
15813 ?: ?=(%| -.parsed) (show-error src p.parsed)
14628 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
15814 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
14629 ?^ duplicate (duplicate-fields-report file src u.duplicate)
15815 ?^ duplicate (duplicate-fields-report file src u.duplicate)
14630− ?: (module-has-reserved-proj p.parsed)
15816+ ?: (module-has-reserved p.parsed)
14631− 'module has reserved proj name'
15817+ 'module has a reserved proj or unface name'
14632 =/ ds=(list def) defs.p.parsed
15818 =/ ds=(list def) defs.p.parsed
14633 =/ molds=imolds (collect-simple-molds ds)
15819 =/ molds=imolds (collect-simple-molds ds)
14634 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
15820 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -14706,7 +15892,7 @@
14706 =. head-evidence.initial heads
15892 =. head-evidence.initial heads
14707 =. initial (reserve-def-caps val.d initial)
15893 =. initial (reserve-def-caps val.d initial)
14708 =/ result=iresult
15894 =/ result=iresult
14709− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
15895+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))
14710 (infer-recursive-gate d env initial)
15896 (infer-recursive-gate d env initial)
14711 (infer-fragment val.d env initial)
15897 (infer-fragment val.d env initial)
14712 ?: ?=(%| -.result)
15898 ?: ?=(%| -.result)
@@ -14736,11 +15922,10 @@
14736 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
15922 ?: (unsupported-atom-vars typ caps.state.p.result binders.state.p.result sub.state.p.result)
14737 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
15923 $(ds t.ds, lines [(crip "++ {(trip name.d)}: unresolved aura-variable inference") lines])
14738 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
15924 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
14739− ?: (gth (lent vars) 26)
14740− $(ds t.ds, lines [(crip "++ {(trip name.d)}: too many variables for partial printer") lines])
14741 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
15925 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
14742 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
15926 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
15927+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.result sub.state.p.result)
14743− =/ printable=itype (canonical-itype typ vars)
15928+ =/ printable=itype (canonical-itype named)
14744 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
15929 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
14745 $(ds t.ds, lines [line lines])
15930 $(ds t.ds, lines [line lines])
14746:: Experimental module-owned pending-constraint generalization only.
15931:: Experimental module-owned pending-constraint generalization only.
@@ -14837,7 +16022,7 @@
14837 =/ normalized=itype (itype-normalize typ sub.state)
16022 =/ normalized=itype (itype-normalize typ sub.state)
14838 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
16023 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
14839 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
16024 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
14840− `[[normalized quantified]]
16025+ `(cap-names normalized quantified caps.state sub.state)
14842+$ dgcommit [env=ienv state=istate]
16027+$ dgcommit [env=ienv state=istate]
14843:: A branch literal must not acquire a value face through replay.
16028:: A branch literal must not acquire a value face through replay.
@@ -14929,6 +16114,8 @@
14929 ?: ?=(%| -.left) left
16114 ?: ?=(%| -.left) left
14930 =/ right=iresult (infer-fragment val.y env state.p.left)
16115 =/ right=iresult (infer-fragment val.y env state.p.left)
14931 ?: ?=(%| -.right) right
16116 ?: ?=(%| -.right) right
16117+ =/ joined=(unit [typ=itype sub=isub]) (itype-branch-join typ.p.left typ.p.right sub.state.p.right)
16118+ ?^ joined [%& typ.u.joined state.p.right(sub sub.u.joined)]
14932 ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)
16119 ?. (dg-stable-fit typ.p.left typ.p.right sub.state.p.right)
14933 =/ st=istate state.p.right
16120 =/ st=istate state.p.right
14934 ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)
16121 ?. (dg-owned-arm-literal val.x typ.p.left tags.st sub.st next.state)
@@ -15173,7 +16360,6 @@
15173 ?~ env &
16360 ?~ env &
15174 =/ sc=ischeme scheme.i.env
16361 =/ sc=ischeme scheme.i.env
15175 ?: |((itype-has-hidden-recursive typ.sc) (itype-has-hidden-generic typ.sc)) |
16362 ?: |((itype-has-hidden-recursive typ.sc) (itype-has-hidden-generic typ.sc)) |
15176− ?: (gth (lent vars.sc) 26) |
15177 $(env t.env)
16363 $(env t.env)
15178:: Parse status and the transaction result come from the same source parse.
16364:: Parse status and the transaction result come from the same source parse.
15179+$ dgparse [parsed=? result=(unit dgcommit)]
16365+$ dgparse [parsed=? result=(unit dgcommit)]
@@ -15202,9 +16388,9 @@
15202 =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)
16388 =/ free=(unit dgscan) (dg-env base ~ 32.768 ~)
15203 ?~ free ~
16389 ?~ free ~
15204 ?^ ids.u.free ~
16390 ?^ ids.u.free ~
15205− =/ all=(unit dgscan) (dg-all-env-ids base 32.768 ~)
16391+ =/ all=(unit @ud) (ienv-fresh-id base)
15206 ?~ all ~
16392 ?~ all ~
15207− =/ fresh=@ud (dg-next-id ids.u.all 0)
16393+ =/ fresh=@ud u.all
15208 =/ st=istate *istate
16394 =/ st=istate *istate
15209 =. st st(next fresh, defer `~, molds molds, globals globals, at at, top-molds (turn molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
16395 =. st st(next fresh, defer `~, molds molds, globals globals, at at, top-molds (turn molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
15210 =/ checked-molds=(each imold-types @t) (module-mold-types molds st)
16396 =/ checked-molds=(each imold-types @t) (module-mold-types molds st)
@@ -15244,33 +16430,61 @@
15244 =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
16430 =/ free=(unit dgscan) (dg-env all-env ~ 32.768 ~)
15245 ?~ free ~
16431 ?~ free ~
15246 ?^ ids.u.free ~
16432 ?^ ids.u.free ~
15247− =/ all=(unit dgscan) (dg-all-env-ids all-env 32.768 ~)
16433+ =/ all=(unit @ud) (ienv-fresh-id all-env)
15248 ?~ all ~
16434 ?~ all ~
15249− =/ fresh=@ud (dg-next-id ids.u.all 0)
16435+ =/ fresh=@ud u.all
15250 =/ st=istate *istate
16436 =/ st=istate *istate
15251 =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
16437 =. st st(next fresh, defer `~, molds local-molds, globals globals, at at, reserved-molds molds.prepared, prelude prelude, top-molds (turn local-molds |=(m=[name=term body=shape] name.m)), in-mold |, jrec-fuel 256)
15252 =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
16438 =/ checked-molds=(each imold-types @t) (module-mold-types local-molds st)
15253 ?: ?=(%| -.checked-molds) ~
16439 ?: ?=(%| -.checked-molds) ~
15254 (dg-stage defs base base st ~ 64)
16440 (dg-stage defs base base st ~ 64)
15256−++ dg-all-env-ids
16442+:: +ienv-fresh-id: one above the largest type variable or tag ID in env
16444+:: One pass over every ID in env's schemes, quantified or free, so a
16445+:: variable numbered from it captures none of them. A %recursive or
16446+:: %jrec type names its mold and holds no variable, so it is a leaf,
16447+:: and the pass is linear in the size of the types, with no budget.
16448+:: A scheme that still holds an unresolved tag declines.
15257− |= [env=ienv fuel=@ud ids=(list @ud)]
16451+ |= env=ienv
15258− ^- (unit dgscan)
16452+ ^- (unit @ud)
15259− ?~ env `[ids fuel]
16453+ =/ top=@ud 0
15260− ?: =(0 fuel) ~
16454+ |-
15261 =/ sc=ischeme scheme.i.env
16456 =/ sc=ischeme scheme.i.env
15262 ?: (itype-has-tag typ.sc) ~
16457 ?: (itype-has-tag typ.sc) ~
15263− =/ raw=(unit dgscan) (dg-scan ~[typ.sc] ~ (dec fuel) ids)
16458+ $(env t.env, top (itype-max-id typ.sc (max top (roll (turn vars.sc var-count) max))))
15265− =/ quant=(unit dgscan) (dg-scan-ids vars.sc ~ fuel.u.raw ids.u.raw)
16460+:: +itype-max-id: the largest variable or tag ID in t, or top, without
15266− ?~ quant ~
16461+:: the variables' names (+named-var)
15267− $(env t.env, fuel fuel.u.quant, ids ids.u.quant)
16462+::
16464+ |= [t=itype top=@ud]
16467+ %var (max top (var-count id.t))
16468+ %fvar (max top (var-count id.t))
16469+ %avar (max top (var-count id.t))
16470+ %rvar (max top (var-count id.t))
16471+ %nvar (max top (var-count id.t))
16472+ %rnvar (max top (var-count id.t))
16473+ %tag (max top id.t)
16474+ ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
16475+ %collection (itype-max-ids args.t top)
16476+ %grec (itype-max-ids args.t top)
16477+ %union (itype-max-ids args.t (itype-max-ids cases.t top))
16479+ %fn $(t sample.t, top $(t product.t))
16480+ %cell $(t hed.t, top $(t tal.t))
15269−++ dg-next-id
16483+++ itype-max-ids
15270− |= [ids=(list @ud) largest=@ud]
16484+ |= [ts=(list itype) top=@ud]
15272− ?~ ids +(largest)
16486+ ?~ ts top
15273− $(ids t.ids, largest (max largest i.ids))
16487+ $(ts t.ts, top (itype-max-id i.ts top))
15275++ dg-eligible-ctor
16489++ dg-eligible-ctor
15276 |= [e=expr head=itype actual=itype expected=itype state=istate]
16490 |= [e=expr head=itype actual=itype expected=itype state=istate]