Agda.TypeChecking.Reduce

Documentation

instantiate :: (Instantiate a, MonadReduce m) => a -> m a

instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a

reduce :: (Reduce a, MonadReduce m) => a -> m a

reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a)

reduceWithBlocker :: (Reduce a, IsMeta a, MonadReduce m) => a -> m (Blocker, a)

withReduced :: (Reduce a, IsMeta a, MonadReduce m, MonadBlock m) => a -> (a -> m b) -> m b

normalise :: (Normalise a, MonadReduce m) => a -> m a

normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t)

Normalise the given term but also preserve blocking tags TODO: implement a more efficient version of this.

simplify :: (Simplify a, MonadReduce m) => a -> m a

isFullyInstantiatedMeta :: MetaId -> TCM Bool

Meaning no metas left in the instantiation.

blockAll :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)

Blocking on all blockers.

blockAny :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)

Blocking on any blockers.

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

Nothing

Methods

instantiate' :: t -> ReduceM t

default instantiate' :: (t ~ f a, Traversable f, Instantiate a) => t -> ReduceM t

Instances

Instantiate EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: EqualityView -> ReduceM EqualityView

Instantiate Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Level -> ReduceM Level

Instantiate Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Sort -> ReduceM Sort

Instantiate Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Term -> ReduceM Term

Instantiate Blocker

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Blocker -> ReduceM Blocker

Instantiate Candidate

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Candidate -> ReduceM Candidate

Instantiate CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: CompareAs -> ReduceM CompareAs

Instantiate Constraint

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Constraint -> ReduceM Constraint

