core

Documentation

Overview

Package core holds Rune's locally-nameless core: the elaborated term language (Tm), the glued NbE value domain (Val, shape only in Phase 0), and structural Merkle hashing.

Three representations, one rule (see CLAUDE.md): the surface is named, the core is locally nameless, and the pretty-printer turns core back into named surface for display. Bound variables are de Bruijn indices; references to top-level definitions are content hashes (Ref), never names.

Phase 0 implements only the term shapes, name resolution's target, and hashing. Type checking, normalization, conversion, and type-directed elaboration are Phase 1 and MUST NOT appear here.

Index

• type Ann
• type App
• type Cast
• type CtorSig
• type DataInfo
• type ElimSig
• type Env
  • func (e Env) Extend(v Val) Env
• type Eq
• type EqStratum
• type Globals
• type Hash
  • func HashTerm(t Tm) Hash
  • func (h Hash) Short() string
  • func (h Hash) String() string
• type Icit
• type Lam
• type Let
• type Machine
  • func NewMachine(g Globals) *Machine
  • func (m *Machine) Apply(fn, arg Val) Val
  • func (m *Machine) ApplyIcit(fn, arg Val, icit Icit) Val
  • func (m *Machine) Conv(lvl int, a, b Val) bool
  • func (m *Machine) DepList() []Hash
  • func (m *Machine) Eval(env Env, t Tm) Val
  • func (m *Machine) EvalCast(a, b, p, x Val) Val
  • func (m *Machine) EvalEq(ty, l, r Val) Val
  • func (m *Machine) EvalSubst(a, x, y, prf, pmot, px Val) Val
  • func (m *Machine) Force(v Val) Val
  • func (m *Machine) Normalize(t Tm) Tm
  • func (m *Machine) NormalizeUnfold(t Tm) Tm
  • func (m *Machine) Quote(lvl int, v Val) Tm
  • func (m *Machine) QuoteUnfold(lvl int, v Val) Tm
  • func (m *Machine) Sub(lvl int, a, b Val) bool
• type Meta
• type MetaSolver
• type NApp
• type NCast
• type NMeta
• type NRef
• type NSubst
• type NVar
• type Neutral
• type Pi
• type Prop
• type Qty
• type Ref
• type Refl
• type Scope
• type Subst
• type Tm
• type Univ
• type VEq
• type VLam
• type VNeu
• type VPi
• type VProp
• type VRefl
• type VU
• type Val
  • func VVar(l int) Val
• type Var

Types

type Ann

type Ann struct {
	Term Tm
	Ty   Tm
}

Ann is a type annotation (Term : Ty). Phase 0 keeps annotations in the core so that the surface round-trips; Phase 1 elaboration will consume them.

type App

type App struct {
	Fn   Tm
	Arg  Tm
	Icit Icit
}

App is an application Fn Arg, at the given plicity.

type Cast

type Cast struct {
	A Tm
	B Tm
	P Tm
	X Tm
}

Cast transports a term along a type equality: Cast A B P X : B, given A B : U, P : Eq U A B, X : A. Cast computes on the structure of A and B and never inspects P (proof irrelevance).

type CtorSig

type CtorSig struct {
	Arity int
	Rec   []bool
}

CtorSig describes one constructor's arguments: its arity (after the data type's parameters) and which of those arguments are recursive occurrences of the datatype (the positions that get induction hypotheses).

type DataInfo

type DataInfo interface {
	CtorOf(Hash) (data Hash, idx int, ok bool)
	ElimOf(Hash) (ElimSig, bool)
}

DataInfo gives the evaluator the datatype roles of stored hashes (Phase 4). store.Store implements it. Nil means no datatypes (ι never fires).

type ElimSig

type ElimSig struct {
	Data      Hash
	NumParams int
	Ctors     []CtorSig
}

ElimSig describes an eliminator: the datatype it eliminates, the number of datatype parameters, and the constructor signatures in declaration order. The eliminator's argument layout is

