Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
- data Delayed
- data Induction
- data Hiding
- data WithHiding a = WithHiding Hiding a
- class LensHiding a where
- mergeHiding :: LensHiding a => WithHiding a -> a
- 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 Big
- data Relevance
- allRelevances :: [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 a -> [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 a -> [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
- data IsInstance
- type Nat = Int
- type Arity = Nat
- data NameId = NameId Integer Integer
- newtype Constr a = Constr a
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data TerminationCheck m
Delayed
Induction
data Induction
Constructors
Inductive | |
CoInductive |
Hiding
data Hiding
data WithHiding a
Decorating something with Hiding
information.
Constructors
WithHiding Hiding a |
Instances
Functor WithHiding | |
Applicative WithHiding | |
Foldable WithHiding | |
Traversable WithHiding | |
Decoration WithHiding | |
Eq a => Eq (WithHiding a) | |
Ord a => Ord (WithHiding a) | |
Show a => Show (WithHiding a) | |
KillRange a => KillRange (WithHiding a) | |
SetRange a => SetRange (WithHiding a) | |
HasRange a => HasRange (WithHiding a) | |
LensHiding (WithHiding a) | |
PrettyTCM a => PrettyTCM (WithHiding a) | |
EmbPrj a => EmbPrj (WithHiding a) | |
ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) | |
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) | |
AddContext ([WithHiding Name], Dom Type) |
class LensHiding a where
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and one of setHiding
or mapHiding
.
Minimal complete definition
Methods
Instances
mergeHiding :: LensHiding a => WithHiding a -> a
Monoidal composition of Hiding
information in some data.
isHidden :: LensHiding a => a -> Bool
notHidden :: LensHiding a => a -> Bool
visible :: LensHiding a => a -> Bool
NotHidden
arguments are visible
.
notVisible :: LensHiding a => a -> Bool
hide :: LensHiding a => a -> a
makeInstance :: LensHiding a => a -> a
Relevance
data Big
An constructor argument is big if the sort of its type is bigger than
the sort of the data type. Only parameters (and maybe forced arguments)
are allowed to be big.
List : Set -> Set
nil : (A : Set) -> List A
A
is big in constructor nil
as the sort Set1
of its type Set
is bigger than the sort Set
of the data type List
.
data Relevance
A function argument can be relevant or irrelevant. See Agda.TypeChecking.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 Big | The argument can be skipped during equality checking because its value is already determined by the type. If a constructor argument is big, it has to be regarded absent, otherwise we get into paradoxes. |
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 |
allRelevances :: [Relevance]
class LensRelevance a where
A lens to access the Relevance
attribute in data structures.
Minimal implementation: getRelevance
and one of setRelevance
or mapRelevance
.
Minimal complete definition
Methods
getRelevance :: a -> Relevance
setRelevance :: Relevance -> a -> a
mapRelevance :: (Relevance -> Relevance) -> a -> a
Instances
LensRelevance Relevance | |
LensRelevance TypedBindings | |
LensRelevance (ArgInfo c) | |
LensRelevance (Dom c e) | |
LensRelevance (Arg c e) |
isRelevant :: LensRelevance a => a -> Bool
isIrrelevant :: LensRelevance a => a -> Bool
moreRelevant :: Relevance -> Relevance -> Bool
Information ordering.
Relevant `moreRelevant`
UnusedArg `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
Argument decoration
data ArgInfo c
A function argument can be hidden and/or irrelevant.
Constructors
ArgInfo | |
Fields
|
Instances
Functor ArgInfo | |
Foldable ArgInfo | |
Traversable ArgInfo | |
ToTerm 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 |
mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c'
defaultArgInfo :: ArgInfo c
Arguments
data Arg c e
Instances
mapArgInfo :: (ArgInfo c -> ArgInfo c') -> Arg c a -> Arg c' a
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]
Names
class Eq a => Underscore a where
Minimal complete definition
Function type domain
data Dom c 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
mapDomInfo :: (ArgInfo c -> ArgInfo c') -> Dom c a -> Dom c' a
argFromDom :: Dom c a -> Arg c a
domFromArg :: Arg c a -> Dom c a
defaultDom :: a -> Dom c a
Named arguments
data Named name a
Something potentially carrying a name.
Constructors
Named | |
Fields
|
Instances
defaultNamedArg :: a -> NamedArg c a
updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c b
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
Range decoration.
data Ranged a
Thing with range info.
Constructors
Ranged | |
Fields
|
Instances
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) | |
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) |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String
stringToRawName :: String -> RawName
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 IsInstance
Is this definition eligible for instance search?
Constructors
InstanceDef | |
NotInstanceDef |
Instances
data NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Interaction meta variables
newtype InteractionId
Constructors
InteractionId | |
Fields
|
Termination
data TerminationCheck m
Termination check? (Default = True).
Constructors
TerminationCheck | Run the termination checker. |
NoTerminationCheck | Skip termination checking (unsafe). |
NonTerminating | Treat as non-terminating. |
Terminating | Treat as terminating (unsafe). Same effect as |
TerminationMeasure !Range m | Skip termination checking but use measure instead. |
Instances
Functor TerminationCheck | |
Eq m => Eq (TerminationCheck m) | |
Show m => Show (TerminationCheck m) | |
KillRange m => KillRange (TerminationCheck m) |