Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Common
Contents
- Delayed
- Induction
- Hiding
- Relevance
- Origin of arguments (user-written, inserted or reflected)
- Argument decoration
- Arguments
- Names
- Function type domain
- Named arguments
- Range decoration.
- Raw names (before parsing into name parts).
- Further constructor and projection info
- Infixity, access, abstract, etc.
- NameId
- Meta variables
- Placeholders (used to parse sections)
- Interaction meta variables
- Import directive
- Termination
- Positivity
Description
Some common syntactic entities are defined in this module.
- data Delayed
- data Induction
- data Overlappable
- data Hiding
- data WithHiding a = WithHiding {}
- class LensHiding a where
- mergeHiding :: LensHiding a => WithHiding a -> a
- visible :: LensHiding a => a -> Bool
- notVisible :: LensHiding a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideOrKeepInstance :: LensHiding a => a -> a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- isOverlappable :: LensHiding a => a -> Bool
- isInstance :: LensHiding a => a -> Bool
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- data Big
- data Relevance
- = Relevant
- | NonStrict
- | Irrelevant
- | Forced Big
- allRelevances :: [Relevance]
- class LensRelevance a where
- isRelevant :: LensRelevance a => a -> Bool
- isIrrelevant :: LensRelevance a => a -> Bool
- moreRelevant :: Relevance -> Relevance -> Bool
- irrelevant :: Relevance -> Bool
- unusableRelevance :: LensRelevance a => a -> Bool
- composeRelevance :: Relevance -> Relevance -> Relevance
- inverseComposeRelevance :: Relevance -> Relevance -> Relevance
- ignoreForced :: Relevance -> Relevance
- irrToNonStrict :: Relevance -> Relevance
- nonStrictToRel :: Relevance -> Relevance
- nonStrictToIrr :: Relevance -> Relevance
- data Origin
- data WithOrigin a = WithOrigin {}
- class LensOrigin a where
- data ArgInfo = ArgInfo {}
- class LensArgInfo a where
- defaultArgInfo :: ArgInfo
- data Arg e = Arg {}
- defaultArg :: a -> Arg a
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- class Eq a => Underscore a where
- data Dom e = Dom {}
- argFromDom :: Dom a -> Arg a
- domFromArg :: Arg a -> Dom a
- defaultDom :: a -> Dom 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 a = Arg (Named_ a)
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- setNamedArg :: NamedArg a -> b -> NamedArg 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 ConOrigin
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- data ProjOrigin
- data DataOrRecord
- data IsInfix
- data Access
- data IsAbstract
- data IsInstance
- data IsMacro
- type Nat = Int
- type Arity = Nat
- data NameId = NameId !Word64 !Word64
- newtype MetaId = MetaId {}
- newtype Constr a = Constr a
- data PositionInName
- data MaybePlaceholder e
- noPlaceholder :: e -> MaybePlaceholder e
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data ImportDirective' a b = ImportDirective {
- importDirRange :: Range
- using :: Using' a b
- hiding :: [ImportedName' a b]
- impRenaming :: [Renaming' a b]
- publicOpen :: Bool
- data Using' a b
- = UseEverything
- | Using [ImportedName' a b]
- defaultImportDir :: ImportDirective' a b
- isDefaultImportDir :: ImportDirective' a b -> Bool
- data ImportedName' a b
- = ImportedModule b
- | ImportedName a
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- data Renaming' a b = Renaming {
- renFrom :: ImportedName' a b
- renTo :: ImportedName' a b
- renToRange :: Range
- data TerminationCheck m
- type PositivityCheck = Bool
Delayed
Used to specify whether something should be delayed.
Constructors
Delayed | |
NotDelayed |
Induction
Constructors
Inductive | |
CoInductive |
Hiding
data Overlappable Source #
Constructors
YesOverlap | |
NoOverlap |
Instances
Eq Overlappable Source # | |
Data Overlappable Source # | |
Ord Overlappable Source # | |
Show Overlappable Source # | |
Semigroup Overlappable Source # | Just for the |
Monoid Overlappable Source # | |
NFData Overlappable Source # | |
Constructors
Hidden | |
Instance Overlappable | |
NotHidden |
Instances
Eq Hiding Source # | |
Data Hiding Source # | |
Ord Hiding Source # | |
Show Hiding Source # | |
Semigroup Hiding Source # |
|
Monoid Hiding Source # | |
NFData Hiding Source # | |
KillRange Hiding Source # | |
LensHiding Hiding Source # | |
ChooseFlex Hiding Source # | |
Unquote Hiding Source # | |
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
data WithHiding a Source #
Decorating something with Hiding
information.
Constructors
WithHiding | |
Instances
Functor WithHiding Source # | |
Applicative WithHiding Source # | |
Foldable WithHiding Source # | |
Traversable WithHiding Source # | |
Decoration WithHiding Source # | |
Eq a => Eq (WithHiding a) Source # | |
Data a => Data (WithHiding a) Source # | |
Ord a => Ord (WithHiding a) Source # | |
Show a => Show (WithHiding a) Source # | |
NFData a => NFData (WithHiding a) Source # | |
KillRange a => KillRange (WithHiding a) Source # | |
SetRange a => SetRange (WithHiding a) Source # | |
HasRange a => HasRange (WithHiding a) Source # | |
LensHiding (WithHiding a) Source # | |
PrettyTCM a => PrettyTCM (WithHiding a) Source # | |
ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) Source # | |
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) Source # | |
AddContext ([WithHiding Name], Dom Type) Source # | |
class LensHiding a where Source #
A lens to access the Hiding
attribute in data structures.
Minimal implementation: getHiding
and one of setHiding
or mapHiding
.
Minimal complete definition
Instances
mergeHiding :: LensHiding a => WithHiding a -> a Source #
Monoidal composition of Hiding
information in some data.
notVisible :: LensHiding a => a -> Bool Source #
LensHiding a => a -> Bool Source #
::Hidden
arguments are hidden
.
hide :: LensHiding a => a -> a Source #
hideOrKeepInstance :: LensHiding a => a -> a Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
isOverlappable :: LensHiding a => a -> Bool Source #
isInstance :: LensHiding a => a -> Bool Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable
.
Relevance
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
.
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. |
allRelevances :: [Relevance] Source #
class LensRelevance a where Source #
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 Source #
setRelevance :: Relevance -> a -> a Source #
mapRelevance :: (Relevance -> Relevance) -> a -> a Source #
Instances
isRelevant :: LensRelevance a => a -> Bool Source #
isIrrelevant :: LensRelevance a => a -> Bool Source #
moreRelevant :: Relevance -> Relevance -> Bool Source #
Information ordering.
Relevant `moreRelevant`
Forced `moreRelevant`
NonStrict `moreRelevant`
Irrelevant
irrelevant :: Relevance -> Bool Source #
unusableRelevance :: LensRelevance a => a -> Bool Source #
unusableRelevance rel == True
iff we cannot use a variable of rel
.
composeRelevance :: Relevance -> Relevance -> Relevance Source #
Relevance
composition.
Irrelevant
is dominant, Relevant
is neutral.
inverseComposeRelevance :: Relevance -> Relevance -> Relevance Source #
inverseComposeRelevance r x
returns the most irrelevant y
such that forall x
, y
we have
x `moreRelevant` (r `composeRelevance` y)
iff
(r `inverseComposeRelevance` x) `moreRelevant` y
(Galois connection).
ignoreForced :: Relevance -> Relevance Source #
For comparing Relevance
ignoring Forced
.
irrToNonStrict :: Relevance -> Relevance Source #
Irrelevant function arguments may appear non-strictly in the codomain type.
nonStrictToRel :: Relevance -> Relevance Source #
Applied when working on types (unless --experimental-irrelevance).
nonStrictToIrr :: Relevance -> Relevance Source #
Origin of arguments (user-written, inserted or reflected)
Origin of arguments.
Constructors
UserWritten | From the source file / user input. (Preserve!) |
Inserted | E.g. inserted hidden arguments. |
Reflected | Produced by the reflection machinery. |
CaseSplit | Produced by an interactive case split. |
data WithOrigin a Source #
Decorating something with Origin
information.
Constructors
WithOrigin | |
Instances
Functor WithOrigin Source # | |
Foldable WithOrigin Source # | |
Traversable WithOrigin Source # | |
Decoration WithOrigin Source # | |
Eq a => Eq (WithOrigin a) Source # | |
Data a => Data (WithOrigin a) Source # | |
Ord a => Ord (WithOrigin a) Source # | |
Show a => Show (WithOrigin a) Source # | |
NFData a => NFData (WithOrigin a) Source # | |
KillRange a => KillRange (WithOrigin a) Source # | |
SetRange a => SetRange (WithOrigin a) Source # | |
HasRange a => HasRange (WithOrigin a) Source # | |
LensOrigin (WithOrigin a) Source # | |
class LensOrigin a where Source #
A lens to access the Origin
attribute in data structures.
Minimal implementation: getOrigin
and one of setOrigin
or mapOrigin
.
Minimal complete definition
Instances
LensOrigin ArgInfo Source # | |
LensOrigin Origin Source # | |
LensOrigin LamInfo Source # | |
LensOrigin (Dom e) Source # | |
LensOrigin (Arg e) Source # | |
LensOrigin (WithOrigin a) Source # | |
LensOrigin (Elim' a) Source # | This instance cheats on |
LensOrigin (FlexibleVar a) Source # | |
Argument decoration
A function argument can be hidden and/or irrelevant.
Constructors
ArgInfo | |
Fields |
Instances
class LensArgInfo a where Source #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo Source #
setArgInfo :: ArgInfo -> a -> a Source #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #
Instances
LensArgInfo ArgInfo Source # | |
LensArgInfo (Dom e) Source # | |
LensArgInfo (Arg a) Source # | |
Arguments
Instances
defaultArg :: a -> Arg a Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
Names
class Eq a => Underscore a where Source #
Minimal complete definition
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 a Source #
domFromArg :: Arg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
Named arguments
Something potentially carrying a name.
Constructors
Named | |
Fields
|
Instances
defaultNamedArg :: a -> NamedArg a Source #
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source #
The functor instance for NamedArg
would be ambiguous,
so we give it another name here.
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
Range decoration.
Thing with range info.
Constructors
Ranged | |
Fields
|
Instances
Functor Ranged Source # | |
Foldable Ranged Source # | |
Traversable Ranged Source # | |
Decoration Ranged Source # | |
MapNamedArgPattern NAP Source # | |
UniverseBi Declaration RString # | |
PatternVars a (NamedArg (Pattern' a)) Source # | |
Eq a => Eq (Ranged a) Source # | |
Data a => Data (Ranged a) Source # | |
Ord a => Ord (Ranged a) Source # | |
Show a => Show (Ranged a) Source # | |
Show a => Show (Named_ a) Source # | |
NFData a => NFData (Ranged a) Source # | Ranges are not forced. |
KillRange (Ranged a) Source # | |
HasRange (Ranged a) Source # | |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a) Source # | |
NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |
ToAbstract [Arg Term] [NamedArg Expr] Source # | |
ToAbstract r a => ToAbstract (Arg r) (NamedArg a) Source # | |
Raw names (before parsing into name parts).
rawNameToString :: RawName -> String Source #
stringToRawName :: String -> RawName Source #
Further constructor and projection info
Where does the ConP
or Con
come from?
Constructors
ConOSystem | Inserted by system or expanded from an implicit pattern. |
ConOCon | User wrote a constructor (pattern). |
ConORec | User wrote a record (pattern). |
ConOSplit | Generated by interactive case splitting. |
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
data ProjOrigin Source #
Where does a projection come from?
Constructors
ProjPrefix | User wrote a prefix projection. |
ProjPostfix | User wrote a postfix projection. |
ProjSystem | Projection was generated by the system. |
data DataOrRecord Source #
Instances
Infixity, access, abstract, etc.
Functions can be defined in both infix and prefix style. See
LHS
.
Access modifier.
Constructors
PrivateAccess Origin | Store the |
PublicAccess | |
OnlyQualified | Visible from outside, but not exported when opening the module Used for qualified constructors. |
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
InstanceDef | |
NotInstanceDef |
Is this a macro definition?
Constructors
MacroDef | |
NotMacroDef |
NameId
The unique identifier of a name. Second argument is the top-level module identifier.
Meta variables
A meta variable identifier is just a natural number.
Instances
Enum MetaId Source # | |
Eq MetaId Source # | |
Integral MetaId Source # | |
Data MetaId Source # | |
Num MetaId Source # | |
Ord MetaId Source # | |
Real MetaId Source # | |
Show MetaId Source # | Show non-record version of this newtype. |
NFData MetaId Source # | |
Pretty MetaId Source # | |
GetDefs MetaId Source # | |
HasFresh MetaId Source # | |
PrettyTCM MetaId Source # | |
UnFreezeMeta MetaId Source # | |
IsInstantiatedMeta MetaId Source # | |
FromTerm MetaId Source # | |
ToTerm MetaId Source # | |
PrimTerm MetaId Source # | |
Unquote MetaId Source # | |
Reify MetaId Expr Source # | |
Constructors
Constr a |
Instances
Placeholders (used to parse sections)
data PositionInName Source #
The position of a name part or underscore in a name.
Constructors
Beginning | The following underscore is at the beginning of the name:
|
Middle | The following underscore is in the middle of the name:
|
End | The following underscore is at the end of the name: |
Instances
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Constructors
Placeholder !PositionInName | |
NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
Functor MaybePlaceholder Source # | |
Foldable MaybePlaceholder Source # | |
Traversable MaybePlaceholder Source # | |
Eq e => Eq (MaybePlaceholder e) Source # | |
Data e => Data (MaybePlaceholder e) Source # | |
Ord e => Ord (MaybePlaceholder e) Source # | |
Show e => Show (MaybePlaceholder e) Source # | |
NFData a => NFData (MaybePlaceholder a) Source # | |
KillRange a => KillRange (MaybePlaceholder a) Source # | |
HasRange a => HasRange (MaybePlaceholder a) Source # | |
ExprLike a => ExprLike (MaybePlaceholder a) Source # | |
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder =
.NoPlaceholder
Nothing
Interaction meta variables
newtype InteractionId Source #
Constructors
InteractionId | |
Fields
|
Instances
Import directive
data ImportDirective' a b Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import
, namespace
, or open
declarations).
Constructors
ImportDirective | |
Fields
|
Instances
(Eq b, Eq a) => Eq (ImportDirective' a b) Source # | |
(Data b, Data a) => Data (ImportDirective' a b) Source # | |
(NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced. |
(KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
(HasRange a, HasRange b) => HasRange (ImportDirective' a b) Source # | |
Constructors
UseEverything | |
Using [ImportedName' a b] |
Instances
(Eq b, Eq a) => Eq (Using' a b) Source # | |
(Data b, Data a) => Data (Using' a b) Source # | |
Semigroup (Using' a b) Source # | |
Monoid (Using' a b) Source # | |
(NFData a, NFData b) => NFData (Using' a b) Source # | |
(KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
(HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
defaultImportDir :: ImportDirective' a b Source #
Default is directive is private
(use everything, but do not export).
isDefaultImportDir :: ImportDirective' a b -> Bool Source #
data ImportedName' a b Source #
An imported name can be a module or a defined name
Constructors
ImportedModule b | |
ImportedName a |
Instances
(Eq a, Eq b) => Eq (ImportedName' a b) Source # | |
(Data b, Data a) => Data (ImportedName' a b) Source # | |
(Ord a, Ord b) => Ord (ImportedName' a b) Source # | |
(Show a, Show b) => Show (ImportedName' a b) Source # | |
(NFData a, NFData b) => NFData (ImportedName' a b) Source # | |
(KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
(HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
Constructors
Renaming | |
Fields
|
Instances
HasRange instances
KillRange instances
NFData instances
Termination
data TerminationCheck m Source #
Termination check? (Default = TerminationCheck).
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 Source # | |
Eq m => Eq (TerminationCheck m) Source # | |
Data m => Data (TerminationCheck m) Source # | |
Show m => Show (TerminationCheck m) Source # | |
NFData a => NFData (TerminationCheck a) Source # | |
KillRange m => KillRange (TerminationCheck m) Source # | |
Positivity
type PositivityCheck = Bool Source #
Positivity check? (Default = True).