{-| 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.
-}

module Agda.Syntax.Notation where

import Prelude hiding (null)

import Control.DeepSeq
import Control.Monad
import Control.Monad.Except

import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set

import GHC.Generics (Generic)

import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Pretty()
import Agda.Syntax.Position

import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Pretty

import Agda.Utils.Impossible

-- | Data type constructed in the Happy parser; converted to
-- 'NotationPart' before it leaves the Happy code.
data HoleName
  = LambdaHole { HoleName -> List1 (Ranged [Char])
_bindHoleNames :: List1 RString
               , HoleName -> Ranged [Char]
holeName       :: RString
               }
    -- ^ @λ x₁ … xₙ → y@: The first argument contains the bound names.
  | ExprHole   { holeName      :: RString }
    -- ^ Simple named hole with hiding.

-- | Is the hole a binder?
isLambdaHole :: HoleName -> Bool
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole List1 (Ranged [Char])
_ Ranged [Char]
_) = Bool
True
isLambdaHole HoleName
_ = Bool
False

-- | Get a flat list of identifier parts of a notation.
stringParts :: Notation -> [String]
stringParts :: Notation -> [[Char]]
stringParts Notation
gs = [ Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
gs ]

-- | Target argument position of a part (Nothing if it is not a hole).
holeTarget :: NotationPart -> Maybe Int
holeTarget :: NotationPart -> Maybe Int
holeTarget (VarPart Range
_ Ranged BoundVariablePosition
n)  = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber (BoundVariablePosition -> Int) -> BoundVariablePosition -> Int
forall a b. (a -> b) -> a -> b
$ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (WildPart Ranged BoundVariablePosition
n)   = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber (BoundVariablePosition -> Int) -> BoundVariablePosition -> Int
forall a b. (a -> b) -> a -> b
$ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (HolePart Range
_ NamedArg (Ranged Int)
n) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Ranged Int -> Int
forall a. Ranged a -> a
rangedThing (Ranged Int -> Int) -> Ranged Int -> Int
forall a b. (a -> b) -> a -> b
$ NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
n
holeTarget IdPart{}       = Maybe Int
forall a. Maybe a
Nothing

-- | Is the part a hole?
isAHole :: NotationPart -> Bool
isAHole :: NotationPart -> Bool
isAHole HolePart{} = Bool
True
isAHole VarPart{}  = Bool
False
isAHole WildPart{} = Bool
False
isAHole IdPart{}   = Bool
False

-- | Is the part a binder?
isBinder :: NotationPart -> Bool
isBinder :: NotationPart -> Bool
isBinder HolePart{} = Bool
False
isBinder VarPart{}  = Bool
True
isBinder WildPart{} = Bool
True
isBinder IdPart{}   = Bool
False

-- | Classification of notations.

data NotationKind
  = InfixNotation   -- ^ Ex: @_bla_blub_@.
  | PrefixNotation  -- ^ Ex: @_bla_blub@.
  | PostfixNotation -- ^ Ex: @bla_blub_@.
  | NonfixNotation  -- ^ Ex: @bla_blub@.
  | NoNotation
   deriving (NotationKind -> NotationKind -> Bool
(NotationKind -> NotationKind -> Bool)
-> (NotationKind -> NotationKind -> Bool) -> Eq NotationKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NotationKind -> NotationKind -> Bool
== :: NotationKind -> NotationKind -> Bool
$c/= :: NotationKind -> NotationKind -> Bool
/= :: NotationKind -> NotationKind -> Bool
Eq, Int -> NotationKind -> ShowS
[NotationKind] -> ShowS
NotationKind -> [Char]
(Int -> NotationKind -> ShowS)
-> (NotationKind -> [Char])
-> ([NotationKind] -> ShowS)
-> Show NotationKind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotationKind -> ShowS
showsPrec :: Int -> NotationKind -> ShowS
$cshow :: NotationKind -> [Char]
show :: NotationKind -> [Char]
$cshowList :: [NotationKind] -> ShowS
showList :: [NotationKind] -> ShowS
Show, (forall x. NotationKind -> Rep NotationKind x)
-> (forall x. Rep NotationKind x -> NotationKind)
-> Generic NotationKind
forall x. Rep NotationKind x -> NotationKind
forall x. NotationKind -> Rep NotationKind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotationKind -> Rep NotationKind x
from :: forall x. NotationKind -> Rep NotationKind x
$cto :: forall x. Rep NotationKind x -> NotationKind
to :: forall x. Rep NotationKind x -> NotationKind
Generic)

