content: --  Copyright (C) 2006-2011 Angelos Charalambidis <a.charalambidis@di.uoa.gr>
  --
  --  This program is free software; you can redistribute it and/or modify
  --  it under the terms of the GNU General Public License as published by
  --  the Free Software Foundation; either version 2, or (at your option)
  --  any later version.
  --
  --  This program is distributed in the hope that it will be useful,
  --  but WITHOUT ANY WARRANTY; without even the implied warranty of
  --  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  --  GNU General Public License for more details.
  --
  --  You should have received a copy of the GNU General Public License
  --  along with this program; see the file COPYING.  If not, write to
  --  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  --  Boston, MA 02110-1301, USA.
  
  {-# LANGUAGE FlexibleContexts #-}
  
  -- | drives the pipeline of compilation + execution
  module Driver where
  
  
  import Language.Hopl (KnowledgeBase(..))
  
  import Parser (runParser, withInput, parseSrc, parseGoal, fromFile)
  import Tc (runTc, withSig, withTypeEnv)
  import WellForm (wfp, wfg)
  import Desugar (runDesugarT, desugarGoal, desugarSrc)
  import Infer
  import CoreLang (kbtoProgram, hopltoCoreGoal)
  import Pretty
  
  import Control.Monad.State (gets, modify)
  import Control.Monad.Trans (liftIO)
  import Control.Monad (when)
  
  import System.IO
  
  import Debugger
  import HopesIO
  
  parseFromFile fname parser = do
      file     <- liftIO $ openFile fname ReadMode
      content  <- liftIO $ hGetContents file
      parsed   <- runParser $ fromFile fname $ withInput content $ parser
      case parsed of
          Right (ast,s) -> return ast
          Left   msgs -> processMsgs msgs
  
  processMsgs (errs, warns) = do
      liftIO $ print $ vcat (map ppr errs)
      fail "errors occured"
  
  --loadSource :: String -> IO (Maybe (Prog, TypeEnv), Messages)
  
  loadSource file = do
      parsed       <- liftIO $ parseFromFile file parseSrc
      (wellformed, msgs) <- runTc (wfp parsed)
      case wellformed of
          Just (wfprog, env) -> do
                  cp <- runDesugarT $ desugarSrc (wfprog, env)
                  return (cp, env)
          Nothing -> processMsgs msgs
  
  loadGoal inp env = do
      parsed_res  <- liftIO $ runParser $ withInput inp $ parseGoal
      parsed_goal <- case parsed_res of
                          Right (g,_) -> return g
                          Left msgs   -> processMsgs msgs
      (tcres, msgs) <- runTc $ withSig parsed_goal $
                                withTypeEnv env $ wfg parsed_goal
      case tcres of
          Just (tcgoal, env') -> do
              cg <- runDesugarT $ desugarGoal (tcgoal, env')
              return (hopltoCoreGoal cg)
          Nothing -> processMsgs msgs
  
  
  consultFile f = do
      (src, env) <- loadSource f
      modify (\s -> s{ kb = KB src,
                       p = (kbtoProgram (KB src)),
                       currentEnv = env})
      liftIO $ putStrLn ("% consulted " ++ show f ++ "")
  
  sayYes    = putStrLn "Yes"
  sayNo     = putStrLn "No"
  
  refute s = do
      src  <- gets kb
      env  <- gets currentEnv
      goal <- loadGoal s env
      consumeSolutions $ attachDebugger $ prove goal
  -- consumeSolutions :: Infer a b -> HopesIO ()
  consumeSolutions i = do
      src  <- gets p
      liftIO $ hSetBuffering stdin NoBuffering
      result <- infer src i
  --    case runIdentity (infer src i) of
      case result of
          Nothing ->
              liftIO $ sayNo
          Just (a, rest) -> do
              liftIO $ sayYes
              liftIO $ print $ ppr a
              c <- liftIO $ getChar
              when (c == ';') $ do
                  liftIO $ putChar '\n';
                  consumeSolutions rest
  