Safe Haskell	None
Language	Haskell98

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 GenPart before it leaves the Happy code.

Constructors

LambdaHole	`x -> y`; 1st argument is the bound name (unused for now).
Fields _bindHoleName :: RawName holeName :: RawName
ExprHole	Simple named hole with hiding.
Fields holeName :: RawName

isLambdaHole :: HoleName -> Bool Source

Is the hole a binder?

type Notation = [GenPart] Source

Notation as provided by the syntax declaration.

data GenPart Source

Part of a Notation

Constructors

BindHole Int	Argument is the position of the hole (with binding) where the binding should occur.
NormalHole (NamedArg () Int)	Argument is where the expression should go.
IdPart RawName

Instances

Eq GenPart Source
Ord GenPart Source
Show GenPart Source
KillRange GenPart Source
EmbPrj GenPart Source

stringParts :: Notation -> [RawName] Source

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe Int Source

Target argument position of a part (Nothing if it is not a hole).

isAHole :: GenPart -> Bool Source

Is the part a hole?

isBindingHole :: GenPart -> 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

Eq NotationKind Source
Show NotationKind Source

notationKind :: Notation -> NotationKind Source

Classify a notation by presence of leading and/or trailing hole.

mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation Source

From notation with names to notation with indices.

Example: ids = ["for", "x", "∈", "xs", "return", "e"] holes = [ LambdaHole "x" "e", ExprHole "xs" ] creates the notation [ IdPart "for" , BindHole 0 , IdPart "∈" , NormalHole 1 , IdPart "return" , NormalHole 0 ]

defaultNotation :: Notation Source

No notation by default.

noNotation :: Notation Source

No notation by default.