{-# LANGUAGE Trustworthy #-}

-- | A prover backend based on Kind2.
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 Data.Map         as Map

import qualified Copilot.Theorem.Misc.Error as Err
import qualified Copilot.Theorem.TransSys   as TS

-- | Options for Kind2
data Options = Options
  { Options -> Int
bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and
                  --   step will perform. A value of 0 means /unlimited/.
  }

-- | Default options with unlimited unrolling for base and step.
instance Default Options where
  def :: Options
def = Options { bmcMax :: Int
bmcMax = Int
0 }

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

-- | A prover backend based on Kind2.
--
-- The executable @kind2@ must exist and its location be in the @PATH@.
kind2Prover :: Options -> Prover
kind2Prover :: Options -> Prover
kind2Prover Options
opts = Prover
  { proverName :: String
proverName =  String
"Kind2"
  , startProver :: Spec -> IO ProverST
startProver  = ProverST -> IO ProverST
forall a. a -> IO a
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 a. a -> IO a
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

  let propId :: String
propId         = [String] -> String
forall a. HasCallStack => [a] -> a
head [String]
toCheck
      propQuantifier :: Prop
propQuantifier = case String -> Map String (ExtVar, Prop) -> Maybe (ExtVar, Prop)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
propId (TransSys -> Map String (ExtVar, Prop)
TS.specProps TransSys
spec) of
                         Just (ExtVar
_, Prop
quantifier) ->
                           Prop
quantifier
                         Maybe (ExtVar, Prop)
Nothing ->
                           String -> Prop
forall a. String -> a
Err.impossible (String -> Prop) -> String -> Prop
forall a b. (a -> b) -> a -> b
$
                             String
"askKind2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
propId String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not in specProps"
  Output -> IO Output
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> IO Output) -> Output -> IO Output
forall a b. (a -> b) -> a -> b
$ String -> Prop -> String -> Output
parseOutput String
propId Prop
propQuantifier String
output