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
      [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Range -> Expr -> ScopeM Expr
parseIdiomBrackets Range
r) [Expr]
es
      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 -> Expr) -> [Expr] -> Expr
forall a. (a -> a -> a) -> [a] -> a
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 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 -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> 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
_ -> 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 {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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 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) -> 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 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 -> m a
forall 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 a. 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 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()