Agda-2.4.2.5: 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 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).

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 

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 

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.