module Lava.Vis
  ( vis
  , writeVis
  , writeVisInput
  , writeVisInputOutput
  , equivCheckVisInput
  )
 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(..)
  , hPutStr
  , hClose
  )

import Lava.IOBuffering
  ( noBuffering
  )

import Data.IORef

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

----------------------------------------------------------------
-- vis

vis :: Checkable a => a -> IO ProofResult
vis :: a -> IO ProofResult
vis 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 (IO () -> IO ProofResult) -> IO () -> IO ProofResult
forall a b. (a -> b) -> a -> b
$
       String -> String -> Maybe () -> Signal Bool -> Signal Bool -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions String
defsFile "circuit"
         (Maybe ()
forall a. Maybe a
Nothing :: Maybe ()) (Signal Bool -> Signal Bool -> Signal Bool
forall a. Generic a => a -> a -> a
delay Signal Bool
high ([Signal Bool] -> Signal Bool
andl [Signal Bool]
props)) (String -> Signal Bool
forall a. Constructive a => String -> a
var "good")
 where
  defsFile :: String
defsFile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.mv"

----------------------------------------------------------------
-- write Vis

writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
writeVis :: String -> (a -> b) -> IO ()
writeVis name :: String
name circ :: a -> b
circ =
  do String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name a -> b
circ (String -> a
forall a. Constructive a => String -> a
var "inp")

writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
writeVisInput :: String -> (a -> b) -> a -> IO ()
writeVisInput name :: String
name circ :: a -> b
circ inp :: a
inp =
  do String -> (a -> b) -> a -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput String
name a -> b
circ a
inp (String -> b -> b
forall a. Generic a => String -> a -> a
symbolize "outp" (a -> b
circ a
inp))

writeVisInputOutput :: (Generic a, Generic b)
                     => String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput :: String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput name :: String
name circ :: a -> b
circ inp :: a
inp out :: b
out =
  do String -> a -> b -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> a -> b -> b -> IO ()
writeItAll String
name a
inp (a -> b
circ a
inp) b
out

writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO ()
writeItAll :: String -> a -> b -> b -> IO ()
writeItAll name :: String
name inp :: a
inp out :: b
out out' :: b
out' =
  do IO ()
noBuffering
     String -> IO ()
putStr ("Writing to file \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" ... ")
     String -> String -> Maybe a -> b -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions String
file String
name (a -> Maybe a
forall a. a -> Maybe a
Just a
inp) b
out b
out'
     String -> IO ()
putStrLn "Done."
 where
  file :: String
file = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".mv"

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

writeDefinitions :: (Generic a, Generic b)
                 => FilePath -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions :: String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions file :: String
file name :: String
name minp :: Maybe a
minp out :: b
out out' :: b
out' =
  do Handle
firstHandle  <- String -> IOMode -> IO Handle
openFile String
file1 IOMode
WriteMode
     Handle
secondHandle <- String -> IOMode -> IO Handle
openFile String
file2 IOMode
WriteMode
     IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0

     Handle -> String -> IO ()
hPutStr Handle
firstHandle (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
$
       [ ".model " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
       ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
       [ ".inputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
       | VarBool v :: String
v <- [S Symbol]
inps
       ]

     Handle -> String -> IO ()
hPutStr Handle
secondHandle (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
$
       [ ".outputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
       | VarBool v :: String
v <- [S Symbol]
outs'
       ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
       [ ".table  -> low"
       , "0"
       , ".latch low initt"
       , ".reset initt"
       , "1"
       ]

     let new :: IO String
new =
           do Integer
n <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
var
              let n' :: Integer
n' = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1
                  v :: String
v  = "w" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n'
              IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
var Integer
n'
              String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v

         define :: String -> S String -> IO ()
define v :: String
v s :: S String
s =
           case S String
s of
             Bool True     -> ([Bool] -> Bool) -> [String] -> IO ()
port (\_   -> Bool
True)  []
             Bool False    -> ([Bool] -> Bool) -> [String] -> IO ()
port (\_   -> Bool
False) []
             Inv x :: String
x         -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool -> Bool
not Bool
p) [String
x]

             And []        -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
True)
             And [x :: String
x]       -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p]   -> Bool
p)      [String
x]
             And [x :: String
x,y :: String
y]     -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
&& Bool
q) [String
x,String
y]
             And (x :: String
x:xs :: [String]
xs)    -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
And [String]
xs)
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v ([String] -> S String
forall s. [s] -> S s
And [String
x,Integer -> String
forall a. Show a => a -> String
w 0])

             Or  []        -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
             Or  [x :: String
x]       -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p]   -> Bool
p)      [String
x]
             Or  [x :: String
x,y :: String
y]     -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
|| Bool
q) [String
x,String
y]
             Or  (x :: String
x:xs :: [String]
xs)    -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
Or [String]
xs)
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v ([String] -> S String
forall s. [s] -> S s
Or [String
x,Integer -> String
forall a. Show a => a -> String
w 0])

             Xor  []       -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
             Xor  [x :: String
x]      -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p]   -> Bool
p)      [String
x]
             Xor  [x :: String
x,y :: String
y]    -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
q) [String
x,String
y]
             Xor  (x :: String
x:xs :: [String]
xs)   -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
Or [String]
xs)
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 1) (String -> S String
forall s. s -> S s
Inv (Integer -> String
forall a. Show a => a -> String
w 0))
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 2) ([String] -> S String
forall s. [s] -> S s
And [String
x, Integer -> String
forall a. Show a => a -> String
w 1])

                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 3) (String -> S String
forall s. s -> S s
Inv String
x)
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 4) ([String] -> S String
forall s. [s] -> S s
Xor [String]
xs)
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 5) ([String] -> S String
forall s. [s] -> S s
And [Integer -> String
forall a. Show a => a -> String
w 3, Integer -> String
forall a. Show a => a -> String
w 4])
                           IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v     ([String] -> S String
forall s. [s] -> S s
Or [Integer -> String
forall a. Show a => a -> String
w 2, Integer -> String
forall a. Show a => a -> String
w 5])

             VarBool s :: String
