module MProver.REPL where

import MProver.Eval
import MProver.Checker
import MProver.Monad
import MProver.Parser
import MProver.PPrint
import System.IO

import Control.Monad.IO.Class

repl :: MPT IO ()
repl = do
         liftIO $ putStr "MProver> "
         liftIO $ hFlush stdout
         inp <- liftIO $ getLine
         case inp of
           ":q" -> return ()
           ""   -> repl
           _    -> do
             case parseExpr "<interactive>" inp of
               (Left err) -> liftIO $ print err
               (Right e)  -> do
                 e'  <- evalCBN e
                 e'_ <- ppr e'
                 liftIO $ print e'_
             repl