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

Safe HaskellNone
LanguageHaskell98

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

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

ExprHole

Simple named hole with hiding.

Fields

holeName :: RawName
 

isLambdaHole :: HoleName -> Bool

Is the hole a binder?

type Notation = [GenPart]

Notation as provided by the syntax declaration.

data GenPart

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 

stringParts :: Notation -> [RawName]

Get a flat list of identifier parts of a notation.

holeTarget :: GenPart -> Maybe Int

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

isAHole :: GenPart -> Bool

Is the part a hole?

isBindingHole :: GenPart -> Bool

Is the part a binder?

data NotationKind

Classification of notations.

Constructors

InfixNotation

Ex: _bla_blub_.

PrefixNotation

Ex: _bla_blub.

PostfixNotation

Ex: bla_blub_.

NonfixNotation

Ex: bla_blub.

NoNotation 

notationKind :: Notation -> NotationKind

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

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

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

No notation by default.

noNotation :: Notation

No notation by default.