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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Reduce

Contents

Synopsis

Documentation

reduce :: Reduce a => a -> TCM a Source

reduceB :: Reduce a => a -> TCM (Blocked a) Source

normalise :: Normalise a => a -> TCM a Source

simplify :: Simplify a => a -> TCM a Source

Reduction to weak head normal form.

ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a Source

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 Source

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

unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term) Source

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

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

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

reduceHead :: Term -> TCM (Blocked Term) Source

Reduce simple (single clause) definitions.

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

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) Source

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) Source

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

Simplification

Normalisation

Full instantiation

class InstantiateFull t where Source

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

Instances

InstantiateFull Bool Source 
InstantiateFull Char Source 
InstantiateFull Int Source 
InstantiateFull ModuleName Source 
InstantiateFull QName Source 
InstantiateFull Name Source 
InstantiateFull Scope Source 
InstantiateFull EqualityView Source 
InstantiateFull Substitution Source 
InstantiateFull ConPatternInfo Source 
InstantiateFull ClauseBody Source 
InstantiateFull Clause Source 
InstantiateFull LevelAtom Source 
InstantiateFull PlusLevel Source 
InstantiateFull Level Source 
InstantiateFull Sort Source 
InstantiateFull Term Source 
InstantiateFull CompiledClauses Source 
InstantiateFull Candidate Source 
InstantiateFull FunctionInverse Source 
InstantiateFull Defn Source 
InstantiateFull Definition Source 
InstantiateFull RewriteRule Source 
InstantiateFull NLPat Source 
InstantiateFull DisplayTerm Source 
InstantiateFull DisplayForm Source 
InstantiateFull Section Source 
InstantiateFull Signature Source 
InstantiateFull Constraint Source 
InstantiateFull ProblemConstraint Source 
InstantiateFull Interface Source 
InstantiateFull LHSResult Source 
InstantiateFull t => InstantiateFull [t] Source 
InstantiateFull a => InstantiateFull (Maybe a) Source 
InstantiateFull t => InstantiateFull (Dom t) Source 
InstantiateFull t => InstantiateFull (Arg t) Source 
InstantiateFull a => InstantiateFull (Pattern' a) Source 
(Subst t a, InstantiateFull a) => InstantiateFull (Tele a) Source 
InstantiateFull a => InstantiateFull (Type' a) Source 
(Subst t a, InstantiateFull a) => InstantiateFull (Abs a) Source 
InstantiateFull a => InstantiateFull (Elim' a) Source 
InstantiateFull a => InstantiateFull (Case a) Source 
InstantiateFull a => InstantiateFull (WithArity a) Source 
InstantiateFull a => InstantiateFull (Builtin a) Source 
InstantiateFull a => InstantiateFull (Open a) Source 
InstantiateFull a => InstantiateFull (Closure a) Source 
(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b) Source 
InstantiateFull e => InstantiateFull (Map k e) Source 
InstantiateFull e => InstantiateFull (HashMap k e) Source 
InstantiateFull t => InstantiateFull (Named name t) Source 
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) Source