content: {-# OPTIONS_GHC -Wunused-matches #-}
  {-# OPTIONS_GHC -Wunused-binds #-}
  
  {-# 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 Control.Monad ((<$!>))
  
  import Data.Either (partitionEithers)
  import qualified Data.Function
  import Data.Foldable
  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.Operator
  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 k = Bench.billTo
    [ Bench.Parsing
    , case k of
        IsExpr    -> Bench.OperatorsExpr
        IsPattern -> Bench.OperatorsPattern
    ]
  
  ---------------------------------------------------------------------------
  -- * Building the parser
  ---------------------------------------------------------------------------
  
  -- | A data structure used internally by 'buildParsers'.
  data InternalParsers e = InternalParsers
    { pTop    :: Parser e e
    , pApp    :: Parser e e
    , pArgs   :: Parser e [NamedArg e]
    , pNonfix :: Parser e e
    , pAtom   :: Parser e e
    }
  
  -- | The data returned by 'buildParsers'.
  
  data Parsers e = Parsers
    { parser :: [e] -> [e]
      -- ^ A parser for expressions or patterns (depending on the
      -- 'ExprKind' argument given to 'buildParsers').
    , argsParser :: [e] -> [[NamedArg e]]
      -- ^ A parser for sequences of arguments.
    , operators :: [NotationSection]
      -- ^ All operators/notations/sections that were used to generate
      -- the grammar.
    , operatorScope :: OperatorScope
      -- ^ A flattened scope that only contains names such that
      -- they occur in the expression or at least one of their
      -- name parts occurs in the expression.
    }
  
  {-# SPECIALIZE
    buildParsersFromOperatorScope ::
       ExprKind -> Maybe QName -> Set QName -> OperatorScope -> ScopeM (Parsers Expr) #-}
  {-# SPECIALIZE
    buildParsersFromOperatorScope ::
       ExprKind -> Maybe QName -> Set QName -> OperatorScope -> ScopeM (Parsers Pattern) #-}
  
  -- | 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.
  
  buildParsersFromOperatorScope ::
       forall e. IsExpr e
    => ExprKind
    -> Maybe QName
    -> Set QName
    -> OperatorScope
    -> ScopeM (Parsers e)
  buildParsersFromOperatorScope kind top namesInExpr opScope = do
  
      (names, ops0) <- localNames kind top opScope
      let ops | kind == IsPattern = filter (not . isLambdaNotation) ops0
              | otherwise         = ops0
  
      let
          partListsInExpr' = map (List1.toList . nameParts . unqualify)
                                 (Set.toList namesInExpr)
  
          partListTrie f =
            foldr (\ps -> Trie.union (Trie.everyPrefix ps ()))
                  Trie.empty
                  (f partListsInExpr')
  
          -- All names.
          partListsInExpr :: Trie NamePart ()
          partListsInExpr = partListTrie id
  
          -- All names, with the name parts in reverse order.
          reversedPartListsInExpr :: Trie NamePart ()
          reversedPartListsInExpr = partListTrie (map reverse)
  
          -- Every regular name part (not holes etc.).
          partsInExpr :: Set RawName
          partsInExpr =
            Set.fromList [ s | Id s <- concat partListsInExpr' ]
  
          -- Are all name parts present in the expression?
          partsPresent n =
            [ Set.member p partsInExpr
            | p <- stringParts (notation n)
            ]
  
          addHole True  p = [Hole, Id p]
          addHole False p = [Id 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 withHole n =
            Trie.member (addHole withHole p) partListsInExpr
            where
            p = case n of
              HolePart{} : IdPart p : _ -> rangedThing p
              IdPart p : _              -> rangedThing p
              _                         -> __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 withHole n =
            Trie.member (addHole withHole p) reversedPartListsInExpr
            where
            p = case reverse n of
              HolePart{} : IdPart p : _ -> rangedThing p
              IdPart p : _              -> rangedThing p
              _                         -> __IMPOSSIBLE__
  
          -- Are the initial and final identifier parts present with
          -- the right mix of leading and trailing underscores?
          correctUnderscores :: Bool -> Bool -> Notation -> Bool
          correctUnderscores withInitialHole withFinalHole n =
            firstPartPresent withInitialHole n
              &&
            lastPartPresent  withFinalHole   n
  
          -- Should be used with operators (not sections) and notations
          -- coming from syntax declarations.
          filterCorrectUnderscoresOp :: [NewNotation] -> [NotationSection]
          filterCorrectUnderscoresOp ns =
            [ noSection n
            | n <- ns
            , if notaIsOperator n
              then correctUnderscores False False (notation n)
              else all (\s -> Trie.member [Id s] partListsInExpr)
                       (stringParts $ notation n)
            ]
  
          -- Should be used with sections.
          correctUnderscoresSect :: NotationKind -> Notation -> Bool
          correctUnderscoresSect k n = case (k, notationKind n) of
            (PrefixNotation,  InfixNotation)   -> correctUnderscores True False n
            (PostfixNotation, InfixNotation)   -> correctUnderscores False True n
            (NonfixNotation,  InfixNotation)   -> correctUnderscores True True n
            (NonfixNotation,  PrefixNotation)  -> correctUnderscores False True n
            (NonfixNotation,  PostfixNotation) -> correctUnderscores True False n
            _                                  -> __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       = getDefinedNames
                         (someKindsOfNames [ConName, CoConName, FldName, PatternSynName]) opScope
          conNames   = Set.fromList $
                         filter (flip Set.member namesInExpr) $
                         map (notaName . List1.head) cons
          conParts   = Set.fromList $
                         concatMap notationNames $
                         filter (or . partsPresent) $
                         List1.concat cons
  
          allNames   = Set.fromList $
                         filter (flip Set.member namesInExpr) names
          allParts   = Set.union conParts
                         (Set.fromList $
                          concatMap notationNames $
                          filter (or . partsPresent) ops)
  
          isAtom x
            | kind == IsPattern && not (isQualified x) =
              not (Set.member x conParts) || Set.member x conNames
            | otherwise =
              not (Set.member x allParts) || Set.member x 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 kind of
            IsPattern -> DoNotParseSections
            IsExpr    -> ParseSections
  
      let nonClosedSections l ns =
            case parseSections of
              DoNotParseSections -> []
              ParseSections      ->
                [ NotationSection n k (Just l) True
                | n <- ns
                , isinfix n && notaIsOperator n
                , k <- [PrefixNotation, PostfixNotation]
                , correctUnderscoresSect k (notation n)
                ]
  
          unrelatedOperators :: [NotationSection]
          unrelatedOperators =
            filterCorrectUnderscoresOp unrelated
              ++
            nonClosedSections Unrelated unrelated
            where
            unrelated = filter ((== Unrelated) . level) fix
  
          nonWithSections :: [NotationSection]
          nonWithSections =
            map (\s -> s { sectLevel = Nothing })
                (filterCorrectUnderscoresOp non)
              ++
            case parseSections of
              DoNotParseSections -> []
              ParseSections      ->
                [ NotationSection n NonfixNotation Nothing True
                | n <- fix
                , notaIsOperator n
                , correctUnderscoresSect NonfixNotation (notation n)
                ]
  
          -- The triples have the form (level, operators). The lowest
          -- level comes first.
          relatedOperators :: [(PrecedenceLevel, [NotationSection])]
          relatedOperators =
            map (\((l, ns) :| rest) -> (l, ns ++ concatMap snd rest)) .
            List1.groupOn fst .
            mapMaybe (\n -> case level n of
                              Unrelated     -> Nothing
                              r@(Related l) ->
                                Just (l, filterCorrectUnderscoresOp [n] ++
                                         nonClosedSections r [n])) $
            fix
  
          everything :: [NotationSection]
          everything =
            concatMap snd relatedOperators ++
            unrelatedOperators ++
            nonWithSections
  
      reportS "scope.operators" 50
        [ "unrelatedOperators = " ++ prettyShow unrelatedOperators
        , "nonWithSections    = " ++ prettyShow nonWithSections
        , "relatedOperators   = " ++ prettyShow relatedOperators
        ]
  
      let g = Data.Function.fix $ \p -> InternalParsers
                { pTop    = memoise TopK $
                            Agda.Utils.List.asum $
                              foldr (\(l, ns) higher ->
                                         mkP (Right l) parseSections
                                             (pTop p) ns higher True) (pApp p)
                                     relatedOperators :
                              zipWith (\ k n ->
                                      mkP (Left k) parseSections
                                          (pTop p) [n] (pApp p) False) [0..] unrelatedOperators
                , pApp    = memoise AppK $ appP (pNonfix p) (pArgs p)
                , pArgs   = argsP (pNonfix p)
                , pNonfix = memoise NonfixK $
                            Agda.Utils.List.asum $
                              pAtom p :
                              map (\sect ->
                                let n = sectNotation sect
  
                                    inner :: forall k. NK k ->
                                             Parser e (OperatorType k e)
                                    inner = opP parseSections (pTop p) n
                                in
                                case notationKind (notation n) of
                                  InfixNotation ->
                                    flip ($) <$> placeholder Beginning
                                             <*> inner In
                                             <*> placeholder End
                                  PrefixNotation ->
                                    inner Pre <*> placeholder End
                                  PostfixNotation ->
                                    flip ($) <$> placeholder Beginning
                                             <*> inner Post
                                  NonfixNotation -> inner Non
                                  NoNotation     -> __IMPOSSIBLE__) nonWithSections
                , pAtom   = atomP isAtom
                }
  
      -- Andreas, 2020-06-03 #4712
      -- Note: needs Agda to be compiled with DEBUG_PARSING to print the grammar.
      reportS "scope.grammar" 20 $
        "Operator grammar:" $$ nest 2 (grammar (pTop g))
  
      return $ Parsers
        { parser         = parse (parseSections, pTop  g)
        , argsParser     = parse (parseSections, pArgs g)
        , operators      = everything
        , operatorScope  = opScope
        }
      where
          level :: NewNotation -> FixityLevel
          level = fixityLevel . notaFixity
  
          nonfix, isinfix, isprefix, ispostfix :: NewNotation -> Bool
          nonfix    = (== NonfixNotation)  . notationKind . notation
          isinfix   = (== InfixNotation)   . notationKind . notation
          isprefix  = (== PrefixNotation)  . notationKind . notation
          ispostfix = (== PostfixNotation) . notationKind . notation
  
          isPrefix, isPostfix :: NotationSection -> Bool
          isPrefix  = (== PrefixNotation)  . sectKind
          isPostfix = (== PostfixNotation) . sectKind
  
          isInfix :: Associativity -> NotationSection -> Bool
          isInfix ass s =
            sectKind s == InfixNotation
               &&
            fixityAssoc (notaFixity (sectNotation s)) == 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 key parseSections p0 ops higher includeHigher =
              memoise (NodeK key) $
                Agda.Utils.List.asum $
                  applyWhen includeHigher (higher :) $
                  catMaybes [nonAssoc, preRights, 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 =
                Agda.Utils.List.asum .
                map \ sect -> opP parseSections p0 (sectNotation sect) In
  
              choicePre :: [NotationSection] -> Parser e (OperatorType 'PrefixNotation e)
              choicePre =
                Agda.Utils.List.asum .
                map \ sect -> do
                  let n = sectNotation sect
                  if   isinfix n || ispostfix n
                  then flip ($) <$> placeholder Beginning
                                <*> opP parseSections p0 n In
                  else opP parseSections p0 n Pre
  
              choicePost :: [NotationSection] -> Parser e (OperatorType 'PostfixNotation e)
              choicePost =
                Agda.Utils.List.asum .
                map \ sect -> do
                  let n = sectNotation sect
                  if isinfix n || isprefix n
                  then flip <$> opP parseSections p0 n In
                            <*> placeholder End
                  else opP parseSections p0 n Post
  
              nonAssoc :: Maybe (Parser e e)
              nonAssoc = case filter (isInfix NonAssoc) ops of
                []  -> Nothing
                ops -> Just $
                  (\x f y -> f (noPlaceholder x) (noPlaceholder y))
                    <$> higher
                    <*> choiceIn ops
                    <*> higher
  
              or _  []   _  []   = Nothing
              or _  []   p2 ops2 = Just (p2 ops2)
              or p1 ops1 _  []   = Just (p1 ops1)
              or p1 ops1 p2 ops2 = Just (p1 ops1 <|> p2 ops2)
  
              preRight :: Maybe (Parser e (MaybePlaceholder e -> e))
              preRight =
                or choicePre
                   (filter isPrefix ops)
                   (\ops -> flip ($) <$> (noPlaceholder <$> higher)
                                     <*> choiceIn ops)
                   (filter (isInfix RightAssoc) ops)
  
              preRights :: Maybe (Parser e e)
              preRights = do
                preRight <- preRight
                return $ Data.Function.fix $ \preRights ->
                  memoiseIfPrinting (PreRightsK key) $
                    preRight <*> (noPlaceholder <$> (preRights <|> higher))
  
              postLeft :: Maybe (Parser e (MaybePlaceholder e -> e))
              postLeft =
                or choicePost
                   (filter isPostfix ops)
                   (\ops -> flip <$> choiceIn ops
                                 <*> (noPlaceholder <$> higher))
                   (filter (isInfix LeftAssoc) ops)
  
              postLefts :: Maybe (Parser e e)
              postLefts = do
                postLeft <- postLeft
                return $ Data.Function.fix $ \postLefts ->
                  memoise (PostLeftsK key) $
                    flip ($) <$> (noPlaceholder <$> (postLefts <|> higher))
                             <*> postLeft
  
  -- | Only build parsers if there's at least one relevant operator or notation in
  --   scope.
  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 (Maybe (Parsers e))
  buildParsers kind top exprNames0 = do
      let namesInExpr = Set.fromList $ applyWhenJust top (:) exprNames0
      opScope <- getOperatorScope namesInExpr <$> getScope
      if osHasOps opScope
        then Just <$!> buildParsersFromOperatorScope kind top namesInExpr opScope
        else pure Nothing
  
  -- | Build parsers regardless of there being operators or notations in the relevant scope.
  alwaysBuildParsers ::
          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)
  alwaysBuildParsers kind top exprNames0 = do
      let namesInExpr = Set.fromList $ applyWhenJust top (:) exprNames0
      opScope <- getOperatorScope namesInExpr <$> getScope
      buildParsersFromOperatorScope kind top namesInExpr opScope
  
  ---------------------------------------------------------------------------
  -- * 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 parse = loop
    where
    loop = \case
      AppP p (Arg info q) ->
          fullParen' <$> (AppP <$> loop p <*> (Arg info <$> traverse loop q))
      RawAppP _ ps     -> fullParen' <$> (loop =<< parse (List2.toList ps))
      OpAppP r d ns ps -> fullParen' . OpAppP r d ns <$> (mapM . traverse . traverse) loop ps
      HiddenP _ _      -> fail "bad hidden argument"
      InstanceP _ _    -> fail "bad instance argument"
      AsP r x p        -> AsP r x <$> loop p
      p@DotP{}         -> return p
      ParenP _r p      -> fullParen' <$> loop p
      p@WildP{}        -> return p
      p@AbsurdP{}      -> return p
      p@LitP{}         -> return p
      p@QuoteP{}       -> return p
      p@IdentP{}       -> return p
      RecP kwr r fs    -> RecP kwr r <$> mapM (traverse loop) fs
      p@EqualP{}       -> return p -- Andrea: cargo culted from DotP
      EllipsisP r mp   -> caseMaybe mp (fail "bad ellipsis") $ \p ->
                            EllipsisP r . Just <$> loop p
      WithP r p        -> WithP r <$> loop 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 = \case
      ParsePattern p  -> pretty p
      ParseLHS _f lhs -> pretty 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' NoDisplayLHS IsLHS (Just qn) WildP{} =
      return (ParseLHS qn $ LHSHead qn [], [])
  
  parseLHS' displayLhs lhsOrPatSyn top p = do
  
      -- Build parser.
      patP <- alwaysBuildParsers IsPattern top (patternQNames p)
  
      -- Run parser, forcing result.
      let ps   = let result = parsePat (parser patP) p
                 in  foldr seq () result `seq` result
  
      -- Classify parse results.
      let cons = getNames (someKindsOfNames $ applyWhen displayLhs (defNameKinds ++) conLikeNameKinds)
                          (operatorScope patP)
      let flds = getNames (someKindsOfNames [FldName])
                          (operatorScope patP)
      let conf = PatternCheckConfig top (hasElem cons) (hasElem 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.
          [(_,lhs)] -> (lhs, operators patP) <$ do
                         reportS "scope.operators" 50 $ "Parsed lhs:" <+> pretty lhs
          -- No result.
          []        -> typeError $ OperatorInformation (operators patP) $
                         NoParseForLHS lhsOrPatSyn (catMaybes errs) p
          -- Ambiguous result.
          r0:r1:rs  -> typeError $ OperatorInformation (operators patP) $
                         AmbiguousParseForLHS lhsOrPatSyn p $
                           fmap (fullParen . fst) $ List2 r0 r1 rs
      where
          getNames kinds flat =
            map (notaName . List1.head) $ getDefinedNames kinds flat
  
          -- The pattern is retained for error reporting in case of ambiguous parses.
          validPattern :: PatternCheckConfig -> Pattern -> PM (Pattern, ParseLHS)
          validPattern conf p = do
            res <- classifyPattern conf p
            case (res, top) of
              (ParsePattern{}, Nothing) -> return (p, res)  -- expect pattern
              (ParseLHS{}    , Just{} ) -> return (p, res)  -- expect lhs
              _ -> throwError Nothing
  
  -- | Name sets for classifying a pattern.
  data PatternCheckConfig = PatternCheckConfig
    { topName :: Maybe QName    -- ^ Name of defined symbol.
    , conName :: QName -> Bool  -- ^ Valid constructor name?
    , 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 conf p =
    case patternAppView p of
  
      -- case @f ps@
      Arg _ (Named _ (IdentP _ x)) :| ps | Just x == topName conf -> do
        mapM_ (valid . namedArg) ps
        return $ ParseLHS x $ lhsCoreAddSpine (LHSHead x []) ps
  
      -- case @d ps@
      Arg _ (Named _ (IdentP _ x)) :| ps | fldName conf x -> do
  
        -- Step 1: check for valid copattern lhs.
        ps0 :: [NamedArg ParseLHS] <- mapM classPat 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           = setNamedArg p2 lhs0
            (ps', _:ps'') = splitAt (length ps1) ps
        return $ ParseLHS f $ lhsCoreAddSpine (LHSProj x ps' lhs []) ps''
  
      -- case @...@
      Arg _ (Named _ (EllipsisP r (Just p))) :| ps -> do
        classifyPattern conf p >>= \case  -- TODO: avoid re-parsing
          ParsePattern{}    -> throwError Nothing
          (ParseLHS f core) -> do
            mapM_ (valid . namedArg) ps
            let ellcore = LHSEllipsis r core
            return $ ParseLHS f $ lhsCoreAddSpine ellcore ps
  
      -- case: ordinary pattern
      _ -> ParsePattern p <$ valid p
  
    where
    valid = validConPattern $ conName conf
  
    classPat :: NamedArg Pattern -> PM (NamedArg ParseLHS)
    classPat = Trav.mapM (Trav.mapM (classifyPattern conf))
  
    isParsePattern = \case
      ParsePattern{} -> True
      ParseLHS{}     -> False
  
    fromParseLHS :: ParseLHS -> (QName, LHSCore)
    fromParseLHS = \case
      ParseLHS f lhs -> (f, lhs)
      ParsePattern{} -> __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 top p = billToParser IsPattern $ do
    (res, ops) <- parseLHS' displayLhs IsLHS (Just top) p
    case res of
      ParseLHS _f lhs -> return lhs
      _ -> typeError $ OperatorInformation ops
                     $ NoParseForLHS IsLHS [] p
  
  -- | Parses a pattern.
  parsePattern :: Pattern -> ScopeM Pattern
  parsePattern = parsePatternOrSyn IsLHS
  
  parsePatternSyn :: Pattern -> ScopeM Pattern
  parsePatternSyn = parsePatternOrSyn IsPatSyn
  
  parsePatternOrSyn :: LHSOrPatSyn -> Pattern -> ScopeM Pattern
  parsePatternOrSyn lhsOrPatSyn p = billToParser IsPattern $ do
    (res, ops) <- parseLHS' NoDisplayLHS lhsOrPatSyn Nothing p
    case res of
      ParsePattern p -> return p
      _ -> typeError $ OperatorInformation ops
                     $ NoParseForLHS lhsOrPatSyn [] 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 cons = loop
    where
    loop p = case appView p of
  
        -- Eliminated by appView:
        AppP{}      :| _   -> __IMPOSSIBLE__
        OpAppP{}    :| _   -> __IMPOSSIBLE__
        ParenP{}    :| _   -> __IMPOSSIBLE__
        RawAppP{}   :| _   -> __IMPOSSIBLE__
        HiddenP{}   :| _   -> __IMPOSSIBLE__
        InstanceP{} :| _   -> __IMPOSSIBLE__
  
        -- Hopeful cases:
        WithP _ p   :| []  -> loop p
        _           :| []  -> ok
        IdentP _ x  :| ps
          | cons x         -> mapM_ loop ps
          | otherwise      -> failure
        QuoteP _    :| [_] -> ok
        DotP _ _ _  :| ps  -> mapM_ loop ps
  
        -- Failures:
        AbsurdP{}   :| _:_ -> failure
        AsP{}       :| _:_ -> failure
        EllipsisP{} :| _:_ -> failure
        EqualP{}    :| _:_ -> failure
        LitP{}      :| _:_ -> failure
        QuoteP{}    :| _:_ -> failure
        RecP{}      :| _:_ -> failure
        WildP{}     :| _:_ -> failure
        WithP{}     :| _:_ -> failure
      where
      ok      = return ()
      failure = throwError $ Just p
  
  
  -- | Helper function for 'parseLHS' and 'parsePattern'.
  appView :: Pattern -> List1 Pattern
  appView = loop []
    where
    loop acc = \case
      AppP p a         -> loop (namedArg a : acc) p
      OpAppP _ op _ ps -> (IdentP True op <| fmap namedArg ps)
                            `List1.appendList`
                          reverse acc
      ParenP _ p       -> loop acc p
      RawAppP _ _      -> __IMPOSSIBLE__
      HiddenP _ _      -> __IMPOSSIBLE__
      InstanceP _ _    -> __IMPOSSIBLE__
      p@IdentP{}       -> ret p
      p@WildP{}        -> ret p
      p@AsP{}          -> ret p
      p@AbsurdP{}      -> ret p
      p@LitP{}         -> ret p
      p@QuoteP{}       -> ret p
      p@DotP{}         -> ret p
      p@RecP{}         -> ret p
      p@EqualP{}       -> ret p
      p@EllipsisP{}    -> ret p
      p@WithP{}        -> ret p
     where
     ret p = p :| reverse acc
  
  -- | Parse a list of expressions (typically from a 'RawApp') into an application.
  parseApplication :: List2 Expr -> ScopeM Expr
  parseApplication es  = billToParser IsExpr $ do
      let es0 = List2.toList es
      p <- buildParsers IsExpr Nothing [ q | Ident q <- es0 ]
      case p of
  
        -- no operators or notations in scope
        Nothing -> do
          let hd :| rest = List2.toList1 es
              app :: Expr -> Expr -> Expr
              app !acc !e = let
                range = fuseRange acc e
                !arg  = case e of
                  HiddenArg _ e    -> hide (defaultArg e)
                  InstanceArg _ e  -> makeInstance (defaultArg e)
                  e                -> defaultArg (unnamed e)
                in App range acc arg
              !res = foldl' app hd rest
          pure res
  
        -- operators or notations in scope
        Just p -> case parser p es0 of
          [e]   -> do
              reportS "scope.operators" 50 $
                "Parsed an operator application:" <+> pretty e
              return $! e
          []    -> typeError $ OperatorInformation (operators p)
                             $ NoParseForApplication es
          e:es' -> typeError $ OperatorInformation (operators p)
                             $ AmbiguousParseForApplication es
                             $ fmap fullParen (e :| es')
  
  -- | Parse the arguments of a raw application with known head.
  --
  parseArguments ::
       Expr                   -- ^ Head
    -> [Expr]                 -- ^ Raw arguments
    -> ScopeM [NamedArg Expr] -- ^ Operator-parsed arguments
  parseArguments hd = \case
    [] -> return []
    es@(e1 : rest) -> billToParser IsExpr $ do
  
      -- Form the raw application for error reporting
      let es2 = List2 hd e1 rest
  
      -- Build the arguments parser
      p <- buildParsers IsExpr Nothing [ q | Ident q <- es ]
      case p of
        Nothing -> do
          let go :: Expr -> NamedArg Expr
              go (HiddenArg _ e)   = hide (defaultArg e)
              go (InstanceArg _ e) = makeInstance (defaultArg e)
              go e                 = defaultArg (unnamed e)
          return $! map' go es
        Just p -> case argsParser p es of
          [as] -> return $! as
          []   -> typeError $ OperatorInformation (operators p)
                            $ NoParseForApplication es2
          as : ass -> do
            let f = fullParen . foldl (App noRange) hd
            typeError $ OperatorInformation (operators p)
                      $ AmbiguousParseForApplication es2
                      $ fmap f (as :| ass)
  
  ---------------------------------------------------------------------------
  -- * Inserting parenthesis
  ---------------------------------------------------------------------------
  
  fullParen :: IsExpr e => e -> e
  fullParen e = case exprView $ fullParen' e of
      ParenV e    -> e
      e'          -> unExprView e'
  
  fullParen' :: IsExpr e => e -> e
  fullParen' e = case exprView e of
      LocalV _     -> e
      WildV _      -> e
      OtherV _     -> e
      HiddenArgV _ -> e
      InstanceArgV _ -> e
      ParenV _     -> e
      AppV e1 (Arg info e2) -> par $ unExprView $ AppV (fullParen' e1) (Arg info e2')
          where
              e2' = case argInfoHiding info of
                  Hidden     -> e2
                  Instance{} -> e2
                  NotHidden  -> fullParen' <$> e2
      OpAppV x ns es -> par $ unExprView $ OpAppV x ns $ (fmap . fmap . fmap . fmap . fmap) fullParen' es
      LamV bs e -> par $ unExprView $ LamV bs (fullParen e)
      where
          par = unExprView . ParenV
  