#Foundation

Shared data structures used throughout the HOL prover. This is the lowest layer -- it has no dependencies on any other HOL sub-package.

#Overview

Type	Role
Subst[A, B]	Substitution as a list of (redex, residue) pairs

#Subst

A substitution is a list of (redex, residue) pairs. New bindings are prepended (add), so lookup finds the most recently added mapping first, giving natural shadowing semantics.

Substitutions are used for:

Type instantiation -- Subst[Type, Type] maps type variables to types
Term replacement -- Subst[Term, Term] maps term variables to terms
Matching -- building mappings from pattern variables to concrete values

///|
test "Subst: add, lookup, and shadowing" {
  let s : @foundation.Subst[String, Int] = Subst()
  assert_true(s.is_empty())

  let s2 = s.add("x", 1).add("y", 2)
  assert_eq(s2.lookup("x"), Some(1))
  assert_eq(s2.lookup("y"), Some(2))
  assert_eq(s2.lookup("z"), None)
  assert_true(s2.contains("x"))

  // Shadowing: a later binding for "x" wins
  let s3 = s2.add("x", 99)
  assert_eq(s3.lookup("x"), Some(99))
}

#mergesort

Sorts an array and optionally removes adjacent duplicates. When unique is true, the result is a canonical sorted set represented as an array. Used throughout the prover for free-variable lists and type-variable lists.

///|
test "mergesort with deduplication" {
  let xs = [3, 1, 2, 1, 3]

  let unique = @foundation.dedup_sort(xs)
  assert_eq(unique, [1, 2, 3])
}

Subst

source

pub struct Subst[A, B] {
  // private fields
} derive(@moonbitlang/core/debug.Debug
Debug)

An immutable substitution mapping keys of type A to values of type B, represented as an association list with most-recent-first lookup.

Subst::Subst

source

fn[A, B] Subst::Subst(pairs? : ArrayView[(A, B)]) -> Subst[A, B]

Construct a Subst[A, B] from an optional array of (redex, residue) pairs. The array order is preserved, and lookup returns the first matching pair — earliest-entry-wins on duplicate keys. (The opposite of Subst::add, which prepends and therefore makes the most recently added binding win; callers building a substitution from an array that wants add-style shadowing should feed pairs into add instead.)

Subst::add

source

fn[A, B] Subst::add(self : Subst[A, B], redex : A, residue : B) -> Subst[A, B]

Extend the substitution with a new (redex, residue) binding.

The new binding is prepended so that lookup finds the most recently added mapping first, giving natural shadowing semantics.

Subst::contains

source

fn[A : Eq, B] Subst::contains(self : Subst[A, B], x : A) -> Bool

Test whether x appears as a redex in the substitution.

Subst::is_empty

source

fn[A, B] Subst::is_empty(self : Subst[A, B]) -> Bool

Test whether the substitution contains no bindings.

Subst::iter

source

fn[A, B] Subst::iter(self : Subst[A, B]) -> Iter[(A, B)]

Iterate over the (redex, residue) bindings.

Subst::lookup

source

fn[A : Eq, B] Subst::lookup(self : Subst[A, B], x : A) -> B?

Look up the residue bound to x, returning None if x is not in the domain. Finds the most recently added binding due to prepend order.

Subst::to_repr

source

fn[A : @moonbitlang/core/debug.Debug
Debug, B : @moonbitlang/core/debug.Debug
Debug] Subst::to_repr(Subst[A, B]) -> @moonbitlang/core/debug.Repr
Repr

dedup_sort

source

fn[A : Compare + Eq] dedup_sort(xs : Array[A]) -> Array[A]

Sort an array, optionally removing duplicates.

When unique is true, adjacent duplicates are eliminated after sorting, producing a canonical set representation as a sorted array. This is used throughout the prover to normalize free-variable and type-variable lists.