- newtype Unify a = U {}
- data Equality = Equal Type Term Term
- type Sub = Map Nat Term
- data UnifyException
- data UnifyState = USt {}
- 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
- 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
data UnifyException Source
checkEqualities :: [Equality] -> TCM ()Source
occursCheck :: Nat -> Term -> Type -> Unify ()Source
Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences
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?
unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm SubstitutionSource
Unify indices.
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResultSource
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.