@@ -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,93 @@
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="") ~]
852+:: ===================================================================
853+:: 5. General checker core (design; not implemented yet)
854+:: ===================================================================
856+:: The existing inference and recovery paths are described in
857+:: docs/compiler.md. This section is a plan for replacing them, not a
858+:: claim that the current checker implements these rules. The Grammar and
859+:: Decisions are authoritative if this design needs adjustment.
861+:: 5.1 State and unification. Give each inference variable an identity and
862+:: a union-find entry: parent or binding, rank, level, source, rigidity,
863+:: and the atom, arithmetic-atom and gate-free obligations it carries.
864+:: Hoon's immutable maps hold the entries; operations return the updated
865+:: state. Find compresses paths in that returned state. Bind only after an
866+:: occurs check, merge obligations at roots, and lower levels throughout
867+:: the bound type to the root's level. A rigid written capital may acquire
868+:: allowed constraints but cannot be forced to a concrete type or a
869+:: different written capital. Keep origins for both sides of each fit so
870+:: a failure can show both excerpts. Recursive named molds retain their
871+:: identity; the occurs check is for inference variables, not a ban on
872+:: declared recursion.
874+:: A scheme quantifies eligible variables above the enclosing level;
875+:: instantiate with fresh variables and copy their obligations. Written
876+:: capitals respect their lexical scope, including sharing with a local
877+:: definition when the enclosing definition uses the same name. Retain
878+:: aura variables and directional aura fits, rather than turning every
879+:: fit into symmetric equality. At a faced position a capital binds the
880+:: type under the face; joining an unnamed position with a faced one keeps
881+:: the face, independently of the order of the inputs. Different explicit
882+:: faces conflict. No gate may hide inside a gate-free type, including in
883+:: a container; propagate the obligation through its arguments.
885+:: 5.2 Work queue. A constraint owns its source span, the types and
886+:: expression shape it depends on, and the information needed to report
887+:: failure. Tags and constructors, null, decimal and cell literals,
888+:: wings, changes, unface and unknown match subjects enter the same queue.
889+:: Index waiting constraints by the roots they read. Binding or merging a
890+:: root wakes its dependants; a retry either solves, fails with its sites,
891+:: or registers the roots still needed. Run to a fixed point, without
892+:: losing constraints when a root is redirected. Check patterns once the
893+:: subject is known. Contextual tags inspect case shapes and noun-equal
894+:: heads, retaining the named union and its site in diagnostics.
896+:: Variables reachable from an open tag constraint remain monomorphic
897+:: across definitions, so a later use, including main, can fix them.
898+:: Other eligible variables can generalize, with their atom and gate-free
899+:: obligations intact. At each definition boundary resolve its holes and
900+:: apply the specified decimal and cell defaults, without defaulting a
901+:: decimal whose definition is generic over its aura. A decimal fits @ud,
902+:: @u, @ and *; other concrete auras need their own literal. At module
903+:: completion retry the queue and report each still-open constraint at its
904+:: source; an unresolved tag asks for a ^-, never a guessed union.
906+:: 5.3 Definition order and kinds. Use the existing dependency graph's
907+:: strongly connected components in dependency order. Give a recursive
908+:: group of gates monomorphic placeholders, infer all members in one state,
909+:: solve what can be solved, then generalize together. Reject a cycle
910+:: involving a non-gate value, including one through a gate, and show the
911+:: cycle. Check a named definition's holes before later uses can fix them.
912+:: Infer main as an ordinary expression against ordinary prelude schemes;
913+:: only its resulting type determines library, page, island or store.
914+:: Afterwards check kind-specific invariants: recursively find the field
915+:: containing a gate in island data or a model, and inspect subscriptions
916+:: for watchability only at %watch. A page load may be any gate to ask,
917+:: including pure and typed paths. Preserve request provenance needed for
918+:: a watchability proof through ordinary calls and aliases.
920+:: 5.4 Matches and migration. A reusable usefulness matrix over noun
921+:: constructors, constants, cells and wildcards checks nested patterns;
922+:: loobeans, lists and units expand to their cases. Test an arm against
923+:: previous rows for usefulness, then test a wildcard for exhaustiveness;
924+:: keep a witness for a missing case and the covering arm's site for a
925+:: dead one. Recursive types require memoized specialization and a
926+:: terminating treatment of recursive states. The same matrix can later
927+:: drive lowering. The bare-name/tag spelling rule is checked against the
928+:: subject and the cases the rest of the pattern can match.
930+:: Migrate in small stages with eval and ship goldens for every change.
931+:: Keep diagnostics and source sites in the single full result; types.txt
932+:: is a rendering of that result. As general inference covers an existing
933+:: recovery or source-proven slice, remove that slice and retain its tests.
934+:: An unsupported construct fails closed at its own site until then.
824+| %positions
937+| %positions
@@ -964,9 +1077,10 @@
965+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
1078+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
967−:: +edit: a change's item or line, name=value
1080+:: +edit: a change's item or line, name=value or wing=value; names
1081+:: as written, as a %wing's: open.cart is ~[%open %cart]
969−+$ edit $~([*span %$ *expr] [at=span name=term val=expr])
1083++$ edit $~([*span ~ *expr] [at=span names=(list term) val=expr])
971:: +arm: a ?- arm, a pattern and an expression or body
1085:: +arm: a ?- arm, a pattern and an expression or body
@@ -1355,10 +1469,10 @@
1355 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
1469 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
1356 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
1470 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
1357 ?: (is-upper a)
1471 ?: (is-upper a)
1472+ =/ n=@ud (run-len t.cs tvar-mask)
1358− => (emit 1 [%tvar a])
1473+ => (emit +(n) [%tvar (crip [a (scag n t.cs)])])
1359− ?. &(?=(^ cs) |((is-lower i.cs) (is-upper i.cs) (is-digit i.cs)))
1474+ ?. &(?=(^ cs) |((is-upper i.cs) =('_' i.cs) =('-' i.cs))) cor
1361− (err col "a type variable is one capital letter")
1475+ (err col "a type variable is a capital, then lowercase letters and digits")
1362 ?: =(':' a)
1476 ?: =(':' a)
1363 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
1477 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
1364 ?: =(':' b) comment
1478 ?: =(':' b) comment
@@ -1662,6 +1776,7 @@
1662++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
1776++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
1663++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f
1777++ 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 -
1778++ name-mask 0x7ff.fffe.0000.0000.03ff.2000.0000.0000 :: a-z 0-9 -
1779+++ 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 . ~ _
1780++ 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 .
1781++ 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
1782++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2
@@ -2280,7 +2395,7 @@
2280++ sexp-edit
2395++ sexp-edit
2281 |= e=edit
2396 |= e=edit
2283− (nod "edit" at.e (trip name.e) ~[(sexp-expr val.e)])
2398+ (nod "edit" at.e (show-names names.e) ~[(sexp-expr val.e)])
2285++ sexp-arm
2400++ sexp-arm
2286 |= a=arm
2401 |= a=arm
@@ -2689,24 +2804,32 @@
2689 ?~ t.els i.els
2804 ?~ t.els i.els
2690 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
2805 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
2807+:: +slot: a bracket's item or line as read, before +bracket-node
2808+:: makes it an item or an edit: its name=, or a change's wing=, else ~
2810++$ slot [at=span face=(list term) val=expr]
2692:: +bracket-node: a tuple, list or change from its items, ending at fin
2812:: +bracket-node: a tuple, list or change from its items, ending at fin
2694++ bracket-node
2814++ bracket-node
2695 |= $: kind=?(%tuple %list %change)
2815 |= $: kind=?(%tuple %list %change)
2696 op=token
2816 op=token
2697 target=(unit [t=token names=(list term)])
2817 target=(unit [t=token names=(list term)])
2698− its=(list item)
2818+ its=(list slot)
2703− %tuple [%tuple [beg.at.op fin] its]
2824+ :+ %tuple [beg.at.op fin]
2704− %list [%list [beg.at.op fin] (turn its |=(i=item val.i))]
2825+ (turn its |=(i=slot ^-(item [at.i ?~(face.i ~ `i.face.i) val.i])))
2827+ %list [%list [beg.at.op fin] (turn its |=(i=slot val.i))]
2707 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
2830 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
2708 :^ %change [beg fin] ?~(target ~ names.u.target)
2831 :^ %change [beg fin] ?~(target ~ names.u.target)
2709− (turn its |=(i=item ^-(edit [at.i ?~(face.i %$ u.face.i) val.i])))
2832+ (turn its |=(i=slot ^-(edit [at.i face.i val.i])))
2712+| %parser
2835+| %parser
@@ -2927,23 +3050,22 @@
2928 :: +unnamed: a change's item or line without its name=
3051 :: +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
3053+ :: 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)`
3054+ :: 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
3055+ :: `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
3056+ :: 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,
3057+ :: 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
3058+ :: `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).
3059+ :: whose text can't begin a name, at that text, as `m( @sd` at the
2939 ++ unnamed
3062 ++ unnamed
2940 |= ts=(list token)
3063 |= ts=(list token)
2941 ^- [%| p=error]
3064 ^- [%| p=error]
2942 =/ why=tape "a change's items are named, as in m(done=%.y)"
3065 =/ why=tape "a change's items are named, as in m(done=%.y)"
2943 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
3066 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
2944− ?: ?=([[* * [%wing *]] *] ts)
3067+ ?. ?=([[* * ?([%name *] [%wing *])] *] ts)
2945− (bad-in-why ts "a named item" lower-mask why)
2946− ?. ?=([[* * [%name *]] *] ts) (bad-why ts "a named item" why)
3068+ (bad-why ts "a named item" why)
2947 =/ want=tape "`=` right after {(show-found i.ts)}"
3069 =/ want=tape "`=` right after {(show-found i.ts)}"
2948 ?: ?& ?=([* [* * [%error *]] *] ts)
3070 ?: ?& ?=([* [* * [%error *]] *] ts)
2949 =(end.at.i.ts from.lex.i.t.ts)
3071 =(end.at.i.ts from.lex.i.t.ts)
@@ -2961,9 +3083,10 @@
2961 :: closes on its line (2.9). A bracket that needs none of these
3083 :: 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
3084 :: 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
3085 :: 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
3086+ :: 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.
3087+ :: after begins with NEWLINE or DEDENT, so it costs nothing on the way
3088+ :: to a tree, except where a rune takes the rest of a body (+read-last):
3089+ :: a look at that rune's line.
2968 ++ doomed
3091 ++ doomed
2969 |= [ts=(list token) after=(list token) want=tape]
3092 |= [ts=(list token) after=(list token) want=tape]
@@ -3120,7 +3243,7 @@
3120 ?: =(%'++' lex.rune)
3243 ?: =(%'++' lex.rune)
3121 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
3244 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
3122 ;< [e=expr more=(list token)] then
3245 ;< [e=expr more=(list token)] then
3123− (read-expr-or-body "the name" after)
3246+ (read-expr-or-body | "the name" after)
3124 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
3247 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
3125 ?: (is-closer rune)
3248 ?: (is-closer rune)
3126 %^ bad-why ts "a definition"
3249 %^ bad-why ts "a definition"
@@ -3200,20 +3323,36 @@
3200 [%& p.lex.i.ts t.ts]
3323 [%& p.lex.i.ts t.ts]
3202 :: +read-expr-or-body: a space and an expression on the line, or a
3325 :: +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
3326+ :: body on deeper lines; what names what comes before, for errors.
3327+ :: On a body's final line (fin, +read-last), a line at the same depth
3328+ :: is the rest of the body instead, and the expression on the line
3329+ :: goes on with fin, except a ?-, which keeps its arms deeper
3205 ++ read-expr-or-body
3331 ++ read-expr-or-body
3206− |= [what=tape ts=(list token)]
3332+ |= [fin=? what=tape ts=(list token)]
3207 ^- (pare expr)
3333 ^- (pare expr)
3208 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3334 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3335+ ?: &(fin ?=([[* * %newline] *] ts)) (read-rest t.ts)
3209 ?: ?=([[* * ?(%newline %dedent)] *] ts)
3336 ?: ?=([[* * ?(%newline %dedent)] *] ts)
3210 (bad ts "an expression, or a body on deeper lines")
3337 (bad ts "an expression, or a body on deeper lines")
3211 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3338 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3212− (read-expr ts)
3339+ (read-last &(fin !?=([[* * %'?-'] *] ts)) ts)
3214− :: +read-body: after its INDENT, { definition NEWLINE } expr DEDENT
3341+ :: +read-body: after its INDENT, the rest of a body, then its DEDENT
3216 ++ read-body
3343 ++ read-body
3346+ ;< [e=expr after=(list token)] then (read-rest ts)
3347+ ?> ?=([[* * %dedent] *] after)
3350+ :: +read-rest: { definition NEWLINE } last, up to the DEDENT that ends
3351+ :: a body, which it leaves for whatever opened the body: its INDENT's
3352+ :: reader, or the rune on the final line that took the rest of it
3217 |= ts=(list token)
3356 |= ts=(list token)
3218 ^- (pare expr)
3357 ^- (pare expr)
3219 =| defs=(list def)
3358 =| defs=(list def)
@@ -3227,12 +3366,15 @@
3227 %: bad-in-why ts "a definition or an expression" plus-mask
3366 %: bad-in-why ts "a definition or an expression" plus-mask
3228 "`+` begins `++` or `+$`"
3367 "`+` begins `++` or `+$`"
3230− ;< [e=expr after=(list token)] then (read-expr ts)
3369+ ;< [e=expr after=(list token)] then (read-last & ts)
3231 ?: ?=([[* * %dedent] *] after)
3370 ?: ?=([[* * %dedent] *] after)
3232 =/ ds=(list def) (flop defs)
3371 =/ ds=(list def) (flop defs)
3233 =/ beg=loc ?~(ds beg:(span-of e) beg:(span-of i.ds))
3372 =/ beg=loc ?~(ds beg:(span-of e) beg:(span-of i.ds))
3234− [%& [%body [beg end:(span-of e)] ds e] t.after]
3373+ [%& [%body [beg end:(span-of e)] ds e] after]
3235 ?. ?=([[* * %newline] *] after) (bad-end-in after (tail-can e))
3374 ?. ?=([[* * %newline] *] after) (bad-end-in after (tail-can e))
3375+ ?: &(?=(%branch -.e) !?=([* [* * ?(%'++' %'+$')] *] after))
3376+ %^ bad-why after "the end of the body"
3377+ "this `?-`'s arms are on deeper lines, so this one goes there too"
3236 %^ bad-why after "the end of the body"
3378 %^ bad-why after "the end of the body"
3237 "a body's final expression is its last line"
3379 "a body's final expression is its last line"
@@ -3241,13 +3383,24 @@
3241 ++ read-expr
3383 ++ read-expr
3242 |= ts=(list token)
3384 |= ts=(list token)
3243 ^- (pare expr)
3385 ^- (pare expr)
3388+ :: +read-last: +read-expr, where fin says the expression is a body's
3389+ :: final line or goes on one, with no bracket open before it: then
3390+ :: the rune that ends the line may take the rest of the body at the
3391+ :: same depth as its last child, and a ?- that begins the line its
3392+ :: arms (section 3, The rest of a body)
3395+ |= [fin=? ts=(list token)]
3244 ?~ ts (bad ts "an expression")
3397 ?~ ts (bad ts "an expression")
3245 =* t i.ts
3398 =* t i.ts
3246 ?+ lex.t (read-call ts)
3399 ?+ lex.t (read-call ts)
3247− %'|=' ?:((is-ctor ts) (read-call ts) (read-gate t t.ts))
3400+ %'|=' ?:((is-ctor ts) (read-call ts) (read-gate fin t t.ts))
3248− %'^-' (read-cast t t.ts)
3401+ %'^-' (read-cast fin t t.ts)
3249− %'~&' (read-trace t t.ts)
3402+ %'~&' (read-trace fin t t.ts)
3250− %'?-' (read-branch t t.ts)
3403+ %'?-' (read-branch fin t t.ts)
3253 :: +read-call: operand { operand }; one operand alone is itself
3406 :: +read-call: operand { operand }; one operand alone is itself
@@ -3462,9 +3615,9 @@
3462 (unclosed par ")" after)
3615 (unclosed par ")" after)
3463 ;< [els=(list expr) after=(list token)] then (read-operands ts)
3616 ;< [els=(list expr) after=(list token)] then (read-operands ts)
3464 ?: ?=([[* * %indent] *] after)
3617 ?: ?=([[* * %indent] *] after)
3465− ;< [ls=(list item) more=(list token)] then
3618+ ;< [ls=(list slot) more=(list token)] then
3466 (read-lines %group t.after)
3619 (read-lines %group t.after)
3467− =/ inner=expr (call-of (weld els (turn ls |=(i=item val.i))))
3620+ =/ inner=expr (call-of (weld els (turn ls |=(i=slot val.i))))
3468 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
3621 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
3470 ?: ?=([[* * ?(%newline %dedent)] *] after)
3623 ?: ?=([[* * ?(%newline %dedent)] *] after)
@@ -3489,7 +3642,7 @@
3490 ^- (pare expr)
3643 ^- (pare expr)
3491 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3644 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3492− =| its=(list item)
3645+ =| its=(list slot)
3493 |- ^- (pare expr)
3646 |- ^- (pare expr)
3494 ?~ ts (bad ts "an item")
3647 ?~ ts (bad ts "an item")
3495 =* t i.ts
3648 =* t i.ts
@@ -3497,8 +3650,8 @@
3497 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
3650 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
3498 ?: (is-closer t) (unclosed op (trip close) ts)
3651 ?: (is-closer t) (unclosed op (trip close) ts)
3499 ?: ?=(%indent lex.t)
3652 ?: ?=(%indent lex.t)
3500− ;< [ls=(list item) more=(list token)] then (read-lines kind t.ts)
3653+ ;< [ls=(list slot) more=(list token)] then (read-lines kind t.ts)
3501− =/ every=(list item) (weld (flop its) ls)
3654+ =/ every=(list slot) (weld (flop its) ls)
3502 =/ fin=loc ?~(every end.at.op end.at:(rear every))
3655 =/ fin=loc ?~(every end.at.op end.at:(rear every))
3503 [%& (bracket-node kind op target every fin) more]
3656 [%& (bracket-node kind op target every fin) more]
3504 ?: &(?=(^ its) (shut op `at.i.its ts))
3657 ?: &(?=(^ its) (shut op `at.i.its ts))
@@ -3506,21 +3659,21 @@
3506 ?: ?=(?(%newline %dedent) lex.t)
3659 ?: ?=(?(%newline %dedent) lex.t)
3507 (unclosed-open op (trip close) "an item" ts)
3660 (unclosed-open op (trip close) "an item" ts)
3508 ?: &(tight.t ?=(^ its)) (no-space ts)
3661 ?: &(tight.t ?=(^ its)) (no-space ts)
3509− ;< [i=item more=(list token)] then (read-item kind ts)
3662+ ;< [i=slot more=(list token)] then (read-item kind ts)
3510 $(its [i its], ts more)
3663 $(its [i its], ts more)
3512 :: +read-item: [ name= ] operand; a tuple's item may be named, a
3665 :: +read-item: [ name= ] operand; a tuple's item may be named, a
3513− :: change's must be, a list's is not
3666+ :: change's must be, by a name or a wing, a list's is not
3515 ++ read-item
3668 ++ read-item
3516 |= [kind=?(%tuple %list %change) ts=(list token)]
3669 |= [kind=?(%tuple %list %change) ts=(list token)]
3517− ^- (pare item)
3670+ ^- (pare slot)
3518− ?: &(!?=(%list kind) ?=([[* * [%name *]] [* %& %'='] *] ts))
3671+ ?: &(?=([* * *] ts) (named-item kind ts))
3519 =* nam i.ts
3672 =* nam i.ts
3520 =/ rest=(list token) t.t.ts
3673 =/ rest=(list token) t.t.ts
3521 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3674 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3522 ;< [v=expr after=(list token)] then (read-operand rest)
3675 ;< [v=expr after=(list token)] then (read-operand rest)
3523− [%& [[beg.at.nam end:(span-of v)] `p.lex.nam v] after]
3676+ [%& [[beg.at.nam end:(span-of v)] (names-of lex.nam) v] after]
3524 ?: ?=(%change kind) (unnamed ts)
3677 ?: ?=(%change kind) (unnamed ts)
3525 ?: &(?=(^ ts) (is-rune i.ts))
3678 ?: &(?=(^ ts) (is-rune i.ts))
3526 %: bad-in-why ts "an expression" operand-mask
3679 %: bad-in-why ts "an expression" operand-mask
@@ -3529,15 +3682,25 @@
3529 ;< [v=expr after=(list token)] then (read-operand ts)
3682 ;< [v=expr after=(list token)] then (read-operand ts)
3530 [%& [(span-of v) ~ v] after]
3683 [%& [(span-of v) ~ v] after]
3685+ :: +named-item: whether ts begins an item's or a line's name=: a
3686+ :: tuple's or a change's name, or a change's wing, then = tight
3689+ |= [kind=?(%tuple %list %change %group) ts=(list token)]
3691+ ?. ?=([* [* %& %'='] *] ts) |
3692+ ?: ?=([[* * [%name *]] *] ts) ?=(?(%tuple %change) kind)
3693+ &(?=(%change kind) ?=([[* * [%wing *]] *] ts))
3532 :: +read-lines: after an open bracket's INDENT, its lines, an item
3695 :: +read-lines: after an open bracket's INDENT, its lines, an item
3533 :: each, to its DEDENT
3696 :: each, to its DEDENT
3535 ++ read-lines
3698 ++ read-lines
3536 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3699 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3537− ^- (pare (list item))
3700+ ^- (pare (list slot))
3538− =| ls=(list item)
3701+ =| ls=(list slot)
3539− |- ^- (pare (list item))
3702+ |- ^- (pare (list slot))
3540− ;< [l=item after=(list token)] then (read-line kind ts)
3703+ ;< [l=slot after=(list token)] then (read-line kind ts)
3541 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
3704 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
3542 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
3705 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
3543 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
3706 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
@@ -3564,22 +3727,20 @@
3564 "its items end at the first line that isn't deeper"
3727 "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
3729 :: +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
3730+ :: be named, a change's must be, by a name or a wing, a list's and a
3568− :: (doc question)
3731+ :: group's are not (doc question)
3570 ++ read-line
3733 ++ read-line
3571 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3734 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3572− ^- (pare item)
3735+ ^- (pare slot)
3573 =/ cf (closer-first ts "an item")
3736 =/ cf (closer-first ts "an item")
3574 ?^ cf u.cf
3737 ?^ cf u.cf
3575− ?: ?& ?=(?(%tuple %change) kind)
3738+ ?: &(?=([* * *] ts) (named-item kind ts))
3576− ?=([[* * [%name *]] [* %& %'='] *] ts)
3578 =* nam i.ts
3739 =* nam i.ts
3579 =/ rest=(list token) t.t.ts
3740 =/ rest=(list token) t.t.ts
3580 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3741 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
3581 ;< [v=expr after=(list token)] then (read-expr rest)
3742 ;< [v=expr after=(list token)] then (read-expr rest)
3582− [%& [[beg.at.nam end:(span-of v)] `p.lex.nam v] after]
3743+ [%& [[beg.at.nam end:(span-of v)] (names-of lex.nam) v] after]
3583 ?: ?=(%change kind) (unnamed ts)
3744 ?: ?=(%change kind) (unnamed ts)
3584 ;< [v=expr after=(list token)] then (read-expr ts)
3745 ;< [v=expr after=(list token)] then (read-expr ts)
3585 [%& [(span-of v) ~ v] after]
3746 [%& [(span-of v) ~ v] after]
@@ -3616,10 +3777,11 @@
3616 %^ bad-why more (closing op ")")
3777 %^ bad-why more (closing op ")")
3617 "the wide gate's body is one operand, so a call goes in parentheses"
3778 "the wide gate's body is one operand, so a call goes in parentheses"
3619− :: +read-gate: |= sample, then an expression or a body
3780+ :: +read-gate: |= sample, then an expression or a body; fin as for
3621 ++ read-gate
3783 ++ read-gate
3622− |= [bar=token ts=(list token)]
3784+ |= [fin=? bar=token ts=(list token)]
3623 ^- (pare expr)
3785 ^- (pare expr)
3624 ?: &(?=(^ ts) tight.i.ts)
3786 ?: &(?=(^ ts) tight.i.ts)
3625 :: a % could begin a constructor's term, as |=%got
3787 :: a % could begin a constructor's term, as |=%got
@@ -3631,13 +3793,14 @@
3631 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3793 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3632 ?^ dm u.dm
3794 ?^ dm u.dm
3633 ;< [e=expr more=(list token)] then
3795 ;< [e=expr more=(list token)] then
3634− (read-expr-or-body "the sample" after)
3796+ (read-expr-or-body fin "the sample" after)
3635 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
3797 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
3637− :: +read-cast: ^- mold, then an expression or a body
3799+ :: +read-cast: ^- mold, then an expression or a body; fin as for
3639 ++ read-cast
3802 ++ read-cast
3640− |= [ket=token ts=(list token)]
3803+ |= [fin=? ket=token ts=(list token)]
3641 ^- (pare expr)
3804 ^- (pare expr)
3642 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
3805 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
3643 ;< [s=shape after=(list token)] then (read-mold ts)
3806 ;< [s=shape after=(list token)] then (read-mold ts)
@@ -3646,41 +3809,65 @@
3646 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3809 =/ dm (doomed ts after "an expression, or a body on deeper lines")
3647 ?^ dm u.dm
3810 ?^ dm u.dm
3648 ;< [e=expr more=(list token)] then
3811 ;< [e=expr more=(list token)] then
3649− (read-expr-or-body "the mold" after)
3812+ (read-expr-or-body fin "the mold" after)
3650 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
3813 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
3652− :: +read-trace: ~& expr, then its body below
3815+ :: +read-trace: ~& expr, then its body below, or, on a body's final
3816+ :: line (fin, +read-last), the rest of the body
3654 ++ read-trace
3818 ++ read-trace
3655− |= [sig=token ts=(list token)]
3819+ |= [fin=? sig=token ts=(list token)]
3656 ^- (pare expr)
3820 ^- (pare expr)
3657 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
3821 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
3658 ;< [v=expr after=(list token)] then (read-expr ts)
3822 ;< [v=expr after=(list token)] then (read-expr ts)
3659− ?. ?=([[* * %indent] *] after)
3660− =/ dm (doomed ts after "`~&`'s body on deeper lines")
3823+ =/ dm (doomed ts after "`~&`'s body on deeper lines")
3661− ?^ dm u.dm
3824+ ?^ dm u.dm
3825+ ;< [b=expr more=(list token)] then
3826+ ?: ?=([[* * %indent] *] after) (read-body t.after)
3827+ ?: &(fin ?=([[* * %newline] *] after)) (read-rest t.after)
3662 (bad after "`~&`'s body on deeper lines")
3828 (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]
3829 [%& [%trace [beg.at.sig end:(span-of b)] v b] more]
3666− :: +read-branch: ?- expr, then its arms below, one per line
3831+ :: +read-branch: ?- expr, then its arms below, one per line; or, when
3832+ :: it begins a body's final line (fin, +read-last), at its own depth
3833+ :: to the end of the body, whose DEDENT it leaves (+read-rest)
3668 ++ read-branch
3835 ++ read-branch
3669− |= [wut=token ts=(list token)]
3836+ |= [fin=? wut=token ts=(list token)]
3670 ^- (pare expr)
3837 ^- (pare expr)
3671 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
3838 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
3672 ;< [s=expr after=(list token)] then (read-expr ts)
3839 ;< [s=expr after=(list token)] then (read-expr ts)
3673− ?. ?=([[* * %indent] *] after)
3674− =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3840+ =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3675− ?^ dm u.dm
3841+ ?^ dm u.dm
3842+ ?. ?=([[* * ?(%indent %newline)] *] after)
3676 (bad after "`?-`'s arms on deeper lines")
3843 (bad after "`?-`'s arms on deeper lines")
3844+ =/ flat=? ?=(%newline lex.i.after)
3845+ ?: &(flat !fin) (bad after "`?-`'s arms on deeper lines")
3677 =| arms=(list arm)
3846 =| arms=(list arm)
3678 =/ rest=(list token) t.after
3847 =/ rest=(list token) t.after
3679 |- ^- (pare expr)
3848 |- ^- (pare expr)
3680− ;< [a=arm more=(list token)] then (read-arm rest)
3849+ ;< [a=arm more=(list token)] then
3850+ ?:(flat (read-flat-arm rest) (read-arm rest))
3681 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
3851 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
3682 ?. ?=([[* * %dedent] *] more) (bad-end-in more (tail-can val.a))
3852 ?. ?=([[* * %dedent] *] more) (bad-end-in more (tail-can val.a))
3683− [%& [%branch [beg.at.wut end.at.a] s (flop [a arms])] t.more]
3853+ =/ at=span [beg.at.wut end.at.a]
3854+ [%& [%branch at s (flop [a arms])] ?:(flat more t.more)]
3856+ :: +read-flat-arm: +read-arm at its ?-'s depth, where a line that
3857+ :: could begin the body's other lines gets a hint
3862+ ?: ?=([[* * ?(%'++' %'+$')] *] ts)
3863+ %: bad-in-why ts "a pattern" pattern-mask
3864+ "a body's local definitions come before its final expression"
3866+ ?: ?=([[* * ?(%'~&' %'^-')] *] ts)
3867+ %: bad-in-why ts "a pattern" pattern-mask
3868+ "a trace or cast goes in the arm's body"
3685 :: +read-arm: a pattern, then an expression or a body
3872 :: +read-arm: a pattern, then an expression or a body
@@ -3695,7 +3882,7 @@
3695 %^ bad-why after "a space after the pattern"
3882 %^ bad-why after "a space after the pattern"
3696 "patterns take no `name=`: a bare name binds, as [a b]"
3883 "patterns take no `name=`: a bare name binds, as [a b]"
3697 ;< [e=expr more=(list token)] then
3884 ;< [e=expr more=(list token)] then
3698− (read-expr-or-body "the pattern" after)
3885+ (read-expr-or-body | "the pattern" after)
3699 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
3886 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
3701 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
3888 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
@@ -4437,7 +4624,7 @@
4437++ outline-edit
4624++ outline-edit
4438 |= e=edit
4625 |= e=edit
4439 ^- outline
4626 ^- outline
4440− [%edit at.e ~[%name] %kid ~[(outline-expr val.e)]]
4627+ [%edit at.e ~[%name %wing] %kid ~[(outline-expr val.e)]]
4442++ outline-arm
4629++ outline-arm
4443 |= a=arm
4630 |= a=arm
@@ -4637,6 +4824,14 @@
4637:: proofs to fewer than 1,024 cells; the projection planner has a separate
4824:: proofs to fewer than 1,024 cells; the projection planner has a separate
4638:: 4,096-step bound. These are inference limits, not language limits.
4825:: 4,096-step bound. These are inference limits, not language limits.
4827+:: `unface` is reserved with proj (+reserved-name) and is also handled by
4828+:: type: (unface e) has e's type with every face removed, through cells,
4829+:: gates and collection arguments, keeping unions and recursive molds
4830+:: whole (+itype-unface). It is not a value, it takes one argument, and
4831+:: a bare type variable is unsupported, as field access on one is. A ++
4832+:: whose body is (unface |= …) is a gate for recursion (+unfaced-gate).
4833+:: It lowers to its argument; no lowering is implemented yet.
4640:: Supported API imports derive request-gate types atomically for multiple
4835:: Supported API imports derive request-gate types atomically for multiple
4641:: paths, including one typed segment or one diff fold per case. Their checked
4836:: paths, including one typed segment or one diff fold per case. Their checked
4642:: ordinary definitions, mark molds and supported poke constructor are also
4837:: ordinary definitions, mark molds and supported poke constructor are also
@@ -4944,6 +5139,35 @@
4944 $(a tal.a, b tal.b, sub u.first)
5139 $(a tal.a, b tal.b, sub u.first)
5142+:: +itype-unface: t with every face removed, for (unface e)
5144+:: It strips through cells, through a gate's sample and product and
5145+:: through a built-in collection's arguments, the prelude's unit
5146+:: included, walking bound variables. Other unions and recursive
5147+:: molds are compared by name or by their exact cases, so stripping
5148+:: inside them would stop them from fitting their own name: they are
5149+:: kept whole. An unbound variable stays, so faces it is bound to
5150+:: later are kept. The unit keeps its own u=, as a list keeps i= and
5154+ |= [t=itype sub=isub]
5156+ =. t (itype-walk t sub)
5159+ %cell [%cell $(t hed.t) $(t tal.t)]
5160+ %fn [%fn $(t sample.t) $(t product.t)]
5161+ %collection [%collection name.t (turn args.t |=(a=itype ^$(t a)))]
5163+ ?. =(origin.t `[/lib/jibb/prelude/jibb %unit]) t
5164+ ?. ?=([* ~] args.t) t
5165+ =/ nil=itype [%const [%null %n 0 '~']]
5166+ ?. =(cases.t ~[nil [%cell nil [%face %u i.args.t]]]) t
5167+ =/ arg=itype $(t i.args.t)
5168+ t(cases ~[nil [%cell nil [%face %u arg]]], args ~[arg])
4947+$ igf-form [typ=itype sub=isub left=@ud]
5171+$ igf-form [typ=itype sub=isub left=@ud]
4948+$ igf-forms [types=(list itype) sub=isub left=@ud]
5172+$ igf-forms [types=(list itype) sub=isub left=@ud]
4949++ itype-gate-free-forms
5173++ itype-gate-free-forms
@@ -6375,15 +6599,67 @@
6376 (itype-var-is-gate-free-fuel n t 256)
6600 (itype-var-is-gate-free-fuel n t 256)
6602+:: +named-var: the ID of the nth type variable, written as name
6604+:: An ID counts in its low 64 bits. The name a variable was written
6605+:: with, as Msg, sits above them, or 0 for none, so the name travels
6606+:: with the variable through substitution, generalization and
6607+:: instantiation, and the printer can show it (+show-var). No two
6608+:: IDs share a count, so a name never makes two variables one.
6613+ (add (lsh 6 name) (end 6 n))
6615+:: +var-name: the name in a type variable's ID, or 0 for none
6622+:: +var-count: a type variable's ID without its name
6629+:: +canonical-itype: t with the variables in vars renumbered to print
6631+:: A variable keeps its name unless one before it in vars has the same
6632+:: name. The others take numbers from 0, skipping any whose letter
6633+:: (+show-var) is a name in vars, so a printed type never shows one
6634+:: name for two variables.
6378++ canonical-itype
6636++ canonical-itype
6379 |= [t=itype vars=(list @ud)]
6637 |= [t=itype vars=(list @ud)]
6380 ^- itype
6638 ^- itype
6639+ =/ names=(list @t) (turn vars var-name)
6640+ =/ used=(list @t) ~
6381 =/ ren=isub ~
6641 =/ ren=isub ~
6382 =/ n=@ud 0
6642 =/ n=@ud 0
6384 ?~ vars (itype-rename t ren)
6644 ?~ vars (itype-rename t ren)
6645+ =/ name=@t (var-name i.vars)
6646+ =/ own=? &(!=(0 name) !(lien used |=(u=@t =(u name))))
6647+ =? n !own (letter-free n names)
6648+ =/ id=@ud ?:(own (named-var name 0) n)
6385− =/ 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])))
6649+ =/ 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])))
6386− $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
6650+ $(vars t.vars, ren [[i.vars replacement] ren], n ?:(own n +(n)), used ?:(own [name used] used))
6652+:: +letter-free: the first number from n whose letter is none of names
6655+ |= [n=@ud names=(list @t)]
6657+ ?. (lien names |=(m=@t =(m (crip (show-var n))))) n
6660+:: +instantiate-scheme: a scheme's type with fresh quantified variables
6662+:: Each fresh variable keeps the name of the one it replaces.
6388++ instantiate-scheme
6664++ instantiate-scheme
6389 |= [scheme=ischeme state=istate]
6665 |= [scheme=ischeme state=istate]
@@ -6392,12 +6668,13 @@
6392 =/ vars=(list @ud) vars.scheme
6668 =/ vars=(list @ud) vars.scheme
6394 ?~ vars [(itype-rename typ.scheme ren) state]
6670 ?~ vars [(itype-rename typ.scheme ren) state]
6671+ =/ fresh=@ud (named-var (var-name i.vars) next.state)
6395 =/ replacement=itype
6672 =/ replacement=itype
6396− ?:((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])))
6673+ ?:((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])))
6397 :: A generalized atom variable is a valid origin for re-generalizing
6674 :: A generalized atom variable is a valid origin for re-generalizing
6398 :: an alias, just as a sample binder is.
6675 :: an alias, just as a sample binder is.
6399 =/ st=istate state(next +(next.state))
6676 =/ st=istate state(next +(next.state))
6400− =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
6677+ =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [fresh binders.state]
6401 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6678 $(vars t.vars, ren [[i.vars replacement] ren], state st)
6403++ icap-lookup
6680++ icap-lookup
@@ -7257,7 +7534,8 @@
7257 ?: in-mold.state ~
7534 ?: in-mold.state ~
7258 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
7535 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
7259 ?^ n `[[%var u.n] state]
7536 ?^ n `[[%var u.n] state]
7537+ =/ id=@ud (named-var name.sh next.state)
7260− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
7538+ `[[%var id] state(next +(next.state), caps [[name.sh id at.sh] caps.state])]
@@ -7290,12 +7568,12 @@
7290 ^- isample-result
7568 ^- isample-result
7293− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7571+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7294 [%| "sample shadows a name"]
7572 [%| "sample shadows a name"]
7295 =/ t=itype [%var next.state]
7573 =/ t=itype [%var next.state]
7296 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
7574 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
7298− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7576+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))
7299 [%| "sample shadows a name"]
7577 [%| "sample shadows a name"]
7300 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
7578 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
7301 ?~ t [%| "sample mold is not supported by partial inference"]
7579 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -7363,7 +7641,7 @@
7365 ?: ?=(%mold -.i.ds) $(ds t.ds)
7643 ?: ?=(%mold -.i.ds) $(ds t.ds)
7366− ?: =(name.i.ds %proj) |
7644+ ?: (reserved-name name.i.ds) |
7367 ?. (unique-value-name name.i.ds names) |
7645 ?. (unique-value-name name.i.ds names) |
7368 ?: ?=(^ (ienv-lookup name.i.ds env)) |
7646 ?: ?=(^ (ienv-lookup name.i.ds env)) |
7369 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
7647 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -7387,7 +7665,7 @@
7388 ?~ locals &
7666 ?~ locals &
7389 =/ n=term name.i.locals
7667 =/ n=term name.i.locals
7390− ?: =(n %proj) |
7668+ ?: (reserved-name n) |
7391 ?. (unique-value-name n names) |
7669 ?. (unique-value-name n names) |
7392 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
7670 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
7393 ?: (lien marks.state |=(m=term =(n m))) |
7671 ?: (lien marks.state |=(m=term =(n m))) |
@@ -7537,7 +7815,8 @@
7537 ^- istate
7815 ^- istate
7538 ?~ sites state
7816 ?~ sites state
7539 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7817 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7818+ =/ id=@ud (named-var name.i.sites next.state)
7540− $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
7819+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites id at.i.sites] caps.state]))
7542++ reserve-def-caps
7821++ reserve-def-caps
7543 |= [e=expr state=istate]
7822 |= [e=expr state=istate]
@@ -7711,7 +7990,8 @@
7711 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7990 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
7712 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7991 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
7713 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7992 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7993+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.inferred sub.state.p.inferred)
7714− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
7994+ $(ds t.ds, env [[name.d named] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
7716:: Try complete cyclic local groups after individual definitions stall.
7996:: Try complete cyclic local groups after individual definitions stall.
7717:: Components with non-gates or unresolved constraints stay unavailable.
7997:: Components with non-gates or unresolved constraints stay unavailable.
@@ -8065,7 +8345,7 @@
8065 [%| ["list branch pattern is not supported by partial inference" ~]]
8345 [%| ["list branch pattern is not supported by partial inference" ~]]
8066 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
8346 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
8067 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
8347 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
8068− ?: |(=(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)))))
8348+ ?: |((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)))))
8069 [%| ["pattern binder shadows a name" ~]]
8349 [%| ["pattern binder shadows a name" ~]]
8070 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
8350 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
8071 =/ left=iresult
8351 =/ left=iresult
@@ -8102,7 +8382,7 @@
8102 [%| ["unit branch pattern is not supported by partial inference" ~]]
8382 [%| ["unit branch pattern is not supported by partial inference" ~]]
8103 =/ binder=(unit term) ?:(first-empty second-name first-name)
8383 =/ binder=(unit term) ?:(first-empty second-name first-name)
8104 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
8384 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
8105− ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
8385+ ?: |((reserved-name u.binder) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))
8106 [%| ["pattern binder shadows a name" ~]]
8386 [%| ["pattern binder shadows a name" ~]]
8107 =/ payload=(unit itype) (unit-union-payload typ)
8387 =/ payload=(unit itype) (unit-union-payload typ)
8108 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
8388 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -8209,7 +8489,7 @@
8209 ^- (unit ienv)
8489 ^- (unit ienv)
8210 =. t ?:(?=(%face -.t) body.t t)
8490 =. t ?:(?=(%face -.t) body.t t)
8211 ?: ?=(%bind -.p)
8491 ?: ?=(%bind -.p)
8212− ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
8492+ ?: |((reserved-name name.p) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~
8213 `[[name.p [t ~]] env]
8493 `[[name.p [t ~]] env]
8214 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
8494 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
@@ -8735,7 +9015,9 @@
8735 `subject
9015 `subject
8737:: Infer changes only against a fully known record spine. Retain the
9017:: Infer changes only against a fully known record spine. Retain the
8738−:: target type; unknown spines and repeated edits remain unsupported.
9018+:: target type; unknown spines and overlapping edits remain unsupported.
9019+:: An edit's wing, as open.cart, reads through record fields only,
9020+:: outermost first, and its value fits the field it names.
8739++ change-spine-known
9021++ change-spine-known
8740 |= [t=itype sub=isub]
9022 |= [t=itype sub=isub]
@@ -8747,19 +9029,18 @@
8747 $(t tal.t)
9029 $(t tal.t)
8749++ infer-change-edits
9031++ infer-change-edits
8750− |= [edits=(list edit) target=itype env=ienv state=istate seen=(list term)]
9032+ |= [edits=(list edit) target=itype env=ienv state=istate seen=(list (list term))]
8751 ^- iresult
9033 ^- iresult
8752 ?~ edits [%& target state]
9034 ?~ edits [%& target state]
8753 =/ entry=edit i.edits
9035 =/ entry=edit i.edits
8754− ?: (lien seen |=(name=term =(name name.entry)))
9036+ =/ outer=(list term) (flop names.entry)
9037+ ?: (lien seen |=(prior=(list term) (wing-overlap prior outer)))
8755 [%| ["repeated change fields are not supported by partial inference" ~]]
9038 [%| ["repeated change fields are not supported by partial inference" ~]]
8756 ?. (change-spine-known target sub.state)
9039 ?. (change-spine-known target sub.state)
8757 [%| ["change target needs a known record in partial inference" ~]]
9040 [%| ["change target needs a known record in partial inference" ~]]
8758− =/ found=(list itype) (record-fields-named name.entry target sub.state)
9041+ =/ field=(each itype idiag) (change-wing-field entry target sub.state)
8759− ?~ found
9042+ ?: ?=(%| -.field) [%| p.field]
8760− [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
8761− ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
8762− =/ expected=itype i.found
9043+ =/ expected=itype p.field
8763 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
9044 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
8764 ?: ?=(%| -.value) value
9045 ?: ?=(%| -.value) value
8765 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
9046 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
@@ -8768,7 +9049,67 @@
8768 =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
9049 =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
8769 ?^ decimal [%| u.decimal]
9050 ?^ decimal [%| u.decimal]
8770 [%| ["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)]]]]
9051 [%| ["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)]]]]
8771− $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
9052+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [outer seen])
9054+:: +change-wing-field: the type of the field an edit's wing names in
9055+:: a known record target, read through record fields, outermost first
9057+++ change-wing-field
9058+ |= [entry=edit target=itype sub=isub]
9059+ ^- (each itype idiag)
9060+ =/ outer=(list term) (flop names.entry)
9061+ =/ k=@ud (lent names.entry)
9062+ =/ typ=itype target
9063+ =| through=(unit [name=term at=span])
9064+ |- ^- (each itype idiag)
9066+ =/ here=span (edit-name-at entry (dec k))
9067+ ?: &(?=(^ through) !(change-spine-known typ sub))
9068+ ?. (itype-not-record typ sub)
9069+ [%| ["change wing needs a known record in partial inference" ~]]
9070+ =/ label=tape "field `{(trip name.u.through)}`"
9072+ :- "change wing `{(show-names names.entry)}` goes through `{(trip name.u.through)}`, which is not a record"
9073+ ~[[at.u.through (site-type-note label typ sub)]]
9074+ =/ found=(list itype) (record-fields-named i.outer typ sub)
9076+ [%| ["record has no field `{(trip i.outer)}`" ~[[here "unknown field"]]]]
9077+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
9078+ $(outer t.outer, k (dec k), typ i.found, through `[i.outer here])
9080+:: +edit-name-at: where the kth name of an edit's wing is written,
9081+:: counting from 0: its names are joined by dots from the edit's start
9086+ =/ col=@ud col.beg.at.e
9087+ =/ ns=(list term) names.e
9090+ =/ len=@ud (met 3 i.ns)
9091+ ?: =(0 k) [[line.beg.at.e col] [line.beg.at.e (add col len)]]
9092+ $(ns t.ns, k (dec k), col +((add col len)))
9094+:: +itype-not-record: whether a type is surely no record: an atom, a
9095+:: loobean, a list or other collection, a gate, a union or a noun
9098+ |= [t=itype sub=isub]
9100+ =. t (itype-walk t sub)
9101+ ?=(?(%atom %any-atom %flag %const %tag %collection %fn %union %noun %empty) -.t)
9103+:: +wing-overlap: whether two edits' wings, outermost first, name the
9104+:: same field or one a field inside the other's
9107+ |= [a=(list term) b=(list term)]
8773:: Backtick constructs the canonical prelude unit, after checking its
9114:: Backtick constructs the canonical prelude unit, after checking its
8774:: prepared template has the standard null and [~ u=A] cases.
9115:: prepared template has the standard null and [~ u=A] cases.
@@ -9138,6 +9479,7 @@
9138 [%& typ.instance state.instance]
9479 [%& typ.instance state.instance]
9139 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
9480 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
9140 ?~ scheme
9481 ?~ scheme
9482+ ?: =(i.names.e %unface) [%| (unface-value at.e)]
9141 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
9483 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
9142 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
9484 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
9143 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
9485 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
@@ -9145,7 +9487,10 @@
9145 [%& typ.inst state.inst]
9487 [%& typ.inst state.inst]
9146 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
9488 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
9147 [%& typ.instance state.instance]
9489 [%& typ.instance state.instance]
9491+ ?: &(?=(%wing -.inner.e) =(names.inner.e ~[%unface]) ?=(~ (ienv-lookup %unface env)))
9492+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
9148− %group $(e inner.e)
9493+ $(e inner.e)
9150 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
9495 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
9151 =/ target=iresult $(e [%wing at.e target.e])
9496 =/ target=iresult $(e [%wing at.e target.e])
@@ -9289,6 +9634,7 @@
9289 ?~ args.e [%| ["call has no argument" ~]]
9634 ?~ args.e [%| ["call has no argument" ~]]
9290 ?: (explicit-proj-call e env state)
9635 ?: (explicit-proj-call e env state)
9291 [%| ["proj needs an expected record type" ~]]
9636 [%| ["proj needs an expected record type" ~]]
9637+ ?: (reserved-call %unface e env state) (infer-unface e env state)
9292 (infer-call-with-head e env state (infer-fragment head.e env state))
9638 (infer-call-with-head e env state (infer-fragment head.e env state))
9293 * [%| ["expression is not supported by partial inference" ~]]
9639 * [%| ["expression is not supported by partial inference" ~]]
@@ -9679,6 +10025,7 @@
9679 ^- iresult
10025 ^- iresult
9680 ?> ?=(%call -.e)
10026 ?> ?=(%call -.e)
9681 ?~ args.e [%| ["call has no argument" ~]]
10027 ?~ args.e [%| ["call has no argument" ~]]
10028+ ?: (reserved-call %unface e env state) (infer-unface e env state)
9682 =/ head=iresult (infer-fragment head.e env state)
10029 =/ head=iresult (infer-fragment head.e env state)
9683 ?: ?=(%| -.head) head
10030 ?: ?=(%| -.head) head
9684 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
10031 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
@@ -9761,18 +10108,70 @@
9761 `(infer-simple-items items.e env state)
10108 `(infer-simple-items items.e env state)
9762 `(width-infer-items items.e index.u.target env state context)
10109 `(width-infer-items items.e index.u.target env state context)
10111+:: +reserved-call: whether e calls the reserved operation n
9764−:: Experimental intrinsic recognition; real bindings retain normal calls.
10113+:: Experimental intrinsic recognition; real bindings retain normal calls.
10115+ |= [n=term e=expr env=ienv state=istate]
10117+ ?. ?=(%call -.e) |
10118+ ?. ?=(%wing -.head.e) |
10119+ ?. =(names.head.e ~[n]) |
10120+ ?: ?=(^ (ienv-lookup n env)) |
10121+ ?: (lien globals.state |=(x=term =(x n))) |
10122+ ?~ prelude.state &
10123+ ?:(?=(^ (ienv-lookup n values.u.prelude.state)) | &)
9765++ explicit-proj-call
10124++ explicit-proj-call
9766 |= [e=expr env=ienv state=istate]
10125 |= [e=expr env=ienv state=istate]
9768 ?. ?=(%call -.e) |
10127 ?. ?=(%call -.e) |
9769 ?. ?=([* ~] args.e) |
10128 ?. ?=([* ~] args.e) |
9770− ?. ?=(%wing -.head.e) |
10129+ (reserved-call %proj e env state)
9771− ?. =(names.head.e ~[%proj]) |
10130+::
9772− ?: ?=(^ (ienv-lookup %proj env)) |
10131+:: +infer-unface: (unface e), e's type with every face removed
9773− ?: (lien globals.state |=(n=term =(n %proj))) |
10132+::
9774− ?~ prelude.state &
10133+:: A reserved operation handled by type, like proj. Any number of
9775− ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
10134+:: arguments is taken here so that a wrong count is an error. A type
10135+:: not yet known would wait, as wing access does; the partial checker
10136+:: has no such wait and reports it as unsupported, as it does field
10137+:: access on such a type.
10139+ |= [e=expr env=ienv state=istate]
10142+ ?. ?=([* ~] args.e)
10143+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
10144+ ?^ defer.state [%| ["deferred unface needs unsupported inference" ~]]
10145+ =/ value=iresult (infer-fragment i.args.e env state)
10146+ ?: ?=(%| -.value) value
10147+ =/ typ=itype (itype-walk typ.p.value sub.state.p.value)
10148+ ?: ?=(?(%var %fvar) -.typ)
10149+ [%| ["unface on a type not yet known is not supported by partial inference" ~]]
10150+ [%& (itype-unface typ sub.state.p.value) state.p.value]
10152+:: +unface-value: the error for unface written where a value goes
10157+ ["unface is not a value; write |=(g (unface g))" ~[[at "unface used as a value"]]]
10159+:: +unfaced-gate: the gate under a ++'s (unface |= …), or ~
10161+:: Such a ++ is a gate for recursion: its own name has the unfaced
10162+:: type, and its body may call it.
10164+ |= [e=expr env=ienv state=istate]
10166+ ?: ?=(%group -.e) $(e inner.e)
10167+ ?. (reserved-call %unface e env state) ~
10169+ ?. ?=([* ~] args.e) ~
10170+ =/ gate=expr i.args.e
10172+ ?: ?=(%group -.gate) $(gate inner.gate)
10173+ ?. ?=(?(%gate %gate-wide) -.gate) ~
9776++ infer-proj-source
10175++ infer-proj-source
9777 |= [e=expr expected=itype env=ienv state=istate context=span]
10176 |= [e=expr expected=itype env=ienv state=istate context=span]
9778 ^- iresult
10177 ^- iresult
@@ -10179,7 +10578,7 @@
10179 ?~ pats [%& ~]
10578 ?~ pats [%& ~]
10180 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
10579 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
10181 =/ name=term name.i.pats
10580 =/ name=term name.i.pats
10182− ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
10581+ ?: |((reserved-name name) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))
10183 [%| 'pattern shadows a name']
10582 [%| 'pattern shadows a name']
10184 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
10583 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
10185 ?: ?=(%| -.rest) rest
10584 ?: ?=(%| -.rest) rest
@@ -10256,24 +10655,12 @@
10256 ^- tape
10655 ^- tape
10257 =. t (itype-walk t sub)
10656 =. t (itype-walk t sub)
10259− %var
10658+ %var (show-var id.t)
10260− ?: (lth id.t 26) [(add 65 id.t) ~]
10262− %fvar
10659+ %fvar (show-var id.t)
10263− ?: (lth id.t 26) [(add 65 id.t) ~]
10265− %avar
10660+ %avar (show-var id.t)
10266− ?: (lth id.t 26) [(add 65 id.t) ~]
10268− %rvar
10661+ %rvar (show-var id.t)
10269− ?: (lth id.t 26) [(add 65 id.t) ~]
10271− %nvar
10662+ %nvar (show-var id.t)
10272− ?: (lth id.t 26) [(add 65 id.t) ~]
10274− %rnvar
10663+ %rnvar (show-var id.t)
10275− ?: (lth id.t 26) [(add 65 id.t) ~]
10277 %atom "@{(trip aura.t)}"
10664 %atom "@{(trip aura.t)}"
10278 %any-atom "@"
10665 %any-atom "@"
10279 %flag "?"
10666 %flag "?"
@@ -10294,6 +10681,17 @@
10294 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
10681 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
10684+:: +show-var: a type variable as printed: its name if it has one, else
10685+:: a letter for its number, A to Z, then T26, T27 and on
10690+ =/ name=@t (var-name id)
10691+ ?. =(0 name) (trip name)
10692+ ?: (lth id 26) [(add 65 id) ~]
10297++ show-itype-item
10695++ show-itype-item
10298 |= [t=itype sub=isub]
10696 |= [t=itype sub=isub]
10299 ^- tape
10697 ^- tape
@@ -10352,7 +10750,7 @@
10352 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
10750 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
10353 ?: (itype-has-hidden-recursive normalized) label
10751 ?: (itype-has-hidden-recursive normalized) label
10354 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
10752 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
10355− =/ printable=itype (canonical-itype normalized vars)
10753+ =/ printable=itype (canonical-itype (cap-names normalized vars ~ sub))
10356 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
10754 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
10358:: A capital in a written mold is generalized with its enclosing ++.
10756:: A capital in a written mold is generalized with its enclosing ++.
@@ -10393,6 +10791,116 @@
10393 ?: =(n u.ident) `i.caps
10791 ?: =(n u.ident) `i.caps
10394 $(caps t.caps)
10792 $(caps t.caps)
10794+:: +cap-names: give each variable in vars the name it was written with
10796+:: Unification joins variables, and the one an ID resolves to may not
10797+:: carry the name its definition wrote, as when a capital meets a
10798+:: called gate's variable or an atom variable. Each variable in vars
10799+:: takes the name of the first capital in caps that resolves to it;
10800+:: failing that, of the earliest made of the named variables that
10801+:: resolve to it, itself included (+joined-names). Only the name part
10802+:: of an ID changes, not its count, so IDs stay distinct.
10805+ |= [typ=itype vars=(list @ud) caps=icaps sub=isub]
10806+ ^- [typ=itype vars=(list @ud)]
10807+ =/ written=icaps (flop caps)
10808+ =/ joined=(map @ud @ud) (joined-names sub)
10809+ =/ ren=(map @ud @ud) ~
10810+ =/ out=(list @ud) ~
10812+ ?~ vars [?~(ren typ (itype-reid typ ren)) (flop out)]
10813+ =/ cap=(unit icap) (cap-with-id i.vars written sub)
10814+ =/ first=(unit @ud) (~(get by joined) i.vars)
10817+ ?~ first (var-name i.vars)
10818+ ?: =(0 (var-name i.vars)) (var-name u.first)
10819+ ?: (lth (var-count u.first) (var-count i.vars)) (var-name u.first)
10821+ =/ to=@ud (named-var name i.vars)
10822+ ?: =(to i.vars) $(vars t.vars, out [i.vars out])
10823+ $(vars t.vars, out [to out], ren (~(put by ren) i.vars to))
10825+:: +joined-names: for each variable that named ones resolve to, the
10826+:: earliest made of those, by count
10828+:: One pass over sub keeps each ID's newest binding, as +itype-lookup
10829+:: would find it: the variable it is bound to, or ~ for another type.
10830+:: Each named ID then follows those bindings to the variable it
10831+:: resolves to, if any.
10836+ =/ edges=(map @ud (unit @ud))
10837+ %+ roll (flop sub)
10838+ |= [b=ibinding m=(map @ud (unit @ud))]
10839+ (~(put by m) id.b (var-of val.b))
10840+ =/ named=(list @ud)
10841+ (murn ~(tap by edges) |=([k=@ud *] ?:(=(0 (var-name k)) ~ `k)))
10842+ =/ fuel=@ud ~(wyt by edges)
10843+ =/ out=(map @ud @ud) ~
10846+ =/ root=(unit @ud) (follow-var i.named edges fuel)
10847+ ?~ root $(named t.named)
10848+ ?: =(u.root i.named) $(named t.named)
10849+ =/ best=(unit @ud) (~(get by out) u.root)
10850+ ?: &(?=(^ best) (lth (var-count u.best) (var-count i.named)))
10852+ $(named t.named, out (~(put by out) u.root i.named))
10854+:: +follow-var: the variable that id resolves to through edges, or ~ if
10855+:: it resolves to another type; fuel bounds the steps
10858+ |= [id=@ud edges=(map @ud (unit @ud)) fuel=@ud]
10862+ =/ edge=(unit (unit @ud)) (~(get by edges) id)
10865+ ?: =(u.u.edge id) `id
10866+ $(id u.u.edge, fuel (dec fuel))
10868+:: +var-of: the ID of a type variable node, or ~ for another type
10882+:: +itype-reid: t with the variable IDs in ids replaced, each node
10883+:: keeping its kind
10886+ |= [t=itype ids=(map @ud @ud)]
10889+ %var t(id (fall (~(get by ids) id.t) id.t))
10890+ %fvar t(id (fall (~(get by ids) id.t) id.t))
10891+ %avar t(id (fall (~(get by ids) id.t) id.t))
10892+ %rvar t(id (fall (~(get by ids) id.t) id.t))
10893+ %nvar t(id (fall (~(get by ids) id.t) id.t))
10894+ %rnvar t(id (fall (~(get by ids) id.t) id.t))
10895+ ?(%atom %any-atom %flag %noun %empty %tag %const %recursive %jrec) t
10896+ %union t(cases (turn cases.t |=(c=itype ^$(t c))), args (turn args.t |=(c=itype ^$(t c))))
10897+ %grec t(args (turn args.t |=(c=itype ^$(t c))))
10898+ %collection t(args (turn args.t |=(c=itype ^$(t c))))
10899+ %face t(body $(t body.t))
10900+ %fn t(sample $(t sample.t), product $(t product.t))
10901+ %cell t(hed $(t hed.t), tal $(t tal.t))
10396++ merged-capitals
10904++ merged-capitals
10397 |= [caps=icaps sub=isub]
10905 |= [caps=icaps sub=isub]
10398 ^- (unit [first=icap second=icap])
10906 ^- (unit [first=icap second=icap])
@@ -10612,6 +11120,9 @@
10612 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
11120 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
10613 =. gate-defs.state ~
11121 =. gate-defs.state ~
10614 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
11122 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]
11123+ :: A ++ whose body is (unface |= …) is a gate too, unfaced
11124+ =/ peeled=(unit expr) (unfaced-gate val.d env state)
11125+ =? val.d ?=(^ peeled) u.peeled
10615 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
11126 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
10616 [%| ["recursive definition is not a gate" ~]]
11127 [%| ["recursive definition is not a gate" ~]]
10617 =/ result=(unit itype) (recursive-branch-seed d env state)
11128 =/ result=(unit itype) (recursive-branch-seed d env state)
@@ -10635,6 +11146,7 @@
10635 =/ product=itype ?~(result [%var id] u.result)
11146 =/ product=itype ?~(result [%var id] u.result)
10636 =/ st=istate state.p.sam(next +(id))
11147 =/ st=istate state.p.sam(next +(id))
10637 =/ seed=itype [%fn typ.p.sam product]
11148 =/ seed=itype [%fn typ.p.sam product]
11149+ =? seed ?=(^ peeled) (itype-unface seed sub.st)
10638 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
11150 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
10639 =/ body=expr
11151 =/ body=expr
10640 ?- -.gate
11152 ?- -.gate
@@ -10646,7 +11158,9 @@
10646 ?: ?=(%| -.out) out
11158 ?: ?=(%| -.out) out
10647 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
11159 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
10648 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
11160 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
11161+ =/ typ=itype [%fn typ.p.sam typ.p.out]
11162+ =? typ ?=(^ peeled) (itype-unface typ u.uni)
10649− [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
11163+ [%& typ state.p.out(sub u.uni)]
10651++ dependency-root
11165++ dependency-root
10652 |= names=(list term)
11166 |= names=(list term)
@@ -10754,7 +11268,7 @@
10754:: Infer a cyclic component with one monomorphic seed per gate. All members
11268:: Infer a cyclic component with one monomorphic seed per gate. All members
10755:: must succeed before any scheme is available; pending constraints and
11269:: must succeed before any scheme is available; pending constraints and
10756:: unresolved branch joins remain partial.
11270:: unresolved branch joins remain partial.
10757−+$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]
11271++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps unfaced=?]
10758+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
11272+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
10759++ seed-gate-group
11273++ seed-gate-group
10760 |= [ds=(list def) env=ienv state=istate]
11274 |= [ds=(list def) env=ienv state=istate]
@@ -10762,7 +11276,9 @@
10762 ?~ ds [%& [~ state]]
11276 ?~ ds [%& [~ state]]
10763 =/ d=def i.ds
11277 =/ d=def i.ds
10764 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
11278 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
11279+ :: A ++ whose body is (unface |= …) is a gate too, unfaced
11280+ =/ peeled=(unit expr) (unfaced-gate val.d env state)
10765− =/ gate=expr val.d
11281+ =/ gate=expr ?~(peeled val.d u.peeled)
10766 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
11282 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
10767 [%| ["recursive group contains a non-gate" ~]]
11283 [%| ["recursive group contains a non-gate" ~]]
10768 =/ initial=istate (reserve-def-caps gate state)
11284 =/ initial=istate (reserve-def-caps gate state)
@@ -10780,7 +11296,8 @@
10782 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
11298 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
11299+ =? seed ?=(^ peeled) (itype-unface seed sub.state.p.sam)
10783− =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
11300+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam ?=(^ peeled)]
10784 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
11301 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
10785 =/ rest=igate-seeds $(ds t.ds, state after)
11302 =/ rest=igate-seeds $(ds t.ds, state after)
10786 ?: ?=(%| -.rest) rest
11303 ?: ?=(%| -.rest) rest
@@ -10820,6 +11337,7 @@
10820 ?: (constrained-capitals caps.entry sub.state)
11337 ?: (constrained-capitals caps.entry sub.state)
10821 [%| ["explicit capital constraints are not supported by partial inference" ~]]
11338 [%| ["explicit capital constraints are not supported by partial inference" ~]]
10822 =/ typ=itype (itype-normalize typ.entry sub.state)
11339 =/ typ=itype (itype-normalize typ.entry sub.state)
11340+ =? typ unfaced.entry (itype-unface typ ~)
10823 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
11341 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
10824 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
11342 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
10825 [%| ["recursive group needs unsupported inference" ~]]
11343 [%| ["recursive group needs unsupported inference" ~]]
@@ -10828,7 +11346,7 @@
10828 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
11346 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
10829 =/ rest=(each ienv idiag) $(entries t.entries)
11347 =/ rest=(each ienv idiag) $(entries t.entries)
10830 ?: ?=(%| -.rest) rest
11348 ?: ?=(%| -.rest) rest
10831− [%& [[name.entry [typ vars]] p.rest]]
11349+ [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]
10833++ infer-gate-group
11351++ infer-gate-group
10834 |= [ds=(list def) env=ienv state=istate]
11352 |= [ds=(list def) env=ienv state=istate]
@@ -10873,7 +11391,7 @@
10873 `[entry u.rest]
11391 `[entry u.rest]
10876−+$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition)]
11394++$ iresolved [env=ienv grouped=(list term) artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
10877+$ iadj (map term (list term))
11395+$ iadj (map term (list term))
10878+$ ivisited (map term ?)
11396+$ ivisited (map term ?)
10879+$ iwork (list [name=term done=?])
11397+$ iwork (list [name=term done=?])
@@ -10969,7 +11487,7 @@
10969++ add-groups
11487++ add-groups
10970 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
11488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
10971 ^- iresolved
11489 ^- iresolved
10972− ?~ components [env grouped artifacts]
11490+ ?~ components [env grouped artifacts ~]
10973 =/ component=(list term) i.components
11491 =/ component=(list term) i.components
10974 ?. (graph-cycle component graph) $(components t.components)
11492 ?. (graph-cycle component graph) $(components t.components)
10975 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
11493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -11010,11 +11528,13 @@
11010 =? artifacts ?=(^ u.finalized)
11528 =? artifacts ?=(^ u.finalized)
11011 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
11529 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
11012 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
11530 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
11013− `[[[name.d [typ vars]] env] checked artifacts]
11531+ `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]
11014++ add-supported-defs-core
11532++ add-supported-defs-core
11015 |= [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)])]
11533 |= [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)])]
11016− ^- [env=ienv artifacts=(list iwidth-definition)]
11534+ ^- [env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11535+ =/ failures=(list [name=term diag=idiag]) ~
11017− ?~ ds [env artifacts]
11537+ ?~ ds [env artifacts (flop failures)]
11018 =/ d=def i.ds
11538 =/ d=def i.ds
11019 ?: ?=(%mold -.d) $(ds t.ds)
11539 ?: ?=(%mold -.d) $(ds t.ds)
11020 ?. (unique-value-name name.d globals) $(ds t.ds)
11540 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -11025,37 +11545,34 @@
11025 =. gate-defs.initial checked
11545 =. gate-defs.initial checked
11026 =. head-evidence.initial heads
11546 =. head-evidence.initial heads
11027 =. initial (reserve-def-caps val.d initial)
11547 =. initial (reserve-def-caps val.d initial)
11028− =/ result=iresult (infer-fragment val.d env initial)
11548+ =/ plain=iresult (infer-fragment val.d env initial)
11549+ =/ result=iresult plain
11029 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11550 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11551+ ?: ?=(%| -.result)
11553+ ?: (definite-diag p.result) p.result
11554+ ?: ?=(%| -.plain) p.plain
11556+ =? failures (definite-diag failure) [[name.d failure] failures]
11030 =/ added=(unit iadded-definition)
11558 =/ added=(unit iadded-definition)
11031 (add-supported-result d result initial env checked artifacts)
11559 (add-supported-result d result initial env checked artifacts)
11032 ?~ added $(ds t.ds)
11560 ?~ added $(ds t.ds)
11033 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
11561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
11035−:: Full checking discards unsupported definitions. On that failure path only,
11563+:: Retry one unresolved definition to explain a pending tag. The gate
11036−:: retry a bounded number of missing definitions to explain a pending tag
11564+:: evidence is built from the whole module, not only this definition.
11037−:: from the same ordinary inference state instead of hiding it behind the
11038−:: generic completeness error. No successful definition takes this path.
11039−++ module-pending-tag
11565+++ module-pending-tag-one
11040− |= [ds=(list def) env=ienv base=istate fuel=@ud]
11566+ |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]
11041 ^- (unit [at=span msg=tape])
11567 ^- (unit [at=span msg=tape])
11042− =/ checked=(map term def) (direct-checked-gates ds env)
11568+ ?. ?=(%value -.d) ~
11043− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
11048− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
11049− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
11569+ ?^ (ienv-lookup name.d env) ~
11050 =/ initial=istate base(gate-defs checked, head-evidence heads)
11570 =/ initial=istate base(gate-defs checked, head-evidence heads)
11051 =. initial (reserve-def-caps val.d initial)
11571 =. initial (reserve-def-caps val.d initial)
11052 =/ result=iresult (infer-fragment val.d env initial)
11572 =/ result=iresult (infer-fragment val.d env initial)
11053 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11054− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
11574+ ?: ?=(%| -.result) ~
11055− =/ pending=(unit [at=span msg=tape])
11056− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11057− ?^ pending pending
11058− $(ds t.ds, fuel (dec fuel))
11060++ resolve-groups-core
11577++ resolve-groups-core
11061 |= [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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
11578 |= [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) index=(unit [at=path source=@t prelude=ifile shapes=(map term shape)])]
@@ -11071,12 +11588,12 @@
11071 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
11072 =/ ordered=(list def) (dependency-order ds components)
11589 =/ ordered=(list def) (dependency-order ds components)
11074− =/ next=[env=ienv artifacts=(list iwidth-definition)]
11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11075 (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)
11592 (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)
11076 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
11593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
11077 =. grec-index.initial index
11594 =. grec-index.initial index
11078 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11595 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
11079− ?: =(env env.out) out
11596+ ?: =(env env.out) out(failures failures.next)
11080 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11597 $(env env.out, grouped grouped.out, artifacts artifacts.out)
11082:: +dependency-order: the value definitions, dependencies first
11599:: +dependency-order: the value definitions, dependencies first
@@ -11948,13 +12465,29 @@
11948 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
12465 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
11949 ?^ first first
12466 ?^ first first
11950 $(segs t.segs)
12467 $(segs t.segs)
12468+:: A change's items each set a field once: two that name the same field,
12469+:: or one a field inside the other's, as cart and open.cart, overlap.
11951++ duplicate-edits
12470++ duplicate-edits
11952 |= edits=(list edit)
12471 |= edits=(list edit)
11953 ^- (unit idiag)
12472 ^- (unit idiag)
12473+ =| seen=(list edit)
12474+ |- ^- (unit idiag)
11954 ?~ edits ~
12475 ?~ edits ~
12477+ =/ prior=(list edit)
12478+ (skim seen |=(p=edit (wing-overlap (flop names.p) (flop names.e))))
12480+ =/ same=? =(names.i.prior names.e)
12481+ =/ sites=(list [at=span note=tape])
12482+ :~ [at.i.prior "first field"]
12483+ [at.e ?:(same "repeated field" "overlapping field")]
12485+ ?: same `["change field `{(show-names names.e)}` is repeated" sites]
12486+ =/ a=tape (show-names names.i.prior)
12487+ `["change fields `{a}` and `{(show-names names.e)}` overlap" sites]
11955− =/ first (duplicate-expr val.i.edits)
12488+ =/ first (duplicate-expr val.e)
11956 ?^ first first
12489 ?^ first first
11957− $(edits t.edits)
12490+ $(edits t.edits, seen [e seen])
11958++ duplicate-arms
12491++ duplicate-arms
11959 |= arms=(list arm)
12492 |= arms=(list arm)
11960 ^- (unit idiag)
12493 ^- (unit idiag)
@@ -12027,59 +12560,142 @@
12028 [n $(imports t.imports)]
12561 [n $(imports t.imports)]
12563+:: +reserved-name: whether n names a reserved operation
12565+:: proj and unface are handled by the checker by type, not bound, so
12566+:: no module may define, import or bind either name, as a value or
12567+:: as a mold. A field, tag or path segment may still be spelled so.
12030−++ reserved-proj-sample
12568+++ reserved-name
12571+ |(=(n %proj) =(n %unface))
12031 |= sam=sample
12573 |= sam=sample
12033 ?- -.sam
12575 ?- -.sam
12034− %bind =(name.sam %proj)
12576+ %bind (reserved-name name.sam)
12035− %face =(name.sam %proj)
12577+ %face (reserved-name name.sam)
12036− %pun =(name.sam %proj)
12578+ %pun (reserved-name name.sam)
12037− %cell (lien items.sam reserved-proj-sample)
12579+ %cell (lien items.sam reserved-sample)
12040−++ reserved-proj-pattern
12582+++ reserved-pattern
12041 |= p=pattern
12583 |= p=pattern
12044− %bind =(name.p %proj)
12586+ %bind (reserved-name name.p)
12045− %cell (lien items.p reserved-proj-pattern)
12587+ %cell (lien items.p reserved-pattern)
12048−++ reserved-proj-def
12590+++ reserved-def
12049 |= d=def
12591 |= d=def
12051− ?: =(name.d %proj) &
12593+ ?: (reserved-name name.d) &
12052− ?: ?=(%value -.d) (reserved-proj-expr val.d)
12594+ ?: ?=(%value -.d) (reserved-expr val.d)
12054−++ reserved-proj-expr
12596+++ reserved-expr
12055 |= e=expr
12597 |= e=expr
12058− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12600+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12059− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12601+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12060− %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
12602+ %change (lien edits.e |=(p=edit (reserved-expr val.p)))
12061 %pair $(e val.e)
12603 %pair $(e val.e)
12062 %unit $(e val.e)
12604 %unit $(e val.e)
12063 %group $(e inner.e)
12605 %group $(e inner.e)
12064− %list (lien items.e reserved-proj-expr)
12606+ %list (lien items.e reserved-expr)
12065− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
12607+ %tuple (lien items.e |=(i=item (reserved-expr val.i)))
12066− ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
12608+ ?(%gate %gate-wide) |((reserved-sample sample.e) $(e body.e))
12067 %cast $(e val.e)
12609 %cast $(e val.e)
12068− %call |($(e head.e) (lien args.e reserved-proj-expr))
12610+ %call |($(e head.e) (lien args.e reserved-expr))
12069 %trace |($(e val.e) $(e then.e))
12611 %trace |($(e val.e) $(e then.e))
12070− %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
12612+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-pattern pat.a) (reserved-expr val.a)))))
12071− %body |((lien defs.e reserved-proj-def) $(e final.e))
12613+ %body |((lien defs.e reserved-def) $(e final.e))
12075−++ module-has-reserved-proj
12617+++ module-has-reserved
12076 |= mod=module
12618 |= mod=module
12078 =/ imported=(list term) (import-binding-names imports.mod)
12620 =/ imported=(list term) (import-binding-names imports.mod)
12079 =/ vals=(list term) (global-value-names defs.mod)
12621 =/ vals=(list term) (global-value-names defs.mod)
12080 =/ molds=imolds (collect-simple-molds defs.mod)
12622 =/ molds=imolds (collect-simple-molds defs.mod)
12081 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12623 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12082− |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
12624+ |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))
12626+:: A scope collision retains source sites. Prelude declarations may be in
12627+:: another source, so their name and namespace are retained separately.
12628++$ iscope-diagnostic
12629+ [issue=idiag prelude=(unit [name=term kind=?(%value %mold %any)])]
12630+++ scope-import-diagnostic
12631+ |= [imports=(list import) prelude-values=(list term) prelude-molds=(list term) seen=written-fields]
12632+ ^- (each written-fields iscope-diagnostic)
12633+ ?~ imports [%& seen]
12634+ =/ imp=import i.imports
12641+ ?: (reserved-name n)
12642+ [%| [["`{(trip n)}` is reserved and cannot be bound" ~[[at.imp "reserved name"]]] ~]]
12643+ =/ earlier=(unit span) (~(get by seen) n)
12645+ [%| [["import `{(trip n)}` shadows an earlier import" ~[[u.earlier "earlier import"] [at.imp "conflicting import"]]] ~]]
12646+ ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x))))
12647+ [%| [["import `{(trip n)}` shadows a prelude name" ~[[at.imp "conflicting import"]]] `[n %any]]]
12648+ $(imports t.imports, seen (~(put by seen) n at.imp))
12649+++ scope-def-diagnostic
12650+ |= [defs=(list def) imports=written-fields prelude-values=(list term) prelude-molds=(list term) values=written-fields molds=written-fields]
12651+ ^- (unit iscope-diagnostic)
12655+ ?: (reserved-name n)
12656+ `[["`{(trip n)}` is reserved and cannot be bound" ~[[at.d "reserved name"]]] ~]
12657+ =/ imported=(unit span) (~(get by imports) n)
12659+ `[["definition `{(trip n)}` shadows an import" ~[[u.imported "import"] [at.d "conflicting definition"]]] ~]
12660+ =/ seen=written-fields ?:(?=(%value -.d) values molds)
12661+ =/ earlier=(unit span) (~(get by seen) n)
12663+ `[["definition `{(trip n)}` shadows an earlier definition" ~[[u.earlier "earlier definition"] [at.d "conflicting definition"]]] ~]
12664+ =/ prelude-names=(list term) ?:(?=(%value -.d) prelude-values prelude-molds)
12665+ ?: (lien prelude-names |=(x=term =(n x)))
12666+ `[["definition `{(trip n)}` shadows a prelude name" ~[[at.d "conflicting definition"]]] `[n ?:(?=(%value -.d) %value %mold)]]
12668+ $(defs t.defs, values (~(put by values) n at.d))
12669+ $(defs t.defs, molds (~(put by molds) n at.d))
12670+++ module-scope-diagnostic
12671+ |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12672+ ^- (unit iscope-diagnostic)
12673+ =/ imports=(each written-fields iscope-diagnostic)
12674+ (scope-import-diagnostic imports.mod prelude-values prelude-molds ~)
12675+ ?: ?=(%| -.imports) `p.imports
12676+ (scope-def-diagnostic defs.mod p.imports prelude-values prelude-molds ~ ~)
12677+++ show-scope-diagnostic
12678+ |= [file=path src=@t diagnostic=iscope-diagnostic prelude=(unit ifile)]
12680+ =/ excerpts=(list @t)
12681+ %+ turn sites.issue.diagnostic
12682+ |= site=[at=span note=tape]
12683+ (show-error src [file line.beg.at.site col.beg.at.site note.site])
12684+ =/ previous=(list @t)
12685+ ?~ prelude.diagnostic ~
12687+ ?~ source.u.prelude ~
12688+ =/ parsed (parse at.u.prelude u.source.u.prelude)
12689+ ?: ?=(%| -.parsed) ~
12690+ =/ matching=(list def)
12691+ %+ skim defs.p.parsed
12693+ ?& =(name.d name.u.prelude.diagnostic)
12694+ |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))
12697+ ~[(show-error u.source.u.prelude [at.u.prelude line.beg.at.i.matching col.beg.at.i.matching "prelude declaration"])]
12698+ (of-wain:format [(crip msg.issue.diagnostic) (weld excerpts previous)])
12084++ module-scope-valid
12700++ module-scope-valid
12085 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -12088,7 +12704,7 @@
12088 =/ vals=(list term) (global-value-names defs.mod)
12704 =/ vals=(list term) (global-value-names defs.mod)
12089 =/ molds=imolds (collect-simple-molds defs.mod)
12705 =/ molds=imolds (collect-simple-molds defs.mod)
12090 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12706 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12091− ?: (module-has-reserved-proj mod) |
12707+ ?: (module-has-reserved mod) |
12092 ?. %+ levy imported
12708 ?. %+ levy imported
12093 |= n=term
12709 |= n=term
12094 &((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))))
12710 &((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))))
@@ -12511,6 +13127,31 @@
12511 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
13127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
12512 `[u.name at.s]
13128 `[u.name at.s]
13130+:: Select the first available reason in dependency order, rather than
13131+:: preferring one class of diagnostic across the whole module. Only the
13132+:: first 64 definitions are retried for pending tags, as before.
13133+++ module-unresolved-diagnostic
13134+ |= [ds=(list def) env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence) failures=(list [name=term diag=idiag]) values=(list term) file=path src=@t fuel=@ud]
13138+ =/ remaining=@ud ?:(=(0 fuel) 0 (dec fuel))
13139+ ?: ?=(%mold -.d) $(ds t.ds, fuel remaining)
13140+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel remaining)
13141+ =/ found=(list [name=term diag=idiag])
13142+ (skim failures |=(failure=[name=term diag=idiag] =(name.failure name.d)))
13143+ ?^ found `(show-inference-diagnostic file src name.d diag.i.found)
13144+ =/ pending=(unit [at=span msg=tape])
13146+ (module-pending-tag-one d env base checked heads)
13148+ `(show-error src [file line.beg.at.u.pending col.beg.at.u.pending msg.u.pending])
13149+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow ~[d] env values)
13151+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
13152+ `(show-error src [file line.beg.at.u.shadow col.beg.at.u.shadow msg])
13153+ $(ds t.ds, fuel remaining)
12514:: Cache only completed interfaces for this invocation. The source bundle,
13155:: Cache only completed interfaces for this invocation. The source bundle,
12515:: imported Hoon types and prelude are fixed for the whole graph. Check the
13156:: imported Hoon types and prelude are fixed for the whole graph. Check the
12516:: active path and duplicate sources before consulting it, so a cache hit
13157:: active path and duplicate sources before consulting it, so a cache hit
@@ -12777,7 +13418,7 @@
12778 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
13419 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
12779 =/ derived=(list term) (weld path-names poke-names)
13420 =/ derived=(list term) (weld path-names poke-names)
12780− ?: (lien derived |=(n=term =(n %proj))) |
13421+ ?: (lien derived reserved-name) |
12781 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
13422 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
12782 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
13423 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
@@ -12809,7 +13450,7 @@
12809 =/ clashes=(list term)
13450 =/ clashes=(list term)
12810 %+ skip names
13451 %+ skip names
12811 |= n=term
13452 |= n=term
12812− ?| =(n %proj)
13453+ ?| (reserved-name n)
12813 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
13454 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
12815 ?~ clashes ~
13456 ?~ clashes ~
@@ -13584,7 +14225,7 @@
13584 =/ action=term %poke
14225 =/ action=term %poke
13585 =/ ordinary=(list def) ds
14226 =/ ordinary=(list def) ds
13586 =/ derived=(list term) ~[%state action]
14227 =/ derived=(list term) ~[%state action]
13587− ?: (lien derived |=(n=term =(n %proj))) [%| ~]
14228+ ?: (lien derived reserved-name) [%| ~]
13588 =/ outer=(list term)
14229 =/ outer=(list term)
13589 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
14230 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
13590 =/ clashes=(list term)
14231 =/ clashes=(list term)
@@ -13771,7 +14412,7 @@
13771 ?~ recovered ~
14412 ?~ recovered ~
13772 ?. ?=(~ vars.u.recovered) ~
14413 ?. ?=(~ vars.u.recovered) ~
13773 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14414 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13774− `[env.u.added grouped.resolution artifacts.u.added]
14415+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
13776++ program-inferred-slot
14417++ program-inferred-slot
13777 |= [typ=itype name=(unit term)]
14418 |= [typ=itype name=(unit term)]
@@ -13927,7 +14568,7 @@
13927 ?~ recovered ~
14568 ?~ recovered ~
13928 ?. ?=(~ vars.u.recovered) ~
14569 ?. ?=(~ vars.u.recovered) ~
13929 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14570 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13930− `[env.u.added grouped.resolution artifacts.u.added]
14571+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
13932+$ iview-site [xs=expr mapper=term]
14573+$ iview-site [xs=expr mapper=term]
13933++ program-view-site
14574++ program-view-site
@@ -14254,7 +14895,7 @@
14254 ?~ recovered ~
14895 ?~ recovered ~
14255 ?. ?=(~ vars.u.recovered) ~
14896 ?. ?=(~ vars.u.recovered) ~
14256 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14897 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14257− `[env.u.added grouped.resolution artifacts.u.added]
14898+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14259:: Recover exactly one direct keyed each/turn row mapper, then its view.
14900:: Recover exactly one direct keyed each/turn row mapper, then its view.
14260:: The prelude's own each and turn schemes determine the mapper gate: the
14901:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -14476,7 +15117,7 @@
14476 ?~ recovered ~
15117 ?~ recovered ~
14477 ?. ?=(~ vars.u.recovered) ~
15118 ?. ?=(~ vars.u.recovered) ~
14478 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15119 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14479− `[env.u.added grouped.resolution artifacts.u.added]
15120+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14481:: The model a direct program's initializer must produce. Update's written
15122:: The model a direct program's initializer must produce. Update's written
14482:: two-item sample gives it when it can be read. Otherwise main's own program
15123:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -14633,7 +15274,7 @@
14633 ?~ recovered ~
15274 ?~ recovered ~
14634 ?. ?=(~ vars.u.recovered) ~
15275 ?. ?=(~ vars.u.recovered) ~
14635 ?. ?=(~ (itype-vars typ.u.recovered)) ~
15276 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14636− `[env.u.added grouped.resolution artifacts.u.added]
15277+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
14638++ derived-poke-command-scheme
15279++ derived-poke-command-scheme
14639 |= [prelude=ifile action=itype]
15280 |= [prelude=ifile action=itype]
@@ -14801,9 +15442,9 @@
14801 (direct-prelude-evidence ds prelude.initial)
15442 (direct-prelude-evidence ds prelude.initial)
14802 ?~ heads resolution
15443 ?~ heads resolution
14803 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
15444 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
14804− =/ completed=[env=ienv artifacts=(list iwidth-definition)]
15445+ =/ completed=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
14805 (add-supported-defs-core ~[main] checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
15446 (add-supported-defs-core ~[main] checked heads env.resolution molds.initial globals.initial externals.initial surs.initial mark-externals.initial marks.initial jimports.initial reserved-molds.initial at.initial prelude.initial artifacts.resolution grec-index.initial)
14806− [env.completed grouped.resolution artifacts.completed]
15447+ [env.completed grouped.resolution artifacts.completed failures.resolution]
14808:: A static main may retain a generic element message in its ordinary
15449:: A static main may retain a generic element message in its ordinary
14809:: scheme. Instantiate that scheme, specialize it to canonical element !!,
15450:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -15019,6 +15660,9 @@
15019 !(lien prelude-molds |=(m=term =(m n)))
15660 !(lien prelude-molds |=(m=term =(m n)))
15663+ =/ scope=(unit iscope-diagnostic)
15664+ (module-scope-diagnostic mod(defs ordinary, imports faces) prelude-values prelude-molds)
15665+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
15022 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15023 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
15024 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
15668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -15067,6 +15711,9 @@
15067 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
15711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
15068 =/ checking=module mod(defs ds)
15712 =/ checking=module mod(defs ds)
15069 ?. (module-scope-valid checking prelude-values prelude-molds)
15713 ?. (module-scope-valid checking prelude-values prelude-molds)
15714+ =/ scope=(unit iscope-diagnostic)
15715+ (module-scope-diagnostic checking prelude-values prelude-molds)
15716+ ?^ scope [%| [(show-scope-diagnostic at src u.scope prelude) ~]]
15070 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
15071 =/ vals=(list term) (global-value-names ds)
15718 =/ vals=(list term) (global-value-names ds)
15072 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
15719 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
@@ -15142,15 +15789,14 @@
15142 ?~ store-parts ds
15789 ?~ store-parts ds
15143 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
15790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
15144 ?. (module-values-complete required env)
15791 ?. (module-values-complete required env)
15145− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15792+ =/ components=icomponents (graph-components required (global-value-names required))
15146− ?^ pending
15793+ =/ ordered=(list def) (dependency-order required components)
15147− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15148− :: A shadowing sample is an error, so it comes before any named value.
15149 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15794 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15150− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
15795+ =/ checked=(map term def) (direct-checked-gates required env)
15151− ?^ shadow
15796+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)
15152− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15797+ =/ diagnostic=(unit @t)
15153− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
15798+ (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)
15799+ ?^ diagnostic [%| [u.diagnostic ~]]
15154 =/ missing=(unit term) (module-missing-value required env)
15800 =/ missing=(unit term) (module-missing-value required env)
15155 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
15801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
15156 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
15802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
@@ -15354,8 +16000,8 @@
15354 ?: ?=(%| -.parsed) (show-error src p.parsed)
16000 ?: ?=(%| -.parsed) (show-error src p.parsed)
15355 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
16001 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
15356 ?^ duplicate (duplicate-fields-report file src u.duplicate)
16002 ?^ duplicate (duplicate-fields-report file src u.duplicate)
15357− ?: (module-has-reserved-proj p.parsed)
16003+ ?: (module-has-reserved p.parsed)
15358− 'module has reserved proj name'
16004+ 'module has a reserved proj or unface name'
15359 =/ ds=(list def) defs.p.parsed
16005 =/ ds=(list def) defs.p.parsed
15360 =/ molds=imolds (collect-simple-molds ds)
16006 =/ molds=imolds (collect-simple-molds ds)
15361 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
16007 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -15433,7 +16079,7 @@
15433 =. head-evidence.initial heads
16079 =. head-evidence.initial heads
15434 =. initial (reserve-def-caps val.d initial)
16080 =. initial (reserve-def-caps val.d initial)
15435 =/ result=iresult
16081 =/ result=iresult
15436− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
16082+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))
15437 (infer-recursive-gate d env initial)
16083 (infer-recursive-gate d env initial)
15438 (infer-fragment val.d env initial)
16084 (infer-fragment val.d env initial)
15439 ?: ?=(%| -.result)
16085 ?: ?=(%| -.result)
@@ -15465,7 +16111,8 @@
15465 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
16111 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
15466 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
16112 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
15467 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
16113 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
16114+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.result sub.state.p.result)
15468− =/ printable=itype (canonical-itype typ vars)
16115+ =/ printable=itype (canonical-itype named)
15469 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
16116 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
15470 $(ds t.ds, lines [line lines])
16117 $(ds t.ds, lines [line lines])
15471:: Experimental module-owned pending-constraint generalization only.
16118:: Experimental module-owned pending-constraint generalization only.
@@ -15562,7 +16209,7 @@
15562 =/ normalized=itype (itype-normalize typ sub.state)
16209 =/ normalized=itype (itype-normalize typ sub.state)
15563 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
16210 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
15564 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
16211 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
15565− `[[normalized quantified]]
16212+ `(cap-names normalized quantified caps.state sub.state)
15567+$ dgcommit [env=ienv state=istate]
16214+$ dgcommit [env=ienv state=istate]
15568:: A branch literal must not acquire a value face through replay.
16215:: A branch literal must not acquire a value face through replay.
@@ -15995,20 +16642,21 @@
15995 ?~ env `+(top)
16642 ?~ env `+(top)
15996 =/ sc=ischeme scheme.i.env
16643 =/ sc=ischeme scheme.i.env
15997 ?: (itype-has-tag typ.sc) ~
16644 ?: (itype-has-tag typ.sc) ~
15998− $(env t.env, top (itype-max-id typ.sc (max top (roll vars.sc max))))
16645+ $(env t.env, top (itype-max-id typ.sc (max top (roll (turn vars.sc var-count) max))))
16000−:: +itype-max-id: the largest variable or tag ID in t, or top
16647+:: +itype-max-id: the largest variable or tag ID in t, or top, without
16648+:: the variables' names (+named-var)
16002++ itype-max-id
16650++ itype-max-id
16003 |= [t=itype top=@ud]
16651 |= [t=itype top=@ud]
16006− %var (max top id.t)
16654+ %var (max top (var-count id.t))
16007− %fvar (max top id.t)
16655+ %fvar (max top (var-count id.t))
16008− %avar (max top id.t)
16656+ %avar (max top (var-count id.t))
16009− %rvar (max top id.t)
16657+ %rvar (max top (var-count id.t))
16010− %nvar (max top id.t)
16658+ %nvar (max top (var-count id.t))
16011− %rnvar (max top id.t)
16659+ %rnvar (max top (var-count id.t))
16012 %tag (max top id.t)
16660 %tag (max top id.t)
16013 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
16661 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
16014 %collection (itype-max-ids args.t top)
16662 %collection (itype-max-ids args.t top)