b71609d · jibb · git.iko.soy

docs/compiler.md+4−2

@@ -132,7 +132,7 @@ For a unique supported declaration, `+api-request-parts` retains that evidence w

132

133`+api-support-analysis-source` additionally infers supported ordinary API molds and values, resolves every declared mark, and retains their source, dependency and path evidence. Unsupported helpers or marks fail closed. An unused `/-` core is not independently validated, ordinary definitions that need derived gates remain unsupported, and this result is not a checked API interface or an exported request.

134

135−The ordinary import resolver can infer derived request-gate types for multiple supported API paths. A case may take one typed path parameter before its reply gate, or one diff fold after the reply; a case with both, multiple parameters or diffs, or a separate scry path remains unsupported. Each reply maps the full mark type to a fresh `M` and the request result is `(ask M)`. Checked ordinary API values and molds, declared mark molds and a supported generic poke command helper are exported too. Every selected `/sur` core must have a directly used, successfully read mold; unselected core bindings are not independently validated, and Jibb module imports remain unsupported in this API fragment. An API module outside the fragment fails with the reason its check gave: without `+$ paths`, the poke-only check's, such as `API poke mark %todo-action has no reader result`; otherwise its request constructor's, such as `request paths need unsupported inference`. A failing Jibb import reports its own error, as it does for other modules. A derived `poke` or request name that clashes with a definition, an import face, a prelude value or another derived name is a definite error showing where the name is derived and what it clashes with; `+api-path-analysis-source` and the path evidence entries report it the same way. Only names that surely exist are checked: `poke` when the module declares `+$ poke`, and the case names of a `+$ paths` that reads as path cases. Two cases with the same name do not read as path cases, so that clash stays unsupported, as does a case named `proj`, a reserved name. A name conflict among an API's imports and ordinary definitions reports `module has conflicting names`, as in other modules; a `/%` mark names a mold, so it conflicts only with another mark or mold, and a mark beside a value of the same name, such as a request, is not a conflict. The unchanged todo API fits this fragment.

135+The ordinary import resolver can infer derived request-gate types for multiple supported API paths. A case may take one typed path parameter before its reply gate, or one diff fold after the reply; a case with both, multiple parameters or diffs, or a separate scry path remains unsupported. Each reply maps the full mark type to a fresh `M` and the request result is `(ask M)`. Checked ordinary API values and molds, declared mark molds and a supported generic poke command helper are exported too. Every selected `/sur` core must have a directly used, successfully read mold; unselected core bindings are not independently validated, and Jibb module imports remain unsupported in this API fragment. An API module outside the fragment fails with the reason its check gave: without `+$ paths`, the poke-only check's, such as `API poke mark %todo-action has no reader result`; otherwise its request constructor's, such as `request paths need unsupported inference`. A failing Jibb import reports its own error, as it does for other modules. A derived `poke` or request name that clashes with a definition, an import face, a prelude value or another derived name is a definite error showing where the name is derived and what it clashes with; `+api-path-analysis-source` and the path evidence entries report it the same way. Only names that surely exist are checked: `poke` when the module declares `+$ poke`, and the case names of a `+$ paths` that reads as path cases. Two cases with the same name do not read as path cases, so that clash stays unsupported, as does a case named `proj` or `unface`, a reserved name. A name conflict among an API's imports and ordinary definitions reports `module has conflicting names`, as in other modules; a `/%` mark names a mold, so it conflicts only with another mark or mold, and a mark beside a value of the same name, such as a request, is not a conflict. The unchanged todo API fits this fragment.

136

137A call whose direct result is a known named generic union can receive a matching same-origin, same-arity result context before its arguments are inferred. This retains the ordered generic arguments and existing capital checks; pending tags, recursive or variable-bound origins and unrestricted atom cases remain conservative. Constructor fitting reports unsupported when an unresolved or opaque case could contain the requested tagged head. It keeps definite missing-case errors for proven nonmatching cases, including an explicitly atom-only faced head. The real todo callback `|=%got` can infer when an `(ask msg)` result context fixes its message union; the uncontextualized call remains unsupported.

138

@@ -187,7 +187,9 @@ The internal prelude defines transparent `(ask M)` cases for pure, agent and sto

187

188Public identity aliases of private generic unions retain their public name when the origin, arity and argument order match exactly, including through imported values. Fixed, reordered, repeated and phantom generic aliases remain unsupported where a safe public name cannot be recovered; a fixed nongeneric alias is not printed as though it accepted type arguments.

189

190−The partial checker reserves `proj` in module, local, sample, pattern and import bindings, including bindings inside unsupported source; a field, tag or path segment may still have that spelling. With a known expected record type, it checks selected explicit `(proj record)` calls over closed, uniquely faced records, preserving the source expression, its type, the result type and field axes in the checked interface. Imported and private-prelude dependencies retain the source needed to lower those plans. The checker does not yet lower or execute them. It supports selecting one or more fields in their original order; a single selected field keeps its face and uses one source axis. Reordered fields, unknown or open record spines, some nested contexts and recursive groups with projections remain unsupported. A directional fit of a wider faced record fails closed instead of inserting a projection, including within supported list, unit and record positions. To limit repeated work, record-spine proofs are reused along the same closed spine and stop at 1,024 fields; field boundaries and the special handling of positional calls reset the appropriate proof. Prepared interfaces and their source remain trusted host inputs.

190+The partial checker reserves `proj` and `unface`, one set checked by `+reserved-name`, in module, local, sample, pattern and import bindings, including bindings inside unsupported source; a field, tag or path segment may still have that spelling. With a known expected record type, it checks selected explicit `(proj record)` calls over closed, uniquely faced records, preserving the source expression, its type, the result type and field axes in the checked interface. Imported and private-prelude dependencies retain the source needed to lower those plans. The checker does not yet lower or execute them. It supports selecting one or more fields in their original order; a single selected field keeps its face and uses one source axis. Reordered fields, unknown or open record spines, some nested contexts and recursive groups with projections remain unsupported. A directional fit of a wider faced record fails closed instead of inserting a projection, including within supported list, unit and record positions. To limit repeated work, record-spine proofs are reused along the same closed spine and stop at 1,024 fields; field boundaries and the special handling of positional calls reset the appropriate proof. Prepared interfaces and their source remain trusted host inputs.

191+

192+An explicit `(unface e)` has e's type with every face removed (`+itype-unface`): through cells, a gate's sample and product, collection arguments and the prelude unit's payload, whose own `u=` stays. Other unions and recursive molds go by name or exact cases, so they are kept whole, and an unbound variable stays, keeping any faces it is bound to later. When e's type is still a bare variable the checker reports `unface on a type not yet known is not supported by partial inference`, as it does field access; the deferred transaction declines `unface`. `unface` written as a value, or with other than one argument, is a definite error. A `++` whose body is `(unface |= …)` counts as a gate for self-recursion, recursive groups and the report, with the unfaced type, while direct-call layout evidence, which reads sample faces, leaves it out. Nothing is lowered yet; the core language's row lowers it to its argument.

191

193

192## The tree

194## The tree

193

195

docs/spec/core-language.md+1

@@ -83,6 +83,7 @@ Types, faces and casts leave nothing behind. Everything else lowers by these rul

83| `/posts/~zod`, `%/blog/(slug)` | A list of knots, typed segments printed by their aura's native; the runtime adds the base path to an application path |

84| `title.p`, `space.theme.theme` | `slot` at the field's axis, nested for longer wings |

85| `(proj record)` | Apply a `lam` to the source once; its body constructs the expected record from the required fields using `slot` and `cons`, discarding extra fields |

86+| `(unface e)` | `e`: only its type changes |

86| `card.card`, an import | The qualified name `components/card:card` |

87| `card.card`, an import | The qualified name `components/card:card` |

87| `m(draft=t error=~)` | One `edit` per item, in order: `(edit 7 (edit 6 m t) ~)`. A wing's item edits at the wing's axis, so with `cart` at 2 and `open` at 3 inside it, `m(open.cart=x)` is `(edit 5 m x)`. Each value is computed from `m` as it was |

88| `m(draft=t error=~)` | One `edit` per item, in order: `(edit 7 (edit 6 m t) ~)`. A wing's item edits at the wing's axis, so with `cart` at 2 and `open` at 3 inside it, `m(open.cart=x)` is `(edit 5 m x)`. Each value is computed from `m` as it was |

88| `f a b c` | `(app f (cons a (cons b c)))`: the arguments are the sample |

89| `f a b c` | `(app f (cons a (cons b c)))`: the arguments are the sample |

docs/spec/grammar.md+3−2

@@ -46,6 +46,7 @@ Every literal reads exactly as Hoon reads it: `1000` is an error (write `1.000`)

46- **Faced cells**: `[text="milk" done=%.n]`, or one `name=value` per line of an open bracket. A change takes one or more of the same items, as `m(done=%.y)`; `m()` is an error. A change's item, inline or on a line, may name a wing instead, read through record fields only: `m(open.cart=(not open.cart.m))` sets field `open` of field `cart`, as Hoon's `m(open.cart x)`. Every value is computed from the original record. Two items that set the same field, or one a field inside the other's, as `m(cart=c open.cart=%.y)`, are an error. A cell's items take plain names.

