Safe Haskell | None |
---|---|
Language | Haskell2010 |
As a concrete name, a notation is a non-empty list of alternating IdPart
s and holes.
In contrast to concrete names, holes can be binders.
Example:
syntax fmap (λ x → e) xs = for x ∈ xs return e
The declared notation for fmap
is for_∈_return_
where the first hole is a binder.
Synopsis
- data HoleName
- = LambdaHole { }
- | ExprHole { }
- isLambdaHole :: HoleName -> Bool
- stringParts :: Notation -> [String]
- holeTarget :: NotationPart -> Maybe Int
- isAHole :: NotationPart -> Bool
- isBinder :: NotationPart -> Bool
- data NotationKind
- notationKind :: Notation -> NotationKind
- mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
- data NewNotation = NewNotation {
- notaName :: QName
- notaNames :: Set Name
- notaFixity :: Fixity
- notation :: Notation
- notaIsOperator :: Bool
- namesToNotation :: QName -> Name -> NewNotation
- useDefaultFixity :: NewNotation -> NewNotation
- notationNames :: NewNotation -> [QName]
- syntaxOf :: Name -> Notation
- mergeNotations :: List1 NewNotation -> List1 NewNotation
- isLambdaNotation :: NewNotation -> Bool
- _notaFixity :: Lens' NewNotation Fixity
- data NotationSection = NotationSection {
- sectNotation :: NewNotation
- sectKind :: NotationKind
- sectLevel :: Maybe FixityLevel
- sectIsSection :: Bool
- noSection :: NewNotation -> NotationSection
Documentation
Data type constructed in the Happy parser; converted to
NotationPart
before it leaves the Happy code.
LambdaHole |
|
ExprHole | Simple named hole with hiding. |
isLambdaHole :: HoleName -> Bool Source #
Is the hole a binder?
stringParts :: Notation -> [String] Source #
Get a flat list of identifier parts of a notation.
holeTarget :: NotationPart -> Maybe Int Source #
Target argument position of a part (Nothing if it is not a hole).
isAHole :: NotationPart -> Bool Source #
Is the part a hole?
isBinder :: NotationPart -> Bool Source #
Is the part a binder?
data NotationKind Source #
Classification of notations.
InfixNotation | Ex: |
PrefixNotation | Ex: |
PostfixNotation | Ex: |
NonfixNotation | Ex: |
NoNotation |
Instances
Pretty NotationKind Source # | |||||
Defined in Agda.Syntax.Notation pretty :: NotationKind -> Doc Source # prettyPrec :: Int -> NotationKind -> Doc Source # prettyList :: [NotationKind] -> Doc Source # | |||||
NFData NotationKind Source # | |||||
Defined in Agda.Syntax.Notation rnf :: NotationKind -> () | |||||
Generic NotationKind Source # | |||||
Defined in Agda.Syntax.Notation
from :: NotationKind -> Rep NotationKind x to :: Rep NotationKind x -> NotationKind | |||||
Show NotationKind Source # | |||||
Defined in Agda.Syntax.Notation showsPrec :: Int -> NotationKind -> ShowS show :: NotationKind -> String showList :: [NotationKind] -> ShowS | |||||
Eq NotationKind Source # | |||||
Defined in Agda.Syntax.Notation (==) :: NotationKind -> NotationKind -> Bool (/=) :: NotationKind -> NotationKind -> Bool | |||||
type Rep NotationKind Source # | |||||
Defined in Agda.Syntax.Notation type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "InfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrefixNotation" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PostfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonfixNotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoNotation" 'PrefixI 'False) (U1 :: Type -> Type)))) |
notationKind :: Notation -> NotationKind Source #
Classify a notation by presence of leading and/or trailing normal holes.
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation Source #
From notation with names to notation with indices.
An example (with some parts of the code omitted):
The lists
["for", "x", "∈", "xs", "return", "e"]
and
[
are mapped to the following notation:
LambdaHole
("x" :| []) "e", ExprHole
"xs"]
[
IdPart
"for" , VarPart
(BoundVariablePosition
0 0)
, IdPart
"∈" , HolePart
1
, IdPart
"return" , HolePart
0
]
data NewNotation Source #
All the notation information related to a name.
NewNotation | |
|
Instances
LensFixity NewNotation Source # | |||||
Defined in Agda.Syntax.Notation | |||||
Pretty NewNotation Source # | |||||
Defined in Agda.Syntax.Notation pretty :: NewNotation -> Doc Source # prettyPrec :: Int -> NewNotation -> Doc Source # prettyList :: [NewNotation] -> Doc Source # | |||||
NFData NewNotation Source # | |||||
Defined in Agda.Syntax.Notation rnf :: NewNotation -> () | |||||
Generic NewNotation Source # | |||||
Defined in Agda.Syntax.Notation
from :: NewNotation -> Rep NewNotation x to :: Rep NewNotation x -> NewNotation | |||||
Show NewNotation Source # | |||||
Defined in Agda.Syntax.Notation showsPrec :: Int -> NewNotation -> ShowS show :: NewNotation -> String showList :: [NewNotation] -> ShowS | |||||
type Rep NewNotation Source # | |||||
Defined in Agda.Syntax.Notation type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "NewNotation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "notaName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "notaNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name))) :*: (S1 ('MetaSel ('Just "notaFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity) :*: (S1 ('MetaSel ('Just "notation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Notation) :*: S1 ('MetaSel ('Just "notaIsOperator") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) |
namesToNotation :: QName -> Name -> NewNotation Source #
If an operator has no specific notation, then it is computed from its name.
useDefaultFixity :: NewNotation -> NewNotation Source #
Replace noFixity
by defaultFixity
.
notationNames :: NewNotation -> [QName] Source #
Return the IdPart
s of a notation, the first part qualified,
the other parts unqualified.
This allows for qualified use of operators, e.g.,
M.for x ∈ xs return e
, or x ℕ.+ y
.
mergeNotations :: List1 NewNotation -> List1 NewNotation Source #
Merges NewNotation
s that have the same precedence level and
notation, with two exceptions:
- Operators and notations coming from syntax declarations are kept separate.
- If all instances of a given
NewNotation
have the same precedence level or are "unrelated", then they are merged. They get the given precedence level, if any, and otherwise they become unrelated (but related to each other).
If NewNotation
s that are merged have distinct associativities,
then they get NonAssoc
as their associativity.
Precondition: No Name
may occur in more than one list element.
Every NewNotation
must have the same notaName
.
Postcondition: No Name
occurs in more than one list element.
isLambdaNotation :: NewNotation -> Bool Source #
Check if a notation contains any lambdas (in which case it cannot be used in a pattern).
_notaFixity :: Lens' NewNotation Fixity Source #
Lens for Fixity
in NewNotation
.
Sections
data NotationSection Source #
Sections, as well as non-sectioned operators.
NotationSection | |
|
Instances
Pretty NotationSection Source # | |||||
Defined in Agda.Syntax.Notation pretty :: NotationSection -> Doc Source # prettyPrec :: Int -> NotationSection -> Doc Source # prettyList :: [NotationSection] -> Doc Source # | |||||
NFData NotationSection Source # | |||||
Defined in Agda.Syntax.Notation rnf :: NotationSection -> () | |||||
Generic NotationSection Source # | |||||
Defined in Agda.Syntax.Notation
from :: NotationSection -> Rep NotationSection x to :: Rep NotationSection x -> NotationSection | |||||
Show NotationSection Source # | |||||
Defined in Agda.Syntax.Notation showsPrec :: Int -> NotationSection -> ShowS show :: NotationSection -> String showList :: [NotationSection] -> ShowS | |||||
type Rep NotationSection Source # | |||||
Defined in Agda.Syntax.Notation type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "NotationSection" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sectNotation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NewNotation) :*: S1 ('MetaSel ('Just "sectKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NotationKind)) :*: (S1 ('MetaSel ('Just "sectLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FixityLevel)) :*: S1 ('MetaSel ('Just "sectIsSection") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) |
noSection :: NewNotation -> NotationSection Source #
Converts a notation to a (non-)section.