b71609d · jibb · git.iko.soy

git.iko.soy/jibb

Add unface, which strips every face from a type

`(unface e)` is a reserved operation the checker handles by type, like `proj`, as Montelot decided for S1 on 2026-11-03: e's type with every face removed, through cells, a gate's sample and product, and the arguments of the built-in collections, the prelude's unit included. Unions and recursive molds go by name or exact cases, so they are kept whole and a gate over `msg` still takes a `msg`. Unbound variables stay, so the faces they are bound to later are kept. The proj reservation becomes one set, `+reserved-name`, checked in the same places, so `unface` cannot be defined, imported, bound as a sample or pattern, or used as a mold. Written as a value it is an error that suggests `|=(g (unface g))`, and it takes exactly one argument. On a bare type variable the partial checker reports it as unsupported, as it does field access. A `++` whose body is `(unface |= ...)` is still a gate for self-recursion, recursive groups and the report. Lowering is not implemented, so only the core-language row says it lowers to e. The spec gets an Expressions bullet, the reserved names in Modules, the waiting rule and a lowering row; compiler.md and the library's notes describe the checker's part. The new inline-unface-* golden cases show what now types and each new error. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01U4FzmThon6Q3x1uL8yUKEY

commitb71609dc6d83abb7768373ceefb5a2c05f8a51af authorClaude <noreply@anthropic.com> dateTue 3 Nov 2026, 03:02 (9 hours ago) parent16c08c8

109 files changed+1959−54

compare with master

unifiedsplit

docs/compiler.md+4−2

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

132132

133133`+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.

134134

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.

136136

137137A 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.

138138

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

187187

188188Public 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.

189189

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.

191193

192194## The tree

193195

docs/spec/core-language.md+1

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

8383| `/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 |

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

8585| `(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 |

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

8788| `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 |

8889| `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`)

4646- **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.

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

4848- **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.

4950- **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`.

5051- **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.

5152- **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

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

100101

101102- `+$ 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.

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

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

105106- 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

146147- `|=%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.

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

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

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

151152

152153```jibb

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

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

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

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

46624662::

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+::

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

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

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

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

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

49684976 ~

49694977::

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+::

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

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

49725009++ itype-gate-free-forms

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

73677404 ^- isample-result

73687405 ?- -.s

73697406 %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))))

73717408 [%| "sample shadows a name"]

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

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

73747411 %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))))

73767413 [%| "sample shadows a name"]

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

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

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

74407477 |-

74417478 ?~ ds &

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

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

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

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

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

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

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

74647501 |-

74657502 ?~ locals &

74667503 =/ n=term name.i.locals

7467− ?: =(n %proj) |

7504+ ?: (reserved-name n) |

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

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

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

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

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

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

81468183 ?~ 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)))))

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

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

81508187 =/ left=iresult

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

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

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

81838220 ?~ 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))))

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

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

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

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

82888325 ^- (unit ienv)

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

82908327 ?: ?=(%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)))) ~

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

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

82948331 `env

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

92789315 [%& typ.instance state.instance]

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

92809317 ?~ scheme

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

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

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

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

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

92859323 [%& typ.inst state.inst]

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

92879325 [%& typ.instance state.instance]

9288− %group $(e inner.e)

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"]]]]

9329+ $(e inner.e)

92899330 %change

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

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

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

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

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

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

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

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

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

94349476 ==

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

98199861 ^- iresult

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

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

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

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

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

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

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

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

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

99039946::

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

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

9948+::

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

99059960++ explicit-proj-call

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

99079962 ^- ?

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

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

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

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

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

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

9914− ?~ prelude.state &

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

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

9966+::

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

9968+::

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

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

991610011++ infer-proj-source

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

991810013 ^- iresult

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

1031910414 ?~ pats [%& ~]

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

1032110416 =/ 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))))

1032310418 [%| 'pattern shadows a name']

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

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

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

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

1086210957 =. gate-defs.state ~

1086310958 ?. ?=(%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

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

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

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

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

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

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

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

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

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

1088810987 =/ body=expr

1088910988 ?- -.gate

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

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

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

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

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

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

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

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

1089911000::

1090011001++ dependency-root

1090111002 |= names=(list term)

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

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

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

1100511106:: 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=?]

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

1100811109++ seed-gate-group

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

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

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

1101211113 =/ d=def i.ds

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

11014− =/ gate=expr val.d

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

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

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

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

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

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

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

1102911132 * !!

1103011133 ==

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1229212397 ==

1229312398 [n $(imports t.imports)]

1229412399::

12295−++ reserved-proj-sample

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.

12405+++ reserved-name

12406+ |= n=term

12407+ ^- ?

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

12409+++ reserved-sample

1229612410 |= sam=sample

1229712411 ^- ?

1229812412 ?- -.sam

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

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

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

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

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

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

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

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

1230312417 * |

1230412418 ==

12305−++ reserved-proj-pattern

12419+++ reserved-pattern

1230612420 |= p=pattern

1230712421 ^- ?

1230812422 ?- -.p

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

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

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

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

1231112425 * |

1231212426 ==

12313−++ reserved-proj-def

12427+++ reserved-def

1231412428 |= d=def

1231512429 ^- ?

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

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

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

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

1231812432 |

12319−++ reserved-proj-expr

12433+++ reserved-expr

1232012434 |= e=expr

1232112435 ^- ?

1232212436 ?- -.e

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

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

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

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

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

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

1232612440 %pair $(e val.e)

1232712441 %unit $(e val.e)

1232812442 %group $(e inner.e)

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

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

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

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

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

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

1233212446 %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))

1233412448 %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)))))

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

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

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

1233712451 * |

1233812452 ==

1233912453::

12340−++ module-has-reserved-proj

12454+++ module-has-reserved

1234112455 |= mod=module

1234212456 ^- ?

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

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

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

1234612460 =/ 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))

1234812462::

1234912463++ module-scope-valid

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

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

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

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

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

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

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

1235712471 ?. %+ levy imported

1235812472 |= n=term

1235912473 &((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 @@

1304213156 ^- ?

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

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

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

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

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

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

1304813162::

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

1307413188 =/ clashes=(list term)

1307513189 %+ skip names

1307613190 |= n=term

13077− ?| =(n %proj)

13191+ ?| (reserved-name n)

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

1307913193 ==

1308013194 ?~ clashes ~

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

1384913963 =/ action=term %poke

1385013964 =/ ordinary=(list def) ds

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

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

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

1385313967 =/ outer=(list term)

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

1385513969 =/ clashes=(list term)

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

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

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

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

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

15623− 'module has reserved proj name'

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

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

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

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

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

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

1569815812 =. head-evidence.initial heads

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

1570015814 =/ result=iresult

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

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

1570215816 (infer-recursive-gate d env initial)

1570315817 (infer-fragment val.d env initial)

1570415818 ?: ?=(%| -.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] ?))