Safe Haskell | None |
---|---|

Language | Haskell2010 |

## 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).

Nothing

instantiate' :: t -> ReduceM t Source #

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 #

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.

Nothing

simplify' :: t -> ReduceM t Source #

simplify' :: (t ~ f a, Traversable f, Simplify a) => t -> ReduceM t Source #

## Instances

# Normalisation

class Normalise t where Source #

Nothing

normalise' :: t -> ReduceM t Source #

normalise' :: (t ~ f a, Traversable f, Normalise a) => t -> ReduceM t Source #

## Instances

# Full instantiation

class InstantiateFull t where Source #

`instantiateFull'`

`instantiate`

s metas everywhere (and recursively)
but does not `reduce`

.

Nothing

instantiateFull' :: t -> ReduceM t Source #

instantiateFull' :: (t ~ f a, Traversable f, InstantiateFull a) => t -> ReduceM t Source #