47- **Pairs and units**: `gap+%s2` and `` `x `` bind tighter than calls, so `pad+%s3 gap+%s2` is two items.

48- **Wing** `title.p`, also for imports and prelude groups, which are records: `card.card`, `space.theme.theme`, `get.by`. **Change** `m(draft="x" error=~)`.

49+- **Unface**: `(unface e)` is `e` with every face removed from its type, so a gate or record fits where other names are expected. `~[(unface lth2) (unface lte2)]` is a list though `lth2` names its sample `[x=A y=A]` and `lte2` names it `[a=A b=A]`, and `(take-kv (unface pair))` passes a `[p=@t q=@ud]` where `[k=@t v=@ud]` is expected; the fields then match by position alone. Faces go from cells, from a gate's sample and product, and from a container's arguments, as in `(list [p=@t q=@ud])`. A union or recursive mold goes by name, so it is kept whole: a gate over `msg` still takes a `msg`. Like `proj`, it is an operation the checker handles by type, not a gate: it takes one argument, and `(turn gs unface)` is an error; write `|=(g (unface g))`. A `++` whose body is `(unface |= …)` is still a gate, so it can call itself.

49- **Inline gate**: `|=(p=post.blog title.p)`, or `|=(p title.p)` when the call fixes the type. A bare name in a sample always binds. `|=%got` is case `%got`'s constructor, typed by the gate expected. A bare name binds at any depth of a sample, so `|= [a=@ b]` binds `a` and `b`.

50- **Inline gate**: `|=(p=post.blog title.p)`, or `|=(p title.p)` when the call fixes the type. A bare name in a sample always binds. `|=%got` is case `%got`'s constructor, typed by the gate expected. A bare name binds at any depth of a sample, so `|= [a=@ b]` binds `a` and `b`.

50- **Interpolation**: `{…}` holds any expression; `\{` writes a brace and `\"` a quote; no `<…>`. Strings take Hoon's escapes: `\\` writes a backslash, and `\` with two lowercase hex digits writes that byte, as `\0a` a line feed; any other `\` is an error. A string and each `{…}` close on the line they open, and `::` inside a string is text.

51- **Interpolation**: `{…}` holds any expression; `\{` writes a brace and `\"` a quote; no `<…>`. Strings take Hoon's escapes: `\\` writes a backslash, and `\` with two lowercase hex digits writes that byte, as `\0a` a line feed; any other `\` is an error. A string and each `{…}` close on the line they open, and `::` inside a string is text.

51- **No operators**: `eq a b`, `not x`, `gth a b` are gates.

52- **No operators**: `eq a b`, `not x`, `gth a b` are gates.

@@ -99,7 +100,7 @@ An imported Hoon record with duplicate field names is an error where used; impor

99A file is a module: imports, then definitions.

100A file is a module: imports, then definitions.

100

101

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

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

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

103+- Names may refer to each other in any order, and no name may shadow one already in scope, imports and the prelude included. `proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold.

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.

104- 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.

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.

105- `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.

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.

106- 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.

@@ -146,7 +147,7 @@ A tag literal or `~` gets a fresh type variable and a pending constraint: the va

146- `|=%typed` is a case's constructor: against `$-(@t M)` it is `|=(t [%typed t])`, requiring `M` to have a case `[%typed @t]`. It works for cases whose head is a literal with the same noun as the tag, regardless of how that literal is written: `|=%$` also constructs a case headed by `%.y` or `~`, since each is the noun 0. A bare tag is always a value.

147- `|=%typed` is a case's constructor: against `$-(@t M)` it is `|=(t [%typed t])`, requiring `M` to have a case `[%typed @t]`. It works for cases whose head is a literal with the same noun as the tag, regardless of how that literal is written: `|=%$` also constructs a case headed by `%.y` or `~`, since each is the noun 0. A bare tag is always a value.

147- A variable constrained by tag resolution, and any it mentions, doesn't generalize; it stays open until something in the module fixes it. An island's `main` fixes its messages, so islands resolve their own tags. The inferred gate-free constraint is retained when a type variable is generalized.

148- A variable constrained by tag resolution, and any it mentions, doesn't generalize; it stays open until something in the module fixes it. An island's `main` fixes its messages, so islands resolve their own tags. The inferred gate-free constraint is retained when a type variable is generalized.

148- A constraint still open when its module is checked is an error asking for a `^-`; the checker never guesses. Library helpers can cast, as in `^- (list attr)`.

149- A constraint still open when its module is checked is an error asking for a `^-`; the checker never guesses. Library helpers can cast, as in `^- (list attr)`.

149−- Wing access, changes and `?-` on a type not yet known wait the same way.

150+- Wing access, changes, `unface` and `?-` on a type not yet known wait the same way.

150- Patterns need none of this; they're checked against the subject's type.

151- Patterns need none of this; they're checked against the subject's type.

151

152

152```jibb

153```jibb

jibb-dev/lib/jibb.hoon+164−50

@@ -4660,6 +4660,14 @@

4660:: proofs to fewer than 1,024 cells; the projection planner has a separate

4661:: 4,096-step bound. These are inference limits, not language limits.

4662::

4663+:: `unface` is reserved with proj (+reserved-name) and is also handled by

4664+:: type: (unface e) has e's type with every face removed, through cells,

4665+:: gates and collection arguments, keeping unions and recursive molds

4666+:: whole (+itype-unface). It is not a value, it takes one argument, and

4667+:: a bare type variable is unsupported, as field access on one is. A ++

4668+:: whose body is (unface |= …) is a gate for recursion (+unfaced-gate).

4669+:: It lowers to its argument; no lowering is implemented yet.

4670+::

4663:: Supported API imports derive request-gate types atomically for multiple

4671:: Supported API imports derive request-gate types atomically for multiple

4664:: paths, including one typed segment or one diff fold per case. Their checked

4672:: paths, including one typed segment or one diff fold per case. Their checked

4665:: ordinary definitions, mark molds and supported poke constructor are also

4673:: ordinary definitions, mark molds and supported poke constructor are also

@@ -4967,6 +4975,35 @@

4967 $(a tal.a, b tal.b, sub u.first)

4975 $(a tal.a, b tal.b, sub u.first)

4968 ~

4976 ~

4969::

4977::

4978+:: +itype-unface: t with every face removed, for (unface e)

4979+::

4980+:: It strips through cells, through a gate's sample and product and

4981+:: through a built-in collection's arguments, the prelude's unit

4982+:: included, walking bound variables. Other unions and recursive

4983+:: molds are compared by name or by their exact cases, so stripping

4984+:: inside them would stop them from fitting their own name: they are

4985+:: kept whole. An unbound variable stays, so faces it is bound to

4986+:: later are kept. The unit keeps its own u=, as a list keeps i= and

4987+:: t= in its mold.

4988+::

4989+++ itype-unface

4990+ |= [t=itype sub=isub]

4991+ ^- itype

4992+ =. t (itype-walk t sub)

4993+ ?+ -.t t

4994+ %face $(t body.t)

4995+ %cell [%cell $(t hed.t) $(t tal.t)]

4996+ %fn [%fn $(t sample.t) $(t product.t)]

4997+ %collection [%collection name.t (turn args.t |=(a=itype ^$(t a)))]

4998+ %union

4999+ ?. =(origin.t `[/lib/jibb/prelude/jibb %unit]) t

5000+ ?. ?=([* ~] args.t) t

5001+ =/ nil=itype [%const [%null %n 0 '~']]

5002+ ?. =(cases.t ~[nil [%cell nil [%face %u i.args.t]]]) t

5003+ =/ arg=itype $(t i.args.t)

5004+ t(cases ~[nil [%cell nil [%face %u arg]]], args ~[arg])

5005+ ==

5006+::

4970+$ igf-form [typ=itype sub=isub left=@ud]

5007+$ igf-form [typ=itype sub=isub left=@ud]

4971+$ igf-forms [types=(list itype) sub=isub left=@ud]

5008+$ igf-forms [types=(list itype) sub=isub left=@ud]

4972++ itype-gate-free-forms

5009++ itype-gate-free-forms

@@ -7367,12 +7404,12 @@

7367 ^- isample-result

7404 ^- isample-result

7368 ?- -.s

7405 ?- -.s

7369 %bind

7406 %bind

7370− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))

7407+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))

7371 [%| "sample shadows a name"]

7408 [%| "sample shadows a name"]

7372 =/ t=itype [%var next.state]

7409 =/ t=itype [%var next.state]

7373 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]

7410 [%& t [[name.s [t ~]] env] state(next +(next.state), binders [next.state binders.state])]

7374 %face

7411 %face

7375− ?: |(=(name.s %proj) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))

7412+ ?: |((reserved-name name.s) ?=(^ (ienv-lookup name.s env)) (lien globals.state |=(x=term =(x name.s))))

7376 [%| "sample shadows a name"]

7413 [%| "sample shadows a name"]

7377 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)

7414 =/ t=(unit [typ=itype state=istate]) (infer-simple-shape shape.s state)

7378 ?~ t [%| "sample mold is not supported by partial inference"]

7415 ?~ t [%| "sample mold is not supported by partial inference"]

@@ -7440,7 +7477,7 @@

7440 |-

7477 |-

7441 ?~ ds &

7478 ?~ ds &

7442 ?: ?=(%mold -.i.ds) $(ds t.ds)

7479 ?: ?=(%mold -.i.ds) $(ds t.ds)

7443− ?: =(name.i.ds %proj) |

7480+ ?: (reserved-name name.i.ds) |

7444 ?. (unique-value-name name.i.ds names) |

7481 ?. (unique-value-name name.i.ds names) |

7445 ?: ?=(^ (ienv-lookup name.i.ds env)) |

7482 ?: ?=(^ (ienv-lookup name.i.ds env)) |

7446 ?: (lien globals.state |=(n=term =(n name.i.ds))) |

7483 ?: (lien globals.state |=(n=term =(n name.i.ds))) |

@@ -7464,7 +7501,7 @@

7464 |-

7501 |-

7465 ?~ locals &

7502 ?~ locals &

7466 =/ n=term name.i.locals

7503 =/ n=term name.i.locals

7467− ?: =(n %proj) |

7504+ ?: (reserved-name n) |

7468 ?. (unique-value-name n names) |

7505 ?. (unique-value-name n names) |

7469 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |

7506 ?: (lien molds.state |=(m=[name=term body=shape] =(n name.m))) |

7470 ?: (lien marks.state |=(m=term =(n m))) |

7507 ?: (lien marks.state |=(m=term =(n m))) |

@@ -8144,7 +8181,7 @@

8144 [%| ["list branch pattern is not supported by partial inference" ~]]

8181 [%| ["list branch pattern is not supported by partial inference" ~]]

8145 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)

8182 =/ binder=(unit [head=term tail=term]) ?:(first-empty second-name first-name)

8146 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]

8183 ?~ binder [%| ["list branch pattern is not supported by partial inference" ~]]

8147− ?: |(=(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)))))

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

8148 [%| ["pattern binder shadows a name" ~]]

8185 [%| ["pattern binder shadows a name" ~]]

8149 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]

8186 =/ extended=ienv [[head.u.binder [i.args.typ ~]] [tail.u.binder [typ ~]] env]

8150 =/ left=iresult

8187 =/ left=iresult

@@ -8181,7 +8218,7 @@

8181 [%| ["unit branch pattern is not supported by partial inference" ~]]

8218 [%| ["unit branch pattern is not supported by partial inference" ~]]

8182 =/ binder=(unit term) ?:(first-empty second-name first-name)

8219 =/ binder=(unit term) ?:(first-empty second-name first-name)

8183 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]

8220 ?~ binder [%| ["unit branch pattern is not supported by partial inference" ~]]

8184− ?: |(=(u.binder %proj) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))

8221+ ?: |((reserved-name u.binder) ?=(^ (ienv-lookup u.binder env)) (lien globals.state |=(n=term =(n u.binder))))

8185 [%| ["pattern binder shadows a name" ~]]

8222 [%| ["pattern binder shadows a name" ~]]

8186 =/ payload=(unit itype) (unit-union-payload typ)

8223 =/ payload=(unit itype) (unit-union-payload typ)

8187 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]

8224 ?~ payload [%| ["unit branch subject is not supported by partial inference" ~]]

@@ -8288,7 +8325,7 @@

8288 ^- (unit ienv)

8325 ^- (unit ienv)

8289 =. t ?:(?=(%face -.t) body.t t)

8326 =. t ?:(?=(%face -.t) body.t t)

8290 ?: ?=(%bind -.p)

8327 ?: ?=(%bind -.p)

8291− ?: |(=(name.p %proj) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~

8328+ ?: |((reserved-name name.p) ?=(^ (ienv-lookup name.p env)) (lien globals |=(n=term =(n name.p)))) ~

8292 `[[name.p [t ~]] env]

8329 `[[name.p [t ~]] env]

8293 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)

8330 ?: ?=(%cell -.p) (union-pattern-bind-items items.p t env globals)

8294 `env

8331 `env

@@ -9278,6 +9315,7 @@

9278 [%& typ.instance state.instance]

9315 [%& typ.instance state.instance]

9279 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)

9316 =/ scheme=(unit ischeme) (ienv-lookup i.names.e env)

9280 ?~ scheme

9317 ?~ scheme

9318+ ?: =(i.names.e %unface) [%| (unface-value at.e)]

9281 ?~ prelude.state [%| ["name is not available to partial inference" ~]]

9319 ?~ prelude.state [%| ["name is not available to partial inference" ~]]

9282 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)

9320 =/ prelude-entry=(unit ischeme) (ienv-lookup i.names.e values.u.prelude.state)

9283 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]

9321 ?~ prelude-entry [%| ["name is not available to partial inference" ~]]

@@ -9285,7 +9323,10 @@

9285 [%& typ.inst state.inst]

9323 [%& typ.inst state.inst]

9286 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)

9324 =/ instance=[typ=itype state=istate] (instantiate-scheme u.scheme state)

9287 [%& typ.instance state.instance]

9325 [%& typ.instance state.instance]

9326+ %group

9327+ ?: &(?=(%wing -.inner.e) =(names.inner.e ~[%unface]) ?=(~ (ienv-lookup %unface env)))

9328+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]

9288− %group $(e inner.e)

9329+ $(e inner.e)

9289 %change

9330 %change

9290 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]

9331 ?~ edits.e [%| ["a change takes at least one field" ~[[at.e "empty change"]]]]

9291 =/ target=iresult $(e [%wing at.e target.e])

9332 =/ target=iresult $(e [%wing at.e target.e])

@@ -9429,6 +9470,7 @@

9429 ?~ args.e [%| ["call has no argument" ~]]

9470 ?~ args.e [%| ["call has no argument" ~]]

9430 ?: (explicit-proj-call e env state)

9471 ?: (explicit-proj-call e env state)

9431 [%| ["proj needs an expected record type" ~]]

9472 [%| ["proj needs an expected record type" ~]]

9473+ ?: (reserved-call %unface e env state) (infer-unface e env state)

9432 (infer-call-with-head e env state (infer-fragment head.e env state))

9474 (infer-call-with-head e env state (infer-fragment head.e env state))

9433 * [%| ["expression is not supported by partial inference" ~]]

9475 * [%| ["expression is not supported by partial inference" ~]]

9434 ==

9476 ==

@@ -9819,6 +9861,7 @@

9819 ^- iresult

9861 ^- iresult

9820 ?> ?=(%call -.e)

9862 ?> ?=(%call -.e)

9821 ?~ args.e [%| ["call has no argument" ~]]

9863 ?~ args.e [%| ["call has no argument" ~]]

9864+ ?: (reserved-call %unface e env state) (infer-unface e env state)

9822 =/ head=iresult (infer-fragment head.e env state)

9865 =/ head=iresult (infer-fragment head.e env state)

9823 ?: ?=(%| -.head) head

9866 ?: ?=(%| -.head) head

9824 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)

9867 =/ ht=itype (itype-walk typ.p.head sub.state.p.head)

@@ -9901,18 +9944,70 @@

9901 `(infer-simple-items items.e env state)

9944 `(infer-simple-items items.e env state)

9902 `(width-infer-items items.e index.u.target env state context)

9945 `(width-infer-items items.e index.u.target env state context)

9903::

9946::

9947+:: +reserved-call: whether e calls the reserved operation n

9948+::

9904−:: Experimental intrinsic recognition; real bindings retain normal calls.

9949+:: Experimental intrinsic recognition; real bindings retain normal calls.

9950+++ reserved-call

9951+ |= [n=term e=expr env=ienv state=istate]

9952+ ^- ?

9953+ ?. ?=(%call -.e) |

9954+ ?. ?=(%wing -.head.e) |

9955+ ?. =(names.head.e ~[n]) |

9956+ ?: ?=(^ (ienv-lookup n env)) |

9957+ ?: (lien globals.state |=(x=term =(x n))) |

9958+ ?~ prelude.state &

9959+ ?:(?=(^ (ienv-lookup n values.u.prelude.state)) | &)

9905++ explicit-proj-call

9960++ explicit-proj-call

9906 |= [e=expr env=ienv state=istate]

9961 |= [e=expr env=ienv state=istate]

9907 ^- ?

9962 ^- ?

9908 ?. ?=(%call -.e) |

9963 ?. ?=(%call -.e) |

9909 ?. ?=([* ~] args.e) |

9964 ?. ?=([* ~] args.e) |

9910− ?. ?=(%wing -.head.e) |

9965+ (reserved-call %proj e env state)

9911− ?. =(names.head.e ~[%proj]) |

9966+::

9912− ?: ?=(^ (ienv-lookup %proj env)) |

9967+:: +infer-unface: (unface e), e's type with every face removed

9913− ?: (lien globals.state |=(n=term =(n %proj))) |

9968+::

9914− ?~ prelude.state &

9969+:: A reserved operation handled by type, like proj. Any number of

9915− ?:(?=(^ (ienv-lookup %proj values.u.prelude.state)) | &)

9970+:: arguments is taken here so that a wrong count is an error. A type

9971+:: not yet known would wait, as wing access does; the partial checker

9972+:: has no such wait and reports it as unsupported, as it does field

9973+:: access on such a type.

9974+++ infer-unface

9975+ |= [e=expr env=ienv state=istate]

9976+ ^- iresult

9977+ ?> ?=(%call -.e)

9978+ ?. ?=([* ~] args.e)

9979+ [%| ["unface takes one argument, as (unface e)" ~[[at.e "unface call"]]]]

9980+ ?^ defer.state [%| ["deferred unface needs unsupported inference" ~]]

9981+ =/ value=iresult (infer-fragment i.args.e env state)

9982+ ?: ?=(%| -.value) value

9983+ =/ typ=itype (itype-walk typ.p.value sub.state.p.value)

9984+ ?: ?=(?(%var %fvar) -.typ)

9985+ [%| ["unface on a type not yet known is not supported by partial inference" ~]]

9986+ [%& (itype-unface typ sub.state.p.value) state.p.value]

9987+::

9988+:: +unface-value: the error for unface written where a value goes

9989+::

9990+++ unface-value

9991+ |= at=span

9992+ ^- idiag

9993+ ["unface is not a value; write |=(g (unface g))" ~[[at "unface used as a value"]]]

9994+::

9995+:: +unfaced-gate: the gate under a ++'s (unface |= …), or ~

9996+::

9997+:: Such a ++ is a gate for recursion: its own name has the unfaced

9998+:: type, and its body may call it.

9999+++ unfaced-gate

10000+ |= [e=expr env=ienv state=istate]

10001+ ^- (unit expr)

10002+ ?: ?=(%group -.e) $(e inner.e)

10003+ ?. (reserved-call %unface e env state) ~

10004+ ?> ?=(%call -.e)

10005+ ?. ?=([* ~] args.e) ~

10006+ =/ gate=expr i.args.e

10007+ |-

10008+ ?: ?=(%group -.gate) $(gate inner.gate)

10009+ ?. ?=(?(%gate %gate-wide) -.gate) ~

10010+ `gate

9916++ infer-proj-source

10011++ infer-proj-source

9917 |= [e=expr expected=itype env=ienv state=istate context=span]

10012 |= [e=expr expected=itype env=ienv state=istate context=span]

9918 ^- iresult

10013 ^- iresult

@@ -10319,7 +10414,7 @@

10319 ?~ pats [%& ~]

10414 ?~ pats [%& ~]

10320 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']

10415 ?. ?=(%bind -.i.pats) [%| 'branch pattern is not supported by partial inference']

10321 =/ name=term name.i.pats

10416 =/ name=term name.i.pats

10322− ?: |(=(name %proj) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))

10417+ ?: |((reserved-name name) ?=(^ (ienv-lookup name env)) (lien globals |=(n=term =(n name))) (lien seen |=(n=term =(n name))))

10323 [%| 'pattern shadows a name']

10418 [%| 'pattern shadows a name']

10324 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])

