Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- 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
- isFullyInstantiatedMeta :: MetaId -> TCM Bool
- class Instantiate t where
- ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (NotBlocked -> Term -> tcm a) -> tcm a
- isBlocked :: MonadTCM tcm => Term -> tcm (Maybe MetaId)
- ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (NotBlocked -> Type -> tcm a) -> tcm a
- isBlockedType :: MonadTCM tcm => Type -> tcm (Maybe MetaId)
- class Reduce t where
- shouldTryFastReduce :: ReduceM Bool
- maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)
- slowReduceTerm :: Term -> ReduceM (Blocked Term)
- unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
- unfoldCorecursion :: Term -> ReduceM (Blocked Term)
- 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 -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
- unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
- reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term)
- reduceHead :: Term -> TCM (Blocked Term)
- reduceHead' :: Term -> ReduceM (Blocked Term)
- unfoldInlined :: Term -> TCM Term
- unfoldInlined' :: Term -> ReduceM Term
- appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- class Simplify t where
- simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
- class Normalise t where
- slowNormaliseArgs :: Term -> ReduceM Term
- class InstantiateFull t where
Documentation
instantiate :: Instantiate a => a -> TCM a Source #
instantiateFull :: InstantiateFull a => a -> TCM a Source #
class Instantiate t where Source #
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).
instantiate' :: t -> ReduceM t Source #
Instances
Reduction to weak head normal form.
ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (NotBlocked -> Term -> tcm a) -> tcm a Source #
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) -> (NotBlocked -> Type -> tcm a) -> tcm a Source #
Case on whether a type is blocked on a meta (or is a meta).
Instances
Reduce EqualityView Source # | |
Defined in Agda.TypeChecking.Reduce reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source # | |
Reduce LevelAtom Source # | |
Reduce PlusLevel Source # | |
Reduce Level Source # | |
Reduce Sort Source # | |
Reduce Telescope Source # | |
Reduce Type Source # | |
Reduce Elim Source # | |
Reduce Term Source # | |
Reduce Candidate Source # | |
Reduce Constraint Source # | |
Defined in Agda.TypeChecking.Reduce reduce' :: Constraint -> ReduceM Constraint Source # reduceB' :: Constraint -> ReduceM (Blocked Constraint) Source # | |
Reduce t => Reduce [t] Source # | |
Reduce t => Reduce (Dom t) Source # | |
Reduce t => Reduce (Arg t) Source # | |
(Subst t a, Reduce a) => Reduce (Abs a) Source # | |
Reduce a => Reduce (Closure a) Source # | |
(Reduce a, Reduce b) => Reduce (a, b) Source # | |
Reduce e => Reduce (Map k e) Source # | |
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) Source # | |
unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term) Source #
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) Source #
unfoldDefinition' :: Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) Source #
unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term) Source #
reduceDefCopy :: QName -> Elims -> TCM (Reduced () Term) Source #
Reduce a non-primitive definition if it is a copy linking to another def.
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #
Apply a definition using the compiled clauses, or fall back to ordinary clauses if no compiled clauses exist.
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #
appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #
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 -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #
appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #
Apply a defined function to it's arguments, using the original clauses.
appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #
Simplification
class Simplify t where Source #
Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched.
Instances
Normalisation
class Normalise t where Source #
normalise' :: t -> ReduceM t Source #
Instances
Full instantiation
class InstantiateFull t where Source #
instantiateFull'
instantiate
s metas everywhere (and recursively)
but does not reduce
.
instantiateFull' :: t -> ReduceM t Source #