Agda-2.2.4: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

newtype Unify a = U { unUnify :: ExceptionT UnifyException (StateT UnifyState TCM) a } data Equality = Equal Type Term Term type Sub = Map Nat Term data UnifyException = ConstructorMismatch Type Term Term | GenericUnifyException String data UnifyState = USt { uniSub :: Sub uniConstr :: [Equality] } constructorMismatch :: Type -> Term -> Term -> Unify a getSub :: Unify Sub onSub :: (Sub -> a) -> Unify a modSub :: (Sub -> Sub) -> Unify () checkEqualities :: [Equality] -> TCM () addEquality :: Type -> Term -> Term -> Unify () takeEqualities :: Unify [Equality] occursCheck :: Nat -> Term -> Type -> Unify () (|->) :: Nat -> (Term, Type) -> Unify () makeSubstitution :: Sub -> [Term] ureduce :: Term -> Unify Term flattenSubstitution :: Substitution -> Substitution data UnificationResult = Unifies Substitution | NoUnify Type Term Term | DontKnow TCErr unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult

Documentation

newtype Unify a Source

Constructors U unUnify :: ExceptionT UnifyException (StateT UnifyState TCM) a Instances Monad Unify Functor Unify Applicative Unify MonadIO Unify MonadTCM Unify MonadReader TCEnv Unify MonadState TCState Unify MonadException UnifyException Unify

data Equality Source

Constructors Equal Type Term Term Instances Subst Equality

type Sub = Map Nat Term Source

data UnifyException Source

Constructors ConstructorMismatch Type Term Term GenericUnifyException String Instances Error UnifyException MonadException UnifyException Unify

data UnifyState Source

Constructors USt uniSub :: Sub uniConstr :: [Equality]

constructorMismatch :: Type -> Term -> Term -> Unify a Source

getSub :: Unify Sub Source

onSub :: (Sub -> a) -> Unify a Source

modSub :: (Sub -> Sub) -> Unify () Source

checkEqualities :: [Equality] -> TCM () Source

addEquality :: Type -> Term -> Term -> Unify () Source

takeEqualities :: Unify [Equality] Source

occursCheck :: Nat -> Term -> Type -> Unify () Source

Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences

(|->) :: Nat -> (Term, Type) -> Unify () Source

makeSubstitution :: Sub -> [Term] Source

ureduce :: Term -> Unify Term Source

Apply the current substitution on a term and reduce to weak head normal form.

flattenSubstitution :: Substitution -> Substitution Source

Take a substitution  and ensure that no variables from the domain appear in the targets. The context of the targets is not changed. TODO: can this be expressed using makeSubstitution and substs?

data UnificationResult Source

Constructors Unifies Substitution NoUnify Type Term Term DontKnow TCErr

unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution Source

Unify indices.

unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult Source

Produced by Haddock version 2.4.2