elim p1..pk motive case1..casen scrutinee

and the ι-rule fires when the scrutinee forces to a saturated constructor.

type Env

type Env []Val

Env is the evaluation environment: index 0 is the innermost binder's value, matching Var's de Bruijn indices.

func (Env) Extend

func (e Env) Extend(v Val) Env

Extend pushes v as the new innermost value.

type Eq

type Eq struct {
	Ty Tm
	L  Tm
	R  Tm
}

Eq is the observational equality type former: Eq Ty L R, the proposition that L and R are equal elements of Ty. It computes on the structure of Ty (Eq over a function type unfolds to pointwise equality — funext is a REDUCTION, not an axiom). Lives in Prop.

type EqStratum

type EqStratum interface {
	// EvalEq computes the value of Eq ty l r, applying the stratum's
	// type-directed reductions (e.g. funext: Eq over a Pi unfolds pointwise).
	EvalEq(m *Machine, ty, l, r Val) Val
	// EvalCast computes cast a b p x, never inspecting p.
	EvalCast(m *Machine, a, b, p, x Val) Val
	// EvalSubst computes subst a x y prf P px, never inspecting prf.
	EvalSubst(m *Machine, a, x, y, prf, pmot, px Val) Val
}

EqStratum is the EQUALITY STRATUM's reduction hooks (Phase 3). The conversion checker and evaluator call these when they reach an equality former; the one v1 implementation is equality.Observational (Pujet–Tabareau). Nil means the formers are stuck (pre-Phase-3 behavior).

type Globals

type Globals interface {
	TypeOf(Hash) (Tm, bool)
	Unfold(Hash) (Tm, bool)
}

Globals is eval/conversion's view of the definition store. store.Store satisfies it. TypeOf is pure — a referenced definition's type is part of the content hash any referencing term already carries, so reading it logs nothing. Unfold is the body gateway; every Machine access to it is logged.

type Hash

type Hash [32]byte

Hash is a content hash: the Merkle digest of a piece of elaborated core.

Hashing uses BLAKE3 (goforge.dev/blake3sum); blake3.New(32, nil) is an unkeyed 256-bit streaming hasher implementing hash.Hash. The digest width and algorithm are an implementation detail behind this type — changing them changes every content hash, which is what the preimage tag (hashFormatVersion) versions.

func HashTerm

func HashTerm(t Tm) Hash

HashTerm computes the structural Merkle hash of a core term.

THE STANDING RULE (CLAUDE.md): hashing operates structurally on the core term and MUST NEVER call eval, normalize, or a future conversion routine. A definition's identity is its SYNTAX, never its meaning modulo conversion. Because the core is de Bruijn, alpha-equivalent terms are literally equal here and therefore hash equal; Scope.Name is a pretty-printing hint and is deliberately not fed to the digest.

func (Hash) Short

func (h Hash) Short() string

Short renders the first 12 hex characters, for human-facing listings.

func (Hash) String

func (h Hash) String() string

String renders the hash as lowercase hex.

type Icit

type Icit byte

Icit is the plicity of a binder or application: explicit (the default) or implicit (Phase 2; surface syntax {x : A}). Implicit arguments are inserted by elaboration, so the core is always fully applied and plicity is part of a term's identity (it is hashed).

const (
	// Expl marks an explicit binder or argument.
	Expl Icit = iota
	// Impl marks an implicit binder or argument.
	Impl
)

type Lam

type Lam struct {
	Icit Icit
	Qty  Qty
	Body Scope
}

Lam is a lambda abstraction \x -> Body. Body is a Scope binding the parameter.

type Let

type Let struct {
	Ty   Tm // optional; nil if the let had no annotation
	Val  Tm
	Body Scope
}

Let is let x = Val in Body, with an optional annotation Ty (nil when absent). Body is a Scope binding x. The bound value is in-band: it lives in the term and is part of the term's content hash (it is not a global definition, so it is not reached through store.Unfold).

