Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
dataOrRecordType :: MonadTCM tcm => QName -> Type -> tcm Type
Documentation
newtype Unify a Source
Constructors
U
unUnify :: ExceptionT UnifyException (StateT UnifyState TCM) a
data Equality Source
Constructors
Equal Type Term Term
type Sub = Map Nat TermSource
data UnifyException Source
Constructors
ConstructorMismatch Type Term Term
GenericUnifyException String
data UnifyState Source
Constructors
USt
uniSub :: Sub
uniConstr :: [Equality]
constructorMismatch :: Type -> Term -> Term -> Unify aSource
getSub :: Unify SubSource
onSub :: (Sub -> a) -> Unify aSource
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 TermSource
Apply the current substitution on a term and reduce to weak head normal form.
flattenSubstitution :: Substitution -> SubstitutionSource
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 SubstitutionSource
Unify indices.
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResultSource
dataOrRecordTypeSource
:: MonadTCM tcm
=> QName
-> Type
-> tcm Type

Given the type of a constructor application the corresponding data or record type, applied to its parameters (extracted from the given type), is returned.

Precondition: The type has to correspond to an application of the given constructor.

Produced by Haddock version 2.6.0