Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Notation

Contents

Sections
Pretty printing

Description

As a concrete name, a notation is a non-empty list of alternating IdParts 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 {
  - _bindHoleNames :: List1 RString
  - holeName :: RString
  }
- | ExprHole {
  - holeName :: RString
  }
isLambdaHole :: HoleName -> Bool
stringParts :: Notation -> [String]
holeTarget :: NotationPart -> Maybe Int
isAHole :: NotationPart -> Bool
isBinder :: NotationPart -> Bool
data NotationKind
- = InfixNotation
- | PrefixNotation
- | PostfixNotation
- | NonfixNotation
- | NoNotation
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 HoleName Source #

Data type constructed in the Happy parser; converted to NotationPart before it leaves the Happy code.

Constructors

LambdaHole	`λ x₁ … xₙ → y`: The first argument contains the bound names.
Fields _bindHoleNames :: List1 RString holeName :: RString
ExprHole	Simple named hole with hiding.
Fields holeName :: RString

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.

Constructors

InfixNotation	Ex: `_bla_blub_`.
PrefixNotation	Ex: `_bla_blub`.
PostfixNotation	Ex: `bla_blub_`.
NonfixNotation	Ex: `bla_blub`.
NoNotation

Instances

Instances details

Pretty NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationKind -> Doc Source # prettyPrec :: Int -> NotationKind -> Doc Source # prettyList :: [NotationKind] -> Doc Source #
Generic NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NotationKind :: Type -> Type Methods from :: NotationKind -> Rep NotationKind x to :: Rep NotationKind x -> NotationKind
Show NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS show :: NotationKind -> String showList :: [NotationKind] -> ShowS
NFData NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationKind -> ()
Eq NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Methods (==) :: NotationKind -> NotationKind -> Bool (/=) :: NotationKind -> NotationKind -> Bool
type Rep NotationKind Source #
Instance details Defined in Agda.Syntax.Notation type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.6.4-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 [LambdaHole ("x" :| []) "e", ExprHole "xs"] are mapped to the following notation: [ IdPart "for" , VarPart (BoundVariablePosition 0 0) , IdPart "∈" , HolePart 1 , IdPart "return" , HolePart 0 ]

data NewNotation Source #

All the notation information related to a name.

Constructors

NewNotation

Fields

notaName :: QName
notaNames :: Set Name
The names the syntax and/or fixity belong to.
Invariant: The set is non-empty. Every name in the list matches notaName.
notaFixity :: Fixity
Associativity and precedence (fixity) of the names.
notation :: Notation
Syntax associated with the names.
notaIsOperator :: Bool
True if the notation comes from an operator (rather than a syntax declaration).

Instances

Instances details

LensFixity NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods lensFixity :: Lens' NewNotation Fixity Source #
Pretty NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NewNotation -> Doc Source # prettyPrec :: Int -> NewNotation -> Doc Source # prettyList :: [NewNotation] -> Doc Source #
Generic NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NewNotation :: Type -> Type Methods from :: NewNotation -> Rep NewNotation x to :: Rep NewNotation x -> NewNotation
Show NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NewNotation -> ShowS show :: NewNotation -> String showList :: [NewNotation] -> ShowS
NFData NewNotation Source #
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NewNotation -> ()
type Rep NewNotation Source #
Instance details Defined in Agda.Syntax.Notation type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.6.4-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 IdParts 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.

syntaxOf :: Name -> Notation Source #

Create a Notation (without binders) from a concrete Name. Does the obvious thing: Holes become HoleParts, Ids become IdParts. If Name has no Holes, it returns noNotation.

mergeNotations :: List1 NewNotation -> List1 NewNotation Source #

Merges NewNotations 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 NewNotations 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.

Constructors

NotationSection
Fields sectNotation :: NewNotation sectKind :: NotationKind For non-sectioned operators this should match the notation's `notationKind`. sectLevel :: Maybe FixityLevel Effective precedence level. `Nothing` for closed notations. sectIsSection :: Bool `False` for non-sectioned operators.

Instances

Instances details

Pretty NotationSection Source #
Instance details Defined in Agda.Syntax.Notation Methods pretty :: NotationSection -> Doc Source # prettyPrec :: Int -> NotationSection -> Doc Source # prettyList :: [NotationSection] -> Doc Source #
Generic NotationSection Source #
Instance details Defined in Agda.Syntax.Notation Associated Types type Rep NotationSection :: Type -> Type Methods from :: NotationSection -> Rep NotationSection x to :: Rep NotationSection x -> NotationSection
Show NotationSection Source #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationSection -> ShowS show :: NotationSection -> String showList :: [NotationSection] -> ShowS
NFData NotationSection Source #
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationSection -> ()
type Rep NotationSection Source #
Instance details Defined in Agda.Syntax.Notation type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.6.4-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.

Documentation

Instances

Instances

Sections

Instances

Pretty printing