surface

Documentation

Overview

Package surface is Rune's named layer: the lexer, parser, named AST, the pretty-printer (core -> named surface), and name resolution (named surface -> locally-nameless core).

Names live here and only here. Resolution is the only "elaboration" in Phase 0: it sends bound identifiers to de Bruijn indices and free identifiers to definition references (content hashes). There is no type elaboration in Phase 0.

Index

• Variables
• func DebugCore(t core.Tm) string
• func FreeIdents(e Exp) []string
• func Pretty(t core.Tm) string
• func PrettyNat(t core.Tm, refNames map[core.Hash]string, zero, succ core.Hash) string
• func PrettyWith(t core.Tm, refNames map[core.Hash]string) string
• func SpineOf(e Exp) (Exp, []Exp)
• type BuiltinNat
• type CaseClause
• type Ctor
• type DataDef
• type Def
  • func ParseFile(src string) ([]Def, error)
• type EAnn
• type EApp
• type ECase
• type ECast
• type EEq
• type EHole
• type ELam
• type ELet
• type EPi
• type EProp
• type ERefl
• type ESubst
• type EUniv
• type EVar
• type Exp
  • func ParseExpr(src string) (Exp, error)
  • func ParseExprNat(src, zero, succ string) (Exp, error)
• type Item
  • func ParseProgram(src string) ([]Item, error)
• type Resolver
  • func (r *Resolver) ResolveExp(e Exp) (core.Tm, error)

Variables

var ErrIncomplete = errors.New("incomplete input")

ErrIncomplete marks a parse that ran out of input mid-form (an unterminated is/seq block, or a binder/let awaiting more tokens). The REPL distinguishes it from a hard syntax error to decide between a continuation prompt and an error message.

Functions

func DebugCore

func DebugCore(t core.Tm) string

