Agda.TypeChecking.Reduce

Documentation

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

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 -> ReduceM t

Instances

Instantiate EqualityView

Instantiate LevelAtom

Instantiate PlusLevel

Instantiate Level

Instantiate Sort

Instantiate Telescope

Instantiate Type

Instantiate Elim

Instantiate Term

Instantiate Candidate

Instantiate Constraint

Instantiate t => Instantiate [t]

Instantiate t => Instantiate (Dom t)

Instantiate t => Instantiate (Arg t)

Instantiate a => Instantiate (Blocked a)

Instantiate t => Instantiate (Abs t)

Instantiate a => Instantiate (Closure a)

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

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

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

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

class Reduce t where

Minimal complete definition

Nothing

Methods

reduce' :: t -> ReduceM t

reduceB' :: t -> ReduceM (Blocked t)

Instances

Reduce EqualityView

Reduce LevelAtom

Reduce PlusLevel

Reduce Level

Reduce Sort

Reduce Telescope

Reduce Type

Reduce Elim

Reduce Term

Reduce Candidate

Reduce Constraint

Reduce t => Reduce [t]

Reduce t => Reduce (Dom t)

Reduce t => Reduce (Arg t)

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

Reduce a => Reduce (Closure a)

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

Reduce e => Reduce (Map k e)

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

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)

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)

unfoldDefinition' :: Bool -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)

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

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

reduceHead :: Term -> TCM (Blocked Term)

Reduce simple (single clause) definitions.

reduceHead' :: Term -> ReduceM (Blocked Term)

appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)

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)

appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)

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)

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

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

appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)

Simplification

class Simplify t where

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

Methods

simplify' :: t -> ReduceM t

Instances

Simplify Bool

Simplify EqualityView

Simplify ClauseBody

Simplify LevelAtom

Simplify PlusLevel

Simplify Level

Simplify Sort

Simplify Type

Simplify Elim

Simplify Term

Simplify Candidate

Simplify DisplayForm

Simplify Constraint

Simplify ProblemConstraint

Simplify t => Simplify [t]

Simplify a => Simplify (Maybe a)

Simplify t => Simplify (Dom t)

Simplify t => Simplify (Arg t)

(Subst t a, Simplify a) => Simplify (Tele a)

(Subst t a, Simplify a) => Simplify (Abs a)

Simplify a => Simplify (Closure a)

(Simplify a, Simplify b) => Simplify (a, b)

Simplify e => Simplify (Map k e)

Simplify t => Simplify (Named name t)

(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c)

simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t

Normalisation

class Normalise t where

Methods

normalise' :: t -> ReduceM t

Instances

Normalise Bool

Normalise Char

Normalise Int

Normalise EqualityView

Normalise ConPatternInfo

Normalise ClauseBody

Normalise LevelAtom

Normalise PlusLevel

Normalise Level

Normalise Sort

Normalise Type

Normalise Elim

Normalise Term

Normalise Candidate

Normalise DisplayForm

Normalise Constraint

Normalise ProblemConstraint

Normalise t => Normalise [t]

Normalise a => Normalise (Maybe a)

Normalise t => Normalise (Dom t)

Normalise t => Normalise (Arg t)

Normalise a => Normalise (Pattern' a)

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

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

Normalise a => Normalise (Closure a)

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

Normalise e => Normalise (Map k e)

Normalise t => Normalise (Named name t)

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

Full instantiation

class InstantiateFull t where

instantiateFull' instantiates metas everywhere (and recursively) but does not reduce.

Methods

instantiateFull' :: t -> ReduceM t

Instances

InstantiateFull Bool

InstantiateFull Char

InstantiateFull Int

InstantiateFull ModuleName

InstantiateFull QName

InstantiateFull Name

InstantiateFull Scope

InstantiateFull EqualityView

InstantiateFull Substitution

InstantiateFull ConPatternInfo

InstantiateFull ClauseBody

InstantiateFull Clause

InstantiateFull LevelAtom

InstantiateFull PlusLevel

InstantiateFull Level

InstantiateFull Sort

InstantiateFull Term

InstantiateFull CompiledClauses

InstantiateFull Candidate

InstantiateFull FunctionInverse

InstantiateFull Defn

InstantiateFull Definition

InstantiateFull RewriteRule

InstantiateFull NLPat

InstantiateFull DisplayTerm

InstantiateFull DisplayForm

InstantiateFull Section

InstantiateFull Signature

InstantiateFull Constraint

InstantiateFull ProblemConstraint

InstantiateFull Interface

InstantiateFull LHSResult

InstantiateFull t => InstantiateFull [t]

InstantiateFull a => InstantiateFull (Maybe a)

InstantiateFull t => InstantiateFull (Dom t)

InstantiateFull t => InstantiateFull (Arg t)

InstantiateFull a => InstantiateFull (Pattern' a)

(Subst t a, InstantiateFull a) => InstantiateFull (Tele a)

InstantiateFull a => InstantiateFull (Type' a)

(Subst t a, InstantiateFull a) => InstantiateFull (Abs a)

InstantiateFull a => InstantiateFull (Elim' a)

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)

InstantiateFull e => InstantiateFull (Map k e)

InstantiateFull e => InstantiateFull (HashMap k e)

InstantiateFull t => InstantiateFull (Named name t)

(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c)