Agda-2.4.2.3: 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

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

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.

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 Name 
InstantiateFull ModuleName 
InstantiateFull QName 
InstantiateFull Scope 
InstantiateFull Substitution 
InstantiateFull ConPatternInfo 
InstantiateFull Pattern 
InstantiateFull ClauseBody 
InstantiateFull Clause 
InstantiateFull LevelAtom 
InstantiateFull PlusLevel 
InstantiateFull Level 
InstantiateFull Sort 
InstantiateFull Type 
InstantiateFull Term 
InstantiateFull CompiledClauses 
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) 
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) 
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) 
InstantiateFull a => InstantiateFull (Elim' a) 
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)