10419 =/ rest=(each (list term) @t) $(pats t.pats, seen [name seen])

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

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

@@ -10861,6 +10956,9 @@

10861 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]

10956 ?^ defer.state [%| ["deferred recursive inference is unsupported" ~]]

10862 =. gate-defs.state ~

10957 =. gate-defs.state ~

10863 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]

10958 ?. ?=(%value -.d) [%| ["recursive definition is not a gate" ~]]

10959+ :: A ++ whose body is (unface |= …) is a gate too, unfaced

10960+ =/ peeled=(unit expr) (unfaced-gate val.d env state)

10961+ =? val.d ?=(^ peeled) u.peeled

10864 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

10962 ?. |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

10865 [%| ["recursive definition is not a gate" ~]]

10963 [%| ["recursive definition is not a gate" ~]]

10866 =/ result=(unit itype) (recursive-branch-seed d env state)

10964 =/ result=(unit itype) (recursive-branch-seed d env state)

@@ -10884,6 +10982,7 @@

10884 =/ product=itype ?~(result [%var id] u.result)

10982 =/ product=itype ?~(result [%var id] u.result)

10885 =/ st=istate state.p.sam(next +(id))

10983 =/ st=istate state.p.sam(next +(id))

10886 =/ seed=itype [%fn typ.p.sam product]

10984 =/ seed=itype [%fn typ.p.sam product]

10985+ =? seed ?=(^ peeled) (itype-unface seed sub.st)

10887 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]

10986 =/ seeded=ienv [[name.d [seed ~]] env.p.sam]

10888 =/ body=expr

10987 =/ body=expr

10889 ?- -.gate

10988 ?- -.gate

@@ -10895,7 +10994,9 @@

10895 ?: ?=(%| -.out) out

10994 ?: ?=(%| -.out) out

10896 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)

10995 =/ uni=(unit isub) (itype-unify product typ.p.out sub.state.p.out)

10897 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]

10996 ?~ uni [%| ["recursive gate constraint is not supported by partial inference" ~]]

10997+ =/ typ=itype [%fn typ.p.sam typ.p.out]

10998+ =? typ ?=(^ peeled) (itype-unface typ u.uni)

10898− [%& [%fn typ.p.sam typ.p.out] state.p.out(sub u.uni)]

10999+ [%& typ state.p.out(sub u.uni)]

10899::

11000::

10900++ dependency-root

11001++ dependency-root

10901 |= names=(list term)

11002 |= names=(list term)

@@ -11003,7 +11104,7 @@

11003:: Infer a cyclic component with one monomorphic seed per gate. All members

11104:: Infer a cyclic component with one monomorphic seed per gate. All members

11004:: must succeed before any scheme is available; pending constraints and

11105:: must succeed before any scheme is available; pending constraints and

11005:: unresolved branch joins remain partial.

11106:: unresolved branch joins remain partial.

11006−+$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps]

11107++$ igate-entry [name=term typ=itype body=expr env=ienv caps=icaps unfaced=?]

11007+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)

11108+$ igate-seeds (each [entries=(list igate-entry) state=istate] idiag)

11008++ seed-gate-group

11109++ seed-gate-group

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

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

@@ -11011,7 +11112,9 @@

11011 ?~ ds [%& [~ state]]

11112 ?~ ds [%& [~ state]]

11012 =/ d=def i.ds

11113 =/ d=def i.ds

11013 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]

11114 ?. ?=(%value -.d) [%| ["recursive group contains a non-gate" ~]]

11115+ :: A ++ whose body is (unface |= …) is a gate too, unfaced

11116+ =/ peeled=(unit expr) (unfaced-gate val.d env state)

11014− =/ gate=expr val.d

11117+ =/ gate=expr ?~(peeled val.d u.peeled)

11015 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))

11118 ?. |(?=(%gate -.gate) ?=(%gate-wide -.gate))

11016 [%| ["recursive group contains a non-gate" ~]]

11119 [%| ["recursive group contains a non-gate" ~]]

11017 =/ initial=istate (reserve-def-caps gate state)

11120 =/ initial=istate (reserve-def-caps gate state)

@@ -11029,7 +11132,8 @@

11029 * !!

11132 * !!

11030 ==

11133 ==

11031 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]

11134 =/ seed=itype [%fn typ.p.sam [%var next.state.p.sam]]

11135+ =? seed ?=(^ peeled) (itype-unface seed sub.state.p.sam)

11032− =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam]

11136+ =/ entry=igate-entry [name.d seed body env.p.sam caps.state.p.sam ?=(^ peeled)]

11033 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)

11137 =/ after=istate state.p.sam(next +(next.state.p.sam), caps caps.state)

11034 =/ rest=igate-seeds $(ds t.ds, state after)

11138 =/ rest=igate-seeds $(ds t.ds, state after)

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

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

@@ -11069,6 +11173,7 @@

11069 ?: (constrained-capitals caps.entry sub.state)

11173 ?: (constrained-capitals caps.entry sub.state)

11070 [%| ["explicit capital constraints are not supported by partial inference" ~]]

11174 [%| ["explicit capital constraints are not supported by partial inference" ~]]

11071 =/ typ=itype (itype-normalize typ.entry sub.state)

11175 =/ typ=itype (itype-normalize typ.entry sub.state)

11176+ =? typ unfaced.entry (itype-unface typ ~)

11072 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]

11177 ?: (itype-has-nvar typ) [%| ["recursive group needs unsupported inference" ~]]

11073 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))

11178 ?: |((itype-has-tag typ) (itype-has-hidden-generic typ) (itype-has-hidden-recursive typ) (unsupported-atom-vars typ caps.entry binders.state sub.state))

11074 [%| ["recursive group needs unsupported inference" ~]]

11179 [%| ["recursive group needs unsupported inference" ~]]

@@ -12292,59 +12397,68 @@

12292 ==

12397 ==

12293 [n $(imports t.imports)]

12398 [n $(imports t.imports)]

12294::

12399::

12400+:: +reserved-name: whether n names a reserved operation

12401+::

12402+:: proj and unface are handled by the checker by type, not bound, so

12403+:: no module may define, import or bind either name, as a value or

12404+:: as a mold. A field, tag or path segment may still be spelled so.

12295−++ reserved-proj-sample

12405+++ reserved-name

12406+ |= n=term

12407+ ^- ?

12408+ |(=(n %proj) =(n %unface))

12409+++ reserved-sample

12296 |= sam=sample

12410 |= sam=sample

12297 ^- ?

12411 ^- ?

12298 ?- -.sam

12412 ?- -.sam

12299− %bind =(name.sam %proj)

12413+ %bind (reserved-name name.sam)

12300− %face =(name.sam %proj)

12414+ %face (reserved-name name.sam)

12301− %pun =(name.sam %proj)

12415+ %pun (reserved-name name.sam)

12302− %cell (lien items.sam reserved-proj-sample)

12416+ %cell (lien items.sam reserved-sample)

12303 * |

12417 * |

12304 ==

12418 ==

12305−++ reserved-proj-pattern

12419+++ reserved-pattern

12306 |= p=pattern

12420 |= p=pattern

12307 ^- ?

12421 ^- ?

12308 ?- -.p

12422 ?- -.p

12309− %bind =(name.p %proj)

12423+ %bind (reserved-name name.p)

12310− %cell (lien items.p reserved-proj-pattern)

12424+ %cell (lien items.p reserved-pattern)

12311 * |

12425 * |

12312 ==

12426 ==

12313−++ reserved-proj-def

12427+++ reserved-def

12314 |= d=def

12428 |= d=def

12315 ^- ?

12429 ^- ?

12316− ?: =(name.d %proj) &

12430+ ?: (reserved-name name.d) &

12317− ?: ?=(%value -.d) (reserved-proj-expr val.d)

12431+ ?: ?=(%value -.d) (reserved-expr val.d)

12318 |

12432 |

12319−++ reserved-proj-expr

12433+++ reserved-expr

12320 |= e=expr

12434 |= e=expr

12321 ^- ?

12435 ^- ?

12322 ?- -.e

12436 ?- -.e

12323− %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))

12437+ %str (lien pieces.e |=(p=piece ?:(?=(%expr -.p) (reserved-expr p.p) |)))

12324− %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-proj-expr p.p) |)))

12438+ %qath (lien segs.e |=(p=qseg ?:(?=(%expr -.p) (reserved-expr p.p) |)))

12325− %change (lien edits.e |=(p=edit (reserved-proj-expr val.p)))

12439+ %change (lien edits.e |=(p=edit (reserved-expr val.p)))

12326 %pair $(e val.e)

12440 %pair $(e val.e)

12327 %unit $(e val.e)

12441 %unit $(e val.e)

12328 %group $(e inner.e)

12442 %group $(e inner.e)

12329− %list (lien items.e reserved-proj-expr)

12443+ %list (lien items.e reserved-expr)

12330− %tuple (lien items.e |=(i=item (reserved-proj-expr val.i)))

12444+ %tuple (lien items.e |=(i=item (reserved-expr val.i)))

12331− ?(%gate %gate-wide) |((reserved-proj-sample sample.e) $(e body.e))

12445+ ?(%gate %gate-wide) |((reserved-sample sample.e) $(e body.e))

12332 %cast $(e val.e)

12446 %cast $(e val.e)

12333− %call |($(e head.e) (lien args.e reserved-proj-expr))

12447+ %call |($(e head.e) (lien args.e reserved-expr))

12334 %trace |($(e val.e) $(e then.e))

12448 %trace |($(e val.e) $(e then.e))

12335− %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-proj-pattern pat.a) (reserved-proj-expr val.a)))))

12449+ %branch |($(e subject.e) (lien arms.e |=(a=arm |((reserved-pattern pat.a) (reserved-expr val.a)))))

12336− %body |((lien defs.e reserved-proj-def) $(e final.e))

12450+ %body |((lien defs.e reserved-def) $(e final.e))

12337 * |

12451 * |

12338 ==

12452 ==

12339::

12453::

12340−++ module-has-reserved-proj

12454+++ module-has-reserved

12341 |= mod=module

12455 |= mod=module

12342 ^- ?

12456 ^- ?

12343 =/ imported=(list term) (import-binding-names imports.mod)

12457 =/ imported=(list term) (import-binding-names imports.mod)

12344 =/ vals=(list term) (global-value-names defs.mod)

12458 =/ vals=(list term) (global-value-names defs.mod)

12345 =/ molds=imolds (collect-simple-molds defs.mod)

12459 =/ molds=imolds (collect-simple-molds defs.mod)

12346 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))

12460 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))

12347− |((lien (weld imported (weld vals mold-names)) |=(n=term =(n %proj))) (lien defs.mod reserved-proj-def))

12461+ |((lien (weld imported (weld vals mold-names)) reserved-name) (lien defs.mod reserved-def))

12348::

12462::

12349++ module-scope-valid

12463++ module-scope-valid

12350 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]

12464 |= [mod=module prelude-values=(list term) prelude-molds=(list term)]

@@ -12353,7 +12467,7 @@

12353 =/ vals=(list term) (global-value-names defs.mod)

12467 =/ vals=(list term) (global-value-names defs.mod)

12354 =/ molds=imolds (collect-simple-molds defs.mod)

12468 =/ molds=imolds (collect-simple-molds defs.mod)

12355 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))

12469 =/ mold-names=(list term) (turn molds |=(m=[name=term body=shape] name.m))

12356− ?: (module-has-reserved-proj mod) |

12470+ ?: (module-has-reserved mod) |

12357 ?. %+ levy imported

12471 ?. %+ levy imported

12358 |= n=term

12472 |= n=term

12359 &((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))))

12473 &((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))))

@@ -13042,7 +13156,7 @@

13042 ^- ?

13156 ^- ?

13043 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))

13157 =/ path-names=(list term) (turn paths |=(p=iapi-path name.p))

13044 =/ derived=(list term) (weld path-names poke-names)

13158 =/ derived=(list term) (weld path-names poke-names)

13045− ?: (lien derived |=(n=term =(n %proj))) |

13159+ ?: (lien derived reserved-name) |

13046 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))

13160 =/ outer=(list term) (weld prelude-values (weld (global-value-names defs.mod) (api-import-faces imports.mod)))

13047 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))

13161 (levy derived |=(n=term &((unique-value-name n derived) !(lien outer |=(x=term =(n x))))))

13048::

13162::

@@ -13074,7 +13188,7 @@

13074 =/ clashes=(list term)

13188 =/ clashes=(list term)

13075 %+ skip names

13189 %+ skip names

13076 |= n=term

13190 |= n=term

13077− ?| =(n %proj)

13191+ ?| (reserved-name n)

13078 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))

13192 &((unique-value-name n names) !(lien outer |=(x=term =(n x))))

13079 ==

13193 ==

13080 ?~ clashes ~

13194 ?~ clashes ~

@@ -13849,7 +13963,7 @@

13849 =/ action=term %poke

13963 =/ action=term %poke

13850 =/ ordinary=(list def) ds

13964 =/ ordinary=(list def) ds

13851 =/ derived=(list term) ~[%state action]

13965 =/ derived=(list term) ~[%state action]

13852− ?: (lien derived |=(n=term =(n %proj))) [%| ~]

13966+ ?: (lien derived reserved-name) [%| ~]

13853 =/ outer=(list term)

13967 =/ outer=(list term)

13854 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))

13968 (weld prelude-values (weld (global-value-names ordinary) (api-import-faces imports.mod)))

13855 =/ clashes=(list term)

13969 =/ clashes=(list term)

@@ -15619,8 +15733,8 @@

