| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
- data Delayed
- data Induction
- data Hiding
- data WithHiding a = WithHiding !Hiding a
- class LensHiding a where
- mergeHiding :: LensHiding a => WithHiding a -> a
- isHidden :: LensHiding a => a -> Bool
- notHidden :: LensHiding a => a -> Bool
- visible :: LensHiding a => a -> Bool
- notVisible :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- data Big
- data Relevance
- allRelevances :: [Relevance]
- class LensRelevance a where
- getRelevance :: a -> Relevance
- setRelevance :: Relevance -> a -> a
- mapRelevance :: (Relevance -> Relevance) -> a -> a
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- irrelevantOrUnused :: Relevance -> Bool
- unusableRelevance :: Relevance -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- ignoreForced :: Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- 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
- underscore :: a
- isUnderscore :: a -> Bool
- 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
- 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 ConPOrigin
- data IsInfix
- data Access
- data IsAbstract
- data IsInstance
- data IsMacro
- type Nat = Int
- type Arity = Nat
- data NameId = NameId !Integer !Integer
- newtype MetaId = MetaId {}
- newtype Constr a = Constr a
- data Placeholder
- data 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
Instances
| Eq Hiding Source | |
| Ord Hiding Source | |
| Show Hiding Source | |
| Monoid Hiding Source |
|
| NFData Hiding Source | |
| KillRange Hiding Source | |
| LensHiding Hiding Source | |
| GenC Hiding Source | |
| ChooseFlex Hiding Source | |
| Unquote Hiding Source | |
| ShrinkC Hiding Hiding Source |
data WithHiding a Source
Decorating something with Hiding information.
Constructors
| WithHiding !Hiding a |
Instances
| Functor WithHiding Source | |
| Applicative WithHiding Source | |
| Foldable WithHiding Source | |
| Traversable WithHiding Source | |
| Decoration WithHiding Source | |
| Eq a => Eq (WithHiding a) Source | |
| Ord a => Ord (WithHiding a) Source | |
| Show a => Show (WithHiding a) Source | |
| NFData a => NFData (WithHiding a) Source | |
| KillRange a => KillRange (WithHiding a) Source | |
| SetRange a => SetRange (WithHiding a) Source | |
| HasRange a => HasRange (WithHiding a) Source | |
| LensHiding (WithHiding a) Source | |
| PrettyTCM a => PrettyTCM (WithHiding a) Source | |
| ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) Source | |
| ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) Source | |
| AddContext ([WithHiding Name], Dom Type) Source |
class LensHiding a where Source
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 Source
Monoidal composition of Hiding information in some data.
notHidden :: LensHiding a => a -> Bool Source
visible :: LensHiding a => a -> Bool Source
NotHidden arguments are visible.
notVisible :: LensHiding a => a -> Bool Source
hide :: LensHiding a => a -> a Source
hideOrKeepInstance :: LensHiding a => a -> a Source
makeInstance :: LensHiding a => a -> a Source
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. |
| UnusedArg | The polarity checker has determined that this argument
is unused in the definition. It can be skipped during
equality checking but should be mined for solutions
of meta-variables with relevance |
allRelevances :: [Relevance] Source
class LensRelevance a where Source
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 Source
setRelevance :: Relevance -> a -> a Source
mapRelevance :: (Relevance -> Relevance) -> a -> a Source
isRelevant :: LensRelevance a => a -> Bool Source
isIrrelevant :: LensRelevance a => a -> Bool Source
moreRelevant :: Relevance -> Relevance -> Bool Source
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
unusableRelevance :: Relevance -> Bool Source
unusableRelevance rel == True iff we cannot use a variable of rel.
composeRelevance :: Relevance -> Relevance -> Relevance Source
Relevance composition.
Irrelevant is dominant, Relevant is neutral.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source
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 Source
For comparing Relevance ignoring Forced and UnusedArg.
irrToNonStrict :: Relevance -> Relevance Source
Irrelevant function arguments may appear non-strictly in the codomain type.
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields | |
class LensArgInfo a where Source
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo Source
setArgInfo :: ArgInfo -> a -> a Source
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source
Instances
| LensArgInfo ArgInfo Source | |
| LensArgInfo (Dom e) Source | |
| LensArgInfo (Arg a) Source |
Arguments
Instances
defaultArg :: a -> Arg a Source
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source
Names
class Eq a => Underscore a where Source
Minimal complete definition
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 Source
domFromArg :: Arg a -> Dom a Source
defaultDom :: a -> Dom a Source
Named arguments
Something potentially carrying a name.
Constructors
| Named | |
Fields
| |
Instances
defaultNamedArg :: a -> NamedArg a Source
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source
The functor instance for NamedArg would be ambiguous,
so we give it another name here.
Range decoration.
Thing with range info.
Constructors
| Ranged | |
Fields
| |
Instances
| Functor Ranged Source | |
| Foldable Ranged Source | |
| Traversable Ranged Source | |
| Decoration Ranged Source | |
| UniverseBi Declaration RString | |
| Eq a => Eq (Ranged a) Source | |
| Ord a => Ord (Ranged a) Source | |
| Show a => Show (Ranged a) Source | |
| Show a => Show (Named_ a) Source | |
| NFData a => NFData (Ranged a) Source | Ranges are not forced. |
| KillRange (Ranged a) Source | |
| HasRange (Ranged a) Source | |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source | |
| ToAbstract [Arg Term] [NamedArg Expr] Source | |
| ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String Source
stringToRawName :: String -> RawName Source
Constructor pattern info
data ConPOrigin Source
Where does the ConP of come from?
Constructors
| ConPImplicit | Expanded from an implicit pattern. |
| ConPCon | User wrote a constructor pattern. |
| ConPRec | User wrote a record pattern. |
Infixity, access, abstract, etc.
Functions can be defined in both infix and prefix style. See
LHS.
Access modifier.
Constructors
| PrivateAccess | |
| PublicAccess | |
| OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
data IsInstance Source
Is this definition eligible for instance search?
Constructors
| InstanceDef | |
| NotInstanceDef |
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 Source | |
| Eq MetaId Source | |
| Integral MetaId Source | |
| Num MetaId Source | |
| Ord MetaId Source | |
| Real MetaId Source | |
| Show MetaId Source | Show non-record version of this newtype. |
| NFData MetaId Source | |
| Pretty MetaId Source | |
| GetDefs MetaId Source | |
| HasFresh MetaId Source | |
| UnFreezeMeta MetaId Source | |
| IsInstantiatedMeta MetaId Source | |
| PrettyTCM MetaId Source | |
| FromTerm MetaId Source | |
| ToTerm MetaId Source | |
| PrimTerm MetaId Source | |
| Unquote MetaId Source | |
| Reify MetaId Expr Source |
Constructors
| Constr a |
Instances
data Placeholder Source
Instances
data MaybePlaceholder e Source
Placeholders are used to represent the underscores in a section.
Constructors
| Placeholder !Placeholder | |
| NoPlaceholder e |
Instances
| Functor MaybePlaceholder Source | |
| Foldable MaybePlaceholder Source | |
| Traversable MaybePlaceholder Source | |
| Eq e => Eq (MaybePlaceholder e) Source | |
| Ord e => Ord (MaybePlaceholder e) Source | |
| Show e => Show (MaybePlaceholder e) Source | |
| NFData a => NFData (MaybePlaceholder a) Source | |
| KillRange a => KillRange (MaybePlaceholder a) Source | |
| HasRange a => HasRange (MaybePlaceholder a) Source | |
| ExprLike a => ExprLike (MaybePlaceholder a) Source |
Interaction meta variables
newtype InteractionId Source
Constructors
| InteractionId | |
Fields
| |
Import directive
data ImportDirective' a b Source
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 a, Eq b) => Eq (ImportDirective' a b) Source | |
| (NFData a, NFData b) => NFData (ImportDirective' a b) Source | Ranges are not forced. |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source | |
| (HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source |
Constructors
| UseEverything | |
| Using [ImportedName' a b] |
defaultImportDir :: ImportDirective' a b Source
Default is directive is private (use everything, but do not export).
isDefaultImportDir :: ImportDirective' a b -> Bool Source
data ImportedName' a b Source
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) Source | |
| (Ord a, Ord b) => Ord (ImportedName' a b) Source | |
| (Show a, Show b) => Show (ImportedName' a b) Source | |
| (NFData a, NFData b) => NFData (ImportedName' a b) Source | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) Source | |
| (HasRange a, HasRange b) => HasRange (ImportedName' a b) Source |
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source
Constructors
| Renaming | |
Fields
| |
HasRange instances
KillRange instances
NFData instances
Termination
data TerminationCheck m Source
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 Source | |
| Eq m => Eq (TerminationCheck m) Source | |
| Show m => Show (TerminationCheck m) Source | |
| NFData a => NFData (TerminationCheck a) Source | |
| KillRange m => KillRange (TerminationCheck m) Source |
Positivity
type PositivityCheck = Bool Source
Positivity check? (Default = True).