core

package
v3.6.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jun 13, 2026 License: MIT Imports: 4 Imported by: 0

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

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

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 FibInfo 

type FibInfo interface {
	FibRoleOf(Hash) FibRole
}

FibInfo gives the evaluator the fibrant-builtin roles of stored hashes (v3). store.Store implements it. Nil means no fibrant builtins.

type FibRole 

type FibRole byte

FibRole classifies a stored hash's role in the fibrant builtin group (v3): the two-level layer's members, builtin definitions like the quotient kit. See store/fib.go for the group, its types, and the computation/postulate line. 

const (
	// FRoleNone: not a fibrant builtin.
	FRoleNone FibRole = iota
	// FRoleUF is the fibrant universe UF : U1.
	FRoleUF
	// FRoleEl decodes a fibrant code to its outer type: El : UF -> U.
	FRoleEl
	// FRoleFib embeds a small outer type as fibrant: fib : U -> UF.
	FRoleFib
	// FRolePiF closes UF under Pi.
	FRolePiF
	// FRolePathF is the inner identity type former.
	FRolePathF
	// FRolePrefl is the inner reflexivity preflF.
	FRolePrefl
	// FRoleJ is inner path induction pathJ (computes on preflF).
	FRoleJ
	// FRolePathU is the type of inner paths between fibrant types.
	FRolePathU
	// FRoleUrefl is ureflU : (A : UF) -> pathU A A.
	FRoleUrefl
	// FRoleUa is POSTULATED univalence (an iso yields a pathU).
	FRoleUa
	// FRoleCastU is transport along a pathU (computes on ureflU and ua).
	FRoleCastU
)

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
	// Quot, when non-nil, supplies quotient-builtin roles for the quotient
	// ι-rules (v2): qlift/qind compute when their scrutinee is qin-headed.
	Quot QuotInfo
	// Fib, when non-nil, supplies fibrant-builtin roles for the two-level
	// ι-rules (v3): El decodes, pathJ computes on preflF, castU computes on
	// ureflU and through ua.
	Fib FibInfo
}

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 QuotInfo 

type QuotInfo interface {
	QuotRoleOf(Hash) QuotRole
}

QuotInfo gives the evaluator the quotient-builtin roles of stored hashes (v2). store.Store implements it. Nil means no quotient builtins (the ι-rules never fire).

type QuotRole 

type QuotRole byte

QuotRole classifies a stored hash's role in the quotient builtin group (v2). The quotient formers are BUILTIN DEFINITIONS, not new core syntax: permanently neutral heads (like datatype constructors) whose eliminators compute by the quotient ι-rules below. See store/quot.go for the group and its types. 

const (
	// QRoleNone: not a quotient builtin.
	QRoleNone QuotRole = iota
	// QRoleQuot is the type former Quot : (A : U) -> (A -> A -> Prop) -> U.
	QRoleQuot
	// QRoleIn is the point constructor qin : … -> A -> Quot A R.
	QRoleIn
	// QRoleSound is the path introduction qsound : … R a b -> Eq (Quot A R) (qin … a) (qin … b).
	QRoleSound
	// QRoleLift is the non-dependent eliminator qlift : … (f : A -> B) -> (resp : …) -> Quot A R -> B.
	QRoleLift
	// QRoleInd is the Prop-motive induction principle qind : … -> (q : Quot A R) -> P q.
	QRoleInd
)

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
	NonDep bool
	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).

NonDep, when true, records that Cod IGNORES its argument: the codomain term never mentions the binder (set by Eval, the strict-language stand-in for a lazy argument thunk). Callers that need only the result type of an application may then skip evaluating the argument — without this, checking an n-deep application chain evaluates each argument subterm from scratch at every node, O(n²) in the chain depth. False is always safe; it is never part of identity (quote and conversion ignore it).

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.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.