package term-indexing

  1. Overview
  2. Docs

Module Subst.UnificationSource

Unification contains facilities to perform first-order term unification

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 : t -> state -> state option

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

Sourceval unify_subst_exn : t -> state -> state

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

Sourceval generalize : term -> term -> bool

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

Sourceval subst : state -> t

subst state returns the substitution underlying the unification state.