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.