16c08c8 · jibb · git.iko.soy

docs/compiler.md+2

@@ -88,6 +88,8 @@ Nested labels of the three public re-exports are normalized recursively to `ask`

88

89For supported closed unions, the type printer keeps the union’s origin separate from its displayed name. It prints an in-scope name such as `msg` or `msg.lib`, including in records and gates; an accessible imported nongeneric alias may name a transitive union. A nongeneric body-local union that escapes its scope, or an origin without an accessible name, prints its cases separated by spaces, parenthesized when nested. That case-list form is print-only. A supported generic union prints its name and all arguments, including unused arguments; when its name is unavailable, the partial printer reports that limitation instead of dropping its arguments. Two faces for the same imported origin remain compatible; compatibility between distinct union origins, including in gate types, remains unsupported. Some comparisons of generic union arguments also remain unsupported rather than deciding equality or mismatch. The Hoon bridge also translates some imported unnamed unions into this representation; unsupported cases remain errors.

90

91+The type printer shows a type variable by the name it was written with. A variable's ID holds that name above a 64-bit count (`+named-var`), so the name travels through substitution, generalization and instantiation, and `+ienv-fresh-id` counts without it. When a definition is generalized, `+cap-names` names each quantified variable after a capital written in the definition that resolves to it, or else after the earliest made of the named variables joined with it; a call note does the same without the capitals. `+canonical-itype` keeps the names and numbers the other variables as the letters (`+show-var`) that no name in the same type spells.

92+

91Multi-argument calls form one right-nested sample: `f a b c` supplies `[a [b c]]`, with the last argument able to be a cell itself. The fragment fits the complete sample, preserving known faces and shared variables. Known sample positions can provide list or union context to arguments; unknown sample shapes use ordinary inference and some contextual forms remain unsupported. For a definite mismatch, the diagnostic points to a specific argument when it can establish which one failed; otherwise it reports the combined sample.

93Multi-argument calls form one right-nested sample: `f a b c` supplies `[a [b c]]`, with the last argument able to be a cell itself. The fragment fits the complete sample, preserving known faces and shared variables. Known sample positions can provide list or union context to arguments; unknown sample shapes use ordinary inference and some contextual forms remain unsupported. For a definite mismatch, the diagnostic points to a specific argument when it can establish which one failed; otherwise it reports the combined sample.

92

94

93A list literal can be inferred when a cast or known gate sample supplies a list type and the supplied prelude has the validated standard list definition. Empty, nonempty and nested literals work, including contextual union tags in elements; mismatched elements report the item and expected type. Imported Hoon lists share this representation. Under the same known context, `~` and zero-valued term literals fit an empty list, and a two-item unfaced cell `[head tail]` is a cons; cons cells and list literals can be nested. Mismatched heads or tails report both sites. A known list result also supplies context through complete loobean, unit-shaped and list-shaped branches, including recursive and nested branches. Known loobean result context can propagate through supported complete branches and binder-only cell arms, with a final directional fit; a binder-only arm over a union subject remains unsupported. A known gate with an unresolved result variable can also receive an enclosing result type before its argument is inferred, for example allowing `^- (list @t) (id ~)`; unknown callees and unresolved targets retain the conservative path. A known gate sample supplies context to corresponding positions of a single tuple or record argument, including nested cells; a zero literal can therefore fit a list position. A bound zero constant still remains unsupported rather than a definite mismatch, and an unknown callee does not supply context. Uncontextualized list literals also infer with a fresh element variable, including empty and nested lists; the resulting variable can generalize. Unresolved item tags and uncertain widening remain unsupported. Faced or longer cons cells, and a missing or altered prelude list remain unsupported. For a known standard list with a supported element type, it also infers a complete two-arm branch using `~` and `[item rest]`, in either order. The binders have the element and list types and cannot shadow or duplicate names. Unknown subjects, unsupported element types, other patterns and incomplete arms remain unsupported.

95A list literal can be inferred when a cast or known gate sample supplies a list type and the supplied prelude has the validated standard list definition. Empty, nonempty and nested literals work, including contextual union tags in elements; mismatched elements report the item and expected type. Imported Hoon lists share this representation. Under the same known context, `~` and zero-valued term literals fit an empty list, and a two-item unfaced cell `[head tail]` is a cons; cons cells and list literals can be nested. Mismatched heads or tails report both sites. A known list result also supplies context through complete loobean, unit-shaped and list-shaped branches, including recursive and nested branches. Known loobean result context can propagate through supported complete branches and binder-only cell arms, with a final directional fit; a binder-only arm over a union subject remains unsupported. A known gate with an unresolved result variable can also receive an enclosing result type before its argument is inferred, for example allowing `^- (list @t) (id ~)`; unknown callees and unresolved targets retain the conservative path. A known gate sample supplies context to corresponding positions of a single tuple or record argument, including nested cells; a zero literal can therefore fit a list position. A bound zero constant still remains unsupported rather than a definite mismatch, and an unknown callee does not supply context. Uncontextualized list literals also infer with a fresh element variable, including empty and nested lists; the resulting variable can generalize. Unresolved item tags and uncertain widening remain unsupported. Faced or longer cons cells, and a missing or altered prelude list remain unsupported. For a known standard list with a supported element type, it also infers a complete two-arm branch using `~` and `[item rest]`, in either order. The binders have the element and list types and cannot shadow or duplicate names. Unknown subjects, unsupported element types, other patterns and incomplete arms remain unsupported.

docs/spec/grammar.md+7−5

@@ -13,6 +13,7 @@ The syntax the compiler accepts.

13- **Spacing**: one space between items; more for alignment. That is style, which the formatter keeps: the parser takes one or more spaces between items, and allows spaces after an opener, before a closer and at the end of a line. Faces `name=value`, puns `=name` and typed path segments `[id=@ud]` take no spaces, and a rune is followed by one.

14- **Comments**: `::` to the end of the line, outside strings; inside a string, `::` is text.

15- **Names**: Hoon terms; lowercase letters, digits and hyphens, starting with a letter.

16+- **Type variables**: a capital, then lowercase letters and digits: `A`, `Msg`, `T2`. `AB`, `MSG`, `Msg_x` and `Msg-x` are errors. In a mold, a capitalized name is a type variable and a lowercase name is a mold: the reverse of Elm, where `Msg` is a concrete type and `msg` a type variable.

16

17

17## Literals

18## Literals

18

19

@@ -100,7 +101,7 @@ A file is a module: imports, then definitions.

100- `+$ name mold` defines a mold; `++ name expr` a value.

101- `+$ name mold` defines a mold; `++ name expr` a value.

101- Names may refer to each other in any order, and no name may shadow one already in scope, imports and the prelude included.

102- Names may refer to each other in any order, and no name may shadow one already in scope, imports and the prelude included.

102- Molds and values have separate namespaces, told apart by position: `todo-action.todo` is a mold, `poke.todo` its command helper, and `todos.todo` a mold and a request.

103- Molds and values have separate namespaces, told apart by position: `todo-action.todo` is a mold, `poke.todo` its command helper, and `todos.todo` a mold and a request.

103−- `main`'s type decides the kind: `(element !!)` a page; `(page R D)` a page with data, from parameters `R` to data `D`; `(program D X M)` an island, with data, model and messages; `(store S)` a store with state `S`. They're built by `(page load view)`, `(program init update view subs)` and `(store init update)`. A module without `main` is a library.

104+- `main`'s type decides the kind: `(element !!)` a page; `(page Params Data)` a page with data, from parameters to data; `(program Data Model Msg)` an island, with data, model and messages; `(store S)` a store with state `S`. They're built by `(page load view)`, `(program init update view subs)` and `(store init update)`. A module without `main` is a library.

104- Everything is exported and read through the import's face, as `card.card`. The prelude keeps private helpers in a separate internal module; it imports them without exposing them.

105- Everything is exported and read through the import's face, as `card.card`. The prelude keeps private helpers in a separate internal module; it imports them without exposing them.

105- An API module, `/ui/api/<agent>.jibb`, also exports derived gates: a generic `poke` command helper, adding the agent and mark and taking a reply, and a request per `paths` case, taking a reply over full state, plus a fold for `(facts full diff …)`. An island may watch a request only when the checker proves it is watchable. A request whose case has a separate `scry=` path, or whose watchability cannot be proved, is a type error. A store's local `+$ poke` is its ordinary action mold; a store exports a generic `poke` command helper and a `state` request. Clashing derived names are errors, including a derived name that clashes with an import face.

106- An API module, `/ui/api/<agent>.jibb`, also exports derived gates: a generic `poke` command helper, adding the agent and mark and taking a reply, and a request per `paths` case, taking a reply over full state, plus a fold for `(facts full diff …)`. An island may watch a request only when the checker proves it is watchable. A request whose case has a separate `scry=` path, or whose watchability cannot be proved, is a type error. A store's local `+$ poke` is its ordinary action mold; a store exports a generic `poke` command helper and a `state` request. Clashing derived names are errors, including a derived name that clashes with an import face.

106

107

@@ -121,15 +122,16 @@ Every other name is free.

121A mold is only a type: never called on a noun, and with no default. Types are inferred, Hindley–Milner with aura variables: every expression has a principal type, and there is no general subtyping. These one-way widenings are allowed: a value of a specific atom type fits `@`, a value of a specific noun type fits `*`, and a more specific aura fits an ancestor in its Hoon aura family; the reverse of each widening needs a check. Records can also be projected explicitly, as described below.

122A mold is only a type: never called on a noun, and with no default. Types are inferred, Hindley–Milner with aura variables: every expression has a principal type, and there is no general subtyping. These one-way widenings are allowed: a value of a specific atom type fits `@`, a value of a specific noun type fits `*`, and a more specific aura fits an ancestor in its Hoon aura family; the reverse of each widening needs a check. Records can also be projected explicitly, as described below.

122

123

123- **Partial annotations**: `_` may appear wherever a mold may appear. It marks a part of the type for the checker to infer, so a type annotation can specify only the parts it needs to. A hole inferred to be a named type variable is resolved: in `++ id |= x=A ^- _ x`, the result hole is `A`. An unconstrained hole is an error. A named mold or value definition must determine its own holes: `+$ box [item=_]` and `++ id |= x=_ x` do not determine their holes, and later uses cannot fix them.

124- **Partial annotations**: `_` may appear wherever a mold may appear. It marks a part of the type for the checker to infer, so a type annotation can specify only the parts it needs to. A hole inferred to be a named type variable is resolved: in `++ id |= x=A ^- _ x`, the result hole is `A`. An unconstrained hole is an error. A named mold or value definition must determine its own holes: `+$ box [item=_]` and `++ id |= x=_ x` do not determine their holes, and later uses cannot fix them.

124−- **Atoms**: `@` is any atom, regardless of aura; auras such as `@ud`, `@t`, `@p` and `@da` are specific atom types. An `@ud` value fits where `@` is expected, but an `@` value needs a check to fit `@ud`. A more specific aura also fits an ancestor in its Hoon aura family: `@ud` and `@ux` fit `@u`, and `@tD` fits `@t`. The reverse needs a check. Distinct specific auras remain distinct; sharing an ancestor does not make them unify. Each bare `@` independently accepts any atom: it is not an aura variable. Atoms that must share a type take one capital, as `[lo=A hi=A]`, with the atom constraint inferred from the body. `add` takes `[A A]` and returns `A`, with `A` constrained to atoms, so `(add n 1)` with `n=@ud` is a `@ud`. Arithmetic rejects loobean operands: `?` contains only 0 and 1, while an arithmetic result need not. Comparison may take loobeans and returns `?`.

