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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Reduce

Contents

- Reduction to weak head normal form.
- Simplification
- Normalisation
- Full instantiation

Synopsis

- 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)
- simplify :: (Simplify a, MonadReduce m) => a -> m a
- isFullyInstantiatedMeta :: MetaId -> TCM Bool
- blockAll :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)
- blockAny :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a)
- class Instantiate t where
  - instantiate' :: t -> ReduceM t
- class IsMeta a where
  - isMeta :: a -> Maybe MetaId
- ifBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
- abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t
- isBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> m (Maybe Blocker)
- class Reduce t where
  - reduce' :: t -> ReduceM t
  - reduceB' :: t -> ReduceM (Blocked t)
- 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)
- 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)
- reduceDefCopy :: forall m. PureTCM m => QName -> Elims -> m (Reduced () Term)
- reduceHead :: PureTCM m => Term -> m (Blocked Term)
- unfoldInlined :: PureTCM m => Term -> m Term
- appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- class Simplify t where
  - simplify' :: t -> ReduceM t
- simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
- class Normalise t where
  - normalise' :: t -> ReduceM t
- slowNormaliseArgs :: Term -> ReduceM Term
- class InstantiateFull t where
  - instantiateFull' :: t -> ReduceM t
- instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface
- instantiateFullExceptForDefinitions :: MonadReduce m => Interface -> m Interface

# Documentation

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

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

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

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

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

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

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

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

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

isFullyInstantiatedMeta :: MetaId -> TCM Bool Source #

Meaning no metas left in the instantiation.

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

Blocking on all blockers.

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

Blocking on any blockers.

class Instantiate t where Source #

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

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

#### Instances

Instances details

