| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce
Synopsis
- class Instantiate t
- instantiate' :: Instantiate t => t -> ReduceM t
- instantiate :: (Instantiate a, MonadReduce m) => a -> m a
- instantiateWhen :: (InstantiateFull a, MonadReduce m) => (MetaId -> ReduceM Bool) -> a -> m a
- class InstantiateFull t
- instantiateFull' :: InstantiateFull t => t -> ReduceM t
- instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a
- class IsMeta a
- isMeta :: IsMeta a => a -> Maybe MetaId
- class Reduce t
- reduce' :: Reduce t => t -> ReduceM t
- reduceB' :: Reduce t => t -> ReduceM (Blocked t)
- 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)
- reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term)
- reduceDefCopy :: PureTCM m => QName -> Elims -> m (Reduced () Term)
- reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term)
- reduceHead :: PureTCM m => Term -> m (Blocked Term)
- slowReduceTerm :: Term -> ReduceM (Blocked Term)
- unfoldCorecursion :: Term -> ReduceM (Blocked Term)
- unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
- unfoldDefinitionE :: (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term)
- unfoldDefinitionStep :: Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
- unfoldInlined :: PureTCM m => Term -> m Term
- appDef' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t
- ifBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
- isBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> m (Maybe Blocker)
- fromBlocked :: MonadBlock m => Blocked a -> m a
- blockOnError :: MonadError TCErr m => Blocker -> m a -> m a
- class Simplify t
- simplify :: (Simplify a, MonadReduce m) => a -> m a
- simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
- class Normalise t
- normalise' :: Normalise t => t -> ReduceM t
- normalise :: (Normalise a, MonadReduce m) => a -> m a
- slowNormaliseArgs :: Term -> ReduceM Term
Documentation
class Instantiate t 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).
Instances
instantiate' :: Instantiate t => t -> ReduceM t Source #
instantiate :: (Instantiate a, MonadReduce m) => a -> m a Source #
instantiateWhen :: (InstantiateFull a, MonadReduce m) => (MetaId -> ReduceM Bool) -> a -> m a Source #
A variant of instantiateFull that only instantiates those
meta-variables that satisfy the predicate.
class InstantiateFull t Source #
instantiateFull' instantiates metas everywhere (and recursively)
but does not reduce.
Instances
instantiateFull' :: InstantiateFull t => t -> ReduceM t Source #
instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a Source #
Is something (an elimination of) a meta variable? Does not perform any reductions.
Minimal complete definition
Instances
| IsMeta Term Source # | |
| IsMeta CompareAs Source # | |
| IsMeta a => IsMeta (Arg a) Source # | |
| IsMeta a => IsMeta (Level' a) Source # | |
| IsMeta a => IsMeta (PlusLevel' a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
| IsMeta a => IsMeta (Sort' a) Source # | |
| IsMeta a => IsMeta (Elim' a) Source # | |
| IsMeta a => IsMeta (Type'' t a) Source # | |
Instances
reduce :: (Reduce a, MonadReduce m) => a -> m a Source #
reduceWithBlocker :: (Reduce a, IsMeta a, MonadReduce m) => a -> m (Blocker, a) Source #
reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term) Source #
reduceDefCopy :: PureTCM m => QName -> Elims -> m (Reduced () Term) Source #
Reduce a non-primitive definition if it is a copy linking to another def.
reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term) Source #
Specialized version to put in boot file.
reduceHead :: PureTCM m => Term -> m (Blocked Term) Source #
Reduce simple (single clause) definitions.
unfoldDefinitionE :: (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term) Source #
appDef' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #
Apply a defined function to it's arguments, using the original clauses.
appDefE' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source #
abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t Source #
Throw pattern violation if blocked or a meta.
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.
fromBlocked :: MonadBlock m => Blocked a -> m a Source #
Throw a pattern violation if the argument is Blocked,
otherwise return the value embedded in the NotBlocked.
blockOnError :: MonadError TCErr m => Blocker -> m a -> m a Source #
Run the given computation but turn any errors into blocked computations with the given blocker
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.
Instances
simplify :: (Simplify a, MonadReduce m) => a -> m a Source #
Instances
normalise' :: Normalise t => t -> ReduceM t Source #
normalise :: (Normalise a, MonadReduce m) => a -> m a Source #