    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE DataKinds    #-}

    module Agda.Syntax.Concrete.Operators.Parser where

    import Control.Applicative ( Alternative((<|>), many) )
    import Control.Monad ((<=<))

    import Data.Either
    import Data.Function (on)
    import Data.Kind ( Type )
    import qualified Data.List as List
    import Data.Maybe
    import qualified Data.Strict.Maybe as Strict

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

    import Agda.Syntax.Common.Pretty
    import Agda.Utils.List  ( spanEnd )
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Set1  ( Set1 )
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    placeholder :: PositionInName -> Parser e (MaybePlaceholder e)
    placeholder :: forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    p =
      Doc
    -> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e)
    forall tok a. Doc -> Parser tok a -> Parser tok a
    doc ([Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char]
    "_" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ PositionInName -> [Char]
    forall a. Show a => a -> [Char]
    show PositionInName
    p)) (Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e))
    -> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder e)
    forall a b. (a -> b) -> a -> b
    $
      (MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e)
    forall tok.
    (MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)
    sat ((MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e))
    -> (MaybePlaceholder e -> Bool) -> Parser e (MaybePlaceholder e)
    forall a b. (a -> b) -> a -> b
    $ \case
        Placeholder PositionInName
    p' | PositionInName
    p' PositionInName -> PositionInName -> Bool
    forall a. Eq a => a -> a -> Bool
    == PositionInName
    p -> Bool
    True
        MaybePlaceholder e
    _                        -> Bool
    False

    maybePlaceholder ::
      Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
    maybePlaceholder :: forall e.
    Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
    maybePlaceholder Maybe PositionInName
    mp Parser e e
    p = case Maybe PositionInName
    mp of
      Maybe PositionInName
    Nothing -> Parser e (MaybePlaceholder e)
    p'
      Just PositionInName
    h  -> PositionInName -> Parser e (MaybePlaceholder e)
    forall e. PositionInName -> Parser e (MaybePlaceholder e)
    placeholder PositionInName
    h Parser e (MaybePlaceholder e)
    -> Parser e (MaybePlaceholder e) -> Parser e (MaybePlaceholder 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 (MaybePlaceholder e)
    p'
      where
      p' :: Parser e (MaybePlaceholder e)
    p' = e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> MaybePlaceholder e)
    -> Parser e e -> Parser e (MaybePlaceholder e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    p

    satNoPlaceholder :: (e -> Maybe a) -> Parser e a
    satNoPlaceholder :: forall e a. (e -> Maybe a) -> Parser e a
    satNoPlaceholder e -> Maybe a
    p = (MaybePlaceholder e -> Maybe a) -> Parser e a
    forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
    sat' ((MaybePlaceholder e -> Maybe a) -> Parser e a)
    -> (MaybePlaceholder e -> Maybe a) -> Parser e a
    forall a b. (a -> b) -> a -> b
    $ \case
        NoPlaceholder Maybe PositionInName
    _ e
    e -> e -> Maybe a
    p e
    e
        Placeholder PositionInName
    _     -> Maybe a
    forall a. Maybe a
    Nothing

    data ExprView e
        = LocalV QName
        | WildV e
        | OtherV e
        | AppV e (NamedArg e)
        | OpAppV QName (Set1 A.Name) (OpAppArgs' e)
          -- ^ The 'QName' is possibly ambiguous, but it must correspond
          -- to one of the names in the set.
        | HiddenArgV (Named_ e)
        | InstanceArgV (Named_ e)
        | LamV (List1 LamBinding) e
        | ParenV e
    --    deriving (Show)

    class HasRange e => IsExpr e where
      exprView    :: e -> ExprView e
      unExprView  :: ExprView e -> e
      patternView :: e -> Maybe Pattern

    instance IsExpr e => HasRange (ExprView e) where
      getRange :: ExprView e -> Range
    getRange = e -> Range
    forall a. HasRange a => a -> Range
    getRange (e -> Range) -> (ExprView e -> e) -> ExprView e -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView

    instance IsExpr Expr where
        exprView :: Expr -> ExprView Expr
    exprView = \case
            Ident QName
    x         -> QName -> ExprView Expr
    forall e. QName -> ExprView e
    LocalV QName
    x
            App Range
    _ Expr
    e1 NamedArg Expr
    e2     -> Expr -> NamedArg Expr -> ExprView Expr
    forall e. e -> NamedArg e -> ExprView e
    AppV Expr
    e1 NamedArg Expr
    e2
            OpApp Range
    r QName
    d Set1 Name
    ns OpAppArgs
    es -> QName -> Set1 Name -> OpAppArgs -> ExprView Expr
    forall e. QName -> Set1 Name -> OpAppArgs' e -> ExprView e
    OpAppV QName
    d Set1 Name
    ns OpAppArgs
    es
            HiddenArg Range
    _ Named_ Expr
    e   -> Named_ Expr -> ExprView Expr
    forall e. Named_ e -> ExprView e
    HiddenArgV Named_ Expr
    e
            InstanceArg Range
    _ Named_ Expr
    e -> Named_ Expr -> ExprView Expr
    forall e. Named_ e -> ExprView e
    InstanceArgV Named_ Expr
    e
            Paren Range
    _ Expr
    e       -> Expr -> ExprView Expr
    forall e. e -> ExprView e
    ParenV Expr
    e
            Lam Range
    _ List1 LamBinding
    bs    Expr
    e   -> List1 LamBinding -> Expr -> ExprView Expr
    forall e. List1 LamBinding -> e -> ExprView e
    LamV List1 LamBinding
    bs Expr
    e
            e :: Expr
    e@Underscore{}  -> Expr -> ExprView Expr
    forall e. e -> ExprView e
    WildV Expr
    e
            Expr
    e               -> Expr -> ExprView Expr
    forall e. e -> ExprView e
    OtherV Expr
    e
        unExprView :: ExprView Expr -> Expr
    unExprView = \case
            LocalV QName
    x       -> QName -> Expr
    Ident QName
    x
            AppV Expr
    e1 NamedArg Expr
    e2     -> Range -> Expr -> NamedArg Expr -> Expr
    App (Expr -> NamedArg Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange Expr
    e1 NamedArg Expr
    e2) Expr
    e1 NamedArg Expr
    e2
            OpAppV QName
    d Set1 Name
    ns OpAppArgs
    es -> Range -> QName -> Set1 Name -> OpAppArgs -> Expr
    OpApp (QName -> OpAppArgs -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange QName
    d OpAppArgs
    es) QName
    d Set1 Name
    ns OpAppArgs
    es
            HiddenArgV Named_ Expr
    e   -> Range -> Named_ Expr -> Expr
    HiddenArg (Named_ Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Named_ Expr
    e) Named_ Expr
    e
            InstanceArgV Named_ Expr
    e -> Range -> Named_ Expr -> Expr
    InstanceArg (Named_ Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Named_ Expr
    e) Named_ Expr
    e
            ParenV Expr
    e       -> Range -> Expr -> Expr
    Paren (Expr -> Range
    forall a. HasRange a => a -> Range
    getRange Expr
    e) Expr
    e
            LamV List1 LamBinding
    bs Expr
    e      -> Range -> List1 LamBinding -> Expr -> Expr
    Lam (List1 LamBinding -> Expr -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange List1 LamBinding
    bs Expr
    e) List1 LamBinding
    bs Expr
    e
            WildV Expr
    e        -> Expr
    e
            OtherV Expr
    e       -> Expr
    e

        patternView :: Expr -> Maybe Pattern
    patternView = Expr -> Maybe Pattern
    isPattern

    instance IsExpr Pattern where
        exprView :: Pattern -> ExprView Pattern
    exprView = \case
            IdentP Bool
    True QName
    x    -> QName -> ExprView Pattern
    forall e. QName -> ExprView e
    LocalV QName
    x
            IdentP Bool
    False QName
    _   -> ExprView Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            AppP Pattern
    e1 NamedArg Pattern
    e2       -> Pattern -> NamedArg Pattern -> ExprView Pattern
    forall e. e -> NamedArg e -> ExprView e
    AppV Pattern
    e1 NamedArg Pattern
    e2
            OpAppP Range
    r QName
    d Set1 Name
    ns List1 (NamedArg Pattern)
    es -> QName -> Set1 Name -> OpAppArgs' Pattern -> ExprView Pattern
    forall e. QName -> Set1 Name -> OpAppArgs' e -> ExprView e
    OpAppV QName
    d Set1 Name
    ns (OpAppArgs' Pattern -> ExprView Pattern)
    -> OpAppArgs' Pattern -> ExprView Pattern
    forall a b. (a -> b) -> a -> b
    $ ((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
    -> List1 (NamedArg Pattern) -> OpAppArgs' Pattern
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
     -> List1 (NamedArg Pattern) -> OpAppArgs' Pattern)
    -> ((Pattern -> MaybePlaceholder (OpApp Pattern))
        -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
    -> (Pattern -> MaybePlaceholder (OpApp Pattern))
    -> List1 (NamedArg Pattern)
    -> OpAppArgs' Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName Pattern
     -> Named_ (MaybePlaceholder (OpApp Pattern)))
    -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern))
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named NamedName Pattern
      -> Named_ (MaybePlaceholder (OpApp Pattern)))
     -> NamedArg Pattern -> NamedArg (MaybePlaceholder (OpApp Pattern)))
    -> ((Pattern -> MaybePlaceholder (OpApp Pattern))
        -> Named NamedName Pattern
        -> Named_ (MaybePlaceholder (OpApp Pattern)))
    -> (Pattern -> MaybePlaceholder (OpApp Pattern))
    -> NamedArg Pattern
    -> NamedArg (MaybePlaceholder (OpApp Pattern))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Pattern -> MaybePlaceholder (OpApp Pattern))
    -> Named NamedName Pattern
    -> Named_ (MaybePlaceholder (OpApp Pattern))
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (OpApp Pattern -> MaybePlaceholder (OpApp Pattern)
    forall e. e -> MaybePlaceholder e
    noPlaceholder (OpApp Pattern -> MaybePlaceholder (OpApp Pattern))
    -> (Pattern -> OpApp Pattern)
    -> Pattern
    -> MaybePlaceholder (OpApp Pattern)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> OpApp Pattern
    forall e. e -> OpApp e
    Ordinary) List1 (NamedArg Pattern)
    es
            HiddenP Range
    _ Named NamedName Pattern
    e      -> Named NamedName Pattern -> ExprView Pattern
    forall e. Named_ e -> ExprView e
    HiddenArgV Named NamedName Pattern
    e
            InstanceP Range
    _ Named NamedName Pattern
    e    -> Named NamedName Pattern -> ExprView Pattern
    forall e. Named_ e -> ExprView e
    InstanceArgV Named NamedName Pattern
    e
            ParenP Range
    _ Pattern
    e       -> Pattern -> ExprView Pattern
    forall e. e -> ExprView e
    ParenV Pattern
    e
            e :: Pattern
    e@WildP{}        -> Pattern -> ExprView Pattern
    forall e. e -> ExprView e
    WildV Pattern
    e
            Pattern
    e                -> Pattern -> ExprView Pattern
    forall e. e -> ExprView e
    OtherV Pattern
    e
        unExprView :: ExprView Pattern -> Pattern
    unExprView = \case
            LocalV QName
    x       -> Bool -> QName -> Pattern
    IdentP Bool
    True QName
    x
            AppV Pattern
    e1 NamedArg Pattern
    e2     -> Pattern -> NamedArg Pattern -> Pattern
    AppP Pattern
    e1 NamedArg Pattern
    e2
            OpAppV QName
    d Set1 Name
    ns OpAppArgs' Pattern
    es -> let ess :: List1 (NamedArg Pattern)
                                  ess :: List1 (NamedArg Pattern)
    ess = ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
    -> OpAppArgs' Pattern -> List1 (NamedArg Pattern)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
     -> OpAppArgs' Pattern -> List1 (NamedArg Pattern))
    -> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
        -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
    -> (MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> OpAppArgs' Pattern
    -> List1 (NamedArg Pattern)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named_ (MaybePlaceholder (OpApp Pattern))
     -> Named NamedName Pattern)
    -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Named_ (MaybePlaceholder (OpApp Pattern))
      -> Named NamedName Pattern)
     -> NamedArg (MaybePlaceholder (OpApp Pattern)) -> NamedArg Pattern)
    -> ((MaybePlaceholder (OpApp Pattern) -> Pattern)
        -> Named_ (MaybePlaceholder (OpApp Pattern))
        -> Named NamedName Pattern)
    -> (MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> NamedArg (MaybePlaceholder (OpApp Pattern))
    -> NamedArg Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MaybePlaceholder (OpApp Pattern) -> Pattern)
    -> Named_ (MaybePlaceholder (OpApp Pattern))
    -> Named NamedName Pattern
    forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap)
                                          (\case
                                              Placeholder{}     -> Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                                              NoPlaceholder Maybe PositionInName
    _ OpApp Pattern
    x -> Pattern -> OpApp Pattern -> Pattern
    forall e. e -> OpApp e -> e
    fromOrdinary Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__ OpApp Pattern
    x)
                                          OpAppArgs' Pattern
    es
                              in Range -> QName -> Set1 Name -> List1 (NamedArg Pattern) -> Pattern
    OpAppP (QName -> List1 (NamedArg Pattern) -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange QName
    d List1 (NamedArg Pattern)
    ess) QName
    d Set1 Name
    ns List1 (NamedArg Pattern)
    ess
            HiddenArgV Named NamedName Pattern
    e   -> Range -> Named NamedName Pattern -> Pattern
    HiddenP (Named NamedName Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange Named NamedName Pattern
    e) Named NamedName Pattern
    e
            InstanceArgV Named NamedName Pattern
    e -> Range -> Named NamedName Pattern -> Pattern
    InstanceP (Named NamedName Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange Named NamedName Pattern
    e) Named NamedName Pattern
    e
            ParenV Pattern
    e       -> Range -> Pattern -> Pattern
    ParenP (Pattern -> Range
    forall a. HasRange a => a -> Range
    getRange Pattern
    e) Pattern
    e
            LamV List1 LamBinding
    _ Pattern
    _       -> Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            WildV Pattern
    e        -> Pattern
    e
            OtherV Pattern
    e       -> Pattern
    e

        patternView :: Pattern -> Maybe Pattern
    patternView = Pattern -> Maybe Pattern
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    -- | Should sections be parsed?
    data ParseSections = ParseSections | DoNotParseSections
      deriving (ParseSections -> ParseSections -> Bool
    (ParseSections -> ParseSections -> Bool)
    -> (ParseSections -> ParseSections -> Bool) -> Eq ParseSections
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ParseSections -> ParseSections -> Bool
    == :: ParseSections -> ParseSections -> Bool
    $c/= :: ParseSections -> ParseSections -> Bool
    /= :: ParseSections -> ParseSections -> Bool
    Eq, Int -> ParseSections -> [Char] -> [Char]
    [ParseSections] -> [Char] -> [Char]
    ParseSections -> [Char]
    (Int -> ParseSections -> [Char] -> [Char])
    -> (ParseSections -> [Char])
    -> ([ParseSections] -> [Char] -> [Char])
    -> Show ParseSections
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> ParseSections -> [Char] -> [Char]
    showsPrec :: Int -> ParseSections -> [Char] -> [Char]
    $cshow :: ParseSections -> [Char]
    show :: ParseSections -> [Char]
    $cshowList :: [ParseSections] -> [Char] -> [Char]
    showList :: [ParseSections] -> [Char] -> [Char]
    Show)

    -- | Runs a parser. If sections should be parsed, then identifiers
    -- with at least two name parts are split up into multiple tokens,
    -- using 'PositionInName' to record the tokens' original positions
    -- within their respective identifiers.

    parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
    parse :: forall e a. IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
    parse (ParseSections
    DoNotParseSections, Parser e a
    p) [e]
    es = Parser e a -> [MaybePlaceholder e] -> [a]
    forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
    P.parse Parser e a
    p ((e -> MaybePlaceholder e) -> [e] -> [MaybePlaceholder e]
    forall a b. (a -> b) -> [a] -> [b]
    map e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder [e]
    es)
    parse (ParseSections
    ParseSections,      Parser e a
    p) [e]
    es = Parser e a -> [MaybePlaceholder e] -> [a]
    forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
    P.parse Parser e a
    p ([List1 (MaybePlaceholder e)] -> [MaybePlaceholder e]
    forall a. [List1 a] -> [a]
    List1.concat ([List1 (MaybePlaceholder e)] -> [MaybePlaceholder e])
    -> [List1 (MaybePlaceholder e)] -> [MaybePlaceholder e]
    forall a b. (a -> b) -> a -> b
    $ (e -> List1 (MaybePlaceholder e))
    -> [e] -> [List1 (MaybePlaceholder e)]
    forall a b. (a -> b) -> [a] -> [b]
    map e -> List1 (MaybePlaceholder e)
    forall e. IsExpr e => e -> List1 (MaybePlaceholder e)
    splitExpr [e]
    es)
      where
      splitExpr :: IsExpr e => e -> List1 (MaybePlaceholder e)
      splitExpr :: forall e. IsExpr e => e -> List1 (MaybePlaceholder e)
    splitExpr e
    e = case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
        LocalV QName
    n -> QName -> NonEmpty (MaybePlaceholder e)
    splitName QName
    n
        ExprView e
    _        -> NonEmpty (MaybePlaceholder e)
    noSplit
        where
        noSplit :: NonEmpty (MaybePlaceholder e)
    noSplit = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall el coll. Singleton el coll => el -> coll
    singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
    -> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall a b. (a -> b) -> a -> b
    $ e -> MaybePlaceholder e
    forall e. e -> MaybePlaceholder e
    noPlaceholder e
    e

        splitName :: QName -> NonEmpty (MaybePlaceholder e)
    splitName QName
    n = case NonEmpty Name -> Name
    forall a. NonEmpty a -> a
    List1.last NonEmpty Name
    ns of
          Name Range
    r NameInScope
    nis ps :: NameParts
    ps@(NamePart
    _ :| NamePart
    _ : [NamePart]
    _) -> Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> NameParts
    -> NonEmpty (MaybePlaceholder e)
    forall {e}.
    IsExpr e =>
    Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> NameParts
    -> NonEmpty (MaybePlaceholder e)
    splitParts Range
    r NameInScope
    nis (NonEmpty Name -> [Name]
    forall a. NonEmpty a -> [a]
    List1.init NonEmpty Name
    ns) PositionInName
    Beginning NameParts
    ps
          Name
    _                          -> NonEmpty (MaybePlaceholder e)
    noSplit
          where
          ns :: NonEmpty Name
    ns = QName -> NonEmpty Name
    qnameParts QName
    n

          -- Note that the same range is used for every name part. This is
          -- not entirely correct, but will hopefully not lead to any
          -- problems.

          -- Note also that the module qualifier, if any, is only applied
          -- to the first name part.

          splitParts :: Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> NameParts
    -> NonEmpty (MaybePlaceholder e)
    splitParts Range
    _ NameInScope
    _   [Name]
    _ PositionInName
    _ (NamePart
    Hole :| [])     = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall el coll. Singleton el coll => el -> coll
    singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
    -> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall a b. (a -> b) -> a -> b
    $ PositionInName -> MaybePlaceholder e
    forall e. PositionInName -> MaybePlaceholder e
    Placeholder PositionInName
    End
          splitParts Range
    r NameInScope
    nis [Name]
    m PositionInName
    _ (Id [Char]
    s :| [])     = MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall el coll. Singleton el coll => el -> coll
    singleton (MaybePlaceholder e -> NonEmpty (MaybePlaceholder e))
    -> MaybePlaceholder e -> NonEmpty (MaybePlaceholder e)
    forall a b. (a -> b) -> a -> b
    $ Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> [Char]
    -> MaybePlaceholder e
    forall {e} {t :: * -> *}.
    (IsExpr e, Foldable t) =>
    Range
    -> NameInScope
    -> t Name
    -> PositionInName
    -> [Char]
    -> MaybePlaceholder e
    part Range
    r NameInScope
    nis [Name]
    m PositionInName
    End [Char]
    s
          splitParts Range
    r NameInScope
    nis [Name]
    m PositionInName
    w (NamePart
    Hole :| NamePart
    p : [NamePart]
    ps) = PositionInName -> MaybePlaceholder e
    forall e. PositionInName -> MaybePlaceholder e
    Placeholder PositionInName
    w    MaybePlaceholder e
    -> NonEmpty (MaybePlaceholder e) -> NonEmpty (MaybePlaceholder e)
    forall a. a -> NonEmpty a -> NonEmpty a
    <| Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> NameParts
    -> NonEmpty (MaybePlaceholder e)
    splitParts Range
    r NameInScope
    nis [Name]
    m  PositionInName
    Middle (NamePart
    p NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| [NamePart]
    ps)
          splitParts Range
    r NameInScope
    nis [Name]
    m PositionInName
    w (Id [Char]
    s :| NamePart
    p : [NamePart]
    ps) = Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> [Char]
    -> MaybePlaceholder e
    forall {e} {t :: * -> *}.
    (IsExpr e, Foldable t) =>
    Range
    -> NameInScope
    -> t Name
    -> PositionInName
    -> [Char]
    -> MaybePlaceholder e
    part Range
    r NameInScope
    nis [Name]
    m PositionInName
    w [Char]
    s MaybePlaceholder e
    -> NonEmpty (MaybePlaceholder e) -> NonEmpty (MaybePlaceholder e)
    forall a. a -> NonEmpty a -> NonEmpty a
    <| Range
    -> NameInScope
    -> [Name]
    -> PositionInName
    -> NameParts
    -> NonEmpty (MaybePlaceholder e)
    splitParts Range
    r NameInScope
    nis [] PositionInName
    Middle (NamePart
    p NamePart -> [NamePart] -> NameParts
    forall a. a -> [a] -> NonEmpty a
    :| [NamePart]
    ps)

          part :: Range
    -> NameInScope
    -> t Name
    -> PositionInName
    -> [Char]
    -> MaybePlaceholder e
    part Range
    r NameInScope
    nis t Name
    m PositionInName
    w [Char]
    s =
            Maybe PositionInName -> e -> MaybePlaceholder e
    forall e. Maybe PositionInName -> e -> MaybePlaceholder e
    NoPlaceholder (PositionInName -> Maybe PositionInName
    forall a. a -> Maybe a
    Strict.Just PositionInName
    w)
                          (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 -> ExprView e
    forall e. QName -> ExprView e
    LocalV (QName -> ExprView e) -> QName -> ExprView e
    forall a b. (a -> b) -> a -> b
    $
                             (Name -> QName -> QName) -> QName -> t Name -> QName
    forall a b. (a -> b -> b) -> b -> t a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Name -> QName -> QName
    Qual (Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Range -> NameInScope -> NameParts -> Name
    Name Range
    r NameInScope
    nis (NameParts -> Name) -> NameParts -> Name
    forall a b. (a -> b) -> a -> b
    $ NamePart -> NameParts
    forall el coll. Singleton el coll => el -> coll
    singleton (NamePart -> NameParts) -> NamePart -> NameParts
    forall a b. (a -> b) -> a -> b
    $ [Char] -> NamePart
    Id [Char]
    s) t Name
    m)

    ---------------------------------------------------------------------------
    -- * Parser combinators
    ---------------------------------------------------------------------------

    ----------------------------
    -- Specific combinators

    -- | Parse a specific identifier as a NamePart
    partP :: IsExpr e => [Name] -> RawName -> Parser e Range
    partP :: forall e. IsExpr e => [Name] -> [Char] -> Parser e Range
    partP [Name]
    ms [Char]
    s =
      Doc -> Parser e Range -> Parser e Range
    forall tok a. Doc -> Parser tok a -> Parser tok a
    doc ([Char] -> Doc
    forall a. [Char] -> Doc a
    text ([Char] -> [Char]
    forall a. Show a => a -> [Char]
    show [Char]
    str)) (Parser e Range -> Parser e Range)
    -> Parser e Range -> Parser e Range
    forall a b. (a -> b) -> a -> b
    $
      (e -> Maybe Range) -> Parser e Range
    forall e a. (e -> Maybe a) -> Parser e a
    satNoPlaceholder e -> Maybe Range
    isLocal
      where
      str :: [Char]
    str = QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (QName -> [Char]) -> QName -> [Char]
    forall a b. (a -> b) -> a -> b
    $ (Name -> QName -> QName) -> QName -> [Name] -> QName
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Name -> QName -> QName
    Qual (Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleName [Char]
    s) [Name]
    ms
      isLocal :: e -> Maybe Range
    isLocal e
    e = case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
          LocalV QName
    y | [Char]
    str [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    y -> Range -> Maybe Range
    forall a. a -> Maybe a
    Just (Range -> Maybe Range) -> Range -> Maybe Range
    forall a b. (a -> b) -> a -> b
    $ QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    y
          ExprView e
    _ -> Maybe Range
    forall a. Maybe a
    Nothing

    -- | Parses a split-up, unqualified name consisting of at least two
    -- name parts.
    --
    -- The parser does not check that underscores and other name parts
    -- alternate. The range of the resulting name is the range of the
    -- first name part that is not an underscore.

    atLeastTwoParts :: IsExpr e => Parser e Name
    atLeastTwoParts :: forall e. IsExpr e => Parser e Name
    atLeastTwoParts =
      (\(Maybe (Range, NameInScope), NamePart)
    p1 [(Maybe (Range, NameInScope), NamePart)]
    ps (Maybe (Range, NameInScope), NamePart)
    p2 ->
          let all :: NonEmpty (Maybe (Range, NameInScope), NamePart)
    all = (Maybe (Range, NameInScope), NamePart)
    p1 (Maybe (Range, NameInScope), NamePart)
    -> [(Maybe (Range, NameInScope), NamePart)]
    -> NonEmpty (Maybe (Range, NameInScope), NamePart)
    forall a. a -> [a] -> NonEmpty a
    :| [(Maybe (Range, NameInScope), NamePart)]
    ps [(Maybe (Range, NameInScope), NamePart)]
    -> [(Maybe (Range, NameInScope), NamePart)]
    -> [(Maybe (Range, NameInScope), NamePart)]
    forall a. [a] -> [a] -> [a]
    ++ [(Maybe (Range, NameInScope), NamePart)
    p2] in
          case ((Maybe (Range, NameInScope), NamePart)
     -> Maybe (Range, NameInScope))
    -> NonEmpty (Maybe (Range, NameInScope), NamePart)
    -> [(Range, NameInScope)]
    forall a b. (a -> Maybe b) -> List1 a -> [b]
    List1.mapMaybe (Maybe (Range, NameInScope), NamePart)
    -> Maybe (Range, NameInScope)
    forall a b. (a, b) -> a
    fst NonEmpty (Maybe (Range, NameInScope), NamePart)
    all of
            (Range
    r,NameInScope
    nis) : [(Range, NameInScope)]
    _ -> Range -> NameInScope -> NameParts -> Name
    Name Range
    r NameInScope
    nis (((Maybe (Range, NameInScope), NamePart) -> NamePart)
    -> NonEmpty (Maybe (Range, NameInScope), NamePart) -> NameParts
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Maybe (Range, NameInScope), NamePart) -> NamePart
    forall a b. (a, b) -> b
    snd NonEmpty (Maybe (Range, NameInScope), NamePart)
    all)
            []          -> Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__)
      ((Maybe (Range, NameInScope), NamePart)
     -> [(Maybe (Range, NameInScope), NamePart)]
     -> (Maybe (Range, NameInScope), NamePart)
     -> Name)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Maybe (Range, NameInScope), NamePart)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ([(Maybe (Range, NameInScope), NamePart)]
          -> (Maybe (Range, NameInScope), NamePart) -> Name)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PositionInName
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Maybe (Range, NameInScope), NamePart)
    forall {e}.
    IsExpr e =>
    PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
    part PositionInName
    Beginning
      Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ([(Maybe (Range, NameInScope), NamePart)]
       -> (Maybe (Range, NameInScope), NamePart) -> Name)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         [(Maybe (Range, NameInScope), NamePart)]
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((Maybe (Range, NameInScope), NamePart) -> Name)
    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)
      (Maybe (Range, NameInScope), NamePart)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         [(Maybe (Range, NameInScope), NamePart)]
    forall a.
    Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) [a]
    forall (f :: * -> *) a. Alternative f => f a -> f [a]
    many (PositionInName
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Maybe (Range, NameInScope), NamePart)
    forall {e}.
    IsExpr e =>
    PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
    part PositionInName
    Middle)
      Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((Maybe (Range, NameInScope), NamePart) -> Name)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Maybe (Range, NameInScope), NamePart)
    -> Parser MemoKey e (MaybePlaceholder e) Name
    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)
         (Maybe (Range, NameInScope), NamePart)
    forall {e}.
    IsExpr e =>
    PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
    part PositionInName
    End
      where
      part :: PositionInName -> Parser e (Maybe (Range, NameInScope), NamePart)
    part PositionInName
    pos = (MaybePlaceholder e
     -> Maybe (Maybe (Range, NameInScope), NamePart))
    -> Parser e (Maybe (Range, NameInScope), NamePart)
    forall tok a. (MaybePlaceholder tok -> Maybe a) -> Parser tok a
    sat' ((MaybePlaceholder e
      -> Maybe (Maybe (Range, NameInScope), NamePart))
     -> Parser e (Maybe (Range, NameInScope), NamePart))
    -> (MaybePlaceholder e
        -> Maybe (Maybe (Range, NameInScope), NamePart))
    -> Parser e (Maybe (Range, NameInScope), NamePart)
    forall a b. (a -> b) -> a -> b
    $ \case
        Placeholder PositionInName
    pos'                   | PositionInName
    pos PositionInName -> PositionInName -> Bool
    forall a. Eq a => a -> a -> Bool
    == PositionInName
    pos' -> (Maybe (Range, NameInScope), NamePart)
    -> Maybe (Maybe (Range, NameInScope), NamePart)
    forall a. a -> Maybe a
    Just ( Maybe (Range, NameInScope)
    forall a. Maybe a
    Nothing
                                                                 , NamePart
    Hole
                                                                 )
        NoPlaceholder (Strict.Just PositionInName
    pos') e
    e | PositionInName
    pos PositionInName -> PositionInName -> Bool
    forall a. Eq a => a -> a -> Bool
    == PositionInName
    pos' ->
          case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
            LocalV (QName (Name Range
    r NameInScope
    nis (Id [Char]
    s :| []))) -> (Maybe (Range, NameInScope), NamePart)
    -> Maybe (Maybe (Range, NameInScope), NamePart)
    forall a. a -> Maybe a
    Just ((Range, NameInScope) -> Maybe (Range, NameInScope)
    forall a. a -> Maybe a
    Just (Range
    r, NameInScope
    nis), [Char] -> NamePart
    Id [Char]
    s)
            ExprView e
    _ -> Maybe (Maybe (Range, NameInScope), NamePart)
    forall a. Maybe a
    Nothing
        MaybePlaceholder e
    _ -> Maybe (Maybe (Range, NameInScope), NamePart)
    forall a. Maybe a
    Nothing

    -- | Parses a potentially pattern-matching binder

    patternBinder :: IsExpr e => Parser e Binder
    patternBinder :: forall e. IsExpr e => Parser e Binder
    patternBinder = Parser e Binder
    inOnePart Parser e Binder -> Parser e Binder -> Parser e Binder
    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
    <|> Name -> Binder
    mkBinder_ (Name -> Binder)
    -> Parser MemoKey e (MaybePlaceholder e) Name -> Parser e Binder
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser MemoKey e (MaybePlaceholder e) Name
    forall e. IsExpr e => Parser e Name
    atLeastTwoParts
      where inOnePart :: Parser e Binder
    inOnePart = (e -> Maybe Binder) -> Parser e Binder
    forall e a. (e -> Maybe a) -> Parser e a
    satNoPlaceholder ((e -> Maybe Binder) -> Parser e Binder)
    -> (e -> Maybe Binder) -> Parser e Binder
    forall a b. (a -> b) -> a -> b
    $ Pattern -> Maybe Binder
    isBinderP (Pattern -> Maybe Binder)
    -> (e -> Maybe Pattern) -> e -> Maybe Binder
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< e -> Maybe Pattern
    forall e. IsExpr e => e -> Maybe Pattern
    patternView

    -- | Used to define the return type of 'opP'.

    type family OperatorType (k :: NotationKind) (e :: Type) :: Type
    type instance OperatorType 'InfixNotation   e = MaybePlaceholder e -> MaybePlaceholder e -> e
    type instance OperatorType 'PrefixNotation  e = MaybePlaceholder e -> e
    type instance OperatorType 'PostfixNotation e = MaybePlaceholder e -> e
    type instance OperatorType 'NonfixNotation  e = e

    -- | A singleton type for 'NotationKind' (except for the constructor
    -- 'NoNotation').

    data NK (k :: NotationKind) :: Type where
      In   :: NK 'InfixNotation
      Pre  :: NK 'PrefixNotation
      Post :: NK 'PostfixNotation
      Non  :: NK 'NonfixNotation

    -- | Parse the \"operator part\" of the given notation.
    --
    -- Normal holes (but not binders) at the beginning and end are
    -- ignored.
    --
    -- If the notation does not contain any binders, then a section
    -- notation is allowed.
    opP :: forall e k. IsExpr e
        => ParseSections
        -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    opP :: forall e (k :: NotationKind).
    IsExpr e =>
    ParseSections
    -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
    opP ParseSections
    parseSections Parser e e
    p (NewNotation QName
    q Set1 Name
    names Fixity
    _ Notation
    syn Bool
    isOp) NK k
    kind =
      (((Range,
       [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)])
      -> OperatorType k e)
     -> Parser
          MemoKey
          e
          (MaybePlaceholder e)
          (Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)])
     -> Parser e (OperatorType k e))
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> ((Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)])
        -> OperatorType k e)
    -> Parser e (OperatorType k e)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
     -> OperatorType k e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> Parser e (OperatorType k e)
    forall a b.
    (a -> b)
    -> Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker (NonEmpty Name -> [Name]
    forall a. NonEmpty a -> [a]
    List1.init (NonEmpty Name -> [Name]) -> NonEmpty Name -> [Name]
    forall a b. (a -> b) -> a -> b
    $ QName -> NonEmpty Name
    qnameParts QName
    q)
                        Notation
    withoutExternalHoles) (((Range,
       [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)])
      -> OperatorType k e)
     -> Parser e (OperatorType k e))
    -> ((Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)])
        -> OperatorType k e)
    -> Parser e (OperatorType k e)
    forall a b. (a -> b) -> a -> b
    $ \(Range
    range, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    hs) ->

      let ([(MaybePlaceholder e, NamedArg (Ranged Int))]
    normal, [(LamBinding, Ranged BoundVariablePosition)]
    binders) = [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    -> ([(MaybePlaceholder e, NamedArg (Ranged Int))],
        [(LamBinding, Ranged BoundVariablePosition)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    hs
          lastHole :: Int
    lastHole          = [Int] -> Int
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ (-Int
    1) Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    : (NotationPart -> Maybe Int) -> Notation -> [Int]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe NotationPart -> Maybe Int
    holeTarget Notation
    syn

          app :: ([(MaybePlaceholder e, NamedArg (Ranged Int))] ->
                  [(MaybePlaceholder e, NamedArg (Ranged Int))]) -> e
          app :: ([(MaybePlaceholder e, NamedArg (Ranged Int))]
     -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
    -> e
    app [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    f =
            -- If we have an operator and there is exactly one
            -- placeholder for every hole, then we only return
            -- the operator.
            if Bool
    isOp Bool -> Bool -> Bool
    && OpAppArgs0 e -> Int
    noPlaceholders OpAppArgs0 e
    args Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    lastHole Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1 then
              -- Note that the information in the set "names" is thrown
              -- away here.
              ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (QName -> ExprView e
    forall e. QName -> ExprView e
    LocalV QName
    q')
            else
              OpAppArgs0 e
    -> e -> (List1 (NamedArg (MaybePlaceholder (OpApp e))) -> e) -> e
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull OpAppArgs0 e
    args
                {-then-} (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 -> ExprView e
    forall e. QName -> ExprView e
    LocalV QName
    q')
                {-else-} ((List1 (NamedArg (MaybePlaceholder (OpApp e))) -> e) -> e)
    -> (List1 (NamedArg (MaybePlaceholder (OpApp e))) -> e) -> e
    forall a b. (a -> b) -> a -> b
    $ ExprView e -> e
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView e -> e)
    -> (List1 (NamedArg (MaybePlaceholder (OpApp e))) -> ExprView e)
    -> List1 (NamedArg (MaybePlaceholder (OpApp e)))
    -> e
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName
    -> Set1 Name
    -> List1 (NamedArg (MaybePlaceholder (OpApp e)))
    -> ExprView e
    forall e. QName -> Set1 Name -> OpAppArgs' e -> ExprView e
    OpAppV QName
    q' Set1 Name
    names
            where
            args :: OpAppArgs0 e
    args = (Int -> NamedArg (MaybePlaceholder (OpApp e)))
    -> [Int] -> OpAppArgs0 e
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(LamBinding, Ranged BoundVariablePosition)]
    -> Int
    -> NamedArg (MaybePlaceholder (OpApp e))
    findExprFor ([(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    f [(MaybePlaceholder e, NamedArg (Ranged Int))]
    normal) [(LamBinding, Ranged BoundVariablePosition)]
    binders) [Int
    0..Int
    lastHole]
            q' :: QName
    q'   = Range -> QName -> QName
    forall a. SetRange a => Range -> a -> a
    setRange Range
    range QName
    q
      in

      case NK k
    kind of
        NK k
    In   -> \MaybePlaceholder e
    x MaybePlaceholder e
    y -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
     -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
    -> e
    app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
    es -> (MaybePlaceholder e
    x, NamedArg (Ranged Int)
    leadingHole) (MaybePlaceholder e, NamedArg (Ranged Int))
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    forall a. a -> [a] -> [a]
    : [(MaybePlaceholder e, NamedArg (Ranged Int))]
    es [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    forall a. [a] -> [a] -> [a]
    ++ [(MaybePlaceholder e
    y, NamedArg (Ranged Int)
    trailingHole)])
        NK k
    Pre  -> \  MaybePlaceholder e
    y -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
     -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
    -> e
    app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
    es ->                    [(MaybePlaceholder e, NamedArg (Ranged Int))]
    es [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    forall a. [a] -> [a] -> [a]
    ++ [(MaybePlaceholder e
    y, NamedArg (Ranged Int)
    trailingHole)])
        NK k
    Post -> \MaybePlaceholder e
    x   -> ([(MaybePlaceholder e, NamedArg (Ranged Int))]
     -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
    -> e
    app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
    es -> (MaybePlaceholder e
    x, NamedArg (Ranged Int)
    leadingHole) (MaybePlaceholder e, NamedArg (Ranged Int))
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(MaybePlaceholder e, NamedArg (Ranged Int))]
    forall a. a -> [a] -> [a]
    : [(MaybePlaceholder e, NamedArg (Ranged Int))]
    es)
        NK k
    Non  ->         ([(MaybePlaceholder e, NamedArg (Ranged Int))]
     -> [(MaybePlaceholder e, NamedArg (Ranged Int))])
    -> e
    app (\[(MaybePlaceholder e, NamedArg (Ranged Int))]
    es ->                    [(MaybePlaceholder e, NamedArg (Ranged Int))]
    es)

      where

      (Notation
    leadingHoles, Notation
    syn1)                  = (NotationPart -> Bool) -> Notation -> (Notation, Notation)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span    NotationPart -> Bool
    isAHole Notation
    syn
      (Notation
    withoutExternalHoles, Notation
    trailingHoles) = (NotationPart -> Bool) -> Notation -> (Notation, Notation)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    spanEnd NotationPart -> Bool
    isAHole Notation
    syn1

      leadingHole :: NamedArg (Ranged Int)
    leadingHole = case Notation
    leadingHoles of
        [HolePart Range
    _ NamedArg (Ranged Int)
    h] -> NamedArg (Ranged Int)
    h
        Notation
    _              -> NamedArg (Ranged Int)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      trailingHole :: NamedArg (Ranged Int)
    trailingHole = case Notation
    trailingHoles of
        [HolePart Range
    _ NamedArg (Ranged Int)
    h] -> NamedArg (Ranged Int)
    h
        Notation
    _              -> NamedArg (Ranged Int)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      worker ::
        [Name] -> Notation ->
        Parser e (Range, [Either (MaybePlaceholder e, NamedArg (Ranged Int))
                                 (LamBinding, Ranged BoundVariablePosition)])
      worker :: [Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker [Name]
    ms []              = (Range,
     [Either
        (MaybePlaceholder e, NamedArg (Ranged Int))
        (LamBinding, Ranged BoundVariablePosition)])
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    forall a. a -> Parser MemoKey e (MaybePlaceholder e) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Range
    forall a. Range' a
    noRange, [])
      worker [Name]
    ms (IdPart RString
    x : Notation
    xs) =
        (\Range
    r1 (Range
    r2, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es) -> (Range -> Range -> Range
    forall a. Ord a => Range' a -> Range' a -> Range' a
    fuseRanges Range
    r1 Range
    r2, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es))
          (Range
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)])
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser MemoKey e (MaybePlaceholder e) Range
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)])
          -> (Range,
              [Either
                 (MaybePlaceholder e, NamedArg (Ranged Int))
                 (LamBinding, Ranged BoundVariablePosition)]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Name] -> [Char] -> Parser MemoKey e (MaybePlaceholder e) Range
    forall e. IsExpr e => [Name] -> [Char] -> Parser e Range
    partP [Name]
    ms (RString -> [Char]
    forall a. Ranged a -> a
    rangedThing RString
    x)
          Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((Range,
        [Either
           (MaybePlaceholder e, NamedArg (Ranged Int))
           (LamBinding, Ranged BoundVariablePosition)])
       -> (Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    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
    <*> [Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker [] Notation
    xs
              -- Only the first part is qualified.
      worker [Name]
    ms (HolePart Range
    _ NamedArg (Ranged Int)
    h : Notation
    xs) =
        (\MaybePlaceholder e
    e (Range
    r, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es) -> (Range
    r, (MaybePlaceholder e, NamedArg (Ranged Int))
    -> Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)
    forall a b. a -> Either a b
    Left (MaybePlaceholder e
    e, NamedArg (Ranged Int)
    h) Either
      (MaybePlaceholder e, NamedArg (Ranged Int))
      (LamBinding, Ranged BoundVariablePosition)
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    forall a. a -> [a] -> [a]
    : [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es))
          (MaybePlaceholder e
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)])
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)])
          -> (Range,
              [Either
                 (MaybePlaceholder e, NamedArg (Ranged Int))
                 (LamBinding, Ranged BoundVariablePosition)]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe PositionInName
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) (MaybePlaceholder e)
    forall e.
    Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)
    maybePlaceholder
                (if Bool
    isOp Bool -> Bool -> Bool
    && ParseSections
    parseSections ParseSections -> ParseSections -> Bool
    forall a. Eq a => a -> a -> Bool
    == ParseSections
    ParseSections
                 then PositionInName -> Maybe PositionInName
    forall a. a -> Maybe a
    Just PositionInName
    Middle else Maybe PositionInName
    forall a. Maybe a
    Nothing)
                Parser e e
    p
          Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((Range,
        [Either
           (MaybePlaceholder e, NamedArg (Ranged Int))
           (LamBinding, Ranged BoundVariablePosition)])
       -> (Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    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
    <*> [Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker [Name]
    ms Notation
    xs
      worker [Name]
    ms (WildPart Ranged BoundVariablePosition
    h : Notation
    xs) =
        (\(Range
    r, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es) -> let anon :: Binder
    anon = Name -> Binder
    mkBinder_ Name
    simpleHole
                     in (Range
    r, (LamBinding, Ranged BoundVariablePosition)
    -> Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)
    forall a b. b -> Either a b
    Right (Ranged BoundVariablePosition
    -> Binder -> (LamBinding, Ranged BoundVariablePosition)
    forall {b} {a}. b -> Binder -> (LamBinding' a, b)
    mkBinding Ranged BoundVariablePosition
    h Binder
    anon) Either
      (MaybePlaceholder e, NamedArg (Ranged Int))
      (LamBinding, Ranged BoundVariablePosition)
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    forall a. a -> [a] -> [a]
    : [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es))
          ((Range,
      [Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)])
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker [Name]
    ms Notation
    xs
      worker [Name]
    ms (VarPart Range
    _ Ranged BoundVariablePosition
    h : Notation
    xs) = do
        (\ Binder
    b (Range
    r, [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es) -> (Range
    r, (LamBinding, Ranged BoundVariablePosition)
    -> Either
         (MaybePlaceholder e, NamedArg (Ranged Int))
         (LamBinding, Ranged BoundVariablePosition)
    forall a b. b -> Either a b
    Right (Ranged BoundVariablePosition
    -> Binder -> (LamBinding, Ranged BoundVariablePosition)
    forall {b} {a}. b -> Binder -> (LamBinding' a, b)
    mkBinding Ranged BoundVariablePosition
    h Binder
    b) Either
      (MaybePlaceholder e, NamedArg (Ranged Int))
      (LamBinding, Ranged BoundVariablePosition)
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    -> [Either
          (MaybePlaceholder e, NamedArg (Ranged Int))
          (LamBinding, Ranged BoundVariablePosition)]
    forall a. a -> [a] -> [a]
    : [Either
       (MaybePlaceholder e, NamedArg (Ranged Int))
       (LamBinding, Ranged BoundVariablePosition)]
    es))
               -- Andreas, 2011-04-07 put just 'Relevant' here, is this
               -- correct?
          (Binder
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)])
     -> (Range,
         [Either
            (MaybePlaceholder e, NamedArg (Ranged Int))
            (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser MemoKey e (MaybePlaceholder e) Binder
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         ((Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)])
          -> (Range,
              [Either
                 (MaybePlaceholder e, NamedArg (Ranged Int))
                 (LamBinding, Ranged BoundVariablePosition)]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser MemoKey e (MaybePlaceholder e) Binder
    forall e. IsExpr e => Parser e Binder
    patternBinder
          Parser
      MemoKey
      e
      (MaybePlaceholder e)
      ((Range,
        [Either
           (MaybePlaceholder e, NamedArg (Ranged Int))
           (LamBinding, Ranged BoundVariablePosition)])
       -> (Range,
           [Either
              (MaybePlaceholder e, NamedArg (Ranged Int))
              (LamBinding, Ranged BoundVariablePosition)]))
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    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
    <*> [Name]
    -> Notation
    -> Parser
         MemoKey
         e
         (MaybePlaceholder e)
         (Range,
          [Either
             (MaybePlaceholder e, NamedArg (Ranged Int))
             (LamBinding, Ranged BoundVariablePosition)])
    worker [Name]
    ms Notation
    xs

      mkBinding :: b -> Binder -> (LamBinding' a, b)
    mkBinding b
    h Binder
    b = (NamedArg Binder -> LamBinding' a
    forall a. NamedArg Binder -> LamBinding' a
    DomainFree (NamedArg Binder -> LamBinding' a)
    -> NamedArg Binder -> LamBinding' a
    forall a b. (a -> b) -> a -> b
    $ Binder -> NamedArg Binder
    forall a. a -> NamedArg a
    defaultNamedArg Binder
    b, b
    h)

      set :: b -> f (f a) -> f (f b)
    set b
    x f (f a)
    arg = (f a -> f b) -> f (f a) -> f (f b)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> b) -> f a -> f b
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (b -> a -> b
    forall a b. a -> b -> a
    const b
    x)) f (f a)
    arg

      findExprFor ::
        [(MaybePlaceholder e, NamedArg (Ranged Int))] ->
        [(LamBinding, Ranged BoundVariablePosition)] -> Int ->
        NamedArg (MaybePlaceholder (OpApp e))
      findExprFor :: [(MaybePlaceholder e, NamedArg (Ranged Int))]
    -> [(LamBinding, Ranged BoundVariablePosition)]
    -> Int
    -> NamedArg (MaybePlaceholder (OpApp e))
    findExprFor [(MaybePlaceholder e, NamedArg (Ranged Int))]
    normalHoles [(LamBinding, Ranged BoundVariablePosition)]
    binders Int
    n =
        case [ (MaybePlaceholder e, NamedArg (Ranged Int))
    h | h :: (MaybePlaceholder e, NamedArg (Ranged Int))
    h@(MaybePlaceholder e
    _, NamedArg (Ranged Int)
    m) <- [(MaybePlaceholder e, NamedArg (Ranged Int))]
    normalHoles, Ranged Int -> Int
    forall a. Ranged a -> a
    rangedThing (NamedArg (Ranged Int) -> Ranged Int
    forall a. NamedArg a -> a
    namedArg NamedArg (Ranged Int)
    m) Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n ] of
          [(Placeholder PositionInName
    p,     NamedArg (Ranged Int)
    arg)] -> MaybePlaceholder (OpApp e)
    -> NamedArg (Ranged Int) -> NamedArg (MaybePlaceholder (OpApp e))
    forall {f :: * -> *} {f :: * -> *} {b} {a}.
    (Functor f, Functor f) =>
    b -> f (f a) -> f (f b)
    set (PositionInName -> MaybePlaceholder (OpApp e)
    forall e. PositionInName -> MaybePlaceholder e
    Placeholder PositionInName
    p) NamedArg (Ranged Int)
    arg
          [(NoPlaceholder Maybe PositionInName
    _ e
    e, NamedArg (Ranged Int)
    arg)] ->
            [LamBinding]
    -> NamedArg (MaybePlaceholder (OpApp e))
    -> (List1 LamBinding -> NamedArg (MaybePlaceholder (OpApp e)))
    -> NamedArg (MaybePlaceholder (OpApp e))
    forall a b. [a] -> b -> (List1 a -> b) -> b
    List1.ifNull
              (((Int, LamBinding) -> LamBinding)
    -> [(Int, LamBinding)] -> [LamBinding]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, LamBinding) -> LamBinding
    forall a b. (a, b) -> b
    snd ([(Int, LamBinding)] -> [LamBinding])
    -> [(Int, LamBinding)] -> [LamBinding]
    forall a b. (a -> b) -> a -> b
    $
               ((Int, LamBinding) -> (Int, LamBinding) -> Ordering)
    -> [(Int, LamBinding)] -> [(Int, LamBinding)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> ((Int, LamBinding) -> Int)
    -> (Int, LamBinding)
    -> (Int, LamBinding)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Int, LamBinding) -> Int
    forall a b. (a, b) -> a
    fst)
                 [ (BoundVariablePosition -> Int
    varNumber (Ranged BoundVariablePosition -> BoundVariablePosition
    forall a. Ranged a -> a
    rangedThing Ranged BoundVariablePosition
    m), LamBinding
    b)
                 | (LamBinding
    b, Ranged BoundVariablePosition
    m) <- [(LamBinding, Ranged BoundVariablePosition)]
    binders
                 , BoundVariablePosition -> Int
    holeNumber (Ranged BoundVariablePosition -> BoundVariablePosition
    forall a. Ranged a -> a
    rangedThing Ranged BoundVariablePosition
    m) Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n
                 ])
            {-then-} (MaybePlaceholder (OpApp e)
    -> NamedArg (Ranged Int) -> NamedArg (MaybePlaceholder (OpApp e))
    forall {f :: * -> *} {f :: * -> *} {b} {a}.
    (Functor f, Functor f) =>
    b -> f (f a) -> f (f b)
    set (OpApp e -> MaybePlaceholder (OpApp e)
    forall e. e -> MaybePlaceholder e
    noPlaceholder (e -> OpApp e
    forall e. e -> OpApp e
    Ordinary e
    e)) NamedArg (Ranged Int)
    arg) -- no variable to bind
            {-else-} ((List1 LamBinding -> NamedArg (MaybePlaceholder (OpApp e)))
     -> NamedArg (MaybePlaceholder (OpApp e)))
    -> (List1 LamBinding -> NamedArg (MaybePlaceholder (OpApp e)))
    -> NamedArg (MaybePlaceholder (OpApp e))
    forall a b. (a -> b) -> a -> b
    $ \ List1 LamBinding
    bs -> MaybePlaceholder (OpApp e)
    -> NamedArg (Ranged Int) -> NamedArg (MaybePlaceholder (OpApp e))
    forall {f :: * -> *} {f :: * -> *} {b} {a}.
    (Functor f, Functor f) =>
    b -> f (f a) -> f (f b)
    set (OpApp e -> MaybePlaceholder (OpApp e)
    forall e. e -> MaybePlaceholder e
    noPlaceholder (Range -> List1 LamBinding -> e -> OpApp e
    forall e. Range -> List1 LamBinding -> e -> OpApp e
    SyntaxBindingLambda (List1 LamBinding -> e -> Range
    forall u t. (HasRange u, HasRange t) => u -> t -> Range
    fuseRange List1 LamBinding
    bs e
    e) List1 LamBinding
    bs e
    e)) NamedArg (Ranged Int)
    arg
          [(MaybePlaceholder e, NamedArg (Ranged Int))]
    _ -> NamedArg (MaybePlaceholder (OpApp e))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      noPlaceholders :: OpAppArgs0 e -> Int
      noPlaceholders :: OpAppArgs0 e -> Int
    noPlaceholders = [Int] -> Int
    forall a. Num a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Int] -> Int) -> (OpAppArgs0 e -> [Int]) -> OpAppArgs0 e -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (NamedArg (MaybePlaceholder (OpApp e)) -> Int)
    -> OpAppArgs0 e -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (MaybePlaceholder (OpApp e) -> Int
    forall {a} {e}. Num a => MaybePlaceholder e -> a
    isPlaceholder (MaybePlaceholder (OpApp e) -> Int)
    -> (NamedArg (MaybePlaceholder (OpApp e))
        -> MaybePlaceholder (OpApp e))
    -> NamedArg (MaybePlaceholder (OpApp e))
    -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (MaybePlaceholder (OpApp e)) -> MaybePlaceholder (OpApp e)
    forall a. NamedArg a -> a
    namedArg)
        where
        isPlaceholder :: MaybePlaceholder e -> a
    isPlaceholder NoPlaceholder{} = a
    0
        isPlaceholder Placeholder{}   = a
    1

    argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
    argsP :: forall e. IsExpr e => Parser e e -> Parser e [NamedArg e]
    argsP Parser e e
    p = Parser MemoKey e (MaybePlaceholder e) (NamedArg e)
    -> Parser MemoKey e (MaybePlaceholder e) [NamedArg e]
    forall a.
    Parser MemoKey e (MaybePlaceholder e) a
    -> Parser MemoKey e (MaybePlaceholder e) [a]
    forall (f :: * -> *) a. Alternative f => f a -> f [a]
    many (e -> NamedArg e
    forall {e}. IsExpr e => e -> Arg (Named_ e)
    mkArg (e -> NamedArg e)
    -> Parser e e -> Parser MemoKey e (MaybePlaceholder e) (NamedArg e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    p)
      where
      mkArg :: e -> Arg (Named_ e)
    mkArg e
    e = case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
        HiddenArgV   Named_ e
    e -> Arg (Named_ e) -> Arg (Named_ e)
    forall a. LensHiding a => a -> a
    hide (Named_ e -> Arg (Named_ e)
    forall a. a -> Arg a
    defaultArg Named_ e
    e)
        InstanceArgV Named_ e
    e -> Arg (Named_ e) -> Arg (Named_ e)
    forall a. LensHiding a => a -> a
    makeInstance (Named_ e -> Arg (Named_ e)
    forall a. a -> Arg a
    defaultArg Named_ e
    e)
        ExprView e
    _              -> Named_ e -> Arg (Named_ e)
    forall a. a -> Arg a
    defaultArg (e -> Named_ e
    forall a name. a -> Named name a
    unnamed e
    e)

    appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
    appP :: forall e.
    IsExpr e =>
    Parser e e -> Parser e [NamedArg e] -> Parser e e
    appP Parser e e
    p Parser e [NamedArg e]
    pa = (e -> NamedArg e -> e) -> e -> [NamedArg e] -> e
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl e -> NamedArg e -> e
    forall {c}. IsExpr c => c -> NamedArg c -> c
    app (e -> [NamedArg e] -> e)
    -> Parser e e
    -> Parser MemoKey e (MaybePlaceholder e) ([NamedArg e] -> e)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Parser e e
    p Parser MemoKey e (MaybePlaceholder e) ([NamedArg e] -> e)
    -> Parser e [NamedArg 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 [NamedArg e]
    pa
        where
            app :: c -> NamedArg c -> c
    app c
    e = ExprView c -> c
    forall e. IsExpr e => ExprView e -> e
    unExprView (ExprView c -> c) -> (NamedArg c -> ExprView c) -> NamedArg c -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . c -> NamedArg c -> ExprView c
    forall e. e -> NamedArg e -> ExprView e
    AppV c
    e

    atomP :: IsExpr e => (QName -> Bool) -> Parser e e
    atomP :: forall e. IsExpr e => (QName -> Bool) -> Parser e e
    atomP QName -> Bool
    p =
      Doc -> Parser e e -> Parser e e
    forall tok a. Doc -> Parser tok a -> Parser tok a
    doc Doc
    "<atom>" (Parser e e -> Parser e e) -> Parser e e -> Parser e e
    forall a b. (a -> b) -> a -> b
    $
      (e -> Maybe e) -> Parser e e
    forall e a. (e -> Maybe a) -> Parser e a
    satNoPlaceholder ((e -> Maybe e) -> Parser e e) -> (e -> Maybe e) -> Parser e e
    forall a b. (a -> b) -> a -> b
    $ \e
    e ->
      case e -> ExprView e
    forall e. IsExpr e => e -> ExprView e
    exprView e
    e of
        LocalV QName
    x | Bool -> Bool
    not (QName -> Bool
    p QName
    x) -> Maybe e
    forall a. Maybe a
    Nothing
        ExprView e
    _                    -> e -> Maybe e
    forall a. a -> Maybe a
    Just e
    e