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.Pretty ( prettyShow )

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
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [RawName -> NamePart
Id RawName
"empty"]
      qPlus :: QName
qPlus  = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [NamePart
Hole, RawName -> NamePart
Id RawName
"<|>", NamePart
Hole]
      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
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [RawName -> NamePart
Id RawName
"pure"]
      qAp :: QName
qAp   = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [NamePart
Hole, RawName -> NamePart
Id RawName
"<*>", NamePart
Hole]
      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
_ [Expr]
es -> do
      Expr
e : [Expr]
es <- Expr -> TCMT IO [Expr]
appViewM (Expr -> TCMT IO [Expr]) -> ScopeM Expr -> TCMT IO [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Expr] -> ScopeM Expr
parseApplication [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 [Expr]
appViewM :: Expr -> TCMT IO [Expr]
appViewM Expr
e =
  case Expr
e of
    App{}           -> let AppView Expr
e' [NamedArg Expr]
es = Expr -> AppView
appView Expr
e in (Expr
e' Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:) ([Expr] -> [Expr]) -> TCMT IO [Expr] -> TCMT IO [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
_ [NamedArg (MaybePlaceholder (OpApp Expr))]
es -> (QName -> Expr
Ident QName
op Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:) ([Expr] -> [Expr]) -> TCMT IO [Expr] -> TCMT IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamedArg (MaybePlaceholder (OpApp Expr)) -> ScopeM Expr)
-> [NamedArg (MaybePlaceholder (OpApp Expr))] -> 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)
-> (NamedArg (MaybePlaceholder (OpApp Expr))
    -> TCMT IO (OpApp Expr))
-> NamedArg (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))
-> (NamedArg (MaybePlaceholder (OpApp Expr))
    -> TCMT IO (MaybePlaceholder (OpApp Expr)))
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> TCMT IO (OpApp Expr)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< NamedArg (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) [NamedArg (MaybePlaceholder (OpApp Expr))]
es
    Expr
_               -> [Expr] -> TCMT IO [Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return [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 = RawName -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError RawName
"Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
    noPlaceholder :: MaybePlaceholder a -> m a
noPlaceholder Placeholder{}       = RawName -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError RawName
"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
_ = RawName -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError RawName
"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 -> RawName -> ScopeM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
RawName -> m a
genericError (RawName -> ScopeM ()) -> RawName -> ScopeM ()
forall a b. (a -> b) -> a -> b
$
      QName -> RawName
forall a. Pretty a => a -> RawName
prettyShow QName
q RawName -> RawName -> RawName
forall a. [a] -> [a] -> [a]
++ RawName
" needs to be in scope to use idiom brackets " RawName -> RawName -> RawName
forall a. [a] -> [a] -> [a]
++ Doc -> RawName
forall a. Pretty a => a -> RawName
prettyShow Doc
leftIdiomBrkt RawName -> RawName -> RawName
forall a. [a] -> [a] -> [a]
++ RawName
" ... " RawName -> RawName -> RawName
forall a. [a] -> [a] -> [a]
++ Doc -> RawName
forall a. Pretty a => a -> RawName
prettyShow Doc
rightIdiomBrkt
    ResolvedName
_ -> () -> ScopeM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()