125+- **Atoms**: `@` is any atom, regardless of aura; auras such as `@ud`, `@t`, `@p` and `@da` are specific atom types. An `@ud` value fits where `@` is expected, but an `@` value needs a check to fit `@ud`. A more specific aura also fits an ancestor in its Hoon aura family: `@ud` and `@ux` fit `@u`, and `@tD` fits `@t`. The reverse needs a check. Distinct specific auras remain distinct; sharing an ancestor does not make them unify. Each bare `@` independently accepts any atom: it is not an aura variable. Atoms that must share a type take one type variable, as `[lo=A hi=A]`, with the atom constraint inferred from the body. `add` takes `[A A]` and returns `A`, with `A` constrained to atoms, so `(add n 1)` with `n=@ud` is a `@ud`. Arithmetic rejects loobean operands: `?` contains only 0 and 1, while an arithmetic result need not. Comparison may take loobeans and returns `?`.

125- **Constants**: `%add`, `~` and the loobeans have one value each.

126- **Constants**: `%add`, `~` and the loobeans have one value each.

126- **Records and tuples**: `[text=@t done=?]`, `[@t ?]`. An empty `[]` is an error. Duplicate field names in a record are an error. Faces are part of the type, so `[a=@ b=@]` and `[x=@ y=@]` don't unify. An unnamed position can unify with a faced position and take its face, so `[0 0]` fits `[x=@ud y=@ud]`; two different faces don't unify. The explicit type-directed operation `(proj record)` selects fields from its argument according to the expected result type: `^- [x=@ud y=@ud] (proj wider)`, or `(f (proj wider))` when `f` expects that record. The source is evaluated once, and the result contains exactly the fields in the expected layout. No projection is inserted for a direct call. `proj` is reserved: a module cannot define or import another name `proj`. A record too long for one line can leave its `[` open, with one field per deeper line, as an expression's bracket does.

127- **Records and tuples**: `[text=@t done=?]`, `[@t ?]`. An empty `[]` is an error. Duplicate field names in a record are an error. Faces are part of the type, so `[a=@ b=@]` and `[x=@ y=@]` don't unify. An unnamed position can unify with a faced position and take its face, so `[0 0]` fits `[x=@ud y=@ud]`; two different faces don't unify. The explicit type-directed operation `(proj record)` selects fields from its argument according to the expected result type: `^- [x=@ud y=@ud] (proj wider)`, or `(f (proj wider))` when `f` expects that record. The source is evaluated once, and the result contains exactly the fields in the expected layout. No projection is inserted for a direct call. `proj` is reserved: a module cannot define or import another name `proj`. A record too long for one line can leave its `[` open, with one field per deeper line, as an expression's bracket does.

127- **Unions**: a `+$` with several cases below it. Every union written in Jibb has a name, so one used in a field, a sample, a cast, a gate's mold or an argument gets its own `+$`; only imports bring in unions without one. Tags take their union from context, as Tag resolution describes. Cases must differ as nouns: inhabited cases must differ at some position of their right-nested cells, where one is an atom and the other a cell, or both are different constants. `*`, type variables and molds that can be either, such as `(list A)`, can overlap atoms and cells. `?` counts as the two atoms `%.y` and `%.n`: it is disjoint from cells and overlaps the constants 0 and 1. The empty mold `!!` is disjoint from every case; a cell with an empty position at any depth is itself empty and is also disjoint from every case. A union whose cases don't all differ is rejected.

128- **Unions**: a `+$` with several cases below it. Every union written in Jibb has a name, so one used in a field, a sample, a cast, a gate's mold or an argument gets its own `+$`; only imports bring in unions without one. Tags take their union from context, as Tag resolution describes. Cases must differ as nouns: inhabited cases must differ at some position of their right-nested cells, where one is an atom and the other a cell, or both are different constants. `*`, type variables and molds that can be either, such as `(list A)`, can overlap atoms and cells. `?` counts as the two atoms `%.y` and `%.n`: it is disjoint from cells and overlaps the constants 0 and 1. The empty mold `!!` is disjoint from every case; a cell with an empty position at any depth is itself empty and is also disjoint from every case. A union whose cases don't all differ is rejected.

128- **Containers**: `(list A)`, `(unit A)`, `(set A)`, `(map K V)`, `(mop K V)`, `(qeu A)`, `(jar K V)`, `(jug K V)`.

129- **Containers**: `(list A)`, `(unit A)`, `(set A)`, `(map K V)`, `(mop K V)`, `(qeu A)`, `(jar K V)`, `(jug K V)`.

129−- **Gates**: `$-(A B)`. Type variables are capitals, generalized per `++`. A capital in a local `++` shares the enclosing `++`'s variable of the same name if the enclosing `++` also uses it; otherwise the local `++` introduces and generalizes its own variable. For example, `++ inner |= y=A y` uses the enclosing `A` when its enclosing gate has a sample `x=A`; if the enclosing `++` does not use `A`, `inner` generalizes its own `A`. Use another capital for a different type. A body can't force two distinct capitals to be equal; use the same capital wherever a type must be shared. A type variable used where an atom is required gains an atom constraint, so `++ clamp |= [lo=A hi=A n=A]`, whose body calls `gth` and `max`, works on any one aura. It can become nothing more specific: a body that makes `A` a `@ud` or a list is an error.

130+- **Gates**: `$-(A B)`. Type variables are capitalized names, as `A` or `Msg`, generalized per `++`. A capital in a local `++` shares the enclosing `++`'s variable of the same name if the enclosing `++` also uses it; otherwise the local `++` introduces and generalizes its own variable. For example, `++ inner |= y=A y` uses the enclosing `A` when its enclosing gate has a sample `x=A`; if the enclosing `++` does not use `A`, `inner` generalizes its own `A`. Use another capital for a different type. A body can't force two distinct capitals to be equal; use the same capital wherever a type must be shared. A type variable used where an atom is required gains an atom constraint, so `++ clamp |= [lo=A hi=A n=A]`, whose body calls `gth` and `max`, works on any one aura. It can become nothing more specific: a body that makes `A` a `@ud` or a list is an error.

131+- **Printed types** show a type variable by the name it was written with: `++ id |= x=Msg x` prints `$-(Msg Msg)`. A variable from a gate a `++` uses keeps that gate's name, so `++ make program` keeps `program`'s `Data`, `Model` and `Msg`. When several named variables become one, a capital written in the `++` names it; otherwise the one made first does, and a called gate's variables are made before its arguments', so `(cork same same)` prints `$-(A A)`, from `cork`'s `A`. A variable with no name prints as a letter that no other variable in the same type uses: `++ h |= x=A [x same]` prints `$-(A [A $-(B B)])`.

130- **Paths**: `/todos` is constant, `/` empty, and `/todo/[id=@ud]` typed by aura. A typed segment may use `_` for an inferred aura; it still must resolve to an aura that the path rules can print and parse. `%/blog/(slug)` is an `qath`, checked against routes and static files.

132- **Paths**: `/todos` is constant, `/` empty, and `/todo/[id=@ud]` typed by aura. A typed segment may use `_` for an inferred aura; it still must resolve to an aura that the path rules can print and parse. `%/blog/(slug)` is an `qath`, checked against routes and static files.

131- **Generic molds**: `+$ result |$ [V E]` with cases below; `|$` goes only right after a `+$`'s name.

133- **Generic molds**: `+$ result |$ [V E]` with cases below; `|$` goes only right after a `+$`'s name.

132−- **Noun**: `*`, not a type variable; use a capital for a generic type. A value already known to have a more specific noun type, such as `@ud`, can be used where `*` is expected. **Empty**: `!!`.

134+- **Noun**: `*`, not a type variable; use a type variable for a generic type. A value already known to have a more specific noun type, such as `@ud`, can be used where `*` is expected. **Empty**: `!!`.

133- **Pokes**: `raw-poke` is defined in the source-backed private internal prelude module and re-exported by the public prelude as an ordinary transparent type. Ordinary modules can construct and inspect its values; derived `poke` helpers return commands.

135- **Pokes**: `raw-poke` is defined in the source-backed private internal prelude module and re-exported by the public prelude as an ordinary transparent type. Ordinary modules can construct and inspect its values; derived `poke` helpers return commands.

134- **Effect and application-path types**: `raw-poke`, `ask` and `qath` are transparent types, defined in the internal prelude and re-exported normally; callers can construct and inspect their values. Derived gates and `pure` also construct requests, and application-path literals have type `qath`. `(facts full diff …)` appears only in an API file's `paths`.

136- **Effect and application-path types**: `raw-poke`, `ask` and `qath` are transparent types, defined in the internal prelude and re-exported normally; callers can construct and inspect their values. Derived gates and `pure` also construct requests, and application-path literals have type `qath`. `(facts full diff …)` appears only in an API file's `paths`.

135- **Identity**: recursive molds go by name and module.

137- **Identity**: recursive molds go by name and module.

@@ -289,7 +291,7 @@ pathlit = "/" knot { "/" knot } ;

289term = "%" name | "%" decimal | "%&" | "%|" | "%$" ;

291term = "%" name | "%" decimal | "%&" | "%|" | "%$" ;

290loobean = "%.y" | "%.n" ;

292loobean = "%.y" | "%.n" ;

291aura = "@" { lower } [ upper ] ;

293aura = "@" { lower } [ upper ] ;

292−typevar = upper ;

294+typevar = upper { lower | digit } ;

293name = lower { lower | digit | "-" } ;

295name = lower { lower | digit | "-" } ;

294knot = { lower | digit | "-" | "." | "~" | "_" } ;

296knot = { lower | digit | "-" | "." | "~" | "_" } ;

295```

297```

jibb-dev/lib/jibb.hoon+215−45

@@ -206,9 +206,11 @@

206:: token holds the text after @. An aura starting @s or

207:: @r is an error at 2nd: "signed and floating-point

208:: auras are left out of Jibb"

209−:: A-Z type variable: one capital. A letter or digit right

209+:: A-Z type variable [A-Z][a-z0-9]*: a capital, then

210+:: lowercase letters and digits, as M, Msg or T2. Right

211+:: after it, which is emitted first, a capital, _ or -

210−:: after it is an error there, "a type variable is one

212+:: is an error there, "a type variable is a capital,

211−:: capital letter", after the type variable's token

213+:: then lowercase letters and digits"

212:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names

214:: a-z name [a-z][a-z0-9-]*, or a wing: two or more names

213:: joined by dots. Right after the name or wing, which

215:: joined by dots. Right after the name or wing, which

214:: is emitted first, a capital or _ is an error there,

216:: is emitted first, a capital or _ is an error there,

@@ -1360,10 +1362,10 @@

1360 =? n &(?=(^ rest) (is-upper i.rest)) +(n)

1362 =? n &(?=(^ rest) (is-upper i.rest)) +(n)

1361 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])

1363 (emit +(n) [%aura (@ta (crip (scag n t.cs)))])

1362 ?: (is-upper a)

