Safe Haskell | None |
---|
- data HoleName
- holeName :: HoleName -> RawName
- type Notation = [GenPart]
- data GenPart
- = BindHole Int
- | NormalHole (NamedArg () Int)
- | IdPart RawName
- stringParts :: Notation -> [RawName]
- holeTarget :: GenPart -> Maybe Int
- isAHole :: GenPart -> Bool
- isBindingHole :: GenPart -> Bool
- isLambdaHole :: HoleName -> Bool
- mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation
- defaultNotation :: [a]
- noNotation :: [a]
Documentation
A name is a non-empty list of alternating Id
s and Hole
s. A normal name
is represented by a singleton list, and operators are represented by a list
with Hole
s where the arguments should go. For instance: [Hole,Id +,Hole]
is infix addition.
Equality and ordering on Name
s are defined to ignore range so same names
in different locations are equal.
Data type constructed in the Happy parser; converted to GenPart
before it leaves the Happy code.
LambdaHole RawName RawName | (x -> y) ; 1st argument is the bound name (unused for now) |
ExprHole RawName | simple named hole with hiding |
Part of a Notation
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 IntSource
Target argument position of a part (Nothing if it is not a hole)
isBindingHole :: GenPart -> BoolSource
isLambdaHole :: HoleName -> BoolSource
mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String NotationSource
From notation with names to notation with indices.
defaultNotation :: [a]Source
No notation by default
noNotation :: [a]Source