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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Reduce

Contents

Synopsis

Documentation

instantiate :: Instantiate 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

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

Minimal complete definition

Nothing

Methods

reduce' :: t -> ReduceM t

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

Instances

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.

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.

reduceHead :: Term -> TCM (Blocked Term)

Reduce simple (single clause) definitions.

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.

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.

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

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

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

Normalisation

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 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) 
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) 
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) 
InstantiateFull t => InstantiateFull (Dom t) 
InstantiateFull t => InstantiateFull (Arg 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 t => InstantiateFull (Named name t) 
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c)