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 forall a b. (a -> b) -> a -> b
$ [Char] -> Name
simpleName [Char]
"empty"
      qPlus :: QName
qPlus  = Name -> QName
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) (forall a. a -> NamedArg a
defaultNamedArg Expr
a)) (forall a. a -> NamedArg a
defaultNamedArg Expr
b)
  case [Expr]
es of
    []       -> QName -> ScopeM ()
ensureInScope QName
qEmpty forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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' <- 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ [Char] -> Name
simpleName [Char]
"pure"
      qAp :: QName
qAp   = Name -> QName
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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) (forall a. a -> NamedArg a
defaultNamedArg Expr
a)) (forall a. a -> NamedArg a
defaultNamedArg Expr
b)
  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 -> TCMT IO (List1 Expr)
appViewM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< List2 Expr -> ScopeM Expr
parseApplication List2 Expr
es
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Expr -> Expr
ePure Expr
e

appViewM :: Expr -> ScopeM (List1 Expr)
appViewM :: Expr -> TCMT IO (List1 Expr)
appViewM = \case
    e :: Expr
e@App{}         -> let AppView Expr
e' [NamedArg Expr]
es = Expr -> AppView
appView Expr
e in (Expr
e' forall a. a -> [a] -> NonEmpty a
:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 forall a. a -> [a] -> NonEmpty a
:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
OpApp a -> m a
ordinary forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
MaybePlaceholder a -> m a
noPlaceholder forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Arg (Named NamedName a) -> m a
onlyVisible) OpAppArgs
es
    Expr
e               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
      | forall a. a -> NamedArg a
defaultNamedArg () forall a. Eq a => a -> a -> Bool
== forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) Arg (Named NamedName a)
a = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg Arg (Named NamedName a)
a
      | Bool
otherwise = 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{}       = 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) = forall (m :: * -> *) a. Monad m => a -> m a
return a
x

    ordinary :: OpApp a -> m a
ordinary (Ordinary a
a) = forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    ordinary OpApp 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 -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$
      forall a. Pretty a => a -> [Char]
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ [Char]
" needs to be in scope to use idiom brackets " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Doc
leftIdiomBrkt forall a. [a] -> [a] -> [a]
++ [Char]
" ... " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Doc
rightIdiomBrkt
    ResolvedName
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()