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

- ifBlocked :: MonadReduce m => Term -> (MetaId -> Term -> m a) -> (NotBlocked -> Term -> m a) -> m a
- isBlocked :: MonadReduce m => Term -> m (Maybe MetaId)
- ifBlockedType :: MonadReduce m => Type -> (MetaId -> Type -> m a) -> (NotBlocked -> Type -> m a) -> m a
- isBlockedType :: MonadReduce m => Type -> 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 :: QName -> Elims -> TCM (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).

instantiate' :: t -> ReduceM t Source #

## Instances

# Reduction to weak head normal form.

ifBlocked :: MonadReduce m => Term -> (MetaId -> Term -> m a) -> (NotBlocked -> Term -> 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.

ifBlockedType :: MonadReduce m => Type -> (MetaId -> Type -> m a) -> (NotBlocked -> Type -> m a) -> m a Source #

Case on whether a type is blocked on a meta (or is a meta).

isBlockedType :: MonadReduce m => Type -> 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 :: QName -> Elims -> TCM (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.

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