1364 ?: (is-upper a)

1365+ =/ n=@ud (run-len t.cs tvar-mask)

1363− => (emit 1 [%tvar a])

1366+ => (emit +(n) [%tvar (crip [a (scag n t.cs)])])

1364− ?. &(?=(^ cs) |((is-lower i.cs) (is-upper i.cs) (is-digit i.cs)))

1367+ ?. &(?=(^ cs) |((is-upper i.cs) =('_' i.cs) =('-' i.cs))) cor

1365− cor

1366− (err col "a type variable is one capital letter")

1368+ (err col "a type variable is a capital, then lowercase letters and digits")

1367 ?: =(':' a)

1369 ?: =(':' a)

1368 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")

1370 ?. =(0 dep) (err col "a comment can't start inside `\{…}`")

1369 ?: =(':' b) comment

1371 ?: =(':' b) comment

@@ -1667,6 +1669,7 @@

1667++ digit-mask 0x3ff.0000.0000.0000 :: 0-9

1669++ digit-mask 0x3ff.0000.0000.0000 :: 0-9

1668++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f

1670++ hex-mask 0x7e.0000.0000.03ff.0000.0000.0000 :: 0-9 a-f

1669++ name-mask 0x7ff.fffe.0000.0000.03ff.2000.0000.0000 :: a-z 0-9 -

1671++ name-mask 0x7ff.fffe.0000.0000.03ff.2000.0000.0000 :: a-z 0-9 -

1672+++ tvar-mask 0x7ff.fffe.0000.0000.03ff.0000.0000.0000 :: a-z 0-9

1670++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _

1673++ knot-mask 0x47ff.fffe.8000.0000.03ff.6000.0000.0000 :: and . ~ _

1671++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .

1674++ number-mask 0x7ff.fffe.07ff.fffe.03ff.4000.0000.0000 :: a-z A-Z 0-9 .

1672++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2

1675++ bad-mask 0x8000.0000.0000.0000.0000.0000.ffff.fbff :: 2.2

@@ -6395,15 +6398,67 @@

6395 ^- ?

6398 ^- ?

6396 (itype-var-is-gate-free-fuel n t 256)

6399 (itype-var-is-gate-free-fuel n t 256)

6397::

6400::

6401+:: +named-var: the ID of the nth type variable, written as name

6402+::

6403+:: An ID counts in its low 64 bits. The name a variable was written

6404+:: with, as Msg, sits above them, or 0 for none, so the name travels

6405+:: with the variable through substitution, generalization and

6406+:: instantiation, and the printer can show it (+show-var). No two

6407+:: IDs share a count, so a name never makes two variables one.

6408+::

6409+++ named-var

6410+ |= [name=@t n=@ud]

6411+ ^- @ud

6412+ (add (lsh 6 name) (end 6 n))

6413+::

6414+:: +var-name: the name in a type variable's ID, or 0 for none

6415+::

6416+++ var-name

6417+ |= id=@ud

6418+ ^- @t

6419+ (rsh 6 id)

6420+::

6421+:: +var-count: a type variable's ID without its name

6422+::

6423+++ var-count

6424+ |= id=@ud

6425+ ^- @ud

6426+ (end 6 id)

6427+::

6428+:: +canonical-itype: t with the variables in vars renumbered to print

6429+::

6430+:: A variable keeps its name unless one before it in vars has the same

6431+:: name. The others take numbers from 0, skipping any whose letter

6432+:: (+show-var) is a name in vars, so a printed type never shows one

6433+:: name for two variables.

6434+::

6398++ canonical-itype

6435++ canonical-itype

6399 |= [t=itype vars=(list @ud)]

6436 |= [t=itype vars=(list @ud)]

6400 ^- itype

6437 ^- itype

6438+ =/ names=(list @t) (turn vars var-name)

6439+ =/ used=(list @t) ~

6401 =/ ren=isub ~

6440 =/ ren=isub ~

6402 =/ n=@ud 0

6441 =/ n=@ud 0

6403 |-

6442 |-

6404 ?~ vars (itype-rename t ren)

6443 ?~ vars (itype-rename t ren)

6444+ =/ name=@t (var-name i.vars)

6445+ =/ own=? &(!=(0 name) !(lien used |=(u=@t =(u name))))

6446+ =? n !own (letter-free n names)

6447+ =/ id=@ud ?:(own (named-var name 0) n)

6405− =/ 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])))

6448+ =/ 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])))

6406− $(vars t.vars, ren [[i.vars replacement] ren], n +(n))

6449+ $(vars t.vars, ren [[i.vars replacement] ren], n ?:(own n +(n)), used ?:(own [name used] used))

6450+::

6451+:: +letter-free: the first number from n whose letter is none of names

6452+::

6453+++ letter-free

6454+ |= [n=@ud names=(list @t)]

6455+ ^- @ud

6456+ ?. (lien names |=(m=@t =(m (crip (show-var n))))) n

6457+ $(n +(n))

6458+::

6459+:: +instantiate-scheme: a scheme's type with fresh quantified variables

6460+::

6461+:: Each fresh variable keeps the name of the one it replaces.

6407::

6462::

6408++ instantiate-scheme

6463++ instantiate-scheme

6409 |= [scheme=ischeme state=istate]

6464 |= [scheme=ischeme state=istate]

@@ -6412,12 +6467,13 @@

6412 =/ vars=(list @ud) vars.scheme

6467 =/ vars=(list @ud) vars.scheme

6413 |-

6468 |-

6414 ?~ vars [(itype-rename typ.scheme ren) state]

6469 ?~ vars [(itype-rename typ.scheme ren) state]

6470+ =/ fresh=@ud (named-var (var-name i.vars) next.state)

6415 =/ replacement=itype

6471 =/ replacement=itype

6416− ?:((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])))

6472+ ?:((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])))

6417 :: A generalized atom variable is a valid origin for re-generalizing

6473 :: A generalized atom variable is a valid origin for re-generalizing

6418 :: an alias, just as a sample binder is.

6474 :: an alias, just as a sample binder is.

6419 =/ st=istate state(next +(next.state))

6475 =/ st=istate state(next +(next.state))

6420− =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [next.state binders.state]

6476+ =? binders.st |(?=(%fvar -.replacement) ?=(%avar -.replacement) ?=(%rvar -.replacement)) [fresh binders.state]

6421 $(vars t.vars, ren [[i.vars replacement] ren], state st)

6477 $(vars t.vars, ren [[i.vars replacement] ren], state st)

6422::

6478::

6423++ icap-lookup

6479++ icap-lookup

@@ -7277,7 +7333,8 @@

7277 ?: in-mold.state ~

7333 ?: in-mold.state ~

7278 =/ n=(unit @ud) (icap-lookup name.sh caps.state)

7334 =/ n=(unit @ud) (icap-lookup name.sh caps.state)

7279 ?^ n `[[%var u.n] state]

7335 ?^ n `[[%var u.n] state]

7336+ =/ id=@ud (named-var name.sh next.state)

7280− `[[%var next.state] state(next +(next.state), caps [[name.sh next.state at.sh] caps.state])]

7337+ `[[%var id] state(next +(next.state), caps [[name.sh id at.sh] caps.state])]

7281 * ~

7338 * ~

7282 ==

7339 ==

7283::

7340::

@@ -7557,7 +7614,8 @@

7557 ^- istate

7614 ^- istate

7558 ?~ sites state

7615 ?~ sites state

7559 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)

7616 ?: ?=(^ (icap-lookup name.i.sites caps.state)) $(sites t.sites)

7617+ =/ id=@ud (named-var name.i.sites next.state)

7560− $(sites t.sites, state state(next +(next.state), caps [[name.i.sites next.state at.i.sites] caps.state]))

7618+ $(sites t.sites, state state(next +(next.state), caps [[name.i.sites id at.i.sites] caps.state]))

7561::

7619::

7562++ reserve-def-caps

7620++ reserve-def-caps

7563 |= [e=expr state=istate]

7621 |= [e=expr state=istate]

@@ -7731,7 +7789,8 @@

7731 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))

7789 (weld (free-env-vars env sub.state.p.inferred) (free-cap-vars caps.state sub.state.p.inferred))

7732 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

7790 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

7733 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))

7791 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))

7792+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.inferred sub.state.p.inferred)

7734− $(ds t.ds, env [[name.d [typ vars]] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)

7793+ $(ds t.ds, env [[name.d named] env], state state.p.inferred(caps caps.state, holes holes.state), progressed &)

7735::

7794::

7736:: Try complete cyclic local groups after individual definitions stall.

7795:: Try complete cyclic local groups after individual definitions stall.

7737:: Components with non-gates or unresolved constraints stay unavailable.

7796:: Components with non-gates or unresolved constraints stay unavailable.

@@ -10337,24 +10396,12 @@

10337 ^- tape

10396 ^- tape

10338 =. t (itype-walk t sub)

10397 =. t (itype-walk t sub)

10339 ?- -.t

10398 ?- -.t

10340− %var

10399+ %var (show-var id.t)

10341− ?: (lth id.t 26) [(add 65 id.t) ~]

10342− "T{<id.t>}"

10343− %fvar

10400+ %fvar (show-var id.t)

10344− ?: (lth id.t 26) [(add 65 id.t) ~]

10345− "T{<id.t>}"

10346− %avar

10401+ %avar (show-var id.t)

10347− ?: (lth id.t 26) [(add 65 id.t) ~]

10348− "T{<id.t>}"

10349− %rvar

10402+ %rvar (show-var id.t)

10350− ?: (lth id.t 26) [(add 65 id.t) ~]

10351− "T{<id.t>}"

10352− %nvar

10403+ %nvar (show-var id.t)

10353− ?: (lth id.t 26) [(add 65 id.t) ~]

10354− "T{<id.t>}"

10355− %rnvar

10404+ %rnvar (show-var id.t)

10356− ?: (lth id.t 26) [(add 65 id.t) ~]

10357− "T{<id.t>}"

10358 %atom "@{(trip aura.t)}"

10405 %atom "@{(trip aura.t)}"

10359 %any-atom "@"

10406 %any-atom "@"

10360 %flag "?"

10407 %flag "?"

@@ -10375,6 +10422,17 @@

10375 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"

10422 %cell "[{(show-itype-item hed.t sub)} {(show-itype-item tal.t sub)}]"

10376 ==

10423 ==

10377::

10424::

10425+:: +show-var: a type variable as printed: its name if it has one, else

10426+:: a letter for its number, A to Z, then T26, T27 and on

10427+::

10428+++ show-var

10429+ |= id=@ud

10430+ ^- tape

10431+ =/ name=@t (var-name id)

10432+ ?. =(0 name) (trip name)

10433+ ?: (lth id 26) [(add 65 id) ~]

10434+ "T{<id>}"

10435+::

10378++ show-itype-item

10436++ show-itype-item

10379 |= [t=itype sub=isub]

10437 |= [t=itype sub=isub]

10380 ^- tape

10438 ^- tape

@@ -10433,7 +10491,7 @@

10433 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label

10491 ?: |(?=(%var -.normalized) ?=(%fvar -.normalized) ?=(%avar -.normalized) ?=(%rvar -.normalized) (itype-has-nvar normalized) (itype-has-tag normalized) (itype-has-union normalized)) label

10434 ?: (itype-has-hidden-recursive normalized) label

10492 ?: (itype-has-hidden-recursive normalized) label

10435 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))

