-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ
{-|
Implements an REPL that can execute Morley instructions.  REPL starts with an
empty stack. At each instruction entered, the modified stack, or an error is
printed. Multiple instructions separated by semicolons should work as expected.
Available meta commads are:

 ':help', displays this help\n ':stack', prints the current stack
 ':loadstack filename', loads the stack from a file
 ':dumpstack filename', dumps the stack to a file
 ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."
-}
module REPL
  ( runRepl
  ) where

import qualified Data.Aeson as Aeson
import qualified Data.ByteString.Lazy as BSL
import Data.List (stripPrefix)
import Data.Text (strip)
import Data.Typeable (cast)
import Data.Vinyl (Rec(..))
import Fmt (pretty)
import System.Console.Haskeline
import Text.Megaparsec (parse)

import Michelson.Interpret (ContractEnv(..), interpretInstr)
import Michelson.Macro (ParsedOp, expandList)
import Michelson.Parser (errorBundlePretty, ops, parseExpandValue, type_)
import Michelson.Parser.Types (noLetEnv)
import Michelson.Printer (printDoc, printTypedValue)
import Michelson.Printer.Util (doesntNeedParens)
import Michelson.Runtime.GState (genesisAddress)
import Michelson.TypeCheck (SomeInstr(..), SomeInstrOut(..), getWTP, runTypeCheckIsolated)
import Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter)
import Michelson.TypeCheck.Types (HST(..), NotWellTyped(..))
import qualified Michelson.Typed as T
import qualified Michelson.Untyped as U
import Tezos.Core (Timestamp(..), dummyChainId, unsafeMkMutez)

data SomeStack = forall t. Typeable t => SomeStack
  { stValues :: (Rec T.Value t)
  , stTypes :: HST t
  }

type ReplM = InputT (StateT SomeStack IO)

runRepl :: IO ()
runRepl = evalStateT (runInputT defaultSettings repl) emptyStack

-- | Prints an error message to stderr
printErr :: (MonadIO m) => Text -> m ()
printErr m = liftIO $ hPutStrLn stderr m

-- | Read commands or instructions from stdin and executes them.
-- If user presses Ctrl-c during execution of an instruction, it will be
-- caught and handled here itself. This ensures that REPL does not crash as
-- a result of user pressing Ctrl-c in an attempt to end a loop.
repl :: ReplM ()
repl = do
  printHelp
  repl_

repl_ :: ReplM ()
repl_ = do
   minput <- getInputLine "Morley>>> "
   case strStrip <$> minput of
     Nothing -> pass -- Ctrl D
     Just ":quit" -> pass
     Just input -> do
      case input of
        "" -> pass
        ":clear" -> lift $ put emptyStack
        ":stack" -> printStack
        (stripPrefix ":dumpstack" -> Just filename) ->
          dumpStackToFile $ toString $ strip $ toText filename
        (stripPrefix ":loadstack" -> Just filename) ->
          loadStackFromFile $ toString $ strip $ toText filename
        ":help" -> printHelp
        (stripPrefix ":" -> Just cmd) ->
          printErr $ "Unknown command`"<> (toText cmd) <> "`. Use :help to see a list of commands"
        _ -> handle (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input)
      repl_
  where
    strStrip = toString . strip . toText

-- | Try to execute the given input string as a Morley instruction.
runCode :: Text -> ReplM ()
runCode code = do
  case parseInstructions code of
    Left err -> printErr err
    Right [] -> pass
    Right parsedOps -> do
      let expandedOps = expandList parsedOps
      lift get >>= \case
        SomeStack {..} -> case cast stTypes of
          Just hstInp -> case runTypeCheckIsolated $ typeCheckList expandedOps hstInp of
            Right someInstr -> do
              case someInstr of
                _ :/ (instr ::: hstOut)-> case interpretInstr dummyContractEnv instr stValues of
                  Right recOut -> do
                    lift $ put (SomeStack recOut hstOut)
                    printStack
                  Left michelsonFail -> putTextLn (pretty michelsonFail)
                _ :/ (AnyOutInstr _) -> putTextLn "Encountered a FAILWITH instruction"
            Left err -> printErr $ show err
          Nothing -> printErr "Casting stack failed"

dummyContractEnv :: ContractEnv
dummyContractEnv = ContractEnv
  { ceNow = Timestamp 100
  , ceMaxSteps = 100500
  , ceBalance = unsafeMkMutez 100
  , ceContracts = mempty
  , ceSelf = genesisAddress
  , ceSource = genesisAddress
  , ceSender = genesisAddress
  , ceAmount = unsafeMkMutez 100
  , ceChainId = dummyChainId
  , ceOperationHash = Nothing
  , ceGlobalCounter = 0
  }

printHelp :: ReplM ()
printHelp = putTextLn "REPL starts with an empty stack. At each instruction entered,\
  \ the modified stack, or an error is printed. Multiple instructions separated by semicolons should work\
  \ as expected. Available meta commads are:\n\
  \ ':help', displays this help\n ':stack', prints the current stack\n\
  \ ':loadstack filename', loads the stack from a file\n\
  \ ':dumpstack filename', dumps the stack to a file \n\
  \ ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."

