Safe Haskell | None |
---|
Agda.TypeChecking.Rules.LHS.Unify
- newtype Unify a = U {}
- 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
data UnifyMayPostpone
Constructors
MayPostpone | |
MayNotPostpone |
type UnifyEnv = UnifyMayPostpone
noPostponing :: Unify a -> Unify a
type UnifyOutput = Unifiable
Output the result of unification (success or maybe).
data Unifiable
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 ()
Tell that something could not be unified right now,
so the unification succeeds only Possibly
.
ifClean :: Unify () -> Unify a -> Unify a -> Unify a
Check whether unification proceeded without postponement.
data UnifyException
Constructors
ConstructorMismatch Type Term Term | |
StronglyRigidOccurrence Type Term Term | |
GenericUnifyException String |
Instances
constructorMismatch :: Type -> Term -> Term -> Unify a
constructorMismatchHH :: TypeHH -> Term -> Term -> Unify a
checkEqualities :: [Equality] -> TCM ()
checkEquality :: Type -> Term -> Term -> TCM ()
Force equality now instead of postponing it using addEquality
.
checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()
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 Type
Check whether heterogeneous situation is really homogeneous. If not, give up.
addEquality :: Type -> Term -> Term -> Unify ()
addEqualityHH :: TypeHH -> 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
makeSubstitution :: Sub -> Substitution
class UReduce t where
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 applySubst?
data UnificationResult
data HomHet a
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 ApplyHH t where
class SubstHH t tHH where
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 Substitution
Unify indices.
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult
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))
Return record type identifier if argument is a record type.
data ShapeView a
Views an expression (pair) as type shape. Fails if not same shape.
shapeView :: Type -> Unify (Type, ShapeView Type)
Return the type and its shape. Expects input in (u)reduced form.
shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH)
Return the reduced type(s) and the common shape.
telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH
telViewUpToHH n t
takes off the first n
function types of t
.
Takes off all if $n < 0$.