| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce
Synopsis
- instantiate :: (Instantiate a, MonadReduce m) => a -> m a
- instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a
- reduce :: (Reduce a, MonadReduce m) => a -> m a
- reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a)
- normalise :: (Normalise a, MonadReduce m) => a -> m a
- normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t)
- simplify :: (Simplify a, MonadReduce m) => a -> m a
- isFullyInstantiatedMeta :: MetaId -> TCM Bool
- class Instantiate t where
- instantiate' :: t -> ReduceM t
- class IsMeta a where
- isMeta :: HasBuiltins m => a -> m (Maybe MetaId)
- ifBlocked :: (Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) => t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
- isBlocked :: (Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) => t -> m (Maybe MetaId)
- class Reduce t where
- reduceIApply :: ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
- blockedOrMeta :: Blocked Term -> Blocked ()
- reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
- 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 :: forall m. (MonadReduce m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> Elims -> m (Reduced () Term)
- reduceHead :: (HasBuiltins m, HasConstInfo m, MonadReduce m, MonadDebug m) => Term -> m (Blocked Term)
- unfoldInlined :: (HasConstInfo m, MonadReduce m) => Term -> m 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
- normalise' :: t -> ReduceM t
- slowNormaliseArgs :: Term -> ReduceM Term
- class InstantiateFull t where
- instantiateFull' :: t -> ReduceM t
Documentation
instantiate :: (Instantiate a, MonadReduce m) => a -> m a Source #
instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a Source #
reduce :: (Reduce a, MonadReduce m) => a -> m a Source #
normalise :: (Normalise a, MonadReduce m) => a -> m a Source #
normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t) Source #
Normalise the given term but also preserve blocking tags TODO: implement a more efficient version of this.
simplify :: (Simplify a, MonadReduce m) => a -> m 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).
Minimal complete definition
Nothing
Methods
instantiate' :: t -> ReduceM t Source #
default instantiate' :: (t ~ f a, Traversable f, Instantiate a) => t -> ReduceM t Source #
Instances
Reduction to weak head normal form.
Instances
| IsMeta Level Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta Sort Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta Type Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta Term Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta CompareAs Source # | |
Defined in Agda.TypeChecking.Reduce | |
ifBlocked :: (Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) => t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m 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.
isBlocked :: (Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) => t -> m (Maybe MetaId) Source #
Minimal complete definition
Nothing
Instances
reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term) 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 :: forall m. (MonadReduce m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> Elims -> m (Reduced () Term) Source #
Reduce a non-primitive definition if it is a copy linking to another def.
reduceHead :: (HasBuiltins m, HasConstInfo m, MonadReduce m, MonadDebug m) => Term -> m (Blocked Term) Source #
Reduce simple (single clause) definitions.
unfoldInlined :: (HasConstInfo m, MonadReduce m) => Term -> m Term Source #
Unfold a single inlined function.
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.
Minimal complete definition
Nothing
Methods
Instances
Normalisation
class Normalise t where Source #
Minimal complete definition
Nothing
Methods
normalise' :: t -> ReduceM t Source #
default normalise' :: (t ~ f a, Traversable f, Normalise a) => t -> ReduceM t Source #
Instances
Full instantiation
class InstantiateFull t where Source #
instantiateFull' instantiates metas everywhere (and recursively)
but does not reduce.
Minimal complete definition
Nothing
Methods
instantiateFull' :: t -> ReduceM t Source #
default instantiateFull' :: (t ~ f a, Traversable f, InstantiateFull a) => t -> ReduceM t Source #