type Machine

type Machine struct {
	G    Globals
	Deps map[Hash]struct{}
	// Metas, when non-nil, resolves metavariable solutions (Phase 2). It is set
	// only during elaboration; pure core runs (the cached checker judgment, REPL
	// normalization) operate on zonked, meta-free terms and leave it nil.
	Metas MetaSolver
	// EqS, when non-nil, supplies the equality stratum's reduction rules.
	EqS EqStratum
	// Data, when non-nil, supplies datatype roles for ι-reduction.
	Data DataInfo
}

Machine carries one checking/evaluation run: the store view and the write-only dependency log (the ConvM accumulator of the proof-cache semantics). A Machine is created per judgment run — its Deps, read after the run, are exactly the definitional dependency set U the certificate is keyed on. Machines and the values they produce must not be shared across runs, or a memoized forced thunk would swallow a later run's dependency.

func NewMachine

func NewMachine(g Globals) *Machine

NewMachine returns a Machine over g with an empty dependency log.

func (*Machine) Apply

func (m *Machine) Apply(fn, arg Val) Val

Apply applies fn to an explicit arg (the common external entry point).

func (*Machine) ApplyIcit

func (m *Machine) ApplyIcit(fn, arg Val, icit Icit) Val

ApplyIcit applies fn to arg at the given plicity.

func (*Machine) Conv

func (m *Machine) Conv(lvl int, a, b Val) bool

Conv reports whether a and b are definitionally equal (βδη) at level lvl.

func (*Machine) DepList

func (m *Machine) DepList() []Hash

DepList returns the logged dependency set as an unordered slice.

func (*Machine) Eval

func (m *Machine) Eval(env Env, t Tm) Val

Eval evaluates t in env. Precondition: t is well-scoped in env (every Var index is < len(env)) and well-typed; eval of ill-typed core may panic (the checker runs first).

func (*Machine) EvalCast

func (m *Machine) EvalCast(a, b, p, x Val) Val

EvalCast applies the equality stratum's cast reduction, or leaves it stuck.

func (*Machine) EvalEq

func (m *Machine) EvalEq(ty, l, r Val) Val

EvalEq applies the equality stratum's Eq reduction, or leaves the type stuck.

func (*Machine) EvalSubst

func (m *Machine) EvalSubst(a, x, y, prf, pmot, px Val) Val

EvalSubst applies the equality stratum's transport, or leaves it stuck.

func (*Machine) Force

func (m *Machine) Force(v Val) Val

Force unfolds a glued neutral to its delta-reduced value, repeatedly, logging each unfolded definition (forcing the thunk is store.Unfold). A flexible neutral whose meta is unsolved is returned as-is (its Unfold yields itself). Non-neutrals and neutrals with nothing to unfold are returned as-is.

func (*Machine) Normalize

func (m *Machine) Normalize(t Tm) Tm

Normalize is quote ∘ eval on a closed term: β-normal, references kept folded.

func (*Machine) NormalizeUnfold

func (m *Machine) NormalizeUnfold(t Tm) Tm

NormalizeUnfold is Normalize with full δ-unfolding of definition references.

func (*Machine) Quote

func (m *Machine) Quote(lvl int, v Val) Tm

Quote reads v back into a term. lvl is the number of binders in scope: a free variable at level l quotes to index lvl-1-l.

func (*Machine) QuoteUnfold

func (m *Machine) QuoteUnfold(lvl int, v Val) Tm

QuoteUnfold is Quote after forcing every glued unfolding: full βδ-normal form. Each forced definition is logged, like any force. It terminates on the acyclic stores Phase 1 admits (recursive definitions arrive with Phase-4 totality).

func (*Machine) Sub

func (m *Machine) Sub(lvl int, a, b Val) bool

