    {-# 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.DeepSeq
    import Control.Monad
    import Control.Monad.Except

    import qualified Data.List as List

    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.Set1            ( Set1 )
    import qualified Agda.Utils.Set1  as Set1
    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
    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"
      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]
    ")"
         ]
      -- 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
            (i, h) <- [(Int, NamedArg HoleName)]
    numberedHoles
            let 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]
    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]
    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 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 -> Set1 Name
    notaNames :: Set1 A.Name
        -- ^ The names the syntax and/or fixity belong to.
        --
        -- Invariant: 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 :: Set1 Name
    notaNames      = Name -> Set1 Name
    forall el coll. Singleton el coll => el -> coll
    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 Set1 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 ns :: NonEmpty NewNotation
    ns@(NewNotation
    _ :| []) = NonEmpty NewNotation
    ns
    mergeNotations NonEmpty NewNotation
    ns =
      (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)
      (NonEmpty NewNotation -> NonEmpty NewNotation)
    -> NonEmpty NewNotation -> NonEmpty NewNotation
    forall a b. (a -> b) -> a -> b
    $ NonEmpty NewNotation
    ns
      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 ns :: NonEmpty NewNotation
    ns@(NewNotation
    n :| [NewNotation]
    _) = NewNotation
    n { notaNames = Set1.unions $ fmap notaNames 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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 Set1 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