Agda.TypeChecking.Reduce

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)