| 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
- data Relevance
- = Relevant
- | NonStrict
- | Irrelevant
- | Forced
- | UnusedArg
- moreRelevant :: Relevance -> Relevance -> Bool
- data Dom e = Dom {
- domHiding :: Hiding
- domRelevance :: Relevance
- unDom :: e
- argFromDom :: Dom a -> Arg a
- domFromArg :: Arg a -> Dom a
- mapDomHiding :: (Hiding -> Hiding) -> Dom a -> Dom a
- mapDomRelevance :: (Relevance -> Relevance) -> Dom a -> Dom a
- data Arg e = Arg {
- argHiding :: Hiding
- argRelevance :: Relevance
- unArg :: e
- mapArgHiding :: (Hiding -> Hiding) -> Arg a -> Arg a
- mapArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a
- makeInstance :: Arg a -> Arg a
- hide :: Arg a -> Arg a
- defaultArg :: a -> Arg a
- isHiddenArg :: Arg a -> Bool
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg a = Arg (Named String a)
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- data IsInfix
- data Access
- data IsAbstract
- type Nat = Int
- type Arity = Nat
- data NameId = NameId Integer Integer
- newtype Constr a = Constr a
Documentation
Used to specify whether something should be delayed.
Constructors
| Delayed | |
| NotDelayed |
Constructors
| Inductive | |
| CoInductive |
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 |
moreRelevant :: Relevance -> Relevance -> BoolSource
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
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 aSource
domFromArg :: Arg a -> Dom aSource
Argument decoration
A function argument can be hidden and/or irrelevant.
Instances
makeInstance :: Arg a -> Arg aSource
defaultArg :: a -> Arg aSource
isHiddenArg :: Arg a -> BoolSource
withArgsFrom :: [a] -> [Arg b] -> [Arg a]Source
Named arguments
Constructors
| Named | |
Fields
| |
Instances
| Typeable2 Named | |
| Functor (Named name) | |
| Foldable (Named name) | |
| Traversable (Named name) | |
| (Eq name, Eq a) => Eq (Named name a) | |
| (Ord name, Ord a) => Ord (Named name a) | |
| Show a => Show (Named String a) | |
| Sized a => Sized (Named name a) | |
| Pretty e => Pretty (Named String e) | |
| KillRange a => KillRange (Named name a) | |
| HasRange a => HasRange (Named name a) | |
| (Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) | |
| (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) | |
| LowerMeta a => LowerMeta (Named name a) | |
| ToConcrete a c => ToConcrete (Named name a) (Named name c) | |
| ToAbstract c a => ToAbstract (Named name c) (Named name a) | |
| Reify i a => Reify (Named n i) (Named n a) | |
| ReifyWhen i a => ReifyWhen (Named n i) (Named n a) |
defaultNamedArg :: a -> NamedArg aSource
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg bSource
The functor instance for NamedArg would be ambiguous,
so we give it another name here.
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.