--------------------------------------------------------------------------------

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Trustworthy #-}

module Copilot.Theorem.Kind2.Prover
  ( module Data.Default
  , Options (..)
  , kind2Prover
  ) where

import Copilot.Theorem.Prove
import Copilot.Theorem.Kind2.Output
import Copilot.Theorem.Kind2.PrettyPrint
import Copilot.Theorem.Kind2.Translate

-- It seems [IO.openTempFile] doesn't work on Mac OSX
import System.IO hiding (openTempFile)
import Copilot.Theorem.Misc.Utils (openTempFile)

import System.Process

import System.Directory
import Data.Default

import qualified Copilot.Theorem.TransSys as TS

--------------------------------------------------------------------------------

data Options = Options
  { Options -> Int
bmcMax :: Int }

instance Default Options where
  def :: Options
def = Options :: Int -> Options
Options { bmcMax :: Int
bmcMax = Int
0 }

data ProverST = ProverST
  { ProverST -> Options
options  :: Options
  , ProverST -> TransSys
transSys :: TS.TransSys }

kind2Prover :: Options -> Prover
kind2Prover :: Options -> Prover
kind2Prover Options
opts = Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
Prover
  { proverName :: String
proverName =  String
"Kind2"
  , startProver :: Spec -> IO ProverST
startProver  = ProverST -> IO ProverST
forall (m :: * -> *) a. Monad m => a -> m a
return (ProverST -> IO ProverST)
-> (Spec -> ProverST) -> Spec -> IO ProverST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> TransSys -> ProverST
ProverST Options
opts (TransSys -> ProverST) -> (Spec -> TransSys) -> Spec -> ProverST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> TransSys
TS.translate
  , askProver :: ProverST -> [String] -> [String] -> IO Output
askProver    = ProverST -> [String] -> [String] -> IO Output
askKind2
  , closeProver :: ProverST -> IO ()
closeProver  = IO () -> ProverST -> IO ()
forall a b. a -> b -> a
const (IO () -> ProverST -> IO ()) -> IO () -> ProverST -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }

--------------------------------------------------------------------------------

kind2Prog :: String
kind2Prog        = String
"kind2"
kind2BaseOptions :: [String]
kind2BaseOptions = [String
"--input-format", String
"native", String
"-xml"]

--------------------------------------------------------------------------------

askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output
askKind2 :: ProverST -> [String] -> [String] -> IO Output
askKind2 (ProverST Options
opts TransSys
spec) [String]
assumptions [String]
toCheck = do

  let kind2Input :: String
kind2Input = File -> String
prettyPrint (File -> String) -> (TransSys -> File) -> TransSys -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> [String] -> [String] -> TransSys -> File
toKind2 Style
Inlined [String]
assumptions [String]
toCheck (TransSys -> String) -> TransSys -> String
forall a b. (a -> b) -> a -> b
$ TransSys
spec

  (String
tempName, Handle
tempHandle) <- String -> String -> String -> IO (String, Handle)
openTempFile String
"." String
"out" String
"kind"
  Handle -> String -> IO ()
hPutStr Handle
tempHandle String
kind2Input
  Handle -> IO ()
hClose Handle
tempHandle

  let kind2Options :: [String]
kind2Options =
        [String]
kind2BaseOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"--bmc_max", Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Options -> Int
bmcMax Options
opts, String
tempName]

  (ExitCode
_, String
output, String
_) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
kind2Prog [String]
kind2Options String
""

  String -> IO ()
putStrLn String
kind2Input

  String -> IO ()
removeFile String
tempName
  Output -> IO Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> IO Output) -> Output -> IO Output
forall a b. (a -> b) -> a -> b
$ String -> String -> Output
parseOutput ([String] -> String
forall a. [a] -> a
head [String]
toCheck) String
output -- TODO support multiple toCheck props

--------------------------------------------------------------------------------