Surface — nix-effects

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