15619 ?: ?=(%| -.parsed) (show-error src p.parsed)

15733 ?: ?=(%| -.parsed) (show-error src p.parsed)

15620 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)

15734 =/ duplicate=(unit idiag) (duplicate-defs defs.p.parsed)

15621 ?^ duplicate (duplicate-fields-report file src u.duplicate)

15735 ?^ duplicate (duplicate-fields-report file src u.duplicate)

15622− ?: (module-has-reserved-proj p.parsed)

15736+ ?: (module-has-reserved p.parsed)

15623− 'module has reserved proj name'

15737+ 'module has a reserved proj or unface name'

15624 =/ ds=(list def) defs.p.parsed

15738 =/ ds=(list def) defs.p.parsed

15625 =/ molds=imolds (collect-simple-molds ds)

15739 =/ molds=imolds (collect-simple-molds ds)

15626 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))

15740 =/ globals=(list term) (weld prelude-values (weld (turn jimports |=(j=[face=term interface=ifile] face.j)) (global-value-names ds)))

@@ -15698,7 +15812,7 @@

15698 =. head-evidence.initial heads

15812 =. head-evidence.initial heads

15699 =. initial (reserve-def-caps val.d initial)

15813 =. initial (reserve-def-caps val.d initial)

15700 =/ result=iresult

15814 =/ result=iresult

15701− ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d))

15815+ ?: |(?=(%gate -.val.d) ?=(%gate-wide -.val.d) ?=(^ (unfaced-gate val.d env initial)))

15702 (infer-recursive-gate d env initial)

15816 (infer-recursive-gate d env initial)

15703 (infer-fragment val.d env initial)

15817 (infer-fragment val.d env initial)

15704 ?: ?=(%| -.result)

15818 ?: ?=(%| -.result)

tests/golden/inline-unface-arity-bad/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "Like `proj`, it is an operation the checker handles by type, not a gate"

2+tests: unface takes exactly one argument: two are an error at the call, and none, (unface), is an error at its parenthesis.

3+expect: parses

4+expect-types: a partial inference report: both are errors at the call

tests/golden/inline-unface-arity-bad/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-arity-bad/source.jibbnew file+3

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

1+++ lt-a |= [a=@ud b=@ud] (gth b a)

2+++ two (unface lt-a lt-a)

3+++ none (unface)

tests/golden/inline-unface-arity-bad/tokens.txtnew file+31

@@ -0,0 +1,31 @@

1+1:1 glyph ++

2+1:4 name lt-a

3+1:9 glyph |=

4+1:12 glyph [

5+1:13 tight name a

6+1:14 tight glyph =

7+1:15 tight aura @ud

8+1:19 name b

9+1:20 tight glyph =

10+1:21 tight aura @ud

11+1:24 tight glyph ]

12+1:26 glyph (

13+1:27 tight name gth

14+1:31 name b

15+1:33 name a

16+1:34 tight glyph )

17+2:1 NEWLINE

18+2:1 glyph ++

19+2:4 name two

20+2:8 glyph (

21+2:9 tight name unface

22+2:16 name lt-a

23+2:21 name lt-a

24+2:25 tight glyph )

25+3:1 NEWLINE

26+3:1 glyph ++

27+3:4 name none

28+3:9 glyph (

29+3:10 tight name unface

30+3:16 tight glyph )

31+3:17 NEWLINE

tests/golden/inline-unface-arity-bad/tree.txtnew file+13

@@ -0,0 +1,13 @@

1+(module

2+ (value 1:1 lt-a

3+ (gate 1:9

4+ (cell 1:12

5+ (face 1:13 a (aura 1:15 @ud))

6+ (face 1:19 b (aura 1:21 @ud)))

7+ (group 1:26

8+ (call 1:27 (wing 1:27 gth) (wing 1:31 b) (wing 1:33 a)))))

9+ (value 2:1 two

10+ (group 2:8

11+ (call 2:9 (wing 2:9 unface) (wing 2:16 lt-a) (wing 2:21 lt-a))))

12+ (value 3:1 none

13+ (group 3:9 (wing 3:10 unface))))

tests/golden/inline-unface-arity-bad/types.txtnew file+10

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

1+partial inference; module not checked

2+++ lt-a: $-([a=@ud b=@ud] ?)

3+++ two: unface takes one argument, as (unface e)

4+/tests/golden/inline-unface-arity-bad/source.jibb:2:9: unface call

5+++ two (unface lt-a lt-a)

6+ ^

7+++ none: unface takes one argument, as (unface e)

8+/tests/golden/inline-unface-arity-bad/source.jibb:3:9: unface call

9+++ none (unface)

10+ ^

tests/golden/inline-unface-deep/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type"

2+tests: Faces are removed all the way down: from a gate's product, from a gate in its sample, and from the arguments of a list and a unit, whose own u= stays; a gate with no faces is unchanged.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-deep/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-deep/source.jibbnew file+10

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

1+++ make |= n=@ud ^- [label=@t n=@ud] ["x" n]

2+++ make-u (unface make)

3+++ made (make-u 1)

4+++ apply |= f=$-([x=@ud y=@ud] ?) [r=(f 1 2)]

5+++ apply-u (unface apply)

6+++ pairs ^- (list [p=@t q=@ud]) ~[["a" 1]]

7+++ pairs-u (unface pairs)

8+++ maybe ^- (unit [p=@t q=@ud]) `["a" 1]

9+++ maybe-u (unface maybe)

10+++ same-u (unface same)

tests/golden/inline-unface-deep/tokens.txtnew file+129

@@ -0,0 +1,129 @@

1+1:1 glyph ++

2+1:4 name make

3+1:9 glyph |=

4+1:12 name n

5+1:13 tight glyph =

6+1:14 tight aura @ud

7+1:18 glyph ^-

8+1:21 glyph [

9+1:22 tight name label

10+1:27 tight glyph =

11+1:28 tight aura @t

12+1:31 name n

13+1:32 tight glyph =

14+1:33 tight aura @ud

15+1:36 tight glyph ]

16+1:38 glyph [

17+1:39 tight str "x"

18+1:43 name n

19+1:44 tight glyph ]

20+2:1 NEWLINE

21+2:1 glyph ++

22+2:4 name make-u

23+2:11 glyph (

24+2:12 tight name unface

25+2:19 name make

26+2:23 tight glyph )

27+3:1 NEWLINE

28+3:1 glyph ++

29+3:4 name made

30+3:9 glyph (

31+3:10 tight name make-u

32+3:17 lit 1

33+3:18 tight glyph )

34+4:1 NEWLINE

35+4:1 glyph ++

36+4:4 name apply

37+4:10 glyph |=

38+4:13 name f

39+4:14 tight glyph =

40+4:15 tight glyph $-(

41+4:18 tight glyph [

42+4:19 tight name x

43+4:20 tight glyph =

44+4:21 tight aura @ud

45+4:25 name y

46+4:26 tight glyph =

47+4:27 tight aura @ud

48+4:30 tight glyph ]

49+4:32 glyph ?

50+4:33 tight glyph )

51+4:35 glyph [

52+4:36 tight name r

53+4:37 tight glyph =

54+4:38 tight glyph (

55+4:39 tight name f

56+4:41 lit 1

57+4:43 lit 2

58+4:44 tight glyph )

59+4:45 tight glyph ]

60+5:1 NEWLINE

61+5:1 glyph ++

62+5:4 name apply-u

63+5:12 glyph (

64+5:13 tight name unface

65+5:20 name apply

66+5:25 tight glyph )

67+6:1 NEWLINE

68+6:1 glyph ++

69+6:4 name pairs

70+6:10 glyph ^-

71+6:13 glyph (

72+6:14 tight name list

73+6:19 glyph [

74+6:20 tight name p

75+6:21 tight glyph =

76+6:22 tight aura @t

77+6:25 name q

78+6:26 tight glyph =

79+6:27 tight aura @ud

80+6:30 tight glyph ]

81+6:31 tight glyph )

82+6:33 glyph ~[

83+6:35 tight glyph [

84+6:36 tight str "a"

85+6:40 lit 1

86+6:41 tight glyph ]

87+6:42 tight glyph ]

88+7:1 NEWLINE

89+7:1 glyph ++

90+7:4 name pairs-u

91+7:12 glyph (

92+7:13 tight name unface

93+7:20 name pairs

94+7:25 tight glyph )

95+8:1 NEWLINE

96+8:1 glyph ++

97+8:4 name maybe

98+8:10 glyph ^-

99+8:13 glyph (

100+8:14 tight name unit

101+8:19 glyph [

102+8:20 tight name p

103+8:21 tight glyph =

104+8:22 tight aura @t

105+8:25 name q

106+8:26 tight glyph =

107+8:27 tight aura @ud

108+8:30 tight glyph ]

109+8:31 tight glyph )

110+8:33 glyph `

111+8:34 tight glyph [

112+8:35 tight str "a"

113+8:39 lit 1

114+8:40 tight glyph ]

115+9:1 NEWLINE

116+9:1 glyph ++

117+9:4 name maybe-u

118+9:12 glyph (

119+9:13 tight name unface

120+9:20 name maybe

121+9:25 tight glyph )

122+10:1 NEWLINE

123+10:1 glyph ++

124+10:4 name same-u

125+10:11 glyph (

126+10:12 tight name unface

127+10:19 name same

128+10:23 tight glyph )

129+10:24 NEWLINE

tests/golden/inline-unface-deep/tree.txtnew file+55

@@ -0,0 +1,55 @@

1+(module

2+ (value 1:1 make

3+ (gate 1:9

4+ (face 1:12 n (aura 1:14 @ud))

5+ (cast 1:18

6+ (cell 1:21

7+ (face 1:22 label (aura 1:28 @t))

8+ (face 1:31 n (aura 1:33 @ud)))

9+ (tuple 1:38 (str 1:39 "x") (wing 1:43 n)))))

10+ (value 2:1 make-u

11+ (group 2:11

12+ (call 2:12 (wing 2:12 unface) (wing 2:19 make))))

13+ (value 3:1 made

14+ (group 3:9

15+ (call 3:10 (wing 3:10 make-u) (lit 3:17 1))))

16+ (value 4:1 apply

17+ (gate 4:10

18+ (face 4:13 f

19+ (fn 4:15

20+ (cell 4:18

21+ (face 4:19 x (aura 4:21 @ud))

22+ (face 4:25 y (aura 4:27 @ud)))

23+ (flag 4:32)))

24+ (tuple 4:35

25+ (face 4:36 r

26+ (group 4:38

27+ (call 4:39 (wing 4:39 f) (lit 4:41 1) (lit 4:43 2)))))))

28+ (value 5:1 apply-u

29+ (group 5:12

30+ (call 5:13 (wing 5:13 unface) (wing 5:20 apply))))

31+ (value 6:1 pairs

32+ (cast 6:10

33+ (apply 6:13 list

34+ (cell 6:19

35+ (face 6:20 p (aura 6:22 @t))

36+ (face 6:25 q (aura 6:27 @ud))))

37+ (list 6:33

38+ (tuple 6:35 (str 6:36 "a") (lit 6:40 1)))))

39+ (value 7:1 pairs-u

40+ (group 7:12

41+ (call 7:13 (wing 7:13 unface) (wing 7:20 pairs))))

42+ (value 8:1 maybe

43+ (cast 8:10

44+ (apply 8:13 unit

45+ (cell 8:19

46+ (face 8:20 p (aura 8:22 @t))

47+ (face 8:25 q (aura 8:27 @ud))))

48+ (unit 8:33

49+ (tuple 8:34 (str 8:35 "a") (lit 8:39 1)))))

50+ (value 9:1 maybe-u

51+ (group 9:12

52+ (call 9:13 (wing 9:13 unface) (wing 9:20 maybe))))

53+ (value 10:1 same-u

54+ (group 10:11

55+ (call 10:12 (wing 10:12 unface) (wing 10:19 same)))))

tests/golden/inline-unface-deep/types.txtnew file+11

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

1+partial inference; module not checked

2+++ make: $-(@ud [label=@t n=@ud])

3+++ make-u: $-(@ud [@t @ud])

4+++ made: [@t @ud]

5+++ apply: $-($-([x=@ud y=@ud] ?) [r=?])

6+++ apply-u: $-($-([@ud @ud] ?) ?)

7+++ pairs: (list [p=@t q=@ud])

8+++ pairs-u: (list [@t @ud])

9+++ maybe: (unit [p=@t q=@ud])

10+++ maybe-u: (unit [@t @ud])

11+++ same-u: $-(A A)

tests/golden/inline-unface-gates/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type"

2+tests: Gates whose samples are labelled differently share a list and fit slots written with capitals once unfaced; the same gates without unface fail, and a direct call of an unfaced gate takes any labels.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-gates/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-gates/source.jibbnew file+11

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

1+++ lth2 |= [x=A y=A] (gth y x)

2+++ lte2 |= [a=A b=A] (not (gth a b))

3+++ lt-a |= [a=@ud b=@ud] (gth b a)

4+++ add-f |= [a=@ud b=@ud] (add a b)

5+++ labelled ~[lth2 lte2]

6+++ pickers ~[(unface lth2) (unface lte2)]

7+++ hunt-labelled (hunt lt-a `1 `2)

8+++ hunt-unfaced (hunt (unface lt-a) `1 `2)

9+++ roll-labelled (roll ~[1 2] 0 add-f)

10+++ roll-unfaced (roll ~[1 2] 0 (unface add-f))

11+++ one-off ((unface add-f) [b=1 a=2])

tests/golden/inline-unface-gates/tokens.txtnew file+160

@@ -0,0 +1,160 @@

1+1:1 glyph ++

2+1:4 name lth2

3+1:9 glyph |=

4+1:12 glyph [

5+1:13 tight name x

6+1:14 tight glyph =

7+1:15 tight tvar A

8+1:17 name y

9+1:18 tight glyph =

10+1:19 tight tvar A

11+1:20 tight glyph ]

12+1:22 glyph (

13+1:23 tight name gth

14+1:27 name y

15+1:29 name x

16+1:30 tight glyph )

17+2:1 NEWLINE

18+2:1 glyph ++

19+2:4 name lte2

20+2:9 glyph |=

21+2:12 glyph [

22+2:13 tight name a

23+2:14 tight glyph =

24+2:15 tight tvar A

25+2:17 name b

26+2:18 tight glyph =

27+2:19 tight tvar A

28+2:20 tight glyph ]

29+2:22 glyph (

30+2:23 tight name not

31+2:27 glyph (

32+2:28 tight name gth

33+2:32 name a

34+2:34 name b

35+2:35 tight glyph )

36+2:36 tight glyph )

