Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

Constructors

U |

Fields

unUnify :: ExceptionT UnifyException (StateT UnifyState TCM) a

Instances

Monad Unify |
Functor Unify |
Applicative Unify |
MonadIO Unify |
MonadTCM Unify |
MonadState TCState Unify |
MonadReader TCEnv Unify |
MonadException UnifyException Unify |

data Equality

Constructors

Equal Type Term Term |

Instances

Subst Equality |

type Sub = Map Nat Term

data UnifyException

Constructors

ConstructorMismatch Type Term Term |
GenericUnifyException String |

Instances

Error UnifyException |
MonadException UnifyException Unify |

data UnifyState

Constructors

USt |

Fields

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 ()

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

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

makeSubstitution :: Sub -> [Term]

ureduce :: Term -> Unify Term

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

flattenSubstitution :: Substitution -> Substitution

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

Constructors

Unifies Substitution |
NoUnify Type Term Term |
DontKnow TCErr |

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

Unify indices.

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

dataOrRecordType

Arguments

:: 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.