summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Notation.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Notation.hs')
-rw-r--r--src/full/Agda/Syntax/Notation.hs18
1 files changed, 13 insertions, 5 deletions
diff --git a/src/full/Agda/Syntax/Notation.hs b/src/full/Agda/Syntax/Notation.hs
index 71bc525..eee7ec5 100644
--- a/src/full/Agda/Syntax/Notation.hs
+++ b/src/full/Agda/Syntax/Notation.hs
@@ -1,6 +1,7 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ ScopedTypeVariables #-}
{-| 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.
@@ -23,6 +24,7 @@ import Data.Maybe
import Data.Typeable (Typeable)
import Agda.Syntax.Common
+import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.List
@@ -54,7 +56,13 @@ data GenPart
| NormalHole (NamedArg () Int)
-- ^ Argument is where the expression should go.
| IdPart RawName
- deriving (Typeable, Show, Eq)
+ deriving (Typeable, Show, Eq, Ord)
+
+instance KillRange GenPart where
+ killRange p = case p of
+ IdPart x -> IdPart x
+ BindHole i -> BindHole i
+ NormalHole x -> NormalHole $ killRange x
-- | Get a flat list of identifier parts of a notation.
stringParts :: Notation -> [RawName]
@@ -83,7 +91,7 @@ data NotationKind
| PostfixNotation -- ^ Ex: @bla_blub_@.
| NonfixNotation -- ^ Ex: @bla_blub@.
| NoNotation
- deriving (Eq)
+ deriving (Eq, Show)
-- | Classify a notation by presence of leading and/or trailing hole.
notationKind :: Notation -> NotationKind