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

isFullyInstantiatedMeta :: MetaId -> TCM Bool

Meaning no metas left in the instantiation.

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

Minimal complete definition

instantiate'

Methods

instantiate' :: t -> ReduceM t

Instances

Instantiate EqualityView

Methods

instantiate' :: EqualityView -> ReduceM EqualityView

Instantiate LevelAtom

Methods

instantiate' :: LevelAtom -> ReduceM LevelAtom

Instantiate PlusLevel

Methods

instantiate' :: PlusLevel -> ReduceM PlusLevel

Instantiate Level

Methods

instantiate' :: Level -> ReduceM Level

Instantiate Sort

Methods

instantiate' :: Sort -> ReduceM Sort

Instantiate Telescope

Methods

instantiate' :: Telescope -> ReduceM Telescope

Instantiate Type

Methods

instantiate' :: Type -> ReduceM Type

Instantiate Elim

Methods

instantiate' :: Elim -> ReduceM Elim

Instantiate Term

Methods

instantiate' :: Term -> ReduceM Term

Instantiate Candidate

Methods

instantiate' :: Candidate -> ReduceM Candidate

Instantiate Constraint

Methods

instantiate' :: Constraint -> ReduceM Constraint

Instantiate t => Instantiate [t]

Methods

instantiate' :: [t] -> ReduceM [t]

Instantiate t => Instantiate (Dom t)

Methods

instantiate' :: Dom t -> ReduceM (Dom t)

Instantiate t => Instantiate (Arg t)

Methods

instantiate' :: Arg t -> ReduceM (Arg t)

Instantiate a => Instantiate (Blocked a)

Methods

instantiate' :: Blocked a -> ReduceM (Blocked a)

Instantiate t => Instantiate (Abs t)

Methods

instantiate' :: Abs t -> ReduceM (Abs t)

Instantiate a => Instantiate (Closure a)

Methods

instantiate' :: Closure a -> ReduceM (Closure a)

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

Methods

instantiate' :: (a, b) -> ReduceM (a, b)

Instantiate e => Instantiate (Map k e)

Methods

instantiate' :: Map k e -> ReduceM (Map k e)

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

Methods

instantiate' :: (a, b, c) -> ReduceM (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

Methods

reduce' :: t -> ReduceM t

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

Instances

Reduce EqualityView

Methods

reduce' :: EqualityView -> ReduceM EqualityView

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

Reduce LevelAtom

Methods

reduce' :: LevelAtom -> ReduceM LevelAtom

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

Reduce PlusLevel

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

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

Reduce Level

Methods

reduce' :: Level -> ReduceM Level

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

Reduce Sort

Methods

reduce' :: Sort -> ReduceM Sort

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

Reduce Telescope

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Reduce Type

Methods

reduce' :: Type -> ReduceM Type

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

Reduce Elim

Methods

reduce' :: Elim -> ReduceM Elim

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

Reduce Term

Methods

reduce' :: Term -> ReduceM Term

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

Reduce Candidate

Methods

reduce' :: Candidate -> ReduceM Candidate

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

Reduce Constraint

Methods

reduce' :: Constraint -> ReduceM Constraint

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

Reduce t => Reduce [t]

Methods

reduce' :: [t] -> ReduceM [t]

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

Reduce t => Reduce (Dom t)

Methods

reduce' :: Dom t -> ReduceM (Dom t)

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

Reduce t => Reduce (Arg t)

Methods

reduce' :: Arg t -> ReduceM (Arg t)

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

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

Methods

reduce' :: Abs a -> ReduceM (Abs a)

reduceB' :: Abs a -> ReduceM (Blocked (Abs a))

Reduce a => Reduce (Closure a)

Methods

reduce' :: Closure a -> ReduceM (Closure a)

reduceB' :: Closure a -> ReduceM (Blocked (Closure a))

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

Methods

reduce' :: (a, b) -> ReduceM (a, b)

reduceB' :: (a, b) -> ReduceM (Blocked (a, b))

Reduce e => Reduce (Map k e)

Methods

reduce' :: Map k e -> ReduceM (Map k e)

reduceB' :: Map k e -> ReduceM (Blocked (Map k e))

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

Methods

reduce' :: (a, b, c) -> ReduceM (a, b, c)

reduceB' :: (a, b, c) -> ReduceM (Blocked (a, b, c))

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term)

slowReduceTerm :: 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 -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)

unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)

reduceDefCopy :: QName -> Elims -> 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 -> RewriteRules -> 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 -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)

appDef :: Term -> CompiledClauses -> RewriteRules -> 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 -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)

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

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

appDefE' :: Term -> [Clause] -> RewriteRules -> 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.

Minimal complete definition

simplify'

Methods

simplify' :: t -> ReduceM t

Instances

Simplify Bool

Methods

simplify' :: Bool -> ReduceM Bool

Simplify EqualityView

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Simplify LevelAtom

Methods

simplify' :: LevelAtom -> ReduceM LevelAtom

Simplify PlusLevel

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Simplify Level

