picologic-0.1: src/Picologic/Repl.hs
module Picologic.Repl (
repl,
stdin,
file,
runRepl,
) where
import Picologic.AST
import Picologic.Parser
import Picologic.Solver
import Picologic.Pretty
import Text.PrettyPrint
import Control.Monad.State
import Data.List (isPrefixOf)
import System.Console.Haskeline
-------------------------------------------------------------------------------
-- REPL
-------------------------------------------------------------------------------
type Repl = StateT IState (InputT IO)
data IState = IState
{ _module :: Maybe Expr
, _curFile :: Maybe FilePath
}
initState :: IState
initState = IState Nothing Nothing
preamble :: Repl ()
preamble = liftIO $ do
putStrLn "Picologic 0.1"
putStrLn "Type :help for help"
runRepl :: Repl a -> IO IState
runRepl f = runInputT defaultSettings (execStateT (preamble >> f) initState)
-------------------------------------------------------------------------------
-- Commands
-------------------------------------------------------------------------------
load :: String -> Repl ()
load arg = do
liftIO $ putStrLn $ "Loading " ++ arg
file arg
modify $ \s -> s { _curFile = Just arg }
reload :: Repl ()
reload = do
fname <- gets _curFile
case fname of
Just fname' -> handleCommand "load" [fname']
Nothing -> liftIO $ putStrLn "No such file"
run :: Repl ()
run = do
mod <- gets _module
case mod of
Nothing -> liftIO $ putStrLn "No expression."
Just ex -> liftIO $ do
sols <- solveProp ex
putStrLn "Solutions:"
putStrLn (ppSolutions sols)
clauses :: Repl ()
clauses = do
env <- gets _module
case env of
Just ex -> liftIO $ print (clausesExpr ex)
Nothing -> liftIO $ putStrLn "No file loaded."
help :: Repl ()
help = liftIO $ do
putStrLn ":clauses Show the SAT solver clauses"
putStrLn ":load <file> Load a program from file"
-------------------------------------------------------------------------------
-- Test
-------------------------------------------------------------------------------
-- evaluate a module
modl :: FilePath -> Repl ()
modl fname = do
mod <- liftIO $ parseFile fname
case mod of
Left err -> liftIO $ print err
Right res ->
let ex = (simp . cnf $ res) in
modify $ \s -> s { _module = Just ex }
-- evaluate an expression
exec :: String -> Repl ()
exec source = do
let mod = parseExpr source
case mod of
Left err -> liftIO $ print err
Right res -> do
let ex = (simp . cnf $ res)
liftIO $ putStrLn (render $ ppExprU ex)
liftIO $ do
sols <- solveProp ex
putStrLn "Solutions:"
putStrLn (ppSolutions sols)
modify $ \s -> s { _module = Just ex }
file :: FilePath -> Repl ()
file fname = modl fname
stdin :: IO ()
stdin = do
contents <- getContents
case parseExpr contents of
Left err -> print err
Right ex -> do
sols <- solveProp ex
putStrLn (ppSolutions sols)
handleCommand :: String -> [String] -> Repl ()
handleCommand cmd args
| "ru" `isPrefixOf` cmd = run
| "r" `isPrefixOf` cmd = reload
| "cl" `isPrefixOf` cmd = clauses
| "h" `isPrefixOf` cmd = help
| length args == 0 = liftIO $ putStrLn "Not enough arguments"
| "l" `isPrefixOf` cmd = load arg
| otherwise = liftIO $ putStrLn "Unknown command"
where
arg = head args
repl :: Repl ()
repl = do
minput <- lift $ getInputLine "Logic> "
case minput of
Nothing -> lift $ outputStrLn "Goodbye."
Just (':' : cmds) -> do
let (cmd:args) = words cmds
handleCommand cmd args
repl
Just input -> do
exec input
repl