    {-| 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 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 'GenPart'
    --   before it leaves the Happy code.
    data HoleName
      = LambdaHole { HoleName -> RString
    _bindHoleName :: RString
                   , HoleName -> RString
    holeName      :: RString }
        -- ^ @\ x -> y@; 1st argument is the bound name (unused for now).
      | ExprHole   { holeName      :: RString }
        -- ^ Simple named hole with hiding.

    -- | Is the hole a binder?
    isLambdaHole :: HoleName -> Bool
    isLambdaHole :: HoleName -> Bool
    isLambdaHole (LambdaHole RString
    _ RString
    _) = 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 = [ RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    x | IdPart RString
    x <- Notation
    gs ]

    -- | Target argument position of a part (Nothing if it is not a hole).
    holeTarget :: GenPart -> Maybe Int
    holeTarget :: GenPart -> Maybe Int
    holeTarget (BindHole Range
    _   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
    n
    holeTarget (WildHole     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
    n
    holeTarget (NormalHole 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? WildHoles don't count since they don't correspond to
    --   anything the user writes.
    isAHole :: GenPart -> Bool
    isAHole :: GenPart -> Bool
    isAHole BindHole{}   = Bool
    True
    isAHole NormalHole{} = Bool
    True
    isAHole WildHole{}   = Bool
    False
    isAHole IdPart{}     = Bool
    False

    -- | Is the part a normal hole?
    isNormalHole :: GenPart -> Bool
    isNormalHole :: GenPart -> Bool
    isNormalHole NormalHole{} = Bool
    True
    isNormalHole BindHole{}   = Bool
    False
    isNormalHole WildHole{}   = Bool
    False
    isNormalHole IdPart{}     = Bool
    False

    -- | Is the part a binder?
    isBindingHole :: GenPart -> Bool
    isBindingHole :: GenPart -> Bool
    isBindingHole BindHole{} = Bool
    True
    isBindingHole WildHole{} = Bool
    True
    isBindingHole GenPart
    _          = 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
    /= :: NotationKind -> NotationKind -> Bool
    $c/= :: NotationKind -> NotationKind -> Bool
    == :: NotationKind -> NotationKind -> Bool
    $c== :: 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
    showList :: [NotationKind] -> ShowS
    $cshowList :: [NotationKind] -> ShowS
    show :: NotationKind -> [Char]
    $cshow :: NotationKind -> [Char]
    showsPrec :: Int -> NotationKind -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep NotationKind x -> NotationKind
    $cfrom :: forall x. NotationKind -> Rep NotationKind x
    Generic)

    -- | Classify a notation by presence of leading and/or trailing
    -- /normal/ holes.
    notationKind :: Notation -> NotationKind
    notationKind :: Notation -> NotationKind
    notationKind []  = NotationKind
    NoNotation
    notationKind (GenPart
    h:Notation
    syn) =
      case (GenPart -> Bool
    isNormalHole GenPart
    h, GenPart -> Bool
    isNormalHole (GenPart -> Bool) -> GenPart -> Bool
    forall a b. (a -> b) -> a -> b
    $ GenPart -> Notation -> GenPart
    forall a. a -> [a] -> a
    last1 GenPart
    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.
    --
    --   Example:
    --   @
    --      ids   = ["for", "x", "∈", "xs", "return", "e"]
    --      holes = [ LambdaHole "x" "e",  ExprHole "xs" ]
    --   @
    --   creates the notation
    --   @
    --      [ IdPart "for"    , BindHole 0
    --      , IdPart "∈"      , NormalHole 1
    --      , IdPart "return" , NormalHole 0
    --      ]
    --   @
    mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
    mkNotation :: [NamedArg HoleName] -> [RString] -> Either [Char] Notation
    mkNotation [NamedArg HoleName]
    _ [] = [Char] -> Either [Char] Notation
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "empty notation is disallowed"
    mkNotation [NamedArg HoleName]
    holes [RString]
    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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "syntax must use unique argument names"
      let Notation
    xs :: Notation = (RString -> GenPart) -> [RString] -> Notation
    forall a b. (a -> b) -> [a] -> [b]
    map RString -> GenPart
    mkPart [RString]
    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 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 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 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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError [Char]
    "syntax cannot be a single hole"
      Notation -> Either [Char] Notation
    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
    insertWildHoles Notation
    xs
        where
          holeNames :: [RString]
          holeNames :: [RString]
    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 -> [RString]) -> [RString]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            LambdaHole RString
    x RString
    y -> [RString
    x, RString
    y]
            ExprHole RString
    y     -> [RString
    y]

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

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

          holeNumbers :: [Int]
    holeNumbers   = [Int
    0 .. [NamedArg HoleName] -> 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 WildHoles 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.
          insertWildHoles :: [GenPart] -> [GenPart]
          insertWildHoles :: Notation -> Notation
    insertWildHoles Notation
    xs = (Ranged Int -> Notation -> Notation)
    -> Notation -> [Ranged Int] -> Notation
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Ranged Int -> Notation -> Notation
    ins Notation
    xs [Ranged Int]
    wilds
            where
              wilds :: [Ranged Int]
    wilds = [ Ranged Int
    i | (RString
    _, WildHole Ranged Int
    i) <- [(RString, GenPart)]
    holeMap ]
              ins :: Ranged Int -> Notation -> Notation
    ins Ranged Int
    w (NormalHole 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
    == Ranged Int
    w = Range -> NamedArg (Ranged Int) -> GenPart
    NormalHole Range
    r NamedArg (Ranged Int)
    h GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Ranged Int -> GenPart
    WildHole Ranged Int
    w GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Notation
    hs
              ins Ranged Int
    w (GenPart
    h : Notation
    hs) = GenPart
    h GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Ranged Int -> Notation -> Notation
    insBefore Ranged Int
    w Notation
    hs
              ins Ranged Int
    _ [] = Notation
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              insBefore :: Ranged Int -> Notation -> Notation
    insBefore Ranged Int
    w (NormalHole 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
    == Ranged Int
    w = Ranged Int -> GenPart
    WildHole Ranged Int
    w GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Range -> NamedArg (Ranged Int) -> GenPart
    NormalHole Range
    r NamedArg (Ranged Int)
    h GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Notation
    hs
              insBefore Ranged Int
    w (GenPart
    h : Notation
    hs) = GenPart
    h GenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    : Ranged Int -> Notation -> Notation
    insBefore Ranged Int
    w Notation
    hs
              insBefore Ranged Int
    _ [] = Notation
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- Create a map (association list) from hole names to holes.
          -- A @LambdaHole@ contributes two entries:
          -- both names are mapped to the same number,
          -- but distinguished by BindHole vs. NormalHole.
          holeMap :: [(RString, GenPart)]
          holeMap :: [(RString, GenPart)]
    holeMap = do
            (Int
    i, NamedArg HoleName
    h) <- [(Int, NamedArg HoleName)]
    numberedHoles    -- v This range is filled in by mkPart
            let ri :: RString -> Ranged Int
    ri RString
    x = Range -> Int -> Ranged Int
    forall a. Range -> a -> Ranged a
    Ranged (RString -> Range
    forall a. HasRange a => a -> Range
    getRange RString
    x) Int
    i
                normalHole :: RString -> GenPart
    normalHole RString
    y = Range -> NamedArg (Ranged Int) -> GenPart
    NormalHole Range
    forall a. Range' a
    noRange (NamedArg (Ranged Int) -> GenPart)
    -> NamedArg (Ranged Int) -> GenPart
    forall a b. (a -> b) -> a -> b
    $ (Named NamedName HoleName -> Named NamedName (Ranged Int))
    -> NamedArg HoleName -> NamedArg (Ranged Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (RString -> Ranged Int
    ri RString
    y Ranged Int
    -> Named NamedName HoleName -> Named NamedName (Ranged Int)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) NamedArg HoleName
    h
            case NamedArg HoleName -> HoleName
    forall a. NamedArg a -> a
    namedArg NamedArg HoleName
    h of
              ExprHole RString
    y       -> [(RString
    y, RString -> GenPart
    normalHole RString
    y)]
              LambdaHole RString
    x RString
    y
                | [Char]
    "_" <- RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    x -> [(RString
    x, Ranged Int -> GenPart
    WildHole (RString -> Ranged Int
    ri RString
    x)),         (RString
    y, RString -> GenPart
    normalHole RString
    y)]
                | Bool
    otherwise            -> [(RString
    x, Range -> Ranged Int -> GenPart
    BindHole Range
    forall a. Range' a
    noRange (RString -> Ranged Int
    ri RString
    x)), (RString
    y, RString -> GenPart
    normalHole RString
    y)]
                                                     -- Filled in by mkPart

          -- Check whether all hole names are distinct.
          -- The hole names are the keys of the @holeMap@.
          uniqueHoleNames :: Bool
    uniqueHoleNames = [RString] -> Bool
    forall a. Eq a => [a] -> Bool
    distinct [ RString
    x | (RString
    x, GenPart
    _) <- [(RString, GenPart)]
    holeMap, RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    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 | GenPart
    x <- Notation
    xs, GenPart -> Bool
    isNormalHole GenPart
    x, let Just Int
    i = GenPart -> Maybe Int
    holeTarget GenPart
    x ] [Int] -> [Int] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Int]
    holeNumbers
          isLambdaLinear :: Notation -> Bool
    isLambdaLinear Notation
    xs = [Int] -> [Int]
    forall a. Ord a => [a] -> [a]
    List.sort [ Ranged Int -> Int
    forall a. Ranged a -> a
    rangedThing Ranged Int
    x | BindHole Range
    _ Ranged Int
    x <- Notation
    xs ] [Int] -> [Int] -> Bool
    forall a. Eq a => a -> a -> Bool
    ==
                              [ Int
    i | (Int
    i, NamedArg HoleName
    h) <- [(Int, NamedArg HoleName)]
    numberedHoles,
                                    LambdaHole RString
    x RString
    _ <- [NamedArg HoleName -> HoleName
    forall a. NamedArg a -> a
    namedArg NamedArg HoleName
    h], RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    x [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    /= [Char]
    "_" ]

          noAdjacentHoles :: [GenPart] -> Bool
          noAdjacentHoles :: Notation -> Bool
    noAdjacentHoles []       = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          noAdjacentHoles [GenPart
    x]      = Bool
    True
          noAdjacentHoles (GenPart
    x:GenPart
    y:Notation
    xs) =
            Bool -> Bool
    not (GenPart -> Bool
    isAHole GenPart
    x Bool -> Bool -> Bool
    && GenPart -> Bool
    isAHole GenPart
    y) Bool -> Bool -> Bool
    && Notation -> Bool
    noAdjacentHoles (GenPart
    yGenPart -> Notation -> Notation
    forall a. a -> [a] -> [a]
    :Notation
    xs)

          isSingleHole :: [GenPart] -> Bool
          isSingleHole :: Notation -> Bool
    isSingleHole = \case
            [ IdPart{} ] -> Bool
    False
            [ GenPart
    _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
    showList :: [NewNotation] -> ShowS
    $cshowList :: [NewNotation] -> ShowS
    show :: NewNotation -> [Char]
    $cshow :: NewNotation -> [Char]
    showsPrec :: Int -> NewNotation -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep NewNotation x -> NewNotation
    $cfrom :: forall x. NewNotation -> Rep NewNotation x
    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 :: QName -> Set Name -> Fixity -> Notation -> Bool -> NewNotation
    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
    $ RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    x | IdPart RString
    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 (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 'NormalHole'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
    $ NonEmpty NamePart -> [NamePart]
    forall a. NonEmpty a -> [a]
    List1.toList (NonEmpty NamePart -> [NamePart])
    -> NonEmpty NamePart -> [NamePart]
    forall a b. (a -> b) -> a -> b
    $ Name -> NonEmpty NamePart
    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) -> GenPart
    NormalHole 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) GenPart -> 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) = RString -> GenPart
    IdPart ([Char] -> RString
    forall a. a -> Ranged a
    unranged [Char]
    x) GenPart -> 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 }

    -- | 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
    showList :: [NotationSection] -> ShowS
    $cshowList :: [NotationSection] -> ShowS
    show :: NotationSection -> [Char]
    $cshow :: NotationSection -> [Char]
    showsPrec :: Int -> NotationSection -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep NotationSection x -> NotationSection
    $cfrom :: forall x. NotationSection -> Rep NotationSection x
    Generic)

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

    noSection :: NewNotation -> NotationSection
    noSection :: NewNotation -> NotationSection
    noSection NewNotation
    n = NotationSection :: NewNotation
    -> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
    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