Instantiate t => Instantiate (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Abs t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate a => Instantiate (Blocked a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (PlusLevel' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Tele t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate a => Instantiate (Closure a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (IPBoundary' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate [t]

Defined in Agda.TypeChecking.Reduce

Methods

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

(Instantiate t, Instantiate e) => Instantiate (Dom' t e)

Defined in Agda.TypeChecking.Reduce

Methods

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

Instantiate t => Instantiate (Map k t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Reduction to weak head normal form.

class IsMeta a where

Is something (an elimination of) a meta variable? Does not perform any reductions.

Methods

isMeta :: a -> Maybe MetaId

Instances

IsMeta Term

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Term -> Maybe MetaId

IsMeta CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: CompareAs -> Maybe MetaId

IsMeta a => IsMeta (Arg a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Arg a -> Maybe MetaId

IsMeta a => IsMeta (Level' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Level' a -> Maybe MetaId

IsMeta a => IsMeta (PlusLevel' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: PlusLevel' a -> Maybe MetaId

IsMeta a => IsMeta (Sort' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Sort' a -> Maybe MetaId

IsMeta a => IsMeta (Elim' a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Elim' a -> Maybe MetaId

IsMeta a => IsMeta (Type'' t a)

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Type'' t a -> Maybe MetaId

ifBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m 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.

abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t

Throw pattern violation if blocked or a meta.

isBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> m (Maybe Blocker)

class Reduce t where

Minimal complete definition

Nothing

Methods

reduce' :: t -> ReduceM t

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

Instances

Reduce DeBruijnPattern

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern

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

Reduce Elim

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Elim -> ReduceM Elim

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

Reduce EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: EqualityView -> ReduceM EqualityView

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

Reduce Level

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Level -> ReduceM Level

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

Reduce PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: PlusLevel -> ReduceM PlusLevel

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

Reduce Sort

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Sort -> ReduceM Sort

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

Reduce Telescope

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope

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

Reduce Term

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Term -> ReduceM Term

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

Reduce Type

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Type -> ReduceM Type

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

Reduce Candidate

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Candidate -> ReduceM Candidate

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

Reduce CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: CompareAs -> ReduceM CompareAs

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

Reduce Constraint

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Constraint -> ReduceM Constraint

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

Reduce t => Reduce (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Reduce t => Reduce (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Reduce a => Reduce (Closure a)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Reduce t => Reduce (IPBoundary' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Reduce a => Reduce (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

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

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

Reduce t => Reduce [t]

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Reduce e => Reduce (Map k e)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

reduceIApply :: ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)

reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)

shouldTryFastReduce :: ReduceM Bool

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)

reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term)

Specialized version to put in boot file.

reduceDefCopy :: forall m. PureTCM m => QName -> Elims -> m (Reduced () Term)

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

reduceHead :: PureTCM m => Term -> m (Blocked Term)

Reduce simple (single clause) definitions.

unfoldInlined :: PureTCM m => Term -> m Term

Unfold a single inlined function.

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. We include reduction of IApply patterns, as `p i0` is akin to matcing on the i0 constructor of interval.

Minimal complete definition

Nothing

Methods

simplify' :: t -> ReduceM t

default simplify' :: (t ~ f a, Traversable f, Simplify a) => t -> ReduceM t

Instances

Simplify EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Simplify Level

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Level -> ReduceM Level

Simplify PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: PlusLevel -> ReduceM PlusLevel

Simplify Sort

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

Simplify Candidate

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Candidate -> ReduceM Candidate

Simplify CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: CompareAs -> ReduceM CompareAs

Simplify Constraint

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Constraint -> ReduceM Constraint

Simplify DisplayForm

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: DisplayForm -> ReduceM DisplayForm

Simplify ProblemConstraint

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: ProblemConstraint -> ReduceM ProblemConstraint

Simplify Bool

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Bool -> ReduceM Bool

Simplify t => Simplify (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify a => Simplify (Closure a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (IPBoundary' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify [t]

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Simplify t => Simplify (Map k t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Normalisation

class Normalise t where

Minimal complete definition

Nothing

Methods

normalise' :: t -> ReduceM t

default normalise' :: (t ~ f a, Traversable f, Normalise a) => t -> ReduceM t

Instances

Normalise ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo

Normalise DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar

Normalise EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: EqualityView -> ReduceM EqualityView

Normalise Level

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Level -> ReduceM Level

Normalise PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: PlusLevel -> ReduceM PlusLevel

Normalise Sort

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Sort -> ReduceM Sort

Normalise Term

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Term -> ReduceM Term

Normalise Candidate

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Candidate -> ReduceM Candidate

Normalise CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: CompareAs -> ReduceM CompareAs

Normalise Constraint

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Constraint -> ReduceM Constraint

Normalise DisplayForm

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: DisplayForm -> ReduceM DisplayForm

Normalise ProblemConstraint

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: ProblemConstraint -> ReduceM ProblemConstraint

Normalise Bool

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Bool -> ReduceM Bool

Normalise Char

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Char -> ReduceM Char

Normalise Int

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Int -> ReduceM Int

Normalise t => Normalise (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (WithHiding t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Dom t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise a => Normalise (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise a => Normalise (Closure a)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (IPBoundary' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise [t]

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

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

Normalise t => Normalise (Map k t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

slowNormaliseArgs :: Term -> ReduceM Term

Full instantiation

class InstantiateFull t where

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

Minimal complete definition

Nothing

Methods

instantiateFull' :: t -> ReduceM t

default instantiateFull' :: (t ~ f a, Traversable f, InstantiateFull a) => t -> ReduceM t

Instances

InstantiateFull ModuleName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ModuleName -> ReduceM ModuleName

InstantiateFull Name

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Name -> ReduceM Name

InstantiateFull QName

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: QName -> ReduceM QName

InstantiateFull Clause

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause

InstantiateFull ConHead

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConHead -> ReduceM ConHead

InstantiateFull ConPatternInfo

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo

InstantiateFull DBPatVar

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar

InstantiateFull EqualityView

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView

InstantiateFull Level

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Level -> ReduceM Level

InstantiateFull PlusLevel

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PlusLevel -> ReduceM PlusLevel

InstantiateFull Sort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Sort -> ReduceM Sort

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

InstantiateFull Term

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Term -> ReduceM Term

InstantiateFull Scope

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Scope -> ReduceM Scope

InstantiateFull CompiledClauses

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses

InstantiateFull Candidate

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Candidate -> ReduceM Candidate

InstantiateFull CompareAs

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: CompareAs -> ReduceM CompareAs

InstantiateFull Constraint

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Constraint -> ReduceM Constraint

InstantiateFull Definition

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Definition -> ReduceM Definition

InstantiateFull Defn

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Defn -> ReduceM Defn

InstantiateFull DisplayForm

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DisplayForm -> ReduceM DisplayForm

InstantiateFull DisplayTerm

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm

InstantiateFull ExtLamInfo

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ExtLamInfo -> ReduceM ExtLamInfo

InstantiateFull FunctionInverse

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

InstantiateFull Interface

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Interface -> ReduceM Interface

InstantiateFull NLPSort

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: NLPSort -> ReduceM NLPSort

InstantiateFull NLPType

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: NLPType -> ReduceM NLPType

InstantiateFull NLPat

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: NLPat -> ReduceM NLPat

InstantiateFull ProblemConstraint

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint

InstantiateFull RewriteRule

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: RewriteRule -> ReduceM RewriteRule

InstantiateFull Section

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Section -> ReduceM Section

InstantiateFull Signature

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Signature -> ReduceM Signature

InstantiateFull System

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: System -> ReduceM System

InstantiateFull LHSResult

Defined in Agda.TypeChecking.Rules.LHS

Methods

instantiateFull' :: LHSResult -> ReduceM LHSResult

InstantiateFull AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

instantiateFull' :: AsBinding -> ReduceM AsBinding

InstantiateFull Bool

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Bool -> ReduceM Bool

InstantiateFull Char

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Char -> ReduceM Char

InstantiateFull Int

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Int -> ReduceM Int

InstantiateFull t => InstantiateFull (Arg t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull a => InstantiateFull (Pattern' a)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Type' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Elim' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull a => InstantiateFull (Case a)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (WithArity t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull a => InstantiateFull (Builtin a)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull a => InstantiateFull (Closure a)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (IPBoundary' t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Open t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Maybe t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull [t]

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Named name t)

Defined in Agda.TypeChecking.Reduce

Methods

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

(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (Map k t)

Defined in Agda.TypeChecking.Reduce

Methods

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

InstantiateFull t => InstantiateFull (HashMap k t)

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

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

Defined in Agda.TypeChecking.Reduce

Methods

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

instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface

Instantiates everything except for definitions in the signature.

instantiateFullExceptForDefinitions :: MonadReduce m => Interface -> m Interface

Instantiates everything except for definitions in the signature.