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
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

//! Unification, exposed to OCaml.

use super::term::OTerm;
use super::theory;
use crate::typing::{Subst, term, unify_modulo};

/// Unify two terms in the free theory. `Some subst` (a solved assoc array) on
/// success, `None` on clash.
#[ocaml::func]
#[must_use]
pub fn aufbau_unify(a: OTerm, b: OTerm) -> Option<Vec<(String, OTerm)>> {
    let mut s = Subst::new();
    term::unify(&a.lower(), &b.lower(), &mut s, true).then(|| theory::solution(&s))
}

/// Unify two terms modulo a rewrite theory (normalize, then unify).
#[ocaml::func]
#[must_use]
pub fn aufbau_unify_modulo(
    rules: Vec<(OTerm, OTerm)>,
    a: OTerm,
    b: OTerm,
) -> Option<Vec<(String, OTerm)>> {
    let norm = theory::normalizer(rules);
    let mut s = Subst::new();
    unify_modulo(&norm, &a.lower(), &b.lower(), &mut s, true).then(|| theory::solution(&s))
}