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 #