Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.TypeChecking.Reduce
- instantiate :: Instantiate a => a -> TCM a
- instantiateFull :: InstantiateFull a => a -> TCM a
- reduce :: Reduce a => a -> TCM a
- reduceB :: Reduce a => a -> TCM (Blocked a)
- normalise :: Normalise a => a -> TCM a
- simplify :: Simplify a => a -> TCM a
- class Instantiate t where
- instantiate' :: t -> ReduceM t
- ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a
- ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a
- class Reduce t where
- unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term)
- unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term)
- unfoldDefinition' :: Bool -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
- reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
- reduceHead :: Term -> TCM (Blocked Term)
- reduceHead' :: Term -> ReduceM (Blocked Term)
- appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- class Simplify t where
- simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
- class Normalise t where
- normalise' :: t -> ReduceM t
- class InstantiateFull t where
- instantiateFull' :: t -> ReduceM t
Documentation
instantiate :: Instantiate a => a -> TCM a
instantiateFull :: InstantiateFull a => a -> TCM a
class Instantiate t where
Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).
Methods
instantiate' :: t -> ReduceM t
Instances
Instantiate LevelAtom | |
Instantiate PlusLevel | |
Instantiate Level | |
Instantiate Sort | |
Instantiate Telescope | |
Instantiate Type | |
Instantiate Elim | |
Instantiate Term | |
Instantiate Constraint | |
Instantiate t => Instantiate [t] | |
Instantiate a => Instantiate (Blocked a) | |
Instantiate t => Instantiate (Abs t) | |
Instantiate t => Instantiate (Dom t) | |
Instantiate t => Instantiate (Arg t) | |
Instantiate a => Instantiate (Closure a) | |
(Instantiate a, Instantiate b) => Instantiate (a, b) | |
(Ord k, Instantiate e) => Instantiate (Map k e) | |
(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) |
Reduction to weak head normal form.
ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a
Case on whether a term is blocked on a meta (or is a meta). That means it can change its shape when the meta is instantiated.
ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a
Case on whether a type is blocked on a meta (or is a meta).
class Reduce t where
Minimal complete definition
Nothing
Instances
Reduce LevelAtom | |
Reduce PlusLevel | |
Reduce Level | |
Reduce Sort | |
Reduce Telescope | |
Reduce Type | |
Reduce Elim | |
Reduce Term | |
Reduce Constraint | |
Reduce t => Reduce [t] | |
(Subst t, Reduce t) => Reduce (Abs t) | |
Reduce t => Reduce (Dom t) | |
Reduce t => Reduce (Arg t) | |
Reduce a => Reduce (Closure a) | |
(Reduce a, Reduce b) => Reduce (a, b) | |
(Ord k, Reduce e) => Reduce (Map k e) | |
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) |
unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term)
If the first argument is True
, then a single delayed clause may
be unfolded.
unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term)
unfoldDefinition' :: Bool -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
Reduce a non-primitive definition if it is a copy linking to another def.
reduceHead :: Term -> TCM (Blocked Term)
Reduce simple (single clause) definitions.
reduceHead' :: Term -> ReduceM (Blocked Term)
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
Apply a definition using the compiled clauses, or fall back to ordinary clauses if no compiled clauses exist.
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
Apply a defined function to it's arguments, using the compiled clauses. The original term is the first argument applied to the third.
appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
Apply a defined function to it's arguments, using the original clauses.
Simplification
class Simplify t where
Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched.
Instances
Simplify Bool | |
Simplify ClauseBody | |
Simplify LevelAtom | |
Simplify PlusLevel | |
Simplify Level | |
Simplify Sort | |
Simplify Type | |
Simplify Elim | |
Simplify Term | |
Simplify DisplayForm | |
Simplify Constraint | |
Simplify ProblemConstraint | |
Simplify t => Simplify [t] | |
Simplify a => Simplify (Maybe a) | |
(Subst a, Simplify a) => Simplify (Tele a) | |
(Subst t, Simplify t) => Simplify (Abs t) | |
Simplify t => Simplify (Dom t) | |
Simplify t => Simplify (Arg t) | |
Simplify a => Simplify (Closure a) | |
(Simplify a, Simplify b) => Simplify (a, b) | |
(Ord k, Simplify e) => Simplify (Map k e) | |
Simplify t => Simplify (Named name t) | |
(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) |
simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
Normalisation
class Normalise t where
Methods
normalise' :: t -> ReduceM t
Instances
Normalise Bool | |
Normalise ConPatternInfo | |
Normalise Pattern | |
Normalise ClauseBody | |
Normalise LevelAtom | |
Normalise PlusLevel | |
Normalise Level | |
Normalise Sort | |
Normalise Type | |
Normalise Elim | |
Normalise Term | |
Normalise DisplayForm | |
Normalise Constraint | |
Normalise ProblemConstraint | |
Normalise t => Normalise [t] | |
Normalise a => Normalise (Maybe a) | |
(Subst a, Normalise a) => Normalise (Tele a) | |
(Subst t, Normalise t) => Normalise (Abs t) | |
Normalise t => Normalise (Dom t) | |
Normalise t => Normalise (Arg t) | |
Normalise a => Normalise (Closure a) | |
(Normalise a, Normalise b) => Normalise (a, b) | |
(Ord k, Normalise e) => Normalise (Map k e) | |
Normalise t => Normalise (Named name t) | |
(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) |
Full instantiation
class InstantiateFull t where
instantiateFull'
instantiate
s metas everywhere (and recursively)
but does not reduce
.
Methods
instantiateFull' :: t -> ReduceM t
Instances