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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Info

Description

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

Synopsis

- data MetaKind
  - = InstanceMeta
  - | UnificationMeta
- hidingToMetaKind :: Hiding -> MetaKind
- type MetaNameSuggestion = String
- data MetaInfo = MetaInfo {
  - metaRange :: Range
  - metaScope :: ScopeInfo
  - metaNumber :: Maybe MetaId
  - metaNameSuggestion :: MetaNameSuggestion
  - metaKind :: MetaKind
  }
- 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
  - defOpaque :: IsOpaque
  - defInstance :: IsInstance
  - defMacro :: IsMacro
  - defInfo :: DeclInfo
  - defTactic :: TacticAttribute' 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 {
  - mutualTerminationCheck :: TerminationCheck Name
  - mutualCoverageCheck :: CoverageCheck
  - mutualPositivityCheck :: PositivityCheck
  - mutualRange :: Range
  }
- 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 MetaKind Source #

Kind of a meta: the method how to solve it.

Constructors

InstanceMeta | Meta variable solved by instance search.
UnificationMeta | Meta variable solved by unification (default).

#### Instances

Instances details

Null MetaKind Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: MetaKind Source # null :: MetaKind -> Bool Source #
NFData MetaKind Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: MetaKind -> () Source #
Generic MetaKind Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaKind |
Instance details Defined in Agda.Syntax.Info type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: MetaKind -> Rep MetaKind x Source #

to :: Rep MetaKind x -> MetaKind Source #