37+3:1 NEWLINE

38+3:1 glyph ++

39+3:4 name lt-a

40+3:9 glyph |=

41+3:12 glyph [

42+3:13 tight name a

43+3:14 tight glyph =

44+3:15 tight aura @ud

45+3:19 name b

46+3:20 tight glyph =

47+3:21 tight aura @ud

48+3:24 tight glyph ]

49+3:26 glyph (

50+3:27 tight name gth

51+3:31 name b

52+3:33 name a

53+3:34 tight glyph )

54+4:1 NEWLINE

55+4:1 glyph ++

56+4:4 name add-f

57+4:10 glyph |=

58+4:13 glyph [

59+4:14 tight name a

60+4:15 tight glyph =

61+4:16 tight aura @ud

62+4:20 name b

63+4:21 tight glyph =

64+4:22 tight aura @ud

65+4:25 tight glyph ]

66+4:27 glyph (

67+4:28 tight name add

68+4:32 name a

69+4:34 name b

70+4:35 tight glyph )

71+5:1 NEWLINE

72+5:1 glyph ++

73+5:4 name labelled

74+5:13 glyph ~[

75+5:15 tight name lth2

76+5:20 name lte2

77+5:24 tight glyph ]

78+6:1 NEWLINE

79+6:1 glyph ++

80+6:4 name pickers

81+6:12 glyph ~[

82+6:14 tight glyph (

83+6:15 tight name unface

84+6:22 name lth2

85+6:26 tight glyph )

86+6:28 glyph (

87+6:29 tight name unface

88+6:36 name lte2

89+6:40 tight glyph )

90+6:41 tight glyph ]

91+7:1 NEWLINE

92+7:1 glyph ++

93+7:4 name hunt-labelled

94+7:18 glyph (

95+7:19 tight name hunt

96+7:24 name lt-a

97+7:29 glyph `

98+7:30 tight lit 1

99+7:32 glyph `

100+7:33 tight lit 2

101+7:34 tight glyph )

102+8:1 NEWLINE

103+8:1 glyph ++

104+8:4 name hunt-unfaced

105+8:17 glyph (

106+8:18 tight name hunt

107+8:23 glyph (

108+8:24 tight name unface

109+8:31 name lt-a

110+8:35 tight glyph )

111+8:37 glyph `

112+8:38 tight lit 1

113+8:40 glyph `

114+8:41 tight lit 2

115+8:42 tight glyph )

116+9:1 NEWLINE

117+9:1 glyph ++

118+9:4 name roll-labelled

119+9:18 glyph (

120+9:19 tight name roll

121+9:24 glyph ~[

122+9:26 tight lit 1

123+9:28 lit 2

124+9:29 tight glyph ]

125+9:31 lit 0

126+9:33 name add-f

127+9:38 tight glyph )

128+10:1 NEWLINE

129+10:1 glyph ++

130+10:4 name roll-unfaced

131+10:17 glyph (

132+10:18 tight name roll

133+10:23 glyph ~[

134+10:25 tight lit 1

135+10:27 lit 2

136+10:28 tight glyph ]

137+10:30 lit 0

138+10:32 glyph (

139+10:33 tight name unface

140+10:40 name add-f

141+10:45 tight glyph )

142+10:46 tight glyph )

143+11:1 NEWLINE

144+11:1 glyph ++

145+11:4 name one-off

146+11:12 glyph (

147+11:13 tight glyph (

148+11:14 tight name unface

149+11:21 name add-f

150+11:26 tight glyph )

151+11:28 glyph [

152+11:29 tight name b

153+11:30 tight glyph =

154+11:31 tight lit 1

155+11:33 name a

156+11:34 tight glyph =

157+11:35 tight lit 2

158+11:36 tight glyph ]

159+11:37 tight glyph )

160+11:38 NEWLINE

tests/golden/inline-unface-gates/tree.txtnew file+78

@@ -0,0 +1,78 @@

1+(module

2+ (value 1:1 lth2

3+ (gate 1:9

4+ (cell 1:12

5+ (face 1:13 x (tvar 1:15 A))

6+ (face 1:17 y (tvar 1:19 A)))

7+ (group 1:22

8+ (call 1:23 (wing 1:23 gth) (wing 1:27 y) (wing 1:29 x)))))

9+ (value 2:1 lte2

10+ (gate 2:9

11+ (cell 2:12

12+ (face 2:13 a (tvar 2:15 A))

13+ (face 2:17 b (tvar 2:19 A)))

14+ (group 2:22

15+ (call 2:23

16+ (wing 2:23 not)

17+ (group 2:27

18+ (call 2:28 (wing 2:28 gth) (wing 2:32 a) (wing 2:34 b)))))))

19+ (value 3:1 lt-a

20+ (gate 3:9

21+ (cell 3:12

22+ (face 3:13 a (aura 3:15 @ud))

23+ (face 3:19 b (aura 3:21 @ud)))

24+ (group 3:26

25+ (call 3:27 (wing 3:27 gth) (wing 3:31 b) (wing 3:33 a)))))

26+ (value 4:1 add-f

27+ (gate 4:10

28+ (cell 4:13

29+ (face 4:14 a (aura 4:16 @ud))

30+ (face 4:20 b (aura 4:22 @ud)))

31+ (group 4:27

32+ (call 4:28 (wing 4:28 add) (wing 4:32 a) (wing 4:34 b)))))

33+ (value 5:1 labelled

34+ (list 5:13 (wing 5:15 lth2) (wing 5:20 lte2)))

35+ (value 6:1 pickers

36+ (list 6:12

37+ (group 6:14

38+ (call 6:15 (wing 6:15 unface) (wing 6:22 lth2)))

39+ (group 6:28

40+ (call 6:29 (wing 6:29 unface) (wing 6:36 lte2)))))

41+ (value 7:1 hunt-labelled

42+ (group 7:18

43+ (call 7:19

44+ (wing 7:19 hunt)

45+ (wing 7:24 lt-a)

46+ (unit 7:29 (lit 7:30 1))

47+ (unit 7:32 (lit 7:33 2)))))

48+ (value 8:1 hunt-unfaced

49+ (group 8:17

50+ (call 8:18

51+ (wing 8:18 hunt)

52+ (group 8:23

53+ (call 8:24 (wing 8:24 unface) (wing 8:31 lt-a)))

54+ (unit 8:37 (lit 8:38 1))

55+ (unit 8:40 (lit 8:41 2)))))

56+ (value 9:1 roll-labelled

57+ (group 9:18

58+ (call 9:19

59+ (wing 9:19 roll)

60+ (list 9:24 (lit 9:26 1) (lit 9:28 2))

61+ (lit 9:31 0)

62+ (wing 9:33 add-f))))

63+ (value 10:1 roll-unfaced

64+ (group 10:17

65+ (call 10:18

66+ (wing 10:18 roll)

67+ (list 10:23 (lit 10:25 1) (lit 10:27 2))

68+ (lit 10:30 0)

69+ (group 10:32

70+ (call 10:33 (wing 10:33 unface) (wing 10:40 add-f))))))

71+ (value 11:1 one-off

72+ (group 11:12

73+ (call 11:13

74+ (group 11:13

75+ (call 11:14 (wing 11:14 unface) (wing 11:21 add-f)))

76+ (tuple 11:28

77+ (face 11:29 b (lit 11:31 1))

78+ (face 11:33 a (lit 11:35 2)))))))

tests/golden/inline-unface-gates/types.txtnew file+30

@@ -0,0 +1,30 @@

1+partial inference; module not checked

2+++ lth2: $-([x=A y=A] ?) where A is an atom

3+++ lte2: $-([a=A b=A] ?) where A is an atom

4+++ lt-a: $-([a=@ud b=@ud] ?)

5+++ add-f: $-([a=@ud b=@ud] @ud)

6+++ labelled: list items do not have compatible types

7+/tests/golden/inline-unface-gates/source.jibb:5:13: expected item has type $-([x=A y=A] ?) where A is an atom

8+++ labelled ~[lth2 lte2]

9+ ^

10+/tests/golden/inline-unface-gates/source.jibb:5:20: list item has type $-([a=A b=A] ?) where A is an atom

11+++ labelled ~[lth2 lte2]

12+ ^

13+++ pickers: (list $-([A A] ?)) where A is an atom

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

15+/tests/golden/inline-unface-gates/source.jibb:7:19: called gate

16+++ hunt-labelled (hunt lt-a `1 `2)

17+ ^

18+/tests/golden/inline-unface-gates/source.jibb:7:24: argument has type $-([a=@ud b=@ud] ?)

19+++ hunt-labelled (hunt lt-a `1 `2)

20+ ^

21+++ hunt-unfaced: (unit @ud)

22+++ roll-labelled: call's sample and argument types do not unify

23+/tests/golden/inline-unface-gates/source.jibb:9:19: called gate

24+++ roll-labelled (roll ~[1 2] 0 add-f)

25+ ^

26+/tests/golden/inline-unface-gates/source.jibb:9:33: argument has type $-([a=@ud b=@ud] @ud)

27+++ roll-labelled (roll ~[1 2] 0 add-f)

28+ ^

29+++ roll-unfaced: @ud

30+++ one-off: @ud

tests/golden/inline-unface-import/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type" and "A `++` whose body is `(unface |= …)` is still a gate, so it can call itself"

2+tests: An imported module, checked in full, exports unfaced gates and records, a recursive one included, and the importer uses them with their unfaced types.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-import/module-trees.txtnew file+43

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

1+/ui/lib.jibb

2+(module

3+ (value 1:1 lt-a

4+ (gate 1:9

5+ (cell 1:12

6+ (face 1:13 a (aura 1:15 @ud))

7+ (face 1:19 b (aura 1:21 @ud)))

8+ (group 1:26

9+ (call 1:27 (wing 1:27 gth) (wing 1:31 b) (wing 1:33 a)))))

10+ (value 2:1 lt-u

11+ (group 2:9

12+ (call 2:10 (wing 2:10 unface) (wing 2:17 lt-a))))

13+ (value 3:1 weld2

14+ (group 3:10

15+ (call 3:11

16+ (wing 3:11 unface)

17+ (gate 4:3

18+ (cell 4:6

19+ (face 4:7 xs

20+ (apply 4:10 list (tvar 4:16 A)))

21+ (face 4:19 ys

22+ (apply 4:22 list (tvar 4:28 A))))

23+ (cast 4:32

24+ (apply 4:35 list (tvar 4:41 A))

25+ (body 5:5

26+ (branch 5:5

27+ (wing 5:8 xs)

28+ (arm 6:7 (lit 6:7 ~) (wing 6:9 ys))

29+ (arm 7:7

30+ (cell 7:7 (bind 7:8 item) (bind 7:13 rest))

31+ (tuple 7:19

32+ (wing 7:20 item)

33+ (group 7:25

34+ (call 7:26 (wing 7:26 weld2) (wing 7:32 rest) (wing 7:37 ys))))))))))))

35+ (value 8:1 pair

36+ (cast 8:9

37+ (cell 8:12

38+ (face 8:13 p (aura 8:15 @t))

39+ (face 8:18 q (aura 8:20 @ud)))

40+ (tuple 8:25 (str 8:26 "a") (lit 8:30 1))))

41+ (value 9:1 pair-u

42+ (group 9:11

43+ (call 9:12 (wing 9:12 unface) (wing 9:19 pair)))))

tests/golden/inline-unface-import/modules.txtnew file+1

@@ -0,0 +1 @@

1+/ui/lib.jibb

tests/golden/inline-unface-import/modules/ui/lib.jibbnew file+9

@@ -0,0 +1,9 @@

1+++ lt-a |= [a=@ud b=@ud] (gth b a)

2+++ lt-u (unface lt-a)

