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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Info

Description

An info object contains additional information about a piece of abstract syntax that isn't part of the actual syntax. For instance, it might contain the source code position of an expression or the concrete syntax that an internal expression originates from.

Synopsis

- data MetaInfo = MetaInfo {
  - metaRange :: Range
  - metaScope :: ScopeInfo
  - metaNumber :: Maybe MetaId
  - metaNameSuggestion :: String
  }
- emptyMetaInfo :: MetaInfo
- newtype ExprInfo = ExprRange Range
- exprNoRange :: ExprInfo
- data AppInfo = AppInfo {
  - appRange :: Range
  - appOrigin :: Origin
  - appParens :: ParenPreference
  }
- defaultAppInfo :: Range -> AppInfo
- defaultAppInfo_ :: AppInfo
- data ModuleInfo = ModuleInfo {
  - minfoRange :: Range
  - minfoAsTo :: Range
  - minfoAsName :: Maybe Name
  - minfoOpenShort :: Maybe OpenShortHand
  - minfoDirective :: Maybe ImportDirective
  }
- newtype LetInfo = LetRange Range
- data DefInfo = DefInfo {
  - defFixity :: Fixity'
  - defAccess :: Access
  - defAbstract :: IsAbstract
  - defInstance :: IsInstance
  - defMacro :: IsMacro
  - defInfo :: DeclInfo
  }
- mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
- mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo
- data DeclInfo = DeclInfo {
  - declName :: Name
  - declRange :: Range
  }
- data MutualInfo = MutualInfo {
  - mutualTermCheck :: TerminationCheck Name
  - mutualPositivityCheck :: PositivityCheck
  - mutualRange :: Range
  }
- newtype LHSInfo = LHSRange Range
- newtype PatInfo = PatRange Range
- patNoRange :: PatInfo
- data ConPatInfo = ConPatInfo {
  - patOrigin :: ConOrigin
  - patInfo :: PatInfo
  - patLazy :: ConPatLazy
  }
- data ConPatLazy
  - = ConPatLazy
  - | ConPatEager

# Documentation

data MetaInfo Source #

Constructors

MetaInfo |

Fields

- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: String

Instances

Eq MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaInfo -> MetaInfo -> Bool Source # (/=) :: MetaInfo -> MetaInfo -> Bool Source #
Data MetaInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MetaInfo -> c MetaInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MetaInfo Source #

toConstr :: MetaInfo -> Constr Source #

dataTypeOf :: MetaInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MetaInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MetaInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> MetaInfo -> MetaInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MetaInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MetaInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MetaInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MetaInfo -> m MetaInfo Source #

Show MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaInfo -> ShowS Source # show :: MetaInfo -> String Source # showList :: [MetaInfo] -> ShowS Source #
KillRange MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo Source #
HasRange MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range Source #

emptyMetaInfo :: MetaInfo Source #

newtype ExprInfo Source #

Constructors

ExprRange Range |

Instances

Eq ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ExprInfo -> ExprInfo -> Bool Source # (/=) :: ExprInfo -> ExprInfo -> Bool Source #
Data ExprInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExprInfo -> c ExprInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExprInfo Source #

toConstr :: ExprInfo -> Constr Source #

dataTypeOf :: ExprInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExprInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExprInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ExprInfo -> ExprInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExprInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ExprInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExprInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExprInfo -> m ExprInfo Source #

Show ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ExprInfo -> ShowS Source # show :: ExprInfo -> String Source # showList :: [ExprInfo] -> ShowS Source #
Null ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo Source # null :: ExprInfo -> Bool Source #
KillRange ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo Source #
HasRange ExprInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range Source #

exprNoRange :: ExprInfo Source #

data AppInfo Source #

Information about application

Constructors

AppInfo |

Fields

- appRange :: Range
- appOrigin :: Origin
- appParens :: ParenPreference

  Do we prefer a appbda argument with or without parens?

Instances

Eq AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: AppInfo -> AppInfo -> Bool Source # (/=) :: AppInfo -> AppInfo -> Bool Source #
Data AppInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AppInfo -> c AppInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AppInfo Source #

toConstr :: AppInfo -> Constr Source #

dataTypeOf :: AppInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AppInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AppInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> AppInfo -> AppInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AppInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> AppInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> AppInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AppInfo -> m AppInfo Source #

Ord AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods compare :: AppInfo -> AppInfo -> Ordering Source # (<) :: AppInfo -> AppInfo -> Bool Source # (<=) :: AppInfo -> AppInfo -> Bool Source # (>) :: AppInfo -> AppInfo -> Bool Source # (>=) :: AppInfo -> AppInfo -> Bool Source # max :: AppInfo -> AppInfo -> AppInfo Source # min :: AppInfo -> AppInfo -> AppInfo Source #
Show AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> AppInfo -> ShowS Source # show :: AppInfo -> String Source # showList :: [AppInfo] -> ShowS Source #
KillRange AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo Source #
HasRange AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range Source #
LensOrigin AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getOrigin :: AppInfo -> Origin Source # setOrigin :: Origin -> AppInfo -> AppInfo Source # mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo Source #

