Agda.Syntax.Info

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.

Documentation

data MetaInfo

Constructors

MetaInfo

Fields

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

Instances

Eq MetaInfo

Defined in Agda.Syntax.Info

Methods

(==) :: MetaInfo -> MetaInfo -> Bool

(/=) :: MetaInfo -> MetaInfo -> Bool

Data MetaInfo

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

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

toConstr :: MetaInfo -> Constr

dataTypeOf :: MetaInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show MetaInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaInfo -> ShowS

show :: MetaInfo -> String

showList :: [MetaInfo] -> ShowS

Generic MetaInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaInfo :: Type -> Type

Methods

from :: MetaInfo -> Rep MetaInfo x

to :: Rep MetaInfo x -> MetaInfo

NFData MetaInfo

Defined in Agda.Syntax.Info

Methods

rnf :: MetaInfo -> ()

KillRange MetaInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MetaInfo

HasRange MetaInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MetaInfo -> Range

type Rep MetaInfo

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "MetaInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "metaRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "metaScope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo)) :*: (S1 ('MetaSel ('Just "metaNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe MetaId)) :*: S1 ('MetaSel ('Just "metaNameSuggestion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))

emptyMetaInfo :: MetaInfo

newtype ExprInfo

Constructors

ExprRange Range

Instances

Eq ExprInfo

Defined in Agda.Syntax.Info

Methods

(==) :: ExprInfo -> ExprInfo -> Bool

(/=) :: ExprInfo -> ExprInfo -> Bool

Data ExprInfo

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

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

toConstr :: ExprInfo -> Constr

dataTypeOf :: ExprInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ExprInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ExprInfo -> ShowS

show :: ExprInfo -> String

showList :: [ExprInfo] -> ShowS

NFData ExprInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ExprInfo -> ()

Null ExprInfo

Defined in Agda.Syntax.Info

Methods

empty :: ExprInfo

null :: ExprInfo -> Bool

KillRange ExprInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ExprInfo

HasRange ExprInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ExprInfo -> Range

exprNoRange :: ExprInfo

data AppInfo

Information about application

Constructors

AppInfo

Fields

• appRange :: Range
• appOrigin :: Origin
• appParens :: ParenPreference

  Do we prefer a lambda argument with or without parens?

Instances

Eq AppInfo

Defined in Agda.Syntax.Info

Methods

(==) :: AppInfo -> AppInfo -> Bool

(/=) :: AppInfo -> AppInfo -> Bool

Data AppInfo

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

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

toConstr :: AppInfo -> Constr

dataTypeOf :: AppInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AppInfo

Defined in Agda.Syntax.Info

Methods

compare :: AppInfo -> AppInfo -> Ordering

(<) :: AppInfo -> AppInfo -> Bool

(<=) :: AppInfo -> AppInfo -> Bool

(>) :: AppInfo -> AppInfo -> Bool

(>=) :: AppInfo -> AppInfo -> Bool

max :: AppInfo -> AppInfo -> AppInfo

min :: AppInfo -> AppInfo -> AppInfo

Show AppInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> AppInfo -> ShowS

show :: AppInfo -> String

showList :: [AppInfo] -> ShowS

Generic AppInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep AppInfo :: Type -> Type

Methods

from :: AppInfo -> Rep AppInfo x

to :: Rep AppInfo x -> AppInfo

NFData AppInfo

Defined in Agda.Syntax.Info

Methods

rnf :: AppInfo -> ()

KillRange AppInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT AppInfo

HasRange AppInfo

Defined in Agda.Syntax.Info

Methods

getRange :: AppInfo -> Range

LensOrigin AppInfo

Defined in Agda.Syntax.Info

Methods

getOrigin :: AppInfo -> Origin

setOrigin :: Origin -> AppInfo -> AppInfo

mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo

type Rep AppInfo

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "AppInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "appRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: (S1 ('MetaSel ('Just "appOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Origin) :*: S1 ('MetaSel ('Just "appParens") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ParenPreference))))

defaultAppInfo :: Range -> AppInfo

Default is system inserted and prefer parens.

defaultAppInfo_ :: AppInfo

AppInfo with no range information.

data ModuleInfo

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

Defined in Agda.Syntax.Info

Methods

(==) :: ModuleInfo -> ModuleInfo -> Bool

(/=) :: ModuleInfo -> ModuleInfo -> Bool

Data ModuleInfo

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

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

toConstr :: ModuleInfo -> Constr

dataTypeOf :: ModuleInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ModuleInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

Generic ModuleInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep ModuleInfo :: Type -> Type

Methods

from :: ModuleInfo -> Rep ModuleInfo x

to :: Rep ModuleInfo x -> ModuleInfo

NFData ModuleInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ModuleInfo -> ()

KillRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ModuleInfo

SetRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ModuleInfo -> ModuleInfo

HasRange ModuleInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ModuleInfo -> Range

type Rep ModuleInfo

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "ModuleInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "minfoRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "minfoAsTo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "minfoAsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: (S1 ('MetaSel ('Just "minfoOpenShort") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe OpenShortHand)) :*: S1 ('MetaSel ('Just "minfoDirective") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ImportDirective))))))

