    module Agda.Syntax.IdiomBrackets (parseIdiomBracketsSeq) where

    import Control.Monad

    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import Agda.Syntax.Concrete
    import Agda.Syntax.Concrete.Operators
    import Agda.Syntax.Concrete.Pretty ( leftIdiomBrkt, rightIdiomBrkt )

    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad
    import Agda.TypeChecking.Monad

    import Agda.Utils.List1  ( List1, pattern (:|), (<|) )
    import Agda.Utils.Pretty ( prettyShow )
    import Agda.Utils.Singleton

    parseIdiomBracketsSeq :: Range -> [Expr] -> ScopeM Expr
    parseIdiomBracketsSeq :: Range -> [Expr] -> ScopeM Expr
    parseIdiomBracketsSeq Range
    r [Expr]
    es = do
      let qEmpty :: QName
    qEmpty = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleName [Char]
    "empty"
          qPlus :: QName
    qPlus  = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleBinaryOperator [Char]
    "<|>"
          ePlus :: Expr -> Expr -> Expr
    ePlus Expr
    a Expr
    b = Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r (Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r (QName -> Expr
    Ident QName
    qPlus) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    a)) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    b)
      case [Expr]
    es of
        []       -> QName -> ScopeM ()
    ensureInScope QName
    qEmpty ScopeM () -> ScopeM Expr -> ScopeM Expr
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Expr -> ScopeM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> Expr
    Ident QName
    qEmpty)
        [Expr
    e]      -> Range -> Expr -> ScopeM Expr
    parseIdiomBrackets Range
    r Expr
    e
        es :: [Expr]
    es@(Expr
    _:[Expr]
    _) -> do
          QName -> ScopeM ()
    ensureInScope QName
    qPlus
          [Expr]
    es' <- (Expr -> ScopeM Expr) -> [Expr] -> TCMT IO [Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Range -> Expr -> ScopeM Expr
    parseIdiomBrackets Range
    r) [Expr]
    es
          Expr -> ScopeM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Expr -> Expr) -> [Expr] -> Expr
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldr1 Expr -> Expr -> Expr
    ePlus [Expr]
    es'

    parseIdiomBrackets :: Range -> Expr -> ScopeM Expr
    parseIdiomBrackets :: Range -> Expr -> ScopeM Expr
    parseIdiomBrackets Range
    r Expr
    e = do
      let qPure :: QName
    qPure = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleName [Char]
    "pure"
          qAp :: QName
    qAp   = Name -> QName
    QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    simpleBinaryOperator [Char]
    "<*>"
          ePure :: Expr -> Expr
    ePure   = Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r (QName -> Expr
    Ident QName
    qPure) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg
          eAp :: Expr -> Expr -> Expr
    eAp Expr
    a Expr
    b = Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r (Range -> Expr -> NamedArg Expr -> Expr
    App Range
    r (QName -> Expr
    Ident QName
    qAp) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    a)) (Expr -> NamedArg Expr
    forall a. a -> NamedArg a
    defaultNamedArg Expr
    b)
      (QName -> ScopeM ()) -> [QName] -> ScopeM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> ScopeM ()
    ensureInScope [QName
    qPure, QName
    qAp]
      case Expr
    e of
        RawApp Range
    _ List2 Expr
    es -> do
          Expr
    e :| [Expr]
    es <- Expr -> ScopeM (List1 Expr)
    appViewM (Expr -> ScopeM (List1 Expr)) -> ScopeM Expr -> ScopeM (List1 Expr)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< List2 Expr -> ScopeM Expr
    parseApplication List2 Expr
    es
          Expr -> ScopeM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Expr -> Expr -> Expr
    eAp (Expr -> Expr
    ePure Expr
    e) [Expr]
    es
        Expr
    _ -> Expr -> ScopeM Expr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr -> ScopeM Expr) -> Expr -> ScopeM Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr
    ePure Expr
    e

    appViewM :: Expr -> ScopeM (List1 Expr)
    appViewM :: Expr -> ScopeM (List1 Expr)
    appViewM = \case
        e :: Expr
    e@App{}         -> let AppView Expr
    e' [NamedArg Expr]
    es = Expr -> AppView
    appView Expr
    e in (Expr
    e' Expr -> [Expr] -> List1 Expr
    forall a. a -> [a] -> NonEmpty a
    :|) ([Expr] -> List1 Expr) -> TCMT IO [Expr] -> ScopeM (List1 Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamedArg Expr -> ScopeM Expr) -> [NamedArg Expr] -> TCMT IO [Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM NamedArg Expr -> ScopeM Expr
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    Arg (Named NamedName a) -> m a
    onlyVisible [NamedArg Expr]
    es
        OpApp Range
    _ QName
    op Set Name
    _ OpAppArgs
    es -> (QName -> Expr
    Ident QName
    op Expr -> [Expr] -> List1 Expr
    forall a. a -> [a] -> NonEmpty a
    :|) ([Expr] -> List1 Expr) -> TCMT IO [Expr] -> ScopeM (List1 Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
     -> ScopeM Expr)
    -> OpAppArgs -> TCMT IO [Expr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (OpApp Expr -> ScopeM Expr
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    OpApp a -> m a
    ordinary (OpApp Expr -> ScopeM Expr)
    -> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
        -> TCMT IO (OpApp Expr))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
    -> ScopeM Expr
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< MaybePlaceholder (OpApp Expr) -> TCMT IO (OpApp Expr)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    MaybePlaceholder a -> m a
    noPlaceholder (MaybePlaceholder (OpApp Expr) -> TCMT IO (OpApp Expr))
    -> (Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
        -> TCMT IO (MaybePlaceholder (OpApp Expr)))
    -> Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
    -> TCMT IO (OpApp Expr)
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Arg (Named NamedName (MaybePlaceholder (OpApp Expr)))
    -> TCMT IO (MaybePlaceholder (OpApp Expr))
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    Arg (Named NamedName a) -> m a
    onlyVisible) OpAppArgs
    es
        Expr
    e               -> List1 Expr -> ScopeM (List1 Expr)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (List1 Expr -> ScopeM (List1 Expr))
    -> List1 Expr -> ScopeM (List1 Expr)
    forall a b. (a -> b) -> a -> b
    $ Expr -> List1 Expr
    forall el coll. Singleton el coll => el -> coll
    singleton Expr
    e
      where
        onlyVisible :: Arg (Named NamedName a) -> m a
    onlyVisible Arg (Named NamedName a)
    a
          | () -> NamedArg ()
    forall a. a -> NamedArg a
    defaultNamedArg () NamedArg () -> NamedArg () -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Named NamedName a -> Named NamedName ())
    -> Arg (Named NamedName a) -> NamedArg ()
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (() () -> Named NamedName a -> Named NamedName ()
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) Arg (Named NamedName a)
    a = a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> m a) -> a -> m a
    forall a b. (a -> b) -> a -> b
    $ Arg (Named NamedName a) -> a
    forall a. NamedArg a -> a
    namedArg Arg (Named NamedName a)
    a
          | Bool
    otherwise = [Char] -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError [Char]
    "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
        noPlaceholder :: MaybePlaceholder a -> m a
    noPlaceholder Placeholder{}       = [Char] -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError [Char]
    "Naked sections are not allowed in idiom brackets"
        noPlaceholder (NoPlaceholder Maybe PositionInName
    _ a
    x) = a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

        ordinary :: OpApp a -> m a
    ordinary (Ordinary a
    a) = a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
        ordinary OpApp a
    _ = [Char] -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError [Char]
    "Binding syntax is not allowed in idiom brackets"

    ensureInScope :: QName -> ScopeM ()
    ensureInScope :: QName -> ScopeM ()
    ensureInScope QName
    q = do
      ResolvedName
    r <- QName -> ScopeM ResolvedName
    resolveName QName
    q
      case ResolvedName
    r of
        ResolvedName
    UnknownName -> [Char] -> ScopeM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> ScopeM ()) -> [Char] -> ScopeM ()
    forall a b. (a -> b) -> a -> b
    $
          QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " needs to be in scope to use idiom brackets " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Doc
    leftIdiomBrkt [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " ... " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Doc
    rightIdiomBrkt
        ResolvedName
    _ -> () -> ScopeM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()