-- | Classify a notation by presence of leading and/or trailing
-- /normal/ holes.
notationKind :: Notation -> NotationKind
notationKind :: Notation -> NotationKind
notationKind []  = NotationKind
NoNotation
notationKind (NotationPart
h:Notation
syn) =
  case (NotationPart -> Bool
isAHole NotationPart
h, NotationPart -> Bool
isAHole (NotationPart -> Bool) -> NotationPart -> Bool
forall a b. (a -> b) -> a -> b
$ NotationPart -> Notation -> NotationPart
forall a. a -> [a] -> a
last1 NotationPart
h Notation
syn) of
    (Bool
True , Bool
True ) -> NotationKind
InfixNotation
    (Bool
True , Bool
False) -> NotationKind
PostfixNotation
    (Bool
False, Bool
True ) -> NotationKind
PrefixNotation
    (Bool
False, Bool
False) -> NotationKind
NonfixNotation

-- | From notation with names to notation with indices.
--
--   An example (with some parts of the code omitted):
--   The lists
--   @["for", "x", "∈", "xs", "return", "e"]@
--   and
--   @['LambdaHole' ("x" :| []) "e", 'ExprHole' "xs"]@
--   are mapped to the following notation:
--   @
--      [ 'IdPart' "for"    , 'VarPart' ('BoundVariablePosition' 0 0)
--      , 'IdPart' "∈"      , 'HolePart' 1
--      , 'IdPart' "return" , 'HolePart' 0
--      ]
--   @
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation :: [NamedArg HoleName] -> [Ranged [Char]] -> Either [Char] Notation
mkNotation [NamedArg HoleName]
_ [] = [Char] -> Either [Char] Notation
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"empty notation is disallowed"
mkNotation [NamedArg HoleName]
holes [Ranged [Char]]
ids = do
  Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
