module Main where

import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer
import System.Environment
import Text.Parsec
import Z3.Monad (evalZ3)

import AST
import Eval
import Parse
import Typecheck

parseProg = parseStmt <* optional (string ";") <* spaces <* eof
propcheck stmt = evalZ3 $ runExceptT $ evalStateT (checkStmt stmt) []
eval stmt = runExceptT $ evalStateT (evalStmt stmt) []

main :: IO ()
main = do
  src <- readFile . head =<< getArgs
  case parse parseProg "program" src of
    Left err -> putStrLn "error in parsing:" >> print err
    Right stmt -> do
      propcheck stmt >>= \case
        Left err -> putStrLn "error in typechecking:" >> print err
        Right () -> do
          eval stmt >>= \case
            Left err -> putStrLn "error in evaluation:" >> print err
            Right () -> putStrLn "👍"
