| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce
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
- 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
- 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
- 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 #
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 #
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
Reduction to weak head normal form.
Is something (an elimination of) a meta variable? Does not perform any reductions.
Instances
| IsMeta Term Source # | |
| IsMeta CompareAs Source # | |
| IsMeta a => IsMeta (Arg a) Source # | |
| IsMeta a => IsMeta (Elim' a) Source # | |
| IsMeta a => IsMeta (PlusLevel' a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta a => IsMeta (Level' a) Source # | |
| IsMeta a => IsMeta (Sort' a) Source # | |
| IsMeta a => IsMeta (Type'' t a) 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.
Minimal complete definition
Nothing
Instances
reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> 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.
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
Instances
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
Full instantiation
class InstantiateFull t where Source #
instantiateFull' instantiates 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
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.