@@ -206,9 +206,11 @@
206206:: token holds the text after @. An aura starting @s or
207207:: @r is an error at 2nd: "signed and floating-point
208208:: auras are left out of Jibb"
209−:: A-Z type variable: one capital. A letter or digit right
210−:: after it is an error there, "a type variable is one
211−:: capital letter", after the type variable's token
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 -
212+:: is an error there, "a type variable is a capital,
213+:: then lowercase letters and digits"
212214:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names
213215:: joined by dots. Right after the name or wing, which
214216:: is emitted first, a capital or _ is an error there,
@@ -405,6 +407,7 @@
405407:: Why: after the layout pass the grammar is LL(2). Each choice is made by
406408:: the next token, at most with the one after it and whether it is tight:
407409:: name, then = tight a face (items, lines, fields, samples)
410+:: wing, then = tight a change's item or line, wing=value
408411:: name, then + tight a pair
409412:: name or wing, then ( tight a change
410413:: |=, then a term tight a constructor; else, where an
@@ -412,6 +415,9 @@
412415:: ++ or +$ a definition; else a body's final expr
413416:: INDENT a body, an open bracket's lines, arms
414417:: 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);
420+:: else an error
415421:: So the parser never backtracks, its first failure is its furthest, and
416422:: "expected X, found Y" falls out of each arm without tracking failures
417423:: across alternatives. Hoon's combinators read tapes of characters and
@@ -455,7 +461,9 @@
455461:: cases below -> %mold; one case is that mold, several
456462:: are %union. The optional generic wraps either in %generic.
457463:: ++ 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)
459467:: call one operand is that operand; more -> %call head args
460468:: operand literal -> %lit or %str; pathlit -> %path, as a path
461469:: literal is an expression (Decisions); !! -> %crash, as
@@ -472,7 +480,9 @@
472480:: that line, as () is no group. A ( followed by a rune is
473481:: the closed form. Lines of an open group or list take no
474482:: 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=
476486:: rune |= -> %gate; ^- -> %cast; ~& -> %trace; ?- -> %branch.
477487:: !! is an operand, not a rune (Decisions): alone where an
478488:: expression goes it is a call of one operand, and !! a
@@ -553,7 +563,23 @@
553563:: - Local definitions: at the start of any body, a gate's, an arm's,
554564:: a ^-'s, a ~&'s or a ++'s, as the EBNF's body takes them
555565:: (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.
557583:: - Where errors point: the doc says only "line, column and an
558584:: excerpt"; 2.0 and Errors below say where.
559585::
@@ -604,11 +630,12 @@
604630:: found the end of the line" (+fail-space). No later line can give
605631:: a tight form its next token. A wing and a ( after a space are no
606632:: 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
608−:: fails just past the name, whatever follows: `m(b c)` at the
609−:: space, `m(b)` at the ), `m(a"x)` at the " with the layout pass's
610−:: message after the parser's (+unnamed, +moved). `m(a==1)` has its
611−:: =, and fails at the second, where the layout pass does.
633+:: change's item is name= or wing=, so a name or a wing there with
634+:: no = right after it fails just past it, whatever follows: `m(b c)`
635+:: and `m(a.b 1)` at the space, `m(b)` at the ), `m(a"x)` at the "
636+:: with the layout pass's message after the parser's (+unnamed,
637+:: +moved). `m(a==1)` has its =, and fails at the second, where the
638+:: layout pass does.
612639:: - Where the place needs text on its own line and the line ends,
613640:: whatever line comes next: at the end of that line, just past its
614641:: last token, "found the end of the line" (+fail-line), as no later
@@ -786,7 +813,9 @@
786813:: (value 8:1 init
787814:: (cast 8:9
788815:: (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)))))
790819:: (value 9:1 update
791820:: (gate 9:11
792821:: (cell 9:14
@@ -795,17 +824,17 @@
795824:: (body 10:3
796825:: (branch 10:3
797826:: (wing 10:6 a)
798−:: (arm 11:5
799−:: (cell 11:5 (lit 11:6 %add) (bind 11:11 item))
800−:: (change 11:18 s
801−:: (edit 11:20 items
802−:: (tuple 11:26 (wing 11:27 item) (wing 11:32 items.s)))))
803−:: (arm 12:5
804−:: (lit 12:5 %toggle)
805−:: (change 12:18 s
806−:: (edit 12:20 open
807−:: (group 12:25
808−:: (call 12:26 (wing 12:26 not) (wing 12:30 open.s)))))))))))
827+:: (arm 11:3
828+:: (cell 11:3 (lit 11:4 %add) (bind 11:9 item))
829+:: (change 11:16 s
830+:: (edit 11:18 items
831+:: (tuple 11:24 (wing 11:25 item) (wing 11:30 items.s)))))
832+:: (arm 12:3
833+:: (lit 12:3 %toggle)
834+:: (change 12:16 s
835+:: (edit 12:18 open
836+:: (group 12:23
837+:: (call 12:24 (wing 12:24 not) (wing 12:28 open.s)))))))))))
809838::
810839:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
811840:: source line, then a caret under the column (col - 1 spaces, then ^).
@@ -816,9 +845,93 @@
816845:: prints as a space, so the caret stays under its column and golden
817846:: files hold no raw control bytes.
818847::
819−:: /ui/basket.jibb:22:5: msg has no case %submitt
820−:: %submitt [m(note="") ~]
821−:: ^
848+:: /ui/basket.jibb:22:3: msg has no case %submitt
849+:: %submitt [m(note="") ~]
850+:: ^
851+::
852+:: ===================================================================
853+:: 5. General checker core (design; not implemented yet)
854+:: ===================================================================
855+::
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.
860+::
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.
873+::
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.
884+::
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.
895+::
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.
905+::
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.
919+::
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.
929+::
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.
822935::
823936|%
824937+| %positions
@@ -964,9 +1077,10 @@
9641077::
9651078+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
9661079::
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]
9681082::
969−+$ edit $~([*span %$ *expr] [at=span name=term val=expr])
1083++$ edit $~([*span ~ *expr] [at=span names=(list term) val=expr])
9701084::
9711085:: +arm: a ?- arm, a pattern and an expression or body
9721086::
@@ -1355,10 +1469,10 @@
13551469 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
13561470 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
13571471 ?: (is-upper a)
1358− => (emit 1 [%tvar a])
1359− ?. &(?=(^ cs) |((is-lower i.cs) (is-upper i.cs) (is-digit i.cs)))
1360− cor
1361− (err col "a type variable is one capital letter")
1472+ =/ n=@ud (run-len t.cs tvar-mask)
1473+ => (emit +(n) [%tvar (crip [a (scag n t.cs)])])
1474+ ?. &(?=(^ cs) |((is-upper i.cs) =('_' i.cs) =('-' i.cs))) cor
1475+ (err col "a type variable is a capital, then lowercase letters and digits")
13621476 ?: =(':' a)
13631477 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
13641478 ?: =(':' b) comment
@@ -1662,6 +1776,7 @@
16621776++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
16631777++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f
16641778++ 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
16651780++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _
16661781++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .
16671782++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2
@@ -2280,7 +2395,7 @@
22802395++ sexp-edit
22812396 |= e=edit
22822397 ^- sexp
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)])
22842399::
22852400++ sexp-arm
22862401 |= a=arm
@@ -2689,24 +2804,32 @@
26892804 ?~ t.els i.els
26902805 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
26912806::
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 ~
2809+::
2810++$ slot [at=span face=(list term) val=expr]
2811+::
26922812:: +bracket-node: a tuple, list or change from its items, ending at fin
26932813::
26942814++ bracket-node
26952815 |= $: kind=?(%tuple %list %change)
26962816 op=token
26972817 target=(unit [t=token names=(list term)])
2698− its=(list item)
2818+ its=(list slot)
26992819 fin=loc
27002820 ==
27012821 ^- expr
27022822 ?- kind
2703− %tuple [%tuple [beg.at.op fin] its]
2704− %list [%list [beg.at.op fin] (turn its |=(i=item val.i))]
2823+ %tuple
2824+ :+ %tuple [beg.at.op fin]
2825+ (turn its |=(i=slot ^-(item [at.i ?~(face.i ~ `i.face.i) val.i])))
2826+ ::
2827+ %list [%list [beg.at.op fin] (turn its |=(i=slot val.i))]
27052828 ::
27062829 %change
27072830 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
27082831 :^ %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])))
27102833 ==
27112834::
27122835+| %parser
@@ -2927,23 +3050,22 @@
29273050 ::
29283051 :: +unnamed: a change's item or line without its name=
29293052 ::
2930− :: A name could still begin one, so the error is just past it, as
2931− :: a tight form's is (+fail-space): `m(b c)` at the space, `m(b)`
2932− :: at the ). So is an error token's text there, unless it begins
2933− :: with the =: `m(a"x)` at the ", with the layout pass's message
2934− :: after the parser's (+moved), but `m(a==1)` at the lexer's error,
2935− :: the second =. So is a wing's first name: `m(a.b=1)` fails at the
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).
3053+ :: A name or a wing could still begin one, so the error is just
3054+ :: past it, as a tight form's is (+fail-space): `m(b c)` and
3055+ :: `m(a.b 1)` at the space, `m(b)` at the ). So is an error token's
3056+ :: text there, unless it begins with the =: `m(a"x)` at the ", with
3057+ :: the layout pass's message after the parser's (+moved), but
3058+ :: `m(a==1)` at the lexer's error, the second =. At an error token
3059+ :: whose text can't begin a name, at that text, as `m( @sd` at the
3060+ :: @ (+fail-in).
29383061 ::
29393062 ++ unnamed
29403063 |= ts=(list token)
29413064 ^- [%| p=error]
29423065 =/ why=tape "a change's items are named, as in m(done=%.y)"
29433066 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
2944− ?: ?=([[* * [%wing *]] *] ts)
2945− (bad-in-why ts "a named item" lower-mask why)
2946− ?. ?=([[* * [%name *]] *] ts) (bad-why ts "a named item" why)
3067+ ?. ?=([[* * ?([%name *] [%wing *])] *] ts)
3068+ (bad-why ts "a named item" why)
29473069 =/ want=tape "`=` right after {(show-found i.ts)}"
29483070 ?: ?& ?=([* [* * [%error *]] *] ts)
29493071 =(end.at.i.ts from.lex.i.t.ts)
@@ -2961,9 +3083,10 @@
29613083 :: closes on its line (2.9). A bracket that needs none of these
29623084 :: closes with the deeper lines instead (+shut). No later line can
29633085 :: 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
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.
3086+ :: them (section 3, Errors). want is what it needs. It looks only when
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.
29673090 ::
29683091 ++ doomed
29693092 |= [ts=(list token) after=(list token) want=tape]
@@ -3120,7 +3243,7 @@
31203243 ?: =(%'++' lex.rune)
31213244 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
31223245 ;< [e=expr more=(list token)] then
3123− (read-expr-or-body "the name" after)
3246+ (read-expr-or-body | "the name" after)
31243247 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
31253248 ?: (is-closer rune)
31263249 %^ bad-why ts "a definition"
@@ -3200,20 +3323,36 @@
32003323 [%& p.lex.i.ts t.ts]
32013324 ::
32023325 :: +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
32043330 ::
32053331 ++ read-expr-or-body
3206− |= [what=tape ts=(list token)]
3332+ |= [fin=? what=tape ts=(list token)]
32073333 ^- (pare expr)
32083334 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3335+ ?: &(fin ?=([[* * %newline] *] ts)) (read-rest t.ts)
32093336 ?: ?=([[* * ?(%newline %dedent)] *] ts)
32103337 (bad ts "an expression, or a body on deeper lines")
32113338 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3212− (read-expr ts)
3339+ (read-last &(fin !?=([[* * %'?-'] *] ts)) ts)
32133340 ::
3214− :: +read-body: after its INDENT, { definition NEWLINE } expr DEDENT
3341+ :: +read-body: after its INDENT, the rest of a body, then its DEDENT
32153342 ::
32163343 ++ read-body
3344+ |= ts=(list token)
3345+ ^- (pare expr)
3346+ ;< [e=expr after=(list token)] then (read-rest ts)
3347+ ?> ?=([[* * %dedent] *] after)
3348+ [%& e t.after]
3349+ ::
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
3353+ :: (+read-last)
3354+ ::
3355+ ++ read-rest
32173356 |= ts=(list token)
32183357 ^- (pare expr)
32193358 =| defs=(list def)
@@ -3227,12 +3366,15 @@
32273366 %: bad-in-why ts "a definition or an expression" plus-mask
32283367 "`+` begins `++` or `+$`"
32293368 ==
3230− ;< [e=expr after=(list token)] then (read-expr ts)
3369+ ;< [e=expr after=(list token)] then (read-last & ts)
32313370 ?: ?=([[* * %dedent] *] after)
32323371 =/ ds=(list def) (flop defs)
32333372 =/ 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]
32353374 ?. ?=([[* * %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"
32363378 %^ bad-why after "the end of the body"
32373379 "a body's final expression is its last line"
32383380 ::
@@ -3241,13 +3383,24 @@
32413383 ++ read-expr
32423384 |= ts=(list token)
32433385 ^- (pare expr)
3386+ (read-last | ts)
3387+ ::
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)
3393+ ::
3394+ ++ read-last
3395+ |= [fin=? ts=(list token)]
3396+ ^- (pare expr)
32443397 ?~ ts (bad ts "an expression")
32453398 =* t i.ts
32463399 ?+ lex.t (read-call ts)
3247− %'|=' ?:((is-ctor ts) (read-call ts) (read-gate t t.ts))
3248− %'^-' (read-cast t t.ts)
3249− %'~&' (read-trace t t.ts)
3250− %'?-' (read-branch t t.ts)
3400+ %'|=' ?:((is-ctor ts) (read-call ts) (read-gate fin t t.ts))
3401+ %'^-' (read-cast fin t t.ts)
3402+ %'~&' (read-trace fin t t.ts)
3403+ %'?-' (read-branch fin t t.ts)
32513404 ==
32523405 ::
32533406 :: +read-call: operand { operand }; one operand alone is itself
@@ -3462,9 +3615,9 @@
34623615 (unclosed par ")" after)
34633616 ;< [els=(list expr) after=(list token)] then (read-operands ts)
34643617 ?: ?=([[* * %indent] *] after)
3465− ;< [ls=(list item) more=(list token)] then
3618+ ;< [ls=(list slot) more=(list token)] then
34663619 (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))))
34683621 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
34693622 ?~ els
34703623 ?: ?=([[* * ?(%newline %dedent)] *] after)
@@ -3489,7 +3642,7 @@
34893642 ==
34903643 ^- (pare expr)
34913644 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3492− =| its=(list item)
3645+ =| its=(list slot)
34933646 |- ^- (pare expr)
34943647 ?~ ts (bad ts "an item")
34953648 =* t i.ts
@@ -3497,8 +3650,8 @@
34973650 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
34983651 ?: (is-closer t) (unclosed op (trip close) ts)
34993652 ?: ?=(%indent lex.t)
3500− ;< [ls=(list item) more=(list token)] then (read-lines kind t.ts)
3501− =/ every=(list item) (weld (flop its) ls)
3653+ ;< [ls=(list slot) more=(list token)] then (read-lines kind t.ts)
3654+ =/ every=(list slot) (weld (flop its) ls)
35023655 =/ fin=loc ?~(every end.at.op end.at:(rear every))
35033656 [%& (bracket-node kind op target every fin) more]
35043657 ?: &(?=(^ its) (shut op `at.i.its ts))
@@ -3506,21 +3659,21 @@
35063659 ?: ?=(?(%newline %dedent) lex.t)
35073660 (unclosed-open op (trip close) "an item" ts)
35083661 ?: &(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)
35103663 $(its [i its], ts more)
35113664 ::
35123665 :: +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
35143667 ::
35153668 ++ read-item
35163669 |= [kind=?(%tuple %list %change) ts=(list token)]
3517− ^- (pare item)
3518− ?: &(!?=(%list kind) ?=([[* * [%name *]] [* %& %'='] *] ts))
3670+ ^- (pare slot)
3671+ ?: &(?=([* * *] ts) (named-item kind ts))
35193672 =* nam i.ts
35203673 =/ rest=(list token) t.t.ts
35213674 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
35223675 ;< [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]
35243677 ?: ?=(%change kind) (unnamed ts)
35253678 ?: &(?=(^ ts) (is-rune i.ts))
35263679 %: bad-in-why ts "an expression" operand-mask
@@ -3529,15 +3682,25 @@
35293682 ;< [v=expr after=(list token)] then (read-operand ts)
35303683 [%& [(span-of v) ~ v] after]
35313684 ::
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
3687+ ::
3688+ ++ named-item
3689+ |= [kind=?(%tuple %list %change %group) ts=(list token)]
3690+ ^- ?
3691+ ?. ?=([* [* %& %'='] *] ts) |
3692+ ?: ?=([[* * [%name *]] *] ts) ?=(?(%tuple %change) kind)
3693+ &(?=(%change kind) ?=([[* * [%wing *]] *] ts))
3694+ ::
35323695 :: +read-lines: after an open bracket's INDENT, its lines, an item
35333696 :: each, to its DEDENT
35343697 ::
35353698 ++ read-lines
35363699 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3537− ^- (pare (list item))
3538− =| ls=(list item)
3539− |- ^- (pare (list item))
3540− ;< [l=item after=(list token)] then (read-line kind ts)
3700+ ^- (pare (list slot))
3701+ =| ls=(list slot)
3702+ |- ^- (pare (list slot))
3703+ ;< [l=slot after=(list token)] then (read-line kind ts)
35413704 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
35423705 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
35433706 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
@@ -3564,22 +3727,20 @@
35643727 "its items end at the first line that isn't deeper"
35653728 ::
35663729 :: +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
3568− :: (doc question)
3730+ :: be named, a change's must be, by a name or a wing, a list's and a
3731+ :: group's are not (doc question)
35693732 ::
35703733 ++ read-line
35713734 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3572− ^- (pare item)
3735+ ^- (pare slot)
35733736 =/ cf (closer-first ts "an item")
35743737 ?^ cf u.cf
3575− ?: ?& ?=(?(%tuple %change) kind)
3576− ?=([[* * [%name *]] [* %& %'='] *] ts)
3577− ==
3738+ ?: &(?=([* * *] ts) (named-item kind ts))
35783739 =* nam i.ts
35793740 =/ rest=(list token) t.t.ts
35803741 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
35813742 ;< [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]
35833744 ?: ?=(%change kind) (unnamed ts)
35843745 ;< [v=expr after=(list token)] then (read-expr ts)
35853746 [%& [(span-of v) ~ v] after]
@@ -3616,10 +3777,11 @@
36163777 %^ bad-why more (closing op ")")
36173778 "the wide gate's body is one operand, so a call goes in parentheses"
36183779 ::
3619− :: +read-gate: |= sample, then an expression or a body
3780+ :: +read-gate: |= sample, then an expression or a body; fin as for
3781+ :: +read-last
36203782 ::
36213783 ++ read-gate
3622− |= [bar=token ts=(list token)]
3784+ |= [fin=? bar=token ts=(list token)]
36233785 ^- (pare expr)
36243786 ?: &(?=(^ ts) tight.i.ts)
36253787 :: a % could begin a constructor's term, as |=%got
@@ -3631,13 +3793,14 @@
36313793 =/ dm (doomed ts after "an expression, or a body on deeper lines")
36323794 ?^ dm u.dm
36333795 ;< [e=expr more=(list token)] then
3634− (read-expr-or-body "the sample" after)
3796+ (read-expr-or-body fin "the sample" after)
36353797 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
36363798 ::
3637− :: +read-cast: ^- mold, then an expression or a body
3799+ :: +read-cast: ^- mold, then an expression or a body; fin as for
3800+ :: +read-last
36383801 ::
36393802 ++ read-cast
3640− |= [ket=token ts=(list token)]
3803+ |= [fin=? ket=token ts=(list token)]
36413804 ^- (pare expr)
36423805 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
36433806 ;< [s=shape after=(list token)] then (read-mold ts)
@@ -3646,41 +3809,65 @@
36463809 =/ dm (doomed ts after "an expression, or a body on deeper lines")
36473810 ?^ dm u.dm
36483811 ;< [e=expr more=(list token)] then
3649− (read-expr-or-body "the mold" after)
3812+ (read-expr-or-body fin "the mold" after)
36503813 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
36513814 ::
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
36533817 ::
36543818 ++ read-trace
3655− |= [sig=token ts=(list token)]
3819+ |= [fin=? sig=token ts=(list token)]
36563820 ^- (pare expr)
36573821 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
36583822 ;< [v=expr after=(list token)] then (read-expr ts)
3659− ?. ?=([[* * %indent] *] after)
3660− =/ dm (doomed ts after "`~&`'s body on deeper lines")
3661− ?^ dm u.dm
3823+ =/ dm (doomed ts after "`~&`'s body on deeper lines")
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)
36623828 (bad after "`~&`'s body on deeper lines")
3663− ;< [b=expr more=(list token)] then (read-body t.after)
36643829 [%& [%trace [beg.at.sig end:(span-of b)] v b] more]
36653830 ::
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)
36673834 ::
36683835 ++ read-branch
3669− |= [wut=token ts=(list token)]
3836+ |= [fin=? wut=token ts=(list token)]
36703837 ^- (pare expr)
36713838 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
36723839 ;< [s=expr after=(list token)] then (read-expr ts)
3673− ?. ?=([[* * %indent] *] after)
3674− =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3675− ?^ dm u.dm
3840+ =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3841+ ?^ dm u.dm
3842+ ?. ?=([[* * ?(%indent %newline)] *] after)
36763843 (bad after "`?-`'s arms on deeper lines")
3844+ =/ flat=? ?=(%newline lex.i.after)
3845+ ?: &(flat !fin) (bad after "`?-`'s arms on deeper lines")
36773846 =| arms=(list arm)
36783847 =/ rest=(list token) t.after
36793848 |- ^- (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))
36813851 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
36823852 ?. ?=([[* * %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)]
3855+ ::
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
3858+ ::
3859+ ++ read-flat-arm
3860+ |= ts=(list token)
3861+ ^- (pare arm)
3862+ ?: ?=([[* * ?(%'++' %'+$')] *] ts)
3863+ %: bad-in-why ts "a pattern" pattern-mask
3864+ "a body's local definitions come before its final expression"
3865+ ==
3866+ ?: ?=([[* * ?(%'~&' %'^-')] *] ts)
3867+ %: bad-in-why ts "a pattern" pattern-mask
3868+ "a trace or cast goes in the arm's body"
3869+ ==
3870+ (read-arm ts)
36843871 ::
36853872 :: +read-arm: a pattern, then an expression or a body
36863873 ::
@@ -3695,7 +3882,7 @@
36953882 %^ bad-why after "a space after the pattern"
36963883 "patterns take no `name=`: a bare name binds, as [a b]"
36973884 ;< [e=expr more=(list token)] then
3698− (read-expr-or-body "the pattern" after)
3885+ (read-expr-or-body | "the pattern" after)
36993886 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
37003887 ::
37013888 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
@@ -4437,7 +4624,7 @@
44374624++ outline-edit
44384625 |= e=edit
44394626 ^- outline
4440− [%edit at.e ~[%name] %kid ~[(outline-expr val.e)]]
4627+ [%edit at.e ~[%name %wing] %kid ~[(outline-expr val.e)]]
44414628::
44424629++ outline-arm
44434630 |= a=arm
@@ -4637,6 +4824,14 @@
46374824:: proofs to fewer than 1,024 cells; the projection planner has a separate
46384825:: 4,096-step bound. These are inference limits, not language limits.
46394826::
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.
4834+::
46404835:: Supported API imports derive request-gate types atomically for multiple
46414836:: paths, including one typed segment or one diff fold per case. Their checked
46424837:: ordinary definitions, mark molds and supported poke constructor are also
@@ -4944,6 +5139,35 @@
49445139 $(a tal.a, b tal.b, sub u.first)
49455140 ~
49465141::
5142+:: +itype-unface: t with every face removed, for (unface e)
5143+::
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
5151+:: t= in its mold.
5152+::
5153+++ itype-unface
5154+ |= [t=itype sub=isub]
5155+ ^- itype
5156+ =. t (itype-walk t sub)
5157+ ?+ -.t t
5158+ %face $(t body.t)
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)))]
5162+ %union
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])
5169+ ==
5170+::
49475171+$ igf-form [typ=itype sub=isub left=@ud]
49485172+$ igf-forms [types=(list itype) sub=isub left=@ud]
49495173++ itype-gate-free-forms
@@ -6375,15 +6599,67 @@
63756599 ^- ?
63766600 (itype-var-is-gate-free-fuel n t 256)
63776601::
6602+:: +named-var: the ID of the nth type variable, written as name
6603+::
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.
6609+::
6610+++ named-var
6611+ |= [name=@t n=@ud]
6612+ ^- @ud
6613+ (add (lsh 6 name) (end 6 n))
6614+::
6615+:: +var-name: the name in a type variable's ID, or 0 for none
6616+::
6617+++ var-name
6618+ |= id=@ud
6619+ ^- @t
6620+ (rsh 6 id)
6621+::
6622+:: +var-count: a type variable's ID without its name
6623+::
6624+++ var-count
6625+ |= id=@ud
6626+ ^- @ud
6627+ (end 6 id)
6628+::
6629+:: +canonical-itype: t with the variables in vars renumbered to print
6630+::
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.
6635+::
63786636++ canonical-itype
63796637 |= [t=itype vars=(list @ud)]
63806638 ^- itype
6639+ =/ names=(list @t) (turn vars var-name)
6640+ =/ used=(list @t) ~
63816641 =/ ren=isub ~
63826642 =/ n=@ud 0
63836643 |-
63846644 ?~ vars (itype-rename t ren)
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])))
6386− $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
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)
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])))
6650+ $(vars t.vars, ren [[i.vars replacement] ren], n ?:(own n +(n)), used ?:(own [name used] used))
6651+::
6652+:: +letter-free: the first number from n whose letter is none of names
6653+::
6654+++ letter-free
6655+ |= [n=@ud names=(list @t)]
6656+ ^- @ud
6657+ ?. (lien names |=(m=@t =(m (crip (show-var n))))) n
6658+ $(n +(n))
6659+::
6660+:: +instantiate-scheme: a scheme's type with fresh quantified variables
6661+::
6662+:: Each fresh variable keeps the name of the one it replaces.
63876663::
63886664++ instantiate-scheme
63896665 |= [scheme=ischeme state=istate]
@@ -6392,12 +6668,13 @@
63926668 =/ vars=(list @ud) vars.scheme
63936669 |-
63946670 ?~ vars [(itype-rename typ.scheme ren) state]
6671+ =/ fresh=@ud (named-var (var-name i.vars) next.state)
63956672 =/ 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])))
63976674 :: A generalized atom variable is a valid origin for re-generalizing
63986675 :: an alias, just as a sample binder is.
63996676 =/ 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]
64016678 $(vars t.vars, ren [[i.vars replacement] ren], state st)
64026679::
64036680++ icap-lookup
@@ -7257,7 +7534,8 @@
72577534 ?: in-mold.state ~
72587535 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
72597536 ?^ n `[[%var u.n] state]
7260− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]
7537+ =/ id=@ud (named-var name.sh next.state)
7538+ `[[%var id] state(next +(next.state), caps [[name.sh id at.sh] caps.state])]
72617539 * ~
72627540 ==
72637541::
@@ -7290,12 +7568,12 @@
72907568 ^- isample-result
72917569 ?- -.s
72927570 %bind
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))))
72947572 [%| "sample shadows a name"]
72957573 =/ t=itype [%var next.state]
72967574 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
72977575 %face
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))))
72997577 [%| "sample shadows a name"]
73007578 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
73017579 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -7363,7 +7641,7 @@
73637641 |-
73647642 ?~ ds &
73657643 ?: ?=(%mold -.i.ds) $(ds t.ds)
7366− ?: =(name.i.ds %proj) |
7644+ ?: (reserved-name name.i.ds) |
73677645 ?. (unique-value-name name.i.ds names) |
73687646 ?: ?=(^ (ienv-lookup name.i.ds env)) |
73697647 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -7387,7 +7665,7 @@
73877665 |-
73887666 ?~ locals &
73897667 =/ n=term name.i.locals
7390− ?: =(n %proj) |
7668+ ?: (reserved-name n) |
73917669 ?. (unique-value-name n names) |
73927670 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
73937671 ?: (lien marks.state |=(m=term =(n m))) |
@@ -7537,7 +7815,8 @@
75377815 ^- istate
75387816 ?~ sites state
75397817 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7540− $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))
7818+ =/ id=@ud (named-var name.i.sites next.state)
7819+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites id at.i.sites] caps.state]))
75417820::
75427821++ reserve-def-caps
75437822 |= [e=expr state=istate]
@@ -7711,7 +7990,8 @@
77117990 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
77127991 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
77137992 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7714− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
7993+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.inferred sub.state.p.inferred)
7994+ $(ds t.ds, env [[name.d named] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)
77157995::
77167996:: Try complete cyclic local groups after individual definitions stall.
77177997:: Components with non-gates or unresolved constraints stay unavailable.
@@ -8065,7 +8345,7 @@
80658345 [%| ["list branch pattern is not supported by partial inference" ~]]
80668346 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
80678347 ?~ 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)))))
80698349 [%| ["pattern binder shadows a name" ~]]
80708350 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
80718351 =/ left=iresult
@@ -8102,7 +8382,7 @@
81028382 [%| ["unit branch pattern is not supported by partial inference" ~]]
81038383 =/ binder=(unit term) ?:(first-empty second-name first-name)
81048384 ?~ 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))))
81068386 [%| ["pattern binder shadows a name" ~]]
81078387 =/ payload=(unit itype) (unit-union-payload typ)
81088388 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -8209,7 +8489,7 @@
82098489 ^- (unit ienv)
82108490 =. t ?:(?=(%face -.t) body.t t)
82118491 ?: ?=(%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)))) ~
82138493 `[[name.p [t ~]] env]
82148494 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
82158495 `env
@@ -8735,7 +9015,9 @@
87359015 `subject
87369016::
87379017:: 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.
87399021++ change-spine-known
87409022 |= [t=itype sub=isub]
87419023 ^- ?
@@ -8747,19 +9029,18 @@
87479029 $(t tal.t)
87489030::
87499031++ 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))]
87519033 ^- iresult
87529034 ?~ edits [%& target state]
87539035 =/ 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)))
87559038 [%| ["repeated change fields are not supported by partial inference" ~]]
87569039 ?. (change-spine-known target sub.state)
87579040 [%| ["change target needs a known record in partial inference" ~]]
8758− =/ found=(list itype) (record-fields-named name.entry target sub.state)
8759− ?~ found
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
9041+ =/ field=(each itype idiag) (change-wing-field entry target sub.state)
9042+ ?: ?=(%| -.field) [%| p.field]
9043+ =/ expected=itype p.field
87639044 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
87649045 ?: ?=(%| -.value) value
87659046 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
@@ -8768,7 +9049,67 @@
87689049 =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
87699050 ?^ decimal [%| u.decimal]
87709051 [%| ["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])
9053+::
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
9056+::
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)
9065+ ?~ outer [%& typ]
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)}`"
9071+ :- %|
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)
9075+ ?~ found
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])
9079+::
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
9082+::
9083+++ edit-name-at
9084+ |= [e=edit k=@ud]
9085+ ^- span
9086+ =/ col=@ud col.beg.at.e
9087+ =/ ns=(list term) names.e
9088+ |- ^- span
9089+ ?~ ns at.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)))
9093+::
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
9096+::
9097+++ itype-not-record
9098+ |= [t=itype sub=isub]
9099+ ^- ?
9100+ =. t (itype-walk t sub)
9101+ ?=(?(%atom %any-atom %flag %const %tag %collection %fn %union %noun %empty) -.t)
9102+::
9103+:: +wing-overlap: whether two edits' wings, outermost first, name the
9104+:: same field or one a field inside the other's
9105+::
9106+++ wing-overlap
9107+ |= [a=(list term) b=(list term)]
9108+ ^- ?
9109+ ?~ a &
9110+ ?~ b &
9111+ ?. =(i.a i.b) |
9112+ $(a t.a, b t.b)
87729113::
87739114:: Backtick constructs the canonical prelude unit, after checking its
87749115:: prepared template has the standard null and [~ u=A] cases.
@@ -9138,6 +9479,7 @@
91389479 [%& typ.instance state.instance]
91399480 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
91409481 ?~ scheme
9482+ ?: =(i.names.e %unface) [%| (unface-value at.e)]
91419483 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
91429484 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
91439485 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
@@ -9145,7 +9487,10 @@
91459487 [%& typ.inst state.inst]
91469488 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
91479489 [%& typ.instance state.instance]
9148− %group $(e inner.e)
9490+ %group
9491+ ?: &(?=(%wing -.inner.e) =(names.inner.e ~[%unface]) ?=(~ (ienv-lookup %unface env)))
9492+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
9493+ $(e inner.e)
91499494 %change
91509495 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
91519496 =/ target=iresult $(e [%wing at.e target.e])
@@ -9289,6 +9634,7 @@
92899634 ?~ args.e [%| ["call has no argument" ~]]
92909635 ?: (explicit-proj-call e env state)
92919636 [%| ["proj needs an expected record type" ~]]
9637+ ?: (reserved-call %unface e env state) (infer-unface e env state)
92929638 (infer-call-with-head e env state (infer-fragment head.e env state))
92939639 * [%| ["expression is not supported by partial inference" ~]]
92949640 ==
@@ -9679,6 +10025,7 @@
967910025 ^- iresult
968010026 ?> ?=(%call -.e)
968110027 ?~ args.e [%| ["call has no argument" ~]]
10028+ ?: (reserved-call %unface e env state) (infer-unface e env state)
968210029 =/ head=iresult (infer-fragment head.e env state)
968310030 ?: ?=(%| -.head) head
968410031 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
@@ -9761,18 +10108,70 @@
976110108 `(infer-simple-items items.e env state)
976210109 `(width-infer-items items.e index.u.target env state context)
976310110::
9764−:: Experimental intrinsic recognition; real bindings retain normal calls.
10111+:: +reserved-call: whether e calls the reserved operation n
10112+::
10113+:: Experimental intrinsic recognition; real bindings retain normal calls.
10114+++ reserved-call
10115+ |= [n=term e=expr env=ienv state=istate]
10116+ ^- ?
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)) | &)
976510124++ explicit-proj-call
976610125 |= [e=expr env=ienv state=istate]
976710126 ^- ?
976810127 ?. ?=(%call -.e) |
976910128 ?. ?=([* ~] args.e) |
9770− ?. ?=(%wing -.head.e) |
9771− ?. =(names.head.e ~[%proj]) |
9772− ?: ?=(^ (ienv-lookup %proj env)) |
9773− ?: (lien globals.state |=(n=term =(n %proj))) |
9774− ?~ prelude.state &
9775− ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
10129+ (reserved-call %proj e env state)
10130+::
10131+:: +infer-unface: (unface e), e's type with every face removed
10132+::
10133+:: A reserved operation handled by type, like proj. Any number of
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.
10138+++ infer-unface
10139+ |= [e=expr env=ienv state=istate]
10140+ ^- iresult
10141+ ?> ?=(%call -.e)
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]
10151+::
10152+:: +unface-value: the error for unface written where a value goes
10153+::
10154+++ unface-value
10155+ |= at=span
10156+ ^- idiag
10157+ ["unface is not a value; write |=(g (unface g))" ~[[at "unface used as a value"]]]
10158+::
10159+:: +unfaced-gate: the gate under a ++'s (unface |= …), or ~
10160+::
10161+:: Such a ++ is a gate for recursion: its own name has the unfaced
10162+:: type, and its body may call it.
10163+++ unfaced-gate
10164+ |= [e=expr env=ienv state=istate]
10165+ ^- (unit expr)
10166+ ?: ?=(%group -.e) $(e inner.e)
10167+ ?. (reserved-call %unface e env state) ~
10168+ ?> ?=(%call -.e)
10169+ ?. ?=([* ~] args.e) ~
10170+ =/ gate=expr i.args.e
10171+ |-
10172+ ?: ?=(%group -.gate) $(gate inner.gate)
10173+ ?. ?=(?(%gate %gate-wide) -.gate) ~
10174+ `gate
977610175++ infer-proj-source
977710176 |= [e=expr expected=itype env=ienv state=istate context=span]
977810177 ^- iresult
@@ -10179,7 +10578,7 @@
1017910578 ?~ pats [%& ~]
1018010579 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
1018110580 =/ 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))))
1018310582 [%| 'pattern shadows a name']
1018410583 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
1018510584 ?: ?=(%| -.rest) rest
@@ -10256,24 +10655,12 @@
1025610655 ^- tape
1025710656 =. t (itype-walk t sub)
1025810657 ?- -.t
10259− %var
10260− ?: (lth id.t 26) [(add 65 id.t) ~]
10261− "T{<id.t>}"
10262− %fvar
10263− ?: (lth id.t 26) [(add 65 id.t) ~]
10264− "T{<id.t>}"
10265− %avar
10266− ?: (lth id.t 26) [(add 65 id.t) ~]
10267− "T{<id.t>}"
10268− %rvar
10269− ?: (lth id.t 26) [(add 65 id.t) ~]
10270− "T{<id.t>}"
10271− %nvar
10272− ?: (lth id.t 26) [(add 65 id.t) ~]
10273− "T{<id.t>}"
10274− %rnvar
10275− ?: (lth id.t 26) [(add 65 id.t) ~]
10276− "T{<id.t>}"
10658+ %var (show-var id.t)
10659+ %fvar (show-var id.t)
10660+ %avar (show-var id.t)
10661+ %rvar (show-var id.t)
10662+ %nvar (show-var id.t)
10663+ %rnvar (show-var id.t)
1027710664 %atom "@{(trip aura.t)}"
1027810665 %any-atom "@"
1027910666 %flag "?"
@@ -10294,6 +10681,17 @@
1029410681 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
1029510682 ==
1029610683::
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
10686+::
10687+++ show-var
10688+ |= id=@ud
10689+ ^- tape
10690+ =/ name=@t (var-name id)
10691+ ?. =(0 name) (trip name)
10692+ ?: (lth id 26) [(add 65 id) ~]
10693+ "T{<id>}"
10694+::
1029710695++ show-itype-item
1029810696 |= [t=itype sub=isub]
1029910697 ^- tape
@@ -10352,7 +10750,7 @@
1035210750 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
1035310751 ?: (itype-has-hidden-recursive normalized) label
1035410752 =/ 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))
1035610754 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
1035710755::
1035810756:: A capital in a written mold is generalized with its enclosing ++.
@@ -10393,6 +10791,116 @@
1039310791 ?: =(n u.ident) `i.caps
1039410792 $(caps t.caps)
1039510793::
10794+:: +cap-names: give each variable in vars the name it was written with
10795+::
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.
10803+::
10804+++ cap-names
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) ~
10811+ |-
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)
10815+ =/ name=@t
10816+ ?^ cap name.u.cap
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)
10820+ (var-name i.vars)
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))
10824+::
10825+:: +joined-names: for each variable that named ones resolve to, the
10826+:: earliest made of those, by count
10827+::
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.
10832+::
10833+++ joined-names
10834+ |= sub=isub
10835+ ^- (map @ud @ud)
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) ~
10844+ |-
10845+ ?~ named out
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)))
10851+ $(named t.named)
10852+ $(named t.named, out (~(put by out) u.root i.named))
10853+::
10854+:: +follow-var: the variable that id resolves to through edges, or ~ if
10855+:: it resolves to another type; fuel bounds the steps
10856+::
10857+++ follow-var
10858+ |= [id=@ud edges=(map @ud (unit @ud)) fuel=@ud]
10859+ ^- (unit @ud)
10860+ |-
10861+ ?: =(0 fuel) ~
10862+ =/ edge=(unit (unit @ud)) (~(get by edges) id)
10863+ ?~ edge `id
10864+ ?~ u.edge ~
10865+ ?: =(u.u.edge id) `id
10866+ $(id u.u.edge, fuel (dec fuel))
10867+::
10868+:: +var-of: the ID of a type variable node, or ~ for another type
10869+::
10870+++ var-of
10871+ |= t=itype
10872+ ^- (unit @ud)
10873+ ?+ -.t ~
10874+ %var `id.t
10875+ %fvar `id.t
10876+ %avar `id.t
10877+ %rvar `id.t
10878+ %nvar `id.t
10879+ %rnvar `id.t
10880+ ==
10881+::
10882+:: +itype-reid: t with the variable IDs in ids replaced, each node
10883+:: keeping its kind
10884+::
10885+++ itype-reid
10886+ |= [t=itype ids=(map @ud @ud)]
10887+ ^- itype
10888+ ?- -.t
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))
10902+ ==
10903+::
1039610904++ merged-capitals
1039710905 |= [caps=icaps sub=isub]
1039810906 ^- (unit [first=icap second=icap])
@@ -10612,6 +11120,9 @@
1061211120 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
1061311121 =. gate-defs.state ~
1061411122 ?. ?=(%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
1061511126 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
1061611127 [%| ["recursive definition is not a gate" ~]]
1061711128 =/ result=(unit itype) (recursive-branch-seed d env state)
@@ -10635,6 +11146,7 @@
1063511146 =/ product=itype ?~(result [%var id] u.result)
1063611147 =/ st=istate state.p.sam(next +(id))
1063711148 =/ seed=itype [%fn typ.p.sam product]
11149+ =? seed ?=(^ peeled) (itype-unface seed sub.st)
1063811150 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
1063911151 =/ body=expr
1064011152 ?- -.gate
@@ -10646,7 +11158,9 @@
1064611158 ?: ?=(%| -.out) out
1064711159 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
1064811160 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
10649− [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]
11161+ =/ typ=itype [%fn typ.p.sam typ.p.out]
11162+ =? typ ?=(^ peeled) (itype-unface typ u.uni)
11163+ [%& typ state.p.out(sub u.uni)]
1065011164::
1065111165++ dependency-root
1065211166 |= names=(list term)
@@ -10754,7 +11268,7 @@
1075411268:: Infer a cyclic component with one monomorphic seed per gate. All members
1075511269:: must succeed before any scheme is available; pending constraints and
1075611270:: 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=?]
1075811272+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
1075911273++ seed-gate-group
1076011274 |= [ds=(list def) env=ienv state=istate]
@@ -10762,7 +11276,9 @@
1076211276 ?~ ds [%& [~ state]]
1076311277 =/ d=def i.ds
1076411278 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
10765− =/ gate=expr val.d
11279+ :: A ++ whose body is (unface |= …) is a gate too, unfaced
11280+ =/ peeled=(unit expr) (unfaced-gate val.d env state)
11281+ =/ gate=expr ?~(peeled val.d u.peeled)
1076611282 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
1076711283 [%| ["recursive group contains a non-gate" ~]]
1076811284 =/ initial=istate (reserve-def-caps gate state)
@@ -10780,7 +11296,8 @@
1078011296 * !!
1078111297 ==
1078211298 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
10783− =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]
11299+ =? seed ?=(^ peeled) (itype-unface seed sub.state.p.sam)
11300+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam ?=(^ peeled)]
1078411301 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
1078511302 =/ rest=igate-seeds $(ds t.ds, state after)
1078611303 ?: ?=(%| -.rest) rest
@@ -10820,6 +11337,7 @@
1082011337 ?: (constrained-capitals caps.entry sub.state)
1082111338 [%| ["explicit capital constraints are not supported by partial inference" ~]]
1082211339 =/ typ=itype (itype-normalize typ.entry sub.state)
11340+ =? typ unfaced.entry (itype-unface typ ~)
1082311341 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
1082411342 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
1082511343 [%| ["recursive group needs unsupported inference" ~]]
@@ -10828,7 +11346,7 @@
1082811346 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
1082911347 =/ rest=(each ienv idiag) $(entries t.entries)
1083011348 ?: ?=(%| -.rest) rest
10831− [%& [[name.entry [typ vars]] p.rest]]
11349+ [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]
1083211350::
1083311351++ infer-gate-group
1083411352 |= [ds=(list def) env=ienv state=istate]
@@ -10873,7 +11391,7 @@
1087311391 `[entry u.rest]
1087411392::
1087511393
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])]
1087711395+$ iadj (map term (list term))
1087811396+$ ivisited (map term ?)
1087911397+$ iwork (list [name=term done=?])
@@ -10969,7 +11487,7 @@
1096911487++ add-groups
1097011488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
1097111489 ^- iresolved
10972− ?~ components [env grouped artifacts]
11490+ ?~ components [env grouped artifacts ~]
1097311491 =/ component=(list term) i.components
1097411492 ?. (graph-cycle component graph) $(components t.components)
1097511493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -11010,11 +11528,13 @@
1101011528 =? artifacts ?=(^ u.finalized)
1101111529 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
1101211530 =? 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]
1101411532++ add-supported-defs-core
1101511533 |= [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)]
11017− ?~ ds [env artifacts]
11534+ ^- [env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11535+ =/ failures=(list [name=term diag=idiag]) ~
11536+ |-
11537+ ?~ ds [env artifacts (flop failures)]
1101811538 =/ d=def i.ds
1101911539 ?: ?=(%mold -.d) $(ds t.ds)
1102011540 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -11025,37 +11545,34 @@
1102511545 =. gate-defs.initial checked
1102611546 =. head-evidence.initial heads
1102711547 =. 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
1102911550 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11551+ ?: ?=(%| -.result)
11552+ =/ failure=idiag
11553+ ?: (definite-diag p.result) p.result
11554+ ?: ?=(%| -.plain) p.plain
11555+ p.result
11556+ =? failures (definite-diag failure) [[name.d failure] failures]
11557+ $(ds t.ds)
1103011558 =/ added=(unit iadded-definition)
1103111559 (add-supported-result d result initial env checked artifacts)
1103211560 ?~ added $(ds t.ds)
1103311561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
1103411562::
11035−:: Full checking discards unsupported definitions. On that failure path only,
11036−:: retry a bounded number of missing definitions to explain a pending tag
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
11040− |= [ds=(list def) env=ienv base=istate fuel=@ud]
11563+:: Retry one unresolved definition to explain a pending tag. The gate
11564+:: evidence is built from the whole module, not only this definition.
11565+++ module-pending-tag-one
11566+ |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]
1104111567 ^- (unit [at=span msg=tape])
11042− =/ checked=(map term def) (direct-checked-gates ds env)
11043− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
11044− |-
11045− ?~ ds ~
11046− ?: =(0 fuel) ~
11047− =/ d=def i.ds
11048− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
11049− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
11568+ ?. ?=(%value -.d) ~
11569+ ?^ (ienv-lookup name.d env) ~
1105011570 =/ initial=istate base(gate-defs checked, head-evidence heads)
1105111571 =. initial (reserve-def-caps val.d initial)
1105211572 =/ result=iresult (infer-fragment val.d env initial)
1105311573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11054− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
11055− =/ pending=(unit [at=span msg=tape])
11056− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11057− ?^ pending pending
11058− $(ds t.ds, fuel (dec fuel))
11574+ ?: ?=(%| -.result) ~
11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
1105911576::
1106011577++ resolve-groups-core
1106111578 |= [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 @@
1107111588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1107211589 =/ ordered=(list def) (dependency-order ds components)
1107311590 |-
11074− =/ next=[env=ienv artifacts=(list iwidth-definition)]
11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1107511592 (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)
1107611593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
1107711594 =. grec-index.initial index
1107811595 =/ 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)
1108011597 $(env env.out, grouped grouped.out, artifacts artifacts.out)
1108111598::
1108211599:: +dependency-order: the value definitions, dependencies first
@@ -11948,13 +12465,29 @@
1194812465 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
1194912466 ?^ first first
1195012467 $(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.
1195112470++ duplicate-edits
1195212471 |= edits=(list edit)
1195312472 ^- (unit idiag)
12473+ =| seen=(list edit)
12474+ |- ^- (unit idiag)
1195412475 ?~ edits ~
11955− =/ first (duplicate-expr val.i.edits)
12476+ =/ e=edit i.edits
12477+ =/ prior=(list edit)
12478+ (skim seen |=(p=edit (wing-overlap (flop names.p) (flop names.e))))
12479+ ?^ prior
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")]
12484+ ==
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]
12488+ =/ first (duplicate-expr val.e)
1195612489 ?^ first first
11957− $(edits t.edits)
12490+ $(edits t.edits, seen [e seen])
1195812491++ duplicate-arms
1195912492 |= arms=(list arm)
1196012493 ^- (unit idiag)
@@ -12027,59 +12560,142 @@
1202712560 ==
1202812561 [n $(imports t.imports)]
1202912562::
12030−++ reserved-proj-sample
12563+:: +reserved-name: whether n names a reserved operation
12564+::
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.
12568+++ reserved-name
12569+ |= n=term
12570+ ^- ?
12571+ |(=(n %proj) =(n %unface))
12572+++ reserved-sample
1203112573 |= sam=sample
1203212574 ^- ?
1203312575 ?- -.sam
12034− %bind =(name.sam %proj)
12035− %face =(name.sam %proj)
12036− %pun =(name.sam %proj)
12037− %cell (lien items.sam reserved-proj-sample)
12576+ %bind (reserved-name name.sam)
12577+ %face (reserved-name name.sam)
12578+ %pun (reserved-name name.sam)
12579+ %cell (lien items.sam reserved-sample)
1203812580 * |
1203912581 ==
12040−++ reserved-proj-pattern
12582+++ reserved-pattern
1204112583 |= p=pattern
1204212584 ^- ?
1204312585 ?- -.p
12044− %bind =(name.p %proj)
12045− %cell (lien items.p reserved-proj-pattern)
12586+ %bind (reserved-name name.p)
12587+ %cell (lien items.p reserved-pattern)
1204612588 * |
1204712589 ==
12048−++ reserved-proj-def
12590+++ reserved-def
1204912591 |= d=def
1205012592 ^- ?
12051− ?: =(name.d %proj) &
12052− ?: ?=(%value -.d) (reserved-proj-expr val.d)
12593+ ?: (reserved-name name.d) &
12594+ ?: ?=(%value -.d) (reserved-expr val.d)
1205312595 |
12054−++ reserved-proj-expr
12596+++ reserved-expr
1205512597 |= e=expr
1205612598 ^- ?
1205712599 ?- -.e
12058− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12059− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12060− %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
12600+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12601+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12602+ %change (lien edits.e |=(p=edit (reserved-expr val.p)))
1206112603 %pair $(e val.e)
1206212604 %unit $(e val.e)
1206312605 %group $(e inner.e)
12064− %list (lien items.e reserved-proj-expr)
12065− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
12066− ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
12606+ %list (lien items.e reserved-expr)
12607+ %tuple (lien items.e |=(i=item (reserved-expr val.i)))
12608+ ?(%gate %gate-wide) |((reserved-sample sample.e) $(e body.e))
1206712609 %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))
1206912611 %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)))))
12071− %body |((lien defs.e reserved-proj-def) $(e final.e))
12612+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-pattern pat.a) (reserved-expr val.a)))))
12613+ %body |((lien defs.e reserved-def) $(e final.e))
1207212614 * |
1207312615 ==
1207412616::
12075−++ module-has-reserved-proj
12617+++ module-has-reserved
1207612618 |= mod=module
1207712619 ^- ?
1207812620 =/ imported=(list term) (import-binding-names imports.mod)
1207912621 =/ vals=(list term) (global-value-names defs.mod)
1208012622 =/ molds=imolds (collect-simple-molds defs.mod)
1208112623 =/ 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))
12625+::
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
12635+ =/ n=term
12636+ ?- -.imp
12637+ %jibb face.imp
12638+ %sur name.imp
12639+ %mark mark.imp
12640+ ==
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)
12644+ ?^ earlier
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)
12652+ ?~ defs ~
12653+ =/ d=def i.defs
12654+ =/ n=term name.d
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)
12658+ ?^ imported
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)
12662+ ?^ earlier
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)]]
12667+ ?: ?=(%value -.d)
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)]
12679+ ^- @t
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 ~
12686+ ?~ prelude ~
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
12692+ |= d=def
12693+ ?& =(name.d name.u.prelude.diagnostic)
12694+ |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))
12695+ ==
12696+ ?~ matching ~
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)])
1208312699::
1208412700++ module-scope-valid
1208512701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -12088,7 +12704,7 @@
1208812704 =/ vals=(list term) (global-value-names defs.mod)
1208912705 =/ molds=imolds (collect-simple-molds defs.mod)
1209012706 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12091− ?: (module-has-reserved-proj mod) |
12707+ ?: (module-has-reserved mod) |
1209212708 ?. %+ levy imported
1209312709 |= n=term
1209412710 &((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 @@
1251113127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
1251213128 `[u.name at.s]
1251313129::
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]
13135+ ^- (unit @t)
13136+ ?~ ds ~
13137+ =/ d=def i.ds
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])
13145+ ?: =(0 fuel) ~
13146+ (module-pending-tag-one d env base checked heads)
13147+ ?^ pending
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)
13150+ ?^ shadow
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)
13154+::
1251413155:: Cache only completed interfaces for this invocation. The source bundle,
1251513156:: imported Hoon types and prelude are fixed for the whole graph. Check the
1251613157:: active path and duplicate sources before consulting it, so a cache hit
@@ -12777,7 +13418,7 @@
1277713418 ^- ?
1277813419 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
1277913420 =/ derived=(list term) (weld path-names poke-names)
12780− ?: (lien derived |=(n=term =(n %proj))) |
13421+ ?: (lien derived reserved-name) |
1278113422 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
1278213423 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
1278313424::
@@ -12809,7 +13450,7 @@
1280913450 =/ clashes=(list term)
1281013451 %+ skip names
1281113452 |= n=term
12812− ?| =(n %proj)
13453+ ?| (reserved-name n)
1281313454 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
1281413455 ==
1281513456 ?~ clashes ~
@@ -13584,7 +14225,7 @@
1358414225 =/ action=term %poke
1358514226 =/ ordinary=(list def) ds
1358614227 =/ derived=(list term) ~[%state action]
13587− ?: (lien derived |=(n=term =(n %proj))) [%| ~]
14228+ ?: (lien derived reserved-name) [%| ~]
1358814229 =/ outer=(list term)
1358914230 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
1359014231 =/ clashes=(list term)
@@ -13771,7 +14412,7 @@
1377114412 ?~ recovered ~
1377214413 ?. ?=(~ vars.u.recovered) ~
1377314414 ?. ?=(~ (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]
1377514416::
1377614417++ program-inferred-slot
1377714418 |= [typ=itype name=(unit term)]
@@ -13927,7 +14568,7 @@
1392714568 ?~ recovered ~
1392814569 ?. ?=(~ vars.u.recovered) ~
1392914570 ?. ?=(~ (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]
1393114572::
1393214573+$ iview-site [xs=expr mapper=term]
1393314574++ program-view-site
@@ -14254,7 +14895,7 @@
1425414895 ?~ recovered ~
1425514896 ?. ?=(~ vars.u.recovered) ~
1425614897 ?. ?=(~ (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]
1425814899::
1425914900:: Recover exactly one direct keyed each/turn row mapper, then its view.
1426014901:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -14476,7 +15117,7 @@
1447615117 ?~ recovered ~
1447715118 ?. ?=(~ vars.u.recovered) ~
1447815119 ?. ?=(~ (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]
1448015121::
1448115122:: The model a direct program's initializer must produce. Update's written
1448215123:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -14633,7 +15274,7 @@
1463315274 ?~ recovered ~
1463415275 ?. ?=(~ vars.u.recovered) ~
1463515276 ?. ?=(~ (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]
1463715278::
1463815279++ derived-poke-command-scheme
1463915280 |= [prelude=ifile action=itype]
@@ -14801,9 +15442,9 @@
1480115442 (direct-prelude-evidence ds prelude.initial)
1480215443 ?~ heads resolution
1480315444 =/ 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])]
1480515446 (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]
1480715448::
1480815449:: A static main may retain a generic element message in its ordinary
1480915450:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -15019,6 +15660,9 @@
1501915660 !(lien prelude-molds |=(m=term =(m n)))
1502015661 ==
1502115662 ==
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) ~]]
1502215666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1502315667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1502415668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -15067,6 +15711,9 @@
1506715711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
1506815712 =/ checking=module mod(defs ds)
1506915713 ?. (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) ~]]
1507015717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1507115718 =/ vals=(list term) (global-value-names ds)
1507215719 =/ 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 @@
1514215789 ?~ store-parts ds
1514315790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
1514415791 ?. (module-values-complete required env)
15145− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15146− ?^ pending
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.
15792+ =/ components=icomponents (graph-components required (global-value-names required))
15793+ =/ ordered=(list def) (dependency-order required components)
1514915794 =/ 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)
15151− ?^ shadow
15152− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15153− [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
15795+ =/ checked=(map term def) (direct-checked-gates required env)
15796+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)
15797+ =/ diagnostic=(unit @t)
15798+ (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)
15799+ ?^ diagnostic [%| [u.diagnostic ~]]
1515415800 =/ missing=(unit term) (module-missing-value required env)
1515515801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
1515615802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
@@ -15354,8 +16000,8 @@
1535416000 ?: ?=(%| -.parsed) (show-error src p.parsed)
1535516001 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
1535616002 ?^ duplicate (duplicate-fields-report file src u.duplicate)
15357− ?: (module-has-reserved-proj p.parsed)
15358− 'module has reserved proj name'
16003+ ?: (module-has-reserved p.parsed)
16004+ 'module has a reserved proj or unface name'
1535916005 =/ ds=(list def) defs.p.parsed
1536016006 =/ molds=imolds (collect-simple-molds ds)
1536116007 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -15433,7 +16079,7 @@
1543316079 =. head-evidence.initial heads
1543416080 =. initial (reserve-def-caps val.d initial)
1543516081 =/ result=iresult
15436− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
16082+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))
1543716083 (infer-recursive-gate d env initial)
1543816084 (infer-fragment val.d env initial)
1543916085 ?: ?=(%| -.result)
@@ -15465,7 +16111,8 @@
1546516111 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
1546616112 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
1546716113 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
15468− =/ printable=itype (canonical-itype typ vars)
16114+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.result sub.state.p.result)
16115+ =/ printable=itype (canonical-itype named)
1546916116 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
1547016117 $(ds t.ds, lines [line lines])
1547116118:: Experimental module-owned pending-constraint generalization only.
@@ -15562,7 +16209,7 @@
1556216209 =/ normalized=itype (itype-normalize typ sub.state)
1556316210 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
1556416211 =/ 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)
1556616213::
1556716214+$ dgcommit [env=ienv state=istate]
1556816215:: A branch literal must not acquire a value face through replay.
@@ -15995,20 +16642,21 @@
1599516642 ?~ env `+(top)
1599616643 =/ sc=ischeme scheme.i.env
1599716644 ?: (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))))
1599916646::
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)
1600116649::
1600216650++ itype-max-id
1600316651 |= [t=itype top=@ud]
1600416652 ^- @ud
1600516653 ?- -.t
16006− %var (max top id.t)
16007− %fvar (max top id.t)
16008− %avar (max top id.t)
16009− %rvar (max top id.t)
16010− %nvar (max top id.t)
16011− %rnvar (max top id.t)
16654+ %var (max top (var-count id.t))
16655+ %fvar (max top (var-count id.t))
16656+ %avar (max top (var-count id.t))
16657+ %rvar (max top (var-count id.t))
16658+ %nvar (max top (var-count id.t))
16659+ %rnvar (max top (var-count id.t))
1601216660 %tag (max top id.t)
1601316661 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
1601416662 %collection (itype-max-ids args.t top)