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
data Induction
Constructors
Inductive | |
CoInductive |
data Hiding
Relevance
data 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 -> Bool
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
Function type domain
data Dom e
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
mapDomHiding :: (Hiding -> Hiding) -> Dom a -> Dom a
mapDomRelevance :: (Relevance -> Relevance) -> Dom a -> Dom a
Argument decoration
data Arg e
A function argument can be hidden and/or irrelevant.
Instances
mapArgHiding :: (Hiding -> Hiding) -> Arg a -> Arg a
mapArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a
makeInstance :: Arg a -> Arg a
defaultArg :: a -> Arg a
isHiddenArg :: Arg a -> Bool
withArgsFrom :: [a] -> [Arg b] -> [Arg a]
Named arguments
data Named name a
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) | |
(Eq n, Alpha a) => Alpha (Named n a) | |
Rename a => Rename (Named n a) | |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) | |
DotVars a => DotVars (Named s 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 a
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
Infixity, access, abstract, etc.
data Access
Access modifier.
Constructors
PrivateAccess | |
PublicAccess | |
OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
data NameId
The unique identifier of a name. Second argument is the top-level module identifier.