Instantiate EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: EqualityView -> ReduceM EqualityView Source #
Instantiate Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Level -> ReduceM Level Source #
Instantiate Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Sort -> ReduceM Sort Source #
Instantiate Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Term -> ReduceM Term Source #
Instantiate Blocker Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocker -> ReduceM Blocker Source #
Instantiate Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Candidate -> ReduceM Candidate Source #
Instantiate CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: CompareAs -> ReduceM CompareAs Source #
Instantiate Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Constraint -> ReduceM Constraint Source #
Instantiate t => Instantiate (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Arg t -> ReduceM (Arg t) Source #
Instantiate t => Instantiate (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Abs t -> ReduceM (Abs t) Source #
Instantiate a => Instantiate (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #
Instantiate t => Instantiate (PlusLevel' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: PlusLevel' t -> ReduceM (PlusLevel' t) Source #
Instantiate t => Instantiate (Tele t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Tele t -> ReduceM (Tele t) Source #
Instantiate t => Instantiate (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Type' t -> ReduceM (Type' t) Source #
Instantiate t => Instantiate (Elim' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Elim' t -> ReduceM (Elim' t) Source #
Instantiate a => Instantiate (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Closure a -> ReduceM (Closure a) Source #
Instantiate t => Instantiate (IPBoundary' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: IPBoundary' t -> ReduceM (IPBoundary' t) Source #
Instantiate t => Instantiate (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Maybe t -> ReduceM (Maybe t) Source #
Instantiate t => Instantiate (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Maybe t -> ReduceM (Maybe t) Source #
Instantiate t => Instantiate [t] Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: [t] -> ReduceM [t] Source #
(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Dom' t e -> ReduceM (Dom' t e) Source #
Instantiate t => Instantiate (Map k t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Map k t -> ReduceM (Map k t) Source #
(Instantiate a, Instantiate b) => Instantiate (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: (a, b) -> ReduceM (a, b) Source #
(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: (a, b, c) -> ReduceM (a, b, c) Source #

# Reduction to weak head normal form.

class IsMeta a where Source #

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

Methods

isMeta :: a -> Maybe MetaId Source #

#### Instances

Instances details

IsMeta Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Term -> Maybe MetaId Source #
IsMeta CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: CompareAs -> Maybe MetaId Source #
IsMeta a => IsMeta (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Arg a -> Maybe MetaId Source #
IsMeta a => IsMeta (Level' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Level' a -> Maybe MetaId Source #
IsMeta a => IsMeta (PlusLevel' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: PlusLevel' a -> Maybe MetaId Source #
IsMeta a => IsMeta (Sort' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Sort' a -> Maybe MetaId Source #
IsMeta a => IsMeta (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Elim' a -> Maybe MetaId Source #
IsMeta a => IsMeta (Type'' t a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods isMeta :: Type'' t a -> Maybe MetaId Source #

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

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

Throw pattern violation if blocked or a meta.

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

class Reduce t where Source #

Minimal complete definition

Nothing

Methods

reduce' :: t -> ReduceM t Source #

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

#### Instances

Instances details

Reduce DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source # reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #
Reduce Elim Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Elim -> ReduceM Elim Source # reduceB' :: Elim -> ReduceM (Blocked Elim) Source #
Reduce EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: EqualityView -> ReduceM EqualityView Source # reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #
Reduce Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Level -> ReduceM Level Source # reduceB' :: Level -> ReduceM (Blocked Level) Source #
Reduce PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: PlusLevel -> ReduceM PlusLevel Source # reduceB' :: PlusLevel -> ReduceM (Blocked PlusLevel) Source #
Reduce Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Sort -> ReduceM Sort Source # reduceB' :: Sort -> ReduceM (Blocked Sort) Source #
Reduce Telescope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Telescope -> ReduceM Telescope Source # reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #
Reduce Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Term -> ReduceM Term Source # reduceB' :: Term -> ReduceM (Blocked Term) Source #
Reduce Type Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Type -> ReduceM Type Source # reduceB' :: Type -> ReduceM (Blocked Type) Source #
Reduce Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Candidate -> ReduceM Candidate Source # reduceB' :: Candidate -> ReduceM (Blocked Candidate) Source #
Reduce CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: CompareAs -> ReduceM CompareAs Source # reduceB' :: CompareAs -> ReduceM (Blocked CompareAs) Source #
Reduce Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Constraint -> ReduceM Constraint Source # reduceB' :: Constraint -> ReduceM (Blocked Constraint) Source #
Reduce t => Reduce (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Arg t -> ReduceM (Arg t) Source # reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) Source #
(Subst a, Reduce a) => Reduce (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Abs a -> ReduceM (Abs a) Source # reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #
Reduce t => Reduce (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Dom t -> ReduceM (Dom t) Source # reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #
Reduce a => Reduce (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Closure a -> ReduceM (Closure a) Source # reduceB' :: Closure a -> ReduceM (Blocked (Closure a)) Source #
Reduce t => Reduce (IPBoundary' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: IPBoundary' t -> ReduceM (IPBoundary' t) Source # reduceB' :: IPBoundary' t -> ReduceM (Blocked (IPBoundary' t)) Source #
Reduce a => Reduce (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a) Source # reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a)) Source #
Reduce t => Reduce [t] Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: [t] -> ReduceM [t] Source # reduceB' :: [t] -> ReduceM (Blocked [t]) Source #
Reduce e => Reduce (Map k e) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: Map k e -> ReduceM (Map k e) Source # reduceB' :: Map k e -> ReduceM (Blocked (Map k e)) Source #
(Reduce a, Reduce b) => Reduce (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: (a, b) -> ReduceM (a, b) Source # reduceB' :: (a, b) -> ReduceM (Blocked (a, b)) Source #
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods reduce' :: (a, b, c) -> ReduceM (a, b, c) Source # reduceB' :: (a, b, c) -> ReduceM (Blocked (a, b, c)) Source #

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

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

shouldTryFastReduce :: ReduceM Bool Source #

maybeFastReduceTerm :: Term -> ReduceM (Blocked Term) Source #

slowReduceTerm :: Term -> ReduceM (Blocked Term) Source #

unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim) Source #

unfoldCorecursion :: Term -> ReduceM (Blocked Term) Source #

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.

unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term) Source #

unfoldDefinition' :: Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) Source #

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

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

Specialized version to put in boot file.

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

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

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

Reduce simple (single clause) definitions.

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

Unfold a single inlined function.

appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> 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.

appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #

appDef :: Term -> CompiledClauses -> RewriteRules -> 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.

appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #

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

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

appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #

# Simplification

class Simplify t where Source #

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

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

#### Instances

Instances details

Simplify EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: EqualityView -> ReduceM EqualityView Source #
Simplify Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Level -> ReduceM Level Source #
Simplify PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: PlusLevel -> ReduceM PlusLevel Source #
Simplify Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Sort -> ReduceM Sort Source #
Simplify Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Term -> ReduceM Term Source #
Simplify Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Candidate -> ReduceM Candidate Source #
Simplify CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: CompareAs -> ReduceM CompareAs Source #
Simplify Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Constraint -> ReduceM Constraint Source #
Simplify DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: DisplayForm -> ReduceM DisplayForm Source #
Simplify ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
Simplify Bool Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Bool -> ReduceM Bool Source #
Simplify t => Simplify (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Arg t -> ReduceM (Arg t) Source #
(Subst a, Simplify a) => Simplify (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Abs a -> ReduceM (Abs a) Source #
Simplify t => Simplify (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Dom t -> ReduceM (Dom t) Source #
(Subst a, Simplify a) => Simplify (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Tele a -> ReduceM (Tele a) Source #
Simplify t => Simplify (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Type' t -> ReduceM (Type' t) Source #
Simplify t => Simplify (Elim' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Elim' t -> ReduceM (Elim' t) Source #
Simplify a => Simplify (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Closure a -> ReduceM (Closure a) Source #
Simplify t => Simplify (IPBoundary' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: IPBoundary' t -> ReduceM (IPBoundary' t) Source #
Simplify t => Simplify (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Maybe t -> ReduceM (Maybe t) Source #
Simplify t => Simplify (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Maybe t -> ReduceM (Maybe t) Source #
Simplify t => Simplify [t] Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: [t] -> ReduceM [t] Source #
Simplify t => Simplify (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Named name t -> ReduceM (Named name t) Source #
Simplify t => Simplify (Map k t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: Map k t -> ReduceM (Map k t) Source #
(Simplify a, Simplify b) => Simplify (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: (a, b) -> ReduceM (a, b) Source #
(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods simplify' :: (a, b, c) -> ReduceM (a, b, c) Source #

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

# Normalisation

class Normalise t where Source #

Minimal complete definition

Nothing

Methods

normalise' :: t -> ReduceM t Source #

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

#### Instances

Instances details

Normalise ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source #
Normalise DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DBPatVar -> ReduceM DBPatVar Source #
Normalise EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: EqualityView -> ReduceM EqualityView Source #
Normalise Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Level -> ReduceM Level Source #
Normalise PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: PlusLevel -> ReduceM PlusLevel Source #
Normalise Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Sort -> ReduceM Sort Source #
Normalise Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Term -> ReduceM Term Source #
Normalise Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Candidate -> ReduceM Candidate Source #
Normalise CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: CompareAs -> ReduceM CompareAs Source #
Normalise Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Constraint -> ReduceM Constraint Source #
Normalise DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: DisplayForm -> ReduceM DisplayForm Source #
Normalise ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
Normalise Bool Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Bool -> ReduceM Bool Source #
Normalise Char Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Char -> ReduceM Char Source #
Normalise Int Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Int -> ReduceM Int Source #
Normalise t => Normalise (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Arg t -> ReduceM (Arg t) Source #
Normalise t => Normalise (WithHiding t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: WithHiding t -> ReduceM (WithHiding t) Source #
(Subst a, Normalise a) => Normalise (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Abs a -> ReduceM (Abs a) Source #
Normalise t => Normalise (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Dom t -> ReduceM (Dom t) Source #
Normalise a => Normalise (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Pattern' a -> ReduceM (Pattern' a) Source #
(Subst a, Normalise a) => Normalise (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Tele a -> ReduceM (Tele a) Source #
Normalise t => Normalise (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Type' t -> ReduceM (Type' t) Source #
Normalise t => Normalise (Elim' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Elim' t -> ReduceM (Elim' t) Source #
Normalise a => Normalise (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Closure a -> ReduceM (Closure a) Source #
Normalise t => Normalise (IPBoundary' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: IPBoundary' t -> ReduceM (IPBoundary' t) Source #
Normalise t => Normalise (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Maybe t -> ReduceM (Maybe t) Source #
Normalise t => Normalise (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Maybe t -> ReduceM (Maybe t) Source #
Normalise t => Normalise [t] Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: [t] -> ReduceM [t] Source #
Normalise t => Normalise (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Named name t -> ReduceM (Named name t) Source #
Normalise t => Normalise (Map k t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: Map k t -> ReduceM (Map k t) Source #
(Normalise a, Normalise b) => Normalise (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: (a, b) -> ReduceM (a, b) Source #
(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods normalise' :: (a, b, c) -> ReduceM (a, b, c) Source #

slowNormaliseArgs :: Term -> ReduceM Term Source #

# Full instantiation

class InstantiateFull t where Source #

`instantiateFull'` `instantiate`s metas everywhere (and recursively) but does not `reduce`.

Minimal complete definition

Nothing

Methods

instantiateFull' :: t -> ReduceM t Source #

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

#### Instances

Instances details

InstantiateFull ModuleName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ModuleName -> ReduceM ModuleName Source #
InstantiateFull Name Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Name -> ReduceM Name Source #
InstantiateFull QName Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: QName -> ReduceM QName Source #
InstantiateFull Clause Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Clause -> ReduceM Clause Source #
InstantiateFull ConHead Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConHead -> ReduceM ConHead Source #
InstantiateFull ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source #
InstantiateFull DBPatVar Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DBPatVar -> ReduceM DBPatVar Source #
InstantiateFull EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: EqualityView -> ReduceM EqualityView Source #
InstantiateFull Level Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Level -> ReduceM Level Source #
InstantiateFull PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PlusLevel -> ReduceM PlusLevel Source #
InstantiateFull Sort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Sort -> ReduceM Sort Source #
InstantiateFull Substitution Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source #
InstantiateFull Term Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Term -> ReduceM Term Source #
InstantiateFull Scope Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Scope -> ReduceM Scope Source #
InstantiateFull CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #
InstantiateFull Candidate Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Candidate -> ReduceM Candidate Source #
InstantiateFull CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompareAs -> ReduceM CompareAs Source #
InstantiateFull Constraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Constraint -> ReduceM Constraint Source #
InstantiateFull Definition Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Definition -> ReduceM Definition Source #
InstantiateFull Defn Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Defn -> ReduceM Defn Source #
InstantiateFull DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayForm -> ReduceM DisplayForm Source #
InstantiateFull DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm Source #
InstantiateFull ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ExtLamInfo -> ReduceM ExtLamInfo Source #
InstantiateFull FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #
InstantiateFull Interface Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Interface -> ReduceM Interface Source #
InstantiateFull NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPSort -> ReduceM NLPSort Source #
InstantiateFull NLPType Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPType -> ReduceM NLPType Source #
InstantiateFull NLPat Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: NLPat -> ReduceM NLPat Source #
InstantiateFull ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint Source #
InstantiateFull RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: RewriteRule -> ReduceM RewriteRule Source #
InstantiateFull Section Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Section -> ReduceM Section Source #
InstantiateFull Signature Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Signature -> ReduceM Signature Source #
InstantiateFull System Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: System -> ReduceM System Source #
InstantiateFull LHSResult Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods instantiateFull' :: LHSResult -> ReduceM LHSResult Source #
InstantiateFull AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods instantiateFull' :: AsBinding -> ReduceM AsBinding Source #
InstantiateFull Bool Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Bool -> ReduceM Bool Source #
InstantiateFull Char Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Char -> ReduceM Char Source #
InstantiateFull Int Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Int -> ReduceM Int Source #
InstantiateFull t => InstantiateFull (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Arg t -> ReduceM (Arg t) Source #
(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Abs a -> ReduceM (Abs a) Source #
InstantiateFull a => InstantiateFull (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) Source #
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Tele a -> ReduceM (Tele a) Source #
InstantiateFull t => InstantiateFull (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Type' t -> ReduceM (Type' t) Source #
InstantiateFull t => InstantiateFull (Elim' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Elim' t -> ReduceM (Elim' t) Source #
InstantiateFull a => InstantiateFull (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Case a -> ReduceM (Case a) Source #
InstantiateFull t => InstantiateFull (WithArity t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity t -> ReduceM (WithArity t) Source #
InstantiateFull a => InstantiateFull (Builtin a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Builtin a -> ReduceM (Builtin a) Source #
InstantiateFull a => InstantiateFull (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Closure a -> ReduceM (Closure a) Source #
InstantiateFull t => InstantiateFull (IPBoundary' t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: IPBoundary' t -> ReduceM (IPBoundary' t) Source #
InstantiateFull t => InstantiateFull (Open t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Open t -> ReduceM (Open t) Source #
InstantiateFull t => InstantiateFull (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Maybe t -> ReduceM (Maybe t) Source #
InstantiateFull t => InstantiateFull (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Maybe t -> ReduceM (Maybe t) Source #
InstantiateFull t => InstantiateFull [t] Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: [t] -> ReduceM [t] Source #
InstantiateFull t => InstantiateFull (Named name t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Named name t -> ReduceM (Named name t) Source #
(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Dom' t e -> ReduceM (Dom' t e) Source #
InstantiateFull t => InstantiateFull (Map k t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Map k t -> ReduceM (Map k t) Source #
InstantiateFull t => InstantiateFull (HashMap k t) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: HashMap k t -> ReduceM (HashMap k t) Source #
(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: (a, b) -> ReduceM (a, b) Source #
(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: (a, b, c) -> ReduceM (a, b, c) Source #
(InstantiateFull a, InstantiateFull b, InstantiateFull c, InstantiateFull d) => InstantiateFull (a, b, c, d) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: (a, b, c, d) -> ReduceM (a, b, c, d) Source #

instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface Source #

Instantiates everything except for definitions in the signature.

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

Instantiates everything except for definitions in the signature.