    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PatternSynonyms #-}

    {-| The parser doesn't know about operators and parses everything as normal
        function application. This module contains the functions that parses the
        operators properly. For a stand-alone implementation of this see
        @src\/prototyping\/mixfix\/old@.

        It also contains the function that puts parenthesis back given the
        precedence of the context.
    -}

    module Agda.Syntax.Concrete.Operators
        ( parseApplication
        , parseModuleApplication
        , parseLHS
        , parsePattern
        , parsePatternSyn
        ) where

    import Control.Applicative ( Alternative((<|>)))
    import Control.Arrow (second)
    import Control.Monad.Except (throwError)

    import Data.Either (partitionEithers)
    import qualified Data.Foldable as Fold
    import Data.Function
    import qualified Data.List as List
    import Data.Maybe
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.Traversable as Trav

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete hiding (appView)
    import Agda.Syntax.Concrete.Operators.Parser
    import Agda.Syntax.Concrete.Operators.Parser.Monad hiding (parse)
    import Agda.Syntax.Concrete.Pattern
    import qualified Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Position
    import Agda.Syntax.Notation
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad

    import Agda.TypeChecking.Monad.Base (typeError, TypeError(..), LHSOrPatSyn(..))
    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Monad.Debug
    import Agda.TypeChecking.Monad.State (getScope)

    import Agda.Utils.Either
    import Agda.Utils.Pretty
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import Agda.Utils.List2 (List2, pattern List2)
    import qualified Agda.Utils.List1 as List1
    import qualified Agda.Utils.List2 as List2
    import Agda.Utils.Maybe
    import Agda.Utils.Monad (guardWithError)
    import Agda.Utils.Trie (Trie)
    import qualified Agda.Utils.Trie as Trie

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Billing
    ---------------------------------------------------------------------------

    -- | Bills the operator parser.

    billToParser :: ExprKind -> ScopeM a -> ScopeM a
    billToParser :: forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    k = Account (BenchPhase (TCMT IO)) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo
      [ BenchPhase (TCMT IO)
    Phase
    Bench.Parsing
      , case ExprKind
    k of
          ExprKind
    IsExpr    -> BenchPhase (TCMT IO)
    Phase
    Bench.OperatorsExpr
          ExprKind
    IsPattern -> BenchPhase (TCMT IO)
    Phase
    Bench.OperatorsPattern
      ]

    ---------------------------------------------------------------------------
    -- * Building the parser
    ---------------------------------------------------------------------------

    type FlatScope = Map QName [AbstractName]

    -- | Compute all defined names in scope and their fixities/notations.
    -- Note that overloaded names (constructors) can have several
    -- fixities/notations. Then we 'mergeNotations'. (See issue 1194.)
    getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
    getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
    getDefinedNames KindsOfNames
    kinds FlatScope
    names =
      [ [NewNotation] -> [NewNotation]
    mergeNotations ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> NewNotation) -> [AbstractName] -> [NewNotation]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> Name -> NewNotation
    namesToNotation QName
    x (Name -> NewNotation)
    -> (AbstractName -> Name) -> AbstractName -> NewNotation
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    A.qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> QName
    anameName) [AbstractName]
    ds
      | (QName
    x, [AbstractName]
    ds) <- FlatScope -> [(QName, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList FlatScope
    names
      , (AbstractName -> Bool) -> [AbstractName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((KindOfName -> KindsOfNames -> Bool
    `elemKindsOfNames` KindsOfNames
    kinds) (KindOfName -> Bool)
    -> (AbstractName -> KindOfName) -> AbstractName -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind) [AbstractName]
    ds
      , Bool -> Bool
    not ([AbstractName] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [AbstractName]
    ds)
      ]
      -- Andreas, 2013-03-21 see Issue 822
      -- Names can have different kinds, i.e., 'defined' and 'constructor'.
      -- We need to consider all names that have *any* matching kind,
      -- not only those whose first appearing kind is matching.

    -- | Compute all names (first component) and operators/notations
    -- (second component) in scope.
    localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
    localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
    localNames FlatScope
    flat = do
      let defs :: [[NewNotation]]
    defs = KindsOfNames -> FlatScope -> [[NewNotation]]
    getDefinedNames KindsOfNames
    allKindsOfNames FlatScope
    flat
      [(Name, Name)]
    locals <- ((Name, Name) -> Name) -> [(Name, Name)] -> [(Name, Name)]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn (Name, Name) -> Name
    forall a b. (a, b) -> a
    fst ([(Name, Name)] -> [(Name, Name)])
    -> (LocalVars -> [(Name, Name)]) -> LocalVars -> [(Name, Name)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LocalVars -> [(Name, Name)]
    notShadowedLocals (LocalVars -> [(Name, Name)])
    -> TCMT IO LocalVars -> TCMT IO [(Name, Name)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO LocalVars
    forall (m :: * -> *). ReadTCState m => m LocalVars
    getLocalVars
      -- Note: Debug printout aligned with the one in buildParsers.
      [Char] -> VerboseLevel -> [[Char]] -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> VerboseLevel -> a -> m ()
    reportS [Char]
    "scope.operators" VerboseLevel
    50
        [ [Char]
    "flat  = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ FlatScope -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow FlatScope
    flat
        , [Char]
    "defs  = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[NewNotation]] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [[NewNotation]]
    defs
        , [Char]
    "locals= " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(Name, Name)] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [(Name, Name)]
    locals
        ]
      let localNots :: [NewNotation]
    localNots  = ((Name, Name) -> NewNotation) -> [(Name, Name)] -> [NewNotation]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Name) -> NewNotation
    localOp [(Name, Name)]
    locals
          notLocal :: NewNotation -> Bool
    notLocal   = Bool -> Bool
    not (Bool -> Bool) -> (NewNotation -> Bool) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem ((NewNotation -> QName) -> [NewNotation] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map NewNotation -> QName
    notaName [NewNotation]
    localNots) (QName -> Bool) -> (NewNotation -> QName) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> QName
    notaName
          otherNots :: [NewNotation]
    otherNots  = ([NewNotation] -> [NewNotation])
    -> [[NewNotation]] -> [NewNotation]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter NewNotation -> Bool
    notLocal) [[NewNotation]]
    defs
      ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation]))
    -> ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
    forall a b. (a -> b) -> a -> b
    $ ([NewNotation] -> [NewNotation])
    -> ([QName], [NewNotation]) -> ([QName], [NewNotation])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
    forall a b. (a -> b) -> [a] -> [b]
    map NewNotation -> NewNotation
    useDefaultFixity) (([QName], [NewNotation]) -> ([QName], [NewNotation]))
    -> ([QName], [NewNotation]) -> ([QName], [NewNotation])
    forall a b. (a -> b) -> a -> b
    $ [NewNotation] -> ([QName], [NewNotation])
    split ([NewNotation] -> ([QName], [NewNotation]))
    -> [NewNotation] -> ([QName], [NewNotation])
    forall a b. (a -> b) -> a -> b
    $ [NewNotation]
    localNots [NewNotation] -> [NewNotation] -> [NewNotation]
    forall a. [a] -> [a] -> [a]
    ++ [NewNotation]
    otherNots
      where
        localOp :: (Name, Name) -> NewNotation
    localOp (Name
    x, Name
    y) = QName -> Name -> NewNotation
    namesToNotation (Name -> QName
    QName Name
    x) Name
    y
        split :: [NewNotation] -> ([QName], [NewNotation])
    split          = [Either QName NewNotation] -> ([QName], [NewNotation])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either QName NewNotation] -> ([QName], [NewNotation]))
    -> ([NewNotation] -> [Either QName NewNotation])
    -> [NewNotation]
    -> ([QName], [NewNotation])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NewNotation -> [Either QName NewNotation])
    -> [NewNotation] -> [Either QName NewNotation]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NewNotation -> [Either QName NewNotation]
    opOrNot
        opOrNot :: NewNotation -> [Either QName NewNotation]
    opOrNot NewNotation
    n      = QName -> Either QName NewNotation
    forall a b. a -> Either a b
    Left (NewNotation -> QName
    notaName NewNotation
    n) Either QName NewNotation
    -> [Either QName NewNotation] -> [Either QName NewNotation]
    forall a. a -> [a] -> [a]
    :
                         [NewNotation -> Either QName NewNotation
    forall a b. b -> Either a b
    Right NewNotation
    n | Bool -> Bool
    not ([GenPart] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (NewNotation -> [GenPart]
    notation NewNotation
    n))]

    -- | A data structure used internally by 'buildParsers'.
    data InternalParsers e = InternalParsers
      { forall e. InternalParsers e -> Parser e e
    pTop    :: Parser e e
      , forall e. InternalParsers e -> Parser e e
    pApp    :: Parser e e
      , forall e. InternalParsers e -> Parser e [NamedArg e]
    pArgs   :: Parser e [NamedArg e]
      , forall e. InternalParsers e -> Parser e e
    pNonfix :: Parser e e
      , forall e. InternalParsers e -> Parser e e
    pAtom   :: Parser e e
      }

    -- | Expression kinds: Expressions or patterns.
    data ExprKind = IsExpr | IsPattern
      deriving (ExprKind -> ExprKind -> Bool
    (ExprKind -> ExprKind -> Bool)
    -> (ExprKind -> ExprKind -> Bool) -> Eq ExprKind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: ExprKind -> ExprKind -> Bool
    $c/= :: ExprKind -> ExprKind -> Bool
    == :: ExprKind -> ExprKind -> Bool
    $c== :: ExprKind -> ExprKind -> Bool
    Eq, VerboseLevel -> ExprKind -> [Char] -> [Char]
    [ExprKind] -> [Char] -> [Char]
    ExprKind -> [Char]
    (VerboseLevel -> ExprKind -> [Char] -> [Char])
    -> (ExprKind -> [Char])
    -> ([ExprKind] -> [Char] -> [Char])
    -> Show ExprKind
    forall a.
    (VerboseLevel -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    showList :: [ExprKind] -> [Char] -> [Char]
    $cshowList :: [ExprKind] -> [Char] -> [Char]
    show :: ExprKind -> [Char]
    $cshow :: ExprKind -> [Char]
    showsPrec :: VerboseLevel -> ExprKind -> [Char] -> [Char]
    $cshowsPrec :: VerboseLevel -> ExprKind -> [Char] -> [Char]
    Show)

    -- | The data returned by 'buildParsers'.

    data Parsers e = Parsers
      { forall e. Parsers e -> [e] -> [e]
    parser :: [e] -> [e]
        -- ^ A parser for expressions or patterns (depending on the
        -- 'ExprKind' argument given to 'buildParsers').
      , forall e. Parsers e -> [e] -> [[NamedArg e]]
    argsParser :: [e] -> [[NamedArg e]]
        -- ^ A parser for sequences of arguments.
      , forall e. Parsers e -> [NotationSection]
    operators :: [NotationSection]
        -- ^ All operators/notations/sections that were used to generate
        -- the grammar.
      , forall e. Parsers e -> FlatScope
    flattenedScope :: FlatScope
        -- ^ A flattened scope that only contains those names that are
        -- unqualified or qualified by qualifiers that occur in the list
        -- of names given to 'buildParsers'.
      }

    -- | Builds parsers for operator applications from all the operators
    -- and function symbols in scope.
    --
    -- When parsing a pattern we do not use bound names. The effect is
    -- that unqualified operator parts (that are not constructor parts)
    -- can be used as atomic names in the pattern (so they can be
    -- rebound). See @test/succeed/OpBind.agda@ for an example.
    --
    -- When parsing a pattern we also disallow the use of sections, mainly
    -- because there is little need for sections in patterns. Note that
    -- sections are parsed by splitting up names into multiple tokens
    -- (@_+_@ is replaced by @_@, @+@ and @_@), and if we were to support
    -- sections in patterns, then we would have to accept certain such
    -- sequences of tokens as single pattern variables.

    buildParsers
      :: forall e. IsExpr e
      => ExprKind
         -- ^ Should expressions or patterns be parsed?
      -> [QName]
         -- ^ This list must include every name part in the
         -- expression/pattern to be parsed (excluding name parts inside
         -- things like parenthesised subexpressions that are treated as
         -- atoms). The list is used to optimise the parser. For
         -- instance, a given notation is only included in the generated
         -- grammar if all of the notation's name parts are present in
         -- the list of names.
      -> ScopeM (Parsers e)
    buildParsers :: forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    kind [QName]
    exprNames = do
        FlatScope
    flat         <- [[Name]] -> ScopeInfo -> FlatScope
    flattenScope ([QName] -> [[Name]]
    qualifierModules [QName]
    exprNames) (ScopeInfo -> FlatScope) -> TCMT IO ScopeInfo -> TCMT IO FlatScope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                          TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
        ([QName]
    names, [NewNotation]
    ops) <- FlatScope -> ScopeM ([QName], [NewNotation])
    localNames FlatScope
    flat

        let -- All names.
            namesInExpr :: Set QName
            namesInExpr :: Set QName
    namesInExpr = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList [QName]
    exprNames

            partListsInExpr' :: [[NamePart]]
    partListsInExpr' = (QName -> [NamePart]) -> [QName] -> [[NamePart]]
    forall a b. (a -> b) -> [a] -> [b]
    map (NonEmpty NamePart -> [NamePart]
    forall a. NonEmpty a -> [a]
    List1.toList (NonEmpty NamePart -> [NamePart])
    -> (QName -> NonEmpty NamePart) -> QName -> [NamePart]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> NonEmpty NamePart
    nameParts (Name -> NonEmpty NamePart)
    -> (QName -> Name) -> QName -> NonEmpty NamePart
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    unqualify) ([QName] -> [[NamePart]]) -> [QName] -> [[NamePart]]
    forall a b. (a -> b) -> a -> b
    $
                               Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    namesInExpr

            partListTrie :: ([[NamePart]] -> t [k]) -> Trie k ()
    partListTrie [[NamePart]] -> t [k]
    f =
              ([k] -> Trie k () -> Trie k ()) -> Trie k () -> t [k] -> Trie k ()
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\[k]
    ps -> Trie k () -> Trie k () -> Trie k ()
    forall k v. Ord k => Trie k v -> Trie k v -> Trie k v
    Trie.union ([k] -> () -> Trie k ()
    forall k v. [k] -> v -> Trie k v
    Trie.everyPrefix [k]
    ps ()))
                    Trie k ()
    forall a. Null a => a
    Trie.empty
                    ([[NamePart]] -> t [k]
    f [[NamePart]]
    partListsInExpr')

            -- All names.
            partListsInExpr :: Trie NamePart ()
            partListsInExpr :: Trie NamePart ()
    partListsInExpr = ([[NamePart]] -> [[NamePart]]) -> Trie NamePart ()
    forall {t :: * -> *} {k}.
    (Foldable t, Ord k) =>
    ([[NamePart]] -> t [k]) -> Trie k ()
    partListTrie [[NamePart]] -> [[NamePart]]
    forall a. a -> a
    id

            -- All names, with the name parts in reverse order.
            reversedPartListsInExpr :: Trie NamePart ()
            reversedPartListsInExpr :: Trie NamePart ()
    reversedPartListsInExpr = ([[NamePart]] -> [[NamePart]]) -> Trie NamePart ()
    forall {t :: * -> *} {k}.
    (Foldable t, Ord k) =>
    ([[NamePart]] -> t [k]) -> Trie k ()
    partListTrie (([NamePart] -> [NamePart]) -> [[NamePart]] -> [[NamePart]]
    forall a b. (a -> b) -> [a] -> [b]
    map [NamePart] -> [NamePart]
    forall a. [a] -> [a]
    reverse)

            -- Every regular name part (not holes etc.).
            partsInExpr :: Set RawName
            partsInExpr :: Set [Char]
    partsInExpr =
              [[Char]] -> Set [Char]
    forall a. Ord a => [a] -> Set a
    Set.fromList [ [Char]
    s | Id [Char]
    s <- [[NamePart]] -> [NamePart]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[NamePart]]
    partListsInExpr' ]

            -- Are all name parts present in the expression?
            partsPresent :: NewNotation -> [Bool]
    partsPresent NewNotation
    n =
              [ [Char] -> Set [Char] -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member [Char]
    p Set [Char]
    partsInExpr
              | [Char]
    p <- [GenPart] -> [[Char]]
    stringParts (NewNotation -> [GenPart]
    notation NewNotation
    n)
              ]

            addHole :: Bool -> [Char] -> [NamePart]
    addHole Bool
    True  [Char]
    p = [NamePart
    Hole, [Char] -> NamePart
    Id [Char]
    p]
            addHole Bool
    False [Char]
    p = [[Char] -> NamePart
    Id [Char]
    p]

            -- Is the first identifier part present in n present in the
            -- expression, without any preceding name parts, except for a
            -- leading underscore iff withHole is True?
            firstPartPresent :: Bool -> [GenPart] -> Bool
    firstPartPresent Bool
    withHole [GenPart]
    n =
              [NamePart] -> Trie NamePart () -> Bool
    forall k v. Ord k => [k] -> Trie k v -> Bool
    Trie.member (Bool -> [Char] -> [NamePart]
    addHole Bool
    withHole [Char]
    p) Trie NamePart ()
    partListsInExpr
              where
              p :: [Char]
    p = case [GenPart]
    n of
                NormalHole{} : IdPart RString
    p : [GenPart]
    _ -> RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    p
                IdPart RString
    p : [GenPart]
    _                -> RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    p
                [GenPart]
    _                           -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Is the last identifier part present in n present in the
            -- expression, without any succeeding name parts, except for a
            -- trailing underscore iff withHole is True?
            lastPartPresent :: Bool -> [GenPart] -> Bool
    lastPartPresent Bool
    withHole [GenPart]
    n =
              [NamePart] -> Trie NamePart () -> Bool
    forall k v. Ord k => [k] -> Trie k v -> Bool
    Trie.member (Bool -> [Char] -> [NamePart]
    addHole Bool
    withHole [Char]
    p) Trie NamePart ()
    reversedPartListsInExpr
              where
              p :: [Char]
    p = case [GenPart] -> [GenPart]
    forall a. [a] -> [a]
    reverse [GenPart]
    n of
                NormalHole{} : IdPart RString
    p : [GenPart]
    _ -> RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    p
                IdPart RString
    p : [GenPart]
    _                -> RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    p
                [GenPart]
    _                           -> [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Are the initial and final identifier parts present with
            -- the right mix of leading and trailing underscores?
            correctUnderscores :: Bool -> Bool -> Notation -> Bool
            correctUnderscores :: Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    withInitialHole Bool
    withFinalHole [GenPart]
    n =
              Bool -> [GenPart] -> Bool
    firstPartPresent Bool
    withInitialHole [GenPart]
    n
                Bool -> Bool -> Bool
    &&
              Bool -> [GenPart] -> Bool
    lastPartPresent  Bool
    withFinalHole   [GenPart]
    n

            -- Should be used with operators (not sections) and notations
            -- coming from syntax declarations.
            filterCorrectUnderscoresOp :: [NewNotation] -> [NotationSection]
            filterCorrectUnderscoresOp :: [NewNotation] -> [NotationSection]
    filterCorrectUnderscoresOp [NewNotation]
    ns =
              [ NewNotation -> NotationSection
    noSection NewNotation
    n
              | NewNotation
    n <- [NewNotation]
    ns
              , if NewNotation -> Bool
    notaIsOperator NewNotation
    n
                then Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    False Bool
    False (NewNotation -> [GenPart]
    notation NewNotation
    n)
                else ([Char] -> Bool) -> [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (\[Char]
    s -> [NamePart] -> Trie NamePart () -> Bool
    forall k v. Ord k => [k] -> Trie k v -> Bool
    Trie.member [[Char] -> NamePart
    Id [Char]
    s] Trie NamePart ()
    partListsInExpr)
                         ([GenPart] -> [[Char]]
    stringParts ([GenPart] -> [[Char]]) -> [GenPart] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ NewNotation -> [GenPart]
    notation NewNotation
    n)
              ]

            -- Should be used with sections.
            correctUnderscoresSect :: NotationKind -> Notation -> Bool
            correctUnderscoresSect :: NotationKind -> [GenPart] -> Bool
    correctUnderscoresSect NotationKind
    k [GenPart]
    n = case (NotationKind
    k, [GenPart] -> NotationKind
    notationKind [GenPart]
    n) of
              (NotationKind
    PrefixNotation,  NotationKind
    InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    True Bool
    False [GenPart]
    n
              (NotationKind
    PostfixNotation, NotationKind
    InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    False Bool
    True [GenPart]
    n
              (NotationKind
    NonfixNotation,  NotationKind
    InfixNotation)   -> Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    True Bool
    True [GenPart]
    n
              (NotationKind
    NonfixNotation,  NotationKind
    PrefixNotation)  -> Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    False Bool
    True [GenPart]
    n
              (NotationKind
    NonfixNotation,  NotationKind
    PostfixNotation) -> Bool -> Bool -> [GenPart] -> Bool
    correctUnderscores Bool
    True Bool
    False [GenPart]
    n
              (NotationKind, NotationKind)
    _                                  -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- If "or" is replaced by "and" in conParts/allParts below,
            -- then the misspelled operator application "if x thenn x else
            -- x" can be parsed as "if" applied to five arguments,
            -- resulting in a confusing error message claiming that "if"
            -- is not in scope.

            ([NewNotation]
    non, [NewNotation]
    fix) = (NewNotation -> Bool)
    -> [NewNotation] -> ([NewNotation], [NewNotation])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition NewNotation -> Bool
    nonfix ((NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [Bool]
    partsPresent) [NewNotation]
    ops)

            cons :: [[NewNotation]]
    cons       = KindsOfNames -> FlatScope -> [[NewNotation]]
    getDefinedNames
                           ([KindOfName] -> KindsOfNames
    someKindsOfNames [KindOfName
    ConName, KindOfName
    CoConName, KindOfName
    FldName, KindOfName
    PatternSynName]) FlatScope
    flat
            conNames :: Set QName
    conNames   = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $
                           (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((QName -> Set QName -> Bool) -> Set QName -> QName -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Set QName
    namesInExpr) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $
                           ([NewNotation] -> QName) -> [[NewNotation]] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (NewNotation -> QName
    notaName (NewNotation -> QName)
    -> ([NewNotation] -> NewNotation) -> [NewNotation] -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NewNotation] -> NewNotation
    forall a. [a] -> a
    head) [[NewNotation]]
    cons
            conParts :: Set QName
    conParts   = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $
                           (NewNotation -> [QName]) -> [NewNotation] -> [QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NewNotation -> [QName]
    notationNames ([NewNotation] -> [QName]) -> [NewNotation] -> [QName]
    forall a b. (a -> b) -> a -> b
    $
                           (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [Bool]
    partsPresent) ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
    forall a b. (a -> b) -> a -> b
    $
                           [[NewNotation]] -> [NewNotation]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[NewNotation]]
    cons

            allNames :: Set QName
    allNames   = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $
                           (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((QName -> Set QName -> Bool) -> Set QName -> QName -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Set QName
    namesInExpr) [QName]
    names
            allParts :: Set QName
    allParts   = Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set QName
    conParts
                           ([QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $
                            (NewNotation -> [QName]) -> [NewNotation] -> [QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NewNotation -> [QName]
    notationNames ([NewNotation] -> [QName]) -> [NewNotation] -> [QName]
    forall a b. (a -> b) -> a -> b
    $
                            (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or ([Bool] -> Bool) -> (NewNotation -> [Bool]) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [Bool]
    partsPresent) [NewNotation]
    ops)

            isAtom :: QName -> Bool
    isAtom QName
    x
              | ExprKind
    kind ExprKind -> ExprKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExprKind
    IsPattern Bool -> Bool -> Bool
    && Bool -> Bool
    not (QName -> Bool
    isQualified QName
    x) =
                Bool -> Bool
    not (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    x Set QName
    conParts) Bool -> Bool -> Bool
    || QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    x Set QName
    conNames
              | Bool
    otherwise =
                Bool -> Bool
    not (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    x Set QName
    allParts) Bool -> Bool -> Bool
    || QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    x Set QName
    allNames
            -- If string is a part of notation, it cannot be used as an identifier,
            -- unless it is also used as an identifier. See issue 307.

            parseSections :: ParseSections
    parseSections = case ExprKind
    kind of
              ExprKind
    IsPattern -> ParseSections
    DoNotParseSections
              ExprKind
    IsExpr    -> ParseSections
    ParseSections

        let nonClosedSections :: FixityLevel -> [NewNotation] -> [NotationSection]
    nonClosedSections FixityLevel
    l [NewNotation]
    ns =
              case ParseSections
    parseSections of
                ParseSections
    DoNotParseSections -> []
                ParseSections
    ParseSections      ->
                  [ NewNotation
    -> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
    NotationSection NewNotation
    n NotationKind
    k (FixityLevel -> Maybe FixityLevel
    forall a. a -> Maybe a
    Just FixityLevel
    l) Bool
    True
                  | NewNotation
    n <- [NewNotation]
    ns
                  , NewNotation -> Bool
    isinfix NewNotation
    n Bool -> Bool -> Bool
    && NewNotation -> Bool
    notaIsOperator NewNotation
    n
                  , NotationKind
    k <- [NotationKind
    PrefixNotation, NotationKind
    PostfixNotation]
                  , NotationKind -> [GenPart] -> Bool
    correctUnderscoresSect NotationKind
    k (NewNotation -> [GenPart]
    notation NewNotation
    n)
                  ]

            unrelatedOperators :: [NotationSection]
            unrelatedOperators :: [NotationSection]
    unrelatedOperators =
              [NewNotation] -> [NotationSection]
    filterCorrectUnderscoresOp [NewNotation]
    unrelated
                [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++
              FixityLevel -> [NewNotation] -> [NotationSection]
    nonClosedSections FixityLevel
    Unrelated [NewNotation]
    unrelated
              where
              unrelated :: [NewNotation]
    unrelated = (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((FixityLevel -> FixityLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    == FixityLevel
    Unrelated) (FixityLevel -> Bool)
    -> (NewNotation -> FixityLevel) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> FixityLevel
    level) [NewNotation]
    fix

            nonWithSections :: [NotationSection]
            nonWithSections :: [NotationSection]
    nonWithSections =
              (NotationSection -> NotationSection)
    -> [NotationSection] -> [NotationSection]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NotationSection
    s -> NotationSection
    s { sectLevel :: Maybe FixityLevel
    sectLevel = Maybe FixityLevel
    forall a. Maybe a
    Nothing })
                  ([NewNotation] -> [NotationSection]
    filterCorrectUnderscoresOp [NewNotation]
    non)
                [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++
              case ParseSections
    parseSections of
                ParseSections
    DoNotParseSections -> []
                ParseSections
    ParseSections      ->
                  [ NewNotation
    -> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
    NotationSection NewNotation
    n NotationKind
    NonfixNotation Maybe FixityLevel
    forall a. Maybe a
    Nothing Bool
    True
                  | NewNotation
    n <- [NewNotation]
    fix
                  , NewNotation -> Bool
    notaIsOperator NewNotation
    n
                  , NotationKind -> [GenPart] -> Bool
    correctUnderscoresSect NotationKind
    NonfixNotation (NewNotation -> [GenPart]
    notation NewNotation
    n)
                  ]

            -- The triples have the form (level, operators). The lowest
            -- level comes first.
            relatedOperators :: [(PrecedenceLevel, [NotationSection])]
            relatedOperators :: [(PrecedenceLevel, [NotationSection])]
    relatedOperators =
              ([(PrecedenceLevel, [NotationSection])]
     -> (PrecedenceLevel, [NotationSection]))
    -> [[(PrecedenceLevel, [NotationSection])]]
    -> [(PrecedenceLevel, [NotationSection])]
    forall a b. (a -> b) -> [a] -> [b]
    map (\((PrecedenceLevel
    l, [NotationSection]
    ns) : [(PrecedenceLevel, [NotationSection])]
    rest) -> (PrecedenceLevel
    l, [NotationSection]
    ns [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++ ((PrecedenceLevel, [NotationSection]) -> [NotationSection])
    -> [(PrecedenceLevel, [NotationSection])] -> [NotationSection]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (PrecedenceLevel, [NotationSection]) -> [NotationSection]
    forall a b. (a, b) -> b
    snd [(PrecedenceLevel, [NotationSection])]
    rest)) ([[(PrecedenceLevel, [NotationSection])]]
     -> [(PrecedenceLevel, [NotationSection])])
    -> ([NewNotation] -> [[(PrecedenceLevel, [NotationSection])]])
    -> [NewNotation]
    -> [(PrecedenceLevel, [NotationSection])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
              ((PrecedenceLevel, [NotationSection])
     -> (PrecedenceLevel, [NotationSection]) -> Bool)
    -> [(PrecedenceLevel, [NotationSection])]
    -> [[(PrecedenceLevel, [NotationSection])]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    List.groupBy (PrecedenceLevel -> PrecedenceLevel -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (PrecedenceLevel -> PrecedenceLevel -> Bool)
    -> ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
    -> (PrecedenceLevel, [NotationSection])
    -> (PrecedenceLevel, [NotationSection])
    -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
    forall a b. (a, b) -> a
    fst) ([(PrecedenceLevel, [NotationSection])]
     -> [[(PrecedenceLevel, [NotationSection])]])
    -> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
    -> [NewNotation]
    -> [[(PrecedenceLevel, [NotationSection])]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
              ((PrecedenceLevel, [NotationSection])
     -> (PrecedenceLevel, [NotationSection]) -> Ordering)
    -> [(PrecedenceLevel, [NotationSection])]
    -> [(PrecedenceLevel, [NotationSection])]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (PrecedenceLevel -> PrecedenceLevel -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (PrecedenceLevel -> PrecedenceLevel -> Ordering)
    -> ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
    -> (PrecedenceLevel, [NotationSection])
    -> (PrecedenceLevel, [NotationSection])
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
    forall a b. (a, b) -> a
    fst) ([(PrecedenceLevel, [NotationSection])]
     -> [(PrecedenceLevel, [NotationSection])])
    -> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
    -> [NewNotation]
    -> [(PrecedenceLevel, [NotationSection])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
              (NewNotation -> Maybe (PrecedenceLevel, [NotationSection]))
    -> [NewNotation] -> [(PrecedenceLevel, [NotationSection])]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (\NewNotation
    n -> case NewNotation -> FixityLevel
    level NewNotation
    n of
                                FixityLevel
    Unrelated     -> Maybe (PrecedenceLevel, [NotationSection])
    forall a. Maybe a
    Nothing
                                r :: FixityLevel
    r@(Related PrecedenceLevel
    l) ->
                                  (PrecedenceLevel, [NotationSection])
    -> Maybe (PrecedenceLevel, [NotationSection])
    forall a. a -> Maybe a
    Just (PrecedenceLevel
    l, [NewNotation] -> [NotationSection]
    filterCorrectUnderscoresOp [NewNotation
    n] [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++
                                           FixityLevel -> [NewNotation] -> [NotationSection]
    nonClosedSections FixityLevel
    r [NewNotation
    n])) ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
    -> [NewNotation] -> [(PrecedenceLevel, [NotationSection])]
    forall a b. (a -> b) -> a -> b
    $
              [NewNotation]
    fix

            everything :: [NotationSection]
            everything :: [NotationSection]
    everything =
              ((PrecedenceLevel, [NotationSection]) -> [NotationSection])
    -> [(PrecedenceLevel, [NotationSection])] -> [NotationSection]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (PrecedenceLevel, [NotationSection]) -> [NotationSection]
    forall a b. (a, b) -> b
    snd [(PrecedenceLevel, [NotationSection])]
    relatedOperators [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++
              [NotationSection]
    unrelatedOperators [NotationSection] -> [NotationSection] -> [NotationSection]
    forall a. [a] -> [a] -> [a]
    ++
              [NotationSection]
    nonWithSections

        [Char] -> VerboseLevel -> [[Char]] -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> VerboseLevel -> a -> m ()
    reportS [Char]
    "scope.operators" VerboseLevel
    50
          [ [Char]
    "unrelatedOperators = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [NotationSection] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [NotationSection]
    unrelatedOperators
          , [Char]
    "nonWithSections    = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [NotationSection] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [NotationSection]
    nonWithSections
          , [Char]
    "relatedOperators   = " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(PrecedenceLevel, [NotationSection])] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [(PrecedenceLevel, [NotationSection])]
    relatedOperators
          ]

        let g :: InternalParsers e
    g = (InternalParsers e -> InternalParsers e) -> InternalParsers e
    forall a. (a -> a) -> a
    Data.Function.fix ((InternalParsers e -> InternalParsers e) -> InternalParsers e)
    -> (InternalParsers e -> InternalParsers e) -> InternalParsers e
    forall a b. (a -> b) -> a -> b
    $ \InternalParsers e
    p -> InternalParsers :: forall e.
    Parser e e
    -> Parser e e
    -> Parser e [NamedArg e]
    -> Parser e e
    -> Parser e e
    -> InternalParsers e
    InternalParsers
                  { pTop :: Parser e e
    pTop    = MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise MemoKey
    TopK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                              [Parser e e] -> Parser e e
    forall (t :: * -> *) (f :: * -> *) a.
    (Foldable t, Alternative f) =>
    t (f a) -> f a
    Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                                ((PrecedenceLevel, [NotationSection]) -> Parser e e -> Parser e e)
    -> Parser e e
    -> [(PrecedenceLevel, [NotationSection])]
    -> Parser e e
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\(PrecedenceLevel
    l, [NotationSection]
    ns) Parser e e
    higher ->
                                           PrecedenceKey
    -> ParseSections
    -> Parser e e
    -> [NotationSection]
    -> Parser e e
    -> Bool
    -> Parser e e
    mkP (PrecedenceLevel -> PrecedenceKey
    forall a b. b -> Either a b
    Right PrecedenceLevel
    l) ParseSections
    parseSections
                                               (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pTop InternalParsers e
    p) [NotationSection]
    ns Parser e e
    higher Bool
    True) (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pApp InternalParsers e
    p)
                                       [(PrecedenceLevel, [NotationSection])]
    relatedOperators Parser e e -> [Parser e e] -> [Parser e e]
    forall a. a -> [a] -> [a]
    :
                                (PrecedenceLevel -> NotationSection -> Parser e e)
    -> [PrecedenceLevel] -> [NotationSection] -> [Parser e e]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ PrecedenceLevel
    k NotationSection
    n ->
                                        PrecedenceKey
    -> ParseSections
    -> Parser e e
    -> [NotationSection]
    -> Parser e e
    -> Bool
    -> Parser e e
    mkP (PrecedenceLevel -> PrecedenceKey
    forall a b. a -> Either a b
    Left PrecedenceLevel
    k) ParseSections
    parseSections
                                            (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pTop InternalParsers e
    p) [NotationSection
    n] (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pApp InternalParsers e
    p) Bool
    False) [PrecedenceLevel
    0..] [NotationSection]
    unrelatedOperators
                  , pApp :: Parser e e
    pApp    = MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise MemoKey
    AppK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $ Parser e e -> Parser e [NamedArg e] -> Parser e e
    forall e.
    IsExpr e =>
    Parser e e -> Parser e [NamedArg e] -> Parser e e
    appP (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pNonfix InternalParsers e
    p) (InternalParsers e -> Parser e [NamedArg e]
    forall e. InternalParsers e -> Parser e [NamedArg e]
    pArgs InternalParsers e
    p)
                  , pArgs :: Parser e [NamedArg e]
    pArgs   = Parser e e -> Parser e [NamedArg e]
    forall e. IsExpr e => Parser e e -> Parser e [NamedArg e]
    argsP (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pNonfix InternalParsers e
    p)
                  , pNonfix :: Parser e e
    pNonfix = MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise MemoKey
    NonfixK (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                              [Parser e e] -> Parser e e
    forall (t :: * -> *) (f :: * -> *) a.
    (Foldable t, Alternative f) =>
    t (f a) -> f a
    Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                                InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pAtom InternalParsers e
    p Parser e e -> [Parser e e] -> [Parser e e]
    forall a. a -> [a] -> [a]
    :
                                (NotationSection -> Parser e e)
    -> [NotationSection] -> [Parser e e]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NotationSection
    sect ->
                                  let n :: NewNotation
    n = NotationSection -> NewNotation
    sectNotation NotationSection
    sect

                                      inner :: forall k. NK k ->
                                               Parser e (OperatorType k e)
                                      inner :: forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner = ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    forall e (k :: NotationKind).
    IsExpr e =>
    ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    opP ParseSections
    parseSections (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pTop InternalParsers e
    p) NewNotation
    n
                                  in
                                  case [GenPart] -> NotationKind
    notationKind (NewNotation -> [GenPart]
    notation NewNotation
    n) of
                                    NotationKind
    InfixNotation ->
                                      ((MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> MaybePlaceholder e -> e
    forall a b. (a -> b) -> a -> b
    ($) (MaybePlaceholder e
     -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e
     -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((MaybePlaceholder e -> MaybePlaceholder e -> e)
          -> MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    Beginning
                                               Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((MaybePlaceholder e -> MaybePlaceholder e -> e)
       -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'InfixNotation
    In
                                               Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    End
                                    NotationKind
    PrefixNotation ->
                                      NK 'PrefixNotation -> Parser e (OperatorType 'PrefixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'PrefixNotation
    Pre Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    End
                                    NotationKind
    PostfixNotation ->
                                      ((MaybePlaceholder e -> e) -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MaybePlaceholder e -> e) -> MaybePlaceholder e -> e
    forall a b. (a -> b) -> a -> b
    ($) (MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    Beginning
                                               Parser
      MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NK 'PostfixNotation -> Parser e (OperatorType 'PostfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'PostfixNotation
    Post
                                    NotationKind
    NonfixNotation -> NK 'NonfixNotation -> Parser e (OperatorType 'NonfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'NonfixNotation
    Non
                                    NotationKind
    NoNotation     -> Parser e e
    forall a. HasCallStack => a
    __IMPOSSIBLE__) [NotationSection]
    nonWithSections
                  , pAtom :: Parser e e
    pAtom   = (QName -> Bool) -> Parser e e
    forall e. IsExpr e => (QName -> Bool) -> Parser e e
    atomP QName -> Bool
    isAtom
                  }

        -- Andreas, 2020-06-03 #4712
        -- Note: needs Agda to be compiled with DEBUG to print the grammar.
        [Char] -> VerboseLevel -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc [Char]
    "scope.grammar" VerboseLevel
    10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $
          Doc
    "Operator grammar:" Doc -> Doc -> Doc
    $$ VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Parser e e -> Doc
    forall tok a. Parser tok a -> Doc
    grammar (InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pTop InternalParsers e
    g))

        Parsers e -> ScopeM (Parsers e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Parsers e -> ScopeM (Parsers e))
    -> Parsers e -> ScopeM (Parsers e)
    forall a b. (a -> b) -> a -> b
    $ Parsers :: forall e.
    ([e] -> [e])
    -> ([e] -> [[NamedArg e]])
    -> [NotationSection]
    -> FlatScope
    -> Parsers e
    Parsers
          { parser :: [e] -> [e]
    parser         = (ParseSections, Parser e e) -> [e] -> [e]
    forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
    parse (ParseSections
    parseSections, InternalParsers e -> Parser e e
    forall e. InternalParsers e -> Parser e e
    pTop  InternalParsers e
    g)
          , argsParser :: [e] -> [[NamedArg e]]
    argsParser     = (ParseSections, Parser e [NamedArg e]) -> [e] -> [[NamedArg e]]
    forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
    parse (ParseSections
    parseSections, InternalParsers e -> Parser e [NamedArg e]
    forall e. InternalParsers e -> Parser e [NamedArg e]
    pArgs InternalParsers e
    g)
          , operators :: [NotationSection]
    operators      = [NotationSection]
    everything
          , flattenedScope :: FlatScope
    flattenedScope = FlatScope
    flat
          }
        where
            level :: NewNotation -> FixityLevel
            level :: NewNotation -> FixityLevel
    level = Fixity -> FixityLevel
    fixityLevel (Fixity -> FixityLevel)
    -> (NewNotation -> Fixity) -> NewNotation -> FixityLevel
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Fixity
    notaFixity

            nonfix, isinfix, isprefix, ispostfix :: NewNotation -> Bool
            nonfix :: NewNotation -> Bool
    nonfix    = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    NonfixNotation)  (NotationKind -> Bool)
    -> (NewNotation -> NotationKind) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [GenPart] -> NotationKind
    notationKind ([GenPart] -> NotationKind)
    -> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [GenPart]
    notation
            isinfix :: NewNotation -> Bool
    isinfix   = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    InfixNotation)   (NotationKind -> Bool)
    -> (NewNotation -> NotationKind) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [GenPart] -> NotationKind
    notationKind ([GenPart] -> NotationKind)
    -> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [GenPart]
    notation
            isprefix :: NewNotation -> Bool
    isprefix  = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    PrefixNotation)  (NotationKind -> Bool)
    -> (NewNotation -> NotationKind) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [GenPart] -> NotationKind
    notationKind ([GenPart] -> NotationKind)
    -> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [GenPart]
    notation
            ispostfix :: NewNotation -> Bool
    ispostfix = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    PostfixNotation) (NotationKind -> Bool)
    -> (NewNotation -> NotationKind) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [GenPart] -> NotationKind
    notationKind ([GenPart] -> NotationKind)
    -> (NewNotation -> [GenPart]) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> [GenPart]
    notation

            isPrefix, isPostfix :: NotationSection -> Bool
            isPrefix :: NotationSection -> Bool
    isPrefix  = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    PrefixNotation)  (NotationKind -> Bool)
    -> (NotationSection -> NotationKind) -> NotationSection -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NotationSection -> NotationKind
    sectKind
            isPostfix :: NotationSection -> Bool
    isPostfix = (NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    PostfixNotation) (NotationKind -> Bool)
    -> (NotationSection -> NotationKind) -> NotationSection -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NotationSection -> NotationKind
    sectKind

            isInfix :: Associativity -> NotationSection -> Bool
            isInfix :: Associativity -> NotationSection -> Bool
    isInfix Associativity
    ass NotationSection
    s =
              NotationSection -> NotationKind
    sectKind NotationSection
    s NotationKind -> NotationKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == NotationKind
    InfixNotation
                 Bool -> Bool -> Bool
    &&
              Fixity -> Associativity
    fixityAssoc (NewNotation -> Fixity
    notaFixity (NotationSection -> NewNotation
    sectNotation NotationSection
    s)) Associativity -> Associativity -> Bool
    forall a. Eq a => a -> a -> Bool
    == Associativity
    ass

            mkP :: PrecedenceKey  -- Memoisation key.
                -> ParseSections
                -> Parser e e
                -> [NotationSection]
                -> Parser e e  -- A parser for an expression of higher precedence.
                -> Bool  -- Include the \"expression of higher precedence\"
                         -- parser as one of the choices?
                -> Parser e e
            mkP :: PrecedenceKey
    -> ParseSections
    -> Parser e e
    -> [NotationSection]
    -> Parser e e
    -> Bool
    -> Parser e e
    mkP PrecedenceKey
    key ParseSections
    parseSections Parser e e
    p0 [NotationSection]
    ops Parser e e
    higher Bool
    includeHigher =
                MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise (PrecedenceKey -> MemoKey
    NodeK PrecedenceKey
    key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                  [Parser e e] -> Parser e e
    forall (t :: * -> *) (f :: * -> *) a.
    (Foldable t, Alternative f) =>
    t (f a) -> f a
    Fold.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                    (if Bool
    includeHigher then (Parser e e
    higher Parser e e -> [Parser e e] -> [Parser e e]
    forall a. a -> [a] -> [a]
    :) else [Parser e e] -> [Parser e e]
    forall a. a -> a
    id) ([Parser e e] -> [Parser e e]) -> [Parser e e] -> [Parser e e]
    forall a b. (a -> b) -> a -> b
    $
                    [Maybe (Parser e e)] -> [Parser e e]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe (Parser e e)
    nonAssoc, Maybe (Parser e e)
    preRights, Maybe (Parser e e)
    postLefts]
                where
                choice :: forall k.
                          NK k -> [NotationSection] ->
                          Parser e (OperatorType k e)
                choice :: forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK k
    k =
                  [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
    -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
    forall (t :: * -> *) (f :: * -> *) a.
    (Foldable t, Alternative f) =>
    t (f a) -> f a
    Fold.asum ([Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
     -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e))
    -> ([NotationSection]
        -> [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)])
    -> [NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                  (NotationSection
     -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e))
    -> [NotationSection]
    -> [Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NotationSection
    sect ->
                    let n :: NewNotation
    n = NotationSection -> NewNotation
    sectNotation NotationSection
    sect

                        inner :: forall k.
                                 NK k -> Parser e (OperatorType k e)
                        inner :: forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner = ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    forall e (k :: NotationKind).
    IsExpr e =>
    ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    opP ParseSections
    parseSections Parser e e
    p0 NewNotation
    n
                    in
                    case NK k
    k of
                      NK k
    In   -> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'InfixNotation
    In

                      NK k
    Pre  -> if NewNotation -> Bool
    isinfix NewNotation
    n Bool -> Bool -> Bool
    || NewNotation -> Bool
    ispostfix NewNotation
    n
                              then ((MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> MaybePlaceholder e -> e
    forall a b. (a -> b) -> a -> b
    ($) (MaybePlaceholder e
     -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e
     -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((MaybePlaceholder e -> MaybePlaceholder e -> e)
          -> MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    Beginning
                                            Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((MaybePlaceholder e -> MaybePlaceholder e -> e)
       -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'InfixNotation
    In
                              else NK 'PrefixNotation -> Parser e (OperatorType 'PrefixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'PrefixNotation
    Pre

                      NK k
    Post -> if NewNotation -> Bool
    isinfix NewNotation
    n Bool -> Bool -> Bool
    || NewNotation -> Bool
    isprefix NewNotation
    n
                              then (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> MaybePlaceholder e -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NK 'InfixNotation -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'InfixNotation
    In
                                        Parser
      MemoKey
      e
      (MaybePlaceholder e)
      (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> PositionInName
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    End
                              else NK 'PostfixNotation -> Parser e (OperatorType 'PostfixNotation e)
    forall (k :: NotationKind). NK k -> Parser e (OperatorType k e)
    inner NK 'PostfixNotation
    Post

                      NK k
    Non  -> Parser MemoKey e (MaybePlaceholder e) (OperatorType k e)
    forall a. HasCallStack => a
    __IMPOSSIBLE__)

                nonAssoc :: Maybe (Parser e e)
                nonAssoc :: Maybe (Parser e e)
    nonAssoc = case (NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Associativity -> NotationSection -> Bool
    isInfix Associativity
    NonAssoc) [NotationSection]
    ops of
                  []  -> Maybe (Parser e e)
    forall a. Maybe a
    Nothing
                  [NotationSection]
    ops -> Parser e e -> Maybe (Parser e e)
    forall a. a -> Maybe a
    Just (Parser e e -> Maybe (Parser e e))
    -> Parser e e -> Maybe (Parser e e)
    forall a b. (a -> b) -> a -> b
    $
                    (\e
    x MaybePlaceholder e -> MaybePlaceholder e -> e
    f e
    y -> MaybePlaceholder e -> MaybePlaceholder e -> e
    f (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder e
    x) (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder e
    y))
                      (e -> (MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
    -> Parser e e
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    higher
                      Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((MaybePlaceholder e -> MaybePlaceholder e -> e) -> e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NK 'InfixNotation
    -> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK 'InfixNotation
    In [NotationSection]
    ops
                      Parser MemoKey e (MaybePlaceholder e) (e -> e)
    -> Parser e e -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Parser e e
    higher

                or :: ([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
    or [a] -> f a
    p1 []   [a] -> f a
    p2 []   = Maybe (f a)
    forall a. Maybe a
    Nothing
                or [a] -> f a
    p1 []   [a] -> f a
    p2 [a]
    ops2 = f a -> Maybe (f a)
    forall a. a -> Maybe a
    Just ([a] -> f a
    p2 [a]
    ops2)
                or [a] -> f a
    p1 [a]
    ops1 [a] -> f a
    p2 []   = f a -> Maybe (f a)
    forall a. a -> Maybe a
    Just ([a] -> f a
    p1 [a]
    ops1)
                or [a] -> f a
    p1 [a]
    ops1 [a] -> f a
    p2 [a]
    ops2 = f a -> Maybe (f a)
    forall a. a -> Maybe a
    Just ([a] -> f a
    p1 [a]
    ops1 f a -> f a -> f a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> [a] -> f a
    p2 [a]
    ops2)

                preRight :: Maybe (Parser e (MaybePlaceholder e -> e))
                preRight :: Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    preRight =
                  ([NotationSection]
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> ([NotationSection]
        -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> Maybe
         (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    forall {f :: * -> *} {a} {a} {a}.
    Alternative f =>
    ([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
    or (NK 'PrefixNotation
    -> [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
    forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK 'PrefixNotation
    Pre)
                     ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
    forall a. (a -> Bool) -> [a] -> [a]
    filter NotationSection -> Bool
    isPrefix [NotationSection]
    ops)
                     (\[NotationSection]
    ops -> ((MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e
    -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> MaybePlaceholder e -> e
    forall a b. (a -> b) -> a -> b
    ($) (MaybePlaceholder e
     -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e
     -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((MaybePlaceholder e -> MaybePlaceholder e -> e)
          -> MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> MaybePlaceholder e)
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    higher)
                                       Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((MaybePlaceholder e -> MaybePlaceholder e -> e)
       -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NK 'InfixNotation
    -> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK 'InfixNotation
    In [NotationSection]
    ops)
                     ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Associativity -> NotationSection -> Bool
    isInfix Associativity
    RightAssoc) [NotationSection]
    ops)

                preRights :: Maybe (Parser e e)
                preRights :: Maybe (Parser e e)
    preRights = do
                  Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    preRight <- Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    preRight
                  Parser e e -> Maybe (Parser e e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Parser e e -> Maybe (Parser e e))
    -> Parser e e -> Maybe (Parser e e)
    forall a b. (a -> b) -> a -> b
    $ (Parser e e -> Parser e e) -> Parser e e
    forall a. (a -> a) -> a
    Data.Function.fix ((Parser e e -> Parser e e) -> Parser e e)
    -> (Parser e e -> Parser e e) -> Parser e e
    forall a b. (a -> b) -> a -> b
    $ \Parser e e
    preRights ->
                    MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoiseIfPrinting (PrecedenceKey -> MemoKey
    PreRightsK PrecedenceKey
    key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                      Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    preRight Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> MaybePlaceholder e)
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Parser e e
    preRights Parser e e -> Parser e e -> Parser e e
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Parser e e
    higher))

                postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
                postLeft :: Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    postLeft =
                  ([NotationSection]
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> ([NotationSection]
        -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> Maybe
         (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    forall {f :: * -> *} {a} {a} {a}.
    Alternative f =>
    ([a] -> f a) -> [a] -> ([a] -> f a) -> [a] -> Maybe (f a)
    or (NK 'PostfixNotation
    -> [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
    forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK 'PostfixNotation
    Post)
                     ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
    forall a. (a -> Bool) -> [a] -> [a]
    filter NotationSection -> Bool
    isPostfix [NotationSection]
    ops)
                     (\[NotationSection]
    ops -> (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> MaybePlaceholder e -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((MaybePlaceholder e -> MaybePlaceholder e -> e)
     -> MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NK 'InfixNotation
    -> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    forall (k :: NotationKind).
    NK k -> [NotationSection] -> Parser e (OperatorType k e)
    choice NK 'InfixNotation
    In [NotationSection]
    ops
                                   Parser
      MemoKey
      e
      (MaybePlaceholder e)
      (MaybePlaceholder e -> MaybePlaceholder e -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> MaybePlaceholder e)
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    higher))
                     ((NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Associativity -> NotationSection -> Bool
    isInfix Associativity
    LeftAssoc) [NotationSection]
    ops)

                postLefts :: Maybe (Parser e e)
                postLefts :: Maybe (Parser e e)
    postLefts = do
                  Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    postLeft <- Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    postLeft
                  Parser e e -> Maybe (Parser e e)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Parser e e -> Maybe (Parser e e))
    -> Parser e e -> Maybe (Parser e e)
    forall a b. (a -> b) -> a -> b
    $ (Parser e e -> Parser e e) -> Parser e e
    forall a. (a -> a) -> a
    Data.Function.fix ((Parser e e -> Parser e e) -> Parser e e)
    -> (Parser e e -> Parser e e) -> Parser e e
    forall a b. (a -> b) -> a -> b
    $ \Parser e e
    postLefts ->
                    MemoKey -> Parser e e -> Parser e e
    forall tok. MemoKey -> Parser tok tok -> Parser tok tok
    memoise (PrecedenceKey -> MemoKey
    PostLeftsK PrecedenceKey
    key) (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                      ((MaybePlaceholder e -> e) -> MaybePlaceholder e -> e)
    -> MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (MaybePlaceholder e -> e) -> MaybePlaceholder e -> e
    forall a b. (a -> b) -> a -> b
    ($) (MaybePlaceholder e -> (MaybePlaceholder e -> e) -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> MaybePlaceholder e)
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Parser e e
    postLefts Parser e e -> Parser e e -> Parser e e
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> Parser e e
    higher))
                               Parser
      MemoKey e (MaybePlaceholder e) ((MaybePlaceholder e -> e) -> e)
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    -> Parser e e
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    postLeft

    ---------------------------------------------------------------------------
    -- * Parse functions
    ---------------------------------------------------------------------------

    -- | Returns the list of possible parses.
    parsePat
      :: ([Pattern] -> [Pattern]) -- ^ Turns a 'RawAppP' into possible parses.
      -> Pattern                  -- ^ Pattern possibly containing 'RawAppP's.
      -> [Pattern]                -- ^ Possible parses, not containing 'RawAppP's.
    parsePat :: ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs = \case
        AppP Pattern
    p (Arg ArgInfo
    info Named_ Pattern
    q) ->
            Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> Arg (Named_ Pattern) -> Pattern
    AppP (Pattern -> Arg (Named_ Pattern) -> Pattern)
    -> [Pattern] -> [Arg (Named_ Pattern) -> Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs Pattern
    p [Arg (Named_ Pattern) -> Pattern]
    -> [Arg (Named_ Pattern)] -> [Pattern]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (ArgInfo -> Named_ Pattern -> Arg (Named_ Pattern)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Named_ Pattern -> Arg (Named_ Pattern))
    -> [Named_ Pattern] -> [Arg (Named_ Pattern)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs) Named_ Pattern
    q))
        RawAppP Range
    _ List2 Pattern
    ps     -> Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs (Pattern -> [Pattern]) -> [Pattern] -> [Pattern]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Pattern] -> [Pattern]
    prs (List2 Pattern -> [Item (List2 Pattern)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 Pattern
    ps))
        OpAppP Range
    r QName
    d Set Name
    ns [Arg (Named_ Pattern)]
    ps -> Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen' (Pattern -> Pattern)
    -> ([Arg (Named_ Pattern)] -> Pattern)
    -> [Arg (Named_ Pattern)]
    -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range -> QName -> Set Name -> [Arg (Named_ Pattern)] -> Pattern
    OpAppP Range
    r QName
    d Set Name
    ns ([Arg (Named_ Pattern)] -> Pattern)
    -> [[Arg (Named_ Pattern)]] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
    -> [Arg (Named_ Pattern)] -> [[Arg (Named_ Pattern)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
     -> [Arg (Named_ Pattern)] -> [[Arg (Named_ Pattern)]])
    -> ((Pattern -> [Pattern])
        -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
    -> (Pattern -> [Pattern])
    -> [Arg (Named_ Pattern)]
    -> [[Arg (Named_ Pattern)]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named_ Pattern -> [Named_ Pattern])
    -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Named_ Pattern -> [Named_ Pattern])
     -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
    -> ((Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern])
    -> (Pattern -> [Pattern])
    -> Arg (Named_ Pattern)
    -> [Arg (Named_ Pattern)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> [Pattern]) -> Named_ Pattern -> [Named_ Pattern]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse) (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs) [Arg (Named_ Pattern)]
    ps
        HiddenP Range
    _ Named_ Pattern
    _      -> [Char] -> [Pattern]
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail [Char]
    "bad hidden argument"
        InstanceP Range
    _ Named_ Pattern
    _    -> [Char] -> [Pattern]
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail [Char]
    "bad instance argument"
        AsP Range
    r Name
    x Pattern
    p        -> Range -> Name -> Pattern -> Pattern
    AsP Range
    r Name
    x (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs Pattern
    p
        p :: Pattern
    p@DotP{}         -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        ParenP Range
    r Pattern
    p       -> Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen' (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs Pattern
    p
        p :: Pattern
    p@WildP{}        -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@AbsurdP{}      -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@LitP{}         -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@QuoteP{}       -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@IdentP{}       -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        RecP Range
    r [FieldAssignment' Pattern]
    fs        -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP Range
    r ([FieldAssignment' Pattern] -> Pattern)
    -> [[FieldAssignment' Pattern]] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FieldAssignment' Pattern -> [FieldAssignment' Pattern])
    -> [FieldAssignment' Pattern] -> [[FieldAssignment' Pattern]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Pattern -> [Pattern])
    -> FieldAssignment' Pattern -> [FieldAssignment' Pattern]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs)) [FieldAssignment' Pattern]
    fs
        p :: Pattern
    p@EqualP{}       -> Pattern -> [Pattern]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p -- Andrea: cargo culted from DotP
        EllipsisP Range
    r Maybe Pattern
    mp   -> Maybe Pattern -> [Pattern] -> (Pattern -> [Pattern]) -> [Pattern]
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Pattern
    mp ([Char] -> [Pattern]
    forall (m :: * -> *) a. MonadFail m => [Char] -> m a
    fail [Char]
    "bad ellipsis") ((Pattern -> [Pattern]) -> [Pattern])
    -> (Pattern -> [Pattern]) -> [Pattern]
    forall a b. (a -> b) -> a -> b
    $ \Pattern
    p ->
                              Range -> Maybe Pattern -> Pattern
    EllipsisP Range
    r (Maybe Pattern -> Pattern)
    -> (Pattern -> Maybe Pattern) -> Pattern -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs Pattern
    p
        WithP Range
    r Pattern
    p        -> Range -> Pattern -> Pattern
    WithP Range
    r (Pattern -> Pattern) -> [Pattern] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat [Pattern] -> [Pattern]
    prs Pattern
    p

    {- Implement parsing of copattern left hand sides, e.g.

      record Tree (A : Set) : Set where
        field
          label : A
          child : Bool -> Tree A

      -- corecursive function defined by copattern matching
      alternate : {A : Set}(a b : A) -> Tree A
      -- shallow copatterns
             label (alternate a b)              = a
             child (alternate a b) True         = alternate b a
      -- deep copatterns:
      label (child (alternate a b) False)       = b
      child (child (alternate a b) False) True  = alternate a b
      child (child (alternate a b) False) False = alternate a b

      Delivers an infinite tree

                       a
                  b        b
                a   a    a   a
               b b b b  b b b b
                     ...

      Each lhs is a pattern tree with a distinct path of destructors
      ("child", "label") from the root to the defined symbol ("alternate").
      All branches besides this distinct path are patterns.

      Syntax.Concrete.LHSCore represents a lhs
       - the destructor path
       - the side patterns
       - the defined function symbol
       - the applied patterns
    -}

    -- | The result of 'parseLHS'.
    data ParseLHS
      = ParsePattern Pattern    -- ^ We parsed a pattern.
      | ParseLHS QName LHSCore  -- ^ We parsed a lhs.

    instance Pretty ParseLHS where
      pretty :: ParseLHS -> Doc
    pretty = \case
        ParsePattern Pattern
    p  -> Pattern -> Doc
    forall a. Pretty a => a -> Doc
    pretty Pattern
    p
        ParseLHS QName
    _f LHSCore
    lhs -> LHSCore -> Doc
    forall a. Pretty a => a -> Doc
    pretty LHSCore
    lhs

    -- | Parses a left-hand side, workhorse for 'parseLHS'.
    --
    parseLHS'
      :: LHSOrPatSyn
           -- ^ Are we trying to parse a lhs or a pattern synonym?
           --   For error reporting only!
      -> Maybe QName
           -- ^ Name of the function/patSyn definition if we parse a lhs.
           --   'Nothing' if we parse a pattern.
      -> Pattern
           -- ^ Thing to parse.
      -> ScopeM (ParseLHS, [NotationSection])
           -- ^ The returned list contains all operators/notations/sections that
           -- were used to generate the grammar.

    parseLHS' :: LHSOrPatSyn
    -> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' LHSOrPatSyn
    IsLHS (Just QName
    qn) WildP{} =
        (ParseLHS, [NotationSection])
    -> ScopeM (ParseLHS, [NotationSection])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> LHSCore -> ParseLHS
    ParseLHS QName
    qn (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
    forall a b. (a -> b) -> a -> b
    $ QName -> [Arg (Named_ Pattern)] -> LHSCore
    LHSHead QName
    qn [], [])

    parseLHS' LHSOrPatSyn
    lhsOrPatSyn Maybe QName
    top Pattern
    p = do

        -- Build parser.
        Parsers Pattern
    patP <- ExprKind -> [QName] -> ScopeM (Parsers Pattern)
    forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    IsPattern (Pattern -> [QName]
    forall p. CPatternLike p => p -> [QName]
    patternQNames Pattern
    p)

        -- Run parser, forcing result.
        let ps :: [Pattern]
    ps   = let result :: [Pattern]
    result = ([Pattern] -> [Pattern]) -> Pattern -> [Pattern]
    parsePat (Parsers Pattern -> [Pattern] -> [Pattern]
    forall e. Parsers e -> [e] -> [e]
    parser Parsers Pattern
    patP) Pattern
    p
                   in  (Pattern -> () -> ()) -> () -> [Pattern] -> ()
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Pattern -> () -> ()
    seq () [Pattern]
    result () -> [Pattern] -> [Pattern]
    `seq` [Pattern]
    result

        -- Classify parse results.
        let cons :: [QName]
    cons = KindsOfNames -> FlatScope -> [QName]
    getNames ([KindOfName] -> KindsOfNames
    someKindsOfNames [KindOfName
    ConName, KindOfName
    CoConName, KindOfName
    PatternSynName])
                            (Parsers Pattern -> FlatScope
    forall e. Parsers e -> FlatScope
    flattenedScope Parsers Pattern
    patP)
        let flds :: [QName]
    flds = KindsOfNames -> FlatScope -> [QName]
    getNames ([KindOfName] -> KindsOfNames
    someKindsOfNames [KindOfName
    FldName])
                            (Parsers Pattern -> FlatScope
    forall e. Parsers e -> FlatScope
    flattenedScope Parsers Pattern
    patP)
        let conf :: PatternCheckConfig
    conf = Maybe QName
    -> (QName -> Bool) -> (QName -> Bool) -> PatternCheckConfig
    PatternCheckConfig Maybe QName
    top ([QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [QName]
    cons) ([QName] -> QName -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [QName]
    flds)

        let ([Maybe Pattern]
    errs, [(Pattern, ParseLHS)]
    results) = [Either (Maybe Pattern) (Pattern, ParseLHS)]
    -> ([Maybe Pattern], [(Pattern, ParseLHS)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either (Maybe Pattern) (Pattern, ParseLHS)]
     -> ([Maybe Pattern], [(Pattern, ParseLHS)]))
    -> [Either (Maybe Pattern) (Pattern, ParseLHS)]
    -> ([Maybe Pattern], [(Pattern, ParseLHS)])
    forall a b. (a -> b) -> a -> b
    $ (Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS))
    -> [Pattern] -> [Either (Maybe Pattern) (Pattern, ParseLHS)]
    forall a b. (a -> b) -> [a] -> [b]
    map (PatternCheckConfig
    -> Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
    validPattern PatternCheckConfig
    conf) [Pattern]
    ps
        [Char] -> VerboseLevel -> Doc -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> VerboseLevel -> a -> m ()
    reportS [Char]
    "scope.operators" VerboseLevel
    60 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [ Doc
    "Possible parses for lhs:" ] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ ((Pattern, ParseLHS) -> Doc) -> [(Pattern, ParseLHS)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (VerboseLevel -> Doc -> Doc
    nest VerboseLevel
    2 (Doc -> Doc)
    -> ((Pattern, ParseLHS) -> Doc) -> (Pattern, ParseLHS) -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseLHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty (ParseLHS -> Doc)
    -> ((Pattern, ParseLHS) -> ParseLHS) -> (Pattern, ParseLHS) -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern, ParseLHS) -> ParseLHS
    forall a b. (a, b) -> b
    snd) [(Pattern, ParseLHS)]
    results
        case [(Pattern, ParseLHS)]
    results of
            -- Unique result.
            [(Pattern
    _,ParseLHS
    lhs)] -> do [Char] -> VerboseLevel -> Doc -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    [Char] -> VerboseLevel -> a -> m ()
    reportS [Char]
    "scope.operators" VerboseLevel
    50 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Parsed lhs:" Doc -> Doc -> Doc
    <+> ParseLHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty ParseLHS
    lhs
                            (ParseLHS, [NotationSection])
    -> ScopeM (ParseLHS, [NotationSection])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseLHS
    lhs, Parsers Pattern -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Pattern
    patP)
            -- No result.
            []        -> TypeError -> ScopeM (ParseLHS, [NotationSection])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM (ParseLHS, [NotationSection]))
    -> TypeError -> ScopeM (ParseLHS, [NotationSection])
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Pattern -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Pattern
    patP)
                                   (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
    NoParseForLHS LHSOrPatSyn
    lhsOrPatSyn ([Maybe Pattern] -> [Pattern]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe Pattern]
    errs) Pattern
    p
            -- Ambiguous result.
            [(Pattern, ParseLHS)]
    rs        -> TypeError -> ScopeM (ParseLHS, [NotationSection])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM (ParseLHS, [NotationSection]))
    -> TypeError -> ScopeM (ParseLHS, [NotationSection])
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Pattern -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Pattern
    patP)
                                   (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ LHSOrPatSyn -> Pattern -> [Pattern] -> TypeError
    AmbiguousParseForLHS LHSOrPatSyn
    lhsOrPatSyn Pattern
    p ([Pattern] -> TypeError) -> [Pattern] -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                           ((Pattern, ParseLHS) -> Pattern)
    -> [(Pattern, ParseLHS)] -> [Pattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen (Pattern -> Pattern)
    -> ((Pattern, ParseLHS) -> Pattern)
    -> (Pattern, ParseLHS)
    -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern, ParseLHS) -> Pattern
    forall a b. (a, b) -> a
    fst) [(Pattern, ParseLHS)]
    rs
        where
            getNames :: KindsOfNames -> FlatScope -> [QName]
    getNames KindsOfNames
    kinds FlatScope
    flat =
              ([NewNotation] -> QName) -> [[NewNotation]] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (NewNotation -> QName
    notaName (NewNotation -> QName)
    -> ([NewNotation] -> NewNotation) -> [NewNotation] -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [NewNotation] -> NewNotation
    forall a. [a] -> a
    head) ([[NewNotation]] -> [QName]) -> [[NewNotation]] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ KindsOfNames -> FlatScope -> [[NewNotation]]
    getDefinedNames KindsOfNames
    kinds FlatScope
    flat

            -- The pattern is retained for error reporting in case of ambiguous parses.
            validPattern :: PatternCheckConfig -> Pattern -> PM (Pattern, ParseLHS)
            validPattern :: PatternCheckConfig
    -> Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
    validPattern PatternCheckConfig
    conf Pattern
    p = do
              ParseLHS
    res <- PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern PatternCheckConfig
    conf Pattern
    p
              case (ParseLHS
    res, Maybe QName
    top) of
                (ParsePattern{}, Maybe QName
    Nothing) -> (Pattern, ParseLHS) -> Either (Maybe Pattern) (Pattern, ParseLHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern
    p, ParseLHS
    res)  -- expect pattern
                (ParseLHS{}    , Just{} ) -> (Pattern, ParseLHS) -> Either (Maybe Pattern) (Pattern, ParseLHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern
    p, ParseLHS
    res)  -- expect lhs
                (ParseLHS, Maybe QName)
    _ -> Maybe Pattern -> Either (Maybe Pattern) (Pattern, ParseLHS)
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError Maybe Pattern
    forall a. Maybe a
    Nothing

    -- | Name sets for classifying a pattern.
    data PatternCheckConfig = PatternCheckConfig
      { PatternCheckConfig -> Maybe QName
    topName :: Maybe QName    -- ^ Name of defined symbol.
      , PatternCheckConfig -> QName -> Bool
    conName :: QName -> Bool  -- ^ Valid constructor name?
      , PatternCheckConfig -> QName -> Bool
    fldName :: QName -> Bool  -- ^ Valid field name?
      }

    -- | The monad for pattern checking and classification.
    --
    --   The error message is either empty or a subpattern that was found to be invalid.
    type PM = Either (Maybe Pattern)

    -- | Returns zero or one classified patterns.
    --   In case of zero, return the offending subpattern.
    classifyPattern :: PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern :: PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern PatternCheckConfig
    conf Pattern
    p =
      case Pattern -> List1 (Arg (Named_ Pattern))
    patternAppView Pattern
    p of

        -- case @f ps@
        Arg ArgInfo
    _ (Named Maybe NamedName
    _ (IdentP QName
    x)) :| [Arg (Named_ Pattern)]
    ps | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    x Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatternCheckConfig -> Maybe QName
    topName PatternCheckConfig
    conf -> do
          (Arg (Named_ Pattern) -> Either (Maybe Pattern) ())
    -> [Arg (Named_ Pattern)] -> Either (Maybe Pattern) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Pattern -> Either (Maybe Pattern) ()
    valid (Pattern -> Either (Maybe Pattern) ())
    -> (Arg (Named_ Pattern) -> Pattern)
    -> Arg (Named_ Pattern)
    -> Either (Maybe Pattern) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg) [Arg (Named_ Pattern)]
    ps
          ParseLHS -> PM ParseLHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
    forall a b. (a -> b) -> a -> b
    $ QName -> LHSCore -> ParseLHS
    ParseLHS QName
    x (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
    forall a b. (a -> b) -> a -> b
    $ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
    lhsCoreAddSpine (QName -> [Arg (Named_ Pattern)] -> LHSCore
    LHSHead QName
    x []) [Arg (Named_ Pattern)]
    ps

        -- case @d ps@
        Arg ArgInfo
    _ (Named Maybe NamedName
    _ (IdentP QName
    x)) :| [Arg (Named_ Pattern)]
    ps | PatternCheckConfig -> QName -> Bool
    fldName PatternCheckConfig
    conf QName
    x -> do

          -- Step 1: check for valid copattern lhs.
          [NamedArg ParseLHS]
    ps0 :: [NamedArg ParseLHS] <- (Arg (Named_ Pattern)
     -> Either (Maybe Pattern) (NamedArg ParseLHS))
    -> [Arg (Named_ Pattern)]
    -> Either (Maybe Pattern) [NamedArg ParseLHS]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Arg (Named_ Pattern) -> Either (Maybe Pattern) (NamedArg ParseLHS)
    classPat [Arg (Named_ Pattern)]
    ps
          let ([NamedArg ParseLHS]
    ps1, [NamedArg ParseLHS]
    rest) = (NamedArg ParseLHS -> Bool)
    -> [NamedArg ParseLHS]
    -> ([NamedArg ParseLHS], [NamedArg ParseLHS])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (ParseLHS -> Bool
    isParsePattern (ParseLHS -> Bool)
    -> (NamedArg ParseLHS -> ParseLHS) -> NamedArg ParseLHS -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg ParseLHS -> ParseLHS
    forall a. NamedArg a -> a
    namedArg) [NamedArg ParseLHS]
    ps0
          (NamedArg ParseLHS
    p2, [NamedArg ParseLHS]
    ps3) <- Maybe Pattern
    -> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
    -> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS])
    forall e a. e -> Maybe a -> Either e a
    maybeToEither Maybe Pattern
    forall a. Maybe a
    Nothing (Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
     -> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS]))
    -> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
    -> Either (Maybe Pattern) (NamedArg ParseLHS, [NamedArg ParseLHS])
    forall a b. (a -> b) -> a -> b
    $ [NamedArg ParseLHS]
    -> Maybe (NamedArg ParseLHS, [NamedArg ParseLHS])
    forall a. [a] -> Maybe (a, [a])
    uncons [NamedArg ParseLHS]
    rest
              -- when (null rest): no field pattern or def pattern found

          -- Ensure that the @ps3@ are patterns rather than lhss.
          (NamedArg ParseLHS -> Either (Maybe Pattern) ())
    -> [NamedArg ParseLHS] -> Either (Maybe Pattern) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Maybe Pattern -> Bool -> Either (Maybe Pattern) ()
    forall e (m :: * -> *). MonadError e m => e -> Bool -> m ()
    guardWithError Maybe Pattern
    forall a. Maybe a
    Nothing (Bool -> Either (Maybe Pattern) ())
    -> (NamedArg ParseLHS -> Bool)
    -> NamedArg ParseLHS
    -> Either (Maybe Pattern) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ParseLHS -> Bool
    isParsePattern (ParseLHS -> Bool)
    -> (NamedArg ParseLHS -> ParseLHS) -> NamedArg ParseLHS -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg ParseLHS -> ParseLHS
    forall a. NamedArg a -> a
    namedArg) [NamedArg ParseLHS]
    ps3

          -- Step 2: construct the lhs.
          let (QName
    f, LHSCore
    lhs0)     = ParseLHS -> (QName, LHSCore)
    fromParseLHS (ParseLHS -> (QName, LHSCore)) -> ParseLHS -> (QName, LHSCore)
    forall a b. (a -> b) -> a -> b
    $ NamedArg ParseLHS -> ParseLHS
    forall a. NamedArg a -> a
    namedArg NamedArg ParseLHS
    p2
              lhs :: NamedArg LHSCore
    lhs           = NamedArg ParseLHS -> LHSCore -> NamedArg LHSCore
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg ParseLHS
    p2 LHSCore
    lhs0
              ([Arg (Named_ Pattern)]
    ps', Arg (Named_ Pattern)
    _:[Arg (Named_ Pattern)]
    ps'') = VerboseLevel
    -> [Arg (Named_ Pattern)]
    -> ([Arg (Named_ Pattern)], [Arg (Named_ Pattern)])
    forall a. VerboseLevel -> [a] -> ([a], [a])
    splitAt ([NamedArg ParseLHS] -> VerboseLevel
    forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
    length [NamedArg ParseLHS]
    ps1) [Arg (Named_ Pattern)]
    ps
          ParseLHS -> PM ParseLHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
    forall a b. (a -> b) -> a -> b
    $ QName -> LHSCore -> ParseLHS
    ParseLHS QName
    f (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
    forall a b. (a -> b) -> a -> b
    $ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
    lhsCoreAddSpine (QName
    -> [Arg (Named_ Pattern)]
    -> NamedArg LHSCore
    -> [Arg (Named_ Pattern)]
    -> LHSCore
    LHSProj QName
    x [Arg (Named_ Pattern)]
    ps' NamedArg LHSCore
    lhs []) [Arg (Named_ Pattern)]
    ps''

        -- case @...@
        Arg ArgInfo
    _ (Named Maybe NamedName
    _ (EllipsisP Range
    r (Just Pattern
    p))) :| [Arg (Named_ Pattern)]
    ps -> do
          PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern PatternCheckConfig
    conf Pattern
    p PM ParseLHS -> (ParseLHS -> PM ParseLHS) -> PM ParseLHS
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case  -- TODO: avoid re-parsing
            ParsePattern{}    -> Maybe Pattern -> PM ParseLHS
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError Maybe Pattern
    forall a. Maybe a
    Nothing
            (ParseLHS QName
    f LHSCore
    core) -> do
              (Arg (Named_ Pattern) -> Either (Maybe Pattern) ())
    -> [Arg (Named_ Pattern)] -> Either (Maybe Pattern) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Pattern -> Either (Maybe Pattern) ()
    valid (Pattern -> Either (Maybe Pattern) ())
    -> (Arg (Named_ Pattern) -> Pattern)
    -> Arg (Named_ Pattern)
    -> Either (Maybe Pattern) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg) [Arg (Named_ Pattern)]
    ps
              let ellcore :: LHSCore
    ellcore = Range -> LHSCore -> LHSCore
    LHSEllipsis Range
    r LHSCore
    core
              ParseLHS -> PM ParseLHS
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ParseLHS -> PM ParseLHS) -> ParseLHS -> PM ParseLHS
    forall a b. (a -> b) -> a -> b
    $ QName -> LHSCore -> ParseLHS
    ParseLHS QName
    f (LHSCore -> ParseLHS) -> LHSCore -> ParseLHS
    forall a b. (a -> b) -> a -> b
    $ LHSCore -> [Arg (Named_ Pattern)] -> LHSCore
    lhsCoreAddSpine LHSCore
    ellcore [Arg (Named_ Pattern)]
    ps

        -- case: ordinary pattern
        List1 (Arg (Named_ Pattern))
    _ -> Pattern -> ParseLHS
    ParsePattern Pattern
    p ParseLHS -> Either (Maybe Pattern) () -> PM ParseLHS
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Pattern -> Either (Maybe Pattern) ()
    valid Pattern
    p

      where
      valid :: Pattern -> Either (Maybe Pattern) ()
    valid = (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
    validConPattern ((QName -> Bool) -> Pattern -> Either (Maybe Pattern) ())
    -> (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
    forall a b. (a -> b) -> a -> b
    $ PatternCheckConfig -> QName -> Bool
    conName PatternCheckConfig
    conf

      classPat :: NamedArg Pattern -> PM (NamedArg ParseLHS)
      classPat :: Arg (Named_ Pattern) -> Either (Maybe Pattern) (NamedArg ParseLHS)
    classPat = (Named_ Pattern
     -> Either (Maybe Pattern) (Named NamedName ParseLHS))
    -> Arg (Named_ Pattern)
    -> Either (Maybe Pattern) (NamedArg ParseLHS)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    Trav.mapM ((Pattern -> PM ParseLHS)
    -> Named_ Pattern
    -> Either (Maybe Pattern) (Named NamedName ParseLHS)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    Trav.mapM (PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern PatternCheckConfig
    conf))

      isParsePattern :: ParseLHS -> Bool
    isParsePattern = \case
        ParsePattern{} -> Bool
    True
        ParseLHS{}     -> Bool
    False

      fromParseLHS :: ParseLHS -> (QName, LHSCore)
      fromParseLHS :: ParseLHS -> (QName, LHSCore)
    fromParseLHS = \case
        ParseLHS QName
    f LHSCore
    lhs -> (QName
    f, LHSCore
    lhs)
        ParsePattern{} -> (QName, LHSCore)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Parses a left-hand side, and makes sure that it defined the expected name.
    parseLHS :: QName -> Pattern -> ScopeM LHSCore
    parseLHS :: QName -> Pattern -> ScopeM LHSCore
    parseLHS QName
    top Pattern
    p = ExprKind -> ScopeM LHSCore -> ScopeM LHSCore
    forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    IsPattern (ScopeM LHSCore -> ScopeM LHSCore)
    -> ScopeM LHSCore -> ScopeM LHSCore
    forall a b. (a -> b) -> a -> b
    $ do
      (ParseLHS
    res, [NotationSection]
    ops) <- LHSOrPatSyn
    -> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' LHSOrPatSyn
    IsLHS (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    top) Pattern
    p
      case ParseLHS
    res of
        ParseLHS QName
    f LHSCore
    lhs -> LHSCore -> ScopeM LHSCore
    forall (m :: * -> *) a. Monad m => a -> m a
    return LHSCore
    lhs
        ParseLHS
    _ -> TypeError -> ScopeM LHSCore
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM LHSCore) -> TypeError -> ScopeM LHSCore
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation [NotationSection]
    ops
                       (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
    NoParseForLHS LHSOrPatSyn
    IsLHS [] Pattern
    p

    -- | Parses a pattern.
    parsePattern :: Pattern -> ScopeM Pattern
    parsePattern :: Pattern -> ScopeM Pattern
    parsePattern = LHSOrPatSyn -> Pattern -> ScopeM Pattern
    parsePatternOrSyn LHSOrPatSyn
    IsLHS

    parsePatternSyn :: Pattern -> ScopeM Pattern
    parsePatternSyn :: Pattern -> ScopeM Pattern
    parsePatternSyn = LHSOrPatSyn -> Pattern -> ScopeM Pattern
    parsePatternOrSyn LHSOrPatSyn
    IsPatSyn

    parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
    parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
    parsePatternOrSyn LHSOrPatSyn
    lhsOrPatSyn Pattern
    p = ExprKind -> ScopeM Pattern -> ScopeM Pattern
    forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    IsPattern (ScopeM Pattern -> ScopeM Pattern)
    -> ScopeM Pattern -> ScopeM Pattern
    forall a b. (a -> b) -> a -> b
    $ do
      (ParseLHS
    res, [NotationSection]
    ops) <- LHSOrPatSyn
    -> Maybe QName -> Pattern -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' LHSOrPatSyn
    lhsOrPatSyn Maybe QName
    forall a. Maybe a
    Nothing Pattern
    p
      case ParseLHS
    res of
        ParsePattern Pattern
    p -> Pattern -> ScopeM Pattern
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        ParseLHS
    _ -> TypeError -> ScopeM Pattern
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM Pattern) -> TypeError -> ScopeM Pattern
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation [NotationSection]
    ops
                       (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ LHSOrPatSyn -> [Pattern] -> Pattern -> TypeError
    NoParseForLHS LHSOrPatSyn
    lhsOrPatSyn [] Pattern
    p

    -- | Helper function for 'parseLHS' and 'parsePattern'.
    --
    --   Returns a subpattern that is not a valid constructor pattern
    --   or nothing if the whole pattern is a valid constructor pattern.
    validConPattern
      :: (QName -> Bool)     -- ^ Test for constructor name.
      -> Pattern             -- ^ Supposedly a constructor pattern.
      -> PM ()   -- ^ Offending subpattern or nothing.
    validConPattern :: (QName -> Bool) -> Pattern -> Either (Maybe Pattern) ()
    validConPattern QName -> Bool
    cons = Pattern -> Either (Maybe Pattern) ()
    loop
      where
      loop :: Pattern -> Either (Maybe Pattern) ()
    loop Pattern
    p = case Pattern -> List1 Pattern
    appView Pattern
    p of
          WithP Range
    _ Pattern
    p :| [] -> Pattern -> Either (Maybe Pattern) ()
    loop Pattern
    p
          Pattern
    _ :| []         -> Either (Maybe Pattern) ()
    ok
          IdentP QName
    x :| [Pattern]
    ps
            | QName -> Bool
    cons QName
    x      -> (Pattern -> Either (Maybe Pattern) ())
    -> [Pattern] -> Either (Maybe Pattern) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Pattern -> Either (Maybe Pattern) ()
    loop [Pattern]
    ps
            | Bool
    otherwise   -> Either (Maybe Pattern) ()
    failure
          QuoteP Range
    _ :| [Pattern
    _] -> Either (Maybe Pattern) ()
    ok
          DotP Range
    _ Expr
    e :| [Pattern]
    ps  -> (Pattern -> Either (Maybe Pattern) ())
    -> [Pattern] -> Either (Maybe Pattern) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Pattern -> Either (Maybe Pattern) ()
    loop [Pattern]
    ps
          List1 Pattern
    _               -> Either (Maybe Pattern) ()
    failure
        where
        ok :: Either (Maybe Pattern) ()
    ok      = () -> Either (Maybe Pattern) ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        failure :: Either (Maybe Pattern) ()
    failure = Maybe Pattern -> Either (Maybe Pattern) ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Maybe Pattern -> Either (Maybe Pattern) ())
    -> Maybe Pattern -> Either (Maybe Pattern) ()
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    Just Pattern
    p

    -- | Helper function for 'parseLHS' and 'parsePattern'.
    appView :: Pattern -> List1 Pattern
    appView :: Pattern -> List1 Pattern
    appView = [Pattern] -> Pattern -> List1 Pattern
    loop []
      where
      loop :: [Pattern] -> Pattern -> List1 Pattern
    loop [Pattern]
    acc = \case
        AppP Pattern
    p Arg (Named_ Pattern)
    a         -> [Pattern] -> Pattern -> List1 Pattern
    loop (Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg Arg (Named_ Pattern)
    a Pattern -> [Pattern] -> [Pattern]
    forall a. a -> [a] -> [a]
    : [Pattern]
    acc) Pattern
    p
        OpAppP Range
    _ QName
    op Set Name
    _ [Arg (Named_ Pattern)]
    ps -> (QName -> Pattern
    IdentP QName
    op Pattern -> [Pattern] -> List1 Pattern
    forall a. a -> [a] -> NonEmpty a
    :| (Arg (Named_ Pattern) -> Pattern)
    -> [Arg (Named_ Pattern)] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg [Arg (Named_ Pattern)]
    ps)
                              List1 Pattern -> [Pattern] -> List1 Pattern
    forall a. List1 a -> [a] -> List1 a
    `List1.appendList`
                            [Pattern] -> [Pattern]
    forall a. [a] -> [a]
    reverse [Pattern]
    acc
        ParenP Range
    _ Pattern
    p       -> [Pattern] -> Pattern -> List1 Pattern
    loop [Pattern]
    acc Pattern
    p
        RawAppP Range
    _ List2 Pattern
    _      -> List1 Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        HiddenP Range
    _ Named_ Pattern
    _      -> List1 Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        InstanceP Range
    _ Named_ Pattern
    _    -> List1 Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        p :: Pattern
    p@IdentP{}       -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@WildP{}        -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@AsP{}          -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@AbsurdP{}      -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@LitP{}         -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@QuoteP{}       -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@DotP{}         -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@RecP{}         -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@EqualP{}       -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@EllipsisP{}    -> Pattern -> List1 Pattern
    ret Pattern
    p
        p :: Pattern
    p@WithP{}        -> Pattern -> List1 Pattern
    ret Pattern
    p
       where
       ret :: Pattern -> List1 Pattern
    ret Pattern
    p = Pattern
    p Pattern -> [Pattern] -> List1 Pattern
    forall a. a -> [a] -> NonEmpty a
    :| [Pattern] -> [Pattern]
    forall a. [a] -> [a]
    reverse [Pattern]
    acc

    -- | Return all qualifiers occuring in a list of 'QName's.
    --   Each qualifier is returned as a list of names, e.g.
    --   for @Data.Nat._+_@ we return the list @[Data,Nat]@.
    qualifierModules :: [QName] -> [[Name]]
    qualifierModules :: [QName] -> [[Name]]
    qualifierModules [QName]
    qs =
      ([Name] -> [Name]) -> [[Name]] -> [[Name]]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn [Name] -> [Name]
    forall a. a -> a
    id ([[Name]] -> [[Name]]) -> [[Name]] -> [[Name]]
    forall a b. (a -> b) -> a -> b
    $ ([Name] -> Bool) -> [[Name]] -> [[Name]]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> ([Name] -> Bool) -> [Name] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null) ([[Name]] -> [[Name]]) -> [[Name]] -> [[Name]]
    forall a b. (a -> b) -> a -> b
    $ (QName -> [Name]) -> [QName] -> [[Name]]
    forall a b. (a -> b) -> [a] -> [b]
    map (NonEmpty Name -> [Name]
    forall a. NonEmpty a -> [a]
    List1.init (NonEmpty Name -> [Name])
    -> (QName -> NonEmpty Name) -> QName -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> NonEmpty Name
    qnameParts) [QName]
    qs

    -- | Parse a list of expressions (typically from a 'RawApp') into an application.
    parseApplication :: List2 Expr -> ScopeM Expr
    parseApplication :: List2 Expr -> ScopeM Expr
    parseApplication List2 Expr
    es  = ExprKind -> ScopeM Expr -> ScopeM Expr
    forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    IsExpr (ScopeM Expr -> ScopeM Expr) -> ScopeM Expr -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ do
        let es0 :: [Item (List2 Expr)]
    es0 = List2 Expr -> [Item (List2 Expr)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 Expr
    es
        -- Build the parser
        Parsers Expr
    p <- ExprKind -> [QName] -> ScopeM (Parsers Expr)
    forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    IsExpr [ QName
    q | Ident QName
    q <- [Item (List2 Expr)]
    [Expr]
    es0 ]

        -- Parse
        let result :: [Expr]
    result = Parsers Expr -> [Expr] -> [Expr]
    forall e. Parsers e -> [e] -> [e]
    parser Parsers Expr
    p [Item (List2 Expr)]
    [Expr]
    es0
        case (Expr -> () -> ()) -> () -> [Expr] -> ()
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Expr -> () -> ()
    seq () [Expr]
    result () -> [Expr] -> [Expr]
    `seq` [Expr]
    result of
          [Expr
    e]   -> do
              [Char] -> VerboseLevel -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc [Char]
    "scope.operators" VerboseLevel
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $
                Doc
    "Parsed an operator application:" Doc -> Doc -> Doc
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
              Expr -> ScopeM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e
          []    -> TypeError -> ScopeM Expr
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM Expr) -> TypeError -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Expr -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Expr
    p)
                             (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> TypeError
    NoParseForApplication List2 Expr
    es
          Expr
    e:[Expr]
    es' -> TypeError -> ScopeM Expr
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM Expr) -> TypeError -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Expr -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Expr
    p)
                             (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> List1 Expr -> TypeError
    AmbiguousParseForApplication List2 Expr
    es
                             (List1 Expr -> TypeError) -> List1 Expr -> TypeError
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Expr) -> List1 Expr -> List1 Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Expr -> Expr
    forall e. IsExpr e => e -> e
    fullParen (Expr
    e Expr -> [Expr] -> List1 Expr
    forall a. a -> [a] -> NonEmpty a
    :| [Expr]
    es')

    parseModuleIdentifier :: Expr -> ScopeM QName
    parseModuleIdentifier :: Expr -> ScopeM QName
    parseModuleIdentifier (Ident QName
    m) = QName -> ScopeM QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    m
    parseModuleIdentifier Expr
    e = TypeError -> ScopeM QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM QName) -> TypeError -> ScopeM QName
    forall a b. (a -> b) -> a -> b
    $ Expr -> TypeError
    NotAModuleExpr Expr
    e

    parseRawModuleApplication :: List2 Expr -> ScopeM (QName, [NamedArg Expr])
    parseRawModuleApplication :: List2 Expr -> ScopeM (QName, [NamedArg Expr])
    parseRawModuleApplication es :: List2 Expr
    es@(List2 Expr
    e Expr
    e2 [Expr]
    rest) = ExprKind
    -> ScopeM (QName, [NamedArg Expr])
    -> ScopeM (QName, [NamedArg Expr])
    forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    IsExpr (ScopeM (QName, [NamedArg Expr])
     -> ScopeM (QName, [NamedArg Expr]))
    -> ScopeM (QName, [NamedArg Expr])
    -> ScopeM (QName, [NamedArg Expr])
    forall a b. (a -> b) -> a -> b
    $ do
        let es_args :: [Expr]
    es_args = Expr
    e2Expr -> [Expr] -> [Expr]
    forall a. a -> [a] -> [a]
    :[Expr]
    rest
        QName
    m <- Expr -> ScopeM QName
    parseModuleIdentifier Expr
    e

        -- Build the arguments parser
        Parsers Expr
    p <- ExprKind -> [QName] -> ScopeM (Parsers Expr)
    forall e. IsExpr e => ExprKind -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    IsExpr [ QName
    q | Ident QName
    q <- [Expr]
    es_args ]

        -- Parse
        -- TODO: not sure about forcing
        case {-force $-} Parsers Expr -> [Expr] -> [[NamedArg Expr]]
    forall e. Parsers e -> [e] -> [[NamedArg e]]
    argsParser Parsers Expr
    p [Expr]
    es_args of
            [[NamedArg Expr]
    as] -> (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    m, [NamedArg Expr]
    as)
            []   -> TypeError -> ScopeM (QName, [NamedArg Expr])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM (QName, [NamedArg Expr]))
    -> TypeError -> ScopeM (QName, [NamedArg Expr])
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Expr -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Expr
    p)
                              (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> TypeError
    NoParseForApplication List2 Expr
    es
            [NamedArg Expr]
    as : [[NamedArg Expr]]
    ass -> do
              let f :: [NamedArg Expr] -> Expr
    f = Expr -> Expr
    forall e. IsExpr e => e -> e
    fullParen (Expr -> Expr)
    -> ([NamedArg Expr] -> Expr) -> [NamedArg Expr] -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (Range -> Expr -> NamedArg Expr -> Expr
    App Range
    forall a. Range' a
    noRange) (QName -> Expr
    Ident QName
    m)
              TypeError -> ScopeM (QName, [NamedArg Expr])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM (QName, [NamedArg Expr]))
    -> TypeError -> ScopeM (QName, [NamedArg Expr])
    forall a b. (a -> b) -> a -> b
    $ [NotationSection] -> TypeError -> TypeError
    OperatorInformation (Parsers Expr -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Expr
    p)
                        (TypeError -> TypeError) -> TypeError -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List2 Expr -> List1 Expr -> TypeError
    AmbiguousParseForApplication List2 Expr
    es
                        (List1 Expr -> TypeError) -> List1 Expr -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ([NamedArg Expr] -> Expr) -> NonEmpty [NamedArg Expr] -> List1 Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [NamedArg Expr] -> Expr
    f ([NamedArg Expr]
    as [NamedArg Expr] -> [[NamedArg Expr]] -> NonEmpty [NamedArg Expr]
    forall a. a -> [a] -> NonEmpty a
    :| [[NamedArg Expr]]
    ass)

    -- | Parse an expression into a module application
    --   (an identifier plus a list of arguments).
    parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])
    parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])
    parseModuleApplication (RawApp Range
    _ List2 Expr
    es) = List2 Expr -> ScopeM (QName, [NamedArg Expr])
    parseRawModuleApplication List2 Expr
    es
    parseModuleApplication (App Range
    r Expr
    e1 NamedArg Expr
    e2) = do -- TODO: do we need this case?
        (QName
    m, [NamedArg Expr]
    args) <- Expr -> ScopeM (QName, [NamedArg Expr])
    parseModuleApplication Expr
    e1
        (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    m, [NamedArg Expr]
    args [NamedArg Expr] -> [NamedArg Expr] -> [NamedArg Expr]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg Expr
    e2])
    parseModuleApplication Expr
    e = do
        QName
    m <- Expr -> ScopeM QName
    parseModuleIdentifier Expr
    e
        (QName, [NamedArg Expr]) -> ScopeM (QName, [NamedArg Expr])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    m, [])

    ---------------------------------------------------------------------------
    -- * Inserting parenthesis
    ---------------------------------------------------------------------------

    fullParen :: IsExpr e => e -> e
    fullParen :: forall e. IsExpr e => e -> e
    fullParen e
    e = case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView (e -> ExprView e) -> e -> ExprView e
    forall a b. (a -> b) -> a -> b
    $ e -> e
    forall e. IsExpr e => e -> e
    fullParen' e
    e of
        ParenV e
    e    -> e
    e
        ExprView e
    e'          -> ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView ExprView e
    e'

    fullParen' :: IsExpr e => e -> e
    fullParen' :: forall e. IsExpr e => e -> e
    fullParen' e
    e = case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
        LocalV QName
    _     -> e
    e
        WildV e
    _      -> e
    e
        OtherV e
    _     -> e
    e
        HiddenArgV Named_ e
    _ -> e
    e
        InstanceArgV Named_ e
    _ -> e
    e
        ParenV e
    _     -> e
    e
        AppV e
    e1 (Arg ArgInfo
    info Named_ e
    e2) -> e -> e
    par (e -> e) -> e -> e
    forall a b. (a -> b) -> a -> b
    $ ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView e -> e) -> ExprView e -> e
    forall a b. (a -> b) -> a -> b
    $ e -> Arg (Named_ e) -> ExprView e
    forall e. e -> NamedArg e -> ExprView e
    AppV (e -> e
    forall e. IsExpr e => e -> e
    fullParen' e
    e1) (ArgInfo -> Named_ e -> Arg (Named_ e)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Named_ e
    e2')
            where
                e2' :: Named_ e
    e2' = case ArgInfo -> Hiding
    argInfoHiding ArgInfo
    info of
                    Hiding
    Hidden     -> Named_ e
    e2
                    Instance{} -> Named_ e
    e2
                    Hiding
    NotHidden  -> e -> e
    forall e. IsExpr e => e -> e
    fullParen' (e -> e) -> Named_ e -> Named_ e
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Named_ e
    e2
        OpAppV QName
    x Set Name
    ns OpAppArgs' e
    es -> e -> e
    par (e -> e) -> e -> e
    forall a b. (a -> b) -> a -> b
    $ ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView e -> e) -> ExprView e -> e
    forall a b. (a -> b) -> a -> b
    $ QName -> Set Name -> OpAppArgs' e -> ExprView e
    forall e. QName -> Set Name -> OpAppArgs' e -> ExprView e
    OpAppV QName
    x Set Name
    ns (OpAppArgs' e -> ExprView e) -> OpAppArgs' e -> ExprView e
    forall a b. (a -> b) -> a -> b
    $ ((Arg (Named NamedName (MaybePlaceholder (OpApp e)))
     -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
    -> OpAppArgs' e -> OpAppArgs' e
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Arg (Named NamedName (MaybePlaceholder (OpApp e)))
      -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
     -> OpAppArgs' e -> OpAppArgs' e)
    -> ((e -> e)
        -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
        -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
    -> (e -> e)
    -> OpAppArgs' e
    -> OpAppArgs' e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName (MaybePlaceholder (OpApp e))
     -> Named NamedName (MaybePlaceholder (OpApp e)))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName (MaybePlaceholder (OpApp e))
      -> Named NamedName (MaybePlaceholder (OpApp e)))
     -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
     -> Arg (Named NamedName (MaybePlaceholder (OpApp e))))
    -> ((e -> e)
        -> Named NamedName (MaybePlaceholder (OpApp e))
        -> Named NamedName (MaybePlaceholder (OpApp e)))
    -> (e -> e)
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp e)))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
    -> Named NamedName (MaybePlaceholder (OpApp e))
    -> Named NamedName (MaybePlaceholder (OpApp e))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
     -> Named NamedName (MaybePlaceholder (OpApp e))
     -> Named NamedName (MaybePlaceholder (OpApp e)))
    -> ((e -> e)
        -> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
    -> (e -> e)
    -> Named NamedName (MaybePlaceholder (OpApp e))
    -> Named NamedName (MaybePlaceholder (OpApp e))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (OpApp e -> OpApp e)
    -> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((OpApp e -> OpApp e)
     -> MaybePlaceholder (OpApp e) -> MaybePlaceholder (OpApp e))
    -> ((e -> e) -> OpApp e -> OpApp e)
    -> (e -> e)
    -> MaybePlaceholder (OpApp e)
    -> MaybePlaceholder (OpApp e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (e -> e) -> OpApp e -> OpApp e
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) e -> e
    forall e. IsExpr e => e -> e
    fullParen' OpAppArgs' e
    es
        LamV List1 LamBinding
    bs e
    e -> e -> e
    par (e -> e) -> e -> e
    forall a b. (a -> b) -> a -> b
    $ ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView e -> e) -> ExprView e -> e
    forall a b. (a -> b) -> a -> b
    $ List1 LamBinding -> e -> ExprView e
    forall e. List1 LamBinding -> e -> ExprView e
    LamV List1 LamBinding
    bs (e -> e
    forall e. IsExpr e => e -> e
    fullParen e
    e)
        where
            par :: e -> e
    par = ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView e -> e) -> (e -> ExprView e) -> e -> e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> ExprView e
    forall e. e -> ExprView e
    ParenV