Methods

simplify' :: Level -> ReduceM Level

Simplify Sort

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Type

Methods

simplify' :: Type -> ReduceM Type

Simplify Elim

Methods

simplify' :: Elim -> ReduceM Elim

Simplify Term

Methods

simplify' :: Term -> ReduceM Term

Simplify Candidate

Methods

simplify' :: Candidate -> ReduceM Candidate

Simplify DisplayForm

Methods

simplify' :: DisplayForm -> ReduceM DisplayForm

Simplify Constraint

Methods

simplify' :: Constraint -> ReduceM Constraint

Simplify ProblemConstraint

Methods

simplify' :: ProblemConstraint -> ReduceM ProblemConstraint

Simplify t => Simplify [t]

Methods

simplify' :: [t] -> ReduceM [t]

Simplify a => Simplify (Maybe a)

Methods

simplify' :: Maybe a -> ReduceM (Maybe a)

Simplify t => Simplify (Dom t)

Methods

simplify' :: Dom t -> ReduceM (Dom t)

Simplify t => Simplify (Arg t)

Methods

simplify' :: Arg t -> ReduceM (Arg t)

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

Methods

simplify' :: Tele a -> ReduceM (Tele a)

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

Methods

simplify' :: Abs a -> ReduceM (Abs a)

Simplify a => Simplify (Closure a)

Methods

simplify' :: Closure a -> ReduceM (Closure a)

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

Methods

simplify' :: (a, b) -> ReduceM (a, b)

Simplify e => Simplify (Map k e)

Methods

simplify' :: Map k e -> ReduceM (Map k e)

Simplify t => Simplify (Named name t)

Methods

simplify' :: Named name t -> ReduceM (Named name t)

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

Methods

simplify' :: (a, b, c) -> ReduceM (a, b, c)

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

Normalisation

class Normalise t where

Minimal complete definition

normalise'

Methods

normalise' :: t -> ReduceM t

Instances

Normalise Bool

Methods

normalise' :: Bool -> ReduceM Bool

Normalise Char

Methods

normalise' :: Char -> ReduceM Char

Normalise Int

Methods

normalise' :: Int -> ReduceM Int

Normalise EqualityView

Methods

normalise' :: EqualityView -> ReduceM EqualityView

Normalise ConPatternInfo

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo

Normalise DBPatVar

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar

Normalise LevelAtom

Methods

normalise' :: LevelAtom -> ReduceM LevelAtom

Normalise PlusLevel

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Normalise Level

Methods

normalise' :: Level -> ReduceM Level

Normalise Sort

Methods

normalise' :: Sort -> ReduceM Sort

Normalise Type

Methods

normalise' :: Type -> ReduceM Type

Normalise Elim

Methods

normalise' :: Elim -> ReduceM Elim

Normalise Term

Methods

normalise' :: Term -> ReduceM Term

Normalise Candidate

Methods

normalise' :: Candidate -> ReduceM Candidate

Normalise DisplayForm

Methods

normalise' :: DisplayForm -> ReduceM DisplayForm

Normalise Constraint

Methods

normalise' :: Constraint -> ReduceM Constraint

Normalise ProblemConstraint

Methods

normalise' :: ProblemConstraint -> ReduceM ProblemConstraint

Normalise t => Normalise [t]

Methods

normalise' :: [t] -> ReduceM [t]

Normalise a => Normalise (Maybe a)

Methods

normalise' :: Maybe a -> ReduceM (Maybe a)

Normalise t => Normalise (Dom t)

Methods

normalise' :: Dom t -> ReduceM (Dom t)

Normalise t => Normalise (Arg t)

Methods

normalise' :: Arg t -> ReduceM (Arg t)