3+++ weld2 (unface

4+ |= [xs=(list A) ys=(list A)] ^- (list A)

5+ ?- xs

6+ ~ ys

7+ [item rest] [item (weld2 rest ys)]

8+++ pair ^- [p=@t q=@ud] ["a" 1]

9+++ pair-u (unface pair)

tests/golden/inline-unface-import/source.jibbnew file+5

@@ -0,0 +1,5 @@

1+/= lib /ui/lib

2+++ a lt-u.lib

3+++ b (weld2.lib ~[1] ~[2])

4+++ c pair-u.lib

5+++ d (hunt lt-u.lib `1 `2)

tests/golden/inline-unface-import/tokens.txtnew file+38

@@ -0,0 +1,38 @@

1+1:1 glyph /=

2+1:5 name lib

3+1:9 glyph /

4+1:10 tight knot ui

5+1:12 tight glyph /

6+1:13 tight knot lib

7+2:1 NEWLINE

8+2:1 glyph ++

9+2:4 name a

10+2:6 wing lt-u.lib

11+3:1 NEWLINE

12+3:1 glyph ++

13+3:4 name b

14+3:6 glyph (

15+3:7 tight wing weld2.lib

16+3:17 glyph ~[

17+3:19 tight lit 1

18+3:20 tight glyph ]

19+3:22 glyph ~[

20+3:24 tight lit 2

21+3:25 tight glyph ]

22+3:26 tight glyph )

23+4:1 NEWLINE

24+4:1 glyph ++

25+4:4 name c

26+4:6 wing pair-u.lib

27+5:1 NEWLINE

28+5:1 glyph ++

29+5:4 name d

30+5:6 glyph (

31+5:7 tight name hunt

32+5:12 wing lt-u.lib

33+5:21 glyph `

34+5:22 tight lit 1

35+5:24 glyph `

36+5:25 tight lit 2

37+5:26 tight glyph )

38+5:27 NEWLINE

tests/golden/inline-unface-import/tree.txtnew file+17

@@ -0,0 +1,17 @@

1+(module

2+ (jibb 1:1 lib /ui/lib)

3+ (value 2:1 a (wing 2:6 lt-u.lib))

4+ (value 3:1 b

5+ (group 3:6

6+ (call 3:7

7+ (wing 3:7 weld2.lib)

8+ (list 3:17 (lit 3:19 1))

9+ (list 3:22 (lit 3:24 2)))))

10+ (value 4:1 c (wing 4:6 pair-u.lib))

11+ (value 5:1 d

12+ (group 5:6

13+ (call 5:7

14+ (wing 5:7 hunt)

15+ (wing 5:12 lt-u.lib)

16+ (unit 5:21 (lit 5:22 1))

17+ (unit 5:24 (lit 5:25 2))))))

tests/golden/inline-unface-import/types.txtnew file+5

@@ -0,0 +1,5 @@

1+partial inference; module not checked

2+++ a: $-([@ud @ud] ?)

3+++ b: (list @ud)

4+++ c: [@t @ud]

5+++ d: (unit @ud)

tests/golden/inline-unface-named-union/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type"

2+tests: A gate over a named union keeps the union by name, so the unfaced gate still takes a msg and fits a slot written with msg; tags inside unface still take their union from a cast.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-named-union/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-named-union/source.jibbnew file+9

@@ -0,0 +1,9 @@

1++$ msg

2+ [%typed text=@t]

3+ [%sent ~]

4+++ update |= [=msg n=@ud] n

5+++ update-u (unface update)

6+++ direct (update-u [%typed "x"] 1)

7+++ run |= f=$-([msg @ud] @ud) (f [%sent ~] 2)

8+++ ran (run (unface update))

9+++ tagged ^- msg (unface [%typed "x"])

tests/golden/inline-unface-named-union/tokens.txtnew file+89

@@ -0,0 +1,89 @@

1+1:1 glyph +$

2+1:4 name msg

3+2:3 INDENT

4+2:3 glyph [

5+2:4 tight lit %typed

6+2:11 name text

7+2:15 tight glyph =

8+2:16 tight aura @t

9+2:18 tight glyph ]

10+3:3 NEWLINE

11+3:3 glyph [

12+3:4 tight lit %sent

13+3:10 lit ~

14+3:11 tight glyph ]

15+4:1 DEDENT

16+4:1 NEWLINE

17+4:1 glyph ++

18+4:4 name update

19+4:11 glyph |=

20+4:14 glyph [

21+4:15 tight glyph =

22+4:16 tight name msg

23+4:20 name n

24+4:21 tight glyph =

25+4:22 tight aura @ud

26+4:25 tight glyph ]

27+4:27 name n

28+5:1 NEWLINE

29+5:1 glyph ++

30+5:4 name update-u

31+5:13 glyph (

32+5:14 tight name unface

33+5:21 name update

34+5:27 tight glyph )

35+6:1 NEWLINE

36+6:1 glyph ++

37+6:4 name direct

38+6:11 glyph (

39+6:12 tight name update-u

40+6:21 glyph [

41+6:22 tight lit %typed

42+6:29 str "x"

43+6:32 tight glyph ]

44+6:34 lit 1

45+6:35 tight glyph )

46+7:1 NEWLINE

47+7:1 glyph ++

48+7:4 name run

49+7:8 glyph |=

50+7:11 name f

51+7:12 tight glyph =

52+7:13 tight glyph $-(

53+7:16 tight glyph [

54+7:17 tight name msg

55+7:21 aura @ud

56+7:24 tight glyph ]

57+7:26 aura @ud

58+7:29 tight glyph )

59+7:31 glyph (

60+7:32 tight name f

61+7:34 glyph [

62+7:35 tight lit %sent

63+7:41 lit ~

64+7:42 tight glyph ]

65+7:44 lit 2

66+7:45 tight glyph )

67+8:1 NEWLINE

68+8:1 glyph ++

69+8:4 name ran

70+8:8 glyph (

71+8:9 tight name run

72+8:13 glyph (

73+8:14 tight name unface

74+8:21 name update

75+8:27 tight glyph )

76+8:28 tight glyph )

77+9:1 NEWLINE

78+9:1 glyph ++

79+9:4 name tagged

80+9:11 glyph ^-

81+9:14 name msg

82+9:18 glyph (

83+9:19 tight name unface

84+9:26 glyph [

85+9:27 tight lit %typed

86+9:34 str "x"

87+9:37 tight glyph ]

88+9:38 tight glyph )

89+9:39 NEWLINE

tests/golden/inline-unface-named-union/tree.txtnew file+46

@@ -0,0 +1,46 @@

1+(module

2+ (mold 1:1 msg

3+ (union 2:3

4+ (cell 2:3

5+ (const 2:4 %typed)

6+ (face 2:11 text (aura 2:16 @t)))

7+ (cell 3:3 (const 3:4 %sent) (const 3:10 ~))))

8+ (value 4:1 update

9+ (gate 4:11

10+ (cell 4:14

11+ (pun 4:15 msg)

12+ (face 4:20 n (aura 4:22 @ud)))

13+ (wing 4:27 n)))

14+ (value 5:1 update-u

15+ (group 5:13

16+ (call 5:14 (wing 5:14 unface) (wing 5:21 update))))

17+ (value 6:1 direct

18+ (group 6:11

19+ (call 6:12

20+ (wing 6:12 update-u)

21+ (tuple 6:21 (lit 6:22 %typed) (str 6:29 "x"))

22+ (lit 6:34 1))))

23+ (value 7:1 run

24+ (gate 7:8

25+ (face 7:11 f

26+ (fn 7:13

27+ (cell 7:16 (ref 7:17 msg) (aura 7:21 @ud))

28+ (aura 7:26 @ud)))

29+ (group 7:31

30+ (call 7:32

31+ (wing 7:32 f)

32+ (tuple 7:34 (lit 7:35 %sent) (lit 7:41 ~))

33+ (lit 7:44 2)))))

34+ (value 8:1 ran

35+ (group 8:8

36+ (call 8:9

37+ (wing 8:9 run)

38+ (group 8:13

39+ (call 8:14 (wing 8:14 unface) (wing 8:21 update))))))

40+ (value 9:1 tagged

41+ (cast 9:11

42+ (ref 9:14 msg)

43+ (group 9:18

44+ (call 9:19

45+ (wing 9:19 unface)

46+ (tuple 9:26 (lit 9:27 %typed) (str 9:34 "x")))))))

tests/golden/inline-unface-named-union/types.txtnew file+8

@@ -0,0 +1,8 @@

1+partial inference; module not checked

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

3+++ update: $-([msg=msg n=@ud] @ud)

4+++ update-u: $-([msg @ud] @ud)

5+++ direct: @ud

6+++ run: $-($-([msg @ud] @ud) @ud)

7+++ ran: @ud

8+++ tagged: msg

tests/golden/inline-unface-records/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type"

2+tests: A record passed where other labels are expected, which fails without unface; data fields then match by position, so swapped labels pass too.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-records/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-records/source.jibbnew file+8

@@ -0,0 +1,8 @@

1+++ pair-pq ^- [p=@t q=@ud] ["a" 1]

2+++ take-kv |= [k=@t v=@ud] v

3+++ labelled (take-kv pair-pq)

4+++ unfaced (take-kv (unface pair-pq))

5+++ hi-lo ^- [hi=@ud lo=@ud] [10 0]

6+++ want-lo-hi |= r=[lo=@ud hi=@ud] lo.r

7+++ swapped (want-lo-hi hi-lo)

8+++ by-position (want-lo-hi (unface hi-lo))

tests/golden/inline-unface-records/tokens.txtnew file+94

@@ -0,0 +1,94 @@

1+1:1 glyph ++

2+1:4 name pair-pq

3+1:12 glyph ^-

4+1:15 glyph [

5+1:16 tight name p

6+1:17 tight glyph =

7+1:18 tight aura @t

8+1:21 name q

9+1:22 tight glyph =

10+1:23 tight aura @ud

11+1:26 tight glyph ]

12+1:28 glyph [

13+1:29 tight str "a"

14+1:33 lit 1

15+1:34 tight glyph ]

16+2:1 NEWLINE

17+2:1 glyph ++

18+2:4 name take-kv

19+2:12 glyph |=

20+2:15 glyph [

21+2:16 tight name k

22+2:17 tight glyph =

23+2:18 tight aura @t

24+2:21 name v

25+2:22 tight glyph =

26+2:23 tight aura @ud

27+2:26 tight glyph ]

28+2:28 name v

29+3:1 NEWLINE

30+3:1 glyph ++

31+3:4 name labelled

32+3:13 glyph (

33+3:14 tight name take-kv

34+3:22 name pair-pq

35+3:29 tight glyph )

36+4:1 NEWLINE

37+4:1 glyph ++

38+4:4 name unfaced

39+4:12 glyph (

40+4:13 tight name take-kv

41+4:21 glyph (

42+4:22 tight name unface

43+4:29 name pair-pq

44+4:36 tight glyph )

45+4:37 tight glyph )

46+5:1 NEWLINE

47+5:1 glyph ++

48+5:4 name hi-lo

49+5:10 glyph ^-

50+5:13 glyph [

51+5:14 tight name hi

52+5:16 tight glyph =

53+5:17 tight aura @ud

54+5:21 name lo

55+5:23 tight glyph =

56+5:24 tight aura @ud

57+5:27 tight glyph ]

58+5:29 glyph [

59+5:30 tight lit 10

60+5:33 lit 0

61+5:34 tight glyph ]

62+6:1 NEWLINE

63+6:1 glyph ++

64+6:4 name want-lo-hi

65+6:15 glyph |=

66+6:18 name r

67+6:19 tight glyph =

68+6:20 tight glyph [

69+6:21 tight name lo

70+6:23 tight glyph =

71+6:24 tight aura @ud

72+6:28 name hi

73+6:30 tight glyph =

74+6:31 tight aura @ud

75+6:34 tight glyph ]

76+6:36 wing lo.r

77+7:1 NEWLINE

78+7:1 glyph ++

79+7:4 name swapped

80+7:12 glyph (

81+7:13 tight name want-lo-hi

82+7:24 name hi-lo

83+7:29 tight glyph )

84+8:1 NEWLINE

85+8:1 glyph ++

86+8:4 name by-position

87+8:16 glyph (

88+8:17 tight name want-lo-hi

89+8:28 glyph (

90+8:29 tight name unface

91+8:36 name hi-lo

92+8:41 tight glyph )

93+8:42 tight glyph )

94+8:43 NEWLINE

tests/golden/inline-unface-records/tree.txtnew file+44

@@ -0,0 +1,44 @@

1+(module

2+ (value 1:1 pair-pq

3+ (cast 1:12

4+ (cell 1:15

5+ (face 1:16 p (aura 1:18 @t))

6+ (face 1:21 q (aura 1:23 @ud)))

7+ (tuple 1:28 (str 1:29 "a") (lit 1:33 1))))

8+ (value 2:1 take-kv

9+ (gate 2:12

10+ (cell 2:15

11+ (face 2:16 k (aura 2:18 @t))

12+ (face 2:21 v (aura 2:23 @ud)))

13+ (wing 2:28 v)))

14+ (value 3:1 labelled

15+ (group 3:13

16+ (call 3:14 (wing 3:14 take-kv) (wing 3:22 pair-pq))))

17+ (value 4:1 unfaced

18+ (group 4:12

19+ (call 4:13

20+ (wing 4:13 take-kv)

21+ (group 4:21

22+ (call 4:22 (wing 4:22 unface) (wing 4:29 pair-pq))))))

23+ (value 5:1 hi-lo

24+ (cast 5:10

25+ (cell 5:13

26+ (face 5:14 hi (aura 5:17 @ud))

27+ (face 5:21 lo (aura 5:24 @ud)))

28+ (tuple 5:29 (lit 5:30 10) (lit 5:33 0))))

29+ (value 6:1 want-lo-hi

30+ (gate 6:15

31+ (face 6:18 r

32+ (cell 6:20

33+ (face 6:21 lo (aura 6:24 @ud))

34+ (face 6:28 hi (aura 6:31 @ud))))

35+ (wing 6:36 lo.r)))

36+ (value 7:1 swapped

37+ (group 7:12

38+ (call 7:13 (wing 7:13 want-lo-hi) (wing 7:24 hi-lo))))

39+ (value 8:1 by-position

40+ (group 8:16

41+ (call 8:17

42+ (wing 8:17 want-lo-hi)

43+ (group 8:28

44+ (call 8:29 (wing 8:29 unface) (wing 8:36 hi-lo)))))))

tests/golden/inline-unface-records/types.txtnew file+21

@@ -0,0 +1,21 @@

1+partial inference; module not checked

2+++ pair-pq: [p=@t q=@ud]

3+++ take-kv: $-([k=@t v=@ud] @ud)

4+++ labelled: call's sample and argument types do not unify

5+/tests/golden/inline-unface-records/source.jibb:3:14: called gate has type $-([k=@t v=@ud] @ud)

6+++ labelled (take-kv pair-pq)

7+ ^

8+/tests/golden/inline-unface-records/source.jibb:3:22: argument has type [p=@t q=@ud]

9+++ labelled (take-kv pair-pq)

10+ ^

11+++ unfaced: @ud

12+++ hi-lo: [hi=@ud lo=@ud]

13+++ want-lo-hi: $-([lo=@ud hi=@ud] @ud)

14+++ swapped: call's sample and argument types do not unify

15+/tests/golden/inline-unface-records/source.jibb:7:13: called gate has type $-([lo=@ud hi=@ud] @ud)

16+++ swapped (want-lo-hi hi-lo)

17+ ^

18+/tests/golden/inline-unface-records/source.jibb:7:24: argument has type [hi=@ud lo=@ud]

19+++ swapped (want-lo-hi hi-lo)

20+ ^

21+++ by-position: @ud

tests/golden/inline-unface-recursive/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "`(unface e)` is `e` with every face removed from its type"

2+tests: A ++ whose body is (unface |= …) is still a gate: it calls itself, two such gates call each other, and a local one recurses; each name has the unfaced type.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-recursive/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-recursive/source.jibbnew file+23

@@ -0,0 +1,23 @@

1+++ weld2 (unface

2+ |= [xs=(list A) ys=(list A)] ^- (list A)

3+ ?- xs

4+ ~ ys

5+ [item rest] [item (weld2 rest ys)]

6+++ joined (weld2 ~[1] ~[2])

7+++ even (unface

8+ |= n=@ud ^- ?

9+ ?- (eq n 0)

10+ %.y %.y

11+ %.n (odd (dec n))

12+++ odd (unface

13+ |= n=@ud ^- ?

14+ ?- (eq n 0)

15+ %.y %.n

16+ %.n (even (dec n))

17+++ outer |= n=@ud

18+ ++ count (unface

19+ |= [a=@ud b=@ud] ^- @ud

20+ ?- (eq a 0)

21+ %.y b

22+ %.n (count (dec a) b)

23+ (count n 1)

tests/golden/inline-unface-recursive/tokens.txtnew file+182

@@ -0,0 +1,182 @@

1+1:1 glyph ++

2+1:4 name weld2

3+1:10 glyph (

4+1:11 tight name unface

5+2:3 INDENT

6+2:3 glyph |=

7+2:6 glyph [

8+2:7 tight name xs

9+2:9 tight glyph =

10+2:10 tight glyph (

11+2:11 tight name list

12+2:16 tvar A

13+2:17 tight glyph )

14+2:19 name ys

15+2:21 tight glyph =

16+2:22 tight glyph (

17+2:23 tight name list

18+2:28 tvar A

19+2:29 tight glyph )

20+2:30 tight glyph ]

21+2:32 glyph ^-

22+2:35 glyph (

23+2:36 tight name list

24+2:41 tvar A

25+2:42 tight glyph )

26+3:5 INDENT

27+3:5 glyph ?-

28+3:8 name xs

29+4:7 INDENT

30+4:7 lit ~

31+4:9 name ys

32+5:7 NEWLINE

33+5:7 glyph [

34+5:8 tight name item

35+5:13 name rest

36+5:17 tight glyph ]

37+5:19 glyph [

38+5:20 tight name item

39+5:25 glyph (

40+5:26 tight name weld2

41+5:32 name rest

42+5:37 name ys

43+5:39 tight glyph )

44+5:40 tight glyph ]

45+6:1 DEDENT

46+6:1 DEDENT

47+6:1 DEDENT

48+6:1 NEWLINE

49+6:1 glyph ++

50+6:4 name joined

51+6:11 glyph (

52+6:12 tight name weld2

53+6:18 glyph ~[

54+6:20 tight lit 1

55+6:21 tight glyph ]

56+6:23 glyph ~[

57+6:25 tight lit 2

58+6:26 tight glyph ]

59+6:27 tight glyph )

60+7:1 NEWLINE

61+7:1 glyph ++

62+7:4 name even

63+7:9 glyph (

64+7:10 tight name unface

65+8:3 INDENT

66+8:3 glyph |=

67+8:6 name n

68+8:7 tight glyph =

69+8:8 tight aura @ud

70+8:12 glyph ^-

71+8:15 glyph ?

72+9:5 INDENT

73+9:5 glyph ?-

74+9:8 glyph (

75+9:9 tight name eq

76+9:12 name n

77+9:14 lit 0

78+9:15 tight glyph )

79+10:7 INDENT

80+10:7 lit %.y

81+10:11 lit %.y

82+11:7 NEWLINE

83+11:7 lit %.n

84+11:11 glyph (

85+11:12 tight name odd

86+11:16 glyph (

87+11:17 tight name dec

88+11:21 name n

89+11:22 tight glyph )

90+11:23 tight glyph )

91+12:1 DEDENT

92+12:1 DEDENT

93+12:1 DEDENT

94+12:1 NEWLINE

95+12:1 glyph ++

96+12:4 name odd

97+12:8 glyph (

98+12:9 tight name unface

99+13:3 INDENT

100+13:3 glyph |=

101+13:6 name n

102+13:7 tight glyph =

103+13:8 tight aura @ud

104+13:12 glyph ^-

105+13:15 glyph ?

106+14:5 INDENT

107+14:5 glyph ?-

108+14:8 glyph (

109+14:9 tight name eq

110+14:12 name n

111+14:14 lit 0

112+14:15 tight glyph )

113+15:7 INDENT

114+15:7 lit %.y

115+15:11 lit %.n

116+16:7 NEWLINE

117+16:7 lit %.n

118+16:11 glyph (

119+16:12 tight name even

120+16:17 glyph (

121+16:18 tight name dec

122+16:22 name n

123+16:23 tight glyph )

124+16:24 tight glyph )

125+17:1 DEDENT

126+17:1 DEDENT

127+17:1 DEDENT

128+17:1 NEWLINE

129+17:1 glyph ++

130+17:4 name outer

131+17:10 glyph |=

132+17:13 name n

133+17:14 tight glyph =

134+17:15 tight aura @ud

135+18:3 INDENT

136+18:3 glyph ++

137+18:6 name count

138+18:12 glyph (

139+18:13 tight name unface

140+19:5 INDENT

141+19:5 glyph |=

142+19:8 glyph [

143+19:9 tight name a

144+19:10 tight glyph =

145+19:11 tight aura @ud

146+19:15 name b

147+19:16 tight glyph =

148+19:17 tight aura @ud

149+19:20 tight glyph ]

150+19:22 glyph ^-

151+19:25 aura @ud

152+20:7 INDENT

153+20:7 glyph ?-

154+20:10 glyph (

155+20:11 tight name eq

156+20:14 name a

157+20:16 lit 0

158+20:17 tight glyph )

159+21:9 INDENT

160+21:9 lit %.y

161+21:13 name b

162+22:9 NEWLINE

163+22:9 lit %.n

164+22:13 glyph (

165+22:14 tight name count

166+22:20 glyph (

167+22:21 tight name dec

168+22:25 name a

169+22:26 tight glyph )

170+22:28 name b

171+22:29 tight glyph )

172+23:3 DEDENT

173+23:3 DEDENT

174+23:3 DEDENT

175+23:3 NEWLINE

176+23:3 glyph (

177+23:4 tight name count

178+23:10 name n

179+23:12 lit 1

180+23:13 tight glyph )

181+23:14 DEDENT

182+23:14 NEWLINE

tests/golden/inline-unface-recursive/tree.txtnew file+98

@@ -0,0 +1,98 @@

1+(module

2+ (value 1:1 weld2

3+ (group 1:10

4+ (call 1:11

5+ (wing 1:11 unface)

6+ (gate 2:3

7+ (cell 2:6

8+ (face 2:7 xs

9+ (apply 2:10 list (tvar 2:16 A)))

10+ (face 2:19 ys

11+ (apply 2:22 list (tvar 2:28 A))))

12+ (cast 2:32

13+ (apply 2:35 list (tvar 2:41 A))

14+ (body 3:5

15+ (branch 3:5

16+ (wing 3:8 xs)

17+ (arm 4:7 (lit 4:7 ~) (wing 4:9 ys))

18+ (arm 5:7

19+ (cell 5:7 (bind 5:8 item) (bind 5:13 rest))

20+ (tuple 5:19

21+ (wing 5:20 item)

22+ (group 5:25

23+ (call 5:26 (wing 5:26 weld2) (wing 5:32 rest) (wing 5:37 ys))))))))))))

24+ (value 6:1 joined

25+ (group 6:11

26+ (call 6:12

27+ (wing 6:12 weld2)

28+ (list 6:18 (lit 6:20 1))

29+ (list 6:23 (lit 6:25 2)))))

30+ (value 7:1 even

31+ (group 7:9

32+ (call 7:10

33+ (wing 7:10 unface)

34+ (gate 8:3

35+ (face 8:6 n (aura 8:8 @ud))

36+ (cast 8:12

37+ (flag 8:15)

38+ (body 9:5

39+ (branch 9:5

40+ (group 9:8

41+ (call 9:9 (wing 9:9 eq) (wing 9:12 n) (lit 9:14 0)))

42+ (arm 10:7 (lit 10:7 %.y) (lit 10:11 %.y))

43+ (arm 11:7

44+ (lit 11:7 %.n)

45+ (group 11:11

46+ (call 11:12

47+ (wing 11:12 odd)

48+ (group 11:16

49+ (call 11:17 (wing 11:17 dec) (wing 11:21 n)))))))))))))

50+ (value 12:1 odd

51+ (group 12:8

52+ (call 12:9

53+ (wing 12:9 unface)

54+ (gate 13:3

55+ (face 13:6 n (aura 13:8 @ud))

56+ (cast 13:12

57+ (flag 13:15)

58+ (body 14:5

59+ (branch 14:5

60+ (group 14:8

61+ (call 14:9 (wing 14:9 eq) (wing 14:12 n) (lit 14:14 0)))

62+ (arm 15:7 (lit 15:7 %.y) (lit 15:11 %.n))

63+ (arm 16:7

64+ (lit 16:7 %.n)

65+ (group 16:11

66+ (call 16:12

67+ (wing 16:12 even)

68+ (group 16:17

69+ (call 16:18 (wing 16:18 dec) (wing 16:22 n)))))))))))))

70+ (value 17:1 outer

71+ (gate 17:10

72+ (face 17:13 n (aura 17:15 @ud))

73+ (body 18:3

74+ (value 18:3 count

75+ (group 18:12

76+ (call 18:13

77+ (wing 18:13 unface)

78+ (gate 19:5

79+ (cell 19:8

80+ (face 19:9 a (aura 19:11 @ud))

81+ (face 19:15 b (aura 19:17 @ud)))

82+ (cast 19:22

83+ (aura 19:25 @ud)

84+ (body 20:7

85+ (branch 20:7

86+ (group 20:10

87+ (call 20:11 (wing 20:11 eq) (wing 20:14 a) (lit 20:16 0)))

88+ (arm 21:9 (lit 21:9 %.y) (wing 21:13 b))

89+ (arm 22:9

90+ (lit 22:9 %.n)

91+ (group 22:13

92+ (call 22:14

93+ (wing 22:14 count)

94+ (group 22:20

95+ (call 22:21 (wing 22:21 dec) (wing 22:25 a)))

96+ (wing 22:28 b)))))))))))

97+ (group 23:3

98+ (call 23:4 (wing 23:4 count) (wing 23:10 n) (lit 23:12 1)))))))

tests/golden/inline-unface-recursive/types.txtnew file+6

@@ -0,0 +1,6 @@

1+partial inference; module not checked

2+++ weld2: $-([(list A) (list A)] (list A))

3+++ joined: (list @ud)

4+++ even: $-(@ud ?)

5+++ odd: $-(@ud ?)

6+++ outer: $-(@ud @ud)

tests/golden/inline-unface-reserved-import/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A Jibb import face named unface is rejected.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-import/module-trees.txtnew file+6

@@ -0,0 +1,6 @@

1+/ui/lib.jibb

2+(module

3+ (value 1:1 identity

4+ (gate 1:13

5+ (face 1:16 x (aura 1:18 @t))

6+ (wing 1:21 x))))

tests/golden/inline-unface-reserved-import/modules.txtnew file+1

@@ -0,0 +1 @@

1+/ui/lib.jibb

tests/golden/inline-unface-reserved-import/modules/ui/lib.jibbnew file+1

@@ -0,0 +1 @@

1+++ identity |= x=@t x

tests/golden/inline-unface-reserved-import/source.jibbnew file+2

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

1+/= unface /ui/lib

2+++ okay "ok"

tests/golden/inline-unface-reserved-import/tokens.txtnew file+11

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

1+1:1 glyph /=

2+1:4 name unface

3+1:11 glyph /

4+1:12 tight knot ui

5+1:14 tight glyph /

6+1:15 tight knot lib

7+2:1 NEWLINE

8+2:1 glyph ++

9+2:4 name okay

10+2:9 str "ok"

11+2:13 NEWLINE

tests/golden/inline-unface-reserved-import/tree.txtnew file+3

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

1+(module

2+ (jibb 1:1 unface /ui/lib)

3+ (value 2:1 okay (str 2:9 "ok")))

tests/golden/inline-unface-reserved-import/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-reserved-local/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A local value named unface is rejected.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-local/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-local/source.jibbnew file+3

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

1+++ okay

2+ ++ unface |= x=@t x

3+ "ok"

tests/golden/inline-unface-reserved-local/tokens.txtnew file+14

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

1+1:1 glyph ++

2+1:4 name okay

3+2:3 INDENT

4+2:3 glyph ++

5+2:6 name unface

6+2:13 glyph |=

7+2:16 name x

8+2:17 tight glyph =

9+2:18 tight aura @t

10+2:21 name x

11+3:3 NEWLINE

12+3:3 str "ok"

13+3:7 DEDENT

14+3:7 NEWLINE

tests/golden/inline-unface-reserved-local/tree.txtnew file+8

@@ -0,0 +1,8 @@

1+(module

2+ (value 1:1 okay

3+ (body 2:3

4+ (value 2:3 unface

5+ (gate 2:13

6+ (face 2:16 x (aura 2:18 @t))

7+ (wing 2:21 x)))

8+ (str 3:3 "ok"))))

tests/golden/inline-unface-reserved-local/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-reserved-mold/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A mold named unface is rejected, even unused.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-mold/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-mold/source.jibbnew file+2

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

1++$ unface @t

2+++ okay "ok"

tests/golden/inline-unface-reserved-mold/tokens.txtnew file+8

@@ -0,0 +1,8 @@

1+1:1 glyph +$

2+1:4 name unface

3+1:11 aura @t

4+2:1 NEWLINE

5+2:1 glyph ++

6+2:4 name okay

7+2:9 str "ok"

8+2:13 NEWLINE

tests/golden/inline-unface-reserved-mold/tree.txtnew file+3

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

1+(module

2+ (mold 1:1 unface (aura 1:11 @t))

3+ (value 2:1 okay (str 2:9 "ok")))

tests/golden/inline-unface-reserved-mold/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-reserved-no-prelude/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: Without the prelude, the report names the reserved names.

3+expect: parses

4+expect-types: the report says the module has a reserved name

tests/golden/inline-unface-reserved-no-prelude/source.jibbnew file+2

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

1++$ unface @t

2+++ okay "ok"

tests/golden/inline-unface-reserved-no-prelude/tokens.txtnew file+8

@@ -0,0 +1,8 @@

1+1:1 glyph +$

2+1:4 name unface

3+1:11 aura @t

4+2:1 NEWLINE

5+2:1 glyph ++

6+2:4 name okay

7+2:9 str "ok"

8+2:13 NEWLINE

tests/golden/inline-unface-reserved-no-prelude/tree.txtnew file+3

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

1+(module

2+ (mold 1:1 unface (aura 1:11 @t))

3+ (value 2:1 okay (str 2:9 "ok")))

tests/golden/inline-unface-reserved-no-prelude/types.txtnew file+1

@@ -0,0 +1 @@

1+module has a reserved proj or unface name

tests/golden/inline-unface-reserved-pattern/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A branch pattern cannot bind unface.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-pattern/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-pattern/source.jibbnew file+3

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

1+++ okay |= x=[@t @p]

2+ ?- x

3+ [unface other] other

tests/golden/inline-unface-reserved-pattern/tokens.txtnew file+21

@@ -0,0 +1,21 @@

1+1:1 glyph ++

2+1:4 name okay

3+1:9 glyph |=

4+1:12 name x

5+1:13 tight glyph =

6+1:14 tight glyph [

7+1:15 tight aura @t

8+1:18 aura @p

9+1:20 tight glyph ]

10+2:3 INDENT

11+2:3 glyph ?-

12+2:6 name x

13+3:5 INDENT

14+3:5 glyph [

15+3:6 tight name unface

16+3:13 name other

17+3:18 tight glyph ]

18+3:20 name other

19+3:25 DEDENT

20+3:25 DEDENT

21+3:25 NEWLINE

tests/golden/inline-unface-reserved-pattern/tree.txtnew file+11

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

1+(module

2+ (value 1:1 okay

3+ (gate 1:9

4+ (face 1:12 x

5+ (cell 1:14 (aura 1:15 @t) (aura 1:18 @p)))

6+ (body 2:3

7+ (branch 2:3

8+ (wing 2:6 x)

9+ (arm 3:5

10+ (cell 3:5 (bind 3:6 unface) (bind 3:13 other))

11+ (wing 3:20 other)))))))

tests/golden/inline-unface-reserved-pattern/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-reserved-positive/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A field label, a tag and a longer name spelled with unface stay free, beside a normal unface call.

3+expect: parses

4+expect-types: a partial inference report

tests/golden/inline-unface-reserved-positive/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-positive/source.jibbnew file+6

@@ -0,0 +1,6 @@

1++$ action

2+ %unface

3+ %other

4+++ unfaced |= x=[unface=@t other=@p] unface.x

5+++ tag ^- action %unface

6+++ plain (unface unfaced)

tests/golden/inline-unface-reserved-positive/tokens.txtnew file+36

@@ -0,0 +1,36 @@

1+1:1 glyph +$

2+1:4 name action

3+2:3 INDENT

4+2:3 lit %unface

5+3:3 NEWLINE

6+3:3 lit %other

7+4:1 DEDENT

8+4:1 NEWLINE

9+4:1 glyph ++

10+4:4 name unfaced

11+4:12 glyph |=

12+4:15 name x

13+4:16 tight glyph =

14+4:17 tight glyph [

15+4:18 tight name unface

16+4:24 tight glyph =

17+4:25 tight aura @t

18+4:28 name other

19+4:33 tight glyph =

20+4:34 tight aura @p

21+4:36 tight glyph ]

22+4:38 wing unface.x

23+5:1 NEWLINE

24+5:1 glyph ++

25+5:4 name tag

26+5:8 glyph ^-

27+5:11 name action

28+5:18 lit %unface

29+6:1 NEWLINE

30+6:1 glyph ++

31+6:4 name plain

32+6:10 glyph (

33+6:11 tight name unface

34+6:18 name unfaced

35+6:25 tight glyph )

36+6:26 NEWLINE

tests/golden/inline-unface-reserved-positive/tree.txtnew file+15

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

1+(module

2+ (mold 1:1 action

3+ (union 2:3 (const 2:3 %unface) (const 3:3 %other)))

4+ (value 4:1 unfaced

5+ (gate 4:12

6+ (face 4:15 x

7+ (cell 4:17

8+ (face 4:18 unface (aura 4:25 @t))

9+ (face 4:28 other (aura 4:34 @p))))

10+ (wing 4:38 unface.x)))

11+ (value 5:1 tag

12+ (cast 5:8 (ref 5:11 action) (lit 5:18 %unface)))

13+ (value 6:1 plain

14+ (group 6:10

15+ (call 6:11 (wing 6:11 unface) (wing 6:18 unfaced)))))

tests/golden/inline-unface-reserved-positive/types.txtnew file+5

@@ -0,0 +1,5 @@

1+partial inference; module not checked

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

3+++ unfaced: $-([unface=@t other=@p] @t)

4+++ tag: action

5+++ plain: $-([@t @p] @t)

tests/golden/inline-unface-reserved-sample/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A gate sample cannot bind unface, alone or inside a cell.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-sample/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-sample/source.jibbnew file+1

@@ -0,0 +1 @@

1+++ okay |= [unface=@t other=@p] other

tests/golden/inline-unface-reserved-sample/tokens.txtnew file+13

@@ -0,0 +1,13 @@

1+1:1 glyph ++

2+1:4 name okay

3+1:9 glyph |=

4+1:12 glyph [

5+1:13 tight name unface

6+1:19 tight glyph =

7+1:20 tight aura @t

8+1:23 name other

9+1:28 tight glyph =

10+1:29 tight aura @p

11+1:31 tight glyph ]

12+1:33 name other

13+1:38 NEWLINE

tests/golden/inline-unface-reserved-sample/tree.txtnew file+7

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

1+(module

2+ (value 1:1 okay

3+ (gate 1:9

4+ (cell 1:12

5+ (face 1:13 unface (aura 1:20 @t))

6+ (face 1:23 other (aura 1:29 @p)))

7+ (wing 1:33 other))))

tests/golden/inline-unface-reserved-sample/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-reserved-value/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Modules: "`proj` and `unface` are reserved: no module can define, import or bind either, as a value or a mold"

2+tests: A top-level value named unface is rejected.

3+expect: parses

4+expect-types: a partial inference report: the module has conflicting names

tests/golden/inline-unface-reserved-value/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-reserved-value/source.jibbnew file+2

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

1+++ unface |= x=@t x

2+++ okay "ok"

tests/golden/inline-unface-reserved-value/tokens.txtnew file+12

@@ -0,0 +1,12 @@

1+1:1 glyph ++

2+1:4 name unface

3+1:11 glyph |=

4+1:14 name x

5+1:15 tight glyph =

6+1:16 tight aura @t

7+1:19 name x

8+2:1 NEWLINE

9+2:1 glyph ++

10+2:4 name okay

11+2:9 str "ok"

12+2:13 NEWLINE

tests/golden/inline-unface-reserved-value/tree.txtnew file+6

@@ -0,0 +1,6 @@

1+(module

2+ (value 1:1 unface

3+ (gate 1:11

4+ (face 1:14 x (aura 1:16 @t))

5+ (wing 1:19 x)))

6+ (value 2:1 okay (str 2:9 "ok")))

tests/golden/inline-unface-reserved-value/types.txtnew file+2

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

1+partial inference; module not checked

2+module has conflicting names

tests/golden/inline-unface-unknown/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "Like `proj`, it is an operation the checker handles by type, not a gate"

2+tests: unface on a type not yet known, a sample with no mold, would wait as wing access does; the partial checker reports it as unsupported, as it does field access, and a sample with a mold infers.

3+expect: parses

4+expect-types: a partial inference report: the untyped sample is unsupported

tests/golden/inline-unface-unknown/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-unknown/source.jibbnew file+3

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

1+++ later |= f (unface f)

2+++ get-label |= r label.r

3+++ known |= f=$-([a=@ud b=@ud] ?) (unface f)

tests/golden/inline-unface-unknown/tokens.txtnew file+36

@@ -0,0 +1,36 @@

1+1:1 glyph ++

2+1:4 name later

3+1:10 glyph |=

4+1:13 name f

5+1:15 glyph (

6+1:16 tight name unface

7+1:23 name f

8+1:24 tight glyph )

9+2:1 NEWLINE

10+2:1 glyph ++

11+2:4 name get-label

12+2:14 glyph |=

13+2:17 name r

14+2:19 wing label.r

15+3:1 NEWLINE

16+3:1 glyph ++

17+3:4 name known

18+3:10 glyph |=

19+3:13 name f

20+3:14 tight glyph =

21+3:15 tight glyph $-(

22+3:18 tight glyph [

23+3:19 tight name a

24+3:20 tight glyph =

25+3:21 tight aura @ud

26+3:25 name b

27+3:26 tight glyph =

28+3:27 tight aura @ud

29+3:30 tight glyph ]

30+3:32 glyph ?

31+3:33 tight glyph )

32+3:35 glyph (

33+3:36 tight name unface

34+3:43 name f

35+3:44 tight glyph )

36+3:45 NEWLINE

tests/golden/inline-unface-unknown/tree.txtnew file+18

@@ -0,0 +1,18 @@

1+(module

2+ (value 1:1 later

3+ (gate 1:10

4+ (bind 1:13 f)

5+ (group 1:15

6+ (call 1:16 (wing 1:16 unface) (wing 1:23 f)))))

7+ (value 2:1 get-label

8+ (gate 2:14 (bind 2:17 r) (wing 2:19 label.r)))

9+ (value 3:1 known

10+ (gate 3:10

11+ (face 3:13 f

12+ (fn 3:15

13+ (cell 3:18

14+ (face 3:19 a (aura 3:21 @ud))

15+ (face 3:25 b (aura 3:27 @ud)))

16+ (flag 3:32)))

17+ (group 3:35

18+ (call 3:36 (wing 3:36 unface) (wing 3:43 f))))))

tests/golden/inline-unface-unknown/types.txtnew file+4

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

1+partial inference; module not checked

2+++ later: unface on a type not yet known is not supported by partial inference

3+++ get-label: field is not available to partial inference

4+++ known: $-($-([a=@ud b=@ud] ?) $-([@ud @ud] ?))

tests/golden/inline-unface-value-bad/about.txtnew file+4

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

1+source: docs/spec/grammar.md, Expressions, Unface: "Like `proj`, it is an operation the checker handles by type, not a gate"

2+tests: unface written where a value goes, alone or as a gate's argument, is an error that suggests a lambda; the lambda itself hits the partial checker's gap for a sample whose type the call fixes, and a typed sample infers.

3+expect: parses

4+expect-types: a partial inference report: the bare uses are errors at the name, and the untyped lambda is unsupported

tests/golden/inline-unface-value-bad/modules.txtnew file+1

@@ -0,0 +1 @@

1+# Use source-backed prelude.

tests/golden/inline-unface-value-bad/source.jibbnew file+6

@@ -0,0 +1,6 @@

1+++ lt-a |= [a=@ud b=@ud] (gth b a)

2+++ gates ~[lt-a]

3+++ alias unface

4+++ mapped (turn gates unface)

5+++ wrapped (turn gates |=(g (unface g)))

6+++ typed (turn gates |=(g=$-([a=@ud b=@ud] ?) (unface g)))

tests/golden/inline-unface-value-bad/tokens.txtnew file+75

@@ -0,0 +1,75 @@

1+1:1 glyph ++

2+1:4 name lt-a

3+1:9 glyph |=

4+1:12 glyph [

5+1:13 tight name a

6+1:14 tight glyph =

7+1:15 tight aura @ud

8+1:19 name b

9+1:20 tight glyph =

10+1:21 tight aura @ud

11+1:24 tight glyph ]

12+1:26 glyph (

13+1:27 tight name gth

14+1:31 name b

15+1:33 name a

16+1:34 tight glyph )

17+2:1 NEWLINE

18+2:1 glyph ++

19+2:4 name gates

20+2:10 glyph ~[

21+2:12 tight name lt-a

22+2:16 tight glyph ]

23+3:1 NEWLINE

24+3:1 glyph ++

25+3:4 name alias

26+3:10 name unface

27+4:1 NEWLINE

28+4:1 glyph ++

29+4:4 name mapped

30+4:11 glyph (

31+4:12 tight name turn

32+4:17 name gates

33+4:23 name unface

34+4:29 tight glyph )

35+5:1 NEWLINE

36+5:1 glyph ++

37+5:4 name wrapped

38+5:12 glyph (

39+5:13 tight name turn

40+5:18 name gates

41+5:24 glyph |=(

42+5:27 tight name g

43+5:29 glyph (

44+5:30 tight name unface

45+5:37 name g

46+5:38 tight glyph )

47+5:39 tight glyph )

48+5:40 tight glyph )

49+6:1 NEWLINE

50+6:1 glyph ++

51+6:4 name typed

52+6:10 glyph (

53+6:11 tight name turn

54+6:16 name gates

55+6:22 glyph |=(

56+6:25 tight name g

57+6:26 tight glyph =

58+6:27 tight glyph $-(

59+6:30 tight glyph [

60+6:31 tight name a

61+6:32 tight glyph =

62+6:33 tight aura @ud

63+6:37 name b

64+6:38 tight glyph =

65+6:39 tight aura @ud

66+6:42 tight glyph ]

67+6:44 glyph ?

68+6:45 tight glyph )

69+6:47 glyph (

70+6:48 tight name unface

71+6:55 name g

72+6:56 tight glyph )

73+6:57 tight glyph )

74+6:58 tight glyph )

75+6:59 NEWLINE

tests/golden/inline-unface-value-bad/tree.txtnew file+37

@@ -0,0 +1,37 @@

1+(module

2+ (value 1:1 lt-a

3+ (gate 1:9

4+ (cell 1:12

5+ (face 1:13 a (aura 1:15 @ud))

6+ (face 1:19 b (aura 1:21 @ud)))

7+ (group 1:26

8+ (call 1:27 (wing 1:27 gth) (wing 1:31 b) (wing 1:33 a)))))

9+ (value 2:1 gates

10+ (list 2:10 (wing 2:12 lt-a)))

11+ (value 3:1 alias (wing 3:10 unface))

12+ (value 4:1 mapped

13+ (group 4:11

14+ (call 4:12 (wing 4:12 turn) (wing 4:17 gates) (wing 4:23 unface))))

15+ (value 5:1 wrapped

16+ (group 5:12

17+ (call 5:13

18+ (wing 5:13 turn)

19+ (wing 5:18 gates)

20+ (gate-wide 5:24

21+ (bind 5:27 g)

22+ (group 5:29

23+ (call 5:30 (wing 5:30 unface) (wing 5:37 g)))))))

24+ (value 6:1 typed

25+ (group 6:10

26+ (call 6:11

27+ (wing 6:11 turn)

28+ (wing 6:16 gates)

29+ (gate-wide 6:22

30+ (face 6:25 g

31+ (fn 6:27

32+ (cell 6:30

33+ (face 6:31 a (aura 6:33 @ud))

34+ (face 6:37 b (aura 6:39 @ud)))

35+ (flag 6:44)))

36+ (group 6:47

37+ (call 6:48 (wing 6:48 unface) (wing 6:55 g))))))))

tests/golden/inline-unface-value-bad/types.txtnew file+13

@@ -0,0 +1,13 @@

1+partial inference; module not checked

2+++ lt-a: $-([a=@ud b=@ud] ?)

3+++ gates: (list $-([a=@ud b=@ud] ?))

4+++ alias: unface is not a value; write |=(g (unface g))

5+/tests/golden/inline-unface-value-bad/source.jibb:3:10: unface used as a value

6+++ alias unface

7+ ^

8+++ mapped: unface is not a value; write |=(g (unface g))

9+/tests/golden/inline-unface-value-bad/source.jibb:4:23: unface used as a value

10+++ mapped (turn gates unface)

11+ ^

12+++ wrapped: unface on a type not yet known is not supported by partial inference

13+++ typed: (list $-([@ud @ud] ?))