Safe Haskell | None |
---|

- traceFun :: String -> TCM a -> TCM a
- traceFun' :: Show a => String -> TCM a -> TCM a
- class Instantiate t where
- instantiate :: t -> TCM t

- 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
- unfoldDefinition :: Bool -> (Term -> TCM (Blocked Term)) -> Term -> QName -> Args -> TCM (Blocked Term)
- reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
- reduceDef :: QName -> Args -> TCM (Reduced () Term)
- reduceDef_ :: Definition -> QName -> Args -> TCM (Reduced () Term)
- appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Term) Term)
- appDef' :: Term -> [Clause] -> MaybeReducedArgs -> TCM (Reduced (Blocked Term) Term)
- class Normalise t where
- class InstantiateFull t where
- instantiateFull :: t -> TCM t

# Documentation

class Instantiate t whereSource

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 -> TCM tSource

Instantiate LevelAtom | |

Instantiate PlusLevel | |

Instantiate Level | |

Instantiate Sort | |

Instantiate Telescope | |

Instantiate Type | |

Instantiate Elim | |

Instantiate Term | |

Instantiate Constraint | |

Instantiate t => Instantiate [t] | |

Instantiate t => Instantiate (Arg t) | |

Instantiate t => Instantiate (Dom t) | |

Instantiate a => Instantiate (Blocked a) | |

Instantiate t => Instantiate (Abs t) | |

Instantiate a => Instantiate (Closure a) | |

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

(Ord k, Instantiate e) => Instantiate (Map k e) | |

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

# Reduction to weak head normal form.

ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm aSource

Reduce LevelAtom | |

Reduce PlusLevel | |

Reduce Level | |

Reduce Sort | |

Reduce Telescope | |

Reduce Type | |

Reduce Elim | |

Reduce Term | |

Reduce Constraint | |

Reduce t => Reduce [t] | |

Reduce t => Reduce (Arg t) | |

Reduce t => Reduce (Dom t) | |

(Subst t, Reduce t) => Reduce (Abs t) | |

Reduce a => Reduce (Closure a) | |

(Reduce a, Reduce b) => Reduce (a, b) | |

(Ord k, Reduce e) => Reduce (Map k e) | |

(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) |

unfoldDefinition :: Bool -> (Term -> TCM (Blocked Term)) -> Term -> QName -> Args -> TCM (Blocked Term)Source

If the first argument is `True`

, then a single delayed clause may
be unfolded.

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

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

reduceDef :: QName -> Args -> TCM (Reduced () Term)Source

Reduce a non-primitive definition once unless it is delayed.

reduceDef_ :: Definition -> QName -> Args -> TCM (Reduced () Term)Source

appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Term) Term)Source

# Normalisation

Normalise Pattern | |

Normalise ClauseBody | |

Normalise LevelAtom | |

Normalise PlusLevel | |

Normalise Level | |

Normalise Sort | |

Normalise Type | |

Normalise Elim | |

Normalise Term | |

Normalise DisplayForm | |

Normalise Constraint | |

Normalise ProblemConstraint | |

Normalise t => Normalise [t] | |

Normalise a => Normalise (Maybe a) | |

Normalise t => Normalise (Arg t) | |

Normalise t => Normalise (Dom t) | |

(Subst a, Normalise a) => Normalise (Tele a) | |

(Subst t, Normalise t) => Normalise (Abs t) | |

Normalise a => Normalise (Closure a) | |

(Normalise a, Normalise b) => Normalise (a, b) | |

(Ord k, Normalise e) => Normalise (Map k e) | |

(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) |

# Full instantiation

class InstantiateFull t whereSource

instantiateFull :: t -> TCM tSource