{-|
Copyright        : (c) Galois, Inc. 2025
Maintainer       : Langston Barrett <langston@galois.com>
-}

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.Debug.Inputs
  ( Inputs
  , recv
  , fail
  , parseInputs
  , parseInputsWithRetry
  , addPrompt
  , prepend
  , defaultDebuggerInputs
  ) where

import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad qualified as Monad
import Control.Monad.Reader qualified as Reader
import Control.Monad.Trans (MonadTrans(lift))
import Data.Char qualified as Char
import Data.Functor.Contravariant (contramap)
import Data.IORef qualified as IORef
import Data.Text.IO qualified as IO
import Data.Text qualified as Text
import Data.Text (Text)
import Lang.Crucible.Debug.Command (CommandExt)
import Lang.Crucible.Debug.Complete (CompletionT)
import Lang.Crucible.Debug.Complete qualified as Complete
import Lang.Crucible.Debug.Outputs (Outputs)
import Lang.Crucible.Debug.Outputs qualified as Outs
import Lang.Crucible.Debug.Statement qualified as Stmt
import Lang.Crucible.Debug.Statement (Statement, ParseError, renderParseError)
import Lang.Crucible.Debug.Style qualified as Style
import Lang.Crucible.Debug.Style (StyleT)
import Prelude hiding (fail)
import System.Console.Isocline qualified as Isocline
import System.IO (Handle, hFlush, stdout)

newtype Inputs m a = Inputs { forall (m :: * -> *) a. Inputs m a -> m a
recv :: m a }
  deriving (Functor (Inputs m)
Functor (Inputs m) =>
(forall a. a -> Inputs m a)
-> (forall a b. Inputs m (a -> b) -> Inputs m a -> Inputs m b)
-> (forall a b c.
    (a -> b -> c) -> Inputs m a -> Inputs m b -> Inputs m c)
-> (forall a b. Inputs m a -> Inputs m b -> Inputs m b)
-> (forall a b. Inputs m a -> Inputs m b -> Inputs m a)
-> Applicative (Inputs m)
forall a. a -> Inputs m a
forall a b. Inputs m a -> Inputs m b -> Inputs m a
forall a b. Inputs m a -> Inputs m b -> Inputs m b
forall a b. Inputs m (a -> b) -> Inputs m a -> Inputs m b
forall a b c.
(a -> b -> c) -> Inputs m a -> Inputs m b -> Inputs m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *). Applicative m => Functor (Inputs m)
forall (m :: * -> *) a. Applicative m => a -> Inputs m a
forall (m :: * -> *) a b.
Applicative m =>
Inputs m a -> Inputs m b -> Inputs m a
forall (m :: * -> *) a b.
Applicative m =>
Inputs m a -> Inputs m b -> Inputs m b
forall (m :: * -> *) a b.
Applicative m =>
Inputs m (a -> b) -> Inputs m a -> Inputs m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> Inputs m a -> Inputs m b -> Inputs m c
$cpure :: forall (m :: * -> *) a. Applicative m => a -> Inputs m a
pure :: forall a. a -> Inputs m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
Inputs m (a -> b) -> Inputs m a -> Inputs m b
<*> :: forall a b. Inputs m (a -> b) -> Inputs m a -> Inputs m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> Inputs m a -> Inputs m b -> Inputs m c
liftA2 :: forall a b c.
(a -> b -> c) -> Inputs m a -> Inputs m b -> Inputs m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
Inputs m a -> Inputs m b -> Inputs m b
*> :: forall a b. Inputs m a -> Inputs m b -> Inputs m b
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
Inputs m a -> Inputs m b -> Inputs m a
<* :: forall a b. Inputs m a -> Inputs m b -> Inputs m a
Applicative, (forall a b. (a -> b) -> Inputs m a -> Inputs m b)
-> (forall a b. a -> Inputs m b -> Inputs m a)
-> Functor (Inputs m)
forall a b. a -> Inputs m b -> Inputs m a
forall a b. (a -> b) -> Inputs m a -> Inputs m b
forall (m :: * -> *) a b.
Functor m =>
a -> Inputs m b -> Inputs m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Inputs m a -> Inputs m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Inputs m a -> Inputs m b
fmap :: forall a b. (a -> b) -> Inputs m a -> Inputs m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> Inputs m b -> Inputs m a
<$ :: forall a b. a -> Inputs m b -> Inputs m a
Functor, Applicative (Inputs m)
Applicative (Inputs m) =>
(forall a b. Inputs m a -> (a -> Inputs m b) -> Inputs m b)
-> (forall a b. Inputs m a -> Inputs m b -> Inputs m b)
-> (forall a. a -> Inputs m a)
-> Monad (Inputs m)
forall a. a -> Inputs m a
forall a b. Inputs m a -> Inputs m b -> Inputs m b
forall a b. Inputs m a -> (a -> Inputs m b) -> Inputs m b
forall (m :: * -> *). Monad m => Applicative (Inputs m)
forall (m :: * -> *) a. Monad m => a -> Inputs m a
forall (m :: * -> *) a b.
Monad m =>
Inputs m a -> Inputs m b -> Inputs m b
forall (m :: * -> *) a b.
Monad m =>
Inputs m a -> (a -> Inputs m b) -> Inputs m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
Inputs m a -> (a -> Inputs m b) -> Inputs m b
>>= :: forall a b. Inputs m a -> (a -> Inputs m b) -> Inputs m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
Inputs m a -> Inputs m b -> Inputs m b
>> :: forall a b. Inputs m a -> Inputs m b -> Inputs m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> Inputs m a
return :: forall a. a -> Inputs m a
Monad)