Normalise a => Normalise (Pattern' a)

Methods

normalise' :: Pattern' a -> ReduceM (Pattern' a)

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

Methods

normalise' :: Tele a -> ReduceM (Tele a)

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

Methods

normalise' :: Abs a -> ReduceM (Abs a)

Normalise a => Normalise (Closure a)

Methods

normalise' :: Closure a -> ReduceM (Closure a)

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

Methods

normalise' :: (a, b) -> ReduceM (a, b)

Normalise e => Normalise (Map k e)

Methods

normalise' :: Map k e -> ReduceM (Map k e)

Normalise t => Normalise (Named name t)

Methods

normalise' :: Named name t -> ReduceM (Named name t)

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

Methods

normalise' :: (a, b, c) -> ReduceM (a, b, c)

Full instantiation

class InstantiateFull t where

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

Minimal complete definition

instantiateFull'

Methods

instantiateFull' :: t -> ReduceM t

Instances

InstantiateFull Bool

Methods

instantiateFull' :: Bool -> ReduceM Bool

InstantiateFull Char

Methods

instantiateFull' :: Char -> ReduceM Char

InstantiateFull Int

Methods

instantiateFull' :: Int -> ReduceM Int

InstantiateFull ModuleName

Methods

instantiateFull' :: ModuleName -> ReduceM ModuleName

InstantiateFull QName

Methods

instantiateFull' :: QName -> ReduceM QName

InstantiateFull Name

Methods

instantiateFull' :: Name -> ReduceM Name

InstantiateFull Scope

Methods

instantiateFull' :: Scope -> ReduceM Scope

InstantiateFull EqualityView

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView

InstantiateFull Substitution

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

InstantiateFull ConPatternInfo

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo

InstantiateFull DBPatVar

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar

InstantiateFull Clause

Methods

instantiateFull' :: Clause -> ReduceM Clause

InstantiateFull LevelAtom

Methods

instantiateFull' :: LevelAtom -> ReduceM LevelAtom

InstantiateFull PlusLevel

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

InstantiateFull Level

Methods

instantiateFull' :: Level -> ReduceM Level

InstantiateFull Sort

Methods

instantiateFull' :: Sort -> ReduceM Sort

InstantiateFull Term

Methods

instantiateFull' :: Term -> ReduceM Term

InstantiateFull CompiledClauses

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

InstantiateFull Candidate

Methods

instantiateFull' :: Candidate -> ReduceM Candidate

InstantiateFull FunctionInverse

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

InstantiateFull Defn

Methods

instantiateFull' :: Defn -> ReduceM Defn

InstantiateFull Definition

Methods

instantiateFull' :: Definition -> ReduceM Definition

InstantiateFull RewriteRule

Methods

instantiateFull' :: RewriteRule -> ReduceM RewriteRule

InstantiateFull NLPType

Methods

instantiateFull' :: NLPType -> ReduceM NLPType

InstantiateFull NLPat

Methods

instantiateFull' :: NLPat -> ReduceM NLPat

InstantiateFull DisplayTerm

Methods

instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm

InstantiateFull DisplayForm

Methods

instantiateFull' :: DisplayForm -> ReduceM DisplayForm

InstantiateFull Section

Methods

instantiateFull' :: Section -> ReduceM Section

InstantiateFull Signature

Methods

instantiateFull' :: Signature -> ReduceM Signature

InstantiateFull Constraint

Methods

instantiateFull' :: Constraint -> ReduceM Constraint

InstantiateFull ProblemConstraint

Methods

instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint

InstantiateFull Interface

Methods

instantiateFull' :: Interface -> ReduceM Interface

InstantiateFull AsBinding

Methods

instantiateFull' :: AsBinding -> ReduceM AsBinding

InstantiateFull LHSResult

Methods

instantiateFull' :: LHSResult -> ReduceM LHSResult

InstantiateFull t => InstantiateFull [t]

Methods

instantiateFull' :: [t] -> ReduceM [t]

InstantiateFull a => InstantiateFull (Maybe a)

Methods

instantiateFull' :: Maybe a -> ReduceM (Maybe a)

InstantiateFull t => InstantiateFull (Dom t)

Methods

instantiateFull' :: Dom t -> ReduceM (Dom t)

InstantiateFull t => InstantiateFull (Arg t)

Methods

instantiateFull' :: Arg t -> ReduceM (Arg t)

InstantiateFull a => InstantiateFull (Pattern' a)

Methods

instantiateFull' :: Pattern' a -> ReduceM (Pattern' a)

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

Methods

instantiateFull' :: Tele a -> ReduceM (Tele a)

InstantiateFull a => InstantiateFull (Type' a)

Methods

instantiateFull' :: Type' a -> ReduceM (Type' a)

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

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a)

InstantiateFull a => InstantiateFull (Elim' a)

Methods

instantiateFull' :: Elim' a -> ReduceM (Elim' a)

InstantiateFull a => InstantiateFull (Case a)

Methods

instantiateFull' :: Case a -> ReduceM (Case a)

InstantiateFull a => InstantiateFull (WithArity a)

Methods

instantiateFull' :: WithArity a -> ReduceM (WithArity a)

InstantiateFull a => InstantiateFull (Builtin a)

Methods

instantiateFull' :: Builtin a -> ReduceM (Builtin a)

InstantiateFull a => InstantiateFull (Local a)

Methods

instantiateFull' :: Local a -> ReduceM (Local a)

InstantiateFull a => InstantiateFull (Open a)

Methods

instantiateFull' :: Open a -> ReduceM (Open a)

InstantiateFull a => InstantiateFull (Closure a)

Methods

instantiateFull' :: Closure a -> ReduceM (Closure a)

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

Methods

instantiateFull' :: (a, b) -> ReduceM (a, b)

InstantiateFull e => InstantiateFull (Map k e)

Methods

instantiateFull' :: Map k e -> ReduceM (Map k e)

InstantiateFull e => InstantiateFull (HashMap k e)

Methods

instantiateFull' :: HashMap k e -> ReduceM (HashMap k e)

InstantiateFull t => InstantiateFull (Named name t)

Methods

instantiateFull' :: Named name t -> ReduceM (Named name t)

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

Methods

instantiateFull' :: (a, b, c) -> ReduceM (a, b, c)