Sub reports a <: b — definitional conversion extended with cumulativity: Prop <: U, and function types are covariant in their codomain (domains stay invariant, which is sound and keeps the relation decidable without antisymmetry games). Used where a Prop-valued thing is supplied at a U-valued expectation (e.g. Prop-valued eliminator motives).

type Meta

type Meta struct {
	ID int
}

Meta is an unsolved metavariable, identified within one elaboration run. It is ELABORATION-INTERNAL: a meta must never reach the store or the hash boundary — HashTerm panics on it, and the session asserts elaborated definitions are meta-free (zonked) before storing.

type MetaSolver

type MetaSolver interface {
	Solution(int) (Val, bool)
}

MetaSolver resolves a metavariable to its solution value, if solved.

type NApp

type NApp struct {
	Fn   Neutral
	Arg  Val
	Icit Icit
}

NApp is a neutral applied to an argument value at the given plicity.

type NCast

type NCast struct {
	A, B, P, X Val
}

NCast is a stuck cast: transport along an equality whose endpoint types are not yet concrete enough to reduce. P is carried for quotation only — conversion compares A, B, and X and SKIPS P (proof irrelevance).

type NMeta

type NMeta struct {
	ID int
}

NMeta is a stuck metavariable head (Phase 2, elaboration-internal). A neutral headed by an NMeta is FLEXIBLE: solving the meta can wake it. The Machine's Metas solver is consulted when forcing.

type NRef

type NRef struct {
	Hash Hash
}

NRef is a stuck reference to a top-level definition (one whose body has not been unfolded on the fast path).

type NSubst

type NSubst struct {
	A, X, Y, Prf, P, Px Val
}

NSubst is a stuck Leibniz transport: its equality's endpoints are not yet convertible. Prf is carried for quotation only; conversion skips it.

type NVar

type NVar struct {
	Lvl int
}

NVar is a free variable, identified by de Bruijn LEVEL (not index) so the head is stable as the value is reused under deeper binders.

type Neutral

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

Neutral is the un-unfolded spine of a stuck computation: a head (a free variable at a de Bruijn level, or a definition reference) under a stack of eliminators.

type Pi

type Pi struct {
	Icit Icit
	Qty  Qty
	Dom  Tm
	Cod  Scope
}

Pi is the dependent function type (x : Dom) -> Cod (explicit) or {x : Dom} -> Cod (implicit). Cod is a Scope: it binds one variable (the argument), reachable as Var{0} inside it.

type Prop

type Prop struct{}

Prop is the universe of propositions (Phase 3, the observational equality stratum): proof-irrelevant, with Prop : U. Equality types live here.

type Qty

type Qty byte

Qty is a binder's usage annotation, drawn from the 0/1/ω semiring the quantity stratum supplies (Phase 5). The zero value is QMany (ω, unrestricted) so unannotated binders cost nothing. The 0-fragment is the erasure boundary codegen reads. Quantities are part of a Pi type's identity and are hashed.

const (
	// QMany is ω: unrestricted use (the default).
	QMany Qty = iota
	// QZero marks an erased binder: usable in types, absent at runtime.
	QZero
	// QOne marks a linear binder: used exactly once.
	QOne
)

type Ref

type Ref struct {
	Hash Hash
}

Ref is a reference to a top-level definition, named by the content hash of that definition's elaborated core (a Pitts constant). References are by hash, never by name, so the core carries no nominal dependency.

type Refl

type Refl struct {
	Tm Tm
}

Refl is the reflexivity proof: Refl x : Eq A x x. Proofs are definitionally irrelevant; Refl's payload exists for type inference, not for computation.

type Scope

type Scope struct {
	Name string
	Body Tm
}

Scope is the body of a binder. Under locally-nameless representation a Scope is just a term with one additional bound variable in scope (reachable as Var{0}).

