# Surface


Surface specifications define constructor tags and handlers. HOAS
elaboration consults the attached registry only for nodes that carry
`_surfaceRegistry`, so existing HOAS terms continue through the built-in
dispatcher.

## `collectImplicitMetas`

_Collect surface-created implicit metavariable terms from an elaborated overlay term._

```
ElabTm -> [SurfaceMeta]
```

## `collectSurfaceMetas`

_Collect explicitly marked overlay metavariable terms from an elaborated surface result._

```
ElabTm -> [SurfaceMeta]
```

## `containsImplicitMeta`

_Predicate for unresolved surface-created implicit metavariable terms._

```
ElabTm -> Bool
```

## `containsSurfaceMeta`

_Predicate for any overlay metavariable term inside an elaborated surface result._

```
ElabTm -> Bool
```

## `defineOrnament`

_Package a surface-to-target mapping with section and forget morphisms for elaborator derivation._

```
{ source, target, mapping?, section?, forget? } -> SurfaceOrnament
```

## `defineSurface`

_Define a named surface language with constructor metadata and elaboration handlers._

```
{ name, description?, scope?, constructors } -> SurfaceSpec
```

## `deriveElaborator`

_Derive an elaborator entry point from a surface specification and optional ornament section. Expected type and source position are threaded into surface handlers._

```
{ surface, ornament? } -> { registry, elaborate }
```

## `deriveParser`

_Derive a parser shell for a surface specification._

```
{ surface, parse? } -> { parse }
```

## `derivePrinter`

_Derive a small printer for surface AST nodes._

```
{ surface, render? } -> { print }
```

## `elaborate`

_Elaborate one surface term, optionally checking it against an expected HOAS type and source position._

```
{ surface, term, expectedType?, position?, ornament? } -> Tm | Error
```

## `finalizeSurfaceElab`

_Return a structured unsolved-implicit error when elaboration leaves surface implicit metas unresolved._

```
{ result, state?, term?, surface?, position? } -> ElabTm | Error
```

## `framework`

_Convenience bundle for the surface-language definition, ornament, elaboration, parser, and printer APIs._

## `handlerContext`

_Build the argument record passed to surface elaboration handlers, adding expected type, source position, and implicit-meta helpers._

```
{ h, depth, lower, hoas, fx, ... } -> HandlerArgs
```

## `implicitMeta`

_Allocate an implicit metavariable using the Phase 6 meta-context shape and return both overlay value and term forms._

```
{ type?, state?, position?, surface?, label? } -> { id, value, term, state }
```

## `parse`

_Parse one input value with a derived parser shell or supplied parser._

```
{ surface, input, parse? } -> Hoas
```

## `prelude`

_Minimal surface prelude with List and an implicit-argument nil proof fixture._

## `print`

_Print one surface AST node with a derived or supplied renderer._

```
{ surface, term, render? } -> String
```

## `surfaceTerm`

_Construct one term from a surface specification._

```
SurfaceSpec -> String -> Attrs -> Hoas
```

## `toy`

_Toy boolean surface used as an end-to-end elaboration fixture._

## `unsolvedImplicitError`

_Build the structured surface error for unresolved implicit metavariables._

```
{ metas, term?, surface?, position? } -> Error
```

## `withSurfaceContext`

_Attach root expected-type and position metadata to a surface AST node before elaboration._

```
{ term, expectedType?, position? } -> Hoas
```

## Sub-namespaces

- [`registry`](/nix-effects/type-checker/surface/registry)

## Source

- [`src/tc/surface/define-ornament.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/define-ornament.nix)
- [`src/tc/surface/define-surface.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/define-surface.nix)
- [`src/tc/surface/derive-elaborator.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/derive-elaborator.nix)
- [`src/tc/surface/derive-parser.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/derive-parser.nix)
- [`src/tc/surface/derive-printer.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/derive-printer.nix)
- [`src/tc/surface/framework.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/framework.nix)
- [`src/tc/surface/handler-context.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/handler-context.nix)
- [`src/tc/surface/implicit.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/implicit.nix)
- [`src/tc/surface/prelude.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/prelude.nix)
- [`src/tc/surface/registry.nix`](https://github.com/kleisli-io/nix-effects/blob/main/src/tc/surface/registry.nix)