module Lava.Eprover
  ( eprover
  )
 where

import Lava.Signal
import Lava.Netlist
import Lava.Generic
import Lava.Sequent
import Lava.Property
import Lava.Error
import Lava.LavaDir
import Lava.Verification

import Data.List
  ( intersperse
  , nub
  )

import System.IO
  ( openFile
  , IOMode(..)
  , hPutStrLn
  , hClose
  )

import Control.Exception
  ( try
  )

import Lava.IOBuffering
  ( noBuffering
  )

import Data.IORef

import System.Process (system)
import System.Exit (ExitCode(..))

----------------------------------------------------------------
-- eprover

eprover :: Checkable a => a -> IO ProofResult
eprover :: a -> IO ProofResult
eprover a :: a
a =
  do IO ()
checkVerifyDir
     IO ()
noBuffering
     (props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
     String -> IO () -> IO ProofResult
proveFile String
defsFile (String -> [Signal Bool] -> IO ()
writeDefinitions String
defsFile [Signal Bool]
props)
 where
  defsFile :: String
defsFile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.tptp"

----------------------------------------------------------------
-- definitions

writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
writeDefinitions :: String -> [Signal Bool] -> IO ()
writeDefinitions file :: String
file props :: [Signal Bool]
props =
  do Handle
han <- String -> IOMode -> IO Handle
openFile String
file IOMode
WriteMode
     Handle -> String -> IO ()
hPutStrLn Handle
han "% Generated by Lava\n"
     Handle -> String -> IO ()
hPutStrLn Handle
han "% definitions:\n"
     IORef Int
ref <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef (2 :: Int)

     let clause :: String -> [String] -> IO ()
clause kind :: String
kind xs :: [String]
xs =
           Handle -> String -> IO ()
hPutStrLn Handle
han (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
             [ "input_clause(name," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
kind String -> String -> String
forall a. [a] -> [a] -> [a]
++ ",["
             , [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse ", " [String]
xs)
             , "])."
             ]

         new :: IO String
new =
           do Int
n <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ref
              let n' :: Int
n' = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1
              Int
n' Int -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
ref Int
n'
              String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ("*" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n')

         define :: String -> S String -> IO ()
define v :: String
v s :: S String
s =
           do String -> String -> IO ()
definition String
v (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                case S String
s of
                  Bool True  -> Int -> String
int 1
                  Bool False -> Int -> String
int 0
                  VarBool s :: String
s  -> String -> String -> String -> String
op2 "mod" String
s (Int -> String
int 2)
                  Inv x :: String
x      -> String -> String -> String
op1 "inv" String
x

                  And xs :: [String]
xs     -> String -> String -> [String] -> String
opl (Int -> String
int 1) "and" [String]
xs
                  Or  xs :: [String]
xs     -> String -> String -> [String] -> String
opl (Int -> String
int 0) "or" [String]
xs
                  Xor xs :: [String]
xs     -> [String] -> String
xor [String]
xs

                  Int n :: Int
n      -> Int -> String
int Int
n
                  Neg x :: String
x      -> String -> String -> String
op1 "neg" String
x
                  Div x :: String
x y :: String
y    -> String -> String -> String -> String
op2 "div" String
x String
y
                  Mod x :: String
x y :: String
y    -> String -> String -> String -> String
op2 "mod" String
x String
y
                  Plus xs :: [String]
xs    -> String -> String -> [String] -> String
opl (Int -> String
int 0) "add" [String]
xs
                  Times xs :: [String]
xs   -> String -> String -> [String] -> String
opl (Int -> String
int 1) "mul" [String]
xs
                  Gte x :: String
x y :: String
y    -> String -> String -> String -> String
op2 "gte" String
x String
y
                  If x :: String
x y :: String
y z :: String
z   -> String -> String -> String -> String -> String
op3 "if" String
x String
y String
z
                  VarInt s :: String
s   -> String
s

                  Equal []     -> Int -> String
int 1
                  Equal (x :: String
x:xs :: [String]
xs) -> String -> String -> [String] -> String
opl (Int -> String
int 1) "and" [String -> String -> String -> String
op2 "eq" String
x String
y | String
y <- [String]
xs]

                  DelayBool x :: String
x y :: String
y -> Error -> String
forall a. Error -> a
wrong Error
Lava.Error.DelayEval
                  DelayInt  x :: String
x y :: String
y -> Error -> String
forall a. Error -> a
wrong Error
Lava.Error.DelayEval
           where
            definition :: String -> String -> IO ()
definition v :: String
v s :: String
s =
              String -> [String] -> IO ()
clause "axiom" [ "++equal(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" ]

            op1 :: String -> String -> String
op1 f :: String
f x :: String
x     = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
            op2 :: String -> String -> String -> String
op2 f :: String
f x :: String
x y :: String
y   = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
            op3 :: String -> String -> String -> String -> String
op3 f :: String
f x :: String
x y :: String
y z :: String
z = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

            opl :: String -> String -> [String] -> String
opl z :: String
z f :: String
f []     = String
z
            opl z :: String
z f :: String
f [x :: String
x]    = String
x
            opl z :: String
z f :: String
f (x :: String
x:xs :: [String]
xs) = String -> String -> String -> String
op2 String
f String
x (String -> String -> [String] -> String
opl String
z String
f [String]
xs)

            int :: Int -> String
int n :: Int
n = String -> String -> [String] -> String
opl "cZero" "add" (Int -> String -> [String]
forall a. Int -> a -> [a]
replicate Int
n "cOne")

            xor :: [String] -> String
xor []     = Int -> String
int 0
            xor [x :: String
x]    = String
x
            xor [x :: String
x,y :: String
y]  = String -> String -> String -> String
op2 "xor" String
x String
y
            xor (x :: String
x:xs :: [String]
xs) = String -> String -> String -> String
op2 "or" (String -> String -> String -> String
op2 "and" String
x (String -> String -> String
op1 "inv" (String -> String -> [String] -> String
opl (Int -> String
int 0) "or" [String]
xs)))
                                  (String -> String -> String -> String
op2 "and" (String -> String -> String
op1 "inv" String
x) ([String] -> String
xor [String]
xs))

     Struct String
outvs <- IO String
-> (String -> S String -> IO ())
-> Struct Symbol
-> IO (Struct String)
forall (f :: * -> *) v.
Sequent f =>
IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistIO IO String
new String -> S String -> IO ()
define ([Signal Bool] -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct [Signal Bool]
props)
     Handle -> String -> IO ()
hPutStrLn Handle
han "% conjecture:\n"
     String -> [String] -> IO ()
clause "conjecture" [ "--truth(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" | String
v <- Struct String -> [String]
forall a. Struct a -> [a]
flatten Struct String
outvs ]
     Handle -> IO ()
hClose Handle
han

     IO ExitCode -> IO (Either IOError ExitCode)
forall e a. Exception e => IO a -> IO (Either e a)
try (do String -> IO String
readFile String
theoryFile
             String -> IO ExitCode
system ("cat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
theoryFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " >> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file))
                :: IO (Either IOError ExitCode)

     () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  theoryFile :: String
theoryFile = "theory.tptp"

----------------------------------------------------------------
-- primitive proving

proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
  do String -> IO ()
putStr "Eprover: "
     IO ()
before
     String -> IO ()
putStr "... "
     String
lavadir <- IO String
getLavaDir
     ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/eprover.wrapper "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime"
                 )
     let res :: ProofResult
res = case ExitCode
x of
                 ExitSuccess   -> ProofResult
Valid
                 ExitFailure 1 -> ProofResult
Indeterminate
                 ExitFailure _ -> ProofResult
Falsifiable
     String -> IO ()
putStrLn (ProofResult -> String
forall a. Show a => a -> String
show ProofResult
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".")
     ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res

----------------------------------------------------------------
-- the end.