Inputs.hs

{-|
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 { recv :: m a }
  deriving (Applicative, Functor, Monad)

instance MonadFail m => MonadFail (Inputs m) where
  fail = Inputs . Monad.fail

instance MonadIO m => MonadIO (Inputs m) where
  liftIO = Inputs . liftIO

instance MonadTrans Inputs where
  lift = Inputs

fail :: MonadFail m => Inputs m a
fail = Monad.fail "No more inputs"

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

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

parseInputs ::
  MonadFail m =>
  CommandExt cExt ->
  Inputs m Text ->
  Inputs m (Statement cExt)
parseInputs cExts (Inputs inps) = Inputs go
  where
    go = do
      txt <- inps
      case Stmt.parse cExts txt of
        Left err -> Monad.fail (show err)
        Right r -> pure r

parseInputsWithRetry ::
  Monad m =>
  CommandExt cExt ->
  Inputs m Text ->
  Outputs m ParseError ->
  Inputs m (Statement cExt)
parseInputsWithRetry cExts (Inputs inps) errs = Inputs go
  where
    go = do
      txt <- inps
      case Stmt.parse cExts txt of
        Left err -> do
          Outs.send errs err
          go
        Right r -> pure 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 = do
  _ <- Isocline.enableAutoTab True
  Isocline.setHistory ".crucible-debug" 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 cenv input isWordChar completer =
  Isocline.completeWordPrim cenv input isWordChar cenvCompleter
  where
    cenvCompleter ce i = do
      completes <- completer i
      _ <- Isocline.addCompletions ce completes
      return ()

readIsocline :: MonadIO m => CompletionT cExt (StyleT cExt m) String
readIsocline = do
  let extraPrompt = ""  -- prompt will be "> "
  styleEnv <- lift Reader.ask
  completionEnv <- Reader.ask
  let completer :: Isocline.CompletionEnv -> String -> IO ()
      completer cEnv input = do
        let isWordChar = Just (not . Char.isSpace)
        let completeWord w =
              mconcat . map Complete.completions <$>
                Complete.complete completionEnv input w
        let wordCompleter = fmap (map Isocline.completion) . completeWord
        completeWordIO cEnv input isWordChar wordCompleter
  liftIO $
    Isocline.readlineEx
      extraPrompt
      (Just completer)
      (Just (Style.runStyle styleEnv . Style.highlighter))

defaultDebuggerInputs ::
  MonadIO m =>
  CommandExt cExt ->
  IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
defaultDebuggerInputs cExts = do
  initIsocline
  pure $
    parseInputsWithRetry
      cExts
      (Text.pack <$> lift readIsocline)
      (contramap renderParseError (Outs.lift (lift . liftIO) (Outs.hPutStrLn stdout)))