Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Notation

Contents

- Sections
- Pretty printing

Description

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 {
    - _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 :: Set1 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 #
NFData NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationKind -> () Source #
Generic NotationKind Source # |

Instance details

Defined in Agda.Syntax.Notation

Associated Types

type Rep NotationKind |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: NotationKind -> Rep NotationKind x Source #

to :: Rep NotationKind x -> NotationKind Source #

Show NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS Source # show :: NotationKind -> String Source # showList :: [NotationKind] -> ShowS Source #
Eq NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods (==) :: NotationKind -> NotationKind -> Bool Source # (/=) :: NotationKind -> NotationKind -> Bool Source #
type Rep NotationKind Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationKind = D1 ('MetaData "NotationKind" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 :: Set1 Name

  The names the syntax and/or fixity belong to.

  Invariant: 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 #
NFData NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NewNotation -> () Source #
Generic NewNotation Source # |

Instance details

Defined in Agda.Syntax.Notation

Associated Types

type Rep NewNotation |

Instance details

Defined in Agda.Syntax.Notation

type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NewNotation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "notaName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "notaNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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)))))

Methods

from :: NewNotation -> Rep NewNotation x Source #

to :: Rep NewNotation x -> NewNotation Source #

Show NewNotation Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NewNotation -> ShowS Source # show :: NewNotation -> String Source # showList :: [NewNotation] -> ShowS Source #
type Rep NewNotation Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NewNotation = D1 ('MetaData "NewNotation" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "NewNotation" 'PrefixI 'True) ((S1 ('MetaSel ('Just "notaName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Just "notaNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set1 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`.

syntaxOf :: Name -> Notation Source #

Create a `Notation` (without binders) from a concrete `Name`. Does the obvious thing: `Hole`s become `HolePart`s, `Id`s become `IdParts`. If `Name` has no `Hole`s, it returns `noNotation`.

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.

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 #
NFData NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: NotationSection -> () Source #
Generic NotationSection Source # |

Instance details

Defined in Agda.Syntax.Notation

Associated Types

type Rep NotationSection |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: NotationSection -> Rep NotationSection x Source #

to :: Rep NotationSection x -> NotationSection Source #

Show NotationSection Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationSection -> ShowS Source # show :: NotationSection -> String Source # showList :: [NotationSection] -> ShowS Source #
type Rep NotationSection Source # |

Instance details

Defined in Agda.Syntax.Notation

type Rep NotationSection = D1 ('MetaData "NotationSection" "Agda.Syntax.Notation" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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.

# Pretty printing