Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Notation

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

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.

ExprHole

Simple named hole with hiding.

Fields

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

NFData NotationKind Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

rnf :: NotationKind -> ()

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.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))))
Show NotationKind Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

showsPrec :: Int -> NotationKind -> ShowS

show :: NotationKind -> String

showList :: [NotationKind] -> ShowS

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

Instances

Instances details
LensFixity NewNotation Source # 
Instance details

Defined in Agda.Syntax.Notation

Pretty NewNotation Source # 
Instance details

Defined in Agda.Syntax.Notation

NFData NewNotation Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

rnf :: NewNotation -> ()

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

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

type Rep NewNotation Source # 
Instance details

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.

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

Sections

data NotationSection Source #

Sections, as well as non-sectioned operators.

Constructors

NotationSection 

Fields

Instances

Instances details
Pretty NotationSection Source # 
Instance details

Defined in Agda.Syntax.Notation

NFData NotationSection Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

rnf :: NotationSection -> ()

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.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))))
Show NotationSection Source # 
Instance details

Defined in Agda.Syntax.Notation

Methods

showsPrec :: Int -> NotationSection -> ShowS

show :: NotationSection -> String

showList :: [NotationSection] -> ShowS

type Rep NotationSection Source # 
Instance details

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.

Pretty printing