DebugCore renders a core term in explicit locally-nameless form: bound variables as their de Bruijn index (#n), references as @hash, binders unnamed (λ, Π). It is the REPL's :core debug view and deliberately is not a sentence of the surface grammar.

func FreeIdents

func FreeIdents(e Exp) []string

FreeIdents returns the free identifiers of e (those not bound by an enclosing lambda, Pi, or let), de-duplicated. The CLI uses this to build the definition dependency graph that drives SCC-ordered hashing.

func Pretty

func Pretty(t core.Tm) string

Pretty turns a core term back into named surface syntax. This is the inverse direction of the three-representation split: the core is locally nameless, and exactly the layer you read gets names back.

Bound variables are named from the Scope.Name hints carried for display, freshened on shadowing so the printed names never capture. Because names are reconstructed, parse . resolve . pretty . resolve is the identity on core up to the de Bruijn form — which is what the round-trip property asserts.

func PrettyNat

func PrettyNat(t core.Tm, refNames map[core.Hash]string, zero, succ core.Hash) string

PrettyNat is PrettyWith with a registered `builtin nat` binding: saturated applications succ (… (succ zero)) print as numerals.

func PrettyWith

func PrettyWith(t core.Tm, refNames map[core.Hash]string) string

PrettyWith is Pretty with a map from definition hashes to names, used to render Ref nodes as the names the user wrote. An unknown reference prints as #<hash>.

func SpineOf

func SpineOf(e Exp) (Exp, []Exp)

SpineOf splits an application into its head and argument list (explicit arguments only; an implicit argument in a former spine disqualifies it).

Types

type BuiltinNat

type BuiltinNat struct {
	TyName string
	Zero   string
	Succ   string
}

BuiltinNat is a builtin-binding declaration (ergonomics rung 2):

builtin nat Nat zero succ

It registers which data type numeric literals mean: from its position to the end of the file, a numeral n parses as the n-fold application of Succ to Zero. The declaration is surface state only — it desugars every literal at parse time and leaves no trace of its own in the core or the store.

type CaseClause

type CaseClause struct {
	Ctor    string
	Binders []string
	IHs     []string
	Body    Exp
}

CaseClause is one clause of a case expression:

| ctor b1 b2 with ih1 -> body

Binders match the constructor's argument positions in order; IHs names the induction hypotheses the eliminator provides for the recursive arguments (in argument order), and may be shorter than the recursive-argument count — missing ones are bound fresh and unused.

type Ctor

type Ctor struct {
	Name string
	Ty   Exp
}

Ctor is one constructor of a datatype declaration: Name : Ty.

type DataDef

type DataDef struct {
	Name  string
	Ty    Exp
	Ctors []Ctor
}

DataDef is a datatype declaration (Phase 4):

data Name : Ty is C1 : T1 | C2 : T2 | … end

type Def

type Def struct {
	Name string
	Ty   Exp
	Body Exp
}

Def is one top-level definition: Name (: Ty)? = Body. The file is a flat list of these (no modules in Phase 0). Ty is nil when omitted.

func ParseFile

func ParseFile(src string) ([]Def, error)

type EAnn

type EAnn struct {
	Term Exp
	Ty   Exp
}

EAnn is a type annotation (Term : Ty).

type EApp

type EApp struct {
	Fn   Exp
	Arg  Exp
	Icit core.Icit // Impl when written f {e}
}

EApp is application Fn Arg, left-associative.

type ECase

type ECase struct {
	Scrut   Exp
	Clauses []CaseClause
}

ECase is `case Scrut of (| Clause)+ end` (GRAMMAR §5.6): sugar for one saturated application of the scrutinee type's eliminator. It elaborates in checking position only — the expected type supplies the motive — and leaves no trace in the core.

type ECast

type ECast struct{}

ECast is the cast head, `cast`, saturated with four arguments: cast A B p x.

type EEq

type EEq struct{}

EEq is the equality former head, `Eq`. It is applied like a function and must be saturated with three arguments: Eq T l r.

type EHole

type EHole struct{}

EHole is `_`: a hole for elaboration to solve with a fresh metavariable (Phase 2). Holes never survive elaboration; the untyped resolver rejects them.

type ELam

type ELam struct {
	Param string
	Icit  core.Icit // Impl when written fn {x : A}
	Qty   core.Qty  // 0 or 1 when annotated (fn (0 x : A) …); ω otherwise
	Dom   Exp
	Body  Exp
}

ELam is one parameter of a lambda: fn (Param : Dom) is Body end. The parser desugars a curried fn (x : A) (y : B) is e end into nested ELam. Dom is the binder's domain annotation; resolution scope-checks it and then discards it, since the Phase-0 core lambda is un-annotated (see GRAMMAR.md §6). Dom is never nil.

type ELet

type ELet struct {
	Name string
	Ty   Exp
	Val  Exp
	Body Exp
}

ELet is let Name (: Ty)? = Val in Body. Ty is nil when the annotation is absent.

type EPi

type EPi struct {
	Param string
	Icit  core.Icit // Impl when written {x : A} -> B
	Qty   core.Qty  // 0 or 1 when annotated ((0 x : A) -> B); ω otherwise
	Dom   Exp
	Cod   Exp
}

EPi is a dependent function type (Param : Dom) -> Cod. A non-dependent arrow A -> B parses to EPi with Param "_".

type EProp

type EProp struct{}

EProp is the universe of propositions, Prop (Phase 3).

type ERefl

type ERefl struct{}

ERefl is the reflexivity proof head, `refl`. Used bare (in checking position) or applied to one argument.

type ESubst

type ESubst struct{}

ESubst is the transport head, `subst`, saturated with six arguments: subst A x y p P px — from p : Eq A x y and px : P x, conclude P y.

type EUniv

type EUniv struct {
	Lvl int
}

EUniv is a universe: `U` is U_0, `U1`…`U9` the higher levels (Phase 6).

type EVar

type EVar struct {
	Name string
}

EVar is an identifier occurrence: either a bound variable or a free reference to a top-level definition. Resolution decides which.

type Exp

type Exp interface {
	// contains filtered or unexported methods
}

Exp is a named surface expression. Like core.Tm it is a sealed interface matched by type switch; the marker keeps the constructor set closed.

func ParseExpr

func ParseExpr(src string) (Exp, error)

ParseExpr parses a single surface expression from src. Used by the REPL, the property harness, and for ad-hoc terms.

func ParseExprNat

func ParseExprNat(src, zero, succ string) (Exp, error)

ParseExprNat is ParseExpr with a registered `builtin nat` binding, so numerals in the expression expand. The REPL uses it once a session has the binding.

type Item

type Item interface {
	// contains filtered or unexported methods
}

Item is one top-level program item: a Def, a DataDef, or a BuiltinNat.

func ParseProgram

func ParseProgram(src string) ([]Item, error)

ParseFile parses a flat list of top-level definitions (GRAMMAR.md §3). Each definition self-delimits with its own `end`, so no layout rule is needed; newlines between definitions are insignificant. ParseProgram parses a file of top-level items: definitions and datatype declarations, in order.

type Resolver

type Resolver struct {
	Refs map[string]core.Hash
}

Resolver carries the only context name resolution needs in Phase 0: a map from top-level definition names to their content hashes. Resolution is the sole "elaboration" in Phase 0 — it sends bound identifiers to de Bruijn indices and free identifiers to definition references. There is NO type elaboration here.

func (*Resolver) ResolveExp

func (r *Resolver) ResolveExp(e Exp) (core.Tm, error)

ResolveExp resolves a closed-or-reference-only surface expression into core. Bound variables become de Bruijn indices; free identifiers are looked up in Refs and become content-hash references.