{-# OPTIONS_GHC -Wunused-imports #-}

{-| 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.Arrow ( (&&&) )
import Control.DeepSeq
import Control.Monad
import Control.Monad.Except

import qualified Data.List as List
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.Common.Pretty
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, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Singleton

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' NewNotation Fixity
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 = 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 = 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 :: List1 NewNotation -> List1 NewNotation
mergeNotations :: NonEmpty NewNotation -> NonEmpty NewNotation
mergeNotations =
  (NonEmpty NewNotation -> NewNotation)
-> List1 (NonEmpty NewNotation) -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty NewNotation -> NewNotation
merge
  (List1 (NonEmpty NewNotation) -> NonEmpty NewNotation)
-> (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation
-> NonEmpty NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> List1 (NonEmpty NewNotation) -> List1 (NonEmpty NewNotation)
forall a b. (a -> List1 b) -> List1 a -> List1 b
List1.concatMap1 NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
groupIfLevelsMatch
  (List1 (NonEmpty NewNotation) -> List1 (NonEmpty NewNotation))
-> (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation
-> List1 (NonEmpty NewNotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NewNotation -> (Notation, Bool))
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
List1.groupOn1 (NewNotation -> Notation
notation (NewNotation -> Notation)
-> (NewNotation -> Bool) -> NewNotation -> (Notation, Bool)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& NewNotation -> Bool
notaIsOperator)
  where
  groupIfLevelsMatch :: List1 NewNotation -> List1 (List1 NewNotation)
  groupIfLevelsMatch :: NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
groupIfLevelsMatch NonEmpty NewNotation
ns =
    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 NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall el coll. Singleton el coll => el -> coll
singleton (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc (NonEmpty NewNotation -> NonEmpty NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel NonEmpty NewNotation
ns
    else (NewNotation -> NonEmpty NewNotation)
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NewNotation -> NonEmpty NewNotation
forall el coll. Singleton el coll => el -> coll
singleton NonEmpty NewNotation
ns
    where
    -- Fixities of operators whose precedence level is not Unrelated.
    related :: [Fixity]
related = (NewNotation -> Maybe Fixity) -> NonEmpty NewNotation -> [Fixity]
forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Fixity -> Maybe Fixity
maybeRelated (Fixity -> Maybe Fixity)
-> (NewNotation -> Fixity) -> NewNotation -> Maybe Fixity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity) NonEmpty NewNotation
ns
      where
        maybeRelated :: Fixity -> Maybe Fixity
maybeRelated 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

    -- Precondition: All related operators have the same precedence
    -- level.
    --
    -- Gives all unrelated operators the same level.
    sameLevel :: NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel = (NewNotation -> NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Lens' NewNotation FixityLevel -> LensSet NewNotation FixityLevel
forall o i. Lens' o i -> LensSet o i
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' NewNotation Fixity
_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' Fixity FixityLevel
_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 :: NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc = (NewNotation -> NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Lens' NewNotation Associativity
-> LensSet NewNotation Associativity
forall o i. Lens' o i -> LensSet o i
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' NewNotation Fixity
_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' Fixity Associativity
_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 :: List1 NewNotation -> NewNotation
  merge :: NonEmpty NewNotation -> NewNotation
merge (NewNotation
n :| [NewNotation]
ns) = NewNotation
n { notaNames = Set.unions $ map notaNames $ n: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' NewNotation Fixity
_notaFixity :: Lens' NewNotation Fixity
_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 = 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