| Agda-2.2.6: 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
dataOrRecordType :: MonadTCM tcm => QName -> Type -> tcm Type

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

dataOrRecordType | Source

:: MonadTCM tcm |
=> QName | Constructor name.
-> 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.4.2