eval

Documentation

Index

• func DebugValue(v Value) string
• func EvalNBE(t ast.Term) ast.Term
• func NeutralEqual(n1, n2 Neutral) bool
• func Normalize(t ast.Term) ast.Term
• func NormalizeNBE(t ast.Term) string
• func PrettyNeutral(n Neutral) string
• func PrettyValue(v Value) string
• func Reify(v Value) ast.Term
• func SprintNeutral(n Neutral) string
• func SprintValue(v Value) string
• func ValueEqual(v1, v2 Value) bool
• type Closure
• type Env
  • func (e *Env) Extend(v Value) *Env
  • func (e *Env) Lookup(ix int) Value
• type Head
• type Neutral
• type VGlobal
• type VLam
• type VNeutral
• type VPair
• type VPi
• type VSigma
• type VSort
• type Value
  • func Apply(fun Value, arg Value) Value
  • func Eval(env *Env, t ast.Term) Value
  • func Fst(v Value) Value
  • func Reflect(neu Neutral) Value
  • func Snd(v Value) Value

Functions

func DebugValue

func DebugValue(v Value) string

DebugValue provides detailed debug information about a Value.

func EvalNBE

func EvalNBE(t ast.Term) ast.Term

EvalNBE is a convenience function that evaluates and reifies a term using NbE.

func NeutralEqual

func NeutralEqual(n1, n2 Neutral) bool

NeutralEqual compares two Neutrals for structural equality.

func Normalize

func Normalize(t ast.Term) ast.Term

Normalize reduces a term to weak head normal form using beta-reduction and projections.

func NormalizeNBE

func NormalizeNBE(t ast.Term) string

NormalizeNBE normalizes a term using NbE and returns its string representation. This function provides compatibility with existing test expectations.

func PrettyNeutral

func PrettyNeutral(n Neutral) string

PrettyNeutral converts a Neutral to a stable string representation for testing.

func PrettyValue

func PrettyValue(v Value) string

PrettyValue converts a Value to a stable string representation for testing. This ensures deterministic output for golden tests.

func Reify

func Reify(v Value) ast.Term

Reify converts a Value back to an ast.Term.

func SprintNeutral

func SprintNeutral(n Neutral) string

SprintNeutral returns a string representation of a Neutral for debugging and testing.

func SprintValue

func SprintValue(v Value) string

SprintValue returns a string representation of a Value for debugging and testing.

func ValueEqual

func ValueEqual(v1, v2 Value) bool

ValueEqual compares two Values for structural equality (useful for testing).

Types

type Closure

type Closure struct {
	Env  *Env
	Term ast.Term
}

Closure captures an environment and a term for lazy evaluation.

type Env

type Env struct {
	Bindings []Value
}

Env represents an evaluation environment mapping de Bruijn indices to Values.

func (*Env) Extend

func (e *Env) Extend(v Value) *Env

Extend adds a new binding to the front of the environment.

func (*Env) Lookup

func (e *Env) Lookup(ix int) Value

Lookup retrieves a value by de Bruijn index.

type Head

type Head struct {
	Var  int    // de Bruijn index
	Glob string // global name
}

Head represents the head of a neutral term.

type Neutral

type Neutral struct {
	Head Head
	Sp   []Value
}

Neutral represents stuck terms with a head and spine of arguments.

type VGlobal

type VGlobal struct{ Name string }

VGlobal represents global constants.

type VLam

type VLam struct{ Body *Closure }

VLam represents lambda closures.

type VNeutral

type VNeutral struct{ N Neutral }

VNeutral represents neutral terms (stuck computations).

type VPair

type VPair struct{ Fst, Snd Value }

VPair represents pairs in WHNF.

type VPi

type VPi struct {
	A Value
	B *Closure
}

VPi represents Pi type closures (optional for now).

type VSigma

type VSigma struct {
	A Value
	B *Closure
}

VSigma represents Sigma type closures (optional for now).

type VSort

type VSort struct{ Level int }

VSort represents universe sorts.

type Value

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

Value is the semantic domain for NbE.

func Apply

func Apply(fun Value, arg Value) Value

Apply performs function application in the semantic domain.

func Eval

func Eval(env *Env, t ast.Term) Value

Eval evaluates a term in an environment to weak head normal form.

func Fst

func Fst(v Value) Value

Fst performs first projection in the semantic domain.

func Reflect

func Reflect(neu Neutral) Value

Reflect converts a Neutral to a Value (identity function, but useful for API completeness).

func Snd

func Snd(v Value) Value

Snd performs second projection in the semantic domain.