Name is a pretty-printing hint ONLY. It is NOT part of a term's identity and is never hashed: alpha-equivalent terms are de Bruijn-equal and therefore hash equal. The pretty-printer may freshen Name to avoid capture.

type Subst

type Subst struct {
	A   Tm
	X   Tm
	Y   Tm
	Prf Tm
	P   Tm
	Px  Tm
}

Subst is Leibniz transport along an equality (Phase 4's induction workhorse): Subst A X Y Prf P Px : P Y, given X Y : A, Prf : Eq A X Y, P : A -> s, Px : P X. It computes to Px when X ≡ Y (in particular at refl) and never inspects Prf.

type Tm

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

Tm is an elaborated core term. It is a sealed interface: the unexported marker method isTm makes the constructor set closed, so every consumer matches by type switch and the compiler flags an unhandled case. This is the one AST encoding used throughout Rune; do not mix in another.

type Univ

type Univ struct {
	Lvl int
}

Univ is a universe U_Lvl in the predicative hierarchy (Phase 6): U_i : U_{i+1}, with cumulativity U_i <: U_j for i ≤ j supplied by Sub. The surface writes `U` for U_0 and `U1`, `U2`, … for higher levels. The type-in-type stance is gone.

type VEq

type VEq struct {
	Ty, L, R Val
}

VEq is a STUCK observational equality type: the stratum's EvalEq could not reduce it further (Ty is not a function type, and not enough structure is known). Values of a VEq type are proofs and are definitionally irrelevant.

type VLam

type VLam struct {
	Name string
	Icit Icit
	Qty  Qty
	Body func(Val) Val
}

VLam is a lambda value, carrying its meaning as a Go closure. Name is a display hint only, like VPi.Name.

type VNeu

type VNeu struct {
	Spine  Neutral
	Unfold func() Val
}

VNeu is a neutral value: a variable or definition reference stuck under eliminators it cannot yet reduce.

Spine is the un-unfolded neutral (the fast-path representative). Unfold is the lazy unfolding: forcing it is store.Unfold and is where the proof-cache dependency is logged. Phase 1 supplies real thunks; Phase 0 fixes the shape only.

type VPi

type VPi struct {
	Name string
	Icit Icit
	Qty  Qty
	Dom  Val
	Cod  func(Val) Val
}

VPi is a dependent function type value (x : Dom) -> Cod. Cod is a Go closure: the NbE meaning function. Name is a pretty-printing hint for the binder, like Scope.Name — never part of identity, never hashed (quote drops it into a Scope).

type VProp

type VProp struct{}

VProp is the universe of propositions as a value (Phase 3).

type VRefl

type VRefl struct {
	V Val
}

VRefl is the reflexivity proof as a value. Its payload is carried for quotation only; conversion never inspects it (proof irrelevance).

type VU

type VU struct {
	Lvl int
}

VU is a universe as a value, at its level.

type Val

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

Val is the glued NbE value domain. SHAPE ONLY in Phase 0: the constructors are fixed here so the Phase-1 evaluator and quoter have a target, but eval and quote are NOT implemented.

"Glued" (after smalltt): a neutral value carries both its un-unfolded spine AND a lazy unfolding. Conversion takes a fast syntactic path over spines and forces the lazy unfolding only on mismatch, so errors print near the source the user wrote.

The coincidence that earns its keep (see ref_docs/rune-proof-cache-semantics.md): forcing a neutral's lazy unfolding is the SAME operation as store.Unfold. The proof-cache dependency log hooks exactly there — the fast path compares spines and logs nothing; forcing logs the unfolded definition's hash. The instrumentation rides on the machinery built for speed. This is on purpose; keep them coincident.

func VVar

func VVar(l int) Val

VVar is the fresh-variable value at de Bruijn level l, used by quote and conversion to go under binders.

type Var

type Var struct {
	Idx int
}

Var is a bound variable, a de Bruijn index. Index 0 is the nearest enclosing binder. Var never names a top-level definition; that is Ref.