uniqueHoleNames     (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use unique argument names"
  let Notation
xs :: Notation = (Ranged [Char] -> NotationPart) -> [Ranged [Char]] -> Notation
forall a b. (a -> b) -> [a] -> [b]
map Ranged [Char] -> NotationPart
mkPart [Ranged [Char]]
ids
  Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
noAdjacentHoles Notation
xs)  (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
     [ [Char]
"syntax must not contain adjacent holes ("
     , [Char]
prettyHoles
     , [Char]
")"
     ]
  Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isExprLinear Notation
xs)   (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use holes exactly once"
  Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isLambdaLinear Notation
xs) (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use binding holes exactly once"
  -- Andreas, 2018-10-18, issue #3285:
  -- syntax that is just a single hole is ill-formed and crashes the operator parser
  Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when   (Notation -> Bool
isSingleHole Notation
xs)   (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax cannot be a single hole"
  Notation -> Either [Char] Notation
forall a. a -> Either [Char] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Notation -> Either [Char] Notation)
-> Notation -> Either [Char] Notation
forall a b. (a -> b) -> a -> b
$ Notation -> Notation
insertWildParts Notation
xs
    where
      holeNames :: [RString]
      holeNames :: [Ranged [Char]]
holeNames = (NamedArg HoleName -> HoleName)
-> [NamedArg HoleName] -> [HoleName]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg [NamedArg HoleName]
holes [HoleName] -> (HoleName -> [Ranged [Char]]) -> [Ranged [Char]]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        LambdaHole List1 (Ranged [Char])
_ Ranged [Char]
y -> [Ranged [Char]
y]
        ExprHole Ranged [Char]
y     -> [Ranged [Char]
y]

      prettyHoles :: String
      prettyHoles :: [Char]
prettyHoles = [[Char]] -> [Char]
List.unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Ranged [Char] -> [Char]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
rawNameToString ShowS -> (Ranged [Char] -> [Char]) -> Ranged [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing) [Ranged [Char]]
holeNames

      mkPart :: Ranged [Char] -> NotationPart
mkPart Ranged [Char]
ident = NotationPart
-> (NotationPart -> NotationPart)
-> Maybe NotationPart
-> NotationPart
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ranged [Char] -> NotationPart
IdPart Ranged [Char]
ident) (NotationPart -> Ranged [Char] -> NotationPart
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` Ranged [Char]
ident) (Maybe NotationPart -> NotationPart)
-> Maybe NotationPart -> NotationPart
forall a b. (a -> b) -> a -> b
$ Ranged [Char]
-> [(Ranged [Char], NotationPart)] -> Maybe NotationPart
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ranged [Char]
ident [(Ranged [Char], NotationPart)]
holeMap

      holeNumbers :: [Int]
holeNumbers   = [Int
0 .. [NamedArg HoleName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg HoleName]
holes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

      numberedHoles :: [(Int, NamedArg HoleName)]
      numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles = [Int] -> [NamedArg HoleName] -> [(Int, NamedArg HoleName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
holeNumbers [NamedArg HoleName]
holes

      -- The WildParts don't correspond to anything in the right-hand side so
      -- we add them next to their corresponding body. Slightly subtle: due to
      -- the way the operator parsing works they can't be added first or last.
      insertWildParts :: [NotationPart] -> [NotationPart]
      insertWildParts :: Notation -> Notation
insertWildParts Notation
xs = (Ranged BoundVariablePosition -> Notation -> Notation)
-> Notation -> [Ranged BoundVariablePosition] -> Notation
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ranged BoundVariablePosition -> Notation -> Notation
ins Notation
xs [Ranged BoundVariablePosition]
wilds
        where
          wilds :: [Ranged BoundVariablePosition]
wilds = [ Ranged BoundVariablePosition
i | (Ranged [Char]
_, WildPart Ranged BoundVariablePosition
i) <- [(Ranged [Char], NotationPart)]
holeMap ]

          ins :: Ranged BoundVariablePosition -> Notation -> Notation
ins Ranged BoundVariablePosition
w (HolePart Range
r NamedArg (Ranged Int)
h : Notation
hs)
            | NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h Ranged Int -> Ranged Int -> Bool
forall a. Eq a => a -> a -> Bool
== (BoundVariablePosition -> Int)
-> Ranged BoundVariablePosition -> Ranged Int
forall a b. (a -> b) -> Ranged a -> Ranged b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundVariablePosition -> Int
holeNumber Ranged BoundVariablePosition
w =
              Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
r NamedArg (Ranged Int)
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
w NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Notation
hs
          ins Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
          ins Ranged BoundVariablePosition
_ [] = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__

          insBefore :: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w (HolePart Range
r NamedArg (Ranged Int)
h : Notation
hs)
            | NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h Ranged Int -> Ranged Int -> Bool
forall a. Eq a => a -> a -> Bool
== (BoundVariablePosition -> Int)
-> Ranged BoundVariablePosition -> Ranged Int
forall a b. (a -> b) -> Ranged a -> Ranged b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundVariablePosition -> Int
holeNumber Ranged BoundVariablePosition
w =
              Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
w NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
r NamedArg (Ranged Int)
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Notation
hs
          insBefore Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
          insBefore Ranged BoundVariablePosition
_ [] = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__

      -- A map (association list) from hole names to notation parts. A
      -- @LambdaHole@ contributes one or more entries, one @HolePart@
      -- and zero or more @VarPart@s or @WildParts@, all mapped to the
      -- same number.
      holeMap :: [(RString, NotationPart)]
      holeMap :: [(Ranged [Char], NotationPart)]
holeMap = do
        (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles
        let ri :: Ranged [Char] -> Ranged Int
ri Ranged [Char]
x   = Range -> Int -> Ranged Int
forall a. Range -> a -> Ranged a
Ranged (Ranged [Char] -> Range
forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) Int
i
            rp :: Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n = Range -> BoundVariablePosition -> Ranged BoundVariablePosition
forall a. Range -> a -> Ranged a
Ranged (Ranged [Char] -> Range
forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) (BoundVariablePosition -> Ranged BoundVariablePosition)
-> BoundVariablePosition -> Ranged BoundVariablePosition
forall a b. (a -> b) -> a -> b
$
                     BoundVariablePosition
                       { holeNumber :: Int
holeNumber = Int
i
                       , varNumber :: Int
varNumber  = Int
n
                       }
            hole :: Ranged [Char] -> NotationPart
hole Ranged [Char]
y = Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
forall a. Range' a
noRange (NamedArg (Ranged Int) -> NotationPart)
-> NamedArg (Ranged Int) -> NotationPart
forall a b. (a -> b) -> a -> b
$ (Named NamedName HoleName -> Named_ (Ranged Int))
-> NamedArg HoleName -> NamedArg (Ranged Int)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ranged [Char] -> Ranged Int
ri Ranged [Char]
y Ranged Int -> Named NamedName HoleName -> Named_ (Ranged Int)
forall a b. a -> Named NamedName b -> Named NamedName a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg HoleName
h
                              -- This range is filled in by mkPart.
        case NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg NamedArg HoleName
h of
          ExprHole Ranged [Char]
y      -> [(Ranged [Char]
y, Ranged [Char] -> NotationPart
hole Ranged [Char]
y)]
          LambdaHole List1 (Ranged [Char])
xs Ranged [Char]
y -> [(Ranged [Char]
y, Ranged [Char] -> NotationPart
hole Ranged [Char]
y)] [(Ranged [Char], NotationPart)]
-> [(Ranged [Char], NotationPart)]
-> [(Ranged [Char], NotationPart)]
forall a. [a] -> [a] -> [a]
++
            (Int -> Ranged [Char] -> (Ranged [Char], NotationPart))
-> [Int] -> [Ranged [Char]] -> [(Ranged [Char], NotationPart)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
              (\ Int
n Ranged [Char]
x -> case Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x of
                [Char]
"_" -> (Ranged [Char]
x, Ranged BoundVariablePosition -> NotationPart
WildPart (Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n))
                [Char]
_   -> (Ranged [Char]
x, Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Range
forall a. Range' a
noRange (Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n)))
                                   -- Filled in by mkPart.
              [Int
0..]
              (List1 (Ranged [Char]) -> [Item (List1 (Ranged [Char]))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
xs)

      -- Check whether all hole names are distinct.
      -- The hole names are the keys of the @holeMap@.
      uniqueHoleNames :: Bool
uniqueHoleNames = [Ranged [Char]] -> Bool
forall a. Eq a => [a] -> Bool
distinct [ Ranged [Char]
x | (Ranged [Char]
x, NotationPart
_) <- [(Ranged [Char], NotationPart)]
holeMap, Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ]

      isExprLinear :: Notation -> Bool
isExprLinear Notation
xs =
        [Int] -> [Int]
forall a. Ord a => [a] -> [a]
List.sort [ Int
i | NotationPart
x <- Notation
xs, NotationPart -> Bool
isAHole NotationPart
x, let Just Int
i = NotationPart -> Maybe Int
holeTarget NotationPart
x ]
          [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
==
        [Int]
holeNumbers

      isLambdaLinear :: Notation -> Bool
isLambdaLinear Notation
xs =
        [BoundVariablePosition] -> [BoundVariablePosition]
forall a. Ord a => [a] -> [a]
List.sort [ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
x | VarPart Range
_ Ranged BoundVariablePosition
x <- Notation
xs ]
          [BoundVariablePosition] -> [BoundVariablePosition] -> Bool
forall a. Eq a => a -> a -> Bool
==
        [ BoundVariablePosition { holeNumber :: Int
holeNumber = Int
i, varNumber :: Int
varNumber = Int
v }
        | (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles
        , LambdaHole List1 (Ranged [Char])
vs Ranged [Char]
_ <- [NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg NamedArg HoleName
h]
        , (Int
v, [Char]
x) <- [Int] -> [[Char]] -> [(Int, [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([[Char]] -> [(Int, [Char])]) -> [[Char]] -> [(Int, [Char])]
forall a b. (a -> b) -> a -> b
$ (Ranged [Char] -> [Char]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing ([Ranged [Char]] -> [[Char]]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ List1 (Ranged [Char]) -> [Item (List1 (Ranged [Char]))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
vs
        , [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_"
        ]

      noAdjacentHoles :: [NotationPart] -> Bool
      noAdjacentHoles :: Notation -> Bool
noAdjacentHoles =
        Notation -> Bool
noAdj (Notation -> Bool) -> (Notation -> Notation) -> Notation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        (NotationPart -> Bool) -> Notation -> Notation
forall a. (a -> Bool) -> [a] -> [a]
filter (\NotationPart
h -> case NotationPart
h of
                   HolePart{} -> Bool
True
                   IdPart{}   -> Bool
True
                   NotationPart
_          -> Bool
False)
        where
        noAdj :: Notation -> Bool
noAdj []       = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
        noAdj [NotationPart
x]      = Bool
True
        noAdj (NotationPart
x:NotationPart
y:Notation
xs) =
          Bool -> Bool
not (NotationPart -> Bool
isAHole NotationPart
x Bool -> Bool -> Bool
&& NotationPart -> Bool
isAHole NotationPart
y) Bool -> Bool -> Bool
&&
          Notation -> Bool
noAdj (NotationPart
yNotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
:Notation
xs)

      isSingleHole :: [NotationPart] -> Bool
      isSingleHole :: Notation -> Bool
isSingleHole = \case
        [ IdPart{} ] -> Bool
False
        [ NotationPart
_hole ]    -> Bool
True
        Notation
_            -> Bool
False

-- | All the notation information related to a name.
data NewNotation = NewNotation
  { NewNotation -> QName
notaName  :: QName
  , NewNotation -> Set Name
notaNames :: Set A.Name
    -- ^ The names the syntax and/or fixity belong to.
    --
    -- Invariant: The set is non-empty. Every name in the list matches
    -- 'notaName'.
  , NewNotation -> Fixity
notaFixity :: Fixity
    -- ^ Associativity and precedence (fixity) of the names.
  , NewNotation -> Notation
notation :: Notation
    -- ^ Syntax associated with the names.
  , NewNotation -> Bool
notaIsOperator :: Bool
    -- ^ True if the notation comes from an operator (rather than a
    -- syntax declaration).
  } deriving (Int -> NewNotation -> ShowS
[NewNotation] -> ShowS
NewNotation -> [Char]
(Int -> NewNotation -> ShowS)
-> (NewNotation -> [Char])
-> ([NewNotation] -> ShowS)
-> Show NewNotation
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NewNotation -> ShowS
showsPrec :: Int -> NewNotation -> ShowS
$cshow :: NewNotation -> [Char]
show :: NewNotation -> [Char]
$cshowList :: [NewNotation] -> ShowS
showList :: [NewNotation] -> ShowS
Show, (forall x. NewNotation -> Rep NewNotation x)
-> (forall x. Rep NewNotation x -> NewNotation)
-> Generic NewNotation
forall x. Rep NewNotation x -> NewNotation
forall x. NewNotation -> Rep NewNotation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NewNotation -> Rep NewNotation x
from :: forall x. NewNotation -> Rep NewNotation x
$cto :: forall x. Rep NewNotation x -> NewNotation
to :: forall x. Rep NewNotation x -> NewNotation
Generic)

instance LensFixity NewNotation where
  lensFixity :: Lens' Fixity NewNotation
lensFixity Fixity -> f Fixity
f NewNotation
nota = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
nota) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Fixity
fx -> NewNotation
nota { notaFixity :: Fixity
notaFixity = Fixity
fx }

-- | If an operator has no specific notation, then it is computed from
-- its name.
namesToNotation :: QName -> A.Name -> NewNotation
namesToNotation :: QName -> Name -> NewNotation
namesToNotation QName
q Name
n = NewNotation
  { notaName :: QName
notaName       = QName
q
  , notaNames :: Set Name
notaNames      = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
n
  , notaFixity :: Fixity
notaFixity     = Fixity
f
  , notation :: Notation
notation       = if Notation -> Bool
forall a. Null a => a -> Bool
null Notation
syn then Name -> Notation
syntaxOf (QName -> Name
unqualify QName
q) else Notation
syn
  , notaIsOperator :: Bool
notaIsOperator = Notation -> Bool
forall a. Null a => a -> Bool
null Notation
syn
  }
  where Fixity' Fixity
f Notation
syn Range
_ = Name -> Fixity'
A.nameFixity Name
n

-- | Replace 'noFixity' by 'defaultFixity'.
useDefaultFixity :: NewNotation -> NewNotation
useDefaultFixity :: NewNotation -> NewNotation
useDefaultFixity NewNotation
n
  | NewNotation -> Fixity
notaFixity NewNotation
n Fixity -> Fixity -> Bool
forall a. Eq a => a -> a -> Bool
== Fixity
noFixity = NewNotation
n { notaFixity :: Fixity
notaFixity = Fixity
defaultFixity }
  | Bool
otherwise                = NewNotation
n

-- | Return the 'IdPart's of a notation, the first part qualified,
--   the other parts unqualified.
--   This allows for qualified use of operators, e.g.,
--   @M.for x ∈ xs return e@, or @x ℕ.+ y@.
notationNames :: NewNotation -> [QName]
notationNames :: NewNotation -> [QName]
notationNames (NewNotation QName
q Set Name
_ Fixity
_ Notation
parts Bool
_) =
  ((Name -> QName) -> Name -> QName)
-> [Name -> QName] -> [Name] -> [QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
($) (Name -> QName
reQualify (Name -> QName) -> [Name -> QName] -> [Name -> QName]
forall a. a -> [a] -> [a]
: (Name -> QName) -> [Name -> QName]
forall a. a -> [a]
repeat Name -> QName
QName) [[Char] -> Name
simpleName ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
parts ]
  where
    -- The qualification of @q@.
    modules :: [Name]
modules     = NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (QName -> NonEmpty Name
qnameParts QName
q)
    -- Putting the qualification onto @x@.
    reQualify :: Name -> QName
reQualify Name
x = (Name -> QName -> QName) -> QName -> [Name] -> QName
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr Name -> QName -> QName
Qual (Name -> QName
QName Name
x) [Name]
modules

-- | Create a 'Notation' (without binders) from a concrete 'Name'.
--   Does the obvious thing:
--   'Hole's become 'HolePart's, 'Id's become 'IdParts'.
--   If 'Name' has no 'Hole's, it returns 'noNotation'.
syntaxOf :: Name -> Notation
syntaxOf :: Name -> Notation
syntaxOf Name
y
  | Name -> Bool
isOperator Name
y = Int -> [NamePart] -> Notation
mkSyn Int
0 ([NamePart] -> Notation) -> [NamePart] -> Notation
forall a b. (a -> b) -> a -> b
$ NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
List1.toList (NameParts -> [Item NameParts]) -> NameParts -> [Item NameParts]
forall a b. (a -> b) -> a -> b
$ Name -> NameParts
nameNameParts Name
y
  | Bool
otherwise    = Notation
noNotation
  where
    -- Turn a concrete name into a Notation,
    -- numbering the holes from left to right.
    -- Result will have no 'BindingHole's.
    mkSyn :: Int -> [NamePart] -> Notation
    mkSyn :: Int -> [NamePart] -> Notation
mkSyn Int
n []          = []
    mkSyn Int
n (NamePart
Hole : [NamePart]
xs) = Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
forall a. Range' a
noRange (Ranged Int -> NamedArg (Ranged Int)
forall a. a -> NamedArg a
defaultNamedArg (Ranged Int -> NamedArg (Ranged Int))
-> Ranged Int -> NamedArg (Ranged Int)
forall a b. (a -> b) -> a -> b
$ Int -> Ranged Int
forall a. a -> Ranged a
unranged Int
n) NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) [NamePart]
xs
    mkSyn Int
n (Id [Char]
x : [NamePart]
xs) = Ranged [Char] -> NotationPart
IdPart ([Char] -> Ranged [Char]
forall a. a -> Ranged a
unranged [Char]
x) NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn Int
n [NamePart]
xs

-- | Merges 'NewNotation's that have the same precedence level and
-- notation, with two exceptions:
--
-- * Operators and notations coming from syntax declarations are kept
--   separate.
--
-- * If /all/ instances of a given 'NewNotation' have the same
--   precedence level or are \"unrelated\", then they are merged. They
--   get the given precedence level, if any, and otherwise they become
--   unrelated (but related to each other).
--
-- If 'NewNotation's that are merged have distinct associativities,
-- then they get 'NonAssoc' as their associativity.
--
-- Precondition: No 'A.Name' may occur in more than one list element.
-- Every 'NewNotation' must have the same 'notaName'.
--
-- Postcondition: No 'A.Name' occurs in more than one list element.
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations =
  ([NewNotation] -> NewNotation) -> [[NewNotation]] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map [NewNotation] -> NewNotation
merge ([[NewNotation]] -> [NewNotation])
-> ([NewNotation] -> [[NewNotation]])
-> [NewNotation]
-> [NewNotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ([NewNotation] -> [[NewNotation]])
-> [[NewNotation]] -> [[NewNotation]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch ([[NewNotation]] -> [[NewNotation]])
-> ([NewNotation] -> [[NewNotation]])
-> [NewNotation]
-> [[NewNotation]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (NewNotation -> (Notation, Bool))
-> [NewNotation] -> [[NewNotation]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn (\NewNotation
n -> ( NewNotation -> Notation
notation NewNotation
n
                 , NewNotation -> Bool
notaIsOperator NewNotation
n
                 ))
  where
  groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
  groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch []         = [[NewNotation]]
forall a. HasCallStack => a
__IMPOSSIBLE__
  groupIfLevelsMatch ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) =
    if [FixityLevel] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((Fixity -> FixityLevel) -> [Fixity] -> [FixityLevel]
forall a b. (a -> b) -> [a] -> [b]
map Fixity -> FixityLevel
fixityLevel [Fixity]
related)
    then [[NewNotation] -> [NewNotation]
sameAssoc ([NewNotation] -> [NewNotation]
sameLevel [NewNotation]
ns)]
    else (NewNotation -> [NewNotation]) -> [NewNotation] -> [[NewNotation]]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> [NewNotation] -> [NewNotation]
forall a. a -> [a] -> [a]
: []) [NewNotation]
ns
    where
    -- Fixities of operators whose precedence level is not Unrelated.
    related :: [Fixity]
related = (NewNotation -> Maybe Fixity) -> [NewNotation] -> [Fixity]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((\Fixity
f -> case Fixity -> FixityLevel
fixityLevel Fixity
f of
                                FixityLevel
Unrelated  -> Maybe Fixity
forall a. Maybe a
Nothing
                                Related {} -> Fixity -> Maybe Fixity
forall a. a -> Maybe a
Just Fixity
f)
                              (Fixity -> Maybe Fixity)
-> (NewNotation -> Fixity) -> NewNotation -> Maybe Fixity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity) [NewNotation]
ns

    -- Precondition: All related operators have the same precedence
    -- level.
    --
    -- Gives all unrelated operators the same level.
    sameLevel :: [NewNotation] -> [NewNotation]
sameLevel = (NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' FixityLevel NewNotation -> LensSet FixityLevel NewNotation
forall i o. Lens' i o -> LensSet i o
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' Fixity NewNotation
_notaFixity ((Fixity -> f Fixity) -> NewNotation -> f NewNotation)
-> ((FixityLevel -> f FixityLevel) -> Fixity -> f Fixity)
-> (FixityLevel -> f FixityLevel)
-> NewNotation
-> f NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixityLevel -> f FixityLevel) -> Fixity -> f Fixity
Lens' FixityLevel Fixity
_fixityLevel) FixityLevel
level)
      where
      level :: FixityLevel
level = case [Fixity]
related of
        Fixity
f : [Fixity]
_ -> Fixity -> FixityLevel
fixityLevel Fixity
f
        []    -> FixityLevel
Unrelated

    -- If all related operators have the same associativity, then the
    -- unrelated operators get the same associativity, and otherwise
    -- all operators get the associativity NonAssoc.
    sameAssoc :: [NewNotation] -> [NewNotation]
sameAssoc = (NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' Associativity NewNotation
-> LensSet Associativity NewNotation
forall i o. Lens' i o -> LensSet i o
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' Fixity NewNotation
_notaFixity ((Fixity -> f Fixity) -> NewNotation -> f NewNotation)
-> ((Associativity -> f Associativity) -> Fixity -> f Fixity)
-> (Associativity -> f Associativity)
-> NewNotation
-> f NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Associativity -> f Associativity) -> Fixity -> f Fixity
Lens' Associativity Fixity
_fixityAssoc) Associativity
assoc)
      where
      assoc :: Associativity
assoc = case [Fixity]
related of
        Fixity
f : [Fixity]
_ | [Associativity] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((Fixity -> Associativity) -> [Fixity] -> [Associativity]
forall a b. (a -> b) -> [a] -> [b]
map Fixity -> Associativity
fixityAssoc [Fixity]
related) -> Fixity -> Associativity
fixityAssoc Fixity
f
        [Fixity]
_                                          -> Associativity
NonAssoc

  merge :: [NewNotation] -> NewNotation
  merge :: [NewNotation] -> NewNotation
merge []         = NewNotation
forall a. HasCallStack => a
__IMPOSSIBLE__
  merge ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) = NewNotation
n { notaNames :: Set Name
notaNames = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Name] -> Set Name) -> [Set Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ (NewNotation -> Set Name) -> [NewNotation] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> Set Name
notaNames [NewNotation]
ns }

-- | Check if a notation contains any lambdas (in which case it cannot be used in a pattern).
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation NewNotation
n = (NotationPart -> Bool) -> Notation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NotationPart -> Bool
isBinder (NewNotation -> Notation
notation NewNotation
n)
  where
    isBinder :: NotationPart -> Bool
isBinder VarPart{}  = Bool
True
    isBinder WildPart{} = Bool
True
    isBinder IdPart{}   = Bool
False
    isBinder HolePart{} = Bool
False

-- | Lens for 'Fixity' in 'NewNotation'.

_notaFixity :: Lens' Fixity NewNotation
_notaFixity :: Lens' Fixity NewNotation
_notaFixity Fixity -> f Fixity
f NewNotation
r = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
r) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Fixity
x -> NewNotation
r { notaFixity :: Fixity
notaFixity = Fixity
x }

-- * Sections

-- | Sections, as well as non-sectioned operators.

data NotationSection = NotationSection
  { NotationSection -> NewNotation
sectNotation  :: NewNotation
  , NotationSection -> NotationKind
sectKind      :: NotationKind
    -- ^ For non-sectioned operators this should match the notation's
    -- 'notationKind'.
  , NotationSection -> Maybe FixityLevel
sectLevel     :: Maybe FixityLevel
    -- ^ Effective precedence level. 'Nothing' for closed notations.
  , NotationSection -> Bool
sectIsSection :: Bool
    -- ^ 'False' for non-sectioned operators.
  }
  deriving (Int -> NotationSection -> ShowS
[NotationSection] -> ShowS
NotationSection -> [Char]
(Int -> NotationSection -> ShowS)
-> (NotationSection -> [Char])
-> ([NotationSection] -> ShowS)
-> Show NotationSection
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotationSection -> ShowS
showsPrec :: Int -> NotationSection -> ShowS
$cshow :: NotationSection -> [Char]
show :: NotationSection -> [Char]
$cshowList :: [NotationSection] -> ShowS
showList :: [NotationSection] -> ShowS
Show, (forall x. NotationSection -> Rep NotationSection x)
-> (forall x. Rep NotationSection x -> NotationSection)
-> Generic NotationSection
forall x. Rep NotationSection x -> NotationSection
forall x. NotationSection -> Rep NotationSection x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NotationSection -> Rep NotationSection x
from :: forall x. NotationSection -> Rep NotationSection x
$cto :: forall x. Rep NotationSection x -> NotationSection
to :: forall x. Rep NotationSection x -> NotationSection
Generic)

-- | Converts a notation to a (non-)section.

noSection :: NewNotation -> NotationSection
noSection :: NewNotation -> NotationSection
noSection NewNotation
n = NotationSection
  { sectNotation :: NewNotation
sectNotation  = NewNotation
n
  , sectKind :: NotationKind
sectKind      = Notation -> NotationKind
notationKind (NewNotation -> Notation
notation NewNotation
n)
  , sectLevel :: Maybe FixityLevel
sectLevel     = FixityLevel -> Maybe FixityLevel
forall a. a -> Maybe a
Just (Fixity -> FixityLevel
fixityLevel (NewNotation -> Fixity
notaFixity NewNotation
n))
  , sectIsSection :: Bool
sectIsSection = Bool
False
  }


-- * Pretty printing

instance Pretty NewNotation where
  pretty :: NewNotation -> Doc
pretty (NewNotation QName
x Set Name
_xs Fixity
fx Notation
nota Bool
isOp) = Doc -> Doc -> Doc -> Doc
hsepWith Doc
"=" Doc
px Doc
pn
    where
    px :: Doc
px = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [ if Bool
isOp then Doc
forall a. Null a => a
empty else Doc
"syntax" , Fixity -> Doc
forall a. Pretty a => a -> Doc
pretty Fixity
fx , QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x ]
    pn :: Doc
pn = if Bool
isOp then Doc
forall a. Null a => a
empty else Notation -> Doc
forall a. Pretty a => a -> Doc
pretty Notation
nota

instance Pretty NotationKind where pretty :: NotationKind -> Doc
pretty = NotationKind -> Doc
forall a. Show a => a -> Doc
pshow

instance Pretty NotationSection where
  pretty :: NotationSection -> Doc
pretty (NotationSection NewNotation
nota NotationKind
kind Maybe FixityLevel
mlevel Bool
isSection)
    | Bool
isSection = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep
        [ Doc
"section"
        , NotationKind -> Doc
forall a. Pretty a => a -> Doc
pretty NotationKind
kind
        , Doc -> (FixityLevel -> Doc) -> Maybe FixityLevel -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty FixityLevel -> Doc
forall a. Pretty a => a -> Doc
pretty Maybe FixityLevel
mlevel
        , NewNotation -> Doc
forall a. Pretty a => a -> Doc
pretty NewNotation
nota
        ]
    | Bool
otherwise = NewNotation -> Doc
forall a. Pretty a => a -> Doc
pretty NewNotation
nota

-- NFData instances

instance NFData NotationKind
instance NFData NewNotation
instance NFData NotationSection