Portability | semi-portable (MPTCs, FlexibleContexts) |
---|---|

Stability | highly experimental |

Maintainer | wren@community.haskell.org |

Safe Haskell | None |

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.

- module Control.Unification.Types
- getFreeVars :: BindingMonad t v m => UTerm t v -> m [v]
- applyBindings :: (BindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m)) => UTerm t v -> e m (UTerm t v)
- freshen :: (BindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m)) => UTerm t v -> e m (UTerm t v)
- (===) :: BindingMonad t v m => UTerm t v -> UTerm t v -> m Bool
- (=~=) :: BindingMonad t v m => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
- (=:=) :: (RankedBindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m)) => UTerm t v -> UTerm t v -> e m (UTerm t v)
- equals :: BindingMonad t v m => UTerm t v -> UTerm t v -> m Bool
- equiv :: BindingMonad t v m => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
- unify :: (RankedBindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m)) => UTerm t v -> UTerm t v -> e m (UTerm t v)
- getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]
- applyBindingsAll :: (BindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m), Traversable s) => s (UTerm t v) -> e m (s (UTerm t v))
- freshenAll :: (BindingMonad t v m, MonadTrans e, Functor (e m), MonadError (UnificationFailure t v) (e m), Traversable s) => s (UTerm t v) -> e m (s (UTerm t v))

# Data types, classes, etc

module Control.Unification.Types

# Operations on one term

getFreeVars :: BindingMonad t v m => UTerm t v -> m [v]Source

Walk a term and determine which 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.

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

=> UTerm t v | |

-> e m (UTerm t v) |

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.

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

=> UTerm t v | |

-> e m (UTerm t v) |

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

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

=> UTerm t v | |

-> UTerm t v | |

-> e m (UTerm t v) |

## Textual names

:: BindingMonad t v m | |

=> UTerm t v | |

-> UTerm t v | |

-> 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`

.

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.

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

=> UTerm t v | |

-> UTerm t v | |

-> e m (UTerm t v) |

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.

# Operations on many terms

getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]Source

Same as `getFreeVars`

, but works on several terms simultaneously.
This is more efficient than getting the free variables for each
of the terms separately because we can make use of sharing across
the whole collection. That is, each time we move to the next
term, we still remember the bound variables we've already looked
at (and therefore do not need to traverse, since we've already
seen whatever free variables there are down there); whereas we
would forget between each call to `getFreeVars`

.

*Since: 0.7.0*

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

=> s (UTerm t v) | |

-> e m (s (UTerm t v)) |

Same as `applyBindings`

, but works on several terms simultaneously.
This function preserves sharing across the entire collection of
terms, whereas applying the bindings to each term separately
would only preserve sharing within each term.

*Since: 0.7.0*

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

=> s (UTerm t v) | |

-> e m (s (UTerm t v)) |

Same as `freshen`

, but works on several terms simultaneously.
This is different from freshening each term separately, because
`freshenAll`

preserves the relationship between the terms. For
instance, the result of

mapM freshen [UVar 1, UVar 1]

would be `[UVar 2, UVar 3]`

or something alpha-equivalent, whereas
the result of

freshenAll [UVar 1, UVar 1]

would be `[UVar 2, UVar 2]`

or something alpha-equivalent.

*Since: 0.7.0*