newtype LetInfo

Constructors

LetRange Range

Instances

Eq LetInfo

Defined in Agda.Syntax.Info

Methods

(==) :: LetInfo -> LetInfo -> Bool

(/=) :: LetInfo -> LetInfo -> Bool

Data LetInfo

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

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

toConstr :: LetInfo -> Constr

dataTypeOf :: LetInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show LetInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LetInfo -> ShowS

show :: LetInfo -> String

showList :: [LetInfo] -> ShowS

NFData LetInfo

Defined in Agda.Syntax.Info

Methods

rnf :: LetInfo -> ()

Null LetInfo

Defined in Agda.Syntax.Info

Methods

empty :: LetInfo

null :: LetInfo -> Bool

KillRange LetInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LetInfo

HasRange LetInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LetInfo -> Range

data DefInfo' t

Constructors

DefInfo

Fields

• defFixity :: Fixity'
• defAccess :: Access
• defAbstract :: IsAbstract
• defInstance :: IsInstance
• defMacro :: IsMacro
• defInfo :: DeclInfo
• defTactic :: Maybe t

Instances

Eq t => Eq (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

(==) :: DefInfo' t -> DefInfo' t -> Bool

(/=) :: DefInfo' t -> DefInfo' t -> Bool

Data t => Data (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefInfo' t -> c (DefInfo' t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefInfo' t)

toConstr :: DefInfo' t -> Constr

dataTypeOf :: DefInfo' t -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> DefInfo' t -> DefInfo' t

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

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

gmapQ :: (forall d. Data d => d -> u) -> DefInfo' t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DefInfo' t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefInfo' t -> m (DefInfo' t)

Show t => Show (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DefInfo' t -> ShowS

show :: DefInfo' t -> String

showList :: [DefInfo' t] -> ShowS

Generic (DefInfo' t)

Defined in Agda.Syntax.Info

Associated Types

type Rep (DefInfo' t) :: Type -> Type

Methods

from :: DefInfo' t -> Rep (DefInfo' t) x

to :: Rep (DefInfo' t) x -> DefInfo' t

NFData t => NFData (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

rnf :: DefInfo' t -> ()

KillRange t => KillRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT (DefInfo' t)

SetRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DefInfo' t -> DefInfo' t

HasRange (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range

AnyIsAbstract (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

anyIsAbstract :: DefInfo' t -> IsAbstract

LensIsAbstract (DefInfo' t)

Defined in Agda.Syntax.Info

Methods

lensIsAbstract :: Lens' IsAbstract (DefInfo' t)

type Rep (DefInfo' t)

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "DefInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity') :*: (S1 ('MetaSel ('Just "defAccess") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Access) :*: S1 ('MetaSel ('Just "defAbstract") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsAbstract))) :*: ((S1 ('MetaSel ('Just "defInstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsInstance) :*: S1 ('MetaSel ('Just "defMacro") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsMacro)) :*: (S1 ('MetaSel ('Just "defInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DeclInfo) :*: S1 ('MetaSel ('Just "defTactic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe t))))))

mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo

Constructors

DeclInfo

Fields

• declName :: Name
• declRange :: Range

Instances

Eq DeclInfo

Defined in Agda.Syntax.Info

Methods

(==) :: DeclInfo -> DeclInfo -> Bool

(/=) :: DeclInfo -> DeclInfo -> Bool

Data DeclInfo

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

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

toConstr :: DeclInfo -> Constr

dataTypeOf :: DeclInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show DeclInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DeclInfo -> ShowS

show :: DeclInfo -> String

showList :: [DeclInfo] -> ShowS

Generic DeclInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep DeclInfo :: Type -> Type

Methods

from :: DeclInfo -> Rep DeclInfo x

to :: Rep DeclInfo x -> DeclInfo

NFData DeclInfo

Defined in Agda.Syntax.Info

Methods

rnf :: DeclInfo -> ()

KillRange DeclInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT DeclInfo

SetRange DeclInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> DeclInfo -> DeclInfo

HasRange DeclInfo

Defined in Agda.Syntax.Info

Methods

getRange :: DeclInfo -> Range

type Rep DeclInfo

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "DeclInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "declName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "declRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data MutualInfo

Constructors

MutualInfo

Fields

• mutualTerminationCheck :: TerminationCheck Name
• mutualCoverageCheck :: CoverageCheck
• mutualPositivityCheck :: PositivityCheck
• mutualRange :: Range

Instances

Eq MutualInfo

Defined in Agda.Syntax.Info

Methods

(==) :: MutualInfo -> MutualInfo -> Bool

(/=) :: MutualInfo -> MutualInfo -> Bool

Data MutualInfo

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

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

toConstr :: MutualInfo -> Constr

dataTypeOf :: MutualInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show MutualInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MutualInfo -> ShowS

show :: MutualInfo -> String

showList :: [MutualInfo] -> ShowS

Generic MutualInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep MutualInfo :: Type -> Type

Methods

from :: MutualInfo -> Rep MutualInfo x

to :: Rep MutualInfo x -> MutualInfo

NFData MutualInfo

Defined in Agda.Syntax.Info

Methods

rnf :: MutualInfo -> ()

Null MutualInfo

Default value for MutualInfo.

Defined in Agda.Syntax.Info

Methods

empty :: MutualInfo

null :: MutualInfo -> Bool

KillRange MutualInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT MutualInfo

HasRange MutualInfo

Defined in Agda.Syntax.Info

Methods

getRange :: MutualInfo -> Range

type Rep MutualInfo

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "MutualInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mutualTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TerminationCheck Name)) :*: S1 ('MetaSel ('Just "mutualCoverageCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CoverageCheck)) :*: (S1 ('MetaSel ('Just "mutualPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PositivityCheck) :*: S1 ('MetaSel ('Just "mutualRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data LHSInfo

Constructors

LHSInfo

Fields

• lhsRange :: Range
• lhsEllipsis :: ExpandedEllipsis

Instances

Eq LHSInfo

Defined in Agda.Syntax.Info

Methods

(==) :: LHSInfo -> LHSInfo -> Bool

(/=) :: LHSInfo -> LHSInfo -> Bool

Data LHSInfo

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

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

toConstr :: LHSInfo -> Constr

dataTypeOf :: LHSInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show LHSInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LHSInfo -> ShowS

show :: LHSInfo -> String

showList :: [LHSInfo] -> ShowS

Generic LHSInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep LHSInfo :: Type -> Type

Methods

from :: LHSInfo -> Rep LHSInfo x

to :: Rep LHSInfo x -> LHSInfo

NFData LHSInfo

Defined in Agda.Syntax.Info

Methods

rnf :: LHSInfo -> ()

Null LHSInfo

Defined in Agda.Syntax.Info

Methods

empty :: LHSInfo

null :: LHSInfo -> Bool

KillRange LHSInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT LHSInfo

HasRange LHSInfo

Defined in Agda.Syntax.Info

Methods

getRange :: LHSInfo -> Range

type Rep LHSInfo

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "LHSInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "lhsEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis)))