instance MonadFail m => MonadFail (Inputs m) where
  fail :: forall a. String -> Inputs m a
fail = m a -> Inputs m a
forall (m :: * -> *) a. m a -> Inputs m a
Inputs (m a -> Inputs m a) -> (String -> m a) -> String -> Inputs m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Monad.fail

instance MonadIO m => MonadIO (Inputs m) where
  liftIO :: forall a. IO a -> Inputs m a
liftIO = m a -> Inputs m a
forall (m :: * -> *) a. m a -> Inputs m a
Inputs (m a -> Inputs m a) -> (IO a -> m a) -> IO a -> Inputs m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

instance MonadTrans Inputs where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Inputs m a
lift = m a -> Inputs m a
forall (m :: * -> *) a. m a -> Inputs m a
Inputs

fail :: MonadFail m => Inputs m a
fail :: forall (m :: * -> *) a. MonadFail m => Inputs m a
fail = String -> Inputs m a
forall a. String -> Inputs m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Monad.fail String
"No more inputs"

addPrompt :: Handle -> Text -> Inputs IO a -> Inputs IO a
addPrompt :: forall a. Handle -> Text -> Inputs IO a -> Inputs IO a
addPrompt Handle
hOut Text
prompt (Inputs IO a
inps) =
  IO a -> Inputs IO a
forall (m :: * -> *) a. m a -> Inputs m a
Inputs (IO a -> Inputs IO a) -> IO a -> Inputs IO a
forall a b. (a -> b) -> a -> b
$ do
    Handle -> Text -> IO ()
IO.hPutStr Handle
hOut Text
prompt
    Handle -> IO ()
hFlush Handle
hOut
    IO a
inps

prepend :: MonadIO m => [a] -> Inputs m a -> IO (Inputs m a)
prepend :: forall (m :: * -> *) a.
MonadIO m =>
[a] -> Inputs m a -> IO (Inputs m a)
prepend [a]
inps (Inputs m a
rest) = do
  IORef [a]
inpsRef <- [a] -> IO (IORef [a])
forall a. a -> IO (IORef a)
IORef.newIORef [a]
inps
  Inputs m a -> IO (Inputs m a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m a -> Inputs m a
forall (m :: * -> *) a. m a -> Inputs m a
Inputs (IORef [a] -> m a
go IORef [a]
inpsRef))
  where
  go :: IORef [a] -> m a
go IORef [a]
inpsRef = do
    [a]
is <- IO [a] -> m [a]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IORef [a] -> IO [a]
forall a. IORef a -> IO a
IORef.readIORef IORef [a]
inpsRef)
    case [a]
is of
      [] -> m a
