README

#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

  fn new(pairs? : ArrayView[(A, B)]) -> Subst[A, B]
} 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::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.

#
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.