defaultAppInfo :: Range -> AppInfo Source #

Default is system inserted and prefer parens.

defaultAppInfo_ :: AppInfo Source #

`AppInfo` with no range information.

data ModuleInfo Source #

Constructors

ModuleInfo |

Fields

- minfoRange :: Range
- minfoAsTo :: Range

  The range of the "as" and "to" keywords, if any. Retained for highlighting purposes.

- minfoAsName :: Maybe Name

  The "as" module name, if any. Retained for highlighting purposes.

- minfoOpenShort :: Maybe OpenShortHand
- minfoDirective :: Maybe ImportDirective

  Retained for `abstractToConcrete` of `ModuleMacro`.

Instances

Eq ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ModuleInfo -> ModuleInfo -> Bool Source # (/=) :: ModuleInfo -> ModuleInfo -> Bool Source #
Data ModuleInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleInfo -> c ModuleInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleInfo Source #

toConstr :: ModuleInfo -> Constr Source #

dataTypeOf :: ModuleInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ModuleInfo -> ModuleInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ModuleInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleInfo -> m ModuleInfo Source #

Show ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS Source # show :: ModuleInfo -> String Source # showList :: [ModuleInfo] -> ShowS Source #
KillRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ModuleInfo Source #
SetRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ModuleInfo -> ModuleInfo Source #
HasRange ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range Source #
UniverseBi Declaration ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [ModuleInfo] Source #

newtype LetInfo Source #

Constructors

LetRange Range |

Instances

Eq LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool Source # (/=) :: LetInfo -> LetInfo -> Bool Source #
Data LetInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetInfo -> c LetInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetInfo Source #

toConstr :: LetInfo -> Constr Source #

dataTypeOf :: LetInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> LetInfo -> LetInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LetInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LetInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetInfo -> m LetInfo Source #

Show LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS Source # show :: LetInfo -> String Source # showList :: [LetInfo] -> ShowS Source #
Null LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo Source # null :: LetInfo -> Bool Source #
KillRange LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo Source #
HasRange LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range Source #

data DefInfo Source #

Constructors

DefInfo |

Fields

- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo

Instances

Eq DefInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: DefInfo -> DefInfo -> Bool Source # (/=) :: DefInfo -> DefInfo -> Bool Source #
Data DefInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefInfo -> c DefInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefInfo Source #

toConstr :: DefInfo -> Constr Source #

dataTypeOf :: DefInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> DefInfo -> DefInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DefInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo -> m DefInfo Source #

Show DefInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DefInfo -> ShowS Source # show :: DefInfo -> String Source # showList :: [DefInfo] -> ShowS Source #
KillRange DefInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DefInfo Source #
SetRange DefInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo -> DefInfo Source #
HasRange DefInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: DefInfo -> Range Source #

mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo Source #

mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo Source #

Same as `mkDefInfo` but where we can also give the `IsInstance`

data DeclInfo Source #

Constructors

DeclInfo |

Fields

- declName :: Name
- declRange :: Range

Instances

Eq DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: DeclInfo -> DeclInfo -> Bool Source # (/=) :: DeclInfo -> DeclInfo -> Bool Source #
Data DeclInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclInfo -> c DeclInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DeclInfo Source #

toConstr :: DeclInfo -> Constr Source #

dataTypeOf :: DeclInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DeclInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DeclInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> DeclInfo -> DeclInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> DeclInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclInfo -> m DeclInfo Source #

Show DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DeclInfo -> ShowS Source # show :: DeclInfo -> String Source # showList :: [DeclInfo] -> ShowS Source #
KillRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT DeclInfo Source #
SetRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DeclInfo -> DeclInfo Source #
HasRange DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range Source #

data MutualInfo Source #

Constructors

MutualInfo |

Fields

- mutualTermCheck :: TerminationCheck Name
- mutualPositivityCheck :: PositivityCheck
- mutualRange :: Range

Instances

Eq MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool Source # (/=) :: MutualInfo -> MutualInfo -> Bool Source #
Data MutualInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualInfo -> c MutualInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualInfo Source #

toConstr :: MutualInfo -> Constr Source #

dataTypeOf :: MutualInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> MutualInfo -> MutualInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> MutualInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualInfo -> m MutualInfo Source #

