| Safe Haskell | None |
|---|
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
- data Delayed
- = Delayed
- | NotDelayed
- data Induction
- = Inductive
- | CoInductive
- data Hiding
- class LensHiding a where
- 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
- makeInstance :: LensHiding a => a -> a
- data Relevance
- = Relevant
- | NonStrict
- | Irrelevant
- | Forced
- | UnusedArg
- 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
- data ArgInfo c = ArgInfo {
- argInfoHiding :: Hiding
- argInfoRelevance :: Relevance
- argInfoColors :: [c]
- mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c'
- defaultArgInfo :: ArgInfo c
- data Arg c e = Arg {}
- mapArgInfo :: (ArgInfo c -> ArgInfo c') -> Arg c a -> Arg c' a
- argColors :: Arg c e -> [c]
- mapArgColors :: ([c] -> [c']) -> Arg c a -> Arg c' a
- setArgColors :: [c] -> Arg c' a -> Arg c a
- defaultArg :: a -> Arg c a
- defaultColoredArg :: ([c], a) -> Arg c a
- noColorArg :: Hiding -> Relevance -> a -> Arg c a
- withArgsFrom :: [a] -> [Arg c b] -> [Arg c a]
- withNamedArgsFrom :: [a] -> [NamedArg c b] -> [NamedArg c a]
- data Dom c e = Dom {}
- mapDomInfo :: (ArgInfo c -> ArgInfo c') -> Dom c a -> Dom c' a
- domColors :: Dom c e -> [c]
- argFromDom :: Dom c a -> Arg c a
- domFromArg :: Arg c a -> Dom c a
- defaultDom :: a -> Dom c a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg c a = Arg c (Named RString a)
- namedArg :: NamedArg c a -> a
- defaultNamedArg :: a -> NamedArg c a
- updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c b
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- unranged :: a -> Ranged a
- type RString = Ranged String
- data IsInfix
- data Access
- data IsAbstract
- type Nat = Int
- type Arity = Nat
- data NameId = NameId Integer Integer
- newtype Constr a = Constr a
- newtype InteractionId = InteractionId {
- interactionId :: Nat
Delayed
Used to specify whether something should be delayed.
Constructors
| Delayed | |
| NotDelayed |
Induction
Constructors
| Inductive | |
| CoInductive |
Hiding
class LensHiding a whereSource
A lens to access the Hiding attribute in data structures.
Minimal implementation: getHiding and one of setHiding or mapHiding.
Instances
| LensHiding Hiding | |
| LensHiding (ArgInfo c) | |
| LensHiding (FlexibleVar a) | |
| LensHiding (Dom c e) | |
| LensHiding (Arg c e) |
notHidden :: LensHiding a => a -> BoolSource
visible :: LensHiding a => a -> BoolSource
NotHidden arguments are visible.
notVisible :: LensHiding a => a -> BoolSource
hide :: LensHiding a => a -> aSource
makeInstance :: LensHiding a => a -> aSource
Relevance
A function argument can be relevant or irrelevant.
See 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 | The argument can be skipped during equality checking because its value is already determined by the type. |
| 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 |
class LensRelevance a whereSource
A lens to access the Relevance attribute in data structures.
Minimal implementation: getRelevance and one of setRelevance or mapRelevance.
Methods
getRelevance :: a -> RelevanceSource
setRelevance :: Relevance -> a -> aSource
mapRelevance :: (Relevance -> Relevance) -> a -> aSource
Instances
| LensRelevance Relevance | |
| LensRelevance (ArgInfo c) | |
| LensRelevance (Dom c e) | |
| LensRelevance (Arg c e) |
isRelevant :: LensRelevance a => a -> BoolSource
isIrrelevant :: LensRelevance a => a -> BoolSource
moreRelevant :: Relevance -> Relevance -> BoolSource
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
| ArgInfo | |
Fields
| |
Instances
| Functor ArgInfo | |
| Typeable1 ArgInfo | |
| Foldable ArgInfo | |
| Traversable ArgInfo | |
| Unquote ArgInfo | |
| ToAbstract ArgInfo ArgInfo | |
| Reify ArgInfo ArgInfo | |
| ConvColor ArgInfo ArgInfo | |
| Eq c => Eq (ArgInfo c) | |
| Ord c => Ord (ArgInfo c) | |
| Show c => Show (ArgInfo c) | |
| KillRange c => KillRange (ArgInfo c) | |
| LensRelevance (ArgInfo c) | |
| LensHiding (ArgInfo c) | |
| GetDefs c => GetDefs (ArgInfo c) | |
| EmbPrj c => EmbPrj (ArgInfo c) | |
| SynEq c => SynEq (ArgInfo c) | |
| ToConcrete (ArgInfo ac) ArgInfo |
mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c'Source
Arguments
Instances
mapArgColors :: ([c] -> [c']) -> Arg c a -> Arg c' aSource
setArgColors :: [c] -> Arg c' a -> Arg c aSource
defaultArg :: a -> Arg c aSource
defaultColoredArg :: ([c], a) -> Arg c aSource
noColorArg :: Hiding -> Relevance -> a -> Arg c aSource
withArgsFrom :: [a] -> [Arg c b] -> [Arg c a]Source
withNamedArgsFrom :: [a] -> [NamedArg c b] -> [NamedArg c a]Source
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 c a -> Arg c aSource
domFromArg :: Arg c a -> Dom c aSource
defaultDom :: a -> Dom c aSource
Named arguments
Constructors
| Named | |
Fields
| |
Instances
defaultNamedArg :: a -> NamedArg c aSource
updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c bSource
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 | |
| Typeable1 Ranged | |
| Foldable Ranged | |
| Traversable Ranged | |
| Decoration Ranged | |
| UniverseBi Declaration RString | |
| Eq a => Eq (Ranged a) | |
| Ord a => Ord (Ranged a) | |
| Show a => Show (Ranged a) | |
| KillRange (Ranged a) | |
| HasRange (Ranged a) | |
| EmbPrj a => EmbPrj (Ranged a) | |
| ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a) | |
| Show a => Show (Named RString a) | |
| Pretty e => Pretty (Named RString e) | |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named RString a) |
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. |
The unique identifier of a name. Second argument is the top-level module identifier.
Interaction meta variables
newtype InteractionId Source
Constructors
| InteractionId | |
Fields
| |