Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Reduce

Contents

- Normalisation
- Full instantiation

Synopsis

- traceFun :: MonadTCM tcm => String -> tcm a -> tcm a
- traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a
- class Instantiate t where
  - instantiate :: MonadTCM tcm => t -> tcm t
- class Reduce t where
  - reduce :: MonadTCM tcm => t -> tcm t
  - reduceB :: MonadTCM tcm => t -> tcm (Blocked t)
- unfoldDefinition :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term)
- class Normalise t where
  - normalise :: MonadTCM tcm => t -> tcm t
- class InstantiateFull t where
  - instantiateFull :: MonadTCM tcm => t -> tcm t
- telViewM :: MonadTCM tcm => Type -> tcm TelView

# Documentation

traceFun :: MonadTCM tcm => String -> tcm a -> tcm a

traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a

class Instantiate t where

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

Methods

instantiate :: MonadTCM tcm => t -> tcm t

Instances

Instantiate Telescope |
Instantiate Sort |
Instantiate Type |
Instantiate Term |
Instantiate Constraint |
Instantiate t => Instantiate [t] |
Instantiate t => Instantiate (Arg t) |
Instantiate t => Instantiate (Abs t) |
Instantiate a => Instantiate (Blocked a) |
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) |

class Reduce t where

Methods

reduce :: MonadTCM tcm => t -> tcm t

reduceB :: MonadTCM tcm => t -> tcm (Blocked t)

Instances

Reduce Telescope |
Reduce Sort |
Reduce Type |
Reduce Term |
Reduce Constraint |
Reduce t => Reduce [t] |
Reduce t => Reduce (Arg 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 :: MonadTCM tcm => Bool -> (Term -> tcm (Blocked Term)) -> Term -> QName -> Args -> tcm (Blocked Term)

If the first argument is `True`, then a single delayed clause may be unfolded.

# Normalisation

class Normalise t where

Methods

normalise :: MonadTCM tcm => t -> tcm t

Instances

Normalise Pattern |
Normalise ClauseBody |
Normalise Sort |
Normalise Type |
Normalise Term |
Normalise DisplayForm |
Normalise Constraint |
Normalise t => Normalise [t] |
Normalise a => Normalise (Maybe a) |
Normalise t => Normalise (Arg t) |
Normalise t => Normalise (Abs t) |
Normalise a => Normalise (Tele a) |
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 where

Methods

instantiateFull :: MonadTCM tcm => t -> tcm t

Instances

InstantiateFull Char |
InstantiateFull ModuleName |
InstantiateFull Name |
InstantiateFull Pattern |
InstantiateFull ClauseBody |
InstantiateFull Clause |
InstantiateFull Clauses |
InstantiateFull Sort |
InstantiateFull Type |
InstantiateFull Term |
InstantiateFull Scope |
InstantiateFull CompiledClauses |
InstantiateFull FunctionInverse |
InstantiateFull Defn |
InstantiateFull Definition |
InstantiateFull DisplayTerm |
InstantiateFull DisplayForm |
InstantiateFull Section |
InstantiateFull Signature |
InstantiateFull Constraint |
InstantiateFull Interface |
InstantiateFull t => InstantiateFull [t] |
InstantiateFull a => InstantiateFull (Maybe a) |
InstantiateFull t => InstantiateFull (Arg t) |
InstantiateFull t => InstantiateFull (Abs t) |
InstantiateFull a => InstantiateFull (Tele a) |
InstantiateFull a => InstantiateFull (Case a) |
InstantiateFull a => InstantiateFull (Builtin a) |
InstantiateFull a => InstantiateFull (Open a) |
InstantiateFull a => InstantiateFull (Closure a) |
(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b) |
(Ord k, InstantiateFull e) => InstantiateFull (Map k e) |
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) |

telViewM :: MonadTCM tcm => Type -> tcm TelView