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