    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE DataKinds #-}

    {-| 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
        , parseArguments
        , parseLHS
        , parsePattern
        , parsePatternSyn
        ) where

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

    import Data.Either (partitionEithers)
    import qualified Data.Function
    import qualified Data.List as List
    import Data.Maybe
    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 Agda.Syntax.Position
    import Agda.Syntax.Notation
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Flat
    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.Function (applyWhen, applyWhenJust)
    import Agda.Utils.Either
    import Agda.Syntax.Common.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
    ---------------------------------------------------------------------------

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

    -- | 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?
      -> Maybe QName
         -- ^ Are we trying to parse the lhs of the function given here?
      -> [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 -> Maybe QName -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    kind Maybe QName
    top [QName]
    exprNames0 = do
        let exprNames :: [QName]
    exprNames = Maybe QName -> (QName -> [QName] -> [QName]) -> [QName] -> [QName]
    forall b a. Maybe b -> (b -> a -> a) -> a -> a
    applyWhenJust Maybe QName
    top (:) [QName]
    exprNames0
        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
        (names, ops0) <- localNames kind top flat
        let ops | ExprKind
    kind ExprKind -> ExprKind -> Bool
    forall a. Eq a => a -> a -> Bool
    == ExprKind
    IsPattern = (NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (NewNotation -> Bool) -> NewNotation -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Bool
    isLambdaNotation) [NewNotation]
    ops0
                | Bool
    otherwise         = [NewNotation]
    ops0

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

            partListsInExpr' = (QName -> [NamePart]) -> [QName] -> [[NamePart]]
    forall a b. (a -> b) -> [a] -> [b]
    map (NameParts -> [Item NameParts]
    NameParts -> [NamePart]
    forall l. IsList l => l -> [Item l]
    List1.toList (NameParts -> [NamePart])
    -> (QName -> NameParts) -> QName -> [NamePart]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> NameParts
    nameParts (Name -> NameParts) -> (QName -> Name) -> QName -> NameParts
    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]
    f =
              ([k] -> Trie k () -> Trie k ()) -> Trie k () -> t [k] -> Trie k ()
    forall a b. (a -> b -> b) -> b -> t a -> b
    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 = ([[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 = ([[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 =
              [RawName] -> Set RawName
    forall a. Ord a => [a] -> Set a
    Set.fromList [ RawName
    s | Id RawName
    s <- [[NamePart]] -> [NamePart]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[NamePart]]
    partListsInExpr' ]

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

            addHole Bool
    True  RawName
    p = [NamePart
    Hole, RawName -> NamePart
    Id RawName
    p]
            addHole Bool
    False RawName
    p = [RawName -> NamePart
    Id RawName
    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
    withHole Notation
    n =
              [NamePart] -> Trie NamePart () -> Bool
    forall k v. Ord k => [k] -> Trie k v -> Bool
    Trie.member (Bool -> RawName -> [NamePart]
    addHole Bool
    withHole RawName
    p) Trie NamePart ()
    partListsInExpr
              where
              p :: RawName
    p = case Notation
    n of
                HolePart{} : IdPart RString
    p : Notation
    _ -> RString -> RawName
    forall a. Ranged a -> a
    rangedThing RString
    p
                IdPart RString
    p : Notation
    _              -> RString -> RawName
    forall a. Ranged a -> a
    rangedThing RString
    p
                Notation
    _                         -> RawName
    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
    withHole Notation
    n =
              [NamePart] -> Trie NamePart () -> Bool
    forall k v. Ord k => [k] -> Trie k v -> Bool
    Trie.member (Bool -> RawName -> [NamePart]
    addHole Bool
    withHole RawName
    p) Trie NamePart ()
    reversedPartListsInExpr
              where
              p :: RawName
    p = case Notation -> Notation
    forall a. [a] -> [a]
    reverse Notation
    n of
                HolePart{} : IdPart RString
    p : Notation
    _ -> RString -> RawName
    forall a. Ranged a -> a
    rangedThing RString
    p
                IdPart RString
    p : Notation
    _              -> RString -> RawName
    forall a. Ranged a -> a
    rangedThing RString
    p
                Notation
    _                         -> RawName
    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
    withInitialHole Bool
    withFinalHole Notation
    n =
              Bool -> Notation -> Bool
    firstPartPresent Bool
    withInitialHole Notation
    n
                Bool -> Bool -> Bool
    &&
              Bool -> Notation -> Bool
    lastPartPresent  Bool
    withFinalHole   Notation
    n

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

            -- Should be used with sections.
            correctUnderscoresSect :: NotationKind -> Notation -> Bool
            correctUnderscoresSect NotationKind
    k Notation
    n = case (NotationKind
    k, Notation -> NotationKind
    notationKind Notation
    n) of
              (NotationKind
    PrefixNotation,  NotationKind
    InfixNotation)   -> Bool -> Bool -> Notation -> Bool
    correctUnderscores Bool
    True Bool
    False Notation
    n
              (NotationKind
    PostfixNotation, NotationKind
    InfixNotation)   -> Bool -> Bool -> Notation -> Bool
    correctUnderscores Bool
    False Bool
    True Notation
    n
              (NotationKind
    NonfixNotation,  NotationKind
    InfixNotation)   -> Bool -> Bool -> Notation -> Bool
    correctUnderscores Bool
    True Bool
    True Notation
    n
              (NotationKind
    NonfixNotation,  NotationKind
    PrefixNotation)  -> Bool -> Bool -> Notation -> Bool
    correctUnderscores Bool
    False Bool
    True Notation
    n
              (NotationKind
    NonfixNotation,  NotationKind
    PostfixNotation) -> Bool -> Bool -> Notation -> Bool
    correctUnderscores Bool
    True Bool
    False Notation
    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.

            (non, fix) = List.partition nonfix (filter (and . partsPresent) ops)

            cons       = KindsOfNames -> FlatScope -> [List1 NewNotation]
    getDefinedNames
                           ([KindOfName] -> KindsOfNames
    someKindsOfNames [KindOfName
    ConName, KindOfName
    CoConName, KindOfName
    FldName, KindOfName
    PatternSynName]) FlatScope
    flat
            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
    $
                           (List1 NewNotation -> QName) -> [List1 NewNotation] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (NewNotation -> QName
    notaName (NewNotation -> QName)
    -> (List1 NewNotation -> NewNotation) -> List1 NewNotation -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 NewNotation -> NewNotation
    forall a. NonEmpty a -> a
    List1.head) [List1 NewNotation]
    cons
            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
    $
                           [List1 NewNotation] -> [NewNotation]
    forall a. [List1 a] -> [a]
    List1.concat [List1 NewNotation]
    cons

            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 -> 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
    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 = case ExprKind
    kind of
              ExprKind
    IsPattern -> ParseSections
    DoNotParseSections
              ExprKind
    IsExpr    -> ParseSections
    ParseSections

        let 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 -> Notation -> Bool
    correctUnderscoresSect NotationKind
    k (NewNotation -> Notation
    notation NewNotation
    n)
                  ]

            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 -> NotationSection)
    -> [NotationSection] -> [NotationSection]
    forall a b. (a -> b) -> [a] -> [b]
    map (\NotationSection
    s -> NotationSection
    s { sectLevel = 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 -> Notation -> Bool
    correctUnderscoresSect NotationKind
    NonfixNotation (NewNotation -> Notation
    notation NewNotation
    n)
                  ]

            -- The triples have the form (level, operators). The lowest
            -- level comes first.
            relatedOperators :: [(PrecedenceLevel, [NotationSection])]
            relatedOperators =
              (NonEmpty (PrecedenceLevel, [NotationSection])
     -> (PrecedenceLevel, [NotationSection]))
    -> [NonEmpty (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)) ([NonEmpty (PrecedenceLevel, [NotationSection])]
     -> [(PrecedenceLevel, [NotationSection])])
    -> ([NewNotation]
        -> [NonEmpty (PrecedenceLevel, [NotationSection])])
    -> [NewNotation]
    -> [(PrecedenceLevel, [NotationSection])]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
              ((PrecedenceLevel, [NotationSection]) -> PrecedenceLevel)
    -> [(PrecedenceLevel, [NotationSection])]
    -> [NonEmpty (PrecedenceLevel, [NotationSection])]
    forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
    List1.groupOn (PrecedenceLevel, [NotationSection]) -> PrecedenceLevel
    forall a b. (a, b) -> a
    fst ([(PrecedenceLevel, [NotationSection])]
     -> [NonEmpty (PrecedenceLevel, [NotationSection])])
    -> ([NewNotation] -> [(PrecedenceLevel, [NotationSection])])
    -> [NewNotation]
    -> [NonEmpty (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 =
              ((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

        reportS "scope.operators" 50
          [ "unrelatedOperators = " ++ prettyShow unrelatedOperators
          , "nonWithSections    = " ++ prettyShow nonWithSections
          , "relatedOperators   = " ++ prettyShow relatedOperators
          ]

        let 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
                  { 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 (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.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 a b. (a -> b -> b) -> b -> [a] -> b
    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 (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.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 MemoKey e (MaybePlaceholder 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 Notation -> NotationKind
    notationKind (NewNotation -> Notation
    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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_PARSING to print the grammar.
        reportSDoc "scope.grammar" 20 $ return $
          "Operator grammar:" $$ nest 2 (grammar (pTop g))

        return $ Parsers
          { parser         = parse (parseSections, pTop  g)
          , argsParser     = parse (parseSections, pArgs g)
          , operators      = everything
          , flattenedScope = 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
    . Notation -> NotationKind
    notationKind (Notation -> NotationKind)
    -> (NewNotation -> Notation) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Notation
    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
    . Notation -> NotationKind
    notationKind (Notation -> NotationKind)
    -> (NewNotation -> Notation) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Notation
    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
    . Notation -> NotationKind
    notationKind (Notation -> NotationKind)
    -> (NewNotation -> Notation) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Notation
    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
    . Notation -> NotationKind
    notationKind (Notation -> NotationKind)
    -> (NewNotation -> Notation) -> NewNotation -> NotationKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NewNotation -> Notation
    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 (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.asum ([Parser e e] -> Parser e e) -> [Parser e e] -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
                    Bool
    -> ([Parser e e] -> [Parser e e]) -> [Parser e e] -> [Parser e e]
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen Bool
    includeHigher (Parser e e
    higher Parser e e -> [Parser e e] -> [Parser e e]
    forall a. a -> [a] -> [a]
    :) ([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
                -- Andreas, 2025-02-27
                -- Break up the choice function into its three cases,
                -- so that matching on @k@ does not have to be performed
                -- inside the mapped function @(\ sect -> ...)@.
                --
                -- choice :: forall k.
                --           NK k -> [NotationSection] ->
                --           Parser e (OperatorType k e)
                -- choice k =
                --   Agda.Utils.List.asum .
                --   map (\sect ->
                --     let n = sectNotation sect

                --         inner :: forall k.
                --                  NK k -> Parser e (OperatorType k e)
                --         inner = opP parseSections p0 n
                --     in
                --     case k of
                --       In   -> inner In

                --       Pre  -> if isinfix n || ispostfix n
                --               then flip ($) <$> placeholder Beginning
                --                             <*> inner In
                --               else inner Pre

                --       Post -> if isinfix n || isprefix n
                --               then flip <$> inner In
                --                         <*> placeholder End
                --               else inner Post

                --       Non  -> __IMPOSSIBLE__)

                choiceIn :: [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
                choiceIn :: [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    choiceIn =
                  [Parser
       MemoKey
       e
       (MaybePlaceholder e)
       (MaybePlaceholder e -> MaybePlaceholder e -> e)]
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    forall (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.asum ([Parser
        MemoKey
        e
        (MaybePlaceholder e)
        (MaybePlaceholder e -> MaybePlaceholder e -> e)]
     -> Parser
          MemoKey
          e
          (MaybePlaceholder e)
          (MaybePlaceholder e -> MaybePlaceholder e -> e))
    -> ([NotationSection]
        -> [Parser
              MemoKey
              e
              (MaybePlaceholder e)
              (MaybePlaceholder e -> MaybePlaceholder e -> e)])
    -> [NotationSection]
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (MaybePlaceholder e -> MaybePlaceholder e -> e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                  (NotationSection
     -> Parser
          MemoKey
          e
          (MaybePlaceholder e)
          (MaybePlaceholder e -> MaybePlaceholder e -> e))
    -> [NotationSection]
    -> [Parser
          MemoKey
          e
          (MaybePlaceholder e)
          (MaybePlaceholder e -> MaybePlaceholder e -> e)]
    forall a b. (a -> b) -> [a] -> [b]
    map \ NotationSection
    sect -> ParseSections
    -> Parser e e
    -> NewNotation
    -> NK 'InfixNotation
    -> Parser e (OperatorType 'InfixNotation 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 (NotationSection -> NewNotation
    sectNotation NotationSection
    sect) NK 'InfixNotation
    In

                choicePre :: [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
                choicePre :: [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
    choicePre =
                  [Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.asum ([Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> ([NotationSection]
        -> [Parser
              MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)])
    -> [NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                  (NotationSection
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> [Parser
          MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
    forall a b. (a -> b) -> [a] -> [b]
    map \ NotationSection
    sect -> do
                    let n :: NewNotation
    n = NotationSection -> NewNotation
    sectNotation NotationSection
    sect
                    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ParseSections
    -> Parser e e
    -> NewNotation
    -> NK 'InfixNotation
    -> Parser e (OperatorType 'InfixNotation 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 NK 'InfixNotation
    In
                    else ParseSections
    -> Parser e e
    -> NewNotation
    -> NK 'PrefixNotation
    -> Parser e (OperatorType 'PrefixNotation 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 NK 'PrefixNotation
    Pre

                choicePost :: [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
                choicePost :: [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
    choicePost =
                  [Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall (m :: * -> *) a. Alternative m => [m a] -> m a
    Agda.Utils.List.asum ([Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> ([NotationSection]
        -> [Parser
              MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)])
    -> [NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                  (NotationSection
     -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    -> [NotationSection]
    -> [Parser
          MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)]
    forall a b. (a -> b) -> [a] -> [b]
    map \ NotationSection
    sect -> do
                    let n :: NewNotation
    n = NotationSection -> NewNotation
    sectNotation NotationSection
    sect
                    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
    <$> ParseSections
    -> Parser e e
    -> NewNotation
    -> NK 'InfixNotation
    -> Parser e (OperatorType 'InfixNotation 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 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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 ParseSections
    -> Parser e e
    -> NewNotation
    -> NK 'PostfixNotation
    -> Parser e (OperatorType 'PostfixNotation 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 NK 'PostfixNotation
    Post

                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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    choiceIn [NotationSection]
    ops
                      Parser MemoKey e (MaybePlaceholder e) (e -> e)
    -> Parser e e -> Parser e e
    forall a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 a. 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 [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
    [NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    choicePre
                     ((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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    choiceIn [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
                  preRight <- Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    preRight
                  return $ Data.Function.fix $ \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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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 a.
    Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) a
    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 [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
    [NotationSection]
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    choicePost
                     ((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
    <$> [NotationSection] -> Parser e (OperatorType 'InfixNotation e)
    choiceIn [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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    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
                  postLeft <- Maybe
      (Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e))
    postLeft
                  return $ Data.Function.fix $ \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 a.
    Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) a
    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 a b.
    Parser MemoKey e (MaybePlaceholder e) (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e -> e)
    postLeft

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

    -- | Parses all 'RawAppP' in the given pattern using the given parser.
    --   Returns the list of possible parses.
    --
    --   Naturally, does not recurse into 'DotP' as this contains no pattern.
    --
    --   Returns the empty list if the given parser does so
    --   or if a 'HiddenP' or 'InstanceP' is encountered.
    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]
    parse = Pattern -> [Pattern]
    loop
      where
      loop :: Pattern -> [Pattern]
    loop = \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]
    loop Pattern
    p [Arg (Named_ Pattern) -> Pattern]
    -> [Arg (Named_ Pattern)] -> [Pattern]
    forall a b. [a -> b] -> [a] -> [b]
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse Pattern -> [Pattern]
    loop 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]
    loop (Pattern -> [Pattern]) -> [Pattern] -> [Pattern]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Pattern] -> [Pattern]
    parse (List2 Pattern -> [Item (List2 Pattern)]
    forall l. IsList l => l -> [Item l]
    List2.toList List2 Pattern
    ps))
        OpAppP Range
    r QName
    d Set1 Name
    ns List1 (Arg (Named_ Pattern))
    ps -> Pattern -> Pattern
    forall e. IsExpr e => e -> e
    fullParen' (Pattern -> Pattern)
    -> (List1 (Arg (Named_ Pattern)) -> Pattern)
    -> List1 (Arg (Named_ Pattern))
    -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Range
    -> QName -> Set1 Name -> List1 (Arg (Named_ Pattern)) -> Pattern
    OpAppP Range
    r QName
    d Set1 Name
    ns (List1 (Arg (Named_ Pattern)) -> Pattern)
    -> [List1 (Arg (Named_ Pattern))] -> [Pattern]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
    -> List1 (Arg (Named_ Pattern)) -> [List1 (Arg (Named_ Pattern))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM ((Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
     -> List1 (Arg (Named_ Pattern)) -> [List1 (Arg (Named_ Pattern))])
    -> ((Pattern -> [Pattern])
        -> Arg (Named_ Pattern) -> [Arg (Named_ Pattern)])
    -> (Pattern -> [Pattern])
    -> List1 (Arg (Named_ Pattern))
    -> [List1 (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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse) Pattern -> [Pattern]
    loop List1 (Arg (Named_ Pattern))
    ps
        HiddenP Range
    _ Named_ Pattern
    _      -> RawName -> [Pattern]
    forall a. RawName -> [a]
    forall (m :: * -> *) a. MonadFail m => RawName -> m a
    fail RawName
    "bad hidden argument"
        InstanceP Range
    _ Named_ Pattern
    _    -> RawName -> [Pattern]
    forall a. RawName -> [a]
    forall (m :: * -> *) a. MonadFail m => RawName -> m a
    fail RawName
    "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]
    loop Pattern
    p
        p :: Pattern
    p@DotP{}         -> Pattern -> [Pattern]
    forall a. a -> [a]
    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]
    loop Pattern
    p
        p :: Pattern
    p@WildP{}        -> Pattern -> [Pattern]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@AbsurdP{}      -> Pattern -> [Pattern]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@LitP{}         -> Pattern -> [Pattern]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@QuoteP{}       -> Pattern -> [Pattern]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        p :: Pattern
    p@IdentP{}       -> Pattern -> [Pattern]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern
    p
        RecP KwRange
    kwr Range
    r [FieldAssignment' Pattern]
    fs    -> KwRange -> Range -> [FieldAssignment' Pattern] -> Pattern
    RecP KwRange
    kwr 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b)
    traverse Pattern -> [Pattern]
    loop) [FieldAssignment' Pattern]
    fs
        p :: Pattern
    p@EqualP{}       -> Pattern -> [Pattern]
    forall a. a -> [a]
    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 (RawName -> [Pattern]
    forall a. RawName -> [a]
    forall (m :: * -> *) a. MonadFail m => RawName -> m a
    fail RawName
    "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]
    loop 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]
    loop 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' ::
         DisplayLHS
           -- ^ Are we parsing a 'DisplayPragma'?
           --   Then defined names are recognized as constructors.
           --
           --   In this case, 'LHSOrPatSyn' is 'IsLHS' and 'Maybe QName' is 'Just'.
      -> 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' :: DisplayLHS
    -> LHSOrPatSyn
    -> Maybe QName
    -> Pattern
    -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' DisplayLHS
    NoDisplayLHS LHSOrPatSyn
    IsLHS (Just QName
    qn) WildP{} =
        (ParseLHS, [NotationSection])
    -> ScopeM (ParseLHS, [NotationSection])
    forall a. a -> TCMT IO a
    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' DisplayLHS
    displayLhs LHSOrPatSyn
    lhsOrPatSyn Maybe QName
    top Pattern
    p = do

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

        -- Run parser, forcing result.
        let 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 a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Pattern -> () -> ()
    forall a b. a -> b -> b
    seq () [Pattern]
    result () -> [Pattern] -> [Pattern]
    forall a b. a -> b -> b
    `seq` [Pattern]
    result

        -- Classify parse results.
        let cons = KindsOfNames -> FlatScope -> [QName]
    getNames ([KindOfName] -> KindsOfNames
    someKindsOfNames ([KindOfName] -> KindsOfNames) -> [KindOfName] -> KindsOfNames
    forall a b. (a -> b) -> a -> b
    $ DisplayLHS
    -> ([KindOfName] -> [KindOfName]) -> [KindOfName] -> [KindOfName]
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen DisplayLHS
    displayLhs ([KindOfName]
    defNameKinds [KindOfName] -> [KindOfName] -> [KindOfName]
    forall a. [a] -> [a] -> [a]
    ++) [KindOfName]
    conLikeNameKinds)
                            (Parsers Pattern -> FlatScope
    forall e. Parsers e -> FlatScope
    flattenedScope Parsers Pattern
    patP)
        let flds = KindsOfNames -> FlatScope -> [QName]
    getNames ([KindOfName] -> KindsOfNames
    someKindsOfNames [KindOfName
    FldName])
                            (Parsers Pattern -> FlatScope
    forall e. Parsers e -> FlatScope
    flattenedScope Parsers Pattern
    patP)
        let 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 (errs, results) = partitionEithers $ map (validPattern conf) ps
        reportS "scope.operators" 60 $ vcat $
          [ "Possible parses for lhs:" ] ++ map (nest 2 . pretty . snd) results
        case results of
            -- Unique result.
            [(Pattern
    _,ParseLHS
    lhs)] -> (ParseLHS
    lhs, Parsers Pattern -> [NotationSection]
    forall e. Parsers e -> [NotationSection]
    operators Parsers Pattern
    patP) (ParseLHS, [NotationSection])
    -> TCMT IO () -> ScopeM (ParseLHS, [NotationSection])
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
                           RawName -> VerboseLevel -> Doc -> TCMT IO ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    RawName -> VerboseLevel -> a -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    RawName -> VerboseLevel -> Doc -> m ()
    reportS RawName
    "scope.operators" VerboseLevel
    50 (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc
    "Parsed lhs:" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> ParseLHS -> Doc
    forall a. Pretty a => a -> Doc
    pretty ParseLHS
    lhs
            -- 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)
    r0:(Pattern, ParseLHS)
    r1:[(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 -> List2 Pattern -> TypeError
    AmbiguousParseForLHS LHSOrPatSyn
    lhsOrPatSyn Pattern
    p (List2 Pattern -> TypeError) -> List2 Pattern -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                             ((Pattern, ParseLHS) -> Pattern)
    -> List2 (Pattern, ParseLHS) -> List2 Pattern
    forall a b. (a -> b) -> List2 a -> List2 b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (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) (List2 (Pattern, ParseLHS) -> List2 Pattern)
    -> List2 (Pattern, ParseLHS) -> List2 Pattern
    forall a b. (a -> b) -> a -> b
    $ (Pattern, ParseLHS)
    -> (Pattern, ParseLHS)
    -> [(Pattern, ParseLHS)]
    -> List2 (Pattern, ParseLHS)
    forall a. a -> a -> [a] -> List2 a
    List2 (Pattern, ParseLHS)
    r0 (Pattern, ParseLHS)
    r1 [(Pattern, ParseLHS)]
    rs
        where
            getNames :: KindsOfNames -> FlatScope -> [QName]
    getNames KindsOfNames
    kinds FlatScope
    flat =
              (List1 NewNotation -> QName) -> [List1 NewNotation] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (NewNotation -> QName
    notaName (NewNotation -> QName)
    -> (List1 NewNotation -> NewNotation) -> List1 NewNotation -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 NewNotation -> NewNotation
    forall a. NonEmpty a -> a
    List1.head) ([List1 NewNotation] -> [QName]) -> [List1 NewNotation] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ KindsOfNames -> FlatScope -> [List1 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
              res <- PatternCheckConfig -> Pattern -> PM ParseLHS
    classifyPattern PatternCheckConfig
    conf Pattern
    p
              case (res, top) of
                (ParsePattern{}, Maybe QName
    Nothing) -> (Pattern, ParseLHS) -> Either (Maybe Pattern) (Pattern, ParseLHS)
    forall a. a -> Either (Maybe Pattern) a
    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 a. a -> Either (Maybe Pattern) a
    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 a. Maybe Pattern -> Either (Maybe Pattern) a
    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 Bool
    _ 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 a. a -> Either (Maybe Pattern) a
    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 Bool
    _ QName
    x)) :| [Arg (Named_ Pattern)]
    ps | PatternCheckConfig -> QName -> Bool
    fldName PatternCheckConfig
    conf QName
    x -> do

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

          -- Ensure that the @ps3@ are patterns rather than lhss.
          mapM_ (guardWithError Nothing . isParsePattern . namedArg) ps3

          -- Step 2: construct the lhs.
          let (f, lhs0)     = fromParseLHS $ namedArg p2
              lhs           = NamedArg ParseLHS -> LHSCore -> NamedArg LHSCore
    forall a b. NamedArg a -> b -> NamedArg b
    setNamedArg NamedArg ParseLHS
    p2 LHSCore
    lhs0
              (ps', _:ps'') = splitAt (length ps1) ps
          return $ ParseLHS f $ lhsCoreAddSpine (LHSProj x ps' lhs []) 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 a b.
    Either (Maybe Pattern) a
    -> (a -> Either (Maybe Pattern) b) -> Either (Maybe Pattern) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case  -- TODO: avoid re-parsing
            ParsePattern{}    -> Maybe Pattern -> PM ParseLHS
    forall a. Maybe Pattern -> Either (Maybe Pattern) a
    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 a. a -> Either (Maybe Pattern) a
    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 a b.
    a -> Either (Maybe Pattern) b -> Either (Maybe Pattern) a
    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_ 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)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Arg a -> m (Arg b)
    Trav.mapM ((Pattern -> PM ParseLHS)
    -> Named_ Pattern -> Either (Maybe Pattern) (Named_ ParseLHS)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Named NamedName a -> m (Named NamedName 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 ::
         DisplayLHS
           -- ^ Are we parsing a 'DisplayPragma'?
      -> QName
           -- ^ Name of the definition.
      -> Pattern
           -- ^ Full left hand side.
      -> ScopeM LHSCore
    parseLHS :: DisplayLHS -> QName -> Pattern -> ScopeM LHSCore
    parseLHS DisplayLHS
    displayLhs 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
      (res, ops) <- DisplayLHS
    -> LHSOrPatSyn
    -> Maybe QName
    -> Pattern
    -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' DisplayLHS
    displayLhs LHSOrPatSyn
    IsLHS (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    top) Pattern
    p
      case res of
        ParseLHS QName
    f LHSCore
    lhs -> LHSCore -> ScopeM LHSCore
    forall a. a -> TCMT IO a
    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
      (res, ops) <- DisplayLHS
    -> LHSOrPatSyn
    -> Maybe QName
    -> Pattern
    -> ScopeM (ParseLHS, [NotationSection])
    parseLHS' DisplayLHS
    NoDisplayLHS LHSOrPatSyn
    lhsOrPatSyn Maybe QName
    forall a. Maybe a
    Nothing Pattern
    p
      case res of
        ParsePattern Pattern
    p -> Pattern -> ScopeM Pattern
    forall a. a -> TCMT IO a
    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

          -- Eliminated by appView:
          AppP{}      :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          OpAppP{}    :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          ParenP{}    :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          RawAppP{}   :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          HiddenP{}   :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          InstanceP{} :| [Pattern]
    _   -> Either (Maybe Pattern) ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- Hopeful cases:
          WithP Range
    _ Pattern
    p   :| []  -> Pattern -> Either (Maybe Pattern) ()
    loop Pattern
    p
          Pattern
    _           :| []  -> Either (Maybe Pattern) ()
    ok
          IdentP Bool
    _ 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 KwRange
    _ Range
    _ Expr
    _  :| [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

          -- Failures:
          AbsurdP{}   :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          AsP{}       :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          EllipsisP{} :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          EqualP{}    :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          LitP{}      :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          QuoteP{}    :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          RecP{}      :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          WildP{}     :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
          WithP{}     :| Pattern
    _:[Pattern]
    _ -> Either (Maybe Pattern) ()
    failure
        where
        ok :: Either (Maybe Pattern) ()
    ok      = () -> Either (Maybe Pattern) ()
    forall a. a -> Either (Maybe Pattern) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        failure :: Either (Maybe Pattern) ()
    failure = Maybe Pattern -> Either (Maybe Pattern) ()
    forall a. Maybe Pattern -> Either (Maybe Pattern) a
    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 Set1 Name
    _ List1 (Arg (Named_ Pattern))
    ps -> (Bool -> QName -> Pattern
    IdentP Bool
    True QName
    op Pattern -> List1 Pattern -> List1 Pattern
    forall a. a -> NonEmpty a -> NonEmpty a
    <| (Arg (Named_ Pattern) -> Pattern)
    -> List1 (Arg (Named_ Pattern)) -> List1 Pattern
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Arg (Named_ Pattern) -> Pattern
    forall a. NamedArg a -> a
    namedArg List1 (Arg (Named_ Pattern))
    ps)
                              List1 Pattern -> [Pattern] -> List1 Pattern
    forall a. NonEmpty a -> [a] -> NonEmpty 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 a. [a] -> 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
        p <- ExprKind -> Maybe QName -> [QName] -> ScopeM (Parsers Expr)
    forall e.
    IsExpr e =>
    ExprKind -> Maybe QName -> [QName] -> ScopeM (Parsers e)
    buildParsers ExprKind
    IsExpr Maybe QName
    forall a. Maybe a
    Nothing [ QName
    q | Ident QName
    q <- [Item (List2 Expr)]
    [Expr]
    es0 ]

        -- Parse
        let result = Parsers Expr -> [Expr] -> [Expr]
    forall e. Parsers e -> [e] -> [e]
    parser Parsers Expr
    p [Item (List2 Expr)]
    [Expr]
    es0
        case foldr seq () result `seq` result of
          [Expr
    e]   -> do
              RawName -> VerboseLevel -> TCM Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    RawName -> VerboseLevel -> TCM Doc -> m ()
    reportSDoc RawName
    "scope.operators" VerboseLevel
    50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall a. a -> TCMT IO a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> Expr -> Doc
    forall a. Pretty a => a -> Doc
    pretty Expr
    e
              Expr -> ScopeM Expr
    forall a. a -> TCMT IO a
    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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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')

    -- | Parse the arguments of a raw application with known head.
    --
    parseArguments ::
         Expr                   -- ^ Head
      -> [Expr]                 -- ^ Raw arguments
      -> ScopeM [NamedArg Expr] -- ^ Operator-parsed arguments
    parseArguments :: Expr -> [Expr] -> ScopeM [NamedArg Expr]
    parseArguments Expr
    hd = \case
      [] -> [NamedArg Expr] -> ScopeM [NamedArg Expr]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      es :: [Expr]
    es@(Expr
    e1 : [Expr]
    rest) -> ExprKind -> ScopeM [NamedArg Expr] -> ScopeM [NamedArg Expr]
    forall a. ExprKind -> ScopeM a -> ScopeM a
    billToParser ExprKind
    IsExpr (ScopeM [NamedArg Expr] -> ScopeM [NamedArg Expr])
    -> ScopeM [NamedArg Expr] -> ScopeM [NamedArg Expr]
    forall a b. (a -> b) -> a -> b
    $ do

        -- Form the raw application for error reporting
        let es2 :: List2 Expr
    es2 = Expr -> Expr -> [Expr] -> List2 Expr
    forall a. a -> a -> [a] -> List2 a
    List2 Expr
    hd Expr
    e1 [Expr]
    rest

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

        -- Parse
        -- TODO: not sure about forcing
        case {-force $-} argsParser p es of
            [[NamedArg Expr]
    as] -> [NamedArg Expr] -> ScopeM [NamedArg Expr]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [NamedArg Expr]
    as
            []   -> TypeError -> ScopeM [NamedArg Expr]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM [NamedArg Expr])
    -> TypeError -> ScopeM [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
    es2
            [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 b a. (b -> a -> b) -> b -> [a] -> b
    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) Expr
    hd
              TypeError -> ScopeM [NamedArg Expr]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> ScopeM [NamedArg Expr])
    -> TypeError -> ScopeM [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
    es2
                        (List1 Expr -> TypeError) -> List1 Expr -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ([NamedArg Expr] -> Expr) -> NonEmpty [NamedArg Expr] -> List1 Expr
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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)

    ---------------------------------------------------------------------------
    -- * 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 Set1 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 -> Set1 Name -> OpAppArgs' e -> ExprView e
    forall e. QName -> Set1 Name -> OpAppArgs' e -> ExprView e
    OpAppV QName
    x Set1 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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
    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 a b. (a -> b) -> Arg a -> Arg b
    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 a b. (a -> b) -> Named NamedName a -> Named NamedName b
    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 a b. (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b
    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 a b. (a -> b) -> OpApp a -> OpApp b
    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