| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- Eta-equality
- Induction
- Hiding
- Modalities
- Quantities
- Relevance
- Origin of arguments (user-written, inserted or reflected)
- Free variable annotations
- Argument decoration
- Arguments
- Names
- Function type domain
- Named arguments
- Range decoration.
- Raw names (before parsing into name parts).
- Further constructor and projection info
- Infixity, access, abstract, etc.
- NameId
- Meta variables
- Placeholders (used to parse sections)
- Interaction meta variables
- Import directive
- Termination
- Positivity
Description
Some common syntactic entities are defined in this module.
Synopsis
- data Delayed
- data HasEta
- data Induction
- data Overlappable
- data Hiding
- data WithHiding a = WithHiding {}
- class LensHiding a where
- mergeHiding :: LensHiding a => WithHiding a -> a
- visible :: LensHiding a => a -> Bool
- notVisible :: LensHiding a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- isOverlappable :: LensHiding a => a -> Bool
- isInstance :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- data Modality = Modality {}
- defaultModality :: Modality
- class LensModality a where
- getRelevanceMod :: LensModality a => LensGet Relevance a
- setRelevanceMod :: LensModality a => LensSet Relevance a
- mapRelevanceMod :: LensModality a => LensMap Relevance a
- getQuantityMod :: LensModality a => LensGet Quantity a
- setQuantityMod :: LensModality a => LensSet Quantity a
- mapQuantityMod :: LensModality a => LensMap Quantity a
- data Quantity
- defaultQuantity :: Quantity
- class LensQuantity a where
- data Relevance
- allRelevances :: [Relevance]
- defaultRelevance :: Relevance
- class LensRelevance a where
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- isNonStrict :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- unusableRelevance :: LensRelevance a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data FreeVariables
- unknownFreeVariables :: FreeVariables
- noFreeVariables :: FreeVariables
- oneFreeVariable :: Int -> FreeVariables
- freeVariablesFromList :: [Int] -> FreeVariables
- class LensFreeVariables a where
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- defaultArgInfo :: ArgInfo
- getHidingArgInfo :: LensArgInfo a => LensGet Hiding a
- setHidingArgInfo :: LensArgInfo a => LensSet Hiding a
- mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
- getModalityArgInfo :: LensArgInfo a => LensGet Modality a
- setModalityArgInfo :: LensArgInfo a => LensSet Modality a
- mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
- getOriginArgInfo :: LensArgInfo a => LensGet Origin a
- setOriginArgInfo :: LensArgInfo a => LensSet Origin a
- mapOriginArgInfo :: LensArgInfo a => LensMap Origin a
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a
- data Arg e = Arg {}
- defaultArg :: a -> Arg a
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- class Eq a => Underscore a where
- data Dom e = Dom {}
- argFromDom :: Dom a -> Arg a
- domFromArg :: Arg a -> Dom a
- defaultDom :: a -> Dom a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- type Named_ = Named RString
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg a = Arg (Named_ a)
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- setNamedArg :: NamedArg a -> b -> NamedArg b
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- unranged :: a -> Ranged a
- type RawName = String
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- type RString = Ranged RawName
- data ConOrigin
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data ProjOrigin
- data DataOrRecord
- data IsInfix
- data Access
- data IsAbstract
- data IsInstance
- data IsMacro
- type Nat = Int
- type Arity = Nat
- data NameId = NameId !Word64 !Word64
- newtype MetaId = MetaId {}
- newtype Constr a = Constr a
- data PositionInName
- data MaybePlaceholder e
- noPlaceholder :: e -> MaybePlaceholder e
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data ImportDirective' a b = ImportDirective {
- importDirRange :: Range
- using :: Using' a b
- hiding :: [ImportedName' a b]
- impRenaming :: [Renaming' a b]
- publicOpen :: Bool
- data Using' a b
- = UseEverything
- | Using [ImportedName' a b]
- defaultImportDir :: ImportDirective' a b
- isDefaultImportDir :: ImportDirective' a b -> Bool
- data ImportedName' a b
- = ImportedModule b
- | ImportedName a
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- data Renaming' a b = Renaming {
- renFrom :: ImportedName' a b
- renTo :: ImportedName' a b
- renToRange :: Range
- data TerminationCheck m
- type PositivityCheck = Bool
Delayed
Used to specify whether something should be delayed.
Constructors
| Delayed | |
| NotDelayed |
Instances
| Eq Delayed # | |
| Data Delayed # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Delayed -> c Delayed # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Delayed # toConstr :: Delayed -> Constr # dataTypeOf :: Delayed -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Delayed) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Delayed) # gmapT :: (forall b. Data b => b -> b) -> Delayed -> Delayed # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Delayed -> r # gmapQ :: (forall d. Data d => d -> u) -> Delayed -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Delayed -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Delayed -> m Delayed # | |
| Ord Delayed # | |
| Show Delayed # | |
| KillRange Delayed # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj Delayed # | |
Eta-equality
Instances
| Eq HasEta # | |
| Data HasEta # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HasEta -> c HasEta # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HasEta # toConstr :: HasEta -> Constr # dataTypeOf :: HasEta -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HasEta) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HasEta) # gmapT :: (forall b. Data b => b -> b) -> HasEta -> HasEta # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HasEta -> r # gmapQ :: (forall d. Data d => d -> u) -> HasEta -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HasEta -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HasEta -> m HasEta # | |
| Ord HasEta # | |
| Show HasEta # | |
| NFData HasEta # | |
Defined in Agda.Syntax.Common | |
| KillRange HasEta # | |
Defined in Agda.Syntax.Common Methods | |
| HasRange HasEta # | |
Defined in Agda.Syntax.Common | |
| EmbPrj HasEta # | |
Induction
Constructors
| Inductive | |
| CoInductive |
Instances
| Eq Induction # | |
| Data Induction # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Induction -> c Induction # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Induction # toConstr :: Induction -> Constr # dataTypeOf :: Induction -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Induction) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Induction) # gmapT :: (forall b. Data b => b -> b) -> Induction -> Induction # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Induction -> r # gmapQ :: (forall d. Data d => d -> u) -> Induction -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Induction -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Induction -> m Induction # | |
| Ord Induction # | |
| Show Induction # | |
| NFData Induction # | |
Defined in Agda.Syntax.Common | |
| Pretty Induction # | |
Defined in Agda.Syntax.Concrete.Pretty | |
| KillRange Induction # | |
Defined in Agda.Syntax.Common Methods | |
| HasRange Induction # | |
Defined in Agda.Syntax.Common | |
| EmbPrj Induction # | |
Hiding
data Overlappable #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
Constructors
| Hidden | |
| Instance Overlappable | |
| NotHidden |
Instances
| Eq Hiding # | |
| Data Hiding # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hiding -> c Hiding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hiding # toConstr :: Hiding -> Constr # dataTypeOf :: Hiding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Hiding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hiding) # gmapT :: (forall b. Data b => b -> b) -> Hiding -> Hiding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hiding -> r # gmapQ :: (forall d. Data d => d -> u) -> Hiding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Hiding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hiding -> m Hiding # | |
| Ord Hiding # | |
| Show Hiding # | |
| Semigroup Hiding # |
|
| Monoid Hiding # | |
| NFData Hiding # | |
Defined in Agda.Syntax.Common | |
| KillRange Hiding # | |
Defined in Agda.Syntax.Common Methods | |
| LensHiding Hiding # | |
| EmbPrj Hiding # | |
| ChooseFlex Hiding # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice # | |
| Unquote Hiding # | |
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) # | |
data WithHiding a #
Decorating something with Hiding information.
Constructors
| WithHiding | |
Instances
class LensHiding a where #
A lens to access the Hiding attribute in data structures.
Minimal implementation: getHiding and one of setHiding or mapHiding.
Minimal complete definition
Instances
mergeHiding :: LensHiding a => WithHiding a -> a #
Monoidal composition of Hiding information in some data.
visible :: LensHiding a => a -> Bool #
NotHidden arguments are visible.
notVisible :: LensHiding a => a -> Bool #
:: LensHiding a => a -> Bool #
Hidden arguments are hidden.
hide :: LensHiding a => a -> a #
hideOrKeepInstance :: LensHiding a => a -> a #
makeInstance :: LensHiding a => a -> a #
makeInstance' :: LensHiding a => Overlappable -> a -> a #
isOverlappable :: LensHiding a => a -> Bool #
isInstance :: LensHiding a => a -> Bool #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool #
Ignores Overlappable.
Modalities
We have a tuple of modalities, which might not be fully orthogonal. For instance, irrelevant stuff is also run-time irrelevant.
Constructors
| Modality | |
Fields
| |
Instances
class LensModality a where #
Minimal complete definition
Methods
getModality :: a -> Modality #
setModality :: Modality -> a -> a #
mapModality :: (Modality -> Modality) -> a -> a #
Instances
| LensModality ArgInfo # | |
Defined in Agda.Syntax.Common Methods getModality :: ArgInfo -> Modality # setModality :: Modality -> ArgInfo -> ArgInfo # mapModality :: (Modality -> Modality) -> ArgInfo -> ArgInfo # | |
| LensModality Modality # | |
Defined in Agda.Syntax.Common Methods getModality :: Modality -> Modality # setModality :: Modality -> Modality -> Modality # mapModality :: (Modality -> Modality) -> Modality -> Modality # | |
| LensModality (Dom e) # | |
Defined in Agda.Syntax.Common | |
| LensModality (Arg e) # | |
Defined in Agda.Syntax.Common | |
getRelevanceMod :: LensModality a => LensGet Relevance a #
setRelevanceMod :: LensModality a => LensSet Relevance a #
mapRelevanceMod :: LensModality a => LensMap Relevance a #
getQuantityMod :: LensModality a => LensGet Quantity a #
setQuantityMod :: LensModality a => LensSet Quantity a #
mapQuantityMod :: LensModality a => LensMap Quantity a #
Quantities
Quantity for linearity.
Constructors
| Quantity0 | Zero uses, erased at runtime. TODO: | Quantity1 -- ^ Linear use (could be updated destructively). (needs postponable constraints between quantities to compute uses). |
| Quantityω | Unrestricted use. |
Instances
| Bounded Quantity # | |
| Enum Quantity # | |
Defined in Agda.Syntax.Common | |
| Eq Quantity # | |
| Data Quantity # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantity -> c Quantity # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantity # toConstr :: Quantity -> Constr # dataTypeOf :: Quantity -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantity) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantity) # gmapT :: (forall b. Data b => b -> b) -> Quantity -> Quantity # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantity -> r # gmapQ :: (forall d. Data d => d -> u) -> Quantity -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantity -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantity -> m Quantity # | |
| Ord Quantity # | Note that the order is |
Defined in Agda.Syntax.Common | |
| Show Quantity # | |
| Generic Quantity # | |
| Semigroup Quantity # | Composition of quantities (multiplication).
|
| Monoid Quantity # | In the absense of finite quantities besides 0, ω is the unit. |
| NFData Quantity # | |
Defined in Agda.Syntax.Common | |
| PartialOrd Quantity # | |
Defined in Agda.Syntax.Common Methods | |
| POMonoid Quantity # | |
Defined in Agda.Syntax.Common | |
| POSemigroup Quantity # | |
Defined in Agda.Syntax.Common | |
| KillRange Quantity # | |
Defined in Agda.Syntax.Common Methods | |
| LensQuantity Quantity # | |
Defined in Agda.Syntax.Common Methods getQuantity :: Quantity -> Quantity # setQuantity :: Quantity -> Quantity -> Quantity # mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity # | |
| EmbPrj Quantity # | |
| type Rep Quantity # | |
class LensQuantity a where #
Minimal complete definition
Methods
getQuantity :: a -> Quantity #
setQuantity :: Quantity -> a -> a #
mapQuantity :: (Quantity -> Quantity) -> a -> a #
Instances
| LensQuantity ArgInfo # | |
Defined in Agda.Syntax.Common Methods getQuantity :: ArgInfo -> Quantity # setQuantity :: Quantity -> ArgInfo -> ArgInfo # mapQuantity :: (Quantity -> Quantity) -> ArgInfo -> ArgInfo # | |
| LensQuantity Quantity # | |
Defined in Agda.Syntax.Common Methods getQuantity :: Quantity -> Quantity # setQuantity :: Quantity -> Quantity -> Quantity # mapQuantity :: (Quantity -> Quantity) -> Quantity -> Quantity # | |
| LensQuantity Modality # | |
Defined in Agda.Syntax.Common Methods getQuantity :: Modality -> Quantity # setQuantity :: Quantity -> Modality -> Modality # mapQuantity :: (Quantity -> Quantity) -> Modality -> Modality # | |
| LensQuantity (Dom e) # | |
Defined in Agda.Syntax.Common | |
| LensQuantity (Arg e) # | |
Defined in Agda.Syntax.Common | |
Relevance
A function argument can be relevant or irrelevant. See Agda.TypeChecking.Irrelevance.
Constructors
| Relevant | The argument is (possibly) relevant at compile-time. |
| NonStrict | The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking. |
| Irrelevant | The argument is irrelevant at compile- and runtime. |
Instances
allRelevances :: [Relevance] #
class LensRelevance a where #
A lens to access the Relevance attribute in data structures.
Minimal implementation: getRelevance and one of setRelevance or mapRelevance.
Minimal complete definition
Methods
getRelevance :: a -> Relevance #
setRelevance :: Relevance -> a -> a #
mapRelevance :: (Relevance -> Relevance) -> a -> a #
Instances
isRelevant :: LensRelevance a => a -> Bool #
isIrrelevant :: LensRelevance a => a -> Bool #
isNonStrict :: LensRelevance a => a -> Bool #
moreRelevant :: Relevance -> Relevance -> Bool #
Information ordering.
Relevant `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
unusableRelevance :: LensRelevance a => a -> Bool #
unusableRelevance rel == True iff we cannot use a variable of rel.
composeRelevance :: Relevance -> Relevance -> Relevance #
Relevance composition.
Irrelevant is dominant, Relevant is neutral.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance #
inverseComposeRelevance r x returns the most irrelevant y
such that forall x, y we have
x `moreRelevant` (r `composeRelevance` y)
iff
(r `inverseComposeRelevance` x) `moreRelevant` y (Galois connection).
irrToNonStrict :: Relevance -> Relevance #
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToRel :: Relevance -> Relevance #
Applied when working on types (unless --experimental-irrelevance).
nonStrictToIrr :: Relevance -> Relevance #
Origin of arguments (user-written, inserted or reflected)
Origin of arguments.
Constructors
| UserWritten | From the source file / user input. (Preserve!) |
| Inserted | E.g. inserted hidden arguments. |
| Reflected | Produced by the reflection machinery. |
| CaseSplit | Produced by an interactive case split. |
Instances
| Eq Origin # | |
| Data Origin # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Origin -> c Origin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Origin # toConstr :: Origin -> Constr # dataTypeOf :: Origin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Origin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Origin) # gmapT :: (forall b. Data b => b -> b) -> Origin -> Origin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Origin -> r # gmapQ :: (forall d. Data d => d -> u) -> Origin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Origin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Origin -> m Origin # | |
| Ord Origin # | |
| Show Origin # | |
| NFData Origin # | |
Defined in Agda.Syntax.Common | |
| KillRange Origin # | |
Defined in Agda.Syntax.Common Methods | |
| LensOrigin Origin # | |
| EmbPrj Origin # | |
| ChooseFlex Origin # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice # | |
data WithOrigin a #
Decorating something with Origin information.
Constructors
| WithOrigin | |
Instances
class LensOrigin a where #
A lens to access the Origin attribute in data structures.
Minimal implementation: getOrigin and one of setOrigin or mapOrigin.
Minimal complete definition
Instances
| LensOrigin ArgInfo # | |
| LensOrigin Origin # | |
| LensOrigin AppInfo # | |
| LensOrigin (Dom e) # | |
| LensOrigin (Arg e) # | |
| LensOrigin (WithOrigin a) # | |
Defined in Agda.Syntax.Common Methods getOrigin :: WithOrigin a -> Origin # setOrigin :: Origin -> WithOrigin a -> WithOrigin a # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a # | |
| LensOrigin (Elim' a) # | This instance cheats on |
| LensOrigin (FlexibleVar a) # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getOrigin :: FlexibleVar a -> Origin # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a # | |
Free variable annotations
data FreeVariables #
Constructors
| UnknownFVs | |
| KnownFVs IntSet |
Instances
oneFreeVariable :: Int -> FreeVariables #
freeVariablesFromList :: [Int] -> FreeVariables #
class LensFreeVariables a where #
A lens to access the FreeVariables attribute in data structures.
Minimal implementation: getFreeVariables and one of setFreeVariables or mapFreeVariables.
Minimal complete definition
Methods
getFreeVariables :: a -> FreeVariables #
setFreeVariables :: FreeVariables -> a -> a #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a #
Instances
| LensFreeVariables ArgInfo # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo # | |
| LensFreeVariables FreeVariables # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables # | |
| LensFreeVariables (Dom e) # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: Dom e -> FreeVariables # setFreeVariables :: FreeVariables -> Dom e -> Dom e # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom e -> Dom e # | |
| LensFreeVariables (Arg e) # | |
Defined in Agda.Syntax.Common Methods getFreeVariables :: Arg e -> FreeVariables # setFreeVariables :: FreeVariables -> Arg e -> Arg e # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e # | |
hasNoFreeVariables :: LensFreeVariables a => a -> Bool #
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields | |
Instances
class LensArgInfo a where #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo #
setArgInfo :: ArgInfo -> a -> a #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a #
Instances
| LensArgInfo ArgInfo # | |
Defined in Agda.Syntax.Common | |
| LensArgInfo (Dom e) # | |
Defined in Agda.Syntax.Common | |
| LensArgInfo (Arg a) # | |
Defined in Agda.Syntax.Common | |
getHidingArgInfo :: LensArgInfo a => LensGet Hiding a #
setHidingArgInfo :: LensArgInfo a => LensSet Hiding a #
mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a #
getModalityArgInfo :: LensArgInfo a => LensGet Modality a #
setModalityArgInfo :: LensArgInfo a => LensSet Modality a #
mapModalityArgInfo :: LensArgInfo a => LensMap Modality a #
getOriginArgInfo :: LensArgInfo a => LensGet Origin a #
setOriginArgInfo :: LensArgInfo a => LensSet Origin a #
mapOriginArgInfo :: LensArgInfo a => LensMap Origin a #
getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a #
setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a #
mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a #
Arguments
Instances
defaultArg :: a -> Arg a #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] #
Names
class Eq a => Underscore a where #
Minimal complete definition
Instances
| Underscore String # | |
Defined in Agda.Syntax.Common | |
| Underscore ByteString # | |
Defined in Agda.Syntax.Common | |
| Underscore Doc # | |
Defined in Agda.Syntax.Common | |
| Underscore QName # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore Name # | |
Defined in Agda.Syntax.Concrete.Name | |
| Underscore Expr # | |
Defined in Agda.Syntax.Abstract | |
Function type domain
Similar to Arg, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
Dom is used in Pi of internal syntax, in Context and Telescope.
Arg is used for actual arguments (Var, Con, Def etc.)
and in Abstract syntax and other situations.
Instances
argFromDom :: Dom a -> Arg a #
domFromArg :: Arg a -> Dom a #
defaultDom :: a -> Dom a #
Named arguments
Something potentially carrying a name.
Constructors
| Named | |
Fields
| |
Instances
| MapNamedArgPattern NAP # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| PatternVars a (NamedArg (Pattern' a)) # | |
Defined in Agda.Syntax.Internal | |
| MapNamedArgPattern a (NamedArg (Pattern' a)) # | Modify the content of Note: the |
| Subst t a => Subst t (Named name a) # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Named name a -> Named name a # | |
| PatternLike a b => PatternLike a (Named x b) # | |
Defined in Agda.Syntax.Internal.Pattern | |
| APatternLike a b => APatternLike a (Named n b) # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| Functor (Named name) # | |
| Show a => Show (Named_ a) # | |
| Foldable (Named name) # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Named name m -> m # foldMap :: Monoid m => (a -> m) -> Named name a -> m # foldr :: (a -> b -> b) -> b -> Named name a -> b # foldr' :: (a -> b -> b) -> b -> Named name a -> b # foldl :: (b -> a -> b) -> b -> Named name a -> b # foldl' :: (b -> a -> b) -> b -> Named name a -> b # foldr1 :: (a -> a -> a) -> Named name a -> a # foldl1 :: (a -> a -> a) -> Named name a -> a # toList :: Named name a -> [a] # null :: Named name a -> Bool # length :: Named name a -> Int # elem :: Eq a => a -> Named name a -> Bool # maximum :: Ord a => Named name a -> a # minimum :: Ord a => Named name a -> a # | |
| Traversable (Named name) # | |
Defined in Agda.Syntax.Common | |
| Decoration (Named name) # | |
| Pretty e => Pretty (Named_ e) # | |
Defined in Agda.Syntax.Concrete.Pretty | |
| Apply [NamedArg (Pattern' a)] # | Make sure we only drop variable patterns. |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) # | |
| NormaliseProjP a => NormaliseProjP (Named_ a) # | |
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) # | |
| ToAbstract [Arg Term] [NamedArg Expr] # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToAbstract r a => ToAbstract (Arg r) (NamedArg a) # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) # | |
| (Eq name, Eq a) => Eq (Named name a) # | |
| (Data name, Data a) => Data (Named name a) # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Named name a -> c (Named name a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Named name a) # toConstr :: Named name a -> Constr # dataTypeOf :: Named name a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Named name a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Named name a)) # gmapT :: (forall b. Data b => b -> b) -> Named name a -> Named name a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Named name a -> r # gmapQ :: (forall d. Data d => d -> u) -> Named name a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Named name a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Named name a -> m (Named name a) # | |
| (Ord name, Ord a) => Ord (Named name a) # | |
Defined in Agda.Syntax.Common | |
| (NFData name, NFData a) => NFData (Named name a) # | |
Defined in Agda.Syntax.Common | |
| (KillRange name, KillRange a) => KillRange (Named name a) # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Named name a) # | |
| SetRange a => SetRange (Named name a) # | |
| HasRange a => HasRange (Named name a) # | |
Defined in Agda.Syntax.Common | |
| IsProjP a => IsProjP (Named n a) # | |
Defined in Agda.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| CPatternLike p => CPatternLike (Named n p) # | |
Defined in Agda.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m # traverseCPatternA :: (Applicative m, Functor m) => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) # | |
| IsWithP p => IsWithP (Named n p) # | |
| ExprLike a => ExprLike (Named name a) # | |
| MaybePostfixProjP a => MaybePostfixProjP (Named n a) # | |
Defined in Agda.Syntax.Abstract Methods maybePostfixProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) # | |
| SubstExpr a => SubstExpr (Named name a) # | |
| AllNames a => AllNames (Named name a) # | |
| CountPatternVars a => CountPatternVars (Named x a) # | |
Defined in Agda.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int # | |
| ExprLike a => ExprLike (Named x a) # | |
Defined in Agda.Syntax.Abstract.Views | |
| (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) # | |
| NamesIn a => NamesIn (Named n a) # | |
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) # | |
Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Named n a -> TCM (Named n a) # | |
| InstantiateFull t => InstantiateFull (Named name t) # | |
Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Named name t -> ReduceM (Named name t) # | |
| Normalise t => Normalise (Named name t) # | |
Defined in Agda.TypeChecking.Reduce Methods normalise' :: Named name t -> ReduceM (Named name t) # | |
| Simplify t => Simplify (Named name t) # | |
| IsFlexiblePattern a => IsFlexiblePattern (Named name a) # | |
Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Named name a -> TCM Bool # | |
| PatternVarModalities a x => PatternVarModalities (Named s a) x # | |
Defined in Agda.Syntax.Internal.Pattern Methods patternVarModalities :: Named s a -> [(x, Modality)] # | |
| ToConcrete a c => ToConcrete (Named name a) (Named name c) # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete | |
| TermToPattern a b => TermToPattern (Named c a) (Named c b) # | |
Defined in Agda.TypeChecking.Patterns.Internal Methods termToPattern :: Named c a -> TCM (Named c b) # | |
| Reify i a => Reify (Named n i) (Named n a) # | |
| ToAbstract r a => ToAbstract (Named name r) (Named name a) # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Named name r -> WithNames (Named name a) # | |
| ToAbstract c a => ToAbstract (Named name c) (Named name a) # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Named name c -> ScopeM (Named name a) # | |
| LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i # | |
Defined in Agda.Syntax.Internal.Pattern Methods labelPatVars :: Named x a -> State [i] (Named x b) # unlabelPatVars :: Named x b -> Named x a # | |
defaultNamedArg :: a -> NamedArg a #
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b #
The functor instance for NamedArg would be ambiguous,
so we give it another name here.
setNamedArg :: NamedArg a -> b -> NamedArg b #
setNamedArg a b = updateNamedArg (const b) a
Range decoration.
Thing with range info.
Constructors
| Ranged | |
Fields
| |
Instances
| Functor Ranged # | |
| Foldable Ranged # | |
Defined in Agda.Syntax.Common Methods fold :: Monoid m => Ranged m -> m # foldMap :: Monoid m => (a -> m) -> Ranged a -> m # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # | |
| Traversable Ranged # | |
| Decoration Ranged # | |
| MapNamedArgPattern NAP # | |
Defined in Agda.Syntax.Abstract.Pattern | |
| UniverseBi Declaration RString # | |
Defined in Agda.Syntax.Abstract Methods universeBi :: Declaration -> [RString] # | |
| PatternVars a (NamedArg (Pattern' a)) # | |
Defined in Agda.Syntax.Internal | |
| MapNamedArgPattern a (NamedArg (Pattern' a)) # | Modify the content of Note: the |
| Eq a => Eq (Ranged a) # | |
| Data a => Data (Ranged a) # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) # toConstr :: Ranged a -> Constr # dataTypeOf :: Ranged a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) # gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r # gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) # | |
| Ord a => Ord (Ranged a) # | |
Defined in Agda.Syntax.Common | |
| Show a => Show (Ranged a) # | |
| Show a => Show (Named_ a) # | |
| NFData a => NFData (Ranged a) # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
| Pretty e => Pretty (Named_ e) # | |
Defined in Agda.Syntax.Concrete.Pretty | |
| KillRange (Ranged a) # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Ranged a) # | |
| HasRange (Ranged a) # | |
Defined in Agda.Syntax.Common | |
| Apply [NamedArg (Pattern' a)] # | Make sure we only drop variable patterns. |
| EmbPrj a => EmbPrj (Ranged a) # | |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) # | |
| NormaliseProjP a => NormaliseProjP (Named_ a) # | |
Defined in Agda.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) # | |
| ToAbstract [Arg Term] [NamedArg Expr] # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract | |
| ToAbstract r a => ToAbstract (Arg r) (NamedArg a) # | |
Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Arg r -> WithNames (NamedArg a) # | |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String #
stringToRawName :: String -> RawName #
Further constructor and projection info
Where does the ConP or Con come from?
Constructors
| ConOSystem | Inserted by system or expanded from an implicit pattern. |
| ConOCon | User wrote a constructor (pattern). |
| ConORec | User wrote a record (pattern). |
| ConOSplit | Generated by interactive case splitting. |
Instances
| Bounded ConOrigin # | |
| Enum ConOrigin # | |
Defined in Agda.Syntax.Common Methods succ :: ConOrigin -> ConOrigin # pred :: ConOrigin -> ConOrigin # fromEnum :: ConOrigin -> Int # enumFrom :: ConOrigin -> [ConOrigin] # enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] # | |
| Eq ConOrigin # | |
| Data ConOrigin # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConOrigin -> c ConOrigin # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConOrigin # toConstr :: ConOrigin -> Constr # dataTypeOf :: ConOrigin -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConOrigin) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConOrigin) # gmapT :: (forall b. Data b => b -> b) -> ConOrigin -> ConOrigin # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConOrigin -> r # gmapQ :: (forall d. Data d => d -> u) -> ConOrigin -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ConOrigin -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConOrigin -> m ConOrigin # | |
| Ord ConOrigin # | |
| Show ConOrigin # | |
| KillRange ConOrigin # | |
Defined in Agda.Syntax.Common Methods | |
| EmbPrj ConOrigin # | |
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin #
Prefer user-written over system-inserted.
data ProjOrigin #
Where does a projection come from?
Constructors
| ProjPrefix | User wrote a prefix projection. |
| ProjPostfix | User wrote a postfix projection. |
| ProjSystem | Projection was generated by the system. |
Instances
data DataOrRecord #
Instances
Infixity, access, abstract, etc.
Functions can be defined in both infix and prefix style. See
LHS.
Instances
| Eq IsInfix # | |
| Data IsInfix # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsInfix -> c IsInfix # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsInfix # toConstr :: IsInfix -> Constr # dataTypeOf :: IsInfix -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsInfix) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsInfix) # gmapT :: (forall b. Data b => b -> b) -> IsInfix -> IsInfix # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsInfix -> r # gmapQ :: (forall d. Data d => d -> u) -> IsInfix -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsInfix -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsInfix -> m IsInfix # | |
| Ord IsInfix # | |
| Show IsInfix # | |
Access modifier.
Constructors
| PrivateAccess Origin | Store the |
| PublicAccess | |
| OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
Instances
| Eq Access # | |
| Data Access # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Access -> c Access # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Access # toConstr :: Access -> Constr # dataTypeOf :: Access -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Access) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Access) # gmapT :: (forall b. Data b => b -> b) -> Access -> Access # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Access -> r # gmapQ :: (forall d. Data d => d -> u) -> Access -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Access -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Access -> m Access # | |
| Ord Access # | |
| Show Access # | |
| NFData Access # | |
Defined in Agda.Syntax.Common | |
| Pretty Access # | |
Defined in Agda.Syntax.Common | |
| KillRange Access # | |
Defined in Agda.Syntax.Common Methods | |
| HasRange Access # | |
Defined in Agda.Syntax.Common | |
| EmbPrj Access # | |
data IsAbstract #
Abstract or concrete
Constructors
| AbstractDef | |
| ConcreteDef |
Instances
data IsInstance #
Is this definition eligible for instance search?
Constructors
| InstanceDef | |
| NotInstanceDef |
Instances
Is this a macro definition?
Constructors
| MacroDef | |
| NotMacroDef |
Instances
| Eq IsMacro # | |
| Data IsMacro # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsMacro -> c IsMacro # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsMacro # toConstr :: IsMacro -> Constr # dataTypeOf :: IsMacro -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsMacro) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsMacro) # gmapT :: (forall b. Data b => b -> b) -> IsMacro -> IsMacro # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsMacro -> r # gmapQ :: (forall d. Data d => d -> u) -> IsMacro -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsMacro -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsMacro -> m IsMacro # | |
| Ord IsMacro # | |
| Show IsMacro # | |
| KillRange IsMacro # | |
Defined in Agda.Syntax.Common Methods | |
| HasRange IsMacro # | |
Defined in Agda.Syntax.Common | |
NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Instances
| Enum NameId # | |
Defined in Agda.Syntax.Common | |
| Eq NameId # | |
| Data NameId # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NameId -> c NameId # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NameId # toConstr :: NameId -> Constr # dataTypeOf :: NameId -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NameId) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NameId) # gmapT :: (forall b. Data b => b -> b) -> NameId -> NameId # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NameId -> r # gmapQ :: (forall d. Data d => d -> u) -> NameId -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NameId -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NameId -> m NameId # | |
| Ord NameId # | |
| Show NameId # | |
| Generic NameId # | |
| NFData NameId # | |
Defined in Agda.Syntax.Common | |
| Hashable NameId # | |
Defined in Agda.Syntax.Common | |
| Pretty NameId # | |
Defined in Agda.TypeChecking.Reduce.Fast | |
| KillRange NameId # | |
Defined in Agda.Syntax.Common Methods | |
| HasFresh NameId # | |
Defined in Agda.TypeChecking.Monad.Base | |
| EmbPrj NameId # | |
| type Rep NameId # | |
Defined in Agda.Syntax.Common type Rep NameId = D1 (MetaData "NameId" "Agda.Syntax.Common" "Agda-2.5.4-BdDHVHYPm5JDI57G7c5E26" False) (C1 (MetaCons "NameId" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64) :*: S1 (MetaSel (Nothing :: Maybe Symbol) SourceUnpack SourceStrict DecidedStrict) (Rec0 Word64))) | |
Meta variables
A meta variable identifier is just a natural number.
Instances
Constructors
| Constr a |
Instances
| ToConcrete (Constr Constructor) Declaration # | |
Defined in Agda.Syntax.Translation.AbstractToConcrete Methods toConcrete :: Constr Constructor -> AbsToCon Declaration # bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b # | |
Placeholders (used to parse sections)
data PositionInName #
The position of a name part or underscore in a name.
Constructors
| Beginning | The following underscore is at the beginning of the name:
|
| Middle | The following underscore is in the middle of the name:
|
| End | The following underscore is at the end of the name: |
Instances
data MaybePlaceholder e #
Placeholders are used to represent the underscores in a section.
Constructors
| Placeholder !PositionInName | |
| NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
noPlaceholder :: e -> MaybePlaceholder e #
An abbreviation: noPlaceholder = .NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId #
Constructors
| InteractionId | |
Fields
| |
Instances
Import directive
data ImportDirective' a b #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import, namespace, or open declarations).
Constructors
| ImportDirective | |
Fields
| |
Instances
Constructors
| UseEverything | |
| Using [ImportedName' a b] |
Instances
| (Eq b, Eq a) => Eq (Using' a b) # | |
| (Data a, Data b) => Data (Using' a b) # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Using' a b -> c (Using' a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Using' a b) # toConstr :: Using' a b -> Constr # dataTypeOf :: Using' a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Using' a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Using' a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Using' a b -> Using' a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Using' a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Using' a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Using' a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Using' a b -> m (Using' a b) # | |
| Semigroup (Using' a b) # | |
| Monoid (Using' a b) # | |
| (NFData a, NFData b) => NFData (Using' a b) # | |
Defined in Agda.Syntax.Common | |
| (Pretty a, Pretty b) => Pretty (Using' a b) # | |
Defined in Agda.Syntax.Concrete.Pretty | |
| (KillRange a, KillRange b) => KillRange (Using' a b) # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Using' a b) # | |
| (HasRange a, HasRange b) => HasRange (Using' a b) # | |
Defined in Agda.Syntax.Common | |
defaultImportDir :: ImportDirective' a b #
Default is directive is private (use everything, but do not export).
isDefaultImportDir :: ImportDirective' a b -> Bool #
data ImportedName' a b #
An imported name can be a module or a defined name
Constructors
| ImportedModule b | |
| ImportedName a |
Instances
setImportedName :: ImportedName' a a -> a -> ImportedName' a a #
Constructors
| Renaming | |
Fields
| |
Instances
| (Eq b, Eq a) => Eq (Renaming' a b) # | |
| (Data a, Data b) => Data (Renaming' a b) # | |
Defined in Agda.Syntax.Common Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Renaming' a b -> c (Renaming' a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Renaming' a b) # toConstr :: Renaming' a b -> Constr # dataTypeOf :: Renaming' a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Renaming' a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Renaming' a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Renaming' a b -> Renaming' a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming' a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Renaming' a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming' a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming' a b -> m (Renaming' a b) # | |
| (NFData a, NFData b) => NFData (Renaming' a b) # | Ranges are not forced. |
Defined in Agda.Syntax.Common | |
| (KillRange a, KillRange b) => KillRange (Renaming' a b) # | |
Defined in Agda.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) # | |
| (HasRange a, HasRange b) => HasRange (Renaming' a b) # | |
Defined in Agda.Syntax.Common | |
HasRange instances
KillRange instances
NFData instances
Termination
data TerminationCheck m #
Termination check? (Default = TerminationCheck).
Constructors
| TerminationCheck | Run the termination checker. |
| NoTerminationCheck | Skip termination checking (unsafe). |
| NonTerminating | Treat as non-terminating. |
| Terminating | Treat as terminating (unsafe). Same effect as |
| TerminationMeasure Range m | Skip termination checking but use measure instead. |
Instances
Positivity
type PositivityCheck = Bool #
Positivity check? (Default = True).