Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Syntax.Internal
Synopsis
- class TermSize a where
- data Suggestion = forall a.Suggest a => Suggestion a
- class Suggest a where
- suggestName :: a -> Maybe String
- class SgTel a where
- class TelToArgs a where
- type ListTel = ListTel' ArgName
- type ListTel' a = [Dom (a, Type)]
- type DummyTermKind = String
- data IntervalView
- data PathView
- data EqualityView
- type PatternSubstitution = Substitution' DeBruijnPattern
- type Substitution = Substitution' Term
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- class PatternVars a where
- type PatternVarOut a
- patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]
- data ConPatternInfo = ConPatternInfo {
- conPInfo :: PatternInfo
- conPRecord :: Bool
- conPFallThrough :: Bool
- conPType :: Maybe (Arg Type)
- conPLazy :: Bool
- type DeBruijnPattern = Pattern' DBPatVar
- data DBPatVar = DBPatVar {
- dbPatVarName :: PatVarName
- dbPatVarIndex :: Int
- type Pattern = Pattern' PatVarName
- data Pattern' x
- = VarP PatternInfo x
- | DotP PatternInfo Term
- | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
- | LitP PatternInfo Literal
- | ProjP ProjOrigin QName
- | IApplyP PatternInfo Term Term x
- | DefP PatternInfo QName [NamedArg (Pattern' x)]
- data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
- data PatternInfo = PatternInfo {
- patOrigin :: PatOrigin
- patAsNames :: [Name]
- type PatVarName = ArgName
- data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: NAPs
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Bool
- clauseExact :: Maybe Bool
- clauseRecursive :: Maybe Bool
- clauseUnreachable :: Maybe Bool
- clauseEllipsis :: ExpandedEllipsis
- type NAPs = [NamedArg DeBruijnPattern]
- type Blocked_ = Blocked ()
- type NotBlocked = NotBlocked' Term
- type Blocked = Blocked' Term
- newtype BraveTerm = BraveTerm {}
- type LevelAtom = Term
- type PlusLevel = PlusLevel' Term
- data PlusLevel' t = Plus Integer t
- type Level = Level' Term
- data Level' t = Max Integer [PlusLevel' t]
- type Sort = Sort' Term
- data Sort' t
- data IsFibrant
- type Telescope = Tele (Dom Type)
- data Tele a
- class LensSort a where
- type Type = Type' Term
- type Type' a = Type'' Term a
- data Type'' t a = El {}
- data Abs a
- type Elims = [Elim]
- type Elim = Elim' Term
- type ConInfo = ConOrigin
- data Term
- class LensConName a where
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
- data ConHead = ConHead {
- conName :: QName
- conDataRecord :: DataOrRecord
- conInductive :: Induction
- conFields :: [Arg QName]
- data DataOrRecord
- type NamedArgs = [NamedArg Term]
- type Args = [Arg Term]
- type Dom = Dom' Term
- data Dom' t e = Dom {}
- pattern ClosedLevel :: Integer -> Level
- argFromDom :: Dom' t a -> Arg a
- namedArgFromDom :: Dom' t a -> NamedArg a
- domFromArg :: Arg a -> Dom a
- domFromNamedArg :: NamedArg a -> Dom a
- defaultDom :: a -> Dom a
- defaultArgDom :: ArgInfo -> a -> Dom a
- defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
- clausePats :: Clause -> [Arg DeBruijnPattern]
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- defaultPatternInfo :: PatternInfo
- varP :: a -> Pattern' a
- dotP :: Term -> Pattern' a
- litP :: Literal -> Pattern' a
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- absurdP :: Int -> DeBruijnPattern
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- patternInfo :: Pattern' x -> Maybe PatternInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- properlyMatching :: Pattern' a -> Bool
- properlyMatching' :: Bool -> Bool -> Pattern' a -> Bool
- isEqualityType :: EqualityView -> Bool
- isPathType :: PathView -> Bool
- isIOne :: IntervalView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- absurdPatternName :: PatVarName
- isAbsurdPatternName :: PatVarName -> Bool
- var :: Nat -> Term
- dontCare :: Term -> Term
- dummyLocName :: CallStack -> String
- dummyTermWith :: DummyTermKind -> CallStack -> Term
- dummyLevel :: CallStack -> Level
- dummyTerm :: CallStack -> Term
- __DUMMY_TERM__ :: HasCallStack => Term
- __DUMMY_LEVEL__ :: HasCallStack => Level
- dummySort :: CallStack -> Sort
- __DUMMY_SORT__ :: HasCallStack => Sort
- dummyType :: CallStack -> Type
- __DUMMY_TYPE__ :: HasCallStack => Type
- dummyDom :: CallStack -> Dom Type
- __DUMMY_DOM__ :: HasCallStack => Dom Type
- atomicLevel :: t -> Level' t
- varSort :: Int -> Sort
- tmSort :: Term -> Sort
- tmSSort :: Term -> Sort
- levelPlus :: Integer -> Level -> Level
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- mkProp :: Integer -> Sort
- mkSSet :: Integer -> Sort
- isSort :: Term -> Maybe Sort
- impossibleTerm :: CallStack -> Term
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- listTel :: Lens' ListTel Telescope
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- suggests :: [Suggestion] -> String
- unSpine :: Term -> Term
- unSpine' :: (ProjOrigin -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- pDom :: LensHiding a => a -> Doc -> Doc
- prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
- module Agda.Syntax.Internal.Blockers
- module Agda.Syntax.Internal.Elim
- module Agda.Syntax.Abstract.Name
- newtype MetaId = MetaId {}
- newtype ProblemId = ProblemId Nat
Documentation
class TermSize a where Source #
The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).
Not counting towards the term size are:
- sort and color annotations,
- projections.
Minimal complete definition
data Suggestion Source #
Constructors
forall a.Suggest a => Suggestion a |
class Suggest a where Source #
Suggest a name if available (i.e. name is not "_")
Methods
suggestName :: a -> Maybe String Source #
Instances
Suggest Name Source # | |
Defined in Agda.Syntax.Internal Methods suggestName :: Name -> Maybe String Source # | |
Suggest Term Source # | |
Defined in Agda.Syntax.Internal Methods suggestName :: Term -> Maybe String Source # | |
Suggest String Source # | |
Defined in Agda.Syntax.Internal Methods suggestName :: String -> Maybe String Source # | |
Suggest (Abs b) Source # | |
Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source # |
Constructing a singleton telescope.
type DummyTermKind = String Source #
data IntervalView Source #
Constructors
IZero | |
IOne | |
IMin (Arg Term) (Arg Term) | |
IMax (Arg Term) (Arg Term) | |
INeg (Arg Term) | |
OTerm Term |
Instances
Show IntervalView Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> IntervalView -> ShowS show :: IntervalView -> String showList :: [IntervalView] -> ShowS |
View type as path type.
data EqualityView Source #
View type as equality type.
Constructors
EqualityType | |
OtherType Type | reduced |
IdiomType Type | reduced |
Instances
type Substitution = Substitution' Term Source #
data Substitution' a Source #
Substitutions.
Constructors
IdS | Identity substitution.
|
EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is |
a :# (Substitution' a) infixr 4 | Substitution extension, ` |
Strengthen Impossible (Substitution' a) | Strengthening substitution. First argument is |
Wk !Int (Substitution' a) | Weakening substitution, lifts to an extended context.
|
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Instances
KillRange Substitution Source # | |
Defined in Agda.Syntax.Internal Methods | |
InstantiateFull Substitution Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source # | |
Foldable Substitution' Source # | |
Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Substitution' m -> m foldMap :: Monoid m => (a -> m) -> Substitution' a -> m foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m foldr :: (a -> b -> b) -> b -> Substitution' a -> b foldr' :: (a -> b -> b) -> b -> Substitution' a -> b foldl :: (b -> a -> b) -> b -> Substitution' a -> b foldl' :: (b -> a -> b) -> b -> Substitution' a -> b foldr1 :: (a -> a -> a) -> Substitution' a -> a foldl1 :: (a -> a -> a) -> Substitution' a -> a toList :: Substitution' a -> [a] null :: Substitution' a -> Bool length :: Substitution' a -> Int elem :: Eq a => a -> Substitution' a -> Bool maximum :: Ord a => Substitution' a -> a minimum :: Ord a => Substitution' a -> a sum :: Num a => Substitution' a -> a product :: Num a => Substitution' a -> a | |
Traversable Substitution' Source # | |
Defined in Agda.Syntax.Internal Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) | |
Functor Substitution' Source # | |
Defined in Agda.Syntax.Internal Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b (<$) :: a -> Substitution' b -> Substitution' a # | |
Eq Substitution | |
Defined in Agda.TypeChecking.Substitute | |
Ord Substitution | |
Defined in Agda.TypeChecking.Substitute Methods compare :: Substitution -> Substitution -> Ordering (<) :: Substitution -> Substitution -> Bool (<=) :: Substitution -> Substitution -> Bool (>) :: Substitution -> Substitution -> Bool (>=) :: Substitution -> Substitution -> Bool max :: Substitution -> Substitution -> Substitution min :: Substitution -> Substitution -> Substitution | |
TermSize a => TermSize (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal | |
(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source # | |
EmbPrj a => EmbPrj (Substitution' a) Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Substitution' a -> S Int32 Source # icod_ :: Substitution' a -> S Int32 Source # value :: Int32 -> R (Substitution' a) Source # | |
EndoSubst a => Subst (Substitution' a) Source # | |
Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Substitution' a) Source # Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |
Null (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal | |
Pretty a => Pretty (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source # | |
Generic (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal Associated Types type Rep (Substitution' a) :: Type -> Type Methods from :: Substitution' a -> Rep (Substitution' a) x to :: Rep (Substitution' a) x -> Substitution' a | |
Show a => Show (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> Substitution' a -> ShowS show :: Substitution' a -> String showList :: [Substitution' a] -> ShowS | |
NFData a => NFData (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal Methods rnf :: Substitution' a -> () | |
type SubstArg (Substitution' a) Source # | |
Defined in Agda.TypeChecking.Substitute | |
type Rep (Substitution' a) Source # | |
Defined in Agda.Syntax.Internal type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))))) |
class PatternVars a where Source #
Extract pattern variables in left-to-right order.
A DotP
is also treated as variable (see docu for Clause
).
Associated Types
type PatternVarOut a Source #
Methods
patternVars :: a -> [Arg (Either (PatternVarOut a) Term)] Source #
Instances
PatternVars (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (Arg (Pattern' a)) Source # Methods patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source # | |
PatternVars (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |
PatternVars a => PatternVars [a] Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut [a] Source # Methods patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)] Source # |
data ConPatternInfo Source #
The ConPatternInfo
states whether the constructor belongs to
a record type (True
) or data type (False
).
In the former case, the PatOrigin
of the conPInfo
says
whether the record pattern orginates from the expansion of an
implicit pattern.
The Type
is the type of the whole record pattern.
The scope used for the type is given by any outer scope
plus the clause's telescope (clauseTel
).
Constructors
ConPatternInfo | |
Fields
|
Instances
KillRange ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods | |
InstantiateFull ConPatternInfo Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source # | |
Normalise ConPatternInfo Source # | |
Defined in Agda.TypeChecking.Reduce Methods normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source # | |
EmbPrj ConPatternInfo Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: ConPatternInfo -> S Int32 Source # icod_ :: ConPatternInfo -> S Int32 Source # value :: Int32 -> R ConPatternInfo Source # | |
Subst ConPatternInfo Source # | |
Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg ConPatternInfo Source # Methods applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source # | |
Data ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatternInfo -> c ConPatternInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatternInfo toConstr :: ConPatternInfo -> Constr dataTypeOf :: ConPatternInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatternInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatternInfo) gmapT :: (forall b. Data b => b -> b) -> ConPatternInfo -> ConPatternInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatternInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ConPatternInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatternInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatternInfo -> m ConPatternInfo | |
Generic ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Associated Types type Rep ConPatternInfo :: Type -> Type | |
Show ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> ConPatternInfo -> ShowS show :: ConPatternInfo -> String showList :: [ConPatternInfo] -> ShowS | |
NFData ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods rnf :: ConPatternInfo -> () | |
type SubstArg ConPatternInfo Source # | |
Defined in Agda.TypeChecking.Substitute | |
type Rep ConPatternInfo Source # | |
Defined in Agda.Syntax.Internal type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) |
type DeBruijnPattern = Pattern' DBPatVar Source #
Type used when numbering pattern variables.
Constructors
DBPatVar | |
Fields
|
Instances
Arguments
= Pattern' PatVarName | The |
Patterns are variables, constructors, or wildcards.
QName
is used in ConP
rather than Name
since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName
.
Constructors
VarP PatternInfo x | x |
DotP PatternInfo Term | .t |
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)] |
|
LitP PatternInfo Literal | E.g. |
ProjP ProjOrigin QName | Projection copattern. Can only appear by itself. |
IApplyP PatternInfo Term Term x | Path elimination pattern, like |
DefP PatternInfo QName [NamedArg (Pattern' x)] | Used for HITs, the QName should be the one from primHComp. |
Instances
UsableSizeVars DeBruijnPattern Source # | |
Defined in Agda.Termination.Monad Methods | |
UsableSizeVars MaskedDeBruijnPatterns Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: MaskedDeBruijnPatterns -> TerM VarSet Source # | |
Reduce DeBruijnPattern Source # | |
Defined in Agda.TypeChecking.Reduce Methods reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source # reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source # | |
Subst DeBruijnPattern Source # | |
Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg DeBruijnPattern Source # Methods applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source # | |
Subst Pattern Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source # | |
Subst SplitPattern Source # | |
Defined in Agda.TypeChecking.Coverage.Match Associated Types type SubstArg SplitPattern Source # Methods applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source # | |
Foldable Pattern' Source # | |
Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Pattern' m -> m foldMap :: Monoid m => (a -> m) -> Pattern' a -> m foldMap' :: Monoid m => (a -> m) -> Pattern' a -> m foldr :: (a -> b -> b) -> b -> Pattern' a -> b foldr' :: (a -> b -> b) -> b -> Pattern' a -> b foldl :: (b -> a -> b) -> b -> Pattern' a -> b foldl' :: (b -> a -> b) -> b -> Pattern' a -> b foldr1 :: (a -> a -> a) -> Pattern' a -> a foldl1 :: (a -> a -> a) -> Pattern' a -> a elem :: Eq a => a -> Pattern' a -> Bool maximum :: Ord a => Pattern' a -> a minimum :: Ord a => Pattern' a -> a | |
Traversable Pattern' Source # | |
Functor Pattern' Source # | |
LabelPatVars Pattern DeBruijnPattern Source # | |
Defined in Agda.Syntax.Internal.Pattern Associated Types Methods labelPatVars :: Pattern -> State [PatVarLabel DeBruijnPattern] DeBruijnPattern Source # | |
MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the |
PatternLike a (Pattern' a) Source # | |
Defined in Agda.Syntax.Internal.Pattern | |
DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Patterns.Internal | |
Conversion TOM (Arg Pattern) (Pat O) Source # | |
IsProjP (Pattern' a) Source # | |
Defined in Agda.Syntax.Internal Methods isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |
PatternVars (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (Arg (Pattern' a)) Source # Methods patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source # | |
PatternVars (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # Methods patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source # | |
NamesIn (Pattern' a) Source # | |
CountPatternVars (Pattern' x) Source # | |
Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source # | |
PatternVarModalities (Pattern' x) Source # | |
KillRange a => KillRange (Pattern' a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Pattern' a) Source # | |
UsableSizeVars (Masked DeBruijnPattern) Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: Masked DeBruijnPattern -> TerM VarSet Source # | |
UsableSizeVars [DeBruijnPattern] Source # | |
Defined in Agda.Termination.Monad Methods usableSizeVars :: [DeBruijnPattern] -> TerM VarSet Source # | |
PrettyTCM a => PrettyTCM (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Pretty | |
NormaliseProjP (Pattern' x) Source # | |
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source # | |
InstantiateFull a => InstantiateFull (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
Normalise a => Normalise (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
IsFlexiblePattern (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern' a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern' a -> m Bool Source # | |
EmbPrj a => EmbPrj (Pattern' a) Source # | |
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. |
DeBruijn a => DeBruijn (Pattern' a) Source # | |
Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> Pattern' a Source # debruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source # | |
Pretty a => Pretty (Pattern' a) Source # | |
Data x => Data (Pattern' x) Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' x -> c (Pattern' x) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' x) toConstr :: Pattern' x -> Constr dataTypeOf :: Pattern' x -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' x)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pattern' x)) gmapT :: (forall b. Data b => b -> b) -> Pattern' x -> Pattern' x gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' x -> r gmapQ :: (forall d. Data d => d -> u) -> Pattern' x -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' x -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' x -> m (Pattern' x) | |
Generic (Pattern' x) Source # | |
Show x => Show (Pattern' x) Source # | |
NFData x => NFData (Pattern' x) Source # | |
Defined in Agda.Syntax.Internal | |
Eq a => Eq (Pattern' a) | |
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |
Defined in Agda.TypeChecking.Rewriting.Clause | |
type PatVarLabel DeBruijnPattern Source # | |
Defined in Agda.Syntax.Internal.Pattern | |
type SubstArg DeBruijnPattern Source # | |
Defined in Agda.TypeChecking.Substitute | |
type SubstArg Pattern Source # | |
Defined in Agda.TypeChecking.Substitute | |
type SubstArg SplitPattern Source # | |
Defined in Agda.TypeChecking.Coverage.Match | |
type PatternVarOut (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
type PatternVarOut (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal | |
type PatVar (Pattern' x) Source # | |
Defined in Agda.Syntax.Internal.Pattern | |
type Rep (Pattern' x) Source # | |
Defined in Agda.Syntax.Internal type Rep (Pattern' x) = D1 ('MetaData "Pattern'" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) ((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x)) :+: (C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConHead) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)]))))) :+: ((C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "IApplyP" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 x))) :+: C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' x)])))))) |
Origin of the pattern: what did the user write in this position?
Constructors
PatOSystem | Pattern inserted by the system |
PatOSplit | Pattern generated by case split |
PatOVar Name | User wrote a variable pattern |
PatODot | User wrote a dot pattern |
PatOWild | User wrote a wildcard pattern |
PatOCon | User wrote a constructor pattern |
PatORec | User wrote a record pattern |
PatOLit | User wrote a literal pattern |
PatOAbsurd | User wrote an absurd pattern |
Instances
KillRange PatOrigin Source # | |
Defined in Agda.Syntax.Internal Methods | |
EmbPrj PatOrigin Source # | |
Data PatOrigin Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatOrigin -> c PatOrigin gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatOrigin toConstr :: PatOrigin -> Constr dataTypeOf :: PatOrigin -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatOrigin) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatOrigin) gmapT :: (forall b. Data b => b -> b) -> PatOrigin -> PatOrigin gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatOrigin -> r gmapQ :: (forall d. Data d => d -> u) -> PatOrigin -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PatOrigin -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatOrigin -> m PatOrigin | |
Generic PatOrigin Source # | |
Show PatOrigin Source # | |
NFData PatOrigin Source # | |
Defined in Agda.Syntax.Internal | |
Eq PatOrigin Source # | |
type Rep PatOrigin Source # | |
Defined in Agda.Syntax.Internal type Rep PatOrigin = D1 ('MetaData "PatOrigin" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (((C1 ('MetaCons "PatOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOSplit" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatOVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "PatODot" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PatOWild" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PatORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PatOLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PatOAbsurd" 'PrefixI 'False) (U1 :: Type -> Type))))) |
data PatternInfo Source #
Constructors
PatternInfo | |
Fields
|
Instances
KillRange PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods | |
EmbPrj PatternInfo Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: PatternInfo -> S Int32 Source # icod_ :: PatternInfo -> S Int32 Source # value :: Int32 -> R PatternInfo Source # | |
Data PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatternInfo -> c PatternInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatternInfo toConstr :: PatternInfo -> Constr dataTypeOf :: PatternInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatternInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatternInfo) gmapT :: (forall b. Data b => b -> b) -> PatternInfo -> PatternInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatternInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatternInfo -> r gmapQ :: (forall d. Data d => d -> u) -> PatternInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PatternInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatternInfo -> m PatternInfo | |
Generic PatternInfo Source # | |
Defined in Agda.Syntax.Internal Associated Types type Rep PatternInfo :: Type -> Type | |
Show PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatternInfo -> ShowS show :: PatternInfo -> String showList :: [PatternInfo] -> ShowS | |
NFData PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods rnf :: PatternInfo -> () | |
Eq PatternInfo Source # | |
Defined in Agda.Syntax.Internal | |
type Rep PatternInfo Source # | |
Defined in Agda.Syntax.Internal type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) |
type PatVarName = ArgName Source #
Pattern variables.
A clause is a list of patterns and the clause body.
The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.
clauseTel ~ permute clausePerm (patternVars namedClausePats)
Terms in dot patterns are valid in the clause telescope.
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Constructors
Clause | |
Fields
|
Instances
GetDefs Clause Source # | |
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Clause -> m () Source # | |
NamesIn Clause Source # | |
FunArity Clause Source # | Get the number of initial |
Defined in Agda.Syntax.Internal.Pattern | |
HasRange Clause Source # | |
KillRange Clause Source # | |
Defined in Agda.Syntax.Internal Methods | |
DropArgs Clause Source # | NOTE: does not work for recursive functions. |
DropArgs FunctionInverse Source # | |
Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> FunctionInverse -> FunctionInverse Source # | |
Free Clause Source # | |
Occurs Clause Source # | |
ComputeOccurrences Clause Source # | |
Defined in Agda.TypeChecking.Positivity Methods | |
PrettyTCM Clause Source # | |
Defined in Agda.TypeChecking.Pretty | |
NormaliseProjP Clause Source # | |
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Clause -> m Clause Source # | |
InstantiateFull Clause Source # | |
Defined in Agda.TypeChecking.Reduce | |
InstantiateFull FunctionInverse Source # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source # | |
EmbPrj Clause Source # | |
Abstract Clause Source # | |
Abstract FunctionInverse Source # | |
Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source # | |
Apply Clause Source # | |
Apply FunctionInverse Source # | |
Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source # | |
Null Clause Source # | A |
Pretty Clause Source # | |
Data Clause Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause -> c Clause gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Clause dataTypeOf :: Clause -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Clause) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Clause) gmapT :: (forall b. Data b => b -> b) -> Clause -> Clause gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause -> r gmapQ :: (forall d. Data d => d -> u) -> Clause -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause -> m Clause gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause -> m Clause | |
Generic Clause Source # | |
Show Clause Source # | |
NFData Clause Source # | |
Defined in Agda.Syntax.Internal | |
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |
Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |
FunArity [Clause] Source # | Get the number of common initial |
Defined in Agda.Syntax.Internal.Pattern | |
Reify (QNamed Clause) Source # | |
PrettyTCM (QNamed Clause) Source # | |
Defined in Agda.TypeChecking.Pretty | |
type Rep Clause Source # | |
Defined in Agda.Syntax.Internal type Rep Clause = D1 ('MetaData "Clause" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term))))) :*: ((S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: (S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "clauseExact") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))) :*: (S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))))) | |
type ReifiesTo (QNamed Clause) Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract |
type NAPs = [NamedArg DeBruijnPattern] Source #
Named pattern arguments.
type NotBlocked = NotBlocked' Term Source #
Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.
Instances
Apply BraveTerm Source # | |
Subst BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |
DeBruijn BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> BraveTerm Source # debruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source # | |
Data BraveTerm Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BraveTerm -> c BraveTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BraveTerm toConstr :: BraveTerm -> Constr dataTypeOf :: BraveTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BraveTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BraveTerm) gmapT :: (forall b. Data b => b -> b) -> BraveTerm -> BraveTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BraveTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BraveTerm -> r gmapQ :: (forall d. Data d => d -> u) -> BraveTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BraveTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BraveTerm -> m BraveTerm | |
Show BraveTerm Source # | |
type SubstArg BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute |
type PlusLevel = PlusLevel' Term Source #
data PlusLevel' t Source #
Constructors
Plus Integer t |
Instances
A level is a maximum expression of a closed level and 0..n
PlusLevel
expressions each of which is an atom plus a number.
Constructors
Max Integer [PlusLevel' t] |
Instances
Sorts.
Constructors
Type (Level' t) |
|
Prop (Level' t) |
|
Inf IsFibrant Integer |
|
SSet (Level' t) |
|
SizeUniv |
|
LockUniv |
|
PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) | Sort of the pi type. |
FunSort (Sort' t) (Sort' t) | Sort of a (non-dependent) function type. |
UnivSort (Sort' t) | Sort of another sort. |
MetaS !MetaId [Elim' t] | |
DefS QName [Elim' t] | A postulated sort. |
DummyS String | A (part of a) term or type which is only used for internal purposes.
Replaces the abuse of |
Instances
Instances
EmbPrj IsFibrant Source # | |
Data IsFibrant Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsFibrant -> c IsFibrant gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsFibrant toConstr :: IsFibrant -> Constr dataTypeOf :: IsFibrant -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsFibrant) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsFibrant) gmapT :: (forall b. Data b => b -> b) -> IsFibrant -> IsFibrant gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsFibrant -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsFibrant -> r gmapQ :: (forall d. Data d => d -> u) -> IsFibrant -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IsFibrant -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsFibrant -> m IsFibrant | |
Generic IsFibrant Source # | |
Show IsFibrant Source # | |
NFData IsFibrant Source # | |
Defined in Agda.Syntax.Internal | |
Eq IsFibrant Source # | |
Ord IsFibrant Source # | |
Defined in Agda.Syntax.Internal | |
type Rep IsFibrant Source # | |
Defined in Agda.Syntax.Internal type Rep IsFibrant = D1 ('MetaData "IsFibrant" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "IsFibrant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsStrict" 'PrefixI 'False) (U1 :: Type -> Type)) |
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
TelToArgs Telescope Source # | |
Reify Telescope Source # | |
DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices. |
AddContext Telescope Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # contextSize :: Telescope -> Nat Source # | |
PrettyTCM Telescope Source # | |
Defined in Agda.TypeChecking.Pretty | |
Reduce Telescope Source # | |
TeleNoAbs Telescope Source # | |
Abstract Telescope Source # | |
Foldable Tele Source # | |
Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Tele m -> m foldMap :: Monoid m => (a -> m) -> Tele a -> m foldMap' :: Monoid m => (a -> m) -> Tele a -> m foldr :: (a -> b -> b) -> b -> Tele a -> b foldr' :: (a -> b -> b) -> b -> Tele a -> b foldl :: (b -> a -> b) -> b -> Tele a -> b foldl' :: (b -> a -> b) -> b -> Tele a -> b foldr1 :: (a -> a -> a) -> Tele a -> a foldl1 :: (a -> a -> a) -> Tele a -> a elem :: Eq a => a -> Tele a -> Bool maximum :: Ord a => Tele a -> a | |
Traversable Tele Source # | |
Functor Tele Source # | |
TermLike a => TermLike (Tele a) Source # | |
TermLike a => AllMetas (Tele a) Source # | |
NamesIn a => NamesIn (Tele a) Source # | |
KillRange a => KillRange (Tele a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Tele a) Source # | |
Free t => Free (Tele t) Source # | |
MentionsMeta a => MentionsMeta (Tele a) Source # | |
Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source # | |
AddContext (KeepNames Telescope) Source # | |
Defined in Agda.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |
ComputeOccurrences a => ComputeOccurrences (Tele a) Source # | |
Defined in Agda.TypeChecking.Positivity Methods occurrences :: Tele a -> OccM OccurrencesBuilder Source # | |
Instantiate t => Instantiate (Tele t) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, Normalise a) => Normalise (Tele a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, Simplify a) => Simplify (Tele a) Source # | |
EmbPrj a => EmbPrj (Tele a) Source # | |
TermSubst a => Apply (Tele a) Source # | |
Subst a => Subst (Tele a) Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source # | |
Null (Tele a) Source # | |
Pretty a => Pretty (Tele (Dom a)) Source # | |
Sized (Tele a) Source # | The size of a telescope is its length (as a list). |
Defined in Agda.Syntax.Internal | |
Data a => Data (Tele a) Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Tele a -> c (Tele a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Tele a) dataTypeOf :: Tele a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Tele a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tele a)) gmapT :: (forall b. Data b => b -> b) -> Tele a -> Tele a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tele a -> r gmapQ :: (forall d. Data d => d -> u) -> Tele a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Tele a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tele a -> m (Tele a) | |
Generic (Tele a) Source # | |
Show a => Show (Tele a) Source # | |
NFData a => NFData (Tele a) Source # | |
Defined in Agda.Syntax.Internal | |
(Subst a, Eq a) => Eq (Tele a) | |
(Subst a, Ord a) => Ord (Tele a) | |
type ReifiesTo Telescope Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
type SubstArg (Tele a) Source # | |
Defined in Agda.TypeChecking.Substitute | |
type Rep (Tele a) Source # | |
Defined in Agda.Syntax.Internal type Rep (Tele a) = D1 ('MetaData "Tele" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "EmptyTel" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ExtendTel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Abs (Tele a))))) |
class LensSort a where Source #
Minimal complete definition
Types are terms with a sort annotation.
Instances
Binder.
Abs
: The bound variable might appear in the body.
NoAbs
is pseudo-binder, it does not introduce a fresh variable,
similar to the const
of Haskell.
Constructors
Abs | The body has (at least) one free variable.
Danger: |
NoAbs | |
Instances
Decoration Abs Source # | |
Foldable Abs Source # | |
Defined in Agda.Syntax.Internal Methods fold :: Monoid m => Abs m -> m foldMap :: Monoid m => (a -> m) -> Abs a -> m foldMap' :: Monoid m => (a -> m) -> Abs a -> m foldr :: (a -> b -> b) -> b -> Abs a -> b foldr' :: (a -> b -> b) -> b -> Abs a -> b foldl :: (b -> a -> b) -> b -> Abs a -> b foldl' :: (b -> a -> b) -> b -> Abs a -> b foldr1 :: (a -> a -> a) -> Abs a -> a foldl1 :: (a -> a -> a) -> Abs a -> a elem :: Eq a => a -> Abs a -> Bool maximum :: Ord a => Abs a -> a | |
Traversable Abs Source # | |
Functor Abs Source # | |
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # | |
Suggest (Abs b) Source # | |
Defined in Agda.Syntax.Internal Methods suggestName :: Abs b -> Maybe String Source # | |
GetDefs a => GetDefs (Abs a) Source # | |
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => Abs a -> m () Source # | |
TermLike a => TermLike (Abs a) Source # | |
NamesIn a => NamesIn (Abs a) Source # | |
KillRange a => KillRange (Abs a) Source # | |
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Abs a) Source # | |
(Free i, Reify i) => Reify (Abs i) Source # | |
(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source # | |
(Subst a, EqualSy a) => EqualSy (Abs a) Source # | Ignores |
Free t => Free (Abs t) Source # | |
PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source # | |
Defined in Agda.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Abs a -> FV (Abs a) Source # | |
(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source # | |
Defined in Agda.TypeChecking.Free.Reduce Methods forceNotFree' :: MonadFreeRed m => Abs a -> m (Abs a) | |
(Subst a, UsableRelevance a) => UsableRelevance (Abs a) Source # | |
Defined in Agda.TypeChecking.Irrelevance Methods usableRel :: (ReadTCState m, HasConstInfo m, MonadTCEnv m, MonadAddContext m, MonadDebug m) => Relevance -> Abs a -> m Bool Source # | |
MentionsMeta t => MentionsMeta (Abs t) Source # | |
Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source # | |
(Subst a, AnyRigid a) => AnyRigid (Abs a) Source # | |
(Occurs a, Subst a) => Occurs (Abs a) Source # | |
IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source # | Does not worry about raising. |
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source # | |
UnFreezeMeta a => UnFreezeMeta (Abs a) Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source # | |
ComputeOccurrences a => ComputeOccurrences (Abs a) Source # | |
Defined in Agda.TypeChecking.Positivity Methods occurrences :: Abs a -> OccM OccurrencesBuilder Source # | |
Instantiate t => Instantiate (Abs t) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, Normalise a) => Normalise (Abs a) Source # | |
Defined in Agda.TypeChecking.Reduce | |
(Subst a, Reduce a) => Reduce (Abs a) Source # | |
(Subst a, Simplify a) => Simplify (Abs a) Source # | |
GetMatchables a => GetMatchables (Abs a) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods getMatchables :: Abs a -> [QName] Source # | |
NLPatVars a => NLPatVars (Abs a) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |
EmbPrj a => EmbPrj (Abs a) Source # | |
Subst a => Subst (Abs a) Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source # | |
(Subst a, SynEq a) => SynEq (Abs a) Source # | |
Pretty t => Pretty (Abs t) Source # | |
Sized a => Sized (Abs a) Source # | |
Defined in Agda.Syntax.Internal | |
Data a => Data (Abs a) Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Abs a -> c (Abs a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Abs a) dataTypeOf :: Abs a -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Abs a)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Abs a)) gmapT :: (forall b. Data b => b -> b) -> Abs a -> Abs a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Abs a -> r gmapQ :: (forall d. Data d => d -> u) -> Abs a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Abs a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Abs a -> m (Abs a) | |
Generic (Abs a) Source # | |
Show a => Show (Abs a) Source # | |
NFData a => NFData (Abs a) Source # | |
Defined in Agda.Syntax.Internal | |
(Subst a, Eq a) => Eq (Abs a) | Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution. |
(Subst a, Ord a) => Ord (Abs a) | |
ToNLPat a b => ToNLPat (Abs a) (Abs b) Source # | |
NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinPattern | |
type ReifiesTo (Abs i) Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
type SubstArg (Abs a) Source # | |
Defined in Agda.TypeChecking.Substitute | |
type Rep (Abs a) Source # | |
Defined in Agda.Syntax.Internal type Rep (Abs a) = D1 ('MetaData "Abs" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) |
Raw values.
Def
is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
Constructors
Var !Int Elims |
|
Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
Lit Literal | |
Def QName Elims |
|
Con ConHead ConInfo Elims |
|
Pi (Dom Type) (Abs Type) | dependent or non-dependent function space |
Sort Sort | |
Level Level | |
MetaV !MetaId Elims | |
DontCare Term | Irrelevant stuff in relevant position, but created
in an irrelevant context. Basically, an internal
version of the irrelevance axiom |
Dummy String Elims | A (part of a) term or type which is only used for internal purposes.
Replaces the |
Instances
class LensConName a where Source #
Minimal complete definition
Methods
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
Instances
LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal |
Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.
Constructors
ConHead | |
Fields
|
Instances
LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal | |
NamesIn ConHead Source # | |
HasRange ConHead Source # | |
KillRange ConHead Source # | |
Defined in Agda.Syntax.Internal Methods | |
SetRange ConHead Source # | |
PrettyTCM ConHead Source # | |
Defined in Agda.TypeChecking.Pretty | |
InstantiateFull ConHead Source # | |
Defined in Agda.TypeChecking.Reduce | |
EmbPrj ConHead Source # | |
Pretty ConHead Source # | |
Data ConHead Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConHead -> c ConHead gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConHead dataTypeOf :: ConHead -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConHead) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConHead) gmapT :: (forall b. Data b => b -> b) -> ConHead -> ConHead gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConHead -> r gmapQ :: (forall d. Data d => d -> u) -> ConHead -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConHead -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConHead -> m ConHead | |
Generic ConHead Source # | |
Show ConHead Source # | |
NFData ConHead Source # | |
Defined in Agda.Syntax.Internal | |
Eq ConHead Source # | |
Ord ConHead Source # | |
type Rep ConHead Source # | |
Defined in Agda.Syntax.Internal type Rep ConHead = D1 ('MetaData "ConHead" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg QName])))) |
data DataOrRecord Source #
Constructors
IsData | |
IsRecord PatternOrCopattern |
Instances
KillRange DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods | |
EmbPrj DataOrRecord Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: DataOrRecord -> S Int32 Source # icod_ :: DataOrRecord -> S Int32 Source # value :: Int32 -> R DataOrRecord Source # | |
Data DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataOrRecord -> c DataOrRecord gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataOrRecord toConstr :: DataOrRecord -> Constr dataTypeOf :: DataOrRecord -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataOrRecord) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataOrRecord) gmapT :: (forall b. Data b => b -> b) -> DataOrRecord -> DataOrRecord gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataOrRecord -> r gmapQ :: (forall d. Data d => d -> u) -> DataOrRecord -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DataOrRecord -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataOrRecord -> m DataOrRecord | |
Generic DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Associated Types type Rep DataOrRecord :: Type -> Type | |
Show DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> DataOrRecord -> ShowS show :: DataOrRecord -> String showList :: [DataOrRecord] -> ShowS | |
NFData DataOrRecord Source # | |
Defined in Agda.Syntax.Internal Methods rnf :: DataOrRecord -> () | |
Eq DataOrRecord Source # | |
Defined in Agda.Syntax.Internal | |
type Rep DataOrRecord Source # | |
Defined in Agda.Syntax.Internal type Rep DataOrRecord = D1 ('MetaData "DataOrRecord" "Agda.Syntax.Internal" "Agda-2.6.2.2-5UP7zU8ZQ991hlQcMxoIJm" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternOrCopattern))) |
Similar to Arg
, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
Dom
is used in Pi
of internal syntax, in Context
and Telescope
.
Arg
is used for actual arguments (Var
, Con
, Def
etc.)
and in Abstract
syntax and other situations.
- cubical
- When
domFinite = True
for the domain of aPi
type, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.
Constructors
Dom | |
Instances
pattern ClosedLevel :: Integer -> Level Source #
Constant level n
argFromDom :: Dom' t a -> Arg a Source #
namedArgFromDom :: Dom' t a -> NamedArg a Source #
domFromArg :: Arg a -> Dom a Source #
domFromNamedArg :: NamedArg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
defaultArgDom :: ArgInfo -> a -> Dom a Source #
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a Source #
clausePats :: Clause -> [Arg DeBruijnPattern] Source #
patVarNameToString :: PatVarName -> String Source #
nameToPatVarName :: Name -> PatVarName Source #
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #
absurdP :: Int -> DeBruijnPattern Source #
Make an absurd pattern with the given de Bruijn index.
toConPatternInfo :: ConInfo -> ConPatternInfo Source #
Build partial ConPatternInfo
from ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo Source #
Build ConInfo
from ConPatternInfo
.
patternInfo :: Pattern' x -> Maybe PatternInfo Source #
Retrieve the PatternInfo from a pattern
patternOrigin :: Pattern' x -> Maybe PatOrigin Source #
Retrieve the origin of a pattern
properlyMatching :: Pattern' a -> Bool Source #
Does the pattern perform a match that could fail?
Arguments
:: Bool | Should absurd patterns count as proper match? |
-> Bool | Should projection patterns count as proper match? |
-> Pattern' a | The pattern. |
-> Bool |
isEqualityType :: EqualityView -> Bool Source #
isPathType :: PathView -> Bool Source #
isIOne :: IntervalView -> Bool Source #
absurdBody :: Abs Term Source #
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdBody :: Abs Term -> Bool Source #
isAbsurdPatternName :: PatVarName -> Bool Source #
dummyLocName :: CallStack -> String Source #
Construct a string representing the call-site that created the dummy thing.
dummyTermWith :: DummyTermKind -> CallStack -> Term Source #
Aux: A dummy term to constitute a dummy termlevelsort/type.
dummyLevel :: CallStack -> Level Source #
A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !
dummyTerm :: CallStack -> Term Source #
A dummy term created at location. Note: use macro DUMMY_TERM !
__DUMMY_TERM__ :: HasCallStack => Term Source #
__DUMMY_LEVEL__ :: HasCallStack => Level Source #
dummySort :: CallStack -> Sort Source #
A dummy sort created at location. Note: use macro DUMMY_SORT !
__DUMMY_SORT__ :: HasCallStack => Sort Source #
dummyType :: CallStack -> Type Source #
A dummy type created at location. Note: use macro DUMMY_TYPE !
__DUMMY_TYPE__ :: HasCallStack => Type Source #
dummyDom :: CallStack -> Dom Type Source #
Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !
__DUMMY_DOM__ :: HasCallStack => Dom Type Source #
atomicLevel :: t -> Level' t Source #
impossibleTerm :: CallStack -> Term Source #
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #
A traversal for the names in a telescope.
telFromList :: ListTel -> Telescope Source #
Convert a list telescope to a telescope.
suggests :: [Suggestion] -> String Source #
unSpine' :: (ProjOrigin -> Bool) -> Term -> Term Source #
Convert Proj
projection eliminations
according to their ProjOrigin
into
Def
projection applications.
hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #
A view distinguishing the neutrals Var
, Def
, and MetaV
which
can be projected.
prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc Source #
module Agda.Syntax.Internal.Elim
module Agda.Syntax.Abstract.Name
A meta variable identifier is just a natural number.
Instances
EncodeTCM MetaId Source # | |
GetDefs MetaId Source # | |
Defined in Agda.Syntax.Internal.Defs Methods getDefs :: MonadGetDefs m => MetaId -> m () Source # | |
Reify MetaId Source # | |
HasFresh MetaId Source # | |
IsInstantiatedMeta MetaId Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars Methods isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source # | |
UnFreezeMeta MetaId Source # | |
Defined in Agda.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |
PrettyTCM MetaId Source # | |
Defined in Agda.TypeChecking.Pretty | |
FromTerm MetaId Source # | |
Defined in Agda.TypeChecking.Primitive | |
PrimTerm MetaId Source # | |
PrimType MetaId Source # | |
ToTerm MetaId Source # | |
EmbPrj MetaId Source # | |
Unquote MetaId Source # | |
Pretty MetaId Source # | |
ToJSON MetaId Source # | |
Defined in Agda.Interaction.JSONTop | |
Data MetaId Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaId -> c MetaId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaId dataTypeOf :: MetaId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaId) gmapT :: (forall b. Data b => b -> b) -> MetaId -> MetaId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaId -> r gmapQ :: (forall d. Data d => d -> u) -> MetaId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaId -> m MetaId | |
Enum MetaId Source # | |
Defined in Agda.Syntax.Common | |
Generic MetaId Source # | |
Num MetaId Source # | |
Integral MetaId Source # | |
Real MetaId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: MetaId -> Rational | |
Show MetaId Source # | Show non-record version of this newtype. |
NFData MetaId Source # | |
Defined in Agda.Syntax.Common | |
Eq MetaId Source # | |
Ord MetaId Source # | |
Hashable MetaId Source # | |
Defined in Agda.Syntax.Common | |
Singleton MetaId MetaSet Source # | |
Singleton MetaId () Source # | |
Defined in Agda.TypeChecking.Free.Lazy | |
type ReifiesTo MetaId Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract | |
type Rep MetaId Source # | |
Defined in Agda.Syntax.Common |
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
EncodeTCM ProblemId Source # | |
HasFresh ProblemId Source # | |
PrettyTCM ProblemId Source # | |
Defined in Agda.TypeChecking.Pretty | |
Pretty ProblemId Source # | |
ToJSON ProblemId Source # | |
Defined in Agda.Interaction.JSONTop | |
Data ProblemId Source # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId toConstr :: ProblemId -> Constr dataTypeOf :: ProblemId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId | |
Enum ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Num ProblemId Source # | |
Integral ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Real ProblemId Source # | |
Defined in Agda.Syntax.Common Methods toRational :: ProblemId -> Rational | |
Show ProblemId Source # | |
NFData ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Eq ProblemId Source # | |
Ord ProblemId Source # | |
Defined in Agda.Syntax.Common | |
Monad m => MonadFresh ProblemId (PureConversionT m) Source # | |
Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source # |