| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rewriting.NonLinPattern
Contents
Description
Various utility functions dealing with the non-linear, higher-order patterns used for rewrite rules.
Synopsis
- class PatternFrom a b where
- patternFrom :: Relevance -> Int -> TypeOf a -> a -> TCM b
- class NLPatToTerm p a where
- nlPatToTerm :: PureTCM m => p -> m a
- class NLPatVars a where
- nlPatVarsUnder :: Int -> a -> IntSet
- nlPatVars :: a -> IntSet
- 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 argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.
Instances
| PatternFrom Level NLPat Source # | |
| PatternFrom Sort NLPSort Source # | |
| PatternFrom Term NLPat Source # | |
| PatternFrom Type NLPType Source # | |
| PatternFrom Elims [Elim' NLPat] 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
class NLPatVars a where Source #
Gather the set of pattern variables of a non-linear pattern
Minimal complete definition
Instances
| NLPatVars NLPSort Source # | |
| NLPatVars NLPType Source # | |
| NLPatVars NLPat Source # | |
| NLPatVars a => NLPatVars (Abs a) Source # | |
| (Foldable f, NLPatVars a) => NLPatVars (f a) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |
| (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 #