Control.Unification.Ranked

This module provides the API of Control.Unification except using RankedBindingMonad where appropriate. This module (and the binding implementations for it) are highly experimental and subject to change in future versions.

Data types, classes, etc

module Control.Unification.Types

Operations on one term

getFreeVars :: BindingMonad v t m => MutTerm v t -> m [v (MutTerm v t)]

Walk a term and determine what variables are still free. N.B., this function does not detect cyclic terms (i.e., throw errors), but it will return the correct answer for them in finite time.

applyBindings

Arguments

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m))

=> MutTerm v t

-> e m (MutTerm v t)

Apply the current bindings from the monad so that any remaining variables in the result must, therefore, be free. N.B., this expensively clones term structure and should only be performed when a pure term is needed, or when OccursIn exceptions must be forced. This function does preserve sharing, however that sharing is no longer observed by the monad.

If any cyclic bindings are detected, then an OccursIn exception will be thrown.

freshen

Arguments

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m))

=> MutTerm v t

-> e m (MutTerm v t)

Freshen all variables in a term, both bound and free. This ensures that the observability of sharing is maintained, while freshening the free variables. N.B., this expensively clones term structure and should only be performed when necessary.

If any cyclic bindings are detected, then an OccursIn exception will be thrown.

Operations on two terms

Symbolic names

(===)

Arguments

:: BindingMonad v t m

=> MutTerm v t

-> MutTerm v t

-> m Bool

equals

(=~=)

Arguments

:: BindingMonad v t m

=> MutTerm v t

-> MutTerm v t

-> m (Maybe (IntMap Int))

equiv

(=:=)

Arguments

:: (RankedBindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m))

=> MutTerm v t

-> MutTerm v t

-> e m (MutTerm v t)

unify

Textual names

equals

Arguments

:: BindingMonad v t m

=> MutTerm v t

-> MutTerm v t

-> m Bool

Determine if two terms are structurally equal. This is essentially equivalent to (==) except that it does not require applying bindings before comparing, so it is more efficient. N.B., this function does not consider alpha-variance, and thus variables with different names are considered unequal. Cf., equiv.

equiv

Arguments

:: BindingMonad v t m

=> MutTerm v t

-> MutTerm v t

-> m (Maybe (IntMap Int))

Determine if two terms are structurally equivalent; that is, structurally equal modulo renaming of free variables. Returns a mapping from variable IDs of the left term to variable IDs of the right term, indicating the renaming used.

unify

Arguments

:: (RankedBindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m))

=> MutTerm v t

-> MutTerm v t

-> e m (MutTerm v t)

Unify two terms, or throw an error with an explanation of why unification failed. Since bindings are stored in the monad, the two input terms and the output term are all equivalent if unification succeeds. However, the returned value makes use of aggressive opportunistic observable sharing, so it will be more efficient to use it in future calculations than either argument.