printStack :: ReplM ()
printStack = lift get >>= \case
  SomeStack stk hst -> do
    putTextLn "--"
    putTextLn $ showStack stk hst

emptyStack :: SomeStack
emptyStack = SomeStack RNil SNil

parseInstructions :: Text -> Either Text [ParsedOp]
parseInstructions src = let
  codeParser = runReaderT ops noLetEnv
  in case parse codeParser "" src of
    Right p -> Right p
    Left err -> Left (toText $ errorBundlePretty err)

-- helpers

addValueToHST
  :: forall t xs. Typeable xs
  => T.Value t
  -> HST xs
  -> Either Text (T.Dict (Typeable (t ': xs)), HST (t ': xs))
addValueToHST v hstIn = case T.valueTypeSanity v of
  T.Dict -> case getWTP @t of
    Right wtpDict -> Right (T.Dict, (T.starNotes @t, wtpDict, U.noAnn) ::&  hstIn)
    Left (NotWellTyped t) -> let
      U.Type t' tann = T.toUType t
      in Left $ "Value of type '" <> (renderT t' (U.fullAnnSet [tann] [] []))
                <> "' is not well typed in the provided Value."

renderType :: T.SingI t => T.Notes t -> U.VarAnn -> Text
renderType notes vann = let
  U.Type t tann = T.mkUType notes
  in renderT t (U.fullAnnSet [tann] [] [vann])

renderT :: U.T -> U.AnnotationSet -> Text
renderT t annSet = toText $ printDoc True $ U.renderType t True doesntNeedParens annSet

dumpStackToFile :: FilePath -> ReplM ()
dumpStackToFile fname =
 lift get >>= \case
  SomeStack stk hst -> case dumpStack stk hst of
    Right stkd -> liftIO $ Prelude.catch (BSL.writeFile fname $ Aeson.encode stkd) handler
    Left err -> printErr err
  where
    handler :: IOException -> IO ()
    handler e = printErr $ toText $ displayException e

loadStackFromFile :: FilePath -> ReplM ()
loadStackFromFile fname = do
  mStack <- liftIO $ flip Prelude.catch handler $ do
    stackTxt <- BSL.readFile fname
    case Aeson.decode @[(Text, Text)] stackTxt of
      Just s -> pure $ loadStack s
      Nothing -> pure $ Left "Decoding error when parsing stack data from file"
  case mStack of
    Right stk -> lift $ put stk
    Left err -> printErr err
  where
    handler :: IOException -> IO (Either Text a)
    handler e = pure $ Left $ toText $ displayException e

-- | Dump stack as a lit of tuples that represent (value, type) pairs.
dumpStack :: forall t. Rec T.Value t -> HST t -> Either Text [(Text, Text)]
dumpStack RNil _ = Right []
dumpStack ((v :: T.Value a) :& rst) ((notes, _, vann) ::& rHst) = case T.valueTypeSanity v of
  T.Dict -> case T.checkOpPresence (T.sing @a) of
    T.OpAbsent -> case dumpStack rst rHst of
      Right t -> Right ((toText $ printTypedValue True v, renderType notes vann) : t)
      Left e -> Left e
    T.OpPresent ->  Left "Cannot dump stack with operations"

-- | Overwrite the current stack with a stack loaded from a list of tuples
-- representing (value/type) pairs.
loadStack :: [(Text, Text)] -> Either Text SomeStack
loadStack = foldl' buildStack (Right emptyStack) . reverse
  where
    buildStack :: Either Text SomeStack -> (Text, Text) -> Either Text SomeStack
    buildStack (Left err) _ = Left err
    buildStack (Right (SomeStack stk hst)) (txVal, txTyp) = case
      (parseExpandValue txVal, parse (runReaderT type_ noLetEnv) "" txTyp) of
        (Right val, Right typ) ->
          case typeCheckParameter mempty typ val of
            Right (T.SomeValue tVal) ->
              case addValueToHST tVal hst of
                Right (T.Dict, newHst) -> Right $ SomeStack (tVal :& stk) newHst
                Left err -> Left err
            Left tcError -> Left $ show tcError
        (Left err, _) -> Left $ pretty err
        (_, Left err) -> Left $ toText $ errorBundlePretty err

showStack :: forall t. Rec T.Value t -> HST t -> Text
showStack RNil _ = "--"
showStack ((v :: T.Value a) :& rst) ((notes, _, vann) ::& rHst)  = case T.valueTypeSanity v of
  T.Dict -> case T.checkOpPresence (T.sing @a) of
    T.OpAbsent -> -- print nice if value has no operations
      addSuffix (toText $ printTypedValue True v)
    _ ->          -- else just call show, and indicate value has operation inside
      case (v, T.sing @a) of
        (T.VList [], T.STList T.STOperation) -> "{ } :: list operation\n" <> showStack rst rHst
        _ -> addSuffix $ "(operations container:" <> show v <> ")"
  where
    addSuffix val = val <>" :: " <> renderType notes vann <> "\n" <> showStack rst rHst