eval

Apr 24, 2026

Changes in this version

+ const DefaultCacheSize

+ func EvalNBECached(t ast.Term, cache *Cache) ast.Term

+ func NormalizeWithCache(t ast.Term) ast.Term

+ func ReifyCached(v Value, cache *Cache) ast.Term

+ func WithCache[T any](f func(*Cache) T) T

+ type Cache struct

+ EvalHits int64

+ EvalMisses int64

+ MaxSize int

+ func NewCache(maxSize int) *Cache

+ func NewDefaultCache() *Cache

+ func (c *Cache) LookupEval(t ast.Term, env *Env) (Value, bool)

+ func (c *Cache) Reset()

+ func (c *Cache) Stats() map[string]int64

+ func (c *Cache) StoreEval(t ast.Term, env *Env, val Value)

type VLam

+ Binder string

type VPi

+ Binder string

type VSigma

+ Binder string

type Value

+ func ApplyCached(fun Value, arg Value, cache *Cache) Value

+ func EvalCached(env *Env, t ast.Term, cache *Cache) Value

Jan 5, 2026

Changes in this version

+ func AlphaEq(a, b ast.Term) bool

+ type BoundarySpec struct

+ AtOneVal Value

+ AtZeroVal Value

+ type BoundaryVal struct

+ AtOne Value

+ AtZero Value

+ type PathConstructorInfo struct

+ Boundaries []BoundarySpec

+ Level int

+ Name string

+ NumArgs int

type RecursorInfo

+ IsHIT bool

+ PathCtors []PathConstructorInfo

+ type VHITPathCtor struct

+ Args []Value

+ Boundaries []BoundaryVal

+ CtorName string

+ HITName string

+ IArgs []Value

Dec 8, 2025

Changes in this version

+ func IsFaceFalse(f FaceValue) bool

+ func IsFaceTrue(f FaceValue) bool

+ func ReifyCubicalAt(level int, ilevel int, v Value) ast.Term

type ConstructorInfo

+ RecursiveArgElims map[int]string

+ type FaceValue interface

+ type IClosure struct

+ Env *Env

+ IEnv *IEnv

+ Term ast.Term

+ type IEnv struct

+ Bindings []Value

+ func EmptyIEnv() *IEnv

+ func (ie *IEnv) Extend(v Value) *IEnv

+ func (ie *IEnv) ILen() int

+ func (ie *IEnv) Lookup(ix int) Value

+ type VComp struct

+ A *IClosure

+ Base Value

+ Phi FaceValue

+ Tube *IClosure

+ type VFaceAnd struct

+ Left FaceValue

+ Right FaceValue

+ type VFaceBot struct

+ type VFaceEq struct

+ ILevel int

+ IsOne bool

+ type VFaceOr struct

+ Left FaceValue

+ Right FaceValue

+ type VFaceTop struct

+ type VFill struct

+ A *IClosure

+ Base Value

+ Phi FaceValue

+ Tube *IClosure

+ type VGlue struct

+ A Value

+ System []VGlueBranch

+ type VGlueBranch struct

+ Equiv Value

+ Phi FaceValue

+ T Value

+ type VGlueElem struct

+ Base Value

+ System []VGlueElemBranch

+ type VGlueElemBranch struct

+ Phi FaceValue

+ Term Value

+ type VHComp struct

+ A Value

+ Base Value

+ Phi FaceValue

+ Tube *IClosure

+ type VI0 struct

+ type VI1 struct

+ type VIVar struct

+ Level int

+ type VPartial struct

+ A Value

+ Phi FaceValue

+ type VPath struct

+ A Value

+ X Value

+ Y Value

+ type VPathLam struct

+ Body *IClosure

+ type VPathP struct

+ A *IClosure

+ X Value

+ Y Value

+ type VSystem struct

+ Branches []VSystemBranch

+ type VSystemBranch struct

+ Phi FaceValue

+ Term Value

+ type VTransport struct

+ A *IClosure

+ E Value

+ type VUA struct

+ A Value

+ B Value

+ Equiv Value

+ type VUABeta struct

+ Arg Value

+ Equiv Value

+ type VUnglue struct

+ G Value

+ Ty Value

type Value

+ func EvalComp(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value

+ func EvalCubical(env *Env, ienv *IEnv, t ast.Term) Value

+ func EvalFill(aClosure *IClosure, phi FaceValue, tubeClosure *IClosure, base Value) Value

+ func EvalGlue(a Value, branches []VGlueBranch) Value

+ func EvalGlueElem(branches []VGlueElemBranch, base Value) Value

+ func EvalHComp(a Value, phi FaceValue, tubeClosure *IClosure, base Value) Value

+ func EvalTransport(aClosure *IClosure, e Value) Value

+ func EvalUA(a, b, equiv Value) Value

+ func EvalUABeta(equiv, arg Value) Value

+ func EvalUnglue(ty Value, g Value) Value

+ func MakeNeutralGlobal(name string) Value

+ func PathApply(p Value, r Value) Value

+ func UAPathApply(ua VUA, r Value) Value

Dec 7, 2025

Changes in this version

type ConstructorInfo

+ IndexArgPositions map[int][]int

Dec 6, 2025

Changes in this version

+ var DebugMode = os.Getenv("HOTTGO_DEBUG") == "1"

+ func ClearRecursorRegistry()

+ func RegisterRecursor(info *RecursorInfo)

+ type ConstructorInfo struct

+ Name string

+ NumArgs int

+ RecursiveIdx []int

+ type RecursorInfo struct

+ Ctors []ConstructorInfo

+ ElimName string

+ IndName string

+ NumCases int

+ NumIndices int

+ NumParams int

+ func LookupRecursor(elimName string) *RecursorInfo

+ type VId struct

+ A Value

+ X Value

+ Y Value

+ type VRefl struct

+ A Value

+ X Value

Sep 14, 2025

Changes in this version

+ func DebugValue(v Value) string

+ func EvalNBE(t ast.Term) ast.Term

+ func NeutralEqual(n1, n2 Neutral) bool

+ 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 struct

+ Env *Env

+ Term ast.Term

+ type Env struct

+ Bindings []Value

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

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

+ type Head struct

+ Glob string

+ Var int

+ type Neutral struct

+ Head Head

+ Sp []Value

+ type VGlobal struct

+ Name string

+ type VLam struct

+ Body *Closure

+ type VNeutral struct

+ N Neutral

+ type VPair struct

+ Fst Value

+ Snd Value

+ type VPi struct

+ A Value

+ B *Closure

+ type VSigma struct

+ A Value

+ B *Closure

+ type VSort struct

+ Level int

+ type Value interface

+ 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

Sep 13, 2025

Changes in this version

+ func Normalize(t ast.Term) ast.Term