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

Safe Haskell | None

Agda.TypeChecking.Reduce

Contents

- Reduction to weak head normal form.
- Normalisation
- Full instantiation

Synopsis

- 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
  - reduce :: t -> TCM t
  - reduceB :: t -> TCM (Blocked t)
- 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
  - normalise :: t -> TCM t
- class InstantiateFull t where
  - instantiateFull :: t -> TCM t

# Documentation

traceFun :: String -> TCM a -> TCM a

traceFun' :: Show a => 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 :: t -> TCM t

Instances

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.

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

Methods

reduce :: t -> TCM t

reduceB :: t -> TCM (Blocked t)

Instances

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)

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

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

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

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

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

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)

# Normalisation

class Normalise t where

Methods

normalise :: t -> TCM t

Instances

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 where

Methods

instantiateFull :: t -> TCM t

Instances

InstantiateFull Char |
InstantiateFull ModuleName |
InstantiateFull QName |
InstantiateFull Name |
InstantiateFull Scope |
InstantiateFull Pattern |
InstantiateFull ClauseBody |
InstantiateFull Clause |
InstantiateFull LevelAtom |
InstantiateFull PlusLevel |
InstantiateFull Level |
InstantiateFull Sort |
InstantiateFull Type |
InstantiateFull Elim |
InstantiateFull Term |
InstantiateFull CompiledClauses |
InstantiateFull FunctionInverse |
InstantiateFull Defn |
InstantiateFull Definition |
InstantiateFull DisplayTerm |
InstantiateFull DisplayForm |
InstantiateFull Section |
InstantiateFull Signature |
InstantiateFull Constraint |
InstantiateFull ProblemConstraint |
InstantiateFull Interface |
InstantiateFull t => InstantiateFull [t] |
InstantiateFull a => InstantiateFull (Maybe a) |
InstantiateFull t => InstantiateFull (Arg t) |
InstantiateFull t => InstantiateFull (Dom t) |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) |
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) |
InstantiateFull a => InstantiateFull (Case a) |
InstantiateFull a => InstantiateFull (WithArity 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) |
(Eq k, Hashable k, InstantiateFull e) => InstantiateFull (HashMap k e) |
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) |