Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data MetaInfo Source #

Constructors

MetaInfo 

Instances

Instances details
Eq MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MetaInfo -> ShowS

show :: MetaInfo -> String

showList :: [MetaInfo] -> ShowS

Generic MetaInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: MetaInfo -> ()

KillRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))))

newtype ExprInfo Source #

Constructors

ExprRange Range 

Instances

Instances details
Eq ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ExprInfo -> ShowS

show :: ExprInfo -> String

showList :: [ExprInfo] -> ShowS

NFData ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ExprInfo -> ()

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

HasRange ExprInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data AppInfo Source #

Information about application

Constructors

AppInfo 

Fields

Instances

Instances details
Eq AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> AppInfo -> ShowS

show :: AppInfo -> String

showList :: [AppInfo] -> ShowS

Generic AppInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: AppInfo -> ()

KillRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

LensOrigin AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

Default is system inserted and prefer parens.

defaultAppInfo_ :: AppInfo Source #

AppInfo with no range information.

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

Instances

Instances details
Eq ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ModuleInfo -> ShowS

show :: ModuleInfo -> String

showList :: [ModuleInfo] -> ShowS

Generic ModuleInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ModuleInfo -> ()

KillRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

Constructors

LetRange Range 

Instances

Instances details
Eq LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LetInfo -> ShowS

show :: LetInfo -> String

showList :: [LetInfo] -> ShowS

NFData LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: LetInfo -> ()

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

HasRange LetInfo Source # 
Instance details

Defined in Agda.Syntax.Info

data DefInfo' t Source #

Instances

Instances details
Eq t => Eq (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

Data t => Data (DefInfo' t) 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' 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) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

show :: DefInfo' t -> String

showList :: [DefInfo' t] -> ShowS

Generic (DefInfo' t) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: DefInfo' t -> ()

KillRange t => KillRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

HasRange (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

getRange :: DefInfo' t -> Range Source #

AnyIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

LensIsAbstract (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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))))))

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

Same as mkDefInfo but where we can also give the IsInstance

data DeclInfo Source #

Constructors

DeclInfo 

Fields

Instances

Instances details
Eq DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> DeclInfo -> ShowS

show :: DeclInfo -> String

showList :: [DeclInfo] -> ShowS

Generic DeclInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: DeclInfo -> ()

KillRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep DeclInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

Instances

Instances details
Eq MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> MutualInfo -> ShowS

show :: MutualInfo -> String

showList :: [MutualInfo] -> ShowS

Generic MutualInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: MutualInfo -> ()

Null MutualInfo Source #

Default value for MutualInfo.

Instance details

Defined in Agda.Syntax.Info

KillRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

Constructors

LHSInfo 

Instances

Instances details
Eq LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> LHSInfo -> ShowS

show :: LHSInfo -> String

showList :: [LHSInfo] -> ShowS

Generic LHSInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: LHSInfo -> ()

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

HasRange LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep LHSInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

For a general pattern we remember the source code position.

Constructors

PatRange Range 

Instances

Instances details
Eq PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> PatInfo -> ShowS

show :: PatInfo -> String

showList :: [PatInfo] -> ShowS

Semigroup PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

sconcat :: NonEmpty PatInfo -> PatInfo

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

Monoid PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

NFData PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: PatInfo -> ()

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

SetRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange PatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

Constructor pattern info.

Constructors

ConPatInfo 

Fields

Instances

Instances details
Eq ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatInfo -> ShowS

show :: ConPatInfo -> String

showList :: [ConPatInfo] -> ShowS

Generic ConPatInfo Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatInfo -> ()

KillRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

SetRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

HasRange ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

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 #

type Rep ConPatInfo Source # 
Instance details

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.6.2.1-LvHTW8pd3Vr2rIoKv0Upjq" '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 Source #

Has the constructor pattern a dotted (forced) constructor?

Constructors

ConPatLazy

Dotted constructor.

ConPatEager

Ordinary constructor.

Instances

Instances details
Bounded ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Enum ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Eq ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Show ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

showsPrec :: Int -> ConPatLazy -> ShowS

show :: ConPatLazy -> String

showList :: [ConPatLazy] -> ShowS

Generic ConPatLazy Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Info

Methods

rnf :: ConPatLazy -> ()

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 #

type Rep ConPatLazy Source # 
Instance details

Defined in Agda.Syntax.Info

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