newtype PatInfo

For a general pattern we remember the source code position.

Constructors

PatRange Range

Instances

Eq PatInfo

Defined in Agda.Syntax.Info

Methods

(==) :: PatInfo -> PatInfo -> Bool

(/=) :: PatInfo -> PatInfo -> Bool

Data PatInfo

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

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

toConstr :: PatInfo -> Constr

dataTypeOf :: PatInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show PatInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> PatInfo -> ShowS

show :: PatInfo -> String

showList :: [PatInfo] -> ShowS

Semigroup PatInfo

Defined in Agda.Syntax.Info

Methods

(<>) :: PatInfo -> PatInfo -> PatInfo

sconcat :: NonEmpty PatInfo -> PatInfo

stimes :: Integral b => b -> PatInfo -> PatInfo

Monoid PatInfo

Defined in Agda.Syntax.Info

Methods

mempty :: PatInfo

mappend :: PatInfo -> PatInfo -> PatInfo

mconcat :: [PatInfo] -> PatInfo

NFData PatInfo

Defined in Agda.Syntax.Info

Methods

rnf :: PatInfo -> ()

Null PatInfo

Defined in Agda.Syntax.Info

Methods

empty :: PatInfo

null :: PatInfo -> Bool

KillRange PatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT PatInfo