Show MetaKind Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaKind -> ShowS Source # show :: MetaKind -> String Source # showList :: [MetaKind] -> ShowS Source #
Eq MetaKind Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaKind -> MetaKind -> Bool Source # (/=) :: MetaKind -> MetaKind -> Bool Source #
type Rep MetaKind Source # |
Instance details Defined in Agda.Syntax.Info type Rep MetaKind = D1 ('MetaData "MetaKind" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "InstanceMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnificationMeta" 'PrefixI 'False) (U1 :: Type -> Type))

hidingToMetaKind :: Hiding -> MetaKind Source #

Default meta kind from its `Hiding` context.

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data MetaInfo Source #

Information associated to a meta variable in the abstract syntax.

Constructors

MetaInfo |

Fields

- metaRange :: Range
- metaScope :: ScopeInfo
- metaNumber :: Maybe MetaId
- metaNameSuggestion :: MetaNameSuggestion
- metaKind :: MetaKind

#### 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 #
Null MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: MetaInfo Source # null :: MetaInfo -> Bool Source #
NFData MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: MetaInfo -> () Source #
Generic MetaInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MetaInfo |

Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 MetaNameSuggestion) :*: S1 ('MetaSel ('Just "metaKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaKind)))))

Methods

from :: MetaInfo -> Rep MetaInfo x Source #

to :: Rep MetaInfo x -> MetaInfo Source #

Show MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MetaInfo -> ShowS Source # show :: MetaInfo -> String Source # showList :: [MetaInfo] -> ShowS Source #
Eq MetaInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: MetaInfo -> MetaInfo -> Bool Source # (/=) :: MetaInfo -> MetaInfo -> Bool Source #
type Rep MetaInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep MetaInfo = D1 ('MetaData "MetaInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 MetaNameSuggestion) :*: S1 ('MetaSel ('Just "metaKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaKind)))))

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

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 #
Null AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods empty :: AppInfo Source # null :: AppInfo -> Bool Source #
NFData AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: AppInfo -> () Source #
Generic AppInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep AppInfo |

Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: AppInfo -> Rep AppInfo x Source #

to :: Rep AppInfo x -> AppInfo Source #

Show AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> AppInfo -> ShowS Source # show :: AppInfo -> String Source # showList :: [AppInfo] -> ShowS Source #
Eq AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: AppInfo -> AppInfo -> Bool Source # (/=) :: AppInfo -> AppInfo -> Bool Source #
Ord AppInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods compare :: AppInfo -> AppInfo -> Ordering Source # (<) :: AppInfo -> AppInfo -> Bool Source # (<=) :: AppInfo -> AppInfo -> Bool Source # (>) :: AppInfo -> AppInfo -> Bool Source # (>=) :: AppInfo -> AppInfo -> Bool Source # max :: AppInfo -> AppInfo -> AppInfo Source # min :: AppInfo -> AppInfo -> AppInfo Source #
type Rep AppInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep AppInfo = D1 ('MetaData "AppInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #
NFData ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: ModuleInfo -> () Source #
Generic ModuleInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ModuleInfo |

Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))

Methods

from :: ModuleInfo -> Rep ModuleInfo x Source #

to :: Rep ModuleInfo x -> ModuleInfo Source #

Show ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ModuleInfo -> ShowS Source # show :: ModuleInfo -> String Source # showList :: [ModuleInfo] -> ShowS Source #
Eq ModuleInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ModuleInfo -> ModuleInfo -> Bool Source # (/=) :: ModuleInfo -> ModuleInfo -> Bool Source #
type Rep ModuleInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep ModuleInfo = D1 ('MetaData "ModuleInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #
NFData LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: LetInfo -> () Source #
Show LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LetInfo -> ShowS Source # show :: LetInfo -> String Source # showList :: [LetInfo] -> ShowS Source #
Eq LetInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: LetInfo -> LetInfo -> Bool Source # (/=) :: LetInfo -> LetInfo -> Bool Source #

data DefInfo' t Source #

Constructors

DefInfo |

Fields

- defFixity :: Fixity'
- defAccess :: Access
- defAbstract :: IsAbstract
- defOpaque :: IsOpaque
- defInstance :: IsInstance
- defMacro :: IsMacro
- defInfo :: DeclInfo
- defTactic :: TacticAttribute' t

#### Instances

Instances details

AllAreOpaque (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source #
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' (DefInfo' t) IsAbstract Source #
LensIsOpaque (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods lensIsOpaque :: Lens' (DefInfo' t) IsOpaque 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 #
NFData t => NFData (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: DefInfo' t -> () Source #
Generic (DefInfo' t) Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep (DefInfo' t) |

Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "defOpaque") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsOpaque))) :*: ((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 (TacticAttribute' t))))))

Methods

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

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

Show t => Show (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DefInfo' t -> ShowS Source # show :: DefInfo' t -> String Source # showList :: [DefInfo' t] -> ShowS Source #
Eq t => Eq (DefInfo' t) Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: DefInfo' t -> DefInfo' t -> Bool Source # (/=) :: DefInfo' t -> DefInfo' t -> Bool Source #
type Rep (DefInfo' t) Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep (DefInfo' t) = D1 ('MetaData "DefInfo'" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "defOpaque") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IsOpaque))) :*: ((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 (TacticAttribute' 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 #
NFData DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: DeclInfo -> () Source #
Generic DeclInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep DeclInfo |

Instance details

Defined in Agda.Syntax.Info

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

Methods

from :: DeclInfo -> Rep DeclInfo x Source #

to :: Rep DeclInfo x -> DeclInfo Source #

Show DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> DeclInfo -> ShowS Source # show :: DeclInfo -> String Source # showList :: [DeclInfo] -> ShowS Source #
Eq DeclInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: DeclInfo -> DeclInfo -> Bool Source # (/=) :: DeclInfo -> DeclInfo -> Bool Source #
type Rep DeclInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep DeclInfo = D1 ('MetaData "DeclInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #
NFData MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: MutualInfo -> () Source #
Generic MutualInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep MutualInfo |

Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: MutualInfo -> Rep MutualInfo x Source #

to :: Rep MutualInfo x -> MutualInfo Source #

Show MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> MutualInfo -> ShowS Source # show :: MutualInfo -> String Source # showList :: [MutualInfo] -> ShowS Source #
Eq MutualInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: MutualInfo -> MutualInfo -> Bool Source # (/=) :: MutualInfo -> MutualInfo -> Bool Source #
type Rep MutualInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep MutualInfo = D1 ('MetaData "MutualInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #
NFData LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: LHSInfo -> () Source #
Generic LHSInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep LHSInfo |

Instance details

Defined in Agda.Syntax.Info

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

Methods

from :: LHSInfo -> Rep LHSInfo x Source #

to :: Rep LHSInfo x -> LHSInfo Source #

Show LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> LHSInfo -> ShowS Source # show :: LHSInfo -> String Source # showList :: [LHSInfo] -> ShowS Source #
Eq LHSInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: LHSInfo -> LHSInfo -> Bool Source # (/=) :: LHSInfo -> LHSInfo -> Bool Source #
type Rep LHSInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep LHSInfo = D1 ('MetaData "LHSInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #
NFData PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: PatInfo -> () Source #
Monoid PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods mempty :: PatInfo Source # mappend :: PatInfo -> PatInfo -> PatInfo Source # mconcat :: [PatInfo] -> PatInfo Source #
Semigroup PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (<>) :: PatInfo -> PatInfo -> PatInfo Source # sconcat :: NonEmpty PatInfo -> PatInfo Source # stimes :: Integral b => b -> PatInfo -> PatInfo Source #
Show PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> PatInfo -> ShowS Source # show :: PatInfo -> String Source # showList :: [PatInfo] -> ShowS Source #
Eq PatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: PatInfo -> PatInfo -> Bool Source # (/=) :: PatInfo -> PatInfo -> Bool Source #

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 Word32 Source # icod_ :: ConPatInfo -> S Word32 Source # value :: Word32 -> R ConPatInfo Source #
NFData ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: ConPatInfo -> () Source #
Generic ConPatInfo Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatInfo |

Instance details

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: ConPatInfo -> Rep ConPatInfo x Source #

to :: Rep ConPatInfo x -> ConPatInfo Source #

Show ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatInfo -> ShowS Source # show :: ConPatInfo -> String Source # showList :: [ConPatInfo] -> ShowS Source #
Eq ConPatInfo Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatInfo -> ConPatInfo -> Bool Source # (/=) :: ConPatInfo -> ConPatInfo -> Bool Source #
type Rep ConPatInfo Source # |

Instance details

Defined in Agda.Syntax.Info

type Rep ConPatInfo = D1 ('MetaData "ConPatInfo" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: ConPatLazy -> S Word32 Source # value :: Word32 -> R ConPatLazy Source #
NFData ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods rnf :: ConPatLazy -> () Source #
Bounded ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods minBound :: ConPatLazy Source # maxBound :: ConPatLazy Source #
Enum ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

succ :: ConPatLazy -> ConPatLazy Source #

pred :: ConPatLazy -> ConPatLazy Source #

toEnum :: Int -> ConPatLazy Source #

fromEnum :: ConPatLazy -> Int Source #

enumFrom :: ConPatLazy -> [ConPatLazy] Source #

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

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

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

Generic ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Associated Types

type Rep ConPatLazy |
Instance details Defined in Agda.Syntax.Info type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ConPatLazy -> Rep ConPatLazy x Source #

to :: Rep ConPatLazy x -> ConPatLazy Source #

Show ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods showsPrec :: Int -> ConPatLazy -> ShowS Source # show :: ConPatLazy -> String Source # showList :: [ConPatLazy] -> ShowS Source #
Eq ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info Methods (==) :: ConPatLazy -> ConPatLazy -> Bool Source # (/=) :: ConPatLazy -> ConPatLazy -> Bool Source #
Ord ConPatLazy Source # |

Instance details

Defined in Agda.Syntax.Info

Methods

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

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

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

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

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

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

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

type Rep ConPatLazy Source # |
Instance details Defined in Agda.Syntax.Info type Rep ConPatLazy = D1 ('MetaData "ConPatLazy" "Agda.Syntax.Info" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ConPatLazy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConPatEager" 'PrefixI 'False) (U1 :: Type -> Type))