module Agda.Interaction.Command.Internal.Parser where

import Agda.Syntax.Abstract (Expr)
import Agda.Syntax.Common (InteractionId (..))
import Agda.Syntax.Parser (exprParser, parse, parsePosString)
import Agda.Syntax.Position (getRange, noRange, rStart)
import Agda.Syntax.Translation.ConcreteToAbstract
  (checkCohesionAttributes, concreteToAbstract, localToAbstract)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupLocalMeta, withInteractionId)
import Agda.TypeChecking.Warnings (runPM)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Pretty (text)
import Control.Monad.Except (MonadError(..))
import Data.ByteString (ByteString)
import Data.Maybe (fromMaybe)
import Text.Read (readMaybe)

import qualified Data.ByteString.Char8 as BS8

metaParseExpr ::  InteractionId -> ByteString -> TCM Expr
metaParseExpr :: InteractionId -> ByteString -> TCM Expr
metaParseExpr InteractionId
ii ByteString
s =
    do  MetaId
m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        ScopeInfo
scope <- MetaVariable -> ScopeInfo
getMetaScope (MetaVariable -> ScopeInfo)
-> TCMT IO MetaVariable -> TCMT IO ScopeInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        Range
r <- MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange (MetaVariable -> Range) -> TCMT IO MetaVariable -> TCMT IO Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        -- liftIO $ putStrLn $ prettyShow scope
        let pos :: Position' SrcFile
pos = Position' SrcFile -> Maybe (Position' SrcFile) -> Position' SrcFile
forall a. a -> Maybe a -> a
fromMaybe (Position' SrcFile
forall a. HasCallStack => a
__IMPOSSIBLE__) (Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range
r)
        (Expr
e, CohesionAttributes
coh) <- PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a. PM a -> TCM a
runPM (PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes))
-> PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Position' SrcFile -> String -> PM (Expr, CohesionAttributes)
forall a.
Parser a
-> Position' SrcFile -> String -> PM (a, CohesionAttributes)
parsePosString Parser Expr
exprParser Position' SrcFile
pos (ByteString -> String
BS8.unpack ByteString
s)
        CohesionAttributes -> ScopeM ()
checkCohesionAttributes CohesionAttributes
coh
        ScopeInfo -> Expr -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
concreteToAbstract ScopeInfo
scope Expr
e

actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta :: [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta (ByteString
is:[ByteString]
es) InteractionId -> Expr -> TCM a
f =
     do  Nat
i <- String -> TCM Nat
forall a. Read a => String -> TCM a
readM (ByteString -> String
BS8.unpack ByteString
is)
         let ii :: InteractionId
ii = Nat -> InteractionId
InteractionId Nat
i
         Expr
e <- InteractionId -> ByteString -> TCM Expr
metaParseExpr InteractionId
ii ([ByteString] -> ByteString
BS8.unwords [ByteString]
es)
         InteractionId -> TCM a -> TCM a
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ InteractionId -> Expr -> TCM a
f InteractionId
ii Expr
e
actOnMeta [ByteString]
_ InteractionId -> Expr -> TCM a
_ = TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__

parseExpr :: String -> TCM Expr
parseExpr :: String -> TCM Expr
parseExpr String
s = do
    (Expr
e, CohesionAttributes
coh) <- PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a. PM a -> TCM a
runPM (PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes))
-> PM (Expr, CohesionAttributes) -> TCM (Expr, CohesionAttributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr -> String -> PM (Expr, CohesionAttributes)
forall a. Parser a -> String -> PM (a, CohesionAttributes)
parse Parser Expr
exprParser String
s
    CohesionAttributes -> ScopeM ()
checkCohesionAttributes CohesionAttributes
coh
    Expr -> (AbsOfCon Expr -> TCM Expr) -> TCM Expr
forall c b.
ToAbstract c =>
c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
localToAbstract Expr
e AbsOfCon Expr -> TCM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return

readM :: Read a => String -> TCM a
readM :: String -> TCM a
readM String
s = TCM a -> (a -> TCM a) -> Maybe a -> TCM a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM a
forall a. TCMT IO a
err a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> TCM a) -> Maybe a -> TCM a
forall a b. (a -> b) -> a -> b
$ String -> Maybe a
forall a. Read a => String -> Maybe a
readMaybe String
s
  where
  err :: TCMT IO a
err    = TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> TCMT IO a) -> TCErr -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TCErr
strMsg (String -> TCErr) -> String -> TCErr
forall a b. (a -> b) -> a -> b
$ String
"Cannot parse: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
  strMsg :: String -> TCErr
strMsg = Range -> Doc -> TCErr
Exception Range
forall a. Range' a
noRange (Doc -> TCErr) -> (String -> Doc) -> String -> TCErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text