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

Language | Haskell98 |

- 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
- 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
- rewriteAfter :: (Term -> ReduceM (Blocked Term)) -> 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 -> (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
- 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 #

Instantiate EqualityView Source # | |

Instantiate LevelAtom Source # | |

Instantiate PlusLevel Source # | |

Instantiate Level Source # | |

Instantiate Sort Source # | |

Instantiate Telescope Source # | |

Instantiate Type Source # | |

Instantiate Elim Source # | |

Instantiate Term Source # | |

Instantiate Candidate Source # | |

Instantiate Constraint Source # | |

Instantiate t => Instantiate [t] Source # | |

Instantiate t => Instantiate (Dom t) Source # | |

Instantiate t => Instantiate (Arg t) Source # | |

Instantiate a => Instantiate (Blocked a) Source # | |

Instantiate t => Instantiate (Abs t) Source # | |

Instantiate a => Instantiate (Closure a) Source # | |

(Instantiate a, Instantiate b) => Instantiate (a, b) Source # | |

Instantiate e => Instantiate (Map k e) Source # | |

(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) Source # | |

# Reduction to weak head normal form.

ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (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) -> (Type -> tcm a) -> tcm a Source #

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

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

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 -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) Source #

reduceDefCopy :: QName -> Args -> TCM (Reduced () Term) Source #

Reduce a non-primitive definition if it is a copy linking to another def.

appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> 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 -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #

appDef :: Term -> CompiledClauses -> 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 -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #

appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #

Apply a defined function to it's arguments, using the original clauses.

# Simplification

class Simplify t where Source #

Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched.

Simplify Bool Source # | |

Simplify EqualityView Source # | |

Simplify ClauseBody Source # | |

Simplify LevelAtom Source # | |

Simplify PlusLevel Source # | |

Simplify Level Source # | |

Simplify Sort Source # | |

Simplify Type Source # | |

Simplify Elim Source # | |

Simplify Term Source # | |

Simplify Candidate Source # | |

Simplify DisplayForm Source # | |

Simplify Constraint Source # | |

Simplify ProblemConstraint Source # | |

Simplify t => Simplify [t] Source # | |

Simplify a => Simplify (Maybe a) Source # | |

Simplify t => Simplify (Dom t) Source # | |

Simplify t => Simplify (Arg t) Source # | |

(Subst t a, Simplify a) => Simplify (Tele a) Source # | |

(Subst t a, Simplify a) => Simplify (Abs a) Source # | |

Simplify a => Simplify (Closure a) Source # | |

(Simplify a, Simplify b) => Simplify (a, b) Source # | |

Simplify e => Simplify (Map k e) Source # | |

Simplify t => Simplify (Named name t) Source # | |

(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) Source # | |

# Normalisation

class Normalise t where Source #

normalise' :: t -> ReduceM t Source #

# Full instantiation

class InstantiateFull t where Source #

`instantiateFull'`

`instantiate`

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

.

instantiateFull' :: t -> ReduceM t Source #