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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rewriting.NonLinPattern

Contents

- Orphan instances

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.

Methods

patternFrom :: Relevance -> Int -> TypeOf a -> a -> TCM b Source #

#### Instances

Instances details

PatternFrom Level NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Level -> Level -> TCM NLPat Source #
PatternFrom Sort NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Sort -> Sort -> TCM NLPSort Source #
PatternFrom Term NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat Source #
PatternFrom Type NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType Source #
PatternFrom Elims [Elim' NLPat] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat] Source #
PatternFrom a b => PatternFrom (Arg a) (Arg b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b) Source #
PatternFrom a b => PatternFrom (Dom a) (Dom b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (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

Instances details

NLPatToTerm Nat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Nat -> m Term Source #
NLPatToTerm NLPSort Sort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPSort -> m Sort Source #
NLPatToTerm NLPType Type Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPType -> m Type Source #
NLPatToTerm NLPat Level Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPat -> m Level Source #
NLPatToTerm NLPat Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => NLPat -> m Term Source #
NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Arg p -> m (Arg a) Source #
NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Abs p -> m (Abs a) Source #
NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Dom p -> m (Dom a) Source #
NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => Elim' p -> m (Elim' a) Source #
NLPatToTerm p a => NLPatToTerm [p] [a] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatToTerm :: PureTCM m => [p] -> m [a] Source #

class NLPatVars a where Source #

Gather the set of pattern variables of a non-linear pattern

Minimal complete definition

nlPatVarsUnder

Methods

nlPatVarsUnder :: Int -> a -> IntSet Source #

nlPatVars :: a -> IntSet Source #

#### Instances

Instances details

NLPatVars NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> NLPSort -> IntSet Source # nlPatVars :: NLPSort -> IntSet Source #
NLPatVars NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> NLPType -> IntSet Source # nlPatVars :: NLPType -> IntSet Source #
NLPatVars NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> NLPat -> IntSet Source # nlPatVars :: NLPat -> IntSet Source #
NLPatVars a => NLPatVars (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> Abs a -> IntSet Source # nlPatVars :: Abs a -> IntSet Source #
(Foldable f, NLPatVars a) => NLPatVars (f a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> f a -> IntSet Source # nlPatVars :: f a -> IntSet Source #
(NLPatVars a, NLPatVars b) => NLPatVars (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods nlPatVarsUnder :: Int -> (a, b) -> IntSet Source # nlPatVars :: (a, b) -> IntSet Source #

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

Instances details

GetMatchables Term Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Term -> [QName] Source #
GetMatchables NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: NLPSort -> [QName] Source #
GetMatchables NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: NLPType -> [QName] Source #
GetMatchables NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: NLPat -> [QName] Source #
GetMatchables RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: RewriteRule -> [QName] Source #
GetMatchables a => GetMatchables (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Arg a -> [QName] Source #
GetMatchables a => GetMatchables (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Abs a -> [QName] Source #
GetMatchables a => GetMatchables (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Dom a -> [QName] Source #
GetMatchables a => GetMatchables (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Elim' a -> [QName] Source #
GetMatchables a => GetMatchables [a] Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: [a] -> [QName] Source #
(GetMatchables a, GetMatchables b) => GetMatchables (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: (a, b) -> [QName] Source #

blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m () Source #

assertPi :: Type -> TCM (Dom Type, Abs Type) Source #

errNotPi :: Type -> TCM a Source #

assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term) Source #

errNotPath :: Type -> TCM a Source #

assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type) Source #

errNotProjOf :: QName -> Type -> TCM a Source #

assertConOf :: ConHead -> Type -> TCM Type Source #

errNotConOf :: ConHead -> Type -> TCM a Source #

# Orphan instances

Free NLPSort Source # |
Instance details Methods freeVars' :: IsVarSet a c => NLPSort -> FreeM a c Source #
Free NLPType Source # |
Instance details Methods freeVars' :: IsVarSet a c => NLPType -> FreeM a c Source #
Free NLPat Source # | Only computes free variables that are not bound (see `nlPatVars`), i.e., those in a `PTerm`.
Instance details Methods freeVars' :: IsVarSet a c => NLPat -> FreeM a c Source #