aufbau 0.3.1

Generalized prefix parsing for a class of context-dependent languages
1
2
3
4
5
6
7
8
9
10
11
12

//! Normalization, exposed to OCaml.

use super::term::OTerm;
use super::theory;

/// The normal form of a term under a rewrite theory.
#[ocaml::func]
#[must_use]
pub fn aufbau_normalize(rules: Vec<(OTerm, OTerm)>, t: OTerm) -> OTerm {
    let norm = theory::normalizer(rules);
    OTerm::lift(&norm.normalize(&t.lower()))
}