@@ -206,11 +206,9 @@
206206:: token holds the text after @. An aura starting @s or
207207:: @r is an error at 2nd: "signed and floating-point
208208:: auras are left out of Jibb"
209−:: A-Z type variable [A-Z][a-z0-9]*: a capital, then
210−:: lowercase letters and digits, as M, Msg or T2. Right
211−:: after it, which is emitted first, a capital, _ or -
212−:: is an error there, "a type variable is a capital,
213−:: then lowercase letters and digits"
209+:: A-Z type variable: one capital. A letter or digit right
210+:: after it is an error there, "a type variable is one
211+:: capital letter", after the type variable's token
214212:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names
215213:: joined by dots. Right after the name or wing, which
216214:: is emitted first, a capital or _ is an error there,
@@ -407,7 +405,6 @@
407405:: Why: after the layout pass the grammar is LL(2). Each choice is made by
408406:: the next token, at most with the one after it and whether it is tight:
409407:: name, then = tight a face (items, lines, fields, samples)
410−:: wing, then = tight a change's item or line, wing=value
411408:: name, then + tight a pair
412409:: name or wing, then ( tight a change
413410:: |=, then a term tight a constructor; else, where an
@@ -415,9 +412,6 @@
415412:: ++ or +$ a definition; else a body's final expr
416413:: INDENT a body, an open bracket's lines, arms
417414:: or cases; else the expression goes on
418−:: NEWLINE, after a rune's head the rest of the body, on a body's
419−:: or ?-'s subject final line (The rest of a body);
420−:: else an error
421415:: So the parser never backtracks, its first failure is its furthest, and
422416:: "expected X, found Y" falls out of each arm without tracking failures
423417:: across alternatives. Hoon's combinators read tapes of characters and
@@ -461,9 +455,7 @@
461455:: cases below -> %mold; one case is that mold, several
462456:: are %union. The optional generic wraps either in %generic.
463457:: ++ name expr or body -> %value (a body becomes a %body expr)
464−:: body INDENT rest DEDENT; rest is { definition NEWLINE } last
465−:: -> %body, and last is expr, or the rest of a body that
466−:: a rune on its final line took (The rest of a body)
458+:: body INDENT { definition NEWLINE } expr DEDENT -> %body
467459:: call one operand is that operand; more -> %call head args
468460:: operand literal -> %lit or %str; pathlit -> %path, as a path
469461:: literal is an expression (Decisions); !! -> %crash, as
@@ -480,9 +472,7 @@
480472:: that line, as () is no group. A ( followed by a rune is
481473:: the closed form. Lines of an open group or list take no
482474:: name= (doc question)
483−:: change every item and line has name= or wing=, as open.cart=
484−:: (the EBNF's edit) -> %change of edits, each with its
485−:: names as written; a tuple's item takes no wing=
475+:: change every item and line has name= (the EBNF's "items named")
486476:: rune |= -> %gate; ^- -> %cast; ~& -> %trace; ?- -> %branch.
487477:: !! is an operand, not a rune (Decisions): alone where an
488478:: expression goes it is a call of one operand, and !! a
@@ -563,23 +553,7 @@
563553:: - Local definitions: at the start of any body, a gate's, an arm's,
564554:: a ^-'s, a ~&'s or a ++'s, as the EBNF's body takes them
565555:: (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.
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.
556+:: says.
583557:: - Where errors point: the doc says only "line, column and an
584558:: excerpt"; 2.0 and Errors below say where.
585559::
@@ -630,12 +604,11 @@
630604:: found the end of the line" (+fail-space). No later line can give
631605:: a tight form its next token. A wing and a ( after a space are no
632606:: 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
634−:: no = right after it fails just past it, whatever follows: `m(b c)`
635−:: and `m(a.b 1)` at the space, `m(b)` at the ), `m(a"x)` at the "
636−:: with the layout pass's message after the parser's (+unnamed,
637−:: +moved). `m(a==1)` has its =, and fails at the second, where the
638−:: layout pass does.
607+:: change's item is name=, so a name there with no = right after it
608+:: fails just past the name, whatever follows: `m(b c)` at the
609+:: space, `m(b)` at the ), `m(a"x)` at the " with the layout pass's
610+:: message after the parser's (+unnamed, +moved). `m(a==1)` has its
611+:: =, and fails at the second, where the layout pass does.
639612:: - Where the place needs text on its own line and the line ends,
640613:: whatever line comes next: at the end of that line, just past its
641614:: last token, "found the end of the line" (+fail-line), as no later
@@ -813,9 +786,7 @@
813786:: (value 8:1 init
814787:: (cast 8:9
815788:: (ref 8:12 state)
816−:: (tuple 8:18
817−:: (face 8:19 items (lit 8:25 ~))
818−:: (face 8:27 open (lit 8:32 %.n)))))
789+:: (tuple 8:18 (lit 8:19 ~) (lit 8:21 %.n))))
819790:: (value 9:1 update
820791:: (gate 9:11
821792:: (cell 9:14
@@ -824,17 +795,17 @@
824795:: (body 10:3
825796:: (branch 10:3
826797:: (wing 10:6 a)
827−:: (arm 11:3
828−:: (cell 11:3 (lit 11:4 %add) (bind 11:9 item))
829−:: (change 11:16 s
830−:: (edit 11:18 items
831−:: (tuple 11:24 (wing 11:25 item) (wing 11:30 items.s)))))
832−:: (arm 12:3
833−:: (lit 12:3 %toggle)
834−:: (change 12:16 s
835−:: (edit 12:18 open
836−:: (group 12:23
837−:: (call 12:24 (wing 12:24 not) (wing 12:28 open.s)))))))))))
798+:: (arm 11:5
799+:: (cell 11:5 (lit 11:6 %add) (bind 11:11 item))
800+:: (change 11:18 s
801+:: (edit 11:20 items
802+:: (tuple 11:26 (wing 11:27 item) (wing 11:32 items.s)))))
803+:: (arm 12:5
804+:: (lit 12:5 %toggle)
805+:: (change 12:18 s
806+:: (edit 12:20 open
807+:: (group 12:25
808+:: (call 12:26 (wing 12:26 not) (wing 12:30 open.s)))))))))))
838809::
839810:: 4.3 Errors (+show-error): "<file>:<line>:<col>: <message>", then the
840811:: source line, then a caret under the column (col - 1 spaces, then ^).
@@ -845,93 +816,9 @@
845816:: prints as a space, so the caret stays under its column and golden
846817:: files hold no raw control bytes.
847818::
848−:: /ui/basket.jibb:22:3: msg has no case %submitt
849−:: %submitt [m(note="") ~]
850−:: ^
851−::
852−:: ===================================================================
853−:: 5. General checker core (design; not implemented yet)
854−:: ===================================================================
855−::
856−:: The existing inference and recovery paths are described in
857−:: docs/compiler.md. This section is a plan for replacing them, not a
858−:: claim that the current checker implements these rules. The Grammar and
859−:: Decisions are authoritative if this design needs adjustment.
860−::
861−:: 5.1 State and unification. Give each inference variable an identity and
862−:: a union-find entry: parent or binding, rank, level, source, rigidity,
863−:: and the atom, arithmetic-atom and gate-free obligations it carries.
864−:: Hoon's immutable maps hold the entries; operations return the updated
865−:: state. Find compresses paths in that returned state. Bind only after an
866−:: occurs check, merge obligations at roots, and lower levels throughout
867−:: the bound type to the root's level. A rigid written capital may acquire
868−:: allowed constraints but cannot be forced to a concrete type or a
869−:: different written capital. Keep origins for both sides of each fit so
870−:: a failure can show both excerpts. Recursive named molds retain their
871−:: identity; the occurs check is for inference variables, not a ban on
872−:: declared recursion.
873−::
874−:: A scheme quantifies eligible variables above the enclosing level;
875−:: instantiate with fresh variables and copy their obligations. Written
876−:: capitals respect their lexical scope, including sharing with a local
877−:: definition when the enclosing definition uses the same name. Retain
878−:: aura variables and directional aura fits, rather than turning every
879−:: fit into symmetric equality. At a faced position a capital binds the
880−:: type under the face; joining an unnamed position with a faced one keeps
881−:: the face, independently of the order of the inputs. Different explicit
882−:: faces conflict. No gate may hide inside a gate-free type, including in
883−:: a container; propagate the obligation through its arguments.
884−::
885−:: 5.2 Work queue. A constraint owns its source span, the types and
886−:: expression shape it depends on, and the information needed to report
887−:: failure. Tags and constructors, null, decimal and cell literals,
888−:: wings, changes, unface and unknown match subjects enter the same queue.
889−:: Index waiting constraints by the roots they read. Binding or merging a
890−:: root wakes its dependants; a retry either solves, fails with its sites,
891−:: or registers the roots still needed. Run to a fixed point, without
892−:: losing constraints when a root is redirected. Check patterns once the
893−:: subject is known. Contextual tags inspect case shapes and noun-equal
894−:: heads, retaining the named union and its site in diagnostics.
895−::
896−:: Variables reachable from an open tag constraint remain monomorphic
897−:: across definitions, so a later use, including main, can fix them.
898−:: Other eligible variables can generalize, with their atom and gate-free
899−:: obligations intact. At each definition boundary resolve its holes and
900−:: apply the specified decimal and cell defaults, without defaulting a
901−:: decimal whose definition is generic over its aura. A decimal fits @ud,
902−:: @u, @ and *; other concrete auras need their own literal. At module
903−:: completion retry the queue and report each still-open constraint at its
904−:: source; an unresolved tag asks for a ^-, never a guessed union.
905−::
906−:: 5.3 Definition order and kinds. Use the existing dependency graph's
907−:: strongly connected components in dependency order. Give a recursive
908−:: group of gates monomorphic placeholders, infer all members in one state,
909−:: solve what can be solved, then generalize together. Reject a cycle
910−:: involving a non-gate value, including one through a gate, and show the
911−:: cycle. Check a named definition's holes before later uses can fix them.
912−:: Infer main as an ordinary expression against ordinary prelude schemes;
913−:: only its resulting type determines library, page, island or store.
914−:: Afterwards check kind-specific invariants: recursively find the field
915−:: containing a gate in island data or a model, and inspect subscriptions
916−:: for watchability only at %watch. A page load may be any gate to ask,
917−:: including pure and typed paths. Preserve request provenance needed for
918−:: a watchability proof through ordinary calls and aliases.
919−::
920−:: 5.4 Matches and migration. A reusable usefulness matrix over noun
921−:: constructors, constants, cells and wildcards checks nested patterns;
922−:: loobeans, lists and units expand to their cases. Test an arm against
923−:: previous rows for usefulness, then test a wildcard for exhaustiveness;
924−:: keep a witness for a missing case and the covering arm's site for a
925−:: dead one. Recursive types require memoized specialization and a
926−:: terminating treatment of recursive states. The same matrix can later
927−:: drive lowering. The bare-name/tag spelling rule is checked against the
928−:: subject and the cases the rest of the pattern can match.
929−::
930−:: Migrate in small stages with eval and ship goldens for every change.
931−:: Keep diagnostics and source sites in the single full result; types.txt
932−:: is a rendering of that result. As general inference covers an existing
933−:: recovery or source-proven slice, remove that slice and retain its tests.
934−:: An unsupported construct fails closed at its own site until then.
819+:: /ui/basket.jibb:22:5: msg has no case %submitt
820+:: %submitt [m(note="") ~]
821+:: ^
935822::
936823|%
937824+| %positions
@@ -1077,10 +964,9 @@
1077964::
1078965+$ item $~([*span ~ *expr] [at=span face=(unit term) val=expr])
1079966::
1080−:: +edit: a change's item or line, name=value or wing=value; names
1081−:: as written, as a %wing's: open.cart is ~[%open %cart]
967+:: +edit: a change's item or line, name=value
1082968::
1083−+$ edit $~([*span ~ *expr] [at=span names=(list term) val=expr])
969++$ edit $~([*span %$ *expr] [at=span name=term val=expr])
1084970::
1085971:: +arm: a ?- arm, a pattern and an expression or body
1086972::
@@ -1469,10 +1355,10 @@
14691355 =? n &(?=(^ rest) (is-upper i.rest)) +(n)
14701356 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])
14711357 ?: (is-upper a)
1472− =/ n=@ud (run-len t.cs tvar-mask)
1473− => (emit +(n) [%tvar (crip [a (scag n t.cs)])])
1474− ?. &(?=(^ cs) |((is-upper i.cs) =('_' i.cs) =('-' i.cs))) cor
1475− (err col "a type variable is a capital, then lowercase letters and digits")
1358+ => (emit 1 [%tvar a])
1359+ ?. &(?=(^ cs) |((is-lower i.cs) (is-upper i.cs) (is-digit i.cs)))
1360+ cor
1361+ (err col "a type variable is one capital letter")
14761362 ?: =(':' a)
14771363 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")
14781364 ?: =(':' b) comment
@@ -1776,7 +1662,6 @@
17761662++ digit-mask 0x3ff.0000.0000.0000 :: 0-9
17771663++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f
17781664++ 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
17801665++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _
17811666++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .
17821667++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2
@@ -2395,7 +2280,7 @@
23952280++ sexp-edit
23962281 |= e=edit
23972282 ^- sexp
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)])
23992284::
24002285++ sexp-arm
24012286 |= a=arm
@@ -2804,32 +2689,24 @@
28042689 ?~ t.els i.els
28052690 [%call [beg:(span-of i.els) end:(span-of (rear t.els))] i.els t.els]
28062691::
2807−:: +slot: a bracket's item or line as read, before +bracket-node
2808−:: makes it an item or an edit: its name=, or a change's wing=, else ~
2809−::
2810−+$ slot [at=span face=(list term) val=expr]
2811−::
28122692:: +bracket-node: a tuple, list or change from its items, ending at fin
28132693::
28142694++ bracket-node
28152695 |= $: kind=?(%tuple %list %change)
28162696 op=token
28172697 target=(unit [t=token names=(list term)])
2818− its=(list slot)
2698+ its=(list item)
28192699 fin=loc
28202700 ==
28212701 ^- expr
28222702 ?- kind
2823− %tuple
2824− :+ %tuple [beg.at.op fin]
2825− (turn its |=(i=slot ^-(item [at.i ?~(face.i ~ `i.face.i) val.i])))
2826− ::
2827− %list [%list [beg.at.op fin] (turn its |=(i=slot val.i))]
2703+ %tuple [%tuple [beg.at.op fin] its]
2704+ %list [%list [beg.at.op fin] (turn its |=(i=item val.i))]
28282705 ::
28292706 %change
28302707 =/ beg=loc ?~(target beg.at.op beg.at.t.u.target)
28312708 :^ %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])))
28332710 ==
28342711::
28352712+| %parser
@@ -3050,22 +2927,23 @@
30502927 ::
30512928 :: +unnamed: a change's item or line without its name=
30522929 ::
3053− :: A name or a wing could still begin one, so the error is just
3054− :: past it, as a tight form's is (+fail-space): `m(b c)` and
3055− :: `m(a.b 1)` at the space, `m(b)` at the ). So is an error token's
3056− :: text there, unless it begins with the =: `m(a"x)` at the ", with
3057− :: the layout pass's message after the parser's (+moved), but
3058− :: `m(a==1)` at the lexer's error, the second =. At an error token
3059− :: whose text can't begin a name, at that text, as `m( @sd` at the
3060− :: @ (+fail-in).
2930+ :: A name could still begin one, so the error is just past it, as
2931+ :: a tight form's is (+fail-space): `m(b c)` at the space, `m(b)`
2932+ :: at the ). So is an error token's text there, unless it begins
2933+ :: with the =: `m(a"x)` at the ", with the layout pass's message
2934+ :: after the parser's (+moved), but `m(a==1)` at the lexer's error,
2935+ :: the second =. So is a wing's first name: `m(a.b=1)` fails at the
2936+ :: dot (+fail-in). At an error token whose text can't begin a name,
2937+ :: at that text, as `m( @sd` at the @ (+fail-in).
30612938 ::
30622939 ++ unnamed
30632940 |= ts=(list token)
30642941 ^- [%| p=error]
30652942 =/ why=tape "a change's items are named, as in m(done=%.y)"
30662943 ?: ?=([[* * [%error *]] *] ts) (bad-in ts "a named item" lower-mask)
3067− ?. ?=([[* * ?([%name *] [%wing *])] *] ts)
3068− (bad-why ts "a named item" why)
2944+ ?: ?=([[* * [%wing *]] *] ts)
2945+ (bad-in-why ts "a named item" lower-mask why)
2946+ ?. ?=([[* * [%name *]] *] ts) (bad-why ts "a named item" why)
30692947 =/ want=tape "`=` right after {(show-found i.ts)}"
30702948 ?: ?& ?=([* [* * [%error *]] *] ts)
30712949 =(end.at.i.ts from.lex.i.t.ts)
@@ -3083,10 +2961,9 @@
30832961 :: closes on its line (2.9). A bracket that needs none of these
30842962 :: closes with the deeper lines instead (+shut). No later line can
30852963 :: 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
3087− :: after begins with NEWLINE or DEDENT, so it costs nothing on the way
3088− :: to a tree, except where a rune takes the rest of a body (+read-last):
3089− :: a look at that rune's line.
2964+ :: them (section 3, Errors). want is what it needs. Only an error path
2965+ :: calls this, and it looks only when after begins with NEWLINE or
2966+ :: DEDENT, so it costs nothing on the way to a tree.
30902967 ::
30912968 ++ doomed
30922969 |= [ts=(list token) after=(list token) want=tape]
@@ -3243,7 +3120,7 @@
32433120 ?: =(%'++' lex.rune)
32443121 ;< [nam=term after=(list token)] then (read-def-name rune t.ts)
32453122 ;< [e=expr more=(list token)] then
3246− (read-expr-or-body | "the name" after)
3123+ (read-expr-or-body "the name" after)
32473124 [%& [%value [beg.at.rune end:(span-of e)] nam e] more]
32483125 ?: (is-closer rune)
32493126 %^ bad-why ts "a definition"
@@ -3323,36 +3200,20 @@
33233200 [%& p.lex.i.ts t.ts]
33243201 ::
33253202 :: +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.
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
3203+ :: body on deeper lines; what names what comes before, for errors
33303204 ::
33313205 ++ read-expr-or-body
3332− |= [fin=? what=tape ts=(list token)]
3206+ |= [what=tape ts=(list token)]
33333207 ^- (pare expr)
33343208 ?: ?=([[* * %indent] *] ts) (read-body t.ts)
3335− ?: &(fin ?=([[* * %newline] *] ts)) (read-rest t.ts)
33363209 ?: ?=([[* * ?(%newline %dedent)] *] ts)
33373210 (bad ts "an expression, or a body on deeper lines")
33383211 ?: &(?=(^ ts) tight.i.ts) (no-gap ts "a space after {what}")
3339− (read-last &(fin !?=([[* * %'?-'] *] ts)) ts)
3212+ (read-expr ts)
33403213 ::
3341− :: +read-body: after its INDENT, the rest of a body, then its DEDENT
3214+ :: +read-body: after its INDENT, { definition NEWLINE } expr DEDENT
33423215 ::
33433216 ++ read-body
3344− |= ts=(list token)
3345− ^- (pare expr)
3346− ;< [e=expr after=(list token)] then (read-rest ts)
3347− ?> ?=([[* * %dedent] *] after)
3348− [%& e t.after]
3349− ::
3350− :: +read-rest: { definition NEWLINE } last, up to the DEDENT that ends
3351− :: a body, which it leaves for whatever opened the body: its INDENT's
3352− :: reader, or the rune on the final line that took the rest of it
3353− :: (+read-last)
3354− ::
3355− ++ read-rest
33563217 |= ts=(list token)
33573218 ^- (pare expr)
33583219 =| defs=(list def)
@@ -3366,15 +3227,12 @@
33663227 %: bad-in-why ts "a definition or an expression" plus-mask
33673228 "`+` begins `++` or `+$`"
33683229 ==
3369− ;< [e=expr after=(list token)] then (read-last & ts)
3230+ ;< [e=expr after=(list token)] then (read-expr ts)
33703231 ?: ?=([[* * %dedent] *] after)
33713232 =/ ds=(list def) (flop defs)
33723233 =/ 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]
33743235 ?. ?=([[* * %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"
33783236 %^ bad-why after "the end of the body"
33793237 "a body's final expression is its last line"
33803238 ::
@@ -3383,24 +3241,13 @@
33833241 ++ read-expr
33843242 |= ts=(list token)
33853243 ^- (pare expr)
3386− (read-last | ts)
3387− ::
3388− :: +read-last: +read-expr, where fin says the expression is a body's
3389− :: final line or goes on one, with no bracket open before it: then
3390− :: the rune that ends the line may take the rest of the body at the
3391− :: same depth as its last child, and a ?- that begins the line its
3392− :: arms (section 3, The rest of a body)
3393− ::
3394− ++ read-last
3395− |= [fin=? ts=(list token)]
3396− ^- (pare expr)
33973244 ?~ ts (bad ts "an expression")
33983245 =* t i.ts
33993246 ?+ lex.t (read-call ts)
3400− %'|=' ?:((is-ctor ts) (read-call ts) (read-gate fin t t.ts))
3401− %'^-' (read-cast fin t t.ts)
3402− %'~&' (read-trace fin t t.ts)
3403− %'?-' (read-branch fin t t.ts)
3247+ %'|=' ?:((is-ctor ts) (read-call ts) (read-gate t t.ts))
3248+ %'^-' (read-cast t t.ts)
3249+ %'~&' (read-trace t t.ts)
3250+ %'?-' (read-branch t t.ts)
34043251 ==
34053252 ::
34063253 :: +read-call: operand { operand }; one operand alone is itself
@@ -3615,9 +3462,9 @@
36153462 (unclosed par ")" after)
36163463 ;< [els=(list expr) after=(list token)] then (read-operands ts)
36173464 ?: ?=([[* * %indent] *] after)
3618− ;< [ls=(list slot) more=(list token)] then
3465+ ;< [ls=(list item) more=(list token)] then
36193466 (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))))
36213468 [%& [%group [beg.at.par end:(span-of inner)] inner] more]
36223469 ?~ els
36233470 ?: ?=([[* * ?(%newline %dedent)] *] after)
@@ -3642,7 +3489,7 @@
36423489 ==
36433490 ^- (pare expr)
36443491 =/ close=?(%')' %']') ?:(?=(%change kind) %')' %']')
3645− =| its=(list slot)
3492+ =| its=(list item)
36463493 |- ^- (pare expr)
36473494 ?~ ts (bad ts "an item")
36483495 =* t i.ts
@@ -3650,8 +3497,8 @@
36503497 [%& (bracket-node kind op target (flop its) end.at.t) t.ts]
36513498 ?: (is-closer t) (unclosed op (trip close) ts)
36523499 ?: ?=(%indent lex.t)
3653− ;< [ls=(list slot) more=(list token)] then (read-lines kind t.ts)
3654− =/ every=(list slot) (weld (flop its) ls)
3500+ ;< [ls=(list item) more=(list token)] then (read-lines kind t.ts)
3501+ =/ every=(list item) (weld (flop its) ls)
36553502 =/ fin=loc ?~(every end.at.op end.at:(rear every))
36563503 [%& (bracket-node kind op target every fin) more]
36573504 ?: &(?=(^ its) (shut op `at.i.its ts))
@@ -3659,21 +3506,21 @@
36593506 ?: ?=(?(%newline %dedent) lex.t)
36603507 (unclosed-open op (trip close) "an item" ts)
36613508 ?: &(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)
36633510 $(its [i its], ts more)
36643511 ::
36653512 :: +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
36673514 ::
36683515 ++ read-item
36693516 |= [kind=?(%tuple %list %change) ts=(list token)]
3670− ^- (pare slot)
3671− ?: &(?=([* * *] ts) (named-item kind ts))
3517+ ^- (pare item)
3518+ ?: &(!?=(%list kind) ?=([[* * [%name *]] [* %& %'='] *] ts))
36723519 =* nam i.ts
36733520 =/ rest=(list token) t.t.ts
36743521 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
36753522 ;< [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]
36773524 ?: ?=(%change kind) (unnamed ts)
36783525 ?: &(?=(^ ts) (is-rune i.ts))
36793526 %: bad-in-why ts "an expression" operand-mask
@@ -3682,25 +3529,15 @@
36823529 ;< [v=expr after=(list token)] then (read-operand ts)
36833530 [%& [(span-of v) ~ v] after]
36843531 ::
3685− :: +named-item: whether ts begins an item's or a line's name=: a
3686− :: tuple's or a change's name, or a change's wing, then = tight
3687− ::
3688− ++ named-item
3689− |= [kind=?(%tuple %list %change %group) ts=(list token)]
3690− ^- ?
3691− ?. ?=([* [* %& %'='] *] ts) |
3692− ?: ?=([[* * [%name *]] *] ts) ?=(?(%tuple %change) kind)
3693− &(?=(%change kind) ?=([[* * [%wing *]] *] ts))
3694− ::
36953532 :: +read-lines: after an open bracket's INDENT, its lines, an item
36963533 :: each, to its DEDENT
36973534 ::
36983535 ++ read-lines
36993536 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3700− ^- (pare (list slot))
3701− =| ls=(list slot)
3702− |- ^- (pare (list slot))
3703− ;< [l=slot after=(list token)] then (read-line kind ts)
3537+ ^- (pare (list item))
3538+ =| ls=(list item)
3539+ |- ^- (pare (list item))
3540+ ;< [l=item after=(list token)] then (read-line kind ts)
37043541 ?: ?=([[* * %newline] *] after) $(ls [l ls], ts t.after)
37053542 ?: ?=([[* * %dedent] *] after) [%& (flop [l ls]) t.after]
37063543 ?. ?=([[* * ?(%')' %']')] *] after) (bad-end-in after (tail-can val.l))
@@ -3727,20 +3564,22 @@
37273564 "its items end at the first line that isn't deeper"
37283565 ::
37293566 :: +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
3731− :: group's are not (doc question)
3567+ :: be named, a change's must be, a list's and a group's are not
3568+ :: (doc question)
37323569 ::
37333570 ++ read-line
37343571 |= [kind=?(%tuple %list %change %group) ts=(list token)]
3735− ^- (pare slot)
3572+ ^- (pare item)
37363573 =/ cf (closer-first ts "an item")
37373574 ?^ cf u.cf
3738− ?: &(?=([* * *] ts) (named-item kind ts))
3575+ ?: ?& ?=(?(%tuple %change) kind)
3576+ ?=([[* * [%name *]] [* %& %'='] *] ts)
3577+ ==
37393578 =* nam i.ts
37403579 =/ rest=(list token) t.t.ts
37413580 ?: |(?=(~ rest) !tight.i.rest) (bad-space i.t.ts rest "a value")
37423581 ;< [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]
37443583 ?: ?=(%change kind) (unnamed ts)
37453584 ;< [v=expr after=(list token)] then (read-expr ts)
37463585 [%& [(span-of v) ~ v] after]
@@ -3777,11 +3616,10 @@
37773616 %^ bad-why more (closing op ")")
37783617 "the wide gate's body is one operand, so a call goes in parentheses"
37793618 ::
3780− :: +read-gate: |= sample, then an expression or a body; fin as for
3781− :: +read-last
3619+ :: +read-gate: |= sample, then an expression or a body
37823620 ::
37833621 ++ read-gate
3784− |= [fin=? bar=token ts=(list token)]
3622+ |= [bar=token ts=(list token)]
37853623 ^- (pare expr)
37863624 ?: &(?=(^ ts) tight.i.ts)
37873625 :: a % could begin a constructor's term, as |=%got
@@ -3793,14 +3631,13 @@
37933631 =/ dm (doomed ts after "an expression, or a body on deeper lines")
37943632 ?^ dm u.dm
37953633 ;< [e=expr more=(list token)] then
3796− (read-expr-or-body fin "the sample" after)
3634+ (read-expr-or-body "the sample" after)
37973635 [%& [%gate [beg.at.bar end:(span-of e)] s e] more]
37983636 ::
3799− :: +read-cast: ^- mold, then an expression or a body; fin as for
3800− :: +read-last
3637+ :: +read-cast: ^- mold, then an expression or a body
38013638 ::
38023639 ++ read-cast
3803− |= [fin=? ket=token ts=(list token)]
3640+ |= [ket=token ts=(list token)]
38043641 ^- (pare expr)
38053642 ?: &(?=(^ ts) tight.i.ts) (wide-rune "^-" ts)
38063643 ;< [s=shape after=(list token)] then (read-mold ts)
@@ -3809,65 +3646,41 @@
38093646 =/ dm (doomed ts after "an expression, or a body on deeper lines")
38103647 ?^ dm u.dm
38113648 ;< [e=expr more=(list token)] then
3812− (read-expr-or-body fin "the mold" after)
3649+ (read-expr-or-body "the mold" after)
38133650 [%& [%cast [beg.at.ket end:(span-of e)] s e] more]
38143651 ::
3815− :: +read-trace: ~& expr, then its body below, or, on a body's final
3816− :: line (fin, +read-last), the rest of the body
3652+ :: +read-trace: ~& expr, then its body below
38173653 ::
38183654 ++ read-trace
3819− |= [fin=? sig=token ts=(list token)]
3655+ |= [sig=token ts=(list token)]
38203656 ^- (pare expr)
38213657 ?: &(?=(^ ts) tight.i.ts) (wide-rune "~&" ts)
38223658 ;< [v=expr after=(list token)] then (read-expr ts)
3823− =/ dm (doomed ts after "`~&`'s body on deeper lines")
3824− ?^ dm u.dm
3825− ;< [b=expr more=(list token)] then
3826− ?: ?=([[* * %indent] *] after) (read-body t.after)
3827− ?: &(fin ?=([[* * %newline] *] after)) (read-rest t.after)
3659+ ?. ?=([[* * %indent] *] after)
3660+ =/ dm (doomed ts after "`~&`'s body on deeper lines")
3661+ ?^ dm u.dm
38283662 (bad after "`~&`'s body on deeper lines")
3663+ ;< [b=expr more=(list token)] then (read-body t.after)
38293664 [%& [%trace [beg.at.sig end:(span-of b)] v b] more]
38303665 ::
3831− :: +read-branch: ?- expr, then its arms below, one per line; or, when
3832− :: it begins a body's final line (fin, +read-last), at its own depth
3833− :: to the end of the body, whose DEDENT it leaves (+read-rest)
3666+ :: +read-branch: ?- expr, then its arms below, one per line
38343667 ::
38353668 ++ read-branch
3836− |= [fin=? wut=token ts=(list token)]
3669+ |= [wut=token ts=(list token)]
38373670 ^- (pare expr)
38383671 ?: &(?=(^ ts) tight.i.ts) (wide-rune "?-" ts)
38393672 ;< [s=expr after=(list token)] then (read-expr ts)
3840− =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3841− ?^ dm u.dm
3842− ?. ?=([[* * ?(%indent %newline)] *] after)
3673+ ?. ?=([[* * %indent] *] after)
3674+ =/ dm (doomed ts after "`?-`'s arms on deeper lines")
3675+ ?^ dm u.dm
38433676 (bad after "`?-`'s arms on deeper lines")
3844− =/ flat=? ?=(%newline lex.i.after)
3845− ?: &(flat !fin) (bad after "`?-`'s arms on deeper lines")
38463677 =| arms=(list arm)
38473678 =/ rest=(list token) t.after
38483679 |- ^- (pare expr)
3849− ;< [a=arm more=(list token)] then
3850− ?:(flat (read-flat-arm rest) (read-arm rest))
3680+ ;< [a=arm more=(list token)] then (read-arm rest)
38513681 ?: ?=([[* * %newline] *] more) $(arms [a arms], rest t.more)
38523682 ?. ?=([[* * %dedent] *] more) (bad-end-in more (tail-can val.a))
3853− =/ at=span [beg.at.wut end.at.a]
3854− [%& [%branch at s (flop [a arms])] ?:(flat more t.more)]
3855− ::
3856− :: +read-flat-arm: +read-arm at its ?-'s depth, where a line that
3857− :: could begin the body's other lines gets a hint
3858− ::
3859− ++ read-flat-arm
3860− |= ts=(list token)
3861− ^- (pare arm)
3862− ?: ?=([[* * ?(%'++' %'+$')] *] ts)
3863− %: bad-in-why ts "a pattern" pattern-mask
3864− "a body's local definitions come before its final expression"
3865− ==
3866− ?: ?=([[* * ?(%'~&' %'^-')] *] ts)
3867− %: bad-in-why ts "a pattern" pattern-mask
3868− "a trace or cast goes in the arm's body"
3869− ==
3870− (read-arm ts)
3683+ [%& [%branch [beg.at.wut end.at.a] s (flop [a arms])] t.more]
38713684 ::
38723685 :: +read-arm: a pattern, then an expression or a body
38733686 ::
@@ -3882,7 +3695,7 @@
38823695 %^ bad-why after "a space after the pattern"
38833696 "patterns take no `name=`: a bare name binds, as [a b]"
38843697 ;< [e=expr more=(list token)] then
3885− (read-expr-or-body | "the pattern" after)
3698+ (read-expr-or-body "the pattern" after)
38863699 [%& [[beg:(span-of p) end:(span-of e)] p e] more]
38873700 ::
38883701 :: +read-pattern: a term, number, string, ship, loobean, ~, * or name,
@@ -4624,7 +4437,7 @@
46244437++ outline-edit
46254438 |= e=edit
46264439 ^- outline
4627− [%edit at.e ~[%name %wing] %kid ~[(outline-expr val.e)]]
4440+ [%edit at.e ~[%name] %kid ~[(outline-expr val.e)]]
46284441::
46294442++ outline-arm
46304443 |= a=arm
@@ -4824,14 +4637,6 @@
48244637:: proofs to fewer than 1,024 cells; the projection planner has a separate
48254638:: 4,096-step bound. These are inference limits, not language limits.
48264639::
4827−:: `unface` is reserved with proj (+reserved-name) and is also handled by
4828−:: type: (unface e) has e's type with every face removed, through cells,
4829−:: gates and collection arguments, keeping unions and recursive molds
4830−:: whole (+itype-unface). It is not a value, it takes one argument, and
4831−:: a bare type variable is unsupported, as field access on one is. A ++
4832−:: whose body is (unface |= …) is a gate for recursion (+unfaced-gate).
4833−:: It lowers to its argument; no lowering is implemented yet.
4834−::
48354640:: Supported API imports derive request-gate types atomically for multiple
48364641:: paths, including one typed segment or one diff fold per case. Their checked
48374642:: ordinary definitions, mark molds and supported poke constructor are also
@@ -5139,35 +4944,6 @@
51394944 $(a tal.a, b tal.b, sub u.first)
51404945 ~
51414946::
5142−:: +itype-unface: t with every face removed, for (unface e)
5143−::
5144−:: It strips through cells, through a gate's sample and product and
5145−:: through a built-in collection's arguments, the prelude's unit
5146−:: included, walking bound variables. Other unions and recursive
5147−:: molds are compared by name or by their exact cases, so stripping
5148−:: inside them would stop them from fitting their own name: they are
5149−:: kept whole. An unbound variable stays, so faces it is bound to
5150−:: later are kept. The unit keeps its own u=, as a list keeps i= and
5151−:: t= in its mold.
5152−::
5153−++ itype-unface
5154− |= [t=itype sub=isub]
5155− ^- itype
5156− =. t (itype-walk t sub)
5157− ?+ -.t t
5158− %face $(t body.t)
5159− %cell [%cell $(t hed.t) $(t tal.t)]
5160− %fn [%fn $(t sample.t) $(t product.t)]
5161− %collection [%collection name.t (turn args.t |=(a=itype ^$(t a)))]
5162− %union
5163− ?. =(origin.t `[/lib/jibb/prelude/jibb %unit]) t
5164− ?. ?=([* ~] args.t) t
5165− =/ nil=itype [%const [%null %n 0 '~']]
5166− ?. =(cases.t ~[nil [%cell nil [%face %u i.args.t]]]) t
5167− =/ arg=itype $(t i.args.t)
5168− t(cases ~[nil [%cell nil [%face %u arg]]], args ~[arg])
5169− ==
5170−::
51714947+$ igf-form [typ=itype sub=isub left=@ud]
51724948+$ igf-forms [types=(list itype) sub=isub left=@ud]
51734949++ itype-gate-free-forms
@@ -6599,67 +6375,15 @@
65996375 ^- ?
66006376 (itype-var-is-gate-free-fuel n t 256)
66016377::
6602−:: +named-var: the ID of the nth type variable, written as name
6603−::
6604−:: An ID counts in its low 64 bits. The name a variable was written
6605−:: with, as Msg, sits above them, or 0 for none, so the name travels
6606−:: with the variable through substitution, generalization and
6607−:: instantiation, and the printer can show it (+show-var). No two
6608−:: IDs share a count, so a name never makes two variables one.
6609−::
6610−++ named-var
6611− |= [name=@t n=@ud]
6612− ^- @ud
6613− (add (lsh 6 name) (end 6 n))
6614−::
6615−:: +var-name: the name in a type variable's ID, or 0 for none
6616−::
6617−++ var-name
6618− |= id=@ud
6619− ^- @t
6620− (rsh 6 id)
6621−::
6622−:: +var-count: a type variable's ID without its name
6623−::
6624−++ var-count
6625− |= id=@ud
6626− ^- @ud
6627− (end 6 id)
6628−::
6629−:: +canonical-itype: t with the variables in vars renumbered to print
6630−::
6631−:: A variable keeps its name unless one before it in vars has the same
6632−:: name. The others take numbers from 0, skipping any whose letter
6633−:: (+show-var) is a name in vars, so a printed type never shows one
6634−:: name for two variables.
6635−::
66366378++ canonical-itype
66376379 |= [t=itype vars=(list @ud)]
66386380 ^- itype
6639− =/ names=(list @t) (turn vars var-name)
6640− =/ used=(list @t) ~
66416381 =/ ren=isub ~
66426382 =/ n=@ud 0
66436383 |-
66446384 ?~ 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])))
6650− $(vars t.vars, ren [[i.vars replacement] ren], n ?:(own n +(n)), used ?:(own [name used] used))
6651−::
6652−:: +letter-free: the first number from n whose letter is none of names
6653−::
6654−++ letter-free
6655− |= [n=@ud names=(list @t)]
6656− ^- @ud
6657− ?. (lien names |=(m=@t =(m (crip (show-var n))))) n
6658− $(n +(n))
6659−::
6660−:: +instantiate-scheme: a scheme's type with fresh quantified variables
6661−::
6662−:: Each fresh variable keeps the name of the one it replaces.
6385+ =/ replacement=itype ?:((itype-var-is-restricted i.vars t) [%rvar n] ?:((itype-var-is-atom i.vars t) [%avar n] ?:((itype-var-is-gate-free i.vars t) [%fvar n] [%var n])))
6386+ $(vars t.vars, ren [[i.vars replacement] ren], n +(n))
66636387::
66646388++ instantiate-scheme
66656389 |= [scheme=ischeme state=istate]
@@ -6668,13 +6392,12 @@
66686392 =/ vars=(list @ud) vars.scheme
66696393 |-
66706394 ?~ vars [(itype-rename typ.scheme ren) state]
6671− =/ fresh=@ud (named-var (var-name i.vars) next.state)
66726395 =/ 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])))
66746397 :: A generalized atom variable is a valid origin for re-generalizing
66756398 :: an alias, just as a sample binder is.
66766399 =/ 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]
66786401 $(vars t.vars, ren [[i.vars replacement] ren], state st)
66796402::
66806403++ icap-lookup
@@ -7534,8 +7257,7 @@
75347257 ?: in-mold.state ~
75357258 =/ n=(unit @ud) (icap-lookup name.sh caps.state)
75367259 ?^ 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])]
75397261 * ~
75407262 ==
75417263::
@@ -7568,12 +7290,12 @@
75687290 ^- isample-result
75697291 ?- -.s
75707292 %bind
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))))
75727294 [%| "sample shadows a name"]
75737295 =/ t=itype [%var next.state]
75747296 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]
75757297 %face
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))))
75777299 [%| "sample shadows a name"]
75787300 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)
75797301 ?~ t [%| "sample mold is not supported by partial inference"]
@@ -7641,7 +7363,7 @@
76417363 |-
76427364 ?~ ds &
76437365 ?: ?=(%mold -.i.ds) $(ds t.ds)
7644− ?: (reserved-name name.i.ds) |
7366+ ?: =(name.i.ds %proj) |
76457367 ?. (unique-value-name name.i.ds names) |
76467368 ?: ?=(^ (ienv-lookup name.i.ds env)) |
76477369 ?: (lien globals.state |=(n=term =(n name.i.ds))) |
@@ -7665,7 +7387,7 @@
76657387 |-
76667388 ?~ locals &
76677389 =/ n=term name.i.locals
7668− ?: (reserved-name n) |
7390+ ?: =(n %proj) |
76697391 ?. (unique-value-name n names) |
76707392 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |
76717393 ?: (lien marks.state |=(m=term =(n m))) |
@@ -7815,8 +7537,7 @@
78157537 ^- istate
78167538 ?~ sites state
78177539 ?: ?=(^ (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]))
78207541::
78217542++ reserve-def-caps
78227543 |= [e=expr state=istate]
@@ -7990,8 +7711,7 @@
79907711 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))
79917712 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
79927713 =. 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 &)
79957715::
79967716:: Try complete cyclic local groups after individual definitions stall.
79977717:: Components with non-gates or unresolved constraints stay unavailable.
@@ -8345,7 +8065,7 @@
83458065 [%| ["list branch pattern is not supported by partial inference" ~]]
83468066 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)
83478067 ?~ 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)))))
83498069 [%| ["pattern binder shadows a name" ~]]
83508070 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]
83518071 =/ left=iresult
@@ -8382,7 +8102,7 @@
83828102 [%| ["unit branch pattern is not supported by partial inference" ~]]
83838103 =/ binder=(unit term) ?:(first-empty second-name first-name)
83848104 ?~ 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))))
83868106 [%| ["pattern binder shadows a name" ~]]
83878107 =/ payload=(unit itype) (unit-union-payload typ)
83888108 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]
@@ -8489,7 +8209,7 @@
84898209 ^- (unit ienv)
84908210 =. t ?:(?=(%face -.t) body.t t)
84918211 ?: ?=(%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)))) ~
84938213 `[[name.p [t ~]] env]
84948214 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)
84958215 `env
@@ -9015,9 +8735,7 @@
90158735 `subject
90168736::
90178737:: Infer changes only against a fully known record spine. Retain the
9018−:: target type; unknown spines and overlapping edits remain unsupported.
9019−:: An edit's wing, as open.cart, reads through record fields only,
9020−:: outermost first, and its value fits the field it names.
8738+:: target type; unknown spines and repeated edits remain unsupported.
90218739++ change-spine-known
90228740 |= [t=itype sub=isub]
90238741 ^- ?
@@ -9029,18 +8747,19 @@
90298747 $(t tal.t)
90308748::
90318749++ 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)]
90338751 ^- iresult
90348752 ?~ edits [%& target state]
90358753 =/ entry=edit i.edits
9036− =/ outer=(list term) (flop names.entry)
9037− ?: (lien seen |=(prior=(list term) (wing-overlap prior outer)))
8754+ ?: (lien seen |=(name=term =(name name.entry)))
90388755 [%| ["repeated change fields are not supported by partial inference" ~]]
90398756 ?. (change-spine-known target sub.state)
90408757 [%| ["change target needs a known record in partial inference" ~]]
9041− =/ field=(each itype idiag) (change-wing-field entry target sub.state)
9042− ?: ?=(%| -.field) [%| p.field]
9043− =/ expected=itype p.field
8758+ =/ found=(list itype) (record-fields-named name.entry target sub.state)
8759+ ?~ found
8760+ [%| ["record has no field `{(trip name.entry)}`" ~[[at.entry "unknown field"]]]]
8761+ ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
8762+ =/ expected=itype i.found
90448763 =/ value=iresult (infer-call-context-arg val.entry expected env state at.entry)
90458764 ?: ?=(%| -.value) value
90468765 =/ fit=ifit (itype-fit typ.p.value expected sub.state.p.value next.state.p.value)
@@ -9049,67 +8768,7 @@
90498768 =/ decimal=(unit idiag) (decimal-misfit val.entry typ.p.value expected sub.state.p.value next.state.p.value)
90508769 ?^ decimal [%| u.decimal]
90518770 [%| ["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])
9053−::
9054−:: +change-wing-field: the type of the field an edit's wing names in
9055−:: a known record target, read through record fields, outermost first
9056−::
9057−++ change-wing-field
9058− |= [entry=edit target=itype sub=isub]
9059− ^- (each itype idiag)
9060− =/ outer=(list term) (flop names.entry)
9061− =/ k=@ud (lent names.entry)
9062− =/ typ=itype target
9063− =| through=(unit [name=term at=span])
9064− |- ^- (each itype idiag)
9065− ?~ outer [%& typ]
9066− =/ here=span (edit-name-at entry (dec k))
9067− ?: &(?=(^ through) !(change-spine-known typ sub))
9068− ?. (itype-not-record typ sub)
9069− [%| ["change wing needs a known record in partial inference" ~]]
9070− =/ label=tape "field `{(trip name.u.through)}`"
9071− :- %|
9072− :- "change wing `{(show-names names.entry)}` goes through `{(trip name.u.through)}`, which is not a record"
9073− ~[[at.u.through (site-type-note label typ sub)]]
9074− =/ found=(list itype) (record-fields-named i.outer typ sub)
9075− ?~ found
9076− [%| ["record has no field `{(trip i.outer)}`" ~[[here "unknown field"]]]]
9077− ?^ t.found [%| ["change field is ambiguous in partial inference" ~]]
9078− $(outer t.outer, k (dec k), typ i.found, through `[i.outer here])
9079−::
9080−:: +edit-name-at: where the kth name of an edit's wing is written,
9081−:: counting from 0: its names are joined by dots from the edit's start
9082−::
9083−++ edit-name-at
9084− |= [e=edit k=@ud]
9085− ^- span
9086− =/ col=@ud col.beg.at.e
9087− =/ ns=(list term) names.e
9088− |- ^- span
9089− ?~ ns at.e
9090− =/ len=@ud (met 3 i.ns)
9091− ?: =(0 k) [[line.beg.at.e col] [line.beg.at.e (add col len)]]
9092− $(ns t.ns, k (dec k), col +((add col len)))
9093−::
9094−:: +itype-not-record: whether a type is surely no record: an atom, a
9095−:: loobean, a list or other collection, a gate, a union or a noun
9096−::
9097−++ itype-not-record
9098− |= [t=itype sub=isub]
9099− ^- ?
9100− =. t (itype-walk t sub)
9101− ?=(?(%atom %any-atom %flag %const %tag %collection %fn %union %noun %empty) -.t)
9102−::
9103−:: +wing-overlap: whether two edits' wings, outermost first, name the
9104−:: same field or one a field inside the other's
9105−::
9106−++ wing-overlap
9107− |= [a=(list term) b=(list term)]
9108− ^- ?
9109− ?~ a &
9110− ?~ b &
9111− ?. =(i.a i.b) |
9112− $(a t.a, b t.b)
8771+ $(edits t.edits, state state.p.value(sub sub.fit, next next.fit), seen [name.entry seen])
91138772::
91148773:: Backtick constructs the canonical prelude unit, after checking its
91158774:: prepared template has the standard null and [~ u=A] cases.
@@ -9479,7 +9138,6 @@
94799138 [%& typ.instance state.instance]
94809139 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)
94819140 ?~ scheme
9482− ?: =(i.names.e %unface) [%| (unface-value at.e)]
94839141 ?~ prelude.state [%| ["name is not available to partial inference" ~]]
94849142 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)
94859143 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]
@@ -9487,10 +9145,7 @@
94879145 [%& typ.inst state.inst]
94889146 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)
94899147 [%& typ.instance state.instance]
9490− %group
9491− ?: &(?=(%wing -.inner.e) =(names.inner.e ~[%unface]) ?=(~ (ienv-lookup %unface env)))
9492− [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
9493− $(e inner.e)
9148+ %group $(e inner.e)
94949149 %change
94959150 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]
94969151 =/ target=iresult $(e [%wing at.e target.e])
@@ -9634,7 +9289,6 @@
96349289 ?~ args.e [%| ["call has no argument" ~]]
96359290 ?: (explicit-proj-call e env state)
96369291 [%| ["proj needs an expected record type" ~]]
9637− ?: (reserved-call %unface e env state) (infer-unface e env state)
96389292 (infer-call-with-head e env state (infer-fragment head.e env state))
96399293 * [%| ["expression is not supported by partial inference" ~]]
96409294 ==
@@ -10025,7 +9679,6 @@
100259679 ^- iresult
100269680 ?> ?=(%call -.e)
100279681 ?~ args.e [%| ["call has no argument" ~]]
10028− ?: (reserved-call %unface e env state) (infer-unface e env state)
100299682 =/ head=iresult (infer-fragment head.e env state)
100309683 ?: ?=(%| -.head) head
100319684 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)
@@ -10108,70 +9761,18 @@
101089761 `(infer-simple-items items.e env state)
101099762 `(width-infer-items items.e index.u.target env state context)
101109763::
10111−:: +reserved-call: whether e calls the reserved operation n
10112−::
10113−:: Experimental intrinsic recognition; real bindings retain normal calls.
10114−++ reserved-call
10115− |= [n=term e=expr env=ienv state=istate]
10116− ^- ?
10117− ?. ?=(%call -.e) |
10118− ?. ?=(%wing -.head.e) |
10119− ?. =(names.head.e ~[n]) |
10120− ?: ?=(^ (ienv-lookup n env)) |
10121− ?: (lien globals.state |=(x=term =(x n))) |
10122− ?~ prelude.state &
10123− ?:(?=(^ (ienv-lookup n values.u.prelude.state)) | &)
9764+:: Experimental intrinsic recognition; real bindings retain normal calls.
101249765++ explicit-proj-call
101259766 |= [e=expr env=ienv state=istate]
101269767 ^- ?
101279768 ?. ?=(%call -.e) |
101289769 ?. ?=([* ~] args.e) |
10129− (reserved-call %proj e env state)
10130−::
10131−:: +infer-unface: (unface e), e's type with every face removed
10132−::
10133−:: A reserved operation handled by type, like proj. Any number of
10134−:: arguments is taken here so that a wrong count is an error. A type
10135−:: not yet known would wait, as wing access does; the partial checker
10136−:: has no such wait and reports it as unsupported, as it does field
10137−:: access on such a type.
10138−++ infer-unface
10139− |= [e=expr env=ienv state=istate]
10140− ^- iresult
10141− ?> ?=(%call -.e)
10142− ?. ?=([* ~] args.e)
10143− [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]
10144− ?^ defer.state [%| ["deferred unface needs unsupported inference" ~]]
10145− =/ value=iresult (infer-fragment i.args.e env state)
10146− ?: ?=(%| -.value) value
10147− =/ typ=itype (itype-walk typ.p.value sub.state.p.value)
10148− ?: ?=(?(%var %fvar) -.typ)
10149− [%| ["unface on a type not yet known is not supported by partial inference" ~]]
10150− [%& (itype-unface typ sub.state.p.value) state.p.value]
10151−::
10152−:: +unface-value: the error for unface written where a value goes
10153−::
10154−++ unface-value
10155− |= at=span
10156− ^- idiag
10157− ["unface is not a value; write |=(g (unface g))" ~[[at "unface used as a value"]]]
10158−::
10159−:: +unfaced-gate: the gate under a ++'s (unface |= …), or ~
10160−::
10161−:: Such a ++ is a gate for recursion: its own name has the unfaced
10162−:: type, and its body may call it.
10163−++ unfaced-gate
10164− |= [e=expr env=ienv state=istate]
10165− ^- (unit expr)
10166− ?: ?=(%group -.e) $(e inner.e)
10167− ?. (reserved-call %unface e env state) ~
10168− ?> ?=(%call -.e)
10169− ?. ?=([* ~] args.e) ~
10170− =/ gate=expr i.args.e
10171− |-
10172− ?: ?=(%group -.gate) $(gate inner.gate)
10173− ?. ?=(?(%gate %gate-wide) -.gate) ~
10174− `gate
9770+ ?. ?=(%wing -.head.e) |
9771+ ?. =(names.head.e ~[%proj]) |
9772+ ?: ?=(^ (ienv-lookup %proj env)) |
9773+ ?: (lien globals.state |=(n=term =(n %proj))) |
9774+ ?~ prelude.state &
9775+ ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)
101759776++ infer-proj-source
101769777 |= [e=expr expected=itype env=ienv state=istate context=span]
101779778 ^- iresult
@@ -10578,7 +10179,7 @@
1057810179 ?~ pats [%& ~]
1057910180 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']
1058010181 =/ 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))))
1058210183 [%| 'pattern shadows a name']
1058310184 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])
1058410185 ?: ?=(%| -.rest) rest
@@ -10655,12 +10256,24 @@
1065510256 ^- tape
1065610257 =. t (itype-walk t sub)
1065710258 ?- -.t
10658− %var (show-var id.t)
10659− %fvar (show-var id.t)
10660− %avar (show-var id.t)
10661− %rvar (show-var id.t)
10662− %nvar (show-var id.t)
10663− %rnvar (show-var id.t)
10259+ %var
10260+ ?: (lth id.t 26) [(add 65 id.t) ~]
10261+ "T{<id.t>}"
10262+ %fvar
10263+ ?: (lth id.t 26) [(add 65 id.t) ~]
10264+ "T{<id.t>}"
10265+ %avar
10266+ ?: (lth id.t 26) [(add 65 id.t) ~]
10267+ "T{<id.t>}"
10268+ %rvar
10269+ ?: (lth id.t 26) [(add 65 id.t) ~]
10270+ "T{<id.t>}"
10271+ %nvar
10272+ ?: (lth id.t 26) [(add 65 id.t) ~]
10273+ "T{<id.t>}"
10274+ %rnvar
10275+ ?: (lth id.t 26) [(add 65 id.t) ~]
10276+ "T{<id.t>}"
1066410277 %atom "@{(trip aura.t)}"
1066510278 %any-atom "@"
1066610279 %flag "?"
@@ -10681,17 +10294,6 @@
1068110294 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"
1068210295 ==
1068310296::
10684−:: +show-var: a type variable as printed: its name if it has one, else
10685−:: a letter for its number, A to Z, then T26, T27 and on
10686−::
10687−++ show-var
10688− |= id=@ud
10689− ^- tape
10690− =/ name=@t (var-name id)
10691− ?. =(0 name) (trip name)
10692− ?: (lth id 26) [(add 65 id) ~]
10693− "T{<id>}"
10694−::
1069510297++ show-itype-item
1069610298 |= [t=itype sub=isub]
1069710299 ^- tape
@@ -10750,7 +10352,7 @@
1075010352 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label
1075110353 ?: (itype-has-hidden-recursive normalized) label
1075210354 =/ 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)
1075410356 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"
1075510357::
1075610358:: A capital in a written mold is generalized with its enclosing ++.
@@ -10791,116 +10393,6 @@
1079110393 ?: =(n u.ident) `i.caps
1079210394 $(caps t.caps)
1079310395::
10794−:: +cap-names: give each variable in vars the name it was written with
10795−::
10796−:: Unification joins variables, and the one an ID resolves to may not
10797−:: carry the name its definition wrote, as when a capital meets a
10798−:: called gate's variable or an atom variable. Each variable in vars
10799−:: takes the name of the first capital in caps that resolves to it;
10800−:: failing that, of the earliest made of the named variables that
10801−:: resolve to it, itself included (+joined-names). Only the name part
10802−:: of an ID changes, not its count, so IDs stay distinct.
10803−::
10804−++ cap-names
10805− |= [typ=itype vars=(list @ud) caps=icaps sub=isub]
10806− ^- [typ=itype vars=(list @ud)]
10807− =/ written=icaps (flop caps)
10808− =/ joined=(map @ud @ud) (joined-names sub)
10809− =/ ren=(map @ud @ud) ~
10810− =/ out=(list @ud) ~
10811− |-
10812− ?~ vars [?~(ren typ (itype-reid typ ren)) (flop out)]
10813− =/ cap=(unit icap) (cap-with-id i.vars written sub)
10814− =/ first=(unit @ud) (~(get by joined) i.vars)
10815− =/ name=@t
10816− ?^ cap name.u.cap
10817− ?~ first (var-name i.vars)
10818− ?: =(0 (var-name i.vars)) (var-name u.first)
10819− ?: (lth (var-count u.first) (var-count i.vars)) (var-name u.first)
10820− (var-name i.vars)
10821− =/ to=@ud (named-var name i.vars)
10822− ?: =(to i.vars) $(vars t.vars, out [i.vars out])
10823− $(vars t.vars, out [to out], ren (~(put by ren) i.vars to))
10824−::
10825−:: +joined-names: for each variable that named ones resolve to, the
10826−:: earliest made of those, by count
10827−::
10828−:: One pass over sub keeps each ID's newest binding, as +itype-lookup
10829−:: would find it: the variable it is bound to, or ~ for another type.
10830−:: Each named ID then follows those bindings to the variable it
10831−:: resolves to, if any.
10832−::
10833−++ joined-names
10834− |= sub=isub
10835− ^- (map @ud @ud)
10836− =/ edges=(map @ud (unit @ud))
10837− %+ roll (flop sub)
10838− |= [b=ibinding m=(map @ud (unit @ud))]
10839− (~(put by m) id.b (var-of val.b))
10840− =/ named=(list @ud)
10841− (murn ~(tap by edges) |=([k=@ud *] ?:(=(0 (var-name k)) ~ `k)))
10842− =/ fuel=@ud ~(wyt by edges)
10843− =/ out=(map @ud @ud) ~
10844− |-
10845− ?~ named out
10846− =/ root=(unit @ud) (follow-var i.named edges fuel)
10847− ?~ root $(named t.named)
10848− ?: =(u.root i.named) $(named t.named)
10849− =/ best=(unit @ud) (~(get by out) u.root)
10850− ?: &(?=(^ best) (lth (var-count u.best) (var-count i.named)))
10851− $(named t.named)
10852− $(named t.named, out (~(put by out) u.root i.named))
10853−::
10854−:: +follow-var: the variable that id resolves to through edges, or ~ if
10855−:: it resolves to another type; fuel bounds the steps
10856−::
10857−++ follow-var
10858− |= [id=@ud edges=(map @ud (unit @ud)) fuel=@ud]
10859− ^- (unit @ud)
10860− |-
10861− ?: =(0 fuel) ~
10862− =/ edge=(unit (unit @ud)) (~(get by edges) id)
10863− ?~ edge `id
10864− ?~ u.edge ~
10865− ?: =(u.u.edge id) `id
10866− $(id u.u.edge, fuel (dec fuel))
10867−::
10868−:: +var-of: the ID of a type variable node, or ~ for another type
10869−::
10870−++ var-of
10871− |= t=itype
10872− ^- (unit @ud)
10873− ?+ -.t ~
10874− %var `id.t
10875− %fvar `id.t
10876− %avar `id.t
10877− %rvar `id.t
10878− %nvar `id.t
10879− %rnvar `id.t
10880− ==
10881−::
10882−:: +itype-reid: t with the variable IDs in ids replaced, each node
10883−:: keeping its kind
10884−::
10885−++ itype-reid
10886− |= [t=itype ids=(map @ud @ud)]
10887− ^- itype
10888− ?- -.t
10889− %var t(id (fall (~(get by ids) id.t) id.t))
10890− %fvar t(id (fall (~(get by ids) id.t) id.t))
10891− %avar t(id (fall (~(get by ids) id.t) id.t))
10892− %rvar t(id (fall (~(get by ids) id.t) id.t))
10893− %nvar t(id (fall (~(get by ids) id.t) id.t))
10894− %rnvar t(id (fall (~(get by ids) id.t) id.t))
10895− ?(%atom %any-atom %flag %noun %empty %tag %const %recursive %jrec) t
10896− %union t(cases (turn cases.t |=(c=itype ^$(t c))), args (turn args.t |=(c=itype ^$(t c))))
10897− %grec t(args (turn args.t |=(c=itype ^$(t c))))
10898− %collection t(args (turn args.t |=(c=itype ^$(t c))))
10899− %face t(body $(t body.t))
10900− %fn t(sample $(t sample.t), product $(t product.t))
10901− %cell t(hed $(t hed.t), tal $(t tal.t))
10902− ==
10903−::
1090410396++ merged-capitals
1090510397 |= [caps=icaps sub=isub]
1090610398 ^- (unit [first=icap second=icap])
@@ -11120,9 +10612,6 @@
1112010612 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]
1112110613 =. gate-defs.state ~
1112210614 ?. ?=(%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
1112610615 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
1112710616 [%| ["recursive definition is not a gate" ~]]
1112810617 =/ result=(unit itype) (recursive-branch-seed d env state)
@@ -11146,7 +10635,6 @@
1114610635 =/ product=itype ?~(result [%var id] u.result)
1114710636 =/ st=istate state.p.sam(next +(id))
1114810637 =/ seed=itype [%fn typ.p.sam product]
11149− =? seed ?=(^ peeled) (itype-unface seed sub.st)
1115010638 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]
1115110639 =/ body=expr
1115210640 ?- -.gate
@@ -11158,9 +10646,7 @@
1115810646 ?: ?=(%| -.out) out
1115910647 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)
1116010648 ?~ 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)]
1116410650::
1116510651++ dependency-root
1116610652 |= names=(list term)
@@ -11268,7 +10754,7 @@
1126810754:: Infer a cyclic component with one monomorphic seed per gate. All members
1126910755:: must succeed before any scheme is available; pending constraints and
1127010756:: 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]
1127210758+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)
1127310759++ seed-gate-group
1127410760 |= [ds=(list def) env=ienv state=istate]
@@ -11276,9 +10762,7 @@
1127610762 ?~ ds [%& [~ state]]
1127710763 =/ d=def i.ds
1127810764 ?. ?=(%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
1128210766 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))
1128310767 [%| ["recursive group contains a non-gate" ~]]
1128410768 =/ initial=istate (reserve-def-caps gate state)
@@ -11296,8 +10780,7 @@
1129610780 * !!
1129710781 ==
1129810782 =/ 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]
1130110784 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)
1130210785 =/ rest=igate-seeds $(ds t.ds, state after)
1130310786 ?: ?=(%| -.rest) rest
@@ -11337,7 +10820,6 @@
1133710820 ?: (constrained-capitals caps.entry sub.state)
1133810821 [%| ["explicit capital constraints are not supported by partial inference" ~]]
1133910822 =/ typ=itype (itype-normalize typ.entry sub.state)
11340− =? typ unfaced.entry (itype-unface typ ~)
1134110823 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]
1134210824 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))
1134310825 [%| ["recursive group needs unsupported inference" ~]]
@@ -11346,7 +10828,7 @@
1134610828 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))
1134710829 =/ rest=(each ienv idiag) $(entries t.entries)
1134810830 ?: ?=(%| -.rest) rest
11349− [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]
10831+ [%& [[name.entry [typ vars]] p.rest]]
1135010832::
1135110833++ infer-gate-group
1135210834 |= [ds=(list def) env=ienv state=istate]
@@ -11391,7 +10873,7 @@
1139110873 `[entry u.rest]
1139210874::
1139310875
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)]
1139510877+$ iadj (map term (list term))
1139610878+$ ivisited (map term ?)
1139710879+$ iwork (list [name=term done=?])
@@ -11487,7 +10969,7 @@
1148710969++ add-groups
1148810970 |= [ds=(list def) components=icomponents graph=iadj env=ienv grouped=(list term) artifacts=(list iwidth-definition) state=istate]
1148910971 ^- iresolved
11490− ?~ components [env grouped artifacts ~]
10972+ ?~ components [env grouped artifacts]
1149110973 =/ component=(list term) i.components
1149210974 ?. (graph-cycle component graph) $(components t.components)
1149310975 ?: (lien component |=(n=term ?=(^ (ienv-lookup n env)))) $(components t.components)
@@ -11528,13 +11010,11 @@
1152811010 =? artifacts ?=(^ u.finalized)
1152911011 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]
1153011012 =? 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]
1153211014++ add-supported-defs-core
1153311015 |= [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])]
11535− =/ failures=(list [name=term diag=idiag]) ~
11536− |-
11537− ?~ ds [env artifacts (flop failures)]
11016+ ^- [env=ienv artifacts=(list iwidth-definition)]
11017+ ?~ ds [env artifacts]
1153811018 =/ d=def i.ds
1153911019 ?: ?=(%mold -.d) $(ds t.ds)
1154011020 ?. (unique-value-name name.d globals) $(ds t.ds)
@@ -11545,34 +11025,37 @@
1154511025 =. gate-defs.initial checked
1154611026 =. head-evidence.initial heads
1154711027 =. initial (reserve-def-caps val.d initial)
11548− =/ plain=iresult (infer-fragment val.d env initial)
11549− =/ result=iresult plain
11028+ =/ result=iresult (infer-fragment val.d env initial)
1155011029 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11551− ?: ?=(%| -.result)
11552− =/ failure=idiag
11553− ?: (definite-diag p.result) p.result
11554− ?: ?=(%| -.plain) p.plain
11555− p.result
11556− =? failures (definite-diag failure) [[name.d failure] failures]
11557− $(ds t.ds)
1155811030 =/ added=(unit iadded-definition)
1155911031 (add-supported-result d result initial env checked artifacts)
1156011032 ?~ added $(ds t.ds)
1156111033 $(ds t.ds, env env.u.added, checked checked.u.added, artifacts artifacts.u.added)
1156211034::
11563−:: Retry one unresolved definition to explain a pending tag. The gate
11564−:: evidence is built from the whole module, not only this definition.
11565−++ module-pending-tag-one
11566− |= [d=def env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence)]
11035+:: Full checking discards unsupported definitions. On that failure path only,
11036+:: retry a bounded number of missing definitions to explain a pending tag
11037+:: from the same ordinary inference state instead of hiding it behind the
11038+:: generic completeness error. No successful definition takes this path.
11039+++ module-pending-tag
11040+ |= [ds=(list def) env=ienv base=istate fuel=@ud]
1156711041 ^- (unit [at=span msg=tape])
11568− ?. ?=(%value -.d) ~
11569− ?^ (ienv-lookup name.d env) ~
11042+ =/ checked=(map term def) (direct-checked-gates ds env)
11043+ =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude.base)
11044+ |-
11045+ ?~ ds ~
11046+ ?: =(0 fuel) ~
11047+ =/ d=def i.ds
11048+ ?: ?=(%mold -.d) $(ds t.ds, fuel (dec fuel))
11049+ ?^ (ienv-lookup name.d env) $(ds t.ds, fuel (dec fuel))
1157011050 =/ initial=istate base(gate-defs checked, head-evidence heads)
1157111051 =. initial (reserve-def-caps val.d initial)
1157211052 =/ result=iresult (infer-fragment val.d env initial)
1157311053 =? result ?=(%| -.result) (infer-recursive-gate d env initial)
11574− ?: ?=(%| -.result) ~
11575− (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11054+ ?: ?=(%| -.result) $(ds t.ds, fuel (dec fuel))
11055+ =/ pending=(unit [at=span msg=tape])
11056+ (pending-tag-diagnostic tags.state.p.result sub.state.p.result)
11057+ ?^ pending pending
11058+ $(ds t.ds, fuel (dec fuel))
1157611059::
1157711060++ resolve-groups-core
1157811061 |= [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 @@
1158811071 =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence ds prelude)
1158911072 =/ ordered=(list def) (dependency-order ds components)
1159011073 |-
11591− =/ next=[env=ienv artifacts=(list iwidth-definition) failures=(list [name=term diag=idiag])]
11074+ =/ next=[env=ienv artifacts=(list iwidth-definition)]
1159211075 (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)
1159311076 =/ initial=istate [0 ~ ~ ~ molds globals externals surs mark-externals marks jimports reserved-molds ~ ~ ~ | at top prelude ~ 256 ~ ~ ~ ~ ~ ~]
1159411077 =. grec-index.initial index
1159511078 =/ 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
1159711080 $(env env.out, grouped grouped.out, artifacts artifacts.out)
1159811081::
1159911082:: +dependency-order: the value definitions, dependencies first
@@ -12465,29 +11948,13 @@
1246511948 =/ first=(unit idiag) ?:(?=(%expr -.i.segs) (duplicate-expr p.i.segs) ~)
1246611949 ?^ first first
1246711950 $(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.
1247011951++ duplicate-edits
1247111952 |= edits=(list edit)
1247211953 ^- (unit idiag)
12473− =| seen=(list edit)
12474− |- ^- (unit idiag)
1247511954 ?~ edits ~
12476− =/ e=edit i.edits
12477− =/ prior=(list edit)
12478− (skim seen |=(p=edit (wing-overlap (flop names.p) (flop names.e))))
12479− ?^ prior
12480− =/ same=? =(names.i.prior names.e)
12481− =/ sites=(list [at=span note=tape])
12482− :~ [at.i.prior "first field"]
12483− [at.e ?:(same "repeated field" "overlapping field")]
12484− ==
12485− ?: same `["change field `{(show-names names.e)}` is repeated" sites]
12486− =/ a=tape (show-names names.i.prior)
12487− `["change fields `{a}` and `{(show-names names.e)}` overlap" sites]
12488− =/ first (duplicate-expr val.e)
11955+ =/ first (duplicate-expr val.i.edits)
1248911956 ?^ first first
12490− $(edits t.edits, seen [e seen])
11957+ $(edits t.edits)
1249111958++ duplicate-arms
1249211959 |= arms=(list arm)
1249311960 ^- (unit idiag)
@@ -12560,142 +12027,59 @@
1256012027 ==
1256112028 [n $(imports t.imports)]
1256212029::
12563−:: +reserved-name: whether n names a reserved operation
12564−::
12565−:: proj and unface are handled by the checker by type, not bound, so
12566−:: no module may define, import or bind either name, as a value or
12567−:: as a mold. A field, tag or path segment may still be spelled so.
12568−++ reserved-name
12569− |= n=term
12570− ^- ?
12571− |(=(n %proj) =(n %unface))
12572−++ reserved-sample
12030+++ reserved-proj-sample
1257312031 |= sam=sample
1257412032 ^- ?
1257512033 ?- -.sam
12576− %bind (reserved-name name.sam)
12577− %face (reserved-name name.sam)
12578− %pun (reserved-name name.sam)
12579− %cell (lien items.sam reserved-sample)
12034+ %bind =(name.sam %proj)
12035+ %face =(name.sam %proj)
12036+ %pun =(name.sam %proj)
12037+ %cell (lien items.sam reserved-proj-sample)
1258012038 * |
1258112039 ==
12582−++ reserved-pattern
12040+++ reserved-proj-pattern
1258312041 |= p=pattern
1258412042 ^- ?
1258512043 ?- -.p
12586− %bind (reserved-name name.p)
12587− %cell (lien items.p reserved-pattern)
12044+ %bind =(name.p %proj)
12045+ %cell (lien items.p reserved-proj-pattern)
1258812046 * |
1258912047 ==
12590−++ reserved-def
12048+++ reserved-proj-def
1259112049 |= d=def
1259212050 ^- ?
12593− ?: (reserved-name name.d) &
12594− ?: ?=(%value -.d) (reserved-expr val.d)
12051+ ?: =(name.d %proj) &
12052+ ?: ?=(%value -.d) (reserved-proj-expr val.d)
1259512053 |
12596−++ reserved-expr
12054+++ reserved-proj-expr
1259712055 |= e=expr
1259812056 ^- ?
1259912057 ?- -.e
12600− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12601− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-expr p.p) |)))
12602− %change (lien edits.e |=(p=edit (reserved-expr val.p)))
12058+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12059+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))
12060+ %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))
1260312061 %pair $(e val.e)
1260412062 %unit $(e val.e)
1260512063 %group $(e inner.e)
12606− %list (lien items.e reserved-expr)
12607− %tuple (lien items.e |=(i=item (reserved-expr val.i)))
12608− ?(%gate %gate-wide) |((reserved-sample sample.e) $(e body.e))
12064+ %list (lien items.e reserved-proj-expr)
12065+ %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))
12066+ ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))
1260912067 %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))
1261112069 %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)))))
12613− %body |((lien defs.e reserved-def) $(e final.e))
12070+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))
12071+ %body |((lien defs.e reserved-proj-def) $(e final.e))
1261412072 * |
1261512073 ==
1261612074::
12617−++ module-has-reserved
12075+++ module-has-reserved-proj
1261812076 |= mod=module
1261912077 ^- ?
1262012078 =/ imported=(list term) (import-binding-names imports.mod)
1262112079 =/ vals=(list term) (global-value-names defs.mod)
1262212080 =/ molds=imolds (collect-simple-molds defs.mod)
1262312081 =/ 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))
12625−::
12626−:: A scope collision retains source sites. Prelude declarations may be in
12627−:: another source, so their name and namespace are retained separately.
12628−+$ iscope-diagnostic
12629− [issue=idiag prelude=(unit [name=term kind=?(%value %mold %any)])]
12630−++ scope-import-diagnostic
12631− |= [imports=(list import) prelude-values=(list term) prelude-molds=(list term) seen=written-fields]
12632− ^- (each written-fields iscope-diagnostic)
12633− ?~ imports [%& seen]
12634− =/ imp=import i.imports
12635− =/ n=term
12636− ?- -.imp
12637− %jibb face.imp
12638− %sur name.imp
12639− %mark mark.imp
12640− ==
12641− ?: (reserved-name n)
12642− [%| [["`{(trip n)}` is reserved and cannot be bound" ~[[at.imp "reserved name"]]] ~]]
12643− =/ earlier=(unit span) (~(get by seen) n)
12644− ?^ earlier
12645− [%| [["import `{(trip n)}` shadows an earlier import" ~[[u.earlier "earlier import"] [at.imp "conflicting import"]]] ~]]
12646− ?: |((lien prelude-values |=(x=term =(n x))) (lien prelude-molds |=(x=term =(n x))))
12647− [%| [["import `{(trip n)}` shadows a prelude name" ~[[at.imp "conflicting import"]]] `[n %any]]]
12648− $(imports t.imports, seen (~(put by seen) n at.imp))
12649−++ scope-def-diagnostic
12650− |= [defs=(list def) imports=written-fields prelude-values=(list term) prelude-molds=(list term) values=written-fields molds=written-fields]
12651− ^- (unit iscope-diagnostic)
12652− ?~ defs ~
12653− =/ d=def i.defs
12654− =/ n=term name.d
12655− ?: (reserved-name n)
12656− `[["`{(trip n)}` is reserved and cannot be bound" ~[[at.d "reserved name"]]] ~]
12657− =/ imported=(unit span) (~(get by imports) n)
12658− ?^ imported
12659− `[["definition `{(trip n)}` shadows an import" ~[[u.imported "import"] [at.d "conflicting definition"]]] ~]
12660− =/ seen=written-fields ?:(?=(%value -.d) values molds)
12661− =/ earlier=(unit span) (~(get by seen) n)
12662− ?^ earlier
12663− `[["definition `{(trip n)}` shadows an earlier definition" ~[[u.earlier "earlier definition"] [at.d "conflicting definition"]]] ~]
12664− =/ prelude-names=(list term) ?:(?=(%value -.d) prelude-values prelude-molds)
12665− ?: (lien prelude-names |=(x=term =(n x)))
12666− `[["definition `{(trip n)}` shadows a prelude name" ~[[at.d "conflicting definition"]]] `[n ?:(?=(%value -.d) %value %mold)]]
12667− ?: ?=(%value -.d)
12668− $(defs t.defs, values (~(put by values) n at.d))
12669− $(defs t.defs, molds (~(put by molds) n at.d))
12670−++ module-scope-diagnostic
12671− |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
12672− ^- (unit iscope-diagnostic)
12673− =/ imports=(each written-fields iscope-diagnostic)
12674− (scope-import-diagnostic imports.mod prelude-values prelude-molds ~)
12675− ?: ?=(%| -.imports) `p.imports
12676− (scope-def-diagnostic defs.mod p.imports prelude-values prelude-molds ~ ~)
12677−++ show-scope-diagnostic
12678− |= [file=path src=@t diagnostic=iscope-diagnostic prelude=(unit ifile)]
12679− ^- @t
12680− =/ excerpts=(list @t)
12681− %+ turn sites.issue.diagnostic
12682− |= site=[at=span note=tape]
12683− (show-error src [file line.beg.at.site col.beg.at.site note.site])
12684− =/ previous=(list @t)
12685− ?~ prelude.diagnostic ~
12686− ?~ prelude ~
12687− ?~ source.u.prelude ~
12688− =/ parsed (parse at.u.prelude u.source.u.prelude)
12689− ?: ?=(%| -.parsed) ~
12690− =/ matching=(list def)
12691− %+ skim defs.p.parsed
12692− |= d=def
12693− ?& =(name.d name.u.prelude.diagnostic)
12694− |(=(%any kind.u.prelude.diagnostic) =(-.d kind.u.prelude.diagnostic))
12695− ==
12696− ?~ matching ~
12697− ~[(show-error u.source.u.prelude [at.u.prelude line.beg.at.i.matching col.beg.at.i.matching "prelude declaration"])]
12698− (of-wain:format [(crip msg.issue.diagnostic) (weld excerpts previous)])
12082+ |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))
1269912083::
1270012084++ module-scope-valid
1270112085 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]
@@ -12704,7 +12088,7 @@
1270412088 =/ vals=(list term) (global-value-names defs.mod)
1270512089 =/ molds=imolds (collect-simple-molds defs.mod)
1270612090 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))
12707− ?: (module-has-reserved mod) |
12091+ ?: (module-has-reserved-proj mod) |
1270812092 ?. %+ levy imported
1270912093 |= n=term
1271012094 &((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 @@
1312712511 ?. (lien values |=(n=term =(n u.name))) $(ds t.ds)
1312812512 `[u.name at.s]
1312912513::
13130−:: Select the first available reason in dependency order, rather than
13131−:: preferring one class of diagnostic across the whole module. Only the
13132−:: first 64 definitions are retried for pending tags, as before.
13133−++ module-unresolved-diagnostic
13134− |= [ds=(list def) env=ienv base=istate checked=(map term def) heads=(unit igate-prelude-evidence) failures=(list [name=term diag=idiag]) values=(list term) file=path src=@t fuel=@ud]
13135− ^- (unit @t)
13136− ?~ ds ~
13137− =/ d=def i.ds
13138− =/ remaining=@ud ?:(=(0 fuel) 0 (dec fuel))
13139− ?: ?=(%mold -.d) $(ds t.ds, fuel remaining)
13140− ?^ (ienv-lookup name.d env) $(ds t.ds, fuel remaining)
13141− =/ found=(list [name=term diag=idiag])
13142− (skim failures |=(failure=[name=term diag=idiag] =(name.failure name.d)))
13143− ?^ found `(show-inference-diagnostic file src name.d diag.i.found)
13144− =/ pending=(unit [at=span msg=tape])
13145− ?: =(0 fuel) ~
13146− (module-pending-tag-one d env base checked heads)
13147− ?^ pending
13148− `(show-error src [file line.beg.at.u.pending col.beg.at.u.pending msg.u.pending])
13149− =/ shadow=(unit [name=term at=span]) (module-sample-shadow ~[d] env values)
13150− ?^ shadow
13151− =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
13152− `(show-error src [file line.beg.at.u.shadow col.beg.at.u.shadow msg])
13153− $(ds t.ds, fuel remaining)
13154−::
1315512514:: Cache only completed interfaces for this invocation. The source bundle,
1315612515:: imported Hoon types and prelude are fixed for the whole graph. Check the
1315712516:: active path and duplicate sources before consulting it, so a cache hit
@@ -13418,7 +12777,7 @@
1341812777 ^- ?
1341912778 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))
1342012779 =/ derived=(list term) (weld path-names poke-names)
13421− ?: (lien derived reserved-name) |
12780+ ?: (lien derived |=(n=term =(n %proj))) |
1342212781 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))
1342312782 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))
1342412783::
@@ -13450,7 +12809,7 @@
1345012809 =/ clashes=(list term)
1345112810 %+ skip names
1345212811 |= n=term
13453− ?| (reserved-name n)
12812+ ?| =(n %proj)
1345412813 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))
1345512814 ==
1345612815 ?~ clashes ~
@@ -14225,7 +13584,7 @@
1422513584 =/ action=term %poke
1422613585 =/ ordinary=(list def) ds
1422713586 =/ derived=(list term) ~[%state action]
14228− ?: (lien derived reserved-name) [%| ~]
13587+ ?: (lien derived |=(n=term =(n %proj))) [%| ~]
1422913588 =/ outer=(list term)
1423013589 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))
1423113590 =/ clashes=(list term)
@@ -14412,7 +13771,7 @@
1441213771 ?~ recovered ~
1441313772 ?. ?=(~ vars.u.recovered) ~
1441413773 ?. ?=(~ (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]
1441613775::
1441713776++ program-inferred-slot
1441813777 |= [typ=itype name=(unit term)]
@@ -14568,7 +13927,7 @@
1456813927 ?~ recovered ~
1456913928 ?. ?=(~ vars.u.recovered) ~
1457013929 ?. ?=(~ (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]
1457213931::
1457313932+$ iview-site [xs=expr mapper=term]
1457413933++ program-view-site
@@ -14895,7 +14254,7 @@
1489514254 ?~ recovered ~
1489614255 ?. ?=(~ vars.u.recovered) ~
1489714256 ?. ?=(~ (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]
1489914258::
1490014259:: Recover exactly one direct keyed each/turn row mapper, then its view.
1490114260:: The prelude's own each and turn schemes determine the mapper gate: the
@@ -15117,7 +14476,7 @@
1511714476 ?~ recovered ~
1511814477 ?. ?=(~ vars.u.recovered) ~
1511914478 ?. ?=(~ (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]
1512114480::
1512214481:: The model a direct program's initializer must produce. Update's written
1512314482:: two-item sample gives it when it can be read. Otherwise main's own program
@@ -15274,7 +14633,7 @@
1527414633 ?~ recovered ~
1527514634 ?. ?=(~ vars.u.recovered) ~
1527614635 ?. ?=(~ (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]
1527814637::
1527914638++ derived-poke-command-scheme
1528014639 |= [prelude=ifile action=itype]
@@ -15442,9 +14801,9 @@
1544214801 (direct-prelude-evidence ds prelude.initial)
1544314802 ?~ heads resolution
1544414803 =/ 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)]
1544614805 (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]
1544814807::
1544914808:: A static main may retain a generic element message in its ordinary
1545014809:: scheme. Instantiate that scheme, specialize it to canonical element !!,
@@ -15660,9 +15019,6 @@
1566015019 !(lien prelude-molds |=(m=term =(m n)))
1566115020 ==
1566215021 ==
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) ~]]
1566615022 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1566715023 ?~ prelude [%| [(crip "API module needs unsupported inference: {(spud at)}") ~]]
1566815024 =/ prepared=iprelude [u.prelude prelude-values prelude-molds]
@@ -15711,9 +15067,6 @@
1571115067 =/ ds=(list def) ?~(declared defs.mod defs.u.declared)
1571215068 =/ checking=module mod(defs ds)
1571315069 ?. (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) ~]]
1571715070 [%| [(crip "module has conflicting names: {(spud at)}") ~]]
1571815071 =/ vals=(list term) (global-value-names ds)
1571915072 =/ 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 @@
1578915142 ?~ store-parts ds
1579015143 (skim ds |=(d=def !&(?=(%value -.d) =(%main name.d))))
1579115144 ?. (module-values-complete required env)
15792− =/ components=icomponents (graph-components required (global-value-names required))
15793− =/ ordered=(list def) (dependency-order required components)
15145+ =/ pending=(unit [at=span msg=tape]) (module-pending-tag required env state 64)
15146+ ?^ pending
15147+ [%| [(show-error src [at line.beg.at.u.pending col.beg.at.u.pending msg.u.pending]) ~]]
15148+ :: A shadowing sample is an error, so it comes before any named value.
1579415149 =/ values=(list term) (weld prelude-values (weld (api-import-faces imports.mod) vals))
15795− =/ checked=(map term def) (direct-checked-gates required env)
15796− =/ heads=(unit igate-prelude-evidence) (direct-prelude-evidence required prelude.state)
15797− =/ diagnostic=(unit @t)
15798− (module-unresolved-diagnostic ordered env state checked heads failures.resolution values at src 64)
15799− ?^ diagnostic [%| [u.diagnostic ~]]
15150+ =/ shadow=(unit [name=term at=span]) (module-sample-shadow required env values)
15151+ ?^ shadow
15152+ =/ msg=tape "sample `{(trip name.u.shadow)}` shadows a name already in scope"
15153+ [%| [(show-error src [at line.beg.at.u.shadow col.beg.at.u.shadow msg]) ~]]
1580015154 =/ missing=(unit term) (module-missing-value required env)
1580115155 =/ named=tape ?~(missing "" ": ++ {(trip u.missing)}")
1580215156 [%| [(crip "module definitions need unsupported inference: {(spud at)}{named}") ~]]
@@ -16000,8 +15354,8 @@
1600015354 ?: ?=(%| -.parsed) (show-error src p.parsed)
1600115355 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)
1600215356 ?^ duplicate (duplicate-fields-report file src u.duplicate)
16003− ?: (module-has-reserved p.parsed)
16004− 'module has a reserved proj or unface name'
15357+ ?: (module-has-reserved-proj p.parsed)
15358+ 'module has reserved proj name'
1600515359 =/ ds=(list def) defs.p.parsed
1600615360 =/ molds=imolds (collect-simple-molds ds)
1600715361 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))
@@ -16079,7 +15433,7 @@
1607915433 =. head-evidence.initial heads
1608015434 =. initial (reserve-def-caps val.d initial)
1608115435 =/ result=iresult
16082− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))
15436+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))
1608315437 (infer-recursive-gate d env initial)
1608415438 (infer-fragment val.d env initial)
1608515439 ?: ?=(%| -.result)
@@ -16111,8 +15465,7 @@
1611115465 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))
1611215466 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)
1611315467 $(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)
1611615469 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")
1611715470 $(ds t.ds, lines [line lines])
1611815471:: Experimental module-owned pending-constraint generalization only.
@@ -16209,7 +15562,7 @@
1620915562 =/ normalized=itype (itype-normalize typ sub.state)
1621015563 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))
1621115564 =/ 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]]
1621315566::
1621415567+$ dgcommit [env=ienv state=istate]
1621515568:: A branch literal must not acquire a value face through replay.
@@ -16642,21 +15995,20 @@
1664215995 ?~ env `+(top)
1664315996 =/ sc=ischeme scheme.i.env
1664415997 ?: (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))))
1664615999::
16647−:: +itype-max-id: the largest variable or tag ID in t, or top, without
16648−:: the variables' names (+named-var)
16000+:: +itype-max-id: the largest variable or tag ID in t, or top
1664916001::
1665016002++ itype-max-id
1665116003 |= [t=itype top=@ud]
1665216004 ^- @ud
1665316005 ?- -.t
16654− %var (max top (var-count id.t))
16655− %fvar (max top (var-count id.t))
16656− %avar (max top (var-count id.t))
16657− %rvar (max top (var-count id.t))
16658− %nvar (max top (var-count id.t))
16659− %rnvar (max top (var-count id.t))
16006+ %var (max top id.t)
16007+ %fvar (max top id.t)
16008+ %avar (max top id.t)
16009+ %rvar (max top id.t)
16010+ %nvar (max top id.t)
16011+ %rnvar (max top id.t)
1666016012 %tag (max top id.t)
1666116013 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top
1666216014 %collection (itype-max-ids args.t top)