SetRange PatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> PatInfo -> PatInfo

HasRange PatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: PatInfo -> Range

patNoRange :: PatInfo

Empty range for patterns.

data ConPatInfo

Constructor pattern info.

Constructors

ConPatInfo

Fields

• conPatOrigin :: ConOrigin

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

• conPatInfo :: PatInfo
• conPatLazy :: ConPatLazy

Instances

Eq ConPatInfo

Defined in Agda.Syntax.Info

Methods

(==) :: ConPatInfo -> ConPatInfo -> Bool

(/=) :: ConPatInfo -> ConPatInfo -> Bool

Data ConPatInfo

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

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

toConstr :: ConPatInfo -> Constr

dataTypeOf :: ConPatInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Show ConPatInfo

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatInfo -> ShowS

show :: ConPatInfo -> String

showList :: [ConPatInfo] -> ShowS

Generic ConPatInfo

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatInfo :: Type -> Type

Methods

from :: ConPatInfo -> Rep ConPatInfo x

to :: Rep ConPatInfo x -> ConPatInfo

NFData ConPatInfo

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatInfo -> ()

KillRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

killRange :: KillRangeT ConPatInfo

SetRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

setRange :: Range -> ConPatInfo -> ConPatInfo

HasRange ConPatInfo

Defined in Agda.Syntax.Info

Methods

getRange :: ConPatInfo -> Range

EmbPrj ConPatInfo

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatInfo -> S Int32

icod_ :: ConPatInfo -> S Int32

value :: Int32 -> R ConPatInfo

type Rep ConPatInfo

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "ConPatInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conPatOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConOrigin) :*: (S1 ('MetaSel ('Just "conPatInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :*: S1 ('MetaSel ('Just "conPatLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatLazy))))

data ConPatLazy

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances

Bounded ConPatLazy

Defined in Agda.Syntax.Info

Methods

minBound :: ConPatLazy

maxBound :: ConPatLazy

Enum ConPatLazy

Defined in Agda.Syntax.Info

Methods

succ :: ConPatLazy -> ConPatLazy

pred :: ConPatLazy -> ConPatLazy

toEnum :: Int -> ConPatLazy

fromEnum :: ConPatLazy -> Int

enumFrom :: ConPatLazy -> [ConPatLazy]

enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy]

enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy]

enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy]

Eq ConPatLazy

Defined in Agda.Syntax.Info

Methods

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

(/=) :: ConPatLazy -> ConPatLazy -> Bool

Data ConPatLazy

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

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

toConstr :: ConPatLazy -> Constr

dataTypeOf :: ConPatLazy -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConPatLazy

Defined in Agda.Syntax.Info

Methods

compare :: ConPatLazy -> ConPatLazy -> Ordering

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

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

(>) :: ConPatLazy -> ConPatLazy -> Bool

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

max :: ConPatLazy -> ConPatLazy -> ConPatLazy

min :: ConPatLazy -> ConPatLazy -> ConPatLazy

Show ConPatLazy

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatLazy -> ShowS

show :: ConPatLazy -> String

showList :: [ConPatLazy] -> ShowS

Generic ConPatLazy

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatLazy :: Type -> Type

Methods

from :: ConPatLazy -> Rep ConPatLazy x

to :: Rep ConPatLazy x -> ConPatLazy

NFData ConPatLazy

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatLazy -> ()

EmbPrj ConPatLazy

Defined in Agda.TypeChecking.Serialise.Instances.Abstract

Methods

icode :: ConPatLazy -> S Int32

icod_ :: ConPatLazy -> S Int32

value :: Int32 -> R ConPatLazy

type Rep ConPatLazy

Defined in Agda.Syntax.Info

type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.6.2-I0Qlyix7vKjGEzjSnBhBdj" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))