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 #

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 #

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.
WildHole !Int	An underscore in binding position.
IdPart RawName

Instances

Eq GenPart #
Instance details Defined in Agda.Syntax.Notation Methods (==) :: GenPart -> GenPart -> Bool # (/=) :: GenPart -> GenPart -> Bool #
Data GenPart #
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 #
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 #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> GenPart -> ShowS # show :: GenPart -> String # showList :: [GenPart] -> ShowS #
NFData GenPart #
Instance details Defined in Agda.Syntax.Notation Methods rnf :: GenPart -> () #
Pretty GenPart #
Instance details Defined in Agda.Syntax.Concrete.Pretty Methods pretty :: GenPart -> Doc # prettyPrec :: Int -> GenPart -> Doc # prettyList :: [GenPart] -> Doc #
KillRange GenPart #
Instance details Defined in Agda.Syntax.Notation Methods killRange :: KillRangeT GenPart #
EmbPrj GenPart #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: GenPart -> S Int32 # icod_ :: GenPart -> S Int32 # value :: Int32 -> R GenPart #

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? WildHoles don't count since they don't correspond to anything the user writes.

isNormalHole :: GenPart -> Bool #

Is the part a normal 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

Instances

Eq NotationKind #
Instance details Defined in Agda.Syntax.Notation Methods (==) :: NotationKind -> NotationKind -> Bool # (/=) :: NotationKind -> NotationKind -> Bool #
Show NotationKind #
Instance details Defined in Agda.Syntax.Notation Methods showsPrec :: Int -> NotationKind -> ShowS # show :: NotationKind -> String # showList :: [NotationKind] -> ShowS #

notationKind :: Notation -> NotationKind #

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

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

noNotation :: Notation #