Safe Haskell | None |
---|---|
Language | Haskell98 |
Some common syntactic entities are defined in this module.
- data Delayed
- data Induction
- 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
- 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]
- class Eq a => Underscore a where
- underscore :: a
- isUnderscore :: a -> Bool
- 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
- type Named_ = Named RString
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg c a = Arg c (Named_ 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 RawName = String
- rawNameToString :: RawName -> String
- stringToRawName :: String -> RawName
- type RString = Ranged RawName
- 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.
Induction
Hiding
class LensHiding a where Source
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and one of setHiding
or mapHiding
.
LensHiding Hiding | |
LensHiding (ArgInfo c) | |
LensHiding (FlexibleVar a) | |
LensHiding (Dom c e) | |
LensHiding (Arg c e) |
notHidden :: LensHiding a => a -> Bool Source
visible :: LensHiding a => a -> Bool Source
NotHidden
arguments are visible
.
notVisible :: LensHiding a => a -> Bool Source
hide :: LensHiding a => a -> a Source
makeInstance :: LensHiding a => a -> a Source
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 |
class LensRelevance a where Source
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and one of setRelevance
or mapRelevance
.
getRelevance :: a -> Relevance Source
setRelevance :: Relevance -> a -> a Source
mapRelevance :: (Relevance -> Relevance) -> a -> a Source
LensRelevance Relevance | |
LensRelevance (ArgInfo c) | |
LensRelevance (Dom c e) | |
LensRelevance (Arg c e) |
isRelevant :: LensRelevance a => a -> Bool Source
isIrrelevant :: LensRelevance a => a -> Bool Source
moreRelevant :: Relevance -> Relevance -> Bool Source
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
Argument decoration
A function argument can be hidden and/or irrelevant.
ArgInfo | |
|
Functor 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 | |
Typeable (* -> *) ArgInfo |
mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c' Source
defaultArgInfo :: ArgInfo c Source
Arguments
mapArgColors :: ([c] -> [c']) -> Arg c a -> Arg c' a Source
setArgColors :: [c] -> Arg c' a -> Arg c a Source
defaultArg :: a -> Arg c a Source
defaultColoredArg :: ([c], a) -> Arg c a Source
noColorArg :: Hiding -> Relevance -> a -> Arg c a Source
withArgsFrom :: [a] -> [Arg c b] -> [Arg c a] Source
withNamedArgsFrom :: [a] -> [NamedArg c b] -> [NamedArg c a] Source
Names
class Eq a => Underscore a where Source
underscore :: a Source
isUnderscore :: a -> Bool 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.
argFromDom :: Dom c a -> Arg c a Source
domFromArg :: Arg c a -> Dom c a Source
defaultDom :: a -> Dom c a Source
Named arguments
Something potentially carrying a name.
Named | |
|
defaultNamedArg :: a -> NamedArg c a Source
updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c b Source
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
Range decoration.
Thing with range info.
Ranged | |
|
Functor 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) | |
Show a => Show (Named_ a) | |
Pretty e => Pretty (Named_ e) | |
KillRange (Ranged a) | |
HasRange (Ranged a) | |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) | |
EmbPrj a => EmbPrj (Ranged a) | |
ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a) | |
Typeable (* -> *) Ranged |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String Source
stringToRawName :: String -> RawName Source
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.
Interaction meta variables
newtype InteractionId Source