Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rewriting.NonLinPattern

Description

Various utility functions dealing with the non-linear, higher-order patterns used for rewrite rules.

Synopsis

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 #

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 :: (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

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 :: (Foldable f, GetMatchables a', a ~ f a') => a -> [QName] Source #

Instances

Instances details
GetMatchables Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

GetMatchables NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

GetMatchables NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

GetMatchables NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

GetMatchables RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

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 #

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 #