package term-tools

  1. Overview
  2. Docs

Module Make.UnificationSource

Solving unification problems on first-order terms.

Sourcetype term = Term.t

The type of terms

Sourcetype subst = Subst.t

The type of substitutions

Sourcetype state

state is the type of unification state.

Sourceexception Cannot_unify

Cannot_unify is raised by unify when a unifier cannot be found.

Sourceval empty : unit -> state

empty () is an empty unification state.

Sourceval unify : term -> term -> state -> state option

unify t1 t2 state unifies terms t1 and t2 in state state and returns an updated state.

Sourceval unify_exn : term -> term -> state -> state

unify_exn t1 t2 state unifies terms t1 and t2 in state state and returns an updated state.

Raises Cannot_unify if no solution was found.

Sourceval unify_subst : subst -> state -> state option

unify_subst s state unifies s with substitution state state and returns an updated state.

Sourceval unify_subst_exn : subst -> state -> state

unify_subst s1 s2 state unifies s1 with s2 in state state and returns an updated state.

Sourceval generalizes : term -> term -> bool

generalizes t1 t2 checks that there exists a substitution subst such that lift t1 subst = t2.

Sourceval subst : state -> subst

subst state returns the substitution underlying the unification state.

Sourceexception Occurs_check

Occurs_check is raised by unfold when the solution contains a cycle.

Sourceval unfold : state -> term -> term

unfold state term returns term with variables substituted for their representative terms. Raises Occurs_check if the solution contains a cycle.