rest
      (a
i:[a]
is') -> do
        IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IORef [a] -> [a] -> IO ()
forall a. IORef a -> a -> IO ()
IORef.writeIORef IORef [a]
inpsRef [a]
is')
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
i

parseInputs ::
  MonadFail m =>
  CommandExt cExt ->
  Inputs m Text ->
  Inputs m (Statement cExt)
parseInputs :: forall (m :: * -> *) cExt.
MonadFail m =>
CommandExt cExt -> Inputs m Text -> Inputs m (Statement cExt)
parseInputs CommandExt cExt
cExts (Inputs m Text
inps) = m (Statement cExt) -> Inputs m (Statement cExt)
forall (m :: * -> *) a. m a -> Inputs m a
Inputs m (Statement cExt)
go
  where
    go :: m (Statement cExt)
go = do
      Text
txt <- m Text
inps
      case CommandExt cExt -> Text -> Either ParseError (Statement cExt)
forall cExt.
CommandExt cExt -> Text -> Either ParseError (Statement cExt)
Stmt.parse CommandExt cExt
cExts Text
txt of
        Left ParseError
err -> String -> m (Statement cExt)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Monad.fail (ParseError -> String
forall a. Show a => a -> String
show ParseError
err)
        Right Statement cExt
r -> Statement cExt -> m (Statement cExt)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Statement cExt
r

parseInputsWithRetry ::
  Monad m =>
  CommandExt cExt ->
  Inputs m Text ->
  Outputs m ParseError ->
  Inputs m (Statement cExt)
parseInputsWithRetry :: forall (m :: * -> *) cExt.
Monad m =>
CommandExt cExt
-> Inputs m Text
-> Outputs m ParseError
-> Inputs m (Statement cExt)
parseInputsWithRetry CommandExt cExt
cExts (Inputs m Text
inps) Outputs m ParseError
errs = m (Statement cExt) -> Inputs m (Statement cExt)
forall (m :: * -> *) a. m a -> Inputs m a
Inputs m (Statement cExt)
go
  where
    go :: m (Statement cExt)
go = do
      Text
txt <- m Text
inps
      case CommandExt cExt -> Text -> Either ParseError (Statement cExt)
forall cExt.
CommandExt cExt -> Text -> Either ParseError (Statement cExt)
Stmt.parse CommandExt cExt
cExts Text
txt of
        Left ParseError
err -> do
          Outputs m ParseError -> ParseError -> m ()
forall (m :: * -> *) a. Outputs m a -> a -> m ()
Outs.send Outputs m ParseError
errs ParseError
err
          m (Statement cExt)
go
        Right Statement cExt
r -> Statement cExt -> m (Statement cExt)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Statement cExt
r

-- NOTE(lb): AFAIK, this only needs to be done once per process, not once per
-- debugger initialization. These settings probably persist no matter how many
-- times different debuggers (or defaultDebuggerInputs) are created.
initIsocline :: IO ()
initIsocline :: IO ()
initIsocline = do
  Bool
_ <- Bool -> IO Bool
Isocline.enableAutoTab Bool
True
  String -> Int -> IO ()
Isocline.setHistory String
".crucible-debug" Int
512

-- | Like 'Isocline.completeWord', but allow IO.
--
-- Implementation copied from 'Isocline.completeWord'.
completeWordIO ::
  Isocline.CompletionEnv ->
  String ->
  Maybe (Char -> Bool) ->
  (String -> IO [Isocline.Completion]) ->
  IO ()
completeWordIO :: CompletionEnv
-> String
-> Maybe (Char -> Bool)
-> (String -> IO [Completion])
-> IO ()
completeWordIO CompletionEnv
cenv String
input Maybe (Char -> Bool)
isWordChar String -> IO [Completion]
completer =
  CompletionEnv
-> String
-> Maybe (Char -> Bool)
-> (CompletionEnv -> String -> IO ())
-> IO ()
Isocline.completeWordPrim CompletionEnv
cenv String
input Maybe (Char -> Bool)
isWordChar CompletionEnv -> String -> IO ()
cenvCompleter
  where
    cenvCompleter :: CompletionEnv -> String -> IO ()
cenvCompleter CompletionEnv
ce String
i = do
      [Completion]
completes <- String -> IO [Completion]
completer String
i
      Bool
_ <- CompletionEnv -> [Completion] -> IO Bool
Isocline.addCompletions CompletionEnv
ce [Completion]
completes
      () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

readIsocline :: MonadIO m => CompletionT cExt (StyleT cExt m) String
readIsocline :: forall (m :: * -> *) cExt.
MonadIO m =>
CompletionT cExt (StyleT cExt m) String
readIsocline = do
  let extraPrompt :: String
extraPrompt = String
""  -- prompt will be "> "
  StyleEnv cExt
styleEnv <- StyleT cExt m (StyleEnv cExt)
-> CompletionT cExt (StyleT cExt m) (StyleEnv cExt)
forall (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StyleT cExt m (StyleEnv cExt)
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask
  CompletionEnv cExt
completionEnv <- CompletionT cExt (StyleT cExt m) (CompletionEnv cExt)
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask
  let completer :: Isocline.CompletionEnv -> String -> IO ()
      completer :: CompletionEnv -> String -> IO ()
completer CompletionEnv
cEnv String
input = do
        let isWordChar :: Maybe (Char -> Bool)
isWordChar = (Char -> Bool) -> Maybe (Char -> Bool)
forall a. a -> Maybe a
Just (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
Char.isSpace)
        let completeWord :: String -> IO [String]
completeWord String
w =
              [[String]] -> [String]
forall a. Monoid a => [a] -> a
mconcat ([[String]] -> [String])
-> ([Completions] -> [[String]]) -> [Completions] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Completions -> [String]) -> [Completions] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Completions -> [String]
Complete.completions ([Completions] -> [String]) -> IO [Completions] -> IO [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                CompletionEnv cExt -> String -> String -> IO [Completions]
forall cExt.
CompletionEnv cExt -> String -> String -> IO [Completions]
Complete.complete CompletionEnv cExt
completionEnv String
input String
w
        let wordCompleter :: String -> IO [Completion]
wordCompleter = ([String] -> [Completion]) -> IO [String] -> IO [Completion]
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Completion) -> [String] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map String -> Completion
Isocline.completion) (IO [String] -> IO [Completion])
-> (String -> IO [String]) -> String -> IO [Completion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO [String]
completeWord
        CompletionEnv
-> String
-> Maybe (Char -> Bool)
-> (String -> IO [Completion])
-> IO ()
completeWordIO CompletionEnv
cEnv String
input Maybe (Char -> Bool)
isWordChar String -> IO [Completion]
wordCompleter
  IO String -> CompletionT cExt (StyleT cExt m) String
forall a. IO a -> CompletionT cExt (StyleT cExt m) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> CompletionT cExt (StyleT cExt m) String)
-> IO String -> CompletionT cExt (StyleT cExt m) String
forall a b. (a -> b) -> a -> b
$
    String
-> Maybe (CompletionEnv -> String -> IO ())
-> Maybe (String -> String)
-> IO String
Isocline.readlineEx
      String
extraPrompt
      ((CompletionEnv -> String -> IO ())
-> Maybe (CompletionEnv -> String -> IO ())
forall a. a -> Maybe a
Just CompletionEnv -> String -> IO ()
completer)
      ((String -> String) -> Maybe (String -> String)
forall a. a -> Maybe a
Just (StyleEnv cExt -> StyleT cExt Identity String -> String
forall cExt a. StyleEnv cExt -> StyleT cExt Identity a -> a
Style.runStyle StyleEnv cExt
styleEnv (StyleT cExt Identity String -> String)
-> (String -> StyleT cExt Identity String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> StyleT cExt Identity String
forall (m :: * -> *) cExt.
Monad m =>
String -> StyleT cExt m String
Style.highlighter))

defaultDebuggerInputs ::
  MonadIO m =>
  CommandExt cExt ->
  IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
defaultDebuggerInputs :: forall (m :: * -> *) cExt.
MonadIO m =>
CommandExt cExt
-> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
defaultDebuggerInputs CommandExt cExt
cExts = do
  IO ()
initIsocline
  Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)
-> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)
 -> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)))
-> Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)
-> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
forall a b. (a -> b) -> a -> b
$
    CommandExt cExt
-> Inputs (CompletionT cExt (StyleT cExt m)) Text
-> Outputs (CompletionT cExt (StyleT cExt m)) ParseError
-> Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)
forall (m :: * -> *) cExt.
Monad m =>
CommandExt cExt
-> Inputs m Text
-> Outputs m ParseError
-> Inputs m (Statement cExt)
parseInputsWithRetry
      CommandExt cExt
cExts
      (String -> Text
Text.pack (String -> Text)
-> Inputs (CompletionT cExt (StyleT cExt m)) String
-> Inputs (CompletionT cExt (StyleT cExt m)) Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompletionT cExt (StyleT cExt m) String
-> Inputs (CompletionT cExt (StyleT cExt m)) String
forall (m :: * -> *) a. Monad m => m a -> Inputs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift CompletionT cExt (StyleT cExt m) String
forall (m :: * -> *) cExt.
MonadIO m =>
CompletionT cExt (StyleT cExt m) String
readIsocline)
      ((ParseError -> Text)
-> Outputs (CompletionT cExt (StyleT cExt m)) Text
-> Outputs (CompletionT cExt (StyleT cExt m)) ParseError
forall a' a.
(a' -> a)
-> Outputs (CompletionT cExt (StyleT cExt m)) a
-> Outputs (CompletionT cExt (StyleT cExt m)) a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ParseError -> Text
renderParseError ((IO () -> CompletionT cExt (StyleT cExt m) ())
-> Outputs IO Text
-> Outputs (CompletionT cExt (StyleT cExt m)) Text
forall (n :: * -> *) (m :: * -> *) a.
(n () -> m ()) -> Outputs n a -> Outputs m a
Outs.lift (StyleT cExt m () -> CompletionT cExt (StyleT cExt m) ()
forall (m :: * -> *) a. Monad m => m a -> CompletionT cExt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StyleT cExt m () -> CompletionT cExt (StyleT cExt m) ())
-> (IO () -> StyleT cExt m ())
-> IO ()
-> CompletionT cExt (StyleT cExt m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> StyleT cExt m ()
forall a. IO a -> StyleT cExt m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO) (Handle -> Outputs IO Text
Outs.hPutStrLn Handle
stdout)))