🥮 mooncakes.io

    #Terms

    The HOL term language. Terms form a simply-typed lambda calculus with constants, represented using the locally nameless convention.

    Depends on: foundation (for Subst), types (for Type, TypeSubst)

    #The Term Enum

    ///|
    enum Term {
      FVar(String, Type) // free (named) variable with its type
      BVar(Int) // bound variable (de Bruijn index)
      Const(String, Type) // declared constant (e.g., "=")
      App(Term, Term) // function application
      Abs(Term, Term) // lambda abstraction
    }

    #Why Locally Nameless?

    Bound variables use de Bruijn indices (BVar(0) = innermost binder), while free variables use names (FVar("x", ty)). This means alpha-equivalent terms have identical representations:

    // \x. x  and  \y. y  both become  Abs(_, BVar(0))

    No alpha-conversion is needed during comparison -- structural equality suffices.

    #Constant Table

    The global signature of constants is stored in a mutable table. The only primitive constant is polymorphic equality:

    = : 'a -> 'a -> bool

    All other connectives (==>, /\, forall, etc.) are defined on top of equality (see the logic package). New constants are registered via @terms.Term::new_const (which also returns the new constant term) or Kernel::defineConst.

    #Building Terms

    ///|
    test "terms: free variables and constants" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let bool_ty = @types.bool_ty()

      // Free variables carry a name and a type
      let p = @terms.mk_var("p", bool_ty)
      guard p is FVar(name, _) else { fail("expected FVar") }
      assert_eq(name, "p")

      // The primitive constant: = : 'a -> 'a -> bool
      let a = @types.mk_var("'a")
      let eq_ty = @types.mk_fun(a, @types.mk_fun(a, bool_ty))
      let eq_const = @terms.Term::mk_const("=", eq_ty)
      assert_true(eq_const is Const(_, _))
    }

    #Lambda Abstraction

    mk_abs(x, body) replaces free occurrences of x in body with BVar(0), producing a locally nameless abstraction. dest_abs reverses the process, picking a fresh name to avoid capture:

    ///|
    test "terms: abstraction roundtrip and type inference" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let a = @types.mk_var("'a")
      let x = @terms.mk_var("x", a)

      // Build the identity: \x. x
      let id_fn = @terms.Term::mk_abs(x, x)
      assert_true(id_fn is Abs(_, _))
      assert_eq(@types.Type::pprint(id_fn.type_of()), "'a --> 'a")

      // Destruct it back
      let (bv, body) = id_fn.dest_abs()
      assert_eq(@terms.Term::pprint(body), @terms.Term::pprint(bv))
    }

    #Equations

    mk_eq(l, r) builds the equation l = r, checking that both sides have the same type. Internally it instantiates the polymorphic = constant:

    ///|
    test "terms: equations" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let a = @types.mk_var("'a")
      let x = @terms.mk_var("x", a)
      let y = @terms.mk_var("y", a)

      let eq = @terms.Term::mk_eq(x, y)
      assert_true(@terms.Term::is_eq(eq))
      let (lhs, rhs) = @terms.Term::dest_eq(eq)
      assert_true(lhs == x)
      assert_true(rhs == y)
    }

    #Alpha-Convertibility

    Because bound variables are de Bruijn indices, alpha-equivalent terms are structurally identical. aconv checks this:

    ///|
    test "terms: alpha-convertibility" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let a = @types.mk_var("'a")
      let x = @terms.mk_var("x", a)
      let y = @terms.mk_var("y", a)

      // \x. x  and  \y. y  are alpha-convertible
      assert_true(@terms.Term::mk_abs(x, x).aconv(@terms.Term::mk_abs(y, y)))
      // But x and y (as free variables) are NOT
      assert_false(x.aconv(y))
    }

    #Substitution

    There are three kinds of substitution:

    OperationWhat it does
    tm.inst(sigma)Apply a type substitution to every type annotation in tm
    tm.subst(sigma)Replace free term variables according to sigma
    ty.subst(sigma)Replace type variables in a type (see types package)

    Type instantiation is how polymorphic constants get specialized:

    ///|
    test "terms: type instantiation" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let a = @types.mk_var("'a")
      let bool_ty = @types.bool_ty()
      let eq_ty = @types.mk_fun(a, @types.mk_fun(a, bool_ty))
      let eq = @terms.Term::mk_const("=", eq_ty)

      // Instantiate 'a := bool
      let sigma : @types.TypeSubst = Subst(pairs=[(a, bool_ty)])
      let eq_bool = eq.inst(sigma)
      let expected = @types.mk_fun(bool_ty, @types.mk_fun(bool_ty, bool_ty))
      assert_true(eq_bool.type_of() == expected)
    }

    #Term Matching

    pattern.match_term(observation) finds both a term substitution and a type substitution such that applying them to pattern yields observation. Used by tactics and rewriting:

    ///|
    test "terms: pattern matching" {
      @types.Type::reset_table()
      @terms.Term::reset_table()
      let a = @types.mk_var("'a")
      let bool_ty = @types.bool_ty()
      let x = @terms.mk_var("x", a)
      let p = @terms.mk_var("p", bool_ty)

      // Match x:'a against p:bool => { x := p } and { 'a := bool }
      let (tm_s, ty_s) = x.match_term(p)
      assert_eq([..tm_s].length(), 1)
      assert_eq([..ty_s].length(), 1)
    }

    #Type Aliases

    AliasExpands to
    TermSubstSubst[Term, Term]
    TermMatchResult(TermSubst, TypeSubst)

    TermMatchResult

    source

    The result of pattern matching a term: a pair of a term substitution and a type substitution that, when applied to the pattern, yield the observation.

    TermSubst

    source

    A substitution mapping terms to terms, used to replace free variables in a term.

    Term

    source
    pub enum Term {
      FVar(String, 
    Type    )
      BVar(Int)
      Const(String, 
    Type    )
      App(Term, Term)
      Abs(Term, Term)
    } derive(Compare, Eq, 
    Debug    )

    HOL term in locally nameless representation: free variables are named, bound variables use de Bruijn indices, and constants carry their (possibly polymorphic) type.
    impl Show for Term

    Term::aconv

    source
    fn Term::aconv(self : Term, rhs : Term) -> Bool

    Test alpha-equivalence: two terms are alpha-convertible if they are identical up to renaming of bound variables. Free variables and constants must match exactly.

    Term::compare

    source
    fn Term::compare(Term, Term) -> Int

    Term::curry_eq

    source
    fn Term::curry_eq(self : Term) -> Term

    Build the partially applied equality (=) : ty -> ty -> bool instantiated at self's type, then apply it to self, yielding a term of type ty -> bool. Used by derived equality rules.

    Term::dest_abs

    source
    fn Term::dest_abs(self : Term) -> (Term, Term)

    Decompose an abstraction Abs(x, body) back into (x', body') where x' is a fresh free variable and body' has every BVar(0) (and any residual free occurrence of x) replaced by x'.

    Because the locally nameless encoding erases the original binder name, dest_abs must invent a fresh name that does not clash with any variable already present in the body. Starting from the annotation name it appends primes (') until the name is unused, guaranteeing that round-tripping mk_abs / dest_abs never accidentally captures a free variable.

    This is the inverse of mk_abs: for any free variable x and term m, mk_abs(x, m).dest_abs() yields a pair (x', m') that is alpha-equivalent to (x, m).

    Aborts if the term is not an abstraction.

    Term::dest_eq

    source
    fn Term::dest_eq(tm : Term) -> (Term, Term) raise

    Decompose an equation into its left- and right-hand sides, aborting if the term is not an equation.

    Term::equal

    source
    fn Term::equal(Term, Term) -> Bool

    Term::inst

    source

    Apply a type substitution to every type annotation in the term, specializing polymorphic constants and variables to concrete types.

    Term::is_bool

    source
    fn Term::is_bool(self : Term) -> Bool

    Test whether the term has boolean type.

    Term::is_eq

    source
    fn Term::is_eq(tm : Term) -> Bool

    Test whether the term is an equation of the form l = r.

    Term::match_term

    source

    First-order pattern matching: find substitutions (sigma, tau) such that self.subst(sigma).inst(tau) == ob.

    self is the pattern and ob is the observation (concrete term). Free variables in the pattern act as match variables — each one is bound to the corresponding sub-term of ob. Constants must match exactly (name and compatible type). Bound variables (de Bruijn indices) must be identical.

    Returns a TermMatchResult = (TermSubst, TypeSubst):
    • The term substitution maps pattern variables to their matched sub-terms.
    • The type substitution maps type variables in the pattern to concrete types. Identity bindings (variable mapped to itself) are removed.

    Aborts if the pattern cannot match the observation (structural mismatch, inconsistent variable binding, or type mismatch).

    Term::mk_abs

    source
    fn Term::mk_abs(x : Term, m : Term) -> Term

    Construct the abstraction \x. m in locally nameless encoding.

    x must be a free variable (FVar). Every free occurrence of x inside m is replaced by BVar(0), and x itself is kept as a binder annotation so that dest_abs can recover a human-readable name. Under nested abstractions the de Bruijn index is shifted so that each BVar always points to its correct binder.

    If x does not occur free in m, the body is left unchanged (a vacuous abstraction). If x is shadowed by an inner Abs with the same binder, occurrences below that inner binder are not captured.

    Aborts if x is not a free variable.

    Term::mk_const

    source
    fn Term::mk_const(name : String, ty : 
    Type    ) -> Term raise

    Construct a constant term, checking that the name is registered in the global signature and that the requested type is a valid instance of the declared polymorphic type.

    Term::mk_eq

    source
    fn Term::mk_eq(lhs : Term, rhs : Term) -> Term

    Build the equation lhs = rhs, checking that both sides have the same type and instantiating the polymorphic equality constant accordingly.

    Term::new_const

    source
    fn Term::new_const(name : String, ty : 
    Type    ) -> Term

    Register a new constant with the given name and type in the global signature, aborting if the name is already in use. Returns the constructed constant term.

    Term::not_equal

    source
    fn Term::not_equal(x : Term, y : Term) -> Bool

    Term::op_ge

    source
    fn Term::op_ge(x : Term, y : Term) -> Bool

    Term::op_gt

    source
    fn Term::op_gt(x : Term, y : Term) -> Bool

    Term::op_le

    source
    fn Term::op_le(x : Term, y : Term) -> Bool

    Term::op_lt

    source
    fn Term::op_lt(x : Term, y : Term) -> Bool

    Term::output

    source
    fn Term::output(self : Term, logger : &Logger) -> Unit

    Term::pprint

    source
    fn Term::pprint(self : Term) -> String

    Pretty-print the term followed by its type annotation, rendering bound variables by name and omitting internal constructors.

    Term::reset_table

    source
    fn Term::reset_table() -> Unit

    Reset the global constant table to the most recent checkpoint, discarding any constants registered since then.

    Term::subst

    source

    Apply a term-level substitution simultaneously, replacing free variables according to the given mapping in a single pass.

    Unlike sequential application (which would let the range of one pair be rewritten by later pairs), this looks up each free variable in the original term independently, matching standard HOL semantics.

    Term::to_repr

    source

    Term::to_string

    source
    fn Term::to_string(self : Term) -> String

    Term::type_of

    source
    fn Term::type_of(self : Term) -> 
    Type

    Infer the type of a term by recursively traversing its structure.

    const_

    source
    fn const_(name : String, ty : 
    Type    ) -> Term

    Construct a constant term without checking the global signature. Intended for the logic layer, which builds connective and type-operator heads before they are formally registered. Prefer mk_const for user-facing code.

    mk_app

    source
    fn mk_app(m : Term, n : Term) -> Term

    Construct a function application term.

    mk_var

    source
    fn mk_var(name : String, ty : 
    Type    ) -> Term

    Construct a free (named) variable with the given name and type.

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io