Safe Haskell | None |
---|
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.
Relevance
A function argument can be relevant or irrelevant.
See Irrelevance
.
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.
argFromDom :: Dom a -> Arg aSource
domFromArg :: Arg a -> Dom aSource
Argument decoration
A function argument can be hidden and/or irrelevant.
makeInstance :: Arg a -> Arg aSource
defaultArg :: a -> Arg aSource
isHiddenArg :: Arg a -> BoolSource
withArgsFrom :: [a] -> [Arg b] -> [Arg a]Source
Named arguments
Named | |
|
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.
PrivateAccess | |
PublicAccess | |
OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
data IsAbstract Source
Abstract or concrete
The unique identifier of a name. Second argument is the top-level module identifier.