s     -> do ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool
p) [String
s]
                                 case (Maybe a
minp,String
s) of
                                   (Nothing, 'i':_) -> String -> IO ()
input String
s
                                   _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
             DelayBool x :: String
x y :: String
y -> String -> String -> IO ()
delay String
x String
y

             _             -> Error -> IO ()
forall a. Error -> a
wrong Error
Lava.Error.NoArithmetic
           where
            w :: a -> String
w i :: a
i = String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

            input :: String -> IO ()
input s :: String
s =
              do Handle -> String -> IO ()
hPutStr Handle
firstHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                   ".inputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"

            port :: ([Bool] -> Bool) -> [String] -> IO ()
port oper :: [Bool] -> Bool
oper args :: [String]
args =
              do Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
                      ".table "
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args
                   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]
++ "\n"
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines
                      [ [Bool] -> String
line ([Bool]
xs [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [[Bool] -> Bool
oper [Bool]
xs])
                      | [Bool]
xs <- Int -> [[Bool]]
forall a. (Eq a, Num a) => a -> [[Bool]]
binary ([String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
args)
                      ]
             where
              line :: [Bool] -> String
line bs :: [Bool]
bs =
                [String] -> String
unwords ((Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\b :: Bool
b -> if Bool
b then "1" else "0") [Bool]
bs)

              binary :: a -> [[Bool]]
binary 0 = [[]]
              binary n :: a
n = ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
FalseBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) [[Bool]]
xs [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [a] -> [a] -> [a]
++ ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
TrueBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) [[Bool]]
xs
               where
                xs :: [[Bool]]
xs = a -> [[Bool]]
binary (a
na -> a -> a
forall a. Num a => a -> a -> a
-1)

            delay :: String -> String -> IO ()
delay x :: String
x y :: String
y =
              do Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                    [ ".latch " 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
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
                    , ".reset " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
                    , "0"
                    , ".table initt " 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
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
                    , "1 - - =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x
                    , "0 - - =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
                    ]

     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 (b -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct b
out)

     [IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
       [ String -> S String -> IO ()
define String
v' (String -> S String
forall s. String -> S s
VarBool String
v)
       | (v :: String
v,v' :: String
v') <- Struct String -> [String]
forall a. Struct a -> [a]
flatten Struct String
outvs [String] -> [String] -> [(String, String)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [ String
v' | VarBool v' :: String
v' <- [S Symbol]
outs' ]
       ]

     Handle -> String -> IO ()
hPutStr Handle
secondHandle (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
$
       [ ".end"
       ]

     Handle -> IO ()
hClose Handle
firstHandle
     Handle -> IO ()
hClose Handle
secondHandle
     String -> IO ExitCode
system ("cat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file)
     String -> IO ExitCode
system ("rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file2)
     () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 where
  file1 :: String
file1 = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_1"
  file2 :: String
file2 = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_2"

  sigs :: a -> [S Symbol]
sigs x :: a
x = (Symbol -> S Symbol) -> [Symbol] -> [S Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> S Symbol
unsymbol ([Symbol] -> [S Symbol]) -> (a -> [Symbol]) -> a -> [S Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Struct Symbol -> [Symbol]
forall a. Struct a -> [a]
flatten (Struct Symbol -> [Symbol])
-> (a -> Struct Symbol) -> a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct (a -> [S Symbol]) -> a -> [S Symbol]
forall a b. (a -> b) -> a -> b
$ a
x

  inps :: [S Symbol]
inps  = case Maybe a
minp of
            Just inp :: a
inp -> a -> [S Symbol]
forall a. Generic a => a -> [S Symbol]
sigs a
inp
            Nothing  -> []
  outs' :: [S Symbol]
outs' = b -> [S Symbol]
forall a. Generic a => a -> [S Symbol]
sigs b
out'

  make :: Int -> String -> String
make n :: Int
n s :: String
s = Int -> String -> String
forall a. Int -> [a] -> [a]
take (Int
n Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat ' ')

----------------------------------------------------------------
-- equivalence checking

equivCheckVisInput :: (a -> b) -> (a -> b) -> a -> IO ProofResult
equivCheckVisInput circ1 :: a -> b
circ1 circ2 :: a -> b
circ2 inp :: a
inp =
  do IO ()
checkVerifyDir
     IO ()
noBuffering
     String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name1 a -> b
circ1 a
inp
     String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name2 a -> b
circ2 a
inp
     String -> IO ()
putStr "Vis: ... "
     String
lavadir <- IO String
getLavaDir
     ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/vis.wrapper "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name2
                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
 where
  name :: String
name  = "Verify/circuit"
  name1 :: String
name1 = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_1"
  name2 :: String
name2 = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_2"

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

proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
  do String -> IO ()
putStr "Vis: "
     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/vis-reach.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.