Safe Haskell	Safe-Inferred
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' t = DefInfo {
- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: Maybe t
}
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
data DeclInfo = DeclInfo {
- declName :: Name
- declRange :: Range
}
data MutualInfo = MutualInfo {
}
data LHSInfo = LHSInfo {
- lhsRange :: Range
- lhsEllipsis :: ExpandedEllipsis
}
newtype PatInfo = PatRange Range
patNoRange :: PatInfo
data ConPatInfo = ConPatInfo {
- conPatOrigin :: ConOrigin
- conPatInfo :: PatInfo
- conPatLazy :: ConPatLazy
}
data ConPatLazy
- = ConPatLazy
- | ConPatEager

Documentation

data MetaInfo Source #

Constructors

MetaInfo
Fields metaRange :: Range metaScope :: ScopeInfo metaNumber :: Maybe MetaId metaNameSuggestion :: String

Instances

Instances details

HasRange MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MetaInfo -> Range Source #
KillRange MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MetaInfo 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 # 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 #
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 #
Show MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaInfo -> ShowS # show :: MetaInfo -> String # showList :: [MetaInfo] -> ShowS #
NFData MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: MetaInfo -> () #
Eq MetaInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaInfo -> MetaInfo -> Bool # (/=) :: MetaInfo -> MetaInfo -> Bool #
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-inplace" '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 Source #

newtype ExprInfo Source #

Constructors

ExprRange Range

Instances

Instances details

HasRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ExprInfo -> Range Source #
KillRange ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT ExprInfo Source #
Null ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: ExprInfo Source # null :: 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 # 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 -> () #
Eq ExprInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ExprInfo -> ExprInfo -> Bool # (/=) :: ExprInfo -> ExprInfo -> Bool #

exprNoRange :: ExprInfo Source #

data AppInfo Source #

Information about application

Constructors

AppInfo
Fields appRange :: Range appOrigin :: Origin appParens :: ParenPreference Do we prefer a lambda argument with or without parens?

Instances

Instances details

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 #
HasRange AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: AppInfo -> Range Source #
KillRange AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT AppInfo 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 # 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 #
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 #
Show AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> AppInfo -> ShowS # show :: AppInfo -> String # showList :: [AppInfo] -> ShowS #
NFData AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: AppInfo -> () #
Eq AppInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: AppInfo -> AppInfo -> Bool # (/=) :: AppInfo -> AppInfo -> Bool #
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 #
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-inplace" '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 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

Instances details

HasRange ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ModuleInfo -> Range 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 #
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 #
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 #
Show ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS # show :: ModuleInfo -> String # showList :: [ModuleInfo] -> ShowS #
NFData ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: ModuleInfo -> () #
Eq ModuleInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ModuleInfo -> ModuleInfo -> Bool # (/=) :: ModuleInfo -> ModuleInfo -> Bool #
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-inplace" '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

HasRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LetInfo -> Range Source #
KillRange LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LetInfo Source #
Null LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: LetInfo Source # null :: 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 # 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 -> () #
Eq LetInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool # (/=) :: LetInfo -> LetInfo -> Bool #

data DefInfo' t Source #

Constructors

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

Instances

Instances details

AnyIsAbstract (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source #
LensIsAbstract (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods lensIsAbstract :: Lens' IsAbstract (DefInfo' t) Source #
HasRange (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DefInfo' t -> Range Source #
KillRange t => KillRange (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT (DefInfo' t) Source #
SetRange (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods setRange :: Range -> DefInfo' t -> DefInfo' t Source #
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) #
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 #
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 #
NFData t => NFData (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: DefInfo' t -> () #
Eq t => Eq (DefInfo' t) Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DefInfo' t -> DefInfo' t -> Bool # (/=) :: DefInfo' t -> DefInfo' t -> Bool #
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-inplace" '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 Source #

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 declName :: Name declRange :: Range

Instances

Instances details

HasRange DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: DeclInfo -> Range 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 #
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 #
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 #
Show DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DeclInfo -> ShowS # show :: DeclInfo -> String # showList :: [DeclInfo] -> ShowS #
NFData DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: DeclInfo -> () #
Eq DeclInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: DeclInfo -> DeclInfo -> Bool # (/=) :: DeclInfo -> DeclInfo -> Bool #
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-inplace" '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 #

Constructors

MutualInfo
Fields mutualTerminationCheck :: TerminationCheck Name mutualCoverageCheck :: CoverageCheck mutualPositivityCheck :: PositivityCheck mutualRange :: Range

Instances

Instances details

HasRange MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: MutualInfo -> Range Source #
KillRange MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT MutualInfo Source #
Null MutualInfo Source #	Default value for `MutualInfo`.
Instance details Defined in Agda.Syntax.Info Methods empty :: MutualInfo Source # null :: 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 # 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 #
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 #
Show MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS # show :: MutualInfo -> String # showList :: [MutualInfo] -> ShowS #
NFData MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: MutualInfo -> () #
Eq MutualInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool # (/=) :: MutualInfo -> MutualInfo -> Bool #
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-inplace" '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
Fields lhsRange :: Range lhsEllipsis :: ExpandedEllipsis

Instances

Instances details

HasRange LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: LHSInfo -> Range Source #
KillRange LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods killRange :: KillRangeT LHSInfo Source #
Null LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: LHSInfo Source # null :: 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 # 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 #
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 #
Show LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LHSInfo -> ShowS # show :: LHSInfo -> String # showList :: [LHSInfo] -> ShowS #
NFData LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: LHSInfo -> () #
Eq LHSInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: LHSInfo -> LHSInfo -> Bool # (/=) :: LHSInfo -> LHSInfo -> Bool #
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-inplace" '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

HasRange PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: PatInfo -> Range 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 #
Null PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods empty :: PatInfo Source # null :: 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 # 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 #
Monoid PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods mempty :: PatInfo # mappend :: PatInfo -> PatInfo -> PatInfo # mconcat :: [PatInfo] -> PatInfo #
Semigroup PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (<>) :: PatInfo -> PatInfo -> PatInfo # sconcat :: NonEmpty PatInfo -> PatInfo # stimes :: Integral b => b -> PatInfo -> PatInfo #
Show PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS # show :: PatInfo -> String # showList :: [PatInfo] -> ShowS #
NFData PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: PatInfo -> () #
Eq PatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool # (/=) :: PatInfo -> PatInfo -> Bool #

patNoRange :: PatInfo Source #

Empty range for patterns.

data ConPatInfo Source #

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

Instances details

HasRange ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods getRange :: ConPatInfo -> Range 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 #
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 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 #
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 #
Show ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS # show :: ConPatInfo -> String # showList :: [ConPatInfo] -> ShowS #
NFData ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: ConPatInfo -> () #
Eq ConPatInfo Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatInfo -> ConPatInfo -> Bool # (/=) :: ConPatInfo -> ConPatInfo -> Bool #
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-inplace" '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

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 #
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 #
Bounded ConPatLazy Source #
Instance details Defined in Agda.Syntax.Info Methods minBound :: ConPatLazy # maxBound :: ConPatLazy #
Enum ConPatLazy Source #
Instance details 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] #
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 #
Show ConPatLazy Source #
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS # show :: ConPatLazy -> String # showList :: [ConPatLazy] -> ShowS #
NFData ConPatLazy Source #
Instance details Defined in Agda.Syntax.Info Methods rnf :: ConPatLazy -> () #
Eq ConPatLazy Source #
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatLazy -> ConPatLazy -> Bool # (/=) :: ConPatLazy -> ConPatLazy -> Bool #
Ord ConPatLazy Source #
Instance details 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 #
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-inplace" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))