    {-# 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

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

      let 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]

      (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options ""

      putStrLn kind2Input

      removeFile tempName

      let propId         = [String] -> String
    forall a. HasCallStack => [a] -> a
    head [String]
    toCheck
          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"
      return $ parseOutput propId propQuantifier output