Safe Haskell	None
Language	Haskell2010

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

data HoleName
- = LambdaHole {
  - _bindHoleName :: RawName
  - holeName :: RawName
  }
- | ExprHole {
  - holeName :: RawName
  }
isLambdaHole :: HoleName -> Bool
type Notation = [GenPart]
data GenPart
- = BindHole !Int
- | NormalHole (NamedArg Int)
- | WildHole !Int
- | IdPart RawName
stringParts :: Notation -> [RawName]
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] -> [RawName] -> 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 :: 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.
WildHole !Int	An underscore in binding position.
IdPart RawName

Instances

Eq GenPart Source #
Instance details Defined in Agda.Syntax.Notation Methods (==) :: GenPart -> GenPart -> Bool # (/=) :: GenPart -> GenPart -> Bool #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenPart # toConstr :: GenPart -> Constr # dataTypeOf :: GenPart -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenPart) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenPart) # gmapT :: (forall b. Data b => b -> b) -> GenPart -> GenPart # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenPart -> r # gmapQ :: (forall d. Data d => d -> u) -> GenPart -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GenPart -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenPart -> m GenPart #
Ord GenPart Source #
Instance details Defined in Agda.Syntax.Notation Methods compare :: GenPart -> GenPart -> Ordering # (<) :: GenPart -> GenPart -> Bool # (<=) :: GenPart -> GenPart -> Bool # (>) :: GenPart -> GenPart -> Bool # (>=) :: GenPart -> GenPart -> Bool # max :: GenPart -> GenPart -> GenPart # min :: GenPart -> GenPart -> GenPart #
Show GenPart Source #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> GenPart -> ShowS # show :: GenPart -> String # showList :: [GenPart] -> ShowS #
NFData GenPart Source #
Instance details Defined in Agda.Syntax.Notation Methods rnf :: GenPart -> () #
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 #
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 -> [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? 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 # (/=) :: NotationKind -> NotationKind -> Bool #
Show NotationKind Source #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS # show :: NotationKind -> String # showList :: [NotationKind] -> ShowS #

notationKind :: Notation -> NotationKind Source #

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

mkNotation :: [NamedArg 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 ]

noNotation :: Notation Source #