Show MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS Source # show :: MutualInfo -> String Source # showList :: [MutualInfo] -> ShowS Source #
Null MutualInfo Source # | Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo Source # null :: MutualInfo -> Bool Source #
KillRange MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo Source #
HasRange MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source #

newtype LHSInfo Source #

Constructors

LHSRange Range |

Instances

Eq LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: LHSInfo -> LHSInfo -> Bool Source # (/=) :: LHSInfo -> LHSInfo -> Bool Source #
Data LHSInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSInfo -> c LHSInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHSInfo Source #

toConstr :: LHSInfo -> Constr Source #

dataTypeOf :: LHSInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHSInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHSInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> LHSInfo -> LHSInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LHSInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSInfo -> m LHSInfo Source #

Show LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LHSInfo -> ShowS Source # show :: LHSInfo -> String Source # showList :: [LHSInfo] -> ShowS Source #
Null LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo Source # null :: LHSInfo -> Bool Source #
KillRange LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo Source #
HasRange LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range Source #

newtype PatInfo Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range |

Instances

Eq PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool Source # (/=) :: PatInfo -> PatInfo -> Bool Source #
Data PatInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PatInfo -> c PatInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PatInfo Source #

toConstr :: PatInfo -> Constr Source #

dataTypeOf :: PatInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PatInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PatInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> PatInfo -> PatInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PatInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> PatInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PatInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PatInfo -> m PatInfo Source #

Show PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS Source # show :: PatInfo -> String Source # showList :: [PatInfo] -> ShowS Source #
Null PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo Source # null :: PatInfo -> Bool Source #
KillRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT PatInfo Source #
SetRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> PatInfo -> PatInfo Source #
HasRange PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range Source #

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

Constructor pattern info.

Constructors

ConPatInfo |

Fields

- patOrigin :: ConOrigin

  Does this pattern come form the eta-expansion of an implicit pattern?

- patInfo :: PatInfo
- patLazy :: ConPatLazy

Instances

Eq ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatInfo -> ConPatInfo -> Bool Source # (/=) :: ConPatInfo -> ConPatInfo -> Bool Source #
Data ConPatInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatInfo -> c ConPatInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatInfo Source #

toConstr :: ConPatInfo -> Constr Source #

dataTypeOf :: ConPatInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> ConPatInfo -> ConPatInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConPatInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatInfo -> m ConPatInfo Source #

Show ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS Source # show :: ConPatInfo -> String Source # showList :: [ConPatInfo] -> ShowS Source #
KillRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ConPatInfo Source #
SetRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> ConPatInfo -> ConPatInfo Source #
HasRange ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range Source #
EmbPrj ConPatInfo Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatInfo -> S Int32 Source # icod_ :: ConPatInfo -> S Int32 Source # value :: Int32 -> R ConPatInfo Source #

data ConPatLazy Source #

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy | Dotted constructor.
ConPatEager | Ordinary constructor.

Instances

Bounded ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods minBound :: ConPatLazy Source # maxBound :: ConPatLazy Source #
Enum ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

succ :: ConPatLazy -> ConPatLazy Source #

pred :: ConPatLazy -> ConPatLazy Source #

toEnum :: Int -> ConPatLazy Source #

fromEnum :: ConPatLazy -> Int Source #

enumFrom :: ConPatLazy -> [ConPatLazy] Source #

enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy] Source #

enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy] Source #

enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy] Source #

Eq ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatLazy -> ConPatLazy -> Bool Source # (/=) :: ConPatLazy -> ConPatLazy -> Bool Source #
Data ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConPatLazy -> c ConPatLazy Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConPatLazy Source #

toConstr :: ConPatLazy -> Constr Source #

dataTypeOf :: ConPatLazy -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConPatLazy) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConPatLazy) Source #

gmapT :: (forall b. Data b => b -> b) -> ConPatLazy -> ConPatLazy Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConPatLazy -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ConPatLazy -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ConPatLazy -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConPatLazy -> m ConPatLazy Source #

Ord ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

compare :: ConPatLazy -> ConPatLazy -> Ordering Source #

(<) :: ConPatLazy -> ConPatLazy -> Bool Source #

(<=) :: ConPatLazy -> ConPatLazy -> Bool Source #

(>) :: ConPatLazy -> ConPatLazy -> Bool Source #

(>=) :: ConPatLazy -> ConPatLazy -> Bool Source #

max :: ConPatLazy -> ConPatLazy -> ConPatLazy Source #

min :: ConPatLazy -> ConPatLazy -> ConPatLazy Source #

Show ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS Source # show :: ConPatLazy -> String Source # showList :: [ConPatLazy] -> ShowS Source #
EmbPrj ConPatLazy Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: ConPatLazy -> S Int32 Source # icod_ :: ConPatLazy -> S Int32 Source # value :: Int32 -> R ConPatLazy Source #