10493 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))

10436− =/ printable=itype (canonical-itype normalized vars)

10494+ =/ printable=itype (canonical-itype (cap-names normalized vars ~ sub))

10437 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"

10495 "{label} has type {(show-itype printable ~)}{(show-atom-constraint printable)}"

10438::

10496::

10439:: A capital in a written mold is generalized with its enclosing ++.

10497:: A capital in a written mold is generalized with its enclosing ++.

@@ -10474,6 +10532,116 @@

10474 ?: =(n u.ident) `i.caps

10532 ?: =(n u.ident) `i.caps

10475 $(caps t.caps)

10533 $(caps t.caps)

10476::

10534::

10535+:: +cap-names: give each variable in vars the name it was written with

10536+::

10537+:: Unification joins variables, and the one an ID resolves to may not

10538+:: carry the name its definition wrote, as when a capital meets a

10539+:: called gate's variable or an atom variable. Each variable in vars

10540+:: takes the name of the first capital in caps that resolves to it;

10541+:: failing that, of the earliest made of the named variables that

10542+:: resolve to it, itself included (+joined-names). Only the name part

10543+:: of an ID changes, not its count, so IDs stay distinct.

10544+::

10545+++ cap-names

10546+ |= [typ=itype vars=(list @ud) caps=icaps sub=isub]

10547+ ^- [typ=itype vars=(list @ud)]

10548+ =/ written=icaps (flop caps)

10549+ =/ joined=(map @ud @ud) (joined-names sub)

10550+ =/ ren=(map @ud @ud) ~

10551+ =/ out=(list @ud) ~

10552+ |-

10553+ ?~ vars [?~(ren typ (itype-reid typ ren)) (flop out)]

10554+ =/ cap=(unit icap) (cap-with-id i.vars written sub)

10555+ =/ first=(unit @ud) (~(get by joined) i.vars)

10556+ =/ name=@t

10557+ ?^ cap name.u.cap

10558+ ?~ first (var-name i.vars)

10559+ ?: =(0 (var-name i.vars)) (var-name u.first)

10560+ ?: (lth (var-count u.first) (var-count i.vars)) (var-name u.first)

10561+ (var-name i.vars)

10562+ =/ to=@ud (named-var name i.vars)

10563+ ?: =(to i.vars) $(vars t.vars, out [i.vars out])

10564+ $(vars t.vars, out [to out], ren (~(put by ren) i.vars to))

10565+::

10566+:: +joined-names: for each variable that named ones resolve to, the

10567+:: earliest made of those, by count

10568+::

10569+:: One pass over sub keeps each ID's newest binding, as +itype-lookup

10570+:: would find it: the variable it is bound to, or ~ for another type.

10571+:: Each named ID then follows those bindings to the variable it

10572+:: resolves to, if any.

10573+::

10574+++ joined-names

10575+ |= sub=isub

10576+ ^- (map @ud @ud)

10577+ =/ edges=(map @ud (unit @ud))

10578+ %+ roll (flop sub)

10579+ |= [b=ibinding m=(map @ud (unit @ud))]

10580+ (~(put by m) id.b (var-of val.b))

10581+ =/ named=(list @ud)

10582+ (murn ~(tap by edges) |=([k=@ud *] ?:(=(0 (var-name k)) ~ `k)))

10583+ =/ fuel=@ud ~(wyt by edges)

10584+ =/ out=(map @ud @ud) ~

10585+ |-

10586+ ?~ named out

10587+ =/ root=(unit @ud) (follow-var i.named edges fuel)

10588+ ?~ root $(named t.named)

10589+ ?: =(u.root i.named) $(named t.named)

10590+ =/ best=(unit @ud) (~(get by out) u.root)

10591+ ?: &(?=(^ best) (lth (var-count u.best) (var-count i.named)))

10592+ $(named t.named)

10593+ $(named t.named, out (~(put by out) u.root i.named))

10594+::

10595+:: +follow-var: the variable that id resolves to through edges, or ~ if

10596+:: it resolves to another type; fuel bounds the steps

10597+::

10598+++ follow-var

10599+ |= [id=@ud edges=(map @ud (unit @ud)) fuel=@ud]

10600+ ^- (unit @ud)

10601+ |-

10602+ ?: =(0 fuel) ~

10603+ =/ edge=(unit (unit @ud)) (~(get by edges) id)

10604+ ?~ edge `id

10605+ ?~ u.edge ~

10606+ ?: =(u.u.edge id) `id

10607+ $(id u.u.edge, fuel (dec fuel))

10608+::

10609+:: +var-of: the ID of a type variable node, or ~ for another type

10610+::

10611+++ var-of

10612+ |= t=itype

10613+ ^- (unit @ud)

10614+ ?+ -.t ~

10615+ %var `id.t

10616+ %fvar `id.t

10617+ %avar `id.t

10618+ %rvar `id.t

10619+ %nvar `id.t

10620+ %rnvar `id.t

10621+ ==

10622+::

10623+:: +itype-reid: t with the variable IDs in ids replaced, each node

10624+:: keeping its kind

10625+::

10626+++ itype-reid

10627+ |= [t=itype ids=(map @ud @ud)]

10628+ ^- itype

10629+ ?- -.t

10630+ %var t(id (fall (~(get by ids) id.t) id.t))

10631+ %fvar t(id (fall (~(get by ids) id.t) id.t))

10632+ %avar t(id (fall (~(get by ids) id.t) id.t))

10633+ %rvar t(id (fall (~(get by ids) id.t) id.t))

10634+ %nvar t(id (fall (~(get by ids) id.t) id.t))

10635+ %rnvar t(id (fall (~(get by ids) id.t) id.t))

10636+ ?(%atom %any-atom %flag %noun %empty %tag %const %recursive %jrec) t

10637+ %union t(cases (turn cases.t |=(c=itype ^$(t c))), args (turn args.t |=(c=itype ^$(t c))))

10638+ %grec t(args (turn args.t |=(c=itype ^$(t c))))

10639+ %collection t(args (turn args.t |=(c=itype ^$(t c))))

10640+ %face t(body $(t body.t))

10641+ %fn t(sample $(t sample.t), product $(t product.t))

10642+ %cell t(hed $(t hed.t), tal $(t tal.t))

10643+ ==

10644+::

10477++ merged-capitals

10645++ merged-capitals

10478 |= [caps=icaps sub=isub]

10646 |= [caps=icaps sub=isub]

10479 ^- (unit [first=icap second=icap])

10647 ^- (unit [first=icap second=icap])

@@ -10909,7 +11077,7 @@

10909 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))

11077 =. vars (skim vars |=(n=@ud !(lien free |=(f=@ud =(f n)))))

10910 =/ rest=(each ienv idiag) $(entries t.entries)

11078 =/ rest=(each ienv idiag) $(entries t.entries)

10911 ?: ?=(%| -.rest) rest

11079 ?: ?=(%| -.rest) rest

10912− [%& [[name.entry [typ vars]] p.rest]]

11080+ [%& [[name.entry (cap-names typ vars caps.entry sub.state)] p.rest]]

10913::

11081::

10914++ infer-gate-group

11082++ infer-gate-group

10915 |= [ds=(list def) env=ienv state=istate]

11083 |= [ds=(list def) env=ienv state=istate]

@@ -11091,7 +11259,7 @@

11091 =? artifacts ?=(^ u.finalized)

11259 =? artifacts ?=(^ u.finalized)

11092 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]

11260 [[name.d val.d typ sub.state.p.result (flop u.finalized)] artifacts]

11093 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)

11261 =? checked |(?=(%gate -.val.d) ?=(%gate-wide -.val.d)) (~(put by checked) name.d d)

11094− `[[[name.d [typ vars]] env] checked artifacts]

11262+ `[[[name.d (cap-names typ vars caps.state.p.result sub.state.p.result)] env] checked artifacts]

11095++ add-supported-defs-core

11263++ add-supported-defs-core

11096 |= [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)])]

11264 |= [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)])]

11097 ^- [env=ienv artifacts=(list iwidth-definition)]

11265 ^- [env=ienv artifacts=(list iwidth-definition)]

@@ -15562,7 +15730,8 @@

15562 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

15730 =/ vars=(list @ud) (unique-type-vars (itype-vars typ))

15563 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)

15731 ?~ (width-finalize projections.state.p.result sub.state.p.result vars)

15564 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])

15732 $(ds t.ds, lines [(crip "++ {(trip name.d)}: record projection elaboration needs unsupported inference") lines])

15733+ =/ named=[typ=itype vars=(list @ud)] (cap-names typ vars caps.state.p.result sub.state.p.result)

15565− =/ printable=itype (canonical-itype typ vars)

15734+ =/ printable=itype (canonical-itype named)

15566 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")

15735 =/ line=@t (crip "++ {(trip name.d)}: {(show-itype printable ~)}{(show-atom-constraint printable)}")

15567 $(ds t.ds, lines [line lines])

15736 $(ds t.ds, lines [line lines])

15568:: Experimental module-owned pending-constraint generalization only.

15737:: Experimental module-owned pending-constraint generalization only.

@@ -15659,7 +15828,7 @@

15659 =/ normalized=itype (itype-normalize typ sub.state)

15828 =/ normalized=itype (itype-normalize typ sub.state)

15660 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))

15829 =/ vars=(list @ud) (unique-type-vars (itype-vars normalized))

15661 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))

15830 =/ quantified=(list @ud) (skim vars |=(n=@ud !(lien ids.u.tagged |=(b=@ud =(b n)))))

15662− `[[normalized quantified]]

15831+ `(cap-names normalized quantified caps.state sub.state)

15663::

15832::

15664+$ dgcommit [env=ienv state=istate]

15833+$ dgcommit [env=ienv state=istate]

15665:: A branch literal must not acquire a value face through replay.

15834:: A branch literal must not acquire a value face through replay.

@@ -16092,20 +16261,21 @@

16092 ?~ env `+(top)

16261 ?~ env `+(top)

16093 =/ sc=ischeme scheme.i.env

16262 =/ sc=ischeme scheme.i.env

16094 ?: (itype-has-tag typ.sc) ~

16263 ?: (itype-has-tag typ.sc) ~

16095− $(env t.env, top (itype-max-id typ.sc (max top (roll vars.sc max))))

16264+ $(env t.env, top (itype-max-id typ.sc (max top (roll (turn vars.sc var-count) max))))

16096::

16265::

16097−:: +itype-max-id: the largest variable or tag ID in t, or top

16266+:: +itype-max-id: the largest variable or tag ID in t, or top, without

16267+:: the variables' names (+named-var)

16098::

16268::

16099++ itype-max-id

16269++ itype-max-id

16100 |= [t=itype top=@ud]

16270 |= [t=itype top=@ud]

16101 ^- @ud

16271 ^- @ud

16102 ?- -.t

16272 ?- -.t

16103− %var (max top id.t)

16273+ %var (max top (var-count id.t))

16104− %fvar (max top id.t)

16274+ %fvar (max top (var-count id.t))

16105− %avar (max top id.t)

16275+ %avar (max top (var-count id.t))

16106− %rvar (max top id.t)

16276+ %rvar (max top (var-count id.t))

16107− %nvar (max top id.t)

16277+ %nvar (max top (var-count id.t))

16108− %rnvar (max top id.t)

16278+ %rnvar (max top (var-count id.t))

16109 %tag (max top id.t)

16279 %tag (max top id.t)

16110 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top

16280 ?(%atom %any-atom %flag %noun %empty %const %recursive %jrec) top

16111 %collection (itype-max-ids args.t top)

16281 %collection (itype-max-ids args.t top)

jibb-dev/lib/jibb/prelude.jibb+12−9

@@ -528,20 +528,23 @@

528 font=(unit qath)

529 dark=(unit [tones=[normal=@t background=@t accent=@t danger=@t muted=@t]])

530

531−+$ program |$ [D X M]

531++$ program |$ [Data Model Msg]

532− [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]

532+ [ init=$-(Data Model)

533+ update=$-([Msg Model] [Model (list (cmd Msg))])

534+ view=$-(Model (element Msg))

535+ subs=$-(Model (list (sub Msg)))

533

536

534−++ program |= [init=$-(D X) update=$-([M X] [X (list (cmd M))]) view=$-(X (element M)) subs=$-(X (list (sub M)))]

537+++ program |= [init=$-(Data Model) update=$-([Msg Model] [Model (list (cmd Msg))]) view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]

535− ^- (program D X M) [init update view subs]

538+ ^- (program Data Model Msg) [init update view subs]

536

539

537−++ island |= [p=(program D X M) data=D]

540+++ island |= [p=(program Data Model Msg) data=Data]

538 ^- (element !!) [%island [p data]]

541 ^- (element !!) [%island [p data]]

539

542

540−+$ page |$ [R D]

543++$ page |$ [Params Data]

541− [load=$-(R (ask D)) view=$-(D (element !!))]

544+ [load=$-(Params (ask Data)) view=$-(Data (element !!))]

542

545

543−++ page |= [load=$-(R (ask D)) view=$-(D (element !!))]

546+++ page |= [load=$-(Params (ask Data)) view=$-(Data (element !!))]

544− ^- (page R D) [load view]

547+ ^- (page Params Data) [load view]

545

548

546+$ store |$ [S] [init=S update=*]

549+$ store |$ [S] [init=S update=*]

547

550

tests/golden/doc-grammar-02-buttons/types.txt+1−1

@@ -1,4 +1,4 @@

1partial inference; module not checked

2++ add-button: tag needs context in partial inference

3−++ labelled: $-([label=@t msg=A] (element A))

3+++ labelled: $-([label=@t msg=M] (element M))

4++ wide: (list attr)

tests/golden/lex-name-bad-5/tokens.txt+4−3

@@ -1,3 +1,4 @@

1−/tests/golden/lex-name-bad-5/source.jibb:1:5: a type variable is one capital letter

1+1:1 glyph ++

2−++ Foo 1

2+1:4 tvar Foo

3− ^

3+1:8 lit 1

4+1:9 NEWLINE

tests/golden/lex-name-bad-5/tree.txt+1−1

@@ -1,3 +1,3 @@

1−/tests/golden/lex-name-bad-5/source.jibb:1:4: expected a name, found `F`; a name starts with a lowercase letter

1+/tests/golden/lex-name-bad-5/source.jibb:1:4: expected a name, found `Foo`; a name starts with a lowercase letter

2++ Foo 1

3 ^

tests/golden/lex-typevar-bad-1/about.txtnew file+3

@@ -0,0 +1,3 @@

1+source: Grammar tab, Lexical rules: "Type variables: a capital, then lowercase letters and digits"; "`AB`, `MSG`, `Msg_x` and `Msg-x` are errors."

2+tests: a second capital right after a type variable's first

3+expect: error at 1:15 — a type variable is a capital, then lowercase letters and digits

tests/golden/lex-typevar-bad-1/source.jibbnew file+1

@@ -0,0 +1 @@

1+++ pair |= x=AB x

tests/golden/lex-typevar-bad-1/tokens.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-1/source.jibb:1:15: a type variable is a capital, then lowercase letters and digits

2+++ pair |= x=AB x

3+ ^

tests/golden/lex-typevar-bad-1/tree.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-1/source.jibb:1:15: a type variable is a capital, then lowercase letters and digits

2+++ pair |= x=AB x

3+ ^

tests/golden/lex-typevar-bad-2/about.txtnew file+3

@@ -0,0 +1,3 @@

1+source: Grammar tab, Lexical rules: "Type variables: a capital, then lowercase letters and digits"; "`AB`, `MSG`, `Msg_x` and `Msg-x` are errors."

2+tests: a type variable written in capitals only, as an Elm or C habit might write it

3+expect: error at 1:15 — a type variable is a capital, then lowercase letters and digits

tests/golden/lex-typevar-bad-2/source.jibbnew file+1

@@ -0,0 +1 @@

1+++ pass |= m=MSG m

tests/golden/lex-typevar-bad-2/tokens.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-2/source.jibb:1:15: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=MSG m

3+ ^

tests/golden/lex-typevar-bad-2/tree.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-2/source.jibb:1:15: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=MSG m

3+ ^

tests/golden/lex-typevar-bad-3/about.txtnew file+3

@@ -0,0 +1,3 @@

1+source: Grammar tab, Lexical rules: "Type variables: a capital, then lowercase letters and digits"; "`AB`, `MSG`, `Msg_x` and `Msg-x` are errors."

2+tests: an underscore inside a type variable

3+expect: error at 1:17 — a type variable is a capital, then lowercase letters and digits

tests/golden/lex-typevar-bad-3/source.jibbnew file+1

@@ -0,0 +1 @@

1+++ pass |= m=Msg_x m

tests/golden/lex-typevar-bad-3/tokens.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-3/source.jibb:1:17: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=Msg_x m

3+ ^

tests/golden/lex-typevar-bad-3/tree.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-3/source.jibb:1:17: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=Msg_x m

3+ ^

tests/golden/lex-typevar-bad-4/about.txtnew file+3

@@ -0,0 +1,3 @@

1+source: Grammar tab, Lexical rules: "Type variables: a capital, then lowercase letters and digits"; "`AB`, `MSG`, `Msg_x` and `Msg-x` are errors."

2+tests: a hyphen inside a type variable, which a name may hold but a type variable may not

3+expect: error at 1:17 — a type variable is a capital, then lowercase letters and digits

tests/golden/lex-typevar-bad-4/source.jibbnew file+1

@@ -0,0 +1 @@

1+++ pass |= m=Msg-x m

tests/golden/lex-typevar-bad-4/tokens.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-4/source.jibb:1:17: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=Msg-x m

3+ ^

tests/golden/lex-typevar-bad-4/tree.txtnew file+3

@@ -0,0 +1,3 @@

1+/tests/golden/lex-typevar-bad-4/source.jibb:1:17: a type variable is a capital, then lowercase letters and digits

2+++ pass |= m=Msg-x m

3+ ^

tests/golden/lex-typevar-ok-1/about.txtnew file+4

@@ -0,0 +1,4 @@

1+source: Grammar tab, Lexical rules: "Type variables: a capital, then lowercase letters and digits: `A`, `Msg`, `T2`."

2+tests: type variables of several letters and with digits, as generic parameters and in molds, beside a one-letter one; the printed type keeps each written name

3+expect: parses

4+expect-types: swap prints $-([key=Msg value=T2] [T2 Msg]) and same-one $-(A A)

tests/golden/lex-typevar-ok-1/source.jibbnew file+3

@@ -0,0 +1,3 @@

1++$ entry |$ [Key Value2] [key=Key value=Value2]

2+++ swap |= p=(entry Msg T2) [value.p key.p]

3+++ same-one |= x=A x

tests/golden/lex-typevar-ok-1/tokens.txtnew file+39

@@ -0,0 +1,39 @@

1+1:1 glyph +$

2+1:4 name entry

3+1:10 glyph |$

4+1:13 glyph [

5+1:14 tight tvar Key

6+1:18 tvar Value2

7+1:24 tight glyph ]

8+1:26 glyph [

9+1:27 tight name key

10+1:30 tight glyph =

11+1:31 tight tvar Key

12+1:35 name value

13+1:40 tight glyph =

14+1:41 tight tvar Value2

15+1:47 tight glyph ]

16+2:1 NEWLINE

17+2:1 glyph ++

18+2:4 name swap

19+2:9 glyph |=

20+2:12 name p

21+2:13 tight glyph =

22+2:14 tight glyph (

23+2:15 tight name entry

24+2:21 tvar Msg

25+2:25 tvar T2

26+2:27 tight glyph )

27+2:29 glyph [

28+2:30 tight wing value.p

29+2:38 wing key.p

30+2:43 tight glyph ]

31+3:1 NEWLINE

32+3:1 glyph ++

33+3:4 name same-one

34+3:13 glyph |=

35+3:16 name x

36+3:17 tight glyph =

37+3:18 tight tvar A

38+3:20 name x

39+3:21 NEWLINE

tests/golden/lex-typevar-ok-1/tree.txtnew file+15

@@ -0,0 +1,15 @@

1+(module

2+ (mold 1:1 entry

3+ (generic 1:10 Key Value2

4+ (cell 1:26

5+ (face 1:27 key (tvar 1:31 Key))

6+ (face 1:35 value (tvar 1:41 Value2)))))

7+ (value 2:1 swap

8+ (gate 2:9

9+ (face 2:12 p

10+ (apply 2:14 entry (tvar 2:21 Msg) (tvar 2:25 T2)))

11+ (tuple 2:29 (wing 2:30 value.p) (wing 2:38 key.p))))

12+ (value 3:1 same-one

13+ (gate 3:13

14+ (face 3:16 x (tvar 3:18 A))

15+ (wing 3:20 x))))

tests/golden/lex-typevar-ok-1/types.txtnew file+4

@@ -0,0 +1,4 @@

1+partial inference; module not checked

2++$ entry: not checked

3+++ swap: $-([key=Msg value=T2] [T2 Msg])

4+++ same-one: $-(A A)

tests/golden/prelude-unit-list-transforms/types.txt+1−1

@@ -64,7 +64,7 @@ partial inference; module not checked

64++ snip: sample mold is not supported by partial inference

65++ rear: sample mold is not supported by partial inference

66++ cork: $-([$-(A B) $-(B C)] $-(A C))

67−++ corl: $-([$-(A B) $-(C A)] $-(C B))

67+++ corl: $-([$-(B C) $-(A B)] $-(A C))

68++ cury: $-([$-([A B] C) A] $-(B C))

69++ curr: $-([$-([A B] C) B] $-(A C))

70+$ cmd: cases proven disjoint; mold not checked

tests/golden/types-constructor-context/types.txt+2−2

@@ -4,8 +4,8 @@ partial inference; module not checked

4+$ wrong-payload: cases proven disjoint; mold not checked

5+$ missing: cases proven disjoint; mold not checked

6+$ maybe: cases proven disjoint; mold not checked

7−++ call: $-($-(@t A) A)

7+++ call: $-($-(@t M) M)

8−++ call-ship: $-($-(@p A) A)

8+++ call-ship: $-($-(@p M) M)

9++ unknown: call constraint is not supported by partial inference

10++ later-context: msg

11++ named-alias: msg

tests/golden/types-generic-union-alias-face/types.txt+1−1

@@ -1,7 +1,7 @@

1partial inference; module not checked

2+$ relay: not checked

3++ make: $-(A (choice.base B A))

4−++ reveal: $-((choice.base A B) (choice.base A B))

4+++ reveal: $-((choice.base B A) (choice.base B A))

5++ with-text: (choice.base @p @t)

6++ with-ship: cast mold and expression type do not unify

7/tests/golden/types-generic-union-alias-face/source.jibb:6:17: cast mold

tests/golden/types-generic-union-alias/types.txt+1−1

@@ -4,7 +4,7 @@ partial inference; module not checked

4+$ repeat: not checked

5+$ extra: not checked

6++ reverse-value: (choice @p @t)

7−++ reverse-gate: $-((choice A B) (choice A B))

7+++ reverse-gate: $-((choice B A) (choice B A))

8++ repeat-gate: $-((choice A A) (choice A A))

9++ repeated-call: distinct type variables `A` and `B` must not be forced equal; use the same capital for a shared type

10/tests/golden/types-generic-union-alias/source.jibb:10:31: first type variable

tests/golden/types-generic-union-local/types.txt+1−1

@@ -11,7 +11,7 @@ partial inference; module not checked

11++ phantom-gate: (phantom $-(@t @p))

12++ identity: $-((choice A B) (choice A B))

13++ repeated: $-((choice A A) (choice A A))

14−++ reverse: $-((choice A B) (choice A B))

14+++ reverse: $-((choice B A) (choice B A))

15++ first: (choice @t @p)

16++ second: (choice @t @p)

17++ third: (choice @p @t)

tests/golden/types-prelude-generic-alias/types.txt+1−1

@@ -5,7 +5,7 @@ partial inference; module not checked

5+$ fixed: not checked

6++ direct: $-((each A B) (each A B))

7++ alias-id: $-((each A B) (each A B))

8−++ reversed: $-((each A B) (each A B))

8+++ reversed: $-((each B A) (each B A))

9++ reversed-concrete: $-((each @p @t) (each @p @t))

10++ repeated-id: $-((each A A) (each A A))

11++ fixed-id: $-((each A @p) (each A @p))

tests/golden/types-prelude-lead-late/types.txt+1−1

@@ -1,7 +1,7 @@

1partial inference; module not checked

2++ text-ship: [@t @p]

3++ ship-text: [@p @t]

4−++ first-fn: $-(A [@t A])

4+++ first-fn: $-(B [@t B])

5++ generic-lead: $-([x=A y=B] [A B])

6++ generic-late: $-([x=A y=B] [B A])

7++ generic-gate: $-([f=$-(A B) x=C] [$-(A B) C])

tests/golden/types-prelude-list-functions/types.txt+1−1

@@ -20,7 +20,7 @@ partial inference; module not checked

20++ turn-nested: (list (list @t))

21++ turn-import: (list @p)

22++ turn-mismatch: call's sample and argument types do not unify

23−/tests/golden/types-prelude-list-functions/source.jibb:18:19: called gate has type $-([(list @t) $-(@t A)] (list A))

23+/tests/golden/types-prelude-list-functions/source.jibb:18:19: called gate has type $-([(list @t) $-(@t B)] (list B))

24++ turn-mismatch (turn ~["a"] |=(x (^- @p x)))

25 ^

26/tests/golden/types-prelude-list-functions/source.jibb:18:31: argument has type $-(@p @p)

tests/golden/types-prelude-ui/types.txt+21−21

@@ -1,27 +1,27 @@

1partial inference; module not checked

2+$ msg: cases proven disjoint; mold not checked

3+$ model: not checked

4−++ row-scheme: $-([attrs=(list attr) kids=(list (element A))] (element A))

4+++ row-scheme: $-([attrs=(list attr) kids=(list (element M))] (element M))

5−++ column-scheme: $-([attrs=(list attr) kids=(list (element A))] (element A))

5+++ column-scheme: $-([attrs=(list attr) kids=(list (element M))] (element M))

6−++ wrap-scheme: $-([attrs=(list attr) kids=(list (element A))] (element A))

6+++ wrap-scheme: $-([attrs=(list attr) kids=(list (element M))] (element M))

7−++ stack-scheme: $-([attrs=(list attr) kids=(list (element A))] (element A))

7+++ stack-scheme: $-([attrs=(list attr) kids=(list (element M))] (element M))

8−++ el-scheme: $-([attrs=(list attr) kid=(element A)] (element A))

8+++ el-scheme: $-([attrs=(list attr) kid=(element M)] (element M))

9−++ para-scheme: $-((list (element A)) (element A))

9+++ para-scheme: $-((list (element M)) (element M))

10−++ text-scheme: $-(@t (element A))

10+++ text-scheme: $-(@t (element M))

11−++ heading-scheme: $-([level=@ud words=@t] (element A))

11+++ heading-scheme: $-([level=@ud words=@t] (element M))

12−++ each-scheme: $-((list [key=A el=(element B)]) (element B))

12+++ each-scheme: $-((list [key=K el=(element M)]) (element M))

13−++ table-scheme: $-([columns=(list [header=@t [width=length align=align]]) rows=(list [key=A cells=(list (element B))])] (element B))

13+++ table-scheme: $-([columns=(list [header=@t [width=length align=align]]) rows=(list [key=K cells=(list (element M))])] (element M))

14−++ image-scheme: $-([source=qath description=@t] (element A))

14+++ image-scheme: $-([source=qath description=@t] (element M))

15−++ image-unsafe-scheme: $-([source=[url=@t [width=@ud height=@ud]] description=@t] (element A))

15+++ image-unsafe-scheme: $-([source=[url=@t [width=@ud height=@ud]] description=@t] (element M))

16−++ link-scheme: $-([target=qath label=@t] (element A))

16+++ link-scheme: $-([target=qath label=@t] (element M))

17−++ link-unsafe-scheme: $-([target=@t label=@t] (element A))

17+++ link-unsafe-scheme: $-([target=@t label=@t] (element M))

18−++ button-scheme: $-([label=@t message=A] (element A))

18+++ button-scheme: $-([label=@t message=M] (element M))

19−++ toggle-scheme: $-([on=? [label=@t message=A]] (element A))

19+++ toggle-scheme: $-([on=? [label=@t message=M]] (element M))

20−++ field-scheme: $-([label=@t [value=@t reply=$-(@t A)]] (element A))

20+++ field-scheme: $-([label=@t [value=@t reply=$-(@t M)]] (element M))

21−++ form-scheme: $-([message=A kids=(list (element A))] (element A))

21+++ form-scheme: $-([message=M kids=(list (element M))] (element M))

22−++ island-scheme: $-([p=[init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]] data=A] (element !!))

22+++ island-scheme: $-([p=[init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] data=Data] (element !!))

23−++ program-scheme: $-([init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]] [init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]])

23+++ program-scheme: $-([init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] [init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]])

24−++ page-scheme: $-([load=$-(A (ask B)) view=$-(B (element !!))] [load=$-(A (ask B)) view=$-(B (element !!))])

24+++ page-scheme: $-([load=$-(Params (ask Data)) view=$-(Data (element !!))] [load=$-(Params (ask Data)) view=$-(Data (element !!))])

25++ static-text: (element !!)

26++ raw-text: (element !!)

27++ static-ui: (element !!)

tests/golden/types-proj-explicit-context/types.txt+2−2

@@ -6,7 +6,7 @@ partial inference; module not checked

6++ from-call: [a=@t b=@p]

7++ into-call: @t

8++ nested: [result=[a=@t b=@p] done=?]

9−++ generic: $-(A [a=@t b=A])

9+++ generic: $-(B [a=@t b=B])

10++ no-context: proj needs an expected record type

11++ unknown-target: proj needs an expected record type

12++ missing: proj constraint needs unsupported inference

@@ -25,7 +25,7 @@ partial inference; module not checked

25++ two-arguments: name is not available to partial inference

26++ one-field: [a=@t]

27++ exact-record: [a=@t b=@p]

28−++ positional-generic: $-([a=@t b=A] @t)

28+++ positional-generic: $-([a=@t b=B] @t)

29++ positional-generic-call: @t

30++ subsequence: [a=@t c=?]

31++ reversed: proj constraint needs unsupported inference

tests/golden/types-proj-nested-no-implicit/types.txt+3−3

@@ -1,7 +1,7 @@

1partial inference; module not checked

2−++ sink-unit: $-((unit [a=@t b=A]) @t)

2+++ sink-unit: $-((unit [a=@t b=B]) @t)

3++ unit-bad: unit payload constraint is not supported by partial inference

4−++ sink-list: $-((list [a=@t b=A]) @t)

4+++ sink-list: $-((list [a=@t b=B]) @t)

5++ list-bad: list item constraint is not supported by partial inference

6−++ sink-nested: $-([one=[a=@t b=A] other=@ud] @t)

6+++ sink-nested: $-([one=[a=@t b=B] other=@ud] @t)

7++ nested-bad: call constraint is not supported by partial inference

tests/golden/types-recursion-scc-groups/types.txt+1−1

@@ -5,6 +5,6 @@ partial inference; module not checked

5++ fourth: $-(@p A)

6++ fifth: $-(@p A)

7++ poly-a: $-(A B)

8−++ poly-b: $-(A B)

8+++ poly-b: $-(B A)

9++ call-text: A

10++ call-ship: A

tests/golden/types-typevar-names/about.txtnew file+4

@@ -0,0 +1,4 @@

1+source: Grammar tab, Types: "Printed types show a type variable by the name it was written with"; "A variable from a gate a `++` uses keeps that gate's name"; "When several named variables become one, a capital written in the `++` names it; otherwise the one made first does".

2+tests: written names of several letters print as written; the prelude's program, island and page keep Data, Model, Msg and Params through instantiation; a written capital names its variable when it meets a called gate's atom or gate-free variable; button's M yields to a written Msg; joined prelude variables take the first made, cork's A and turn's A; a call note and a forced-equal error name the written variables

3+expect: parses

4+expect-types: id $-(Msg Msg); make and embed with Data, Model and Msg; load-page with Params and Data; narrow where Num is an atom other than ?; keyed where Key contains no gates; composed $-(A A); applied (list A); use-hunt's note names Num; forced reports Key and Value

tests/golden/types-typevar-names/modules.txtnew file+1

@@ -0,0 +1 @@

1+# no module fixtures

tests/golden/types-typevar-names/source.jibbnew file+14

@@ -0,0 +1,14 @@

1+++ id |= x=Msg x

2+++ swap |= [a=Key b=Value] [b a]

3+++ make program

4+++ embed island

5+++ load-page page

6+++ narrow |= [lo=Num hi=Num] (add lo hi)

7+++ keyed |= [a=Key b=Key] (eq a b)

8+++ button-of |= m=Msg (button "go" m)

9+++ mapped |= xs=(list Item) (turn xs same)

10+++ composed (cork same same)

11+++ applied (turn ~ same)

12+++ before |= [x=Num y=Num] (gth y x)

13+++ use-hunt (hunt before `1 `2)

14+++ forced |= [a=Key b=Value] ^- (list Key) ~[a b]

tests/golden/types-typevar-names/tokens.txtnew file+162

@@ -0,0 +1,162 @@

1+1:1 glyph ++

2+1:4 name id

3+1:7 glyph |=

4+1:10 name x

5+1:11 tight glyph =

6+1:12 tight tvar Msg

7+1:16 name x

8+2:1 NEWLINE

9+2:1 glyph ++

10+2:4 name swap

11+2:9 glyph |=

12+2:12 glyph [

13+2:13 tight name a

14+2:14 tight glyph =

15+2:15 tight tvar Key

16+2:19 name b

17+2:20 tight glyph =

18+2:21 tight tvar Value

19+2:26 tight glyph ]

20+2:28 glyph [

21+2:29 tight name b

22+2:31 name a

23+2:32 tight glyph ]

24+3:1 NEWLINE

25+3:1 glyph ++

26+3:4 name make

27+3:9 name program

28+4:1 NEWLINE

29+4:1 glyph ++

30+4:4 name embed

31+4:10 name island

32+5:1 NEWLINE

33+5:1 glyph ++

34+5:4 name load-page

35+5:14 name page

36+6:1 NEWLINE

37+6:1 glyph ++

38+6:4 name narrow

39+6:11 glyph |=

40+6:14 glyph [

41+6:15 tight name lo

42+6:17 tight glyph =

43+6:18 tight tvar Num

44+6:22 name hi

45+6:24 tight glyph =

46+6:25 tight tvar Num

47+6:28 tight glyph ]

48+6:30 glyph (

49+6:31 tight name add

50+6:35 name lo

51+6:38 name hi

52+6:40 tight glyph )

53+7:1 NEWLINE

54+7:1 glyph ++

55+7:4 name keyed

56+7:10 glyph |=

57+7:13 glyph [

58+7:14 tight name a

59+7:15 tight glyph =

60+7:16 tight tvar Key

61+7:20 name b

62+7:21 tight glyph =

63+7:22 tight tvar Key

64+7:25 tight glyph ]

65+7:27 glyph (

66+7:28 tight name eq

67+7:31 name a

68+7:33 name b

69+7:34 tight glyph )

70+8:1 NEWLINE

71+8:1 glyph ++

72+8:4 name button-of

73+8:14 glyph |=

74+8:17 name m

75+8:18 tight glyph =

76+8:19 tight tvar Msg

77+8:23 glyph (

78+8:24 tight name button

79+8:31 str "go"

80+8:36 name m

81+8:37 tight glyph )

82+9:1 NEWLINE

83+9:1 glyph ++

84+9:4 name mapped

85+9:11 glyph |=

86+9:14 name xs

87+9:16 tight glyph =

88+9:17 tight glyph (

89+9:18 tight name list

90+9:23 tvar Item

91+9:27 tight glyph )

92+9:29 glyph (

93+9:30 tight name turn

94+9:35 name xs

95+9:38 name same

96+9:42 tight glyph )

97+10:1 NEWLINE

98+10:1 glyph ++

99+10:4 name composed

100+10:13 glyph (

101+10:14 tight name cork

102+10:19 name same

103+10:24 name same

104+10:28 tight glyph )

105+11:1 NEWLINE

106+11:1 glyph ++

107+11:4 name applied

108+11:12 glyph (

109+11:13 tight name turn

110+11:18 lit ~

111+11:20 name same

112+11:24 tight glyph )

113+12:1 NEWLINE

114+12:1 glyph ++

115+12:4 name before

116+12:11 glyph |=

117+12:14 glyph [

118+12:15 tight name x

119+12:16 tight glyph =

120+12:17 tight tvar Num

121+12:21 name y

122+12:22 tight glyph =

123+12:23 tight tvar Num

124+12:26 tight glyph ]

125+12:28 glyph (

126+12:29 tight name gth

127+12:33 name y

128+12:35 name x

129+12:36 tight glyph )

130+13:1 NEWLINE

131+13:1 glyph ++

132+13:4 name use-hunt

133+13:13 glyph (

134+13:14 tight name hunt

135+13:19 name before

136+13:26 glyph `

137+13:27 tight lit 1

138+13:29 glyph `

139+13:30 tight lit 2

140+13:31 tight glyph )

141+14:1 NEWLINE

142+14:1 glyph ++

143+14:4 name forced

144+14:11 glyph |=

145+14:14 glyph [

146+14:15 tight name a

147+14:16 tight glyph =

148+14:17 tight tvar Key

149+14:21 name b

150+14:22 tight glyph =

151+14:23 tight tvar Value

152+14:28 tight glyph ]

153+14:30 glyph ^-

154+14:33 glyph (

155+14:34 tight name list

156+14:39 tvar Key

157+14:42 tight glyph )

158+14:44 glyph ~[

159+14:46 tight name a

160+14:48 name b

161+14:49 tight glyph ]

162+14:50 NEWLINE

tests/golden/types-typevar-names/tree.txtnew file+67

@@ -0,0 +1,67 @@

1+(module

2+ (value 1:1 id

3+ (gate 1:7

4+ (face 1:10 x (tvar 1:12 Msg))

5+ (wing 1:16 x)))

6+ (value 2:1 swap

7+ (gate 2:9

8+ (cell 2:12

9+ (face 2:13 a (tvar 2:15 Key))

10+ (face 2:19 b (tvar 2:21 Value)))

11+ (tuple 2:28 (wing 2:29 b) (wing 2:31 a))))

12+ (value 3:1 make (wing 3:9 program))

13+ (value 4:1 embed (wing 4:10 island))

14+ (value 5:1 load-page (wing 5:14 page))

15+ (value 6:1 narrow

16+ (gate 6:11

17+ (cell 6:14

18+ (face 6:15 lo (tvar 6:18 Num))

19+ (face 6:22 hi (tvar 6:25 Num)))

20+ (group 6:30

21+ (call 6:31 (wing 6:31 add) (wing 6:35 lo) (wing 6:38 hi)))))

22+ (value 7:1 keyed

23+ (gate 7:10

24+ (cell 7:13

25+ (face 7:14 a (tvar 7:16 Key))

26+ (face 7:20 b (tvar 7:22 Key)))

27+ (group 7:27

28+ (call 7:28 (wing 7:28 eq) (wing 7:31 a) (wing 7:33 b)))))

29+ (value 8:1 button-of

30+ (gate 8:14

31+ (face 8:17 m (tvar 8:19 Msg))

32+ (group 8:23

33+ (call 8:24 (wing 8:24 button) (str 8:31 "go") (wing 8:36 m)))))

34+ (value 9:1 mapped

35+ (gate 9:11

36+ (face 9:14 xs

37+ (apply 9:17 list (tvar 9:23 Item)))

38+ (group 9:29

39+ (call 9:30 (wing 9:30 turn) (wing 9:35 xs) (wing 9:38 same)))))

40+ (value 10:1 composed

41+ (group 10:13

42+ (call 10:14 (wing 10:14 cork) (wing 10:19 same) (wing 10:24 same))))

43+ (value 11:1 applied

44+ (group 11:12

45+ (call 11:13 (wing 11:13 turn) (lit 11:18 ~) (wing 11:20 same))))

46+ (value 12:1 before

47+ (gate 12:11

48+ (cell 12:14

49+ (face 12:15 x (tvar 12:17 Num))

50+ (face 12:21 y (tvar 12:23 Num)))

51+ (group 12:28

52+ (call 12:29 (wing 12:29 gth) (wing 12:33 y) (wing 12:35 x)))))

53+ (value 13:1 use-hunt

54+ (group 13:13

55+ (call 13:14

56+ (wing 13:14 hunt)

57+ (wing 13:19 before)

58+ (unit 13:26 (lit 13:27 1))

59+ (unit 13:29 (lit 13:30 2)))))

60+ (value 14:1 forced

61+ (gate 14:11

62+ (cell 14:14

63+ (face 14:15 a (tvar 14:17 Key))

64+ (face 14:21 b (tvar 14:23 Value)))

65+ (cast 14:30

66+ (apply 14:33 list (tvar 14:39 Key))

67+ (list 14:44 (wing 14:46 a) (wing 14:48 b))))))

tests/golden/types-typevar-names/types.txtnew file+27

@@ -0,0 +1,27 @@

1+partial inference; module not checked

2+++ id: $-(Msg Msg)

3+++ swap: $-([a=Key b=Value] [Value Key])

4+++ make: $-([init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] [init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]])

5+++ embed: $-([p=[init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] data=Data] (element !!))

6+++ load-page: $-([load=$-(Params (ask Data)) view=$-(Data (element !!))] [load=$-(Params (ask Data)) view=$-(Data (element !!))])

7+++ narrow: $-([lo=Num hi=Num] Num) where Num is an atom other than ?

8+++ keyed: $-([a=Key b=Key] ?) where Key contains no gates

9+++ button-of: $-(Msg (element Msg))

10+++ mapped: $-((list Item) (list Item))

11+++ composed: $-(A A)

12+++ applied: (list A)

13+++ before: $-([x=Num y=Num] ?) where Num is an atom

14+++ use-hunt: call's sample and argument types do not unify

15+/tests/golden/types-typevar-names/source.jibb:13:14: called gate

16+++ use-hunt (hunt before `1 `2)

17+ ^

18+/tests/golden/types-typevar-names/source.jibb:13:19: argument has type $-([x=Num y=Num] ?) where Num is an atom

19+++ use-hunt (hunt before `1 `2)

20+ ^

21+++ forced: distinct type variables `Key` and `Value` must not be forced equal; use the same capital for a shared type

22+/tests/golden/types-typevar-names/source.jibb:14:17: first type variable

23+++ forced |= [a=Key b=Value] ^- (list Key) ~[a b]

24+ ^

25+/tests/golden/types-typevar-names/source.jibb:14:23: second type variable

26+++ forced |= [a=Key b=Value] ^- (list Key) ~[a b]

27+ ^

tests/golden/types-typevar-print/about.txtnew file+4

@@ -0,0 +1,4 @@

1+source: Grammar tab, Types: "A variable with no name prints as a letter that no other variable in the same type uses".

2+tests: an unnamed variable prints as the first letter no written name in the same type spells; two variables with one name print the second as a letter; names with digits; a local ++ shares the enclosing ++'s written name

3+expect: parses

4+expect-types: same2 $-(A A); with-a $-(A [A $-(B B)]); with-b $-(B [$-(A A) B]); two $-(* [$-(Msg Msg) $-(A A)]); letters $-(Msg [Msg [$-(A A) $-(B B)]]); outer $-(Item Item)

tests/golden/types-typevar-print/source.jibbnew file+11

@@ -0,0 +1,11 @@

1+++ same2 |=(x x)

2+++ with-a |= x=A [x same2]

3+++ with-b |= x=B [same2 x]

4+++ twice |= x=* [same2 same2]

5+++ pass |= x=Msg x

6+++ two |= x=* [pass pass]

7+++ letters |= x=Msg [x same2 pass]

8+++ digits |= [x=T2 y=A1] [y x]

9+++ outer |= x=Item

10+ ++ inner |= y=Item y

11+ (inner x)

tests/golden/types-typevar-print/tokens.txtnew file+108

@@ -0,0 +1,108 @@

1+1:1 glyph ++

2+1:4 name same2

3+1:10 glyph |=(

4+1:13 tight name x

5+1:15 name x

6+1:16 tight glyph )

7+2:1 NEWLINE

8+2:1 glyph ++

9+2:4 name with-a

10+2:11 glyph |=

11+2:14 name x

12+2:15 tight glyph =

13+2:16 tight tvar A

14+2:18 glyph [

15+2:19 tight name x

16+2:21 name same2

17+2:26 tight glyph ]

18+3:1 NEWLINE

19+3:1 glyph ++

20+3:4 name with-b

21+3:11 glyph |=

22+3:14 name x

23+3:15 tight glyph =

24+3:16 tight tvar B

25+3:18 glyph [

26+3:19 tight name same2

27+3:25 name x

28+3:26 tight glyph ]

29+4:1 NEWLINE

30+4:1 glyph ++

31+4:4 name twice

32+4:10 glyph |=

33+4:13 name x

34+4:14 tight glyph =

35+4:15 tight glyph *

36+4:17 glyph [

37+4:18 tight name same2

38+4:24 name same2

39+4:29 tight glyph ]

40+5:1 NEWLINE

41+5:1 glyph ++

42+5:4 name pass

43+5:9 glyph |=

44+5:12 name x

45+5:13 tight glyph =

46+5:14 tight tvar Msg

47+5:18 name x

48+6:1 NEWLINE

49+6:1 glyph ++

50+6:4 name two

51+6:8 glyph |=

52+6:11 name x

53+6:12 tight glyph =

54+6:13 tight glyph *

55+6:15 glyph [

56+6:16 tight name pass

57+6:21 name pass

58+6:25 tight glyph ]

59+7:1 NEWLINE

60+7:1 glyph ++

61+7:4 name letters

62+7:12 glyph |=

63+7:15 name x

64+7:16 tight glyph =

65+7:17 tight tvar Msg

66+7:21 glyph [

67+7:22 tight name x

68+7:24 name same2

69+7:30 name pass

70+7:34 tight glyph ]

71+8:1 NEWLINE

72+8:1 glyph ++

73+8:4 name digits

74+8:11 glyph |=

75+8:14 glyph [

76+8:15 tight name x

77+8:16 tight glyph =

78+8:17 tight tvar T2

79+8:20 name y

80+8:21 tight glyph =

81+8:22 tight tvar A1

82+8:24 tight glyph ]

83+8:26 glyph [

84+8:27 tight name y

85+8:29 name x

86+8:30 tight glyph ]

87+9:1 NEWLINE

88+9:1 glyph ++

89+9:4 name outer

90+9:10 glyph |=

91+9:13 name x

92+9:14 tight glyph =

93+9:15 tight tvar Item

94+10:3 INDENT

95+10:3 glyph ++

96+10:6 name inner

97+10:12 glyph |=

98+10:15 name y

99+10:16 tight glyph =

100+10:17 tight tvar Item

101+10:22 name y

102+11:3 NEWLINE

103+11:3 glyph (

104+11:4 tight name inner

105+11:10 name x

106+11:11 tight glyph )

107+11:12 DEDENT

108+11:12 NEWLINE

tests/golden/types-typevar-print/tree.txtnew file+43

@@ -0,0 +1,43 @@

1+(module

2+ (value 1:1 same2

3+ (gate-wide 1:10 (bind 1:13 x) (wing 1:15 x)))

4+ (value 2:1 with-a

5+ (gate 2:11

6+ (face 2:14 x (tvar 2:16 A))

7+ (tuple 2:18 (wing 2:19 x) (wing 2:21 same2))))

8+ (value 3:1 with-b

9+ (gate 3:11

10+ (face 3:14 x (tvar 3:16 B))

11+ (tuple 3:18 (wing 3:19 same2) (wing 3:25 x))))

12+ (value 4:1 twice

13+ (gate 4:10

14+ (face 4:13 x (noun 4:15))

15+ (tuple 4:17 (wing 4:18 same2) (wing 4:24 same2))))

16+ (value 5:1 pass

17+ (gate 5:9

18+ (face 5:12 x (tvar 5:14 Msg))

19+ (wing 5:18 x)))

20+ (value 6:1 two

21+ (gate 6:8

22+ (face 6:11 x (noun 6:13))

23+ (tuple 6:15 (wing 6:16 pass) (wing 6:21 pass))))

24+ (value 7:1 letters

25+ (gate 7:12

26+ (face 7:15 x (tvar 7:17 Msg))

27+ (tuple 7:21 (wing 7:22 x) (wing 7:24 same2) (wing 7:30 pass))))

28+ (value 8:1 digits

29+ (gate 8:11

30+ (cell 8:14

31+ (face 8:15 x (tvar 8:17 T2))

32+ (face 8:20 y (tvar 8:22 A1)))

33+ (tuple 8:26 (wing 8:27 y) (wing 8:29 x))))

34+ (value 9:1 outer

35+ (gate 9:10

36+ (face 9:13 x (tvar 9:15 Item))

37+ (body 10:3

38+ (value 10:3 inner

39+ (gate 10:12

40+ (face 10:15 y (tvar 10:17 Item))

41+ (wing 10:22 y)))

42+ (group 11:3

43+ (call 11:4 (wing 11:4 inner) (wing 11:10 x)))))))

tests/golden/types-typevar-print/types.txtnew file+10

@@ -0,0 +1,10 @@

1+partial inference; module not checked

2+++ same2: $-(A A)

3+++ with-a: $-(A [A $-(B B)])

4+++ with-b: $-(B [$-(A A) B])

5+++ twice: $-(* [$-(A A) $-(B B)])

6+++ pass: $-(Msg Msg)

7+++ two: $-(* [$-(Msg Msg) $-(A A)])

8+++ letters: $-(Msg [Msg [$-(A A) $-(B B)]])

9+++ digits: $-([x=T2 y=A1] [A1 T2])

10+++ outer: $-(Item Item)

tests/lib/jibb-doc-examples.hoon+1−1

@@ -158,7 +158,7 @@

158 (prepare-prelude-with-internal:jibb public private)

159 ?~ prepared ~["doc-example prelude did not prepare"]

160 ;: weld

161− (doc-positive "view-day" /ui/view-day/jibb view-source %view '$-([day=@da n=@ud] (element A))' u.prepared)

161+ (doc-positive "view-day" /ui/view-day/jibb view-source %view '$-([day=@da n=@ud] (element M))' u.prepared)

162 (doc-positive "step" /ui/step/jibb step-source %describe '$-(step @t)' u.prepared)

163 (doc-cmd-errors cmd-source u.prepared)

164 (doc-import-errors import-source sur action blog card-source u.prepared)

tests/lib/jibb-store.hoon+4−1

@@ -127,8 +127,11 @@

127 =/ store-mold=(unit ischeme:jibb) (find-jibb-mold:jibb %store iface.u.prepared)

128 ?~ store-value ~["store builder is missing"]

129 ?~ store-mold ~["store mold is missing"]

130+ :: The builder's variables keep the names the prelude writes, S and A.

131+ =/ s=@ud (named-var:jibb 'S' 0)

132+ =/ a=@ud (named-var:jibb 'A' 1)

130 =/ expected-builder=itype:jibb

133 =/ expected-builder=itype:jibb

131− [%fn [%cell [%face %init [%var 0]] [%face %update [%fn [%cell [%var 1] [%var 0]] [%var 0]]]] [%cell [%face %init [%var 0]] [%face %update [%noun ~]]]]

134+ [%fn [%cell [%face %init [%var s]] [%face %update [%fn [%cell [%var a] [%var s]] [%var s]]]] [%cell [%face %init [%var s]] [%face %update [%noun ~]]]]

132 ?. &(?=([@ @ ~] vars.u.store-value) =(typ.u.store-value expected-builder)) ~["store builder scheme differs"]

135 ?. &(?=([@ @ ~] vars.u.store-value) =(typ.u.store-value expected-builder)) ~["store builder scheme differs"]

133 =/ expected-mold=itype:jibb [%cell [%face %init [%var 0]] [%face %update [%noun ~]]]

136 =/ expected-mold=itype:jibb [%cell [%face %init [%var 0]] [%face %update [%noun ~]]]

134 ?. &(?=([@ ~] vars.u.store-mold) =(typ.u.store-mold expected-mold)) ~["store mold scheme differs"]

137 ?. &(?=([@ ~] vars.u.store-mold) =(typ.u.store-mold expected-mold)) ~["store mold scheme differs"]

tests/type-buttons/expected.txt+1−1

@@ -1,2 +1,2 @@

1−labelled: $-([label=@t msg=A] (element A))

1+labelled: $-([label=@t msg=M] (element M))

2wide: (list attr)

tests/type-deferred-context/report.txt+1−1

@@ -10,6 +10,6 @@ partial inference; module not checked

10++ first: $-(@t message)

11++ fixed: $-(@t message)

12++ make: $-(A $-(B B))

13−++ built: $-(A A)

13+++ built: $-(B B)

14++ reveal: @t

15++ reveal-ship: @p

tests/type-deferred-resolver/expected.txt+2−2

@@ -1,14 +1,14 @@

1interface retains independent polymorphism

2text use inferred

3ship use inferred

4−stored built: $-(A A)

4+stored built: $-(B B)

5partial inference; module not checked

6+$ message: cases proven disjoint; mold not checked

7++ send: $-($-(@t A) $-(@t A))

8++ make: $-(A $-(B B))

9++ first: $-(@t message)

10++ second: $-(@t message)

11−++ built: $-(A A)

11+++ built: $-(B B)

12++ typed: $-(@t message)

13++ reveal: @t

14++ reveal-ship: @p

tests/type-direct-gate/expected.txt+2−2

@@ -17,7 +17,7 @@ partial inference; module not checked

17++ wrong-msg-update: $-([msg=other state=@ud] [@ud (list (cmd other))])

18++ mismatched-message: call constraint is not supported by partial inference

19++ pending: tag needs context in partial inference

20−++ program-value: $-([init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]] [init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]])

20+++ program-value: $-([init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] [init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]])

21++ update-unfaced: $-([message @ud] [@ud (list (cmd message))])

22++ direct-unfaced: [init=$-(@t @ud) [update=$-([message @ud] [@ud (list (cmd message))]) [view=$-(@ud (element message)) subs=$-(@ud (list (sub message)))]]]

23+$ record: not checked

@@ -58,7 +58,7 @@ partial inference; module not checked

58++ unknown-call: $-($-([A B] C) $-([A B] C))

59++ update-proj-good: $-([msg=message state=[count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))])

60++ program-projection: [init=$-(@t [count=@ud label=@t]) [update=$-([message [count=@ud label=@t]] [[count=@ud label=@t] (list (cmd message))]) [view=$-([count=@ud label=@t] (element message)) subs=$-([count=@ud label=@t] (list (sub message)))]]]

61−++ program-alias: $-([init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]] [init=$-(A B) [update=$-([C B] [B (list (cmd C))]) [view=$-(B (element C)) subs=$-(B (list (sub C)))]]])

61+++ program-alias: $-([init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]] [init=$-(Data Model) [update=$-([Msg Model] [Model (list (cmd Msg))]) [view=$-(Model (element Msg)) subs=$-(Model (list (sub Msg)))]]])

62++ through-head-alias: call constraint is not supported by partial inference

63++ update-alias: $-([msg=message state=@ud] [@ud (list (cmd message))])

64++ through-arg-alias: call constraint is not supported by partial inference