{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}

module Language.Mist.Runner where

import System.IO
import Language.Mist.Types
import Language.Mist.Parser
import Language.Mist.Checker
import Language.Mist.CGen
import Language.Mist.ToFixpoint
import Language.Mist.Normalizer
import Language.Mist.Names
import qualified Language.Fixpoint.Horn.Types as HC
import qualified Language.Fixpoint.Types as F

import Text.Megaparsec.Pos (initialPos) -- NOTE: just for debugging

type R = HC.Pred

{-
  0) parse
  1) unique
  2) convert refinements from mist `Expr`s to fixpoint `Expr`s
  3) elaborate
  4) annotate each node with its type
  5) anf
  6) constraint generation
-}

---------------------------------------------------------------------------
runMist :: Handle -> FilePath -> IO (Result ())
---------------------------------------------------------------------------
runMist h f = act h f >>= \case
  r@Right{} -> hPutStrLn h "SAFE" >> return r
  Left es -> esHandle h (return . Left) es

act :: Handle -> FilePath -> IO (Result ())
act h f = do
  s <- readFile f
  (measures, e) <- parse f s
  let r = mist measures e
  case r of
    Right (measures', t) -> do
      -- !_ <- traceM $ pprint (anormal (annotate t TUnit))
      let c = generateConstraints (anormal (annotate t TUnit))
      solverResult <- solve measures' c
      hPrint h solverResult
      case F.resStatus solverResult of
        F.Safe -> return (Right ())
        _ -> return $ Left [mkError ("solver failed: " ++ show solverResult) (SS {ssBegin = initialPos f, ssEnd = initialPos f})] -- TODO: proper error
    Left l -> return (Left l)

esHandle :: Handle -> ([UserError] -> IO a) -> [UserError] -> IO a
esHandle h exitF es = renderErrors es >>= hPutStrLn h >> exitF es

-----------------------------------------------------------------------------------
mist :: Measures -> SSParsedExpr -> Result (Measures, ElaboratedExpr R SourceSpan)
-----------------------------------------------------------------------------------
mist measures expr =
  case wellFormed expr of
    [] -> do
      let (measures', uniqueExpr) = uniquify (measures, expr)
      let predExpr = parsedExprPredToFixpoint uniqueExpr
      result <- elaborate predExpr
      pure (measures', result)
    errors -> Left errors