@@ -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
@@ -4614,7 +4801,10 @@
46144801:: Restricted-number promotion considers written capitals only; if there
46154802:: are none, it skips the otherwise unnecessary environment traversal.
46164803:: Bare @ is a separate unrestricted atom type. A directional fit check
4617−:: permits concrete atoms to widen to it, never the reverse. A fit that
4804+:: permits concrete atoms to widen to it, never the reverse. A bare
4805+:: decimal is a @ud: its variable binds only @ud or @u, it fits @ and *,
4806+:: and +decimal-misfit names it where it meets another aura (S4); a
4807+:: ++ generic over its aura generalizes it to any aura. A fit that
46184808:: needs a not-yet-implemented constraint remains unsupported. Named unions
46194809:: retain origin and ordered arguments, including phantom arguments, apart
46204810:: from their display name. Generic cases must be disjoint for all arguments.
@@ -4634,6 +4824,14 @@
46344824:: proofs to fewer than 1,024 cells; the projection planner has a separate
46354825:: 4,096-step bound. These are inference limits, not language limits.
46364826::
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+::
46374835:: Supported API imports derive request-gate types atomically for multiple
46384836:: paths, including one typed segment or one diff fold per case. Their checked
46394837:: ordinary definitions, mark molds and supported poke constructor are also
@@ -4845,7 +5043,8 @@
48455043:: +itype-unify: consistent substitutions, or ~ for a mismatch
48465044::
48475045:: Different concrete auras conflict. A variable may become an atom or
4848−:: a function, but cannot contain itself. Aura-only variables and faces
5046+:: a function, but cannot contain itself. A decimal's variable binds
5047+:: only @ud or @u (+decimal-aura). Aura-only variables and faces
48495048:: require further distinctions before this supports general Jibb.
48505049::
48515050++ itype-unify
@@ -4894,10 +5093,10 @@
48945093 ?: &(?=(%rnvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
48955094 ?: &(?=(%avar -.a) ?=(%rnvar -.b)) `[[id.a b] sub]
48965095 ?: ?=(%rnvar -.a)
4897− ?. |(?=(%rnvar -.b) ?=(%atom -.b)) ~
5096+ ?. |(?=(%rnvar -.b) &(?=(%atom -.b) (decimal-aura aura.b))) ~
48985097 `[[id.a b] sub]
48995098 ?: ?=(%rnvar -.b)
4900− ?. ?=(%atom -.a) ~
5099+ ?. &(?=(%atom -.a) (decimal-aura aura.a)) ~
49015100 `[[id.b a] sub]
49025101 ?: &(?=(%avar -.a) ?=(%rvar -.b)) `[[id.a b] sub]
49035102 ?: &(?=(%rvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
@@ -4908,14 +5107,15 @@
49085107 ?. ?=(%atom -.a) ~
49095108 `[[id.b a] sub]
49105109 :: The narrower decimal constraint survives a match with an atom
4911− :: variable; decimal syntax alone does not make it a loobean.
5110+ :: variable; decimal syntax alone does not make it a loobean. A
5111+ :: concrete aura takes a decimal only if it is @ud or @u.
49125112 ?: &(?=(%nvar -.a) ?=(%avar -.b)) `[[id.b a] sub]
49135113 ?: &(?=(%avar -.a) ?=(%nvar -.b)) `[[id.a b] sub]
49145114 ?: ?=(%nvar -.a)
4915− ?. |(?=(%nvar -.b) ?=(%atom -.b)) ~
5115+ ?. |(?=(%nvar -.b) &(?=(%atom -.b) (decimal-aura aura.b))) ~
49165116 `[[id.a b] sub]
49175117 ?: ?=(%nvar -.b)
4918− ?. ?=(%atom -.a) ~
5118+ ?. &(?=(%atom -.a) (decimal-aura aura.a)) ~
49195119 `[[id.b a] sub]
49205120 ?: ?=(%avar -.a)
49215121 ?. |(?=(%avar -.b) ?=(%atom -.b) ?=(%any-atom -.b) ?=(%flag -.b)) ~
@@ -4939,6 +5139,35 @@
49395139 $(a tal.a, b tal.b, sub u.first)
49405140 ~
49415141::
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+::
49425171+$ igf-form [typ=itype sub=isub left=@ud]
49435172+$ igf-forms [types=(list itype) sub=isub left=@ud]
49445173++ itype-gate-free-forms
@@ -5060,6 +5289,16 @@
50605289 ?. =(i.a i.b) |
50615290 $(a t.a, b t.b)
50625291::
5292+:: +decimal-aura: whether a bare decimal fits an atom of this aura
5293+::
5294+:: A decimal is a @ud, so as in Hoon it fits @ud and its ancestors
5295+:: @u and @; every other aura takes its own literal (S4).
5296+::
5297+++ decimal-aura
5298+ |= aura=@ta
5299+ ^- ?
5300+ (aura-prefix aura %ud)
5301+::
50635302:: Related auras in a structural unification need a common-type rule;
50645303:: until that rule is implemented, report an unknown rather than error.
50655304::
@@ -5795,6 +6034,24 @@
57956034 ["canonicalization should retain gate-free variables" problems]
57966035 =? problems !=((show-atom-constraint canonical-free) " where A contains no gates")
57976036 ["the printer should show gate-free constraints" problems]
6037+ =/ decimal=itype [%nvar 50]
6038+ =? problems ?=(~ (itype-unify decimal num ~))
6039+ ["a decimal should unify with @ud" problems]
6040+ =? problems ?=(~ (itype-unify [%atom %u] decimal ~))
6041+ ["a decimal should unify with @u" problems]
6042+ =? problems ?=(^ (itype-unify decimal [%atom %dr] ~))
6043+ ["a decimal should not unify with @dr" problems]
6044+ =? problems ?=(^ (itype-unify [%atom %ux] decimal ~))
6045+ ["a decimal should not unify with @ux" problems]
6046+ =/ restricted=(unit isub) (itype-unify decimal [%rvar 51] ~)
6047+ =? problems |(?=(~ restricted) ?=(^ (itype-unify [%rvar 51] [%atom %p] u.restricted)))
6048+ ["arithmetic should keep a decimal's aura rule" problems]
6049+ =/ decimal-any=ifit (itype-fit decimal [%any-atom ~] ~ 52)
6050+ =? problems !?=(%ok -.decimal-any)
6051+ ["a decimal should fit @" problems]
6052+ =/ decimal-noun=ifit (itype-fit decimal [%noun ~] ~ 52)
6053+ =? problems !?=(%ok -.decimal-noun)
6054+ ["a decimal should fit a noun" problems]
57986055 problems
57996056::
58006057:: The expression inference below is deliberately a fragment: bindings,
@@ -6342,15 +6599,67 @@
63426599 ^- ?
63436600 (itype-var-is-gate-free-fuel n t 256)
63446601::
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+::
63456636++ canonical-itype
63466637 |= [t=itype vars=(list @ud)]
63476638 ^- itype
6639+ =/ names=(list @t) (turn vars var-name)
6640+ =/ used=(list @t) ~
63486641 =/ ren=isub ~
63496642 =/ n=@ud 0
63506643 |-
63516644 ?~ vars (itype-rename t ren)
6352− =/ 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])))
6353− $(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.
63546663::
63556664++ instantiate-scheme
63566665 |= [scheme=ischeme state=istate]
@@ -6359,12 +6668,13 @@
63596668 =/ vars=(list @ud) vars.scheme
63606669 |-
63616670 ?~ vars [(itype-rename typ.scheme ren) state]
6671+ =/ fresh=@ud (named-var (var-name i.vars) next.state)
63626672 =/ replacement=itype
6363− ?:((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])))
63646674 :: A generalized atom variable is a valid origin for re-generalizing
63656675 :: an alias, just as a sample binder is.
63666676 =/ st=istate state(next +(next.state))
6367− =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]
6677+ =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [fresh binders.state]
63686678 $(vars t.vars, ren [[i.vars replacement] ren], state st)
63696679::
63706680++ icap-lookup
@@ -7224,7 +7534,8 @@
72247534 ?: in-mold.state ~
72257535 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
72267536 ?^ n `[[%var u.n] state]
7227− `[[%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])]
72287539 * ~
72297540 ==
72307541::
@@ -7257,12 +7568,12 @@
72577568 ^- isample-result
72587569 ?- -.s
72597570 %bind
7260− ?: |(=(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))))
72617572 [%| "sample shadows a name"]
72627573 =/ t=itype [%var next.state]
72637574 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
72647575 %face
7265− ?: |(=(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))))
72667577 [%| "sample shadows a name"]
72677578 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
72687579 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -7330,7 +7641,7 @@
73307641 |-
73317642 ?~ ds &
73327643 ?: ?=(%mold -.i.ds) $(ds t.ds)
7333− ?: =(name.i.ds %proj) |
7644+ ?: (reserved-name name.i.ds) |
73347645 ?. (unique-value-name name.i.ds names) |
73357646 ?: ?=(^ (ienv-lookup name.i.ds env)) |
73367647 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -7354,7 +7665,7 @@
73547665 |-
73557666 ?~ locals &
73567667 =/ n=term name.i.locals
7357− ?: =(n %proj) |
7668+ ?: (reserved-name n) |
73587669 ?. (unique-value-name n names) |
73597670 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
73607671 ?: (lien marks.state |=(m=term =(n m))) |
@@ -7504,7 +7815,8 @@
75047815 ^- istate
75057816 ?~ sites state
75067817 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)
7507− $(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]))
75087820::
75097821++ reserve-def-caps
75107822 |= [e=expr state=istate]
@@ -7678,7 +7990,8 @@
76787990 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
76797991 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
76807992 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
7681− $(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 &)
76827995::
76837996:: Try complete cyclic local groups after individual definitions stall.
76847997:: Components with non-gates or unresolved constraints stay unavailable.
@@ -7768,6 +8081,8 @@
77688081 ?: &(?=(%collection -.expected) =(%list name.expected) (context-list-expression e))
77698082 (infer-list-context e expected env state context)
77708083 ?: ?=(%branch -.e)
8084+ =/ named=(unit idiag) (branch-tag-name e env state)
8085+ ?^ named [%| u.named]
77718086 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[expected context])
77728087 ?^ empty-list u.empty-list
77738088 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
@@ -7808,6 +8123,8 @@
78088123 ?^ missing [%| u.missing]
78098124 =/ nested=(unit idiag) (nested-missing-tag e typ.p.value expected sub.state.p.value next.state.p.value context)
78108125 ?^ nested [%| u.nested]
8126+ =/ decimal=(unit idiag) (decimal-misfit e typ.p.value expected sub.state.p.value next.state.p.value)
8127+ ?^ decimal [%| u.decimal]
78118128 ?: &(?=(%collection -.expected) =(%list name.expected))
78128129 [%| ["branch arm does not fit its expected list" ~[[context "expected list"] [(span-of e) "branch arm"]]]]
78138130 ?: ?=(%flag -.expected)
@@ -7873,11 +8190,15 @@
78738190 =/ fit=ifit (itype-fit typ.p.tail target sub.state.p.tail next.state.p.tail)
78748191 ?: ?=(%unknown -.fit) [%| ["list tail constraint is not supported by partial inference" ~]]
78758192 ?: ?=(%bad -.fit)
8193+ =/ decimal=(unit idiag) (decimal-misfit val.i.t.items.e typ.p.tail target sub.state.p.tail next.state.p.tail)
8194+ ?^ decimal [%| u.decimal]
78768195 [%| ["list tail does not fit its expected type" ~[[context (site-type-note "expected list" target sub.state.p.tail)] [(span-of val.i.t.items.e) (site-type-note "list tail" typ.p.tail sub.state.p.tail)]]]]
78778196 [%& target state.p.tail(sub sub.fit, next next.fit)]
78788197::
8198+:: done holds the items already checked, the last first, so that a
8199+:: decimal among them can be blamed when a later item fixes its aura.
78798200++ infer-open-list-items
7880− |= [items=(list expr) expected=itype env=ienv state=istate context=span]
8201+ |= [items=(list expr) expected=itype env=ienv state=istate context=span done=(list expr)]
78818202 ^- iresult
78828203 ?~ items [%& expected state]
78838204 =/ target=itype (itype-walk expected sub.state)
@@ -7893,10 +8214,18 @@
78938214 ?: ?=(%bad -.fit)
78948215 ?: |((itype-family-related typ.p.value target sub.state.p.value) (itype-has-any-atom typ.p.value sub.state.p.value) (itype-has-any-atom target sub.state.p.value))
78958216 [%| ["list item widening is not supported by partial inference" ~]]
8217+ =/ decimal=(unit idiag) (decimal-misfit i.items typ.p.value target sub.state.p.value next.state.p.value)
8218+ ?^ decimal [%| u.decimal]
8219+ =/ earlier=(list expr) (flop done)
8220+ |- ^- iresult
8221+ ?^ earlier
8222+ =/ found=(unit idiag) (decimal-misfit-at i.earlier typ.p.value sub.state.p.value)
8223+ ?^ found [%| u.found]
8224+ $(earlier t.earlier)
78968225 [%| ["list items do not have compatible types" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
78978226 ?: (itype-has-tag (itype-normalize expected sub.fit))
78988227 [%| ["list item needs context in partial inference" ~]]
7899− $(items t.items, state state.p.value(sub sub.fit, next next.fit))
8228+ $(items t.items, state state.p.value(sub sub.fit, next next.fit), done [i.items done])
79008229::
79018230++ infer-list-items
79028231 |= [items=(list expr) expected=itype env=ienv state=istate context=span]
@@ -7917,6 +8246,8 @@
79178246 ?^ missing [%| u.missing]
79188247 =/ nested=(unit idiag) (nested-missing-tag i.items typ.p.value target sub.state.p.value next.state.p.value context)
79198248 ?^ nested [%| u.nested]
8249+ =/ decimal=(unit idiag) (decimal-misfit i.items typ.p.value target sub.state.p.value next.state.p.value)
8250+ ?^ decimal [%| u.decimal]
79208251 [%| ["list item does not fit its expected type" ~[[context (site-type-note "expected item" target sub.state.p.value)] [(span-of i.items) (site-type-note "list item" typ.p.value sub.state.p.value)]]]]
79218252 $(items t.items, state state.p.value(sub sub.fit, next next.fit))
79228253::
@@ -8014,7 +8345,7 @@
80148345 [%| ["list branch pattern is not supported by partial inference" ~]]
80158346 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
80168347 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]
8017− ?: |(=(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)))))
80188349 [%| ["pattern binder shadows a name" ~]]
80198350 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
80208351 =/ left=iresult
@@ -8051,7 +8382,7 @@
80518382 [%| ["unit branch pattern is not supported by partial inference" ~]]
80528383 =/ binder=(unit term) ?:(first-empty second-name first-name)
80538384 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]
8054− ?: |(=(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))))
80558386 [%| ["pattern binder shadows a name" ~]]
80568387 =/ payload=(unit itype) (unit-union-payload typ)
80578388 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -8158,11 +8489,83 @@
81588489 ^- (unit ienv)
81598490 =. t ?:(?=(%face -.t) body.t t)
81608491 ?: ?=(%bind -.p)
8161− ?: |(=(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)))) ~
81628493 `[[name.p [t ~]] env]
81638494 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
81648495 `env
81658496::
8497+:: +branch-tag-name: a ?- pattern name that spells one of the subject's tags
8498+::
8499+:: A name in a pattern binds, so `stop` written for `%stop` would
8500+:: catch every case left. Where the subject's type at a name's
8501+:: position is a union, or a one-case mold, with a case whose constant
8502+:: there is the term the name spells, the name is an error (Grammar,
8503+:: Patterns). Every path that checks a ?- asks this first, so they
8504+:: agree; it infers the subject apart and drops the state it leaves.
8505+:: A subject that fails, or whose type isn't known yet, is left to the
8506+:: path. Samples aren't patterns: every sample name binds.
8507+++ branch-tag-name
8508+ |= [e=expr env=ienv state=istate]
8509+ ^- (unit idiag)
8510+ ?. ?=(%branch -.e) ~
8511+ ?. (lien arms.e |=(a=arm (union-pattern-has-bind pat.a))) ~
8512+ =/ subject=iresult (infer-fragment subject.e env state)
8513+ ?: ?=(%| -.subject) ~
8514+ =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
8515+ =/ arms=(list arm) arms.e
8516+ |-
8517+ ?~ arms ~
8518+ =/ found=(unit [at=span name=term]) (tag-name-pattern pat.i.arms typ ~)
8519+ ?~ found $(arms t.arms)
8520+ =/ name=tape (trip name.u.found)
8521+ :- ~
8522+ :- "`{name}` binds a name, but the subject's type has `%{name}` here; write %{name}, or * for a catch-all"
8523+ ~[[(span-of subject.e) "subject"] [at.u.found "pattern name"]]
8524+::
8525+:: +tag-name-pattern: the first name in p that t types by a tag
8526+::
8527+:: The walk enters faces, cells and unions, and of a union only the
8528+:: cases a cell pattern can match, so `[t %draft]` reads t at @t. It
8529+:: stops at atoms, `*`, variables, collections and recursive molds,
8530+:: and at a generic union's argument positions, which a type variable
8531+:: types in its mold, as u in `[~ u=A]`.
8532+++ tag-name-pattern
8533+ |= [p=pattern t=itype args=(list itype)]
8534+ ^- (unit [at=span name=term])
8535+ ?. ?=(?(%bind %cell) -.p) ~
8536+ ?: ?=(%face -.t) $(t body.t)
8537+ ?: (lien args |=(a=itype =(a t))) ~
8538+ ?: ?=(%union -.t)
8539+ =/ inner=(list itype) (weld args.t args)
8540+ =/ cases=(list itype) cases.t
8541+ |-
8542+ ?~ cases ~
8543+ ?: &(?=(%cell -.p) =(%none (union-pattern p i.cases))) $(cases t.cases)
8544+ =/ found=(unit [at=span name=term]) (tag-name-pattern p i.cases inner)
8545+ ?^ found found
8546+ $(cases t.cases)
8547+ ?: ?=(%cell -.p) (tag-name-items items.p t args)
8548+ ?. ?=(%const -.t) ~
8549+ ?. &(=(%term form.literal.t) =(%tas aura.literal.t) =(name.p val.literal.t)) ~
8550+ `[at.p name.p]
8551+::
8552+:: +tag-name-items: +tag-name-pattern along a cell pattern's items
8553+::
8554+:: As in +union-pattern-items, the last item takes the rest of the
8555+:: spine. A union mid-spine is read as the rest of the pattern.
8556+++ tag-name-items
8557+ |= [ps=(list pattern) t=itype args=(list itype)]
8558+ ^- (unit [at=span name=term])
8559+ ?~ ps ~
8560+ ?~ t.ps (tag-name-pattern i.ps t args)
8561+ ?: ?=(%face -.t) $(t body.t)
8562+ ?: (lien args |=(a=itype =(a t))) ~
8563+ ?: ?=(%union -.t) (tag-name-pattern [%cell at.i.ps ps] t args)
8564+ ?. ?=(%cell -.t) ~
8565+ =/ head=(unit [at=span name=term]) (tag-name-pattern i.ps hed.t args)
8566+ ?^ head head
8567+ $(ps t.ps, t tal.t)
8568+::
81668569:: Split loobean fields into finite refinements for partial patterns.
81678570:: Keep original cases for binder types and preserve whole-case matching
81688571:: before trying refinements. Cap products at 64; unknown, empty or opaque
@@ -8210,6 +8613,8 @@
82108613 ^- (unit iresult)
82118614 ?> ?=(%branch -.e)
82128615 ?: ?=(%| -.subject) `subject
8616+ =/ decimal=(unit idiag) (decimal-arms-misfit arms.e typ.p.subject sub.state.p.subject)
8617+ ?^ decimal `[%| u.decimal]
82138618 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
82148619 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
82158620 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
@@ -8248,6 +8653,8 @@
82488653 ^- (unit iresult)
82498654 ?> ?=(%branch -.e)
82508655 ?: ?=(%| -.subject) `subject
8656+ =/ decimal=(unit idiag) (decimal-arms-misfit arms.e typ.p.subject sub.state.p.subject)
8657+ ?^ decimal `[%| u.decimal]
82518658 =/ typ=itype (itype-normalize typ.p.subject sub.state.p.subject)
82528659 ?. ?=(%union -.typ) `[%| ["branch is not supported by partial inference" ~]]
82538660 =/ live=(unit (list itype)) (itype-live-cases cases.typ sub.state.p.subject caps.state.p.subject 4.096)
@@ -8608,7 +9015,9 @@
86089015 `subject
86099016::
86109017:: Infer changes only against a fully known record spine. Retain the
8611−:: 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.
86129021++ change-spine-known
86139022 |= [t=itype sub=isub]
86149023 ^- ?
@@ -8620,26 +9029,87 @@
86209029 $(t tal.t)
86219030::
86229031++ infer-change-edits
8623− |= [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))]
86249033 ^- iresult
86259034 ?~ edits [%& target state]
86269035 =/ entry=edit i.edits
8627− ?: (lien seen |=(name=term =(name name.entry)))
9036+ =/ outer=(list term) (flop names.entry)
9037+ ?: (lien seen |=(prior=(list term) (wing-overlap prior outer)))
86289038 [%| ["repeated change fields are not supported by partial inference" ~]]
86299039 ?. (change-spine-known target sub.state)
86309040 [%| ["change target needs a known record in partial inference" ~]]
8631− =/ found=(list itype) (record-fields-named name.entry target sub.state)
8632− ?~ found
8633− [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
8634− ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
8635− =/ 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
86369044 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
86379045 ?: ?=(%| -.value) value
86389046 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
86399047 ?: ?=(%unknown -.fit) [%| ["change field constraint is not supported by partial inference" ~]]
86409048 ?: ?=(%bad -.fit)
9049+ =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
9050+ ?^ decimal [%| u.decimal]
86419051 [%| ["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)]]]]
8642− $(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)
86439113::
86449114:: Backtick constructs the canonical prelude unit, after checking its
86459115:: prepared template has the standard null and [~ u=A] cases.
@@ -8743,6 +9213,183 @@
87439213 ?. ?=(%ok -.first) ~
87449214 $(items t.items, actual tal.actual, expected tal.expected, sub sub.first, next next.first)
87459215::
9216+:: +decimal-misfit: a decimal's error where another aura is expected
9217+::
9218+:: A bare decimal is a @ud and fits only @ud, @u, @ and * (S4). After
9219+:: a value fails to fit, refit it with each decimal's variable widened
9220+:: to any aura (+decimal-relax), so that a gate's shared capital learns
9221+:: its aura from the other arguments, then walk the value's syntax
9222+:: beside the type it should fit. The first decimal whose place is an
9223+:: atom of another aura gets the error; otherwise ~, and the caller's
9224+:: own error stands.
9225+::
9226+++ decimal-misfit
9227+ |= [e=expr actual=itype expected=itype sub=isub next=@ud]
9228+ ^- (unit idiag)
9229+ =/ loose=isub (turn sub |=(b=ibinding b(val (decimal-relax val.b))))
9230+ =/ fit=ifit (itype-fit (decimal-relax actual) (decimal-relax expected) loose next)
9231+ (decimal-misfit-at e (decimal-relax expected) ?:(?=(%ok -.fit) sub.fit loose))
9232+::
9233+:: +decimal-relax: a type with each decimal's variable taking any aura
9234+::
9235+++ decimal-relax
9236+ |= t=itype
9237+ ^- itype
9238+ ?+ -.t t
9239+ %nvar [%avar id.t]
9240+ %rnvar [%rvar id.t]
9241+ %collection t(args (turn args.t |=(c=itype (decimal-relax c))))
9242+ %grec t(args (turn args.t |=(c=itype (decimal-relax c))))
9243+ %union t(cases (turn cases.t |=(c=itype (decimal-relax c))), args (turn args.t |=(c=itype (decimal-relax c))))
9244+ %face t(body $(t body.t))
9245+ %fn [%fn $(t sample.t) $(t product.t)]
9246+ %cell [%cell $(t hed.t) $(t tal.t)]
9247+ ==
9248+::
9249+:: +decimal-misfit-at: walk a value beside the type it should fit
9250+::
9251+:: Through groups, faces, tuples and term-headed pairs, the union case
9252+:: a tuple's head tag picks, units and list literals.
9253+::
9254+++ decimal-misfit-at
9255+ |= [e=expr expected=itype sub=isub]
9256+ ^- (unit idiag)
9257+ =. expected (itype-walk expected sub)
9258+ ?: ?=(%face -.expected) $(expected body.expected)
9259+ ?+ -.e ~
9260+ %lit (decimal-lit-misfit at.e lit.e expected |)
9261+ %group $(e inner.e)
9262+ %pair $(e (pair-as-cell e))
9263+ %tuple (decimal-misfit-items items.e expected sub)
9264+ %unit
9265+ ?. ?=(%collection -.expected) ~
9266+ ?. &(=(%unit name.expected) ?=([* ~] args.expected)) ~
9267+ $(e val.e, expected i.args.expected)
9268+ %list
9269+ ?. ?=(%collection -.expected) ~
9270+ ?. &(=(%list name.expected) ?=([* ~] args.expected)) ~
9271+ =/ items=(list expr) items.e
9272+ |-
9273+ ?~ items ~
9274+ =/ found=(unit idiag) ^$(e i.items, expected i.args.expected)
9275+ ?^ found found
9276+ $(items t.items)
9277+ ==
9278+::
9279+:: +decimal-misfit-items: a tuple's items beside a cell, the last its tail
9280+::
9281+++ decimal-misfit-items
9282+ |= [items=(list item) expected=itype sub=isub]
9283+ ^- (unit idiag)
9284+ ?~ items ~
9285+ ?~ t.items (decimal-misfit-at val.i.items expected sub)
9286+ =. expected (itype-walk expected sub)
9287+ ?: ?=(%face -.expected) $(expected body.expected)
9288+ ?: ?=(%union -.expected)
9289+ =/ head=expr val.i.items
9290+ ?. ?=(%lit -.head) ~
9291+ =/ case=(unit itype) (decimal-case val.lit.head cases.expected sub)
9292+ ?~ case ~
9293+ $(expected u.case)
9294+ ?. ?=(%cell -.expected) ~
9295+ =/ found=(unit idiag) (decimal-misfit-at val.i.items hed.expected sub)
9296+ ?^ found found
9297+ $(items t.items, expected tal.expected)
9298+::
9299+:: +decimal-pattern-misfit: a decimal pattern where another aura is matched
9300+::
9301+:: The subject's type is known, so no refit is needed. A cell pattern
9302+:: picks its union case by its head, as a tuple does.
9303+::
9304+++ decimal-pattern-misfit
9305+ |= [p=pattern expected=itype sub=isub]
9306+ ^- (unit idiag)
9307+ =. expected (itype-walk expected sub)
9308+ ?: ?=(%face -.expected) $(expected body.expected)
9309+ ?: ?=(%lit -.p) (decimal-lit-misfit at.p lit.p expected &)
9310+ ?. ?=(%cell -.p) ~
9311+ (decimal-pattern-items items.p expected sub)
9312+::
9313+:: +decimal-pattern-items: a cell pattern's items, as +decimal-misfit-items
9314+::
9315+++ decimal-pattern-items
9316+ |= [items=(list pattern) expected=itype sub=isub]
9317+ ^- (unit idiag)
9318+ ?~ items ~
9319+ ?~ t.items (decimal-pattern-misfit i.items expected sub)
9320+ =. expected (itype-walk expected sub)
9321+ ?: ?=(%face -.expected) $(expected body.expected)
9322+ ?: ?=(%union -.expected)
9323+ ?. ?=(%lit -.i.items) ~
9324+ =/ case=(unit itype) (decimal-case val.lit.i.items cases.expected sub)
9325+ ?~ case ~
9326+ $(expected u.case)
9327+ ?. ?=(%cell -.expected) ~
9328+ =/ found=(unit idiag) (decimal-pattern-misfit i.items hed.expected sub)
9329+ ?^ found found
9330+ $(items t.items, expected tal.expected)
9331+::
9332+:: +decimal-arms-misfit: the first arm whose pattern has a misplaced decimal
9333+::
9334+++ decimal-arms-misfit
9335+ |= [arms=(list arm) subject=itype sub=isub]
9336+ ^- (unit idiag)
9337+ ?~ arms ~
9338+ =/ found=(unit idiag) (decimal-pattern-misfit pat.i.arms subject sub)
9339+ ?^ found found
9340+ $(arms t.arms)
9341+::
9342+:: +decimal-case: the one union case whose head is the constant value
9343+::
9344+++ decimal-case
9345+ |= [value=@ cases=(list itype) sub=isub]
9346+ ^- (unit itype)
9347+ =/ hits=(list itype)
9348+ %+ skim cases
9349+ |= c=itype
9350+ =. c (itype-walk c sub)
9351+ ?. ?=(%cell -.c) |
9352+ =/ head=itype (itype-walk hed.c sub)
9353+ =? head ?=(%face -.head) (itype-walk body.head sub)
9354+ &(?=(%const -.head) =(value val.literal.head))
9355+ ?. ?=([* ~] hits) ~
9356+ `i.hits
9357+::
9358+:: +decimal-lit-misfit: the error for a decimal at a place of known type
9359+::
9360+++ decimal-lit-misfit
9361+ |= [at=span l=lit expected=itype pattern=?]
9362+ ^- (unit idiag)
9363+ ?. &(=(%number form.l) =(%ud aura.l)) ~
9364+ ?. ?=(%atom -.expected) ~
9365+ ?: (decimal-aura aura.expected) ~
9366+ `[(decimal-misfit-msg l aura.expected pattern) ~[[at "decimal"]]]
9367+::
9368+:: +decimal-misfit-msg: "`30` is a @ud, not a @dr; write ~s30"
9369+::
9370+:: The hint writes the value in the expected aura's own literal where
9371+:: that reads naturally: 30 seconds, the text "30", the ship ~syd; a
9372+:: date gets an example. Patterns take no dates, durations or knots,
9373+:: so in a pattern those auras get no hint.
9374+::
9375+++ decimal-misfit-msg
9376+ |= [l=lit aura=@ta pattern=?]
9377+ ^- tape
9378+ =/ what=tape "`{(trip txt.l)}` is a @ud, not a @{(trip aura)}"
9379+ =/ hint=tape
9380+ ?: &(pattern ?=(?(%da %dr %ta) aura)) ""
9381+ ?+ aura ""
9382+ %da "a date, as ~2026.1.1"
9383+ %dr (trip (scot %dr (mul val.l ~s1)))
9384+ %p (trip (scot %p val.l))
9385+ %t (show-quoted txt.l)
9386+ %ta "~.{(trip txt.l)}"
9387+ %ux (trip (scot %ux val.l))
9388+ %uv (trip (scot %uv val.l))
9389+ ==
9390+ ?~ hint what
9391+ "{what}; write {hint}"
9392+::
87469393:: A term-headed pair is the same noun as a two-item cell. Preserve the
87479394:: whole pair span for the synthetic head and the value's own span for
87489395:: the payload; unresolved term constraints follow ordinary cell inference.
@@ -8800,7 +9447,7 @@
88009447 ?. =(u.standard [[%collection %list ~[[%var 0]]] ~[0]])
88019448 [%| ["list literal needs the standard prelude in partial inference" ~]]
88029449 =/ element=itype [%var next.state]
8803− =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e)
9450+ =/ result=iresult (infer-open-list-items items.e element env state(next +(next.state)) at.e ~)
88049451 ?: ?=(%| -.result) result
88059452 [%& [%collection %list ~[element]] state.p.result]
88069453 %str (infer-string-pieces pieces.e env state)
@@ -8832,6 +9479,7 @@
88329479 [%& typ.instance state.instance]
88339480 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
88349481 ?~ scheme
9482+ ?: =(i.names.e %unface) [%| (unface-value at.e)]
88359483 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
88369484 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
88379485 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
@@ -8839,7 +9487,10 @@
88399487 [%& typ.inst state.inst]
88409488 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
88419489 [%& typ.instance state.instance]
8842− %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)
88439494 %change
88449495 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
88459496 =/ target=iresult $(e [%wing at.e target.e])
@@ -8876,6 +9527,8 @@
88769527 ?: ?=(%| -.result) result
88779528 [%& typ.p.result state.p.result(globals globals.state, molds molds.state)]
88789529 %branch
9530+ =/ named=(unit idiag) (branch-tag-name e env state)
9531+ ?^ named [%| u.named]
88799532 ?^ defer.state (dg-boolean-branch e env state)
88809533 ?~ arms.e [%| ["branch is not supported by partial inference" ~]]
88819534 ?~ t.arms.e
@@ -8926,6 +9579,10 @@
89269579 [%| ["record branch matching is not supported by partial inference" ~]]
89279580 ?: |((itype-has-any-atom typ.p.left sub.state.p.right) (itype-has-any-atom typ.p.right sub.state.p.right) (itype-family-related typ.p.left typ.p.right sub.state.p.right))
89289581 [%| ["branch widening is not supported by partial inference" ~]]
9582+ =/ decimal-x=(unit idiag) (decimal-misfit val.x typ.p.left typ.p.right sub.state.p.right next.state.p.right)
9583+ ?^ decimal-x [%| u.decimal-x]
9584+ =/ decimal-y=(unit idiag) (decimal-misfit val.y typ.p.right typ.p.left sub.state.p.right next.state.p.right)
9585+ ?^ decimal-y [%| u.decimal-y]
89299586 [%| ["branch arms have incompatible types" ~[[(span-of val.x) (site-type-note "first arm" typ.p.left sub.state.p.right)] [(span-of val.y) (site-type-note "second arm" typ.p.right sub.state.p.right)]]]]
89309587 [%& typ.u.joined state.p.right(sub sub.u.joined)]
89319588 %cast
@@ -8947,6 +9604,8 @@
89479604 ?^ missing [%| u.missing]
89489605 =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value at.shape.e)
89499606 ?^ nested [%| u.nested]
9607+ =/ decimal=(unit idiag) (decimal-misfit val.e typ.p.value typ.u.target sub.state.p.value next.state.p.value)
9608+ ?^ decimal [%| u.decimal]
89509609 [%| ["cast mold and expression type do not unify" ~[[at.shape.e (site-type-note "cast mold" typ.u.target sub.state.p.value)] [(span-of val.e) (site-type-note "expression" typ.p.value sub.state.p.value)]]]]
89519610 ?: &(?=(^ defer.state.p.value) !(dg-stable-fit typ.p.value typ.u.target sub.fit))
89529611 [%| ["deferred cast fit needs stable inference" ~]]
@@ -8975,6 +9634,7 @@
89759634 ?~ args.e [%| ["call has no argument" ~]]
89769635 ?: (explicit-proj-call e env state)
89779636 [%| ["proj needs an expected record type" ~]]
9637+ ?: (reserved-call %unface e env state) (infer-unface e env state)
89789638 (infer-call-with-head e env state (infer-fragment head.e env state))
89799639 * [%| ["expression is not supported by partial inference" ~]]
89809640 ==
@@ -9270,11 +9930,17 @@
92709930 ?^ missing [%| u.missing]
92719931 =/ nested=(unit idiag) (nested-missing-tag i.args.e typ.p.arg sample.ht sub.st next.st (span-of head.e))
92729932 ?^ nested [%| u.nested]
9933+ =/ decimal=(unit idiag) (decimal-misfit i.args.e typ.p.arg sample.ht sub.st next.st)
9934+ ?^ decimal [%| u.decimal]
92739935 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [(span-of i.args.e) (site-type-note "argument" typ.p.arg sub.st)]]]]
92749936 =/ bad=(unit [at=span typ=itype])
92759937 (call-error-site args.e typ.p.arg sample.ht sub.st next.st)
92769938 =/ whole-args=span
92779939 [beg:(span-of i.args.e) end:(span-of (rear args.e))]
9940+ =/ decimal=(unit idiag)
9941+ =/ items=(list item) (turn args.e |=(a=expr [(span-of a) ~ a]))
9942+ (decimal-misfit [%tuple whole-args items] typ.p.arg sample.ht sub.st next.st)
9943+ ?^ decimal [%| u.decimal]
92789944 =/ arg-at=span ?~(bad whole-args at.u.bad)
92799945 =/ arg-type=itype ?~(bad typ.p.arg typ.u.bad)
92809946 [%| ["call's sample and argument types do not unify" ~[[(span-of head.e) (site-type-note "called gate" ht sub.st)] [arg-at (site-type-note "argument" arg-type sub.st)]]]]
@@ -9345,6 +10011,8 @@
934510011 ?^ missing [%| u.missing]
934610012 =/ nested=(unit idiag) (nested-missing-tag val.e typ.p.value payload sub.state.p.value next.state.p.value context)
934710013 ?^ nested [%| u.nested]
10014+ =/ decimal=(unit idiag) (decimal-misfit val.e typ.p.value payload sub.state.p.value next.state.p.value)
10015+ ?^ decimal [%| u.decimal]
934810016 [%| ["unit payload does not fit its expected type" ~[[context (site-type-note "expected unit payload" payload sub.state.p.value)] [(span-of val.e) (site-type-note "payload" typ.p.value sub.state.p.value)]]]]
934910017 [%& expected state.p.value(sub sub.fit, next next.fit)]
935010018::
@@ -9357,6 +10025,7 @@
935710025 ^- iresult
935810026 ?> ?=(%call -.e)
935910027 ?~ args.e [%| ["call has no argument" ~]]
10028+ ?: (reserved-call %unface e env state) (infer-unface e env state)
936010029 =/ head=iresult (infer-fragment head.e env state)
936110030 ?: ?=(%| -.head) head
936210031 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
@@ -9439,18 +10108,70 @@
943910108 `(infer-simple-items items.e env state)
944010109 `(width-infer-items items.e index.u.target env state context)
944110110::
9442−:: 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)) | &)
944310124++ explicit-proj-call
944410125 |= [e=expr env=ienv state=istate]
944510126 ^- ?
944610127 ?. ?=(%call -.e) |
944710128 ?. ?=([* ~] args.e) |
9448− ?. ?=(%wing -.head.e) |
9449− ?. =(names.head.e ~[%proj]) |
9450− ?: ?=(^ (ienv-lookup %proj env)) |
9451− ?: (lien globals.state |=(n=term =(n %proj))) |
9452− ?~ prelude.state &
9453− ?:(?=(^ (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
945410175++ infer-proj-source
945510176 |= [e=expr expected=itype env=ienv state=istate context=span]
945610177 ^- iresult
@@ -9713,6 +10434,8 @@
971310434 ?: ?=(%bad -.fit) [%| ["recursive mold cell does not fit its source shape" ~]]
971410435 [%& target state.p.value(sub sub.fit, next next.fit)]
971510436 ?: ?=(%call -.e) (infer-contextual-call e target env state)
10437+ =/ named=(unit idiag) (branch-tag-name e env state)
10438+ ?^ named [%| u.named]
971610439 =/ empty-list=(unit iresult) (empty-list-null-branch e env state `[target context])
971710440 ?^ empty-list u.empty-list
971810441 ?: (single-structured-pattern e)
@@ -9855,7 +10578,7 @@
985510578 ?~ pats [%& ~]
985610579 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
985710580 =/ name=term name.i.pats
9858− ?: |(=(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))))
985910582 [%| 'pattern shadows a name']
986010583 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
986110584 ?: ?=(%| -.rest) rest
@@ -9932,24 +10655,12 @@
993210655 ^- tape
993310656 =. t (itype-walk t sub)
993410657 ?- -.t
9935− %var
9936− ?: (lth id.t 26) [(add 65 id.t) ~]
9937− "T{<id.t>}"
9938− %fvar
9939− ?: (lth id.t 26) [(add 65 id.t) ~]
9940− "T{<id.t>}"
9941− %avar
9942− ?: (lth id.t 26) [(add 65 id.t) ~]
9943− "T{<id.t>}"
9944− %rvar
9945− ?: (lth id.t 26) [(add 65 id.t) ~]
9946− "T{<id.t>}"
9947− %nvar
9948− ?: (lth id.t 26) [(add 65 id.t) ~]
9949− "T{<id.t>}"
9950− %rnvar
9951− ?: (lth id.t 26) [(add 65 id.t) ~]
9952− "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)
995310664 %atom "@{(trip aura.t)}"
995410665 %any-atom "@"
995510666 %flag "?"
@@ -9970,6 +10681,17 @@
997010681 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
997110682 ==
997210683::
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+::
997310695++ show-itype-item
997410696 |= [t=itype sub=isub]
997510697 ^- tape
@@ -10028,7 +10750,7 @@
1002810750 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
1002910751 ?: (itype-has-hidden-recursive normalized) label
1003010752 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
10031− =/ printable=itype (canonical-itype normalized vars)
10753+ =/ printable=itype (canonical-itype (cap-names normalized vars ~ sub))
1003210754 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
1003310755::
1003410756:: A capital in a written mold is generalized with its enclosing ++.
@@ -10069,6 +10791,116 @@
1006910791 ?: =(n u.ident) `i.caps
1007010792 $(caps t.caps)
1007110793::
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+::
1007210904++ merged-capitals
1007310905 |= [caps=icaps sub=isub]
1007410906 ^- (unit [first=icap second=icap])
@@ -10288,6 +11120,9 @@
1028811120 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
1028911121 =. gate-defs.state ~
1029011122 ?. ?=(%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
1029111126 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
1029211127 [%| ["recursive definition is not a gate" ~]]
1029311128 =/ result=(unit itype) (recursive-branch-seed d env state)
@@ -10311,6 +11146,7 @@
1031111146 =/ product=itype ?~(result [%var id] u.result)
1031211147 =/ st=istate state.p.sam(next +(id))
1031311148 =/ seed=itype [%fn typ.p.sam product]
11149+ =? seed ?=(^ peeled) (itype-unface seed sub.st)
1031411150 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
1031511151 =/ body=expr
1031611152 ?- -.gate
@@ -10322,7 +11158,9 @@
1032211158 ?: ?=(%| -.out) out
1032311159 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
1032411160 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]
10325− [%& [%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)]
1032611164::
1032711165++ dependency-root
1032811166 |= names=(list term)
@@ -10430,7 +11268,7 @@
1043011268:: Infer a cyclic component with one monomorphic seed per gate. All members
1043111269:: must succeed before any scheme is available; pending constraints and
1043211270:: unresolved branch joins remain partial.
10433−+$ 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=?]
1043411272+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
1043511273++ seed-gate-group
1043611274 |= [ds=(list def) env=ienv state=istate]
@@ -10438,7 +11276,9 @@
1043811276 ?~ ds [%& [~ state]]
1043911277 =/ d=def i.ds
1044011278 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]
10441− =/ 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)
1044211282 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
1044311283 [%| ["recursive group contains a non-gate" ~]]
1044411284 =/ initial=istate (reserve-def-caps gate state)
@@ -10456,7 +11296,8 @@
1045611296 * !!
1045711297 ==
1045811298 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]
10459− =/ 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)]
1046011301 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
1046111302 =/ rest=igate-seeds $(ds t.ds, state after)
1046211303 ?: ?=(%| -.rest) rest
@@ -10496,6 +11337,7 @@
1049611337 ?: (constrained-capitals caps.entry sub.state)
1049711338 [%| ["explicit capital constraints are not supported by partial inference" ~]]
1049811339 =/ typ=itype (itype-normalize typ.entry sub.state)
11340+ =? typ unfaced.entry (itype-unface typ ~)
1049911341 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
1050011342 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
1050111343 [%| ["recursive group needs unsupported inference" ~]]
@@ -10504,7 +11346,7 @@
1050411346 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
1050511347 =/ rest=(each ienv idiag) $(entries t.entries)
1050611348 ?: ?=(%| -.rest) rest
10507− [%& [[name.entry [typ vars]] p.rest]]
11349+ [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]
1050811350::
1050911351++ infer-gate-group
1051011352 |= [ds=(list def) env=ienv state=istate]
@@ -10549,7 +11391,7 @@
1054911391 `[entry u.rest]
1055011392::
1055111393
10552−+$ 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])]
1055311395+$ iadj (map term (list term))
1055411396+$ ivisited (map term ?)
1055511397+$ iwork (list [name=term done=?])
@@ -10645,7 +11487,7 @@
1064511487++ add-groups
1064611488 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
1064711489 ^- iresolved
10648− ?~ components [env grouped artifacts]
11490+ ?~ components [env grouped artifacts ~]
1064911491 =/ component=(list term) i.components
1065011492 ?. (graph-cycle component graph) $(components t.components)
1065111493 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -10686,11 +11528,13 @@
1068611528 =? artifacts ?=(^ u.finalized)
1068711529 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
1068811530 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)
10689− `[[[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]
1069011532++ add-supported-defs-core
1069111533 |= [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)])]
10692− ^- [env=ienv artifacts=(list iwidth-definition)]
10693− ?~ 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)]
1069411538 =/ d=def i.ds
1069511539 ?: ?=(%mold -.d) $(ds t.ds)
1069611540 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -10701,37 +11545,34 @@
1070111545 =. gate-defs.initial checked
1070211546 =. head-evidence.initial heads
1070311547 =. initial (reserve-def-caps val.d initial)
10704− =/ result=iresult (infer-fragment val.d env initial)
11548+ =/ plain=iresult (infer-fragment val.d env initial)
11549+ =/ result=iresult plain
1070511550 =? 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)
1070611558 =/ added=(unit iadded-definition)
1070711559 (add-supported-result d result initial env checked artifacts)
1070811560 ?~ added $(ds t.ds)
1070911561 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
1071011562::
10711−:: Full checking discards unsupported definitions. On that failure path only,
10712−:: retry a bounded number of missing definitions to explain a pending tag
10713−:: from the same ordinary inference state instead of hiding it behind the
10714−:: generic completeness error. No successful definition takes this path.
10715−++ module-pending-tag
10716− |= [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)]
1071711567 ^- (unit [at=span msg=tape])
10718− =/ checked=(map term def) (direct-checked-gates ds env)
10719− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
10720− |-
10721− ?~ ds ~
10722− ?: =(0 fuel) ~
10723− =/ d=def i.ds
10724− ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
10725− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
11568+ ?. ?=(%value -.d) ~
11569+ ?^ (ienv-lookup name.d env) ~
1072611570 =/ initial=istate base(gate-defs checked, head-evidence heads)
1072711571 =. initial (reserve-def-caps val.d initial)
1072811572 =/ result=iresult (infer-fragment val.d env initial)
1072911573 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
10730− ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
10731− =/ pending=(unit [at=span msg=tape])
10732− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
10733− ?^ pending pending
10734− $(ds t.ds, fuel (dec fuel))
11574+ ?: ?=(%| -.result) ~
11575+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
1073511576::
1073611577++ resolve-groups-core
1073711578 |= [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)])]
@@ -10747,12 +11588,12 @@
1074711588 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1074811589 =/ ordered=(list def) (dependency-order ds components)
1074911590 |-
10750− =/ next=[env=ienv artifacts=(list iwidth-definition)]
11591+ =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1075111592 (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)
1075211593 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
1075311594 =. grec-index.initial index
1075411595 =/ out=iresolved (add-groups ds components graph env.next grouped artifacts.next initial)
10755− ?: =(env env.out) out
11596+ ?: =(env env.out) out(failures failures.next)
1075611597 $(env env.out, grouped grouped.out, artifacts artifacts.out)
1075711598::
1075811599:: +dependency-order: the value definitions, dependencies first
@@ -11624,13 +12465,29 @@
1162412465 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
1162512466 ?^ first first
1162612467 $(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.
1162712470++ duplicate-edits
1162812471 |= edits=(list edit)
1162912472 ^- (unit idiag)
12473+ =| seen=(list edit)
12474+ |- ^- (unit idiag)
1163012475 ?~ edits ~
11631− =/ 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)
1163212489 ?^ first first
11633− $(edits t.edits)
12490+ $(edits t.edits, seen [e seen])
1163412491++ duplicate-arms
1163512492 |= arms=(list arm)
1163612493 ^- (unit idiag)
@@ -11703,59 +12560,142 @@
1170312560 ==
1170412561 [n $(imports t.imports)]
1170512562::
11706−++ 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
1170712573 |= sam=sample
1170812574 ^- ?
1170912575 ?- -.sam
11710− %bind =(name.sam %proj)
11711− %face =(name.sam %proj)
11712− %pun =(name.sam %proj)
11713− %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)
1171412580 * |
1171512581 ==
11716−++ reserved-proj-pattern
12582+++ reserved-pattern
1171712583 |= p=pattern
1171812584 ^- ?
1171912585 ?- -.p
11720− %bind =(name.p %proj)
11721− %cell (lien items.p reserved-proj-pattern)
12586+ %bind (reserved-name name.p)
12587+ %cell (lien items.p reserved-pattern)
1172212588 * |
1172312589 ==
11724−++ reserved-proj-def
12590+++ reserved-def
1172512591 |= d=def
1172612592 ^- ?
11727− ?: =(name.d %proj) &
11728− ?: ?=(%value -.d) (reserved-proj-expr val.d)
12593+ ?: (reserved-name name.d) &
12594+ ?: ?=(%value -.d) (reserved-expr val.d)
1172912595 |
11730−++ reserved-proj-expr
12596+++ reserved-expr
1173112597 |= e=expr
1173212598 ^- ?
1173312599 ?- -.e
11734− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
11735− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
11736− %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)))
1173712603 %pair $(e val.e)
1173812604 %unit $(e val.e)
1173912605 %group $(e inner.e)
11740− %list (lien items.e reserved-proj-expr)
11741− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
11742− ?(%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))
1174312609 %cast $(e val.e)
11744− %call |($(e head.e) (lien args.e reserved-proj-expr))
12610+ %call |($(e head.e) (lien args.e reserved-expr))
1174512611 %trace |($(e val.e) $(e then.e))
11746− %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
11747− %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))
1174812614 * |
1174912615 ==
1175012616::
11751−++ module-has-reserved-proj
12617+++ module-has-reserved
1175212618 |= mod=module
1175312619 ^- ?
1175412620 =/ imported=(list term) (import-binding-names imports.mod)
1175512621 =/ vals=(list term) (global-value-names defs.mod)
1175612622 =/ molds=imolds (collect-simple-molds defs.mod)
1175712623 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11758− |((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)])
1175912699::
1176012700++ module-scope-valid
1176112701 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -11764,7 +12704,7 @@
1176412704 =/ vals=(list term) (global-value-names defs.mod)
1176512705 =/ molds=imolds (collect-simple-molds defs.mod)
1176612706 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
11767− ?: (module-has-reserved-proj mod) |
12707+ ?: (module-has-reserved mod) |
1176812708 ?. %+ levy imported
1176912709 |= n=term
1177012710 &((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))))
@@ -12187,6 +13127,31 @@
1218713127 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
1218813128 `[u.name at.s]
1218913129::
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+::
1219013155:: Cache only completed interfaces for this invocation. The source bundle,
1219113156:: imported Hoon types and prelude are fixed for the whole graph. Check the
1219213157:: active path and duplicate sources before consulting it, so a cache hit
@@ -12453,7 +13418,7 @@
1245313418 ^- ?
1245413419 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
1245513420 =/ derived=(list term) (weld path-names poke-names)
12456− ?: (lien derived |=(n=term =(n %proj))) |
13421+ ?: (lien derived reserved-name) |
1245713422 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
1245813423 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
1245913424::
@@ -12485,7 +13450,7 @@
1248513450 =/ clashes=(list term)
1248613451 %+ skip names
1248713452 |= n=term
12488− ?| =(n %proj)
13453+ ?| (reserved-name n)
1248913454 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
1249013455 ==
1249113456 ?~ clashes ~
@@ -13260,7 +14225,7 @@
1326014225 =/ action=term %poke
1326114226 =/ ordinary=(list def) ds
1326214227 =/ derived=(list term) ~[%state action]
13263− ?: (lien derived |=(n=term =(n %proj))) [%| ~]
14228+ ?: (lien derived reserved-name) [%| ~]
1326414229 =/ outer=(list term)
1326514230 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
1326614231 =/ clashes=(list term)
@@ -13447,7 +14412,7 @@
1344714412 ?~ recovered ~
1344814413 ?. ?=(~ vars.u.recovered) ~
1344914414 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13450− `[env.u.added grouped.resolution artifacts.u.added]
14415+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1345114416::
1345214417++ program-inferred-slot
1345314418 |= [typ=itype name=(unit term)]
@@ -13603,7 +14568,7 @@
1360314568 ?~ recovered ~
1360414569 ?. ?=(~ vars.u.recovered) ~
1360514570 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13606− `[env.u.added grouped.resolution artifacts.u.added]
14571+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1360714572::
1360814573+$ iview-site [xs=expr mapper=term]
1360914574++ program-view-site
@@ -13930,7 +14895,7 @@
1393014895 ?~ recovered ~
1393114896 ?. ?=(~ vars.u.recovered) ~
1393214897 ?. ?=(~ (itype-vars typ.u.recovered)) ~
13933− `[env.u.added grouped.resolution artifacts.u.added]
14898+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1393414899::
1393514900:: Recover exactly one direct keyed each/turn row mapper, then its view.
1393614901:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -14152,7 +15117,7 @@
1415215117 ?~ recovered ~
1415315118 ?. ?=(~ vars.u.recovered) ~
1415415119 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14155− `[env.u.added grouped.resolution artifacts.u.added]
15120+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1415615121::
1415715122:: The model a direct program's initializer must produce. Update's written
1415815123:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -14309,7 +15274,7 @@
1430915274 ?~ recovered ~
1431015275 ?. ?=(~ vars.u.recovered) ~
1431115276 ?. ?=(~ (itype-vars typ.u.recovered)) ~
14312− `[env.u.added grouped.resolution artifacts.u.added]
15277+ `[env.u.added grouped.resolution artifacts.u.added failures.resolution]
1431315278::
1431415279++ derived-poke-command-scheme
1431515280 |= [prelude=ifile action=itype]
@@ -14477,9 +15442,9 @@
1447715442 (direct-prelude-evidence ds prelude.initial)
1447815443 ?~ heads resolution
1447915444 =/ checked=(map term def) (direct-checked-gates ds env.resolution)
14480− =/ completed=[env=ienv artifacts=(list iwidth-definition)]
15445+ =/ completed=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
1448115446 (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)
14482− [env.completed grouped.resolution artifacts.completed]
15447+ [env.completed grouped.resolution artifacts.completed failures.resolution]
1448315448::
1448415449:: A static main may retain a generic element message in its ordinary
1448515450:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -14695,6 +15660,9 @@
1469515660 !(lien prelude-molds |=(m=term =(m n)))
1469615661 ==
1469715662 ==
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) ~]]
1469815666 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1469915667 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1470015668 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -14743,6 +15711,9 @@
1474315711 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
1474415712 =/ checking=module mod(defs ds)
1474515713 ?. (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) ~]]
1474615717 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1474715718 =/ vals=(list term) (global-value-names ds)
1474815719 =/ js=jimports-detailed-result (resolve-jibb-imports-detailed imports.mod externals mark-externals modules active prelude-values prelude-molds cache prelude)
@@ -14818,15 +15789,14 @@
1481815789 ?~ store-parts ds
1481915790 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
1482015791 ?. (module-values-complete required env)
14821− =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
14822− ?^ pending
14823− [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
14824− :: 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)
1482515794 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
14826− =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
14827− ?^ shadow
14828− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
14829− [%| [(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 ~]]
1483015800 =/ missing=(unit term) (module-missing-value required env)
1483115801 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
1483215802 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
@@ -15030,8 +16000,8 @@
1503016000 ?: ?=(%| -.parsed) (show-error src p.parsed)
1503116001 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
1503216002 ?^ duplicate (duplicate-fields-report file src u.duplicate)
15033− ?: (module-has-reserved-proj p.parsed)
15034− 'module has reserved proj name'
16003+ ?: (module-has-reserved p.parsed)
16004+ 'module has a reserved proj or unface name'
1503516005 =/ ds=(list def) defs.p.parsed
1503616006 =/ molds=imolds (collect-simple-molds ds)
1503716007 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -15109,7 +16079,7 @@
1510916079 =. head-evidence.initial heads
1511016080 =. initial (reserve-def-caps val.d initial)
1511116081 =/ result=iresult
15112− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
16082+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))
1511316083 (infer-recursive-gate d env initial)
1511416084 (infer-fragment val.d env initial)
1511516085 ?: ?=(%| -.result)
@@ -15141,7 +16111,8 @@
1514116111 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
1514216112 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
1514316113 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])
15144− =/ 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)
1514516116 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
1514616117 $(ds t.ds, lines [line lines])
1514716118:: Experimental module-owned pending-constraint generalization only.
@@ -15238,7 +16209,7 @@
1523816209 =/ normalized=itype (itype-normalize typ sub.state)
1523916210 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
1524016211 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))
15241− `[[normalized quantified]]
16212+ `(cap-names normalized quantified caps.state sub.state)
1524216213::
1524316214+$ dgcommit [env=ienv state=istate]
1524416215:: A branch literal must not acquire a value face through replay.
@@ -15671,20 +16642,21 @@
1567116642 ?~ env `+(top)
1567216643 =/ sc=ischeme scheme.i.env
1567316644 ?: (itype-has-tag typ.sc) ~
15674− $(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))))
1567516646::
15676−:: +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)
1567716649::
1567816650++ itype-max-id
1567916651 |= [t=itype top=@ud]
1568016652 ^- @ud
1568116653 ?- -.t
15682− %var (max top id.t)
15683− %fvar (max top id.t)
15684− %avar (max top id.t)
15685− %rvar (max top id.t)
15686− %nvar (max top id.t)
15687− %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))
1568816660 %tag (max top id.t)
1568916661 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
1569016662 %collection (itype-max-ids args.t top)