| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- Induction
- Hiding
- Relevance
- Origin of arguments (user-written, inserted or reflected)
- 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.
- data Delayed
- 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 Big
- data Relevance
- = Relevant
- | NonStrict
- | Irrelevant
- | Forced Big
- allRelevances :: [Relevance]
- class LensRelevance a where
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- irrelevant :: Relevance -> Bool
- unusableRelevance :: LensRelevance a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- ignoreForced :: Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- defaultArgInfo :: ArgInfo
- 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 |
Induction
Constructors
| Inductive | |
| CoInductive |
Hiding
data Overlappable #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
| Eq Overlappable # | |
| Data Overlappable # | |
| Ord Overlappable # | |
| Show Overlappable # | |
| Semigroup Overlappable # | Just for the |
| Monoid Overlappable # | |
| NFData Overlappable # | |
Constructors
| Hidden | |
| Instance Overlappable | |
| NotHidden |
Instances
| Eq Hiding # | |
| Data Hiding # | |
| Ord Hiding # | |
| Show Hiding # | |
| Semigroup Hiding # |
|
| Monoid Hiding # | |
| NFData Hiding # | |
| KillRange Hiding # | |
| LensHiding Hiding # | |
| ChooseFlex Hiding # | |
| Unquote Hiding # | |
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) # | |
data WithHiding a #
Decorating something with Hiding information.
Constructors
| WithHiding | |
Instances
| Functor WithHiding # | |
| Applicative WithHiding # | |
| Foldable WithHiding # | |
| Traversable WithHiding # | |
| Decoration WithHiding # | |
| Eq a => Eq (WithHiding a) # | |
| Data a => Data (WithHiding a) # | |
| Ord a => Ord (WithHiding a) # | |
| Show a => Show (WithHiding a) # | |
| NFData a => NFData (WithHiding a) # | |
| KillRange a => KillRange (WithHiding a) # | |
| SetRange a => SetRange (WithHiding a) # | |
| HasRange a => HasRange (WithHiding a) # | |
| LensHiding (WithHiding a) # | |
| PrettyTCM a => PrettyTCM (WithHiding a) # | |
| ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) # | |
| ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) # | |
| AddContext ([WithHiding Name], Dom Type) # | |
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.
Relevance
An constructor argument is big if the sort of its type is bigger than
the sort of the data type. Only parameters (and maybe forced arguments)
are allowed to be big.
List : Set -> Set
nil : (A : Set) -> List A
A is big in constructor nil as the sort Set1 of its type Set
is bigger than the sort Set of the data type List.
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. |
| Forced Big | The argument can be skipped during equality checking because its value is already determined by the type. If a constructor argument is big, it has to be regarded absent, otherwise we get into paradoxes. |
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 #
moreRelevant :: Relevance -> Relevance -> Bool #
Information ordering.
Relevant `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
irrelevant :: Relevance -> Bool #
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).
ignoreForced :: Relevance -> Relevance #
For comparing Relevance ignoring Forced.
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. |
data WithOrigin a #
Decorating something with Origin information.
Constructors
| WithOrigin | |
Instances
| Functor WithOrigin # | |
| Foldable WithOrigin # | |
| Traversable WithOrigin # | |
| Decoration WithOrigin # | |
| Eq a => Eq (WithOrigin a) # | |
| Data a => Data (WithOrigin a) # | |
| Ord a => Ord (WithOrigin a) # | |
| Show a => Show (WithOrigin a) # | |
| NFData a => NFData (WithOrigin a) # | |
| KillRange a => KillRange (WithOrigin a) # | |
| SetRange a => SetRange (WithOrigin a) # | |
| HasRange a => HasRange (WithOrigin a) # | |
| LensOrigin (WithOrigin a) # | |
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 LamInfo # | |
| LensOrigin (Dom e) # | |
| LensOrigin (Arg e) # | |
| LensOrigin (WithOrigin a) # | |
| LensOrigin (Elim' a) # | This instance cheats on |
| LensOrigin (FlexibleVar a) # | |
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields | |
class LensArgInfo a where #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo #
setArgInfo :: ArgInfo -> a -> a #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a #
Instances
| LensArgInfo ArgInfo # | |
| LensArgInfo (Dom e) # | |
| LensArgInfo (Arg a) # | |
Arguments
Instances
defaultArg :: a -> Arg a #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] #
Names
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
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 # | |
| Traversable Ranged # | |
| Decoration Ranged # | |
| MapNamedArgPattern NAP # | |
| UniverseBi Declaration RString # | |
| PatternVars a (NamedArg (Pattern' a)) # | |
| Eq a => Eq (Ranged a) # | |
| Data a => Data (Ranged a) # | |
| Ord a => Ord (Ranged a) # | |
| Show a => Show (Ranged a) # | |
| Show a => Show (Named_ a) # | |
| NFData a => NFData (Ranged a) # | Ranges are not forced. |
| KillRange (Ranged a) # | |
| HasRange (Ranged a) # | |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) # | |
| NormaliseProjP a => NormaliseProjP (Named_ a) # | |
| ToAbstract [Arg Term] [NamedArg Expr] # | |
| ToAbstract r a => ToAbstract (Arg r) (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. |
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.
Access modifier.
Constructors
| PrivateAccess Origin | Store the |
| PublicAccess | |
| OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
data IsInstance #
Is this definition eligible for instance search?
Constructors
| InstanceDef | |
| NotInstanceDef |
Instances
Is this a macro definition?
Constructors
| MacroDef | |
| NotMacroDef |
NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Meta variables
A meta variable identifier is just a natural number.
Instances
| Enum MetaId # | |
| Eq MetaId # | |
| Integral MetaId # | |
| Data MetaId # | |
| Num MetaId # | |
| Ord MetaId # | |
| Real MetaId # | |
| Show MetaId # | Show non-record version of this newtype. |
| NFData MetaId # | |
| Pretty MetaId # | |
| GetDefs MetaId # | |
| HasFresh MetaId # | |
| PrettyTCM MetaId # | |
| UnFreezeMeta MetaId # | |
| IsInstantiatedMeta MetaId # | |
| FromTerm MetaId # | |
| ToTerm MetaId # | |
| PrimTerm MetaId # | |
| Unquote MetaId # | |
| Reify MetaId Expr # | |
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
| Functor MaybePlaceholder # | |
| Foldable MaybePlaceholder # | |
| Traversable MaybePlaceholder # | |
| Eq e => Eq (MaybePlaceholder e) # | |
| Data e => Data (MaybePlaceholder e) # | |
| Ord e => Ord (MaybePlaceholder e) # | |
| Show e => Show (MaybePlaceholder e) # | |
| NFData a => NFData (MaybePlaceholder a) # | |
| KillRange a => KillRange (MaybePlaceholder a) # | |
| HasRange a => HasRange (MaybePlaceholder a) # | |
| ExprLike a => ExprLike (MaybePlaceholder a) # | |
noPlaceholder :: e -> MaybePlaceholder e #
An abbreviation: noPlaceholder = .NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId #
Constructors
| InteractionId | |
Fields
| |
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
| (Eq b, Eq a) => Eq (ImportDirective' a b) # | |
| (Data b, Data a) => Data (ImportDirective' a b) # | |
| (NFData a, NFData b) => NFData (ImportDirective' a b) # | Ranges are not forced. |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) # | |
| (HasRange a, HasRange b) => HasRange (ImportDirective' a b) # | |
Constructors
| UseEverything | |
| Using [ImportedName' a b] |
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
| (Eq a, Eq b) => Eq (ImportedName' a b) # | |
| (Data b, Data a) => Data (ImportedName' a b) # | |
| (Ord a, Ord b) => Ord (ImportedName' a b) # | |
| (Show a, Show b) => Show (ImportedName' a b) # | |
| (NFData a, NFData b) => NFData (ImportedName' a b) # | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) # | |
| (HasRange a, HasRange b) => HasRange (ImportedName' a b) # | |
setImportedName :: ImportedName' a a -> a -> ImportedName' a a #
Constructors
| Renaming | |
Fields
| |
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
| Functor TerminationCheck # | |
| Eq m => Eq (TerminationCheck m) # | |
| Data m => Data (TerminationCheck m) # | |
| Show m => Show (TerminationCheck m) # | |
| NFData a => NFData (TerminationCheck a) # | |
| KillRange m => KillRange (TerminationCheck m) # | |
Positivity
type PositivityCheck = Bool #
Positivity check? (Default = True).