{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test.Cardano.Ledger.Constrained.Preds.Repl (goRepl, repl, ReplMode (..), modeRepl) where

import Data.Char (toLower)
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import System.Console.Haskeline (
  InputT,
  defaultSettings,
  getInputLine,
  outputStrLn,
  runInputT,
  setComplete,
 )
import System.Console.Haskeline.Completion (completeWord, simpleCompletion)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Size (seps)
import Test.Cardano.Ledger.Constrained.TypeRep

-- =====================================================

repl :: Proof era -> Env era -> IO ()
repl :: forall era. Proof era -> Env era -> IO ()
repl Proof era
proof Env era
env = forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT forall (m :: * -> *). MonadIO m => Settings m
defaultSettings (forall era. Proof era -> Env era -> InputT IO ()
loop Proof era
proof Env era
env)

goRepl :: Proof era -> Env era -> String -> IO ()
goRepl :: forall era. Proof era -> Env era -> String -> IO ()
goRepl Proof era
p env :: Env era
env@(Env Map String (Payload era)
emap) String
str = forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete CompletionFunc IO
comp forall (m :: * -> *). MonadIO m => Settings m
defaultSettings) (forall era. Proof era -> Env era -> String -> InputT IO ()
helpRepl Proof era
p Env era
env String
str)
  where
    keys :: [String]
keys = forall a. Set a -> [a]
Set.toList (forall k a. Map k a -> Set k
Map.keysSet Map String (Payload era)
emap)
    comp :: CompletionFunc IO
comp = forall (m :: * -> *).
Monad m =>
Maybe Char
-> String -> (String -> m [Completion]) -> CompletionFunc m
completeWord forall a. Maybe a
Nothing [Char
' '] (\String
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a -> b) -> [a] -> [b]
map String -> Completion
simpleCompletion (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf String
s) [String]
keys)))

loop :: Proof era -> Env era -> InputT IO ()
loop :: forall era. Proof era -> Env era -> InputT IO ()
loop Proof era
proof env :: Env era
env@(Env Map String (Payload era)
emap) = do
  Maybe String
minput <- forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine String
"prompt> "
  case Maybe String
minput of
    Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just String
":q" -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just String
"help" -> forall era. Proof era -> Env era -> String -> InputT IO ()
helpRepl Proof era
proof Env era
env []
    Just String
"?" -> forall era. Proof era -> Env era -> String -> InputT IO ()
helpRepl Proof era
proof Env era
env []
    Just (Char
':' : Char
'p' : String
more) -> forall era. Proof era -> Env era -> String -> InputT IO ()
helpRepl Proof era
proof Env era
env String
more
    Just String
str ->
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
' ') String
str) Map String (Payload era)
emap of
        Maybe (Payload era)
Nothing -> forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn String
"Not found" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall era. Proof era -> Env era -> InputT IO ()
loop Proof era
proof Env era
env
        Just (Payload Rep era t
rep t
t Access era s t
_) -> do
          forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn (String
str forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
rep)
          forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn (forall era t. Rep era t -> t -> String
format Rep era t
rep t
t)
          forall era. Proof era -> Env era -> InputT IO ()
loop Proof era
proof Env era
env

helpRepl :: forall era. Proof era -> Env era -> [Char] -> InputT IO ()
helpRepl :: forall era. Proof era -> Env era -> String -> InputT IO ()
helpRepl Proof era
proof env :: Env era
env@(Env Map String (Payload era)
emap) String
more = do
  let keys :: [String]
keys = forall a. Set a -> [a]
Set.toList (forall k a. Map k a -> Set k
Map.keysSet Map String (Payload era)
emap)
      matches :: [String]
matches = forall a. (a -> Bool) -> [a] -> [a]
filter (\String
k -> forall a. Eq a => [a] -> [a] -> Bool
List.isInfixOf (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
more) (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
k)) [String]
keys
  if String
more forall a. Eq a => a -> a -> Bool
== String
""
    then
      forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn
        ( [String] -> String
unlines
            [ String
"\nEnter one of these Strings at the 'prompt>' to see its value."
            , String
"Type ':q' to exit."
            , String
"Type ':pXXX' to see variables whose name contains the substring 'XXX' (case insensitive)."
            , String
"Type 'help' or '?' to see these instructions.\n"
            ]
        )
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn ([String] -> String
seps [String]
matches)
  forall (m :: * -> *). MonadIO m => String -> InputT m ()
outputStrLn String
""
  forall era. Proof era -> Env era -> InputT IO ()
loop Proof era
proof Env era
env

-- ========================================

data ReplMode = Interactive | CI
  deriving (ReplMode -> ReplMode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReplMode -> ReplMode -> Bool
$c/= :: ReplMode -> ReplMode -> Bool
== :: ReplMode -> ReplMode -> Bool
$c== :: ReplMode -> ReplMode -> Bool
Eq)

modeRepl :: ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl :: forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
Interactive Proof era
p Env era
e String
s = forall era. Proof era -> Env era -> String -> IO ()
goRepl Proof era
p Env era
e String
s
modeRepl ReplMode
CI Proof era
_ (Env Map String (Payload era)
emap) String
_ = do
  let keys :: [String]
keys = forall a. Set a -> [a]
Set.toList (forall k a. Map k a -> Set k
Map.keysSet Map String (Payload era)
emap)
  String -> IO ()
putStrLn ([String] -> String
seps [String]
keys)