mprover-0.0.0.0: Main.hs

module Main where

import MProver.Parser as Parser
import MProver.Syntax

import MProver.Eval
import MProver.Checker
import MProver.REPL

import Control.Monad
import Control.Monad.Reader
import Control.Monad.Error
import Control.Monad.Identity

import qualified Data.Map

import System (getArgs)

import Unbound.LocallyNameless

test :: FilePath -> IO ()
test filename = do
     fileContents <- readFile filename

     let pResult  =  Parser.parse filename fileContents

     case pResult of
       (Left err)               -> putStrLn $ "Parse error: " ++ show err
       (Right p@(Program _ _)) -> do
         let result = runFreshM $ runReaderT (runErrorT (checkProg p)) (Data.Map.empty,Data.Map.empty,Data.Map.empty,Data.Map.empty)
         case result of
           (Left err) -> do
                           putStr "Error: "
                           putStrLn err
           (Right ()) -> putStrLn "Succeeded."

testParse :: FilePath -> IO ()
testParse filename = do
  fileContents <- readFile filename
  print (Parser.parse filename fileContents)

dorepl :: IO ()
dorepl = runFreshMT (runReaderT (runErrorT repl) (Data.Map.empty,Data.Map.empty,Data.Map.empty,Data.Map.empty)) >> return ()

main :: IO ()
main = do
  args <- getArgs
  case args of
    (filename:_) -> test filename
    []           -> dorepl