| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rewriting.NonLinPattern
Description
Various utility functions dealing with the non-linear, higher-order patterns used for rewrite rules.
Synopsis
- class PatternFrom a b where
- class NLPatToTerm p a where
- nlPatToTerm :: PureTCM m => p -> m a
- data PatVars = PatVars {}
- class NLPatVars a where
- nlPatVarsUnder :: Int -> a -> PatVars
- nlPatVars :: a -> PatVars
- class GetMatchables a where
- getMatchables :: a -> [QName]
- blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m ()
- assertPi :: Type -> TCM (Dom Type, Abs Type)
- errNotPi :: Type -> TCM a
- assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
- errNotPath :: Type -> TCM a
- assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
- errNotProjOf :: QName -> Type -> TCM a
- assertConOf :: ConHead -> Type -> TCM Type
- errNotConOf :: ConHead -> Type -> TCM a
Documentation
class PatternFrom a b where Source #
Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first two arguments indicate whether the pattern we are under is definitionally singular. Specifically, the first tracks the definitional singularity of the last |PDef|/|PBoundVar| match, while the second tracks the current definitional singularity. The third argument and fourth arguments, k0 and k1, partition the context into three chunks: the local context, the telescope of of pattern variables associated with the rewrite and the pattern-lambda bound variables. The fifth argument is the type of the term.
Instances
| PatternFrom Elims PElims Source # | |
| PatternFrom Level NLPat Source # | |
| PatternFrom Sort NLPSort Source # | |
| PatternFrom Term NLPat Source # | |
| PatternFrom Type NLPType Source # | |
| PatternFrom a b => PatternFrom (Arg a) (Arg b) Source # | |
| PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # | |
class NLPatToTerm p a where Source #
Convert from a non-linear pattern to a term.
Minimal complete definition
Nothing
Methods
nlPatToTerm :: PureTCM m => p -> m a Source #
default nlPatToTerm :: forall p' a' (f :: Type -> Type) m. (NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a', PureTCM m) => p -> m a Source #
Instances
Constructors
| PatVars | |
Fields
| |
class NLPatVars a where Source #
Gather the set of pattern variables of a non-linear pattern
Minimal complete definition
Nothing
Methods
nlPatVarsUnder :: Int -> a -> PatVars Source #
Instances
| NLPatVars NLPSort Source # | |
| NLPatVars NLPType Source # | |
| NLPatVars NLPat Source # | |
| NLPatVars PElims Source # | |
| NLPatVars a => NLPatVars (Arg a) Source # | |
| NLPatVars a => NLPatVars (Abs a) Source # | |
| NLPatVars a => NLPatVars (Dom a) Source # | |
| NLPatVars a => NLPatVars (Elim' a) Source # | |
| (NLPatVars a, NLPatVars b) => NLPatVars (a, b) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |
class GetMatchables a where Source #
Get all symbols that a non-linear pattern matches against
Minimal complete definition
Nothing
Methods
getMatchables :: a -> [QName] Source #
default getMatchables :: forall (f :: Type -> Type) a'. (Foldable f, GetMatchables a', a ~ f a') => a -> [QName] Source #
Instances
blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m () Source #
errNotPath :: Type -> TCM a Source #