| Safe Haskell | None |
|---|
Agda.TypeChecking.Rules.LHS.Unify
- newtype Unify a = U {
- unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a
- data UnifyMayPostpone
- type UnifyEnv = UnifyMayPostpone
- emptyUEnv :: UnifyMayPostpone
- noPostponing :: Unify a -> Unify a
- askPostpone :: Unify UnifyMayPostpone
- type UnifyOutput = Unifiable
- emptyUOutput :: UnifyOutput
- data Unifiable
- = Definitely
- | Possibly
- reportPostponing :: Unify ()
- ifClean :: Unify () -> Unify a -> Unify a -> Unify a
- data Equality = Equal TypeHH Term Term
- type Sub = Map Nat Term
- data UnifyException
- data UnifyState = USt {}
- emptyUState :: UnifyState
- constructorMismatch :: Type -> Term -> Term -> Unify a
- constructorMismatchHH :: TypeHH -> Term -> Term -> Unify a
- onSub :: (Sub -> a) -> Unify a
- modSub :: (Sub -> Sub) -> Unify ()
- checkEqualities :: [Equality] -> TCM ()
- checkEquality :: Type -> Term -> Term -> TCM ()
- checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()
- forceHom :: TypeHH -> TCM Type
- addEquality :: Type -> Term -> Term -> Unify ()
- addEqualityHH :: TypeHH -> Term -> Term -> Unify ()
- takeEqualities :: Unify [Equality]
- occursCheck :: Nat -> Term -> Type -> Unify ()
- (|->) :: Nat -> (Term, Type) -> Unify ()
- makeSubstitution :: Sub -> Substitution
- class UReduce t where
- flattenSubstitution :: Substitution -> Substitution
- data UnificationResult
- data HomHet a
- isHom :: HomHet a -> Bool
- fromHom :: HomHet a -> a
- leftHH :: HomHet a -> a
- rightHH :: HomHet a -> a
- type TermHH = HomHet Term
- type TypeHH = HomHet Type
- type TelHH = Tele (Dom TypeHH)
- type TelViewHH = TelV TypeHH
- absAppHH :: SubstHH t tHH => Abs t -> TermHH -> tHH
- class ApplyHH t where
- substHH :: SubstHH t tHH => TermHH -> t -> tHH
- class SubstHH t tHH where
- substUnderHH :: Nat -> TermHH -> t -> tHH
- trivialHH :: t -> tHH
- unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution
- unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult
- dataOrRecordType :: QName -> Type -> TCM (Maybe Type)
- dataOrRecordType' :: QName -> Type -> TCM (Maybe (QName, Type, Args))
- dataOrRecordTypeHH :: QName -> TypeHH -> TCM (Maybe TypeHH)
- isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args))
- data ShapeView a
- shapeView :: Type -> Unify (Type, ShapeView Type)
- shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH)
- telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH
Documentation
Constructors
| U | |
Fields
| |
Instances
| Monad Unify | |
| Functor Unify | |
| Applicative Unify | |
| MonadIO Unify | |
| MonadTCM Unify | |
| MonadState TCState Unify | |
| MonadReader TCEnv Unify | |
| MonadWriter UnifyOutput Unify | |
| MonadException UnifyException Unify |
data UnifyMayPostpone Source
Constructors
| MayPostpone | |
| MayNotPostpone |
type UnifyEnv = UnifyMayPostponeSource
noPostponing :: Unify a -> Unify aSource
type UnifyOutput = UnifiableSource
Output the result of unification (success or maybe).
Were two terms unifiable or did we have to postpone some equation such that we are not sure?
Constructors
| Definitely | Unification succeeded. |
| Possibly | Unification did not fail, but we had to postpone a part. |
Instances
| Monoid Unifiable | Conjunctive monoid. |
| MonadWriter UnifyOutput Unify |
reportPostponing :: Unify ()Source
Tell that something could not be unified right now,
so the unification succeeds only Possibly.
ifClean :: Unify () -> Unify a -> Unify a -> Unify aSource
Check whether unification proceeded without postponement.
data UnifyException Source
Constructors
| ConstructorMismatch Type Term Term | |
| StronglyRigidOccurrence Type Term Term | |
| GenericUnifyException String |
Instances
checkEqualities :: [Equality] -> TCM ()Source
checkEquality :: Type -> Term -> Term -> TCM ()Source
Force equality now instead of postponing it using addEquality.
checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()Source
Try equality. If constraints remain, postpone (enter unsafe mode). Heterogeneous equalities cannot be tried nor reawakened, so we can throw them away and flag dirty.
forceHom :: TypeHH -> TCM TypeSource
Check whether heterogeneous situation is really homogeneous. If not, give up.
occursCheck :: Nat -> Term -> Type -> Unify ()Source
Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences
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 applySubst?
data UnificationResult Source
Are we in a homogeneous (one type) or heterogeneous (two types) situation?
Instances
| Functor HomHet | |
| Typeable1 HomHet | |
| Foldable HomHet | |
| Traversable HomHet | |
| SubstHH Type (HomHet Type) | |
| SubstHH Term (HomHet Term) | |
| Eq a => Eq (HomHet a) | |
| Ord a => Ord (HomHet a) | |
| Show a => Show (HomHet a) | |
| Subst a => Subst (HomHet a) | |
| PrettyTCM a => PrettyTCM (HomHet a) | |
| UReduce t => UReduce (HomHet t) | |
| (Free a, Subst a) => SubstHH (HomHet a) (HomHet a) |
class SubstHH t tHH whereSource
substHH u t substitutes u for the 0th variable in t.
Instances
| SubstHH Type (HomHet Type) | |
| SubstHH Term (HomHet Term) | |
| SubstHH a b => SubstHH (Arg a) (Arg b) | |
| SubstHH a b => SubstHH (Dom a) (Dom b) | |
| SubstHH a b => SubstHH (Tele a) (Tele b) | |
| SubstHH a b => SubstHH (Abs a) (Abs b) | |
| (Free a, Subst a) => SubstHH (HomHet a) (HomHet a) | |
| (SubstHH a a', SubstHH b b') => SubstHH (a, b) (a', b') |
unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm SubstitutionSource
Unify indices.
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResultSource
Arguments
| :: QName | Constructor name. |
| -> Type | Type of constructor application (must end in data/record). |
| -> TCM (Maybe Type) | Type of constructor, applied to pars. |
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.
Arguments
| :: QName | Constructor name. |
| -> TypeHH | Type(s) of constructor application (must end in same data/record). |
| -> TCM (Maybe TypeHH) | Type of constructor, instantiated possibly heterogeneously to parameters. |
Heterogeneous situation.
a1 and a2 need to end in same datatype/record.
isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args))Source
Return record type identifier if argument is a record type.
Views an expression (pair) as type shape. Fails if not same shape.
shapeView :: Type -> Unify (Type, ShapeView Type)Source
Return the type and its shape. Expects input in (u)reduced form.