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 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

Instance details

Defined in Agda.Syntax.Notation

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

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.1-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

Instance details

Defined in Agda.Syntax.Notation

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

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.1-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.