    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.Syntax.Common.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 a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Expr -> ScopeM Expr
    forall a. a -> TCMT IO a
    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
          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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Range -> Expr -> ScopeM Expr
    parseIdiomBrackets Range
    r) [Expr]
    es
          return $ foldr1 ePlus 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
          e :| 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
          return $ foldl eAp (ePure e) es
        Expr
    _ -> Expr -> ScopeM Expr
    forall a. a -> TCMT IO a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM NamedArg Expr -> ScopeM Expr
    forall {a}. Arg (Named NamedName a) -> TCMT IO a
    onlyVisible [NamedArg Expr]
    es
        OpApp Range
    _ QName
    op Set1 Name
    _ OpAppArgs
    es -> (QName -> Expr
    Ident QName
    op Expr -> List1 Expr -> List1 Expr
    forall a. a -> NonEmpty a -> NonEmpty a
    <|) (List1 Expr -> List1 Expr)
    -> ScopeM (List1 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 -> ScopeM (List1 Expr)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> NonEmpty a -> m (NonEmpty b)
    mapM (OpApp Expr -> ScopeM Expr
    forall {a}. OpApp a -> TCMT IO 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 {a}. MaybePlaceholder a -> ScopeM 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 {a}. Arg (Named NamedName a) -> TCMT IO a
    onlyVisible) OpAppArgs
    es
        Expr
    e               -> List1 Expr -> ScopeM (List1 Expr)
    forall a. a -> TCMT IO a
    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) -> TCMT IO 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 a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (() () -> Named NamedName a -> Named NamedName ()
    forall a b. a -> Named NamedName b -> Named NamedName a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) Arg (Named NamedName a)
    a = a -> TCMT IO a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> TCMT IO a) -> a -> TCMT IO 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] -> TCMT IO a
    forall a. [Char] -> ScopeM a
    idiomBracketError [Char]
    "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
        noPlaceholder :: MaybePlaceholder a -> ScopeM a
    noPlaceholder Placeholder{}       = [Char] -> ScopeM a
    forall a. [Char] -> ScopeM a
    idiomBracketError [Char]
    "Naked sections are not allowed in idiom brackets"
        noPlaceholder (NoPlaceholder Maybe PositionInName
    _ a
    x) = a -> ScopeM a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

        ordinary :: OpApp a -> TCMT IO a
    ordinary (Ordinary a
    a) = a -> TCMT IO a
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
        ordinary OpApp a
    _ = [Char] -> TCMT IO a
    forall a. [Char] -> ScopeM a
    idiomBracketError [Char]
    "Binding syntax is not allowed in idiom brackets"

    ensureInScope :: QName -> ScopeM ()
    ensureInScope :: QName -> ScopeM ()
    ensureInScope QName
    q = do
      r <- QName -> ScopeM ResolvedName
    resolveName QName
    q
      case r of
        ResolvedName
    UnknownName -> [Char] -> ScopeM ()
    forall a. [Char] -> ScopeM a
    idiomBracketError ([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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    idiomBracketError :: String -> ScopeM a
    idiomBracketError :: forall a. [Char] -> ScopeM a
    idiomBracketError = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a)
    -> ([Char] -> TypeError) -> [Char] -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> TypeError
    IdiomBracketError