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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Notation

Description

As a concrete name, a notation is a non-empty list of alternating `IdPart`s 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 {
    - _bindHoleName :: RString
    - holeName :: RString
    }
  - | ExprHole {
    - holeName :: RString
    }
- isLambdaHole :: HoleName -> Bool
- type Notation = [GenPart]
- data GenPart
  - = BindHole Range (Ranged Int)
  - | NormalHole Range (NamedArg (Ranged Int))
  - | WildHole (Ranged Int)
  - | IdPart RString
- stringParts :: Notation -> [String]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isNormalHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- data NotationKind
  - = InfixNotation
  - | PrefixNotation
  - | PostfixNotation
  - | NonfixNotation
  - | NoNotation
- notationKind :: Notation -> NotationKind
- mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
- noNotation :: Notation

# 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 :: RString
- holeName :: RString

ExprHole | Simple named hole with hiding.

Fields

- holeName :: RString

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 Range (Ranged Int) | Argument is the position of the hole (with binding) where the binding should occur. First range is the rhs range and second is the binder.
NormalHole Range (NamedArg (Ranged Int)) | Argument is where the expression should go.
WildHole (Ranged Int) | An underscore in binding position.
IdPart RString |

Instances

Eq GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods (==) :: GenPart -> GenPart -> Bool Source # (/=) :: GenPart -> GenPart -> Bool Source #
Data GenPart Source # |

Instance details

Defined in Agda.Syntax.Notation

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenPart -> c GenPart Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart Source #

toConstr :: GenPart -> Constr Source #

dataTypeOf :: GenPart -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart) Source #

gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart Source #

Ord GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods compare :: GenPart -> GenPart -> Ordering Source # (<) :: GenPart -> GenPart -> Bool Source # (<=) :: GenPart -> GenPart -> Bool Source # (>) :: GenPart -> GenPart -> Bool Source # (>=) :: GenPart -> GenPart -> Bool Source # max :: GenPart -> GenPart -> GenPart Source # min :: GenPart -> GenPart -> GenPart Source #
Show GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> GenPart -> ShowS Source # show :: GenPart -> String Source # showList :: [GenPart] -> ShowS Source #
NFData GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods rnf :: GenPart -> () Source #
Pretty GenPart Source # |
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: GenPart -> Doc Source # prettyPrec :: Int -> GenPart -> Doc Source # prettyList :: [GenPart] -> Doc Source #
KillRange GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods killRange :: KillRangeT GenPart Source #
SetRange GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods setRange :: Range -> GenPart -> GenPart Source #
HasRange GenPart Source # |
Instance details Defined in Agda.Syntax.Notation Methods getRange :: GenPart -> Range Source #
EmbPrj GenPart Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: GenPart -> S Int32 Source # icod_ :: GenPart -> S Int32 Source # value :: Int32 -> R GenPart Source #

stringParts :: Notation -> [String] 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? WildHoles don't count since they don't correspond to anything the user writes.

isNormalHole :: GenPart -> Bool Source #

Is the part a normal 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 # |
Instance details Defined in Agda.Syntax.Notation Methods (==) :: NotationKind -> NotationKind -> Bool Source # (/=) :: NotationKind -> NotationKind -> Bool Source #
Show NotationKind Source # |
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS Source # show :: NotationKind -> String Source # showList :: [NotationKind] -> ShowS Source #

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.

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

noNotation :: Notation Source #