module Lava.Isc
 ( IscMethod(..)
 , isc
 , iscWith
 ) where

import Lava.Ref
import Lava.Signal
import Lava.Generic

import Lava.Property
import Lava.LavaDir
import Lava.Sequent
import Lava.Netlist
import Lava.Verification
import Lava.IOBuffering

import Data.Array
import Lava.MyST
import Data.List(intersperse)
import System.Process (system)
import System.Exit (ExitCode(..))

----------------------------------------------------------------------------------------------------
-- options

data IscMethod
 = StepMin
 | StepMax
 | Mixed
 | Bmc

----------------------------------------------------------------------------------------------------
-- toplevel proving

isc :: Checkable a => a -> IO ProofResult
isc :: a -> IO ProofResult
isc = IscMethod -> Int -> a -> IO ProofResult
forall a. Checkable a => IscMethod -> Int -> a -> IO ProofResult
iscWith IscMethod
Mixed 10

iscWith :: Checkable a => IscMethod -> Int -> a -> IO ProofResult
iscWith :: IscMethod -> Int -> a -> IO ProofResult
iscWith m :: IscMethod
m n :: Int
n a :: a
a =
  do IO ()
checkVerifyDir
     IO ()
noBuffering
     String -> a -> IO ()
forall a. Checkable a => String -> a -> IO ()
net_ String
netfile a
a
     String
lavadir <- IO String
getLavaDir
--     r <- system (lavadir ++ execute)
     ExitCode
r <- String -> IO ExitCode
system (String
execute)
     ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofResult -> IO ProofResult) -> ProofResult -> IO ProofResult
forall a b. (a -> b) -> a -> b
$ case ExitCode
r of
       ExitSuccess   -> ProofResult
Valid
       ExitFailure 1 -> ProofResult
Indeterminate
       ExitFailure _ -> ProofResult
Falsifiable

 where
--  execute = "/Scripts/isc "
  execute :: String
execute = "isc "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
netfile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IscMethod -> String
m2par IscMethod
m) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
  netfile :: String
netfile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.net"

  m2par :: IscMethod -> String
m2par StepMin = "-smin"
  m2par StepMax = "-smax"
  m2par Mixed   = "-mix"
  m2par Bmc     = "-bmc"

----------------------------------------------------------------------------------------------------
-- netlist

data Sign a  = Pos a | Not a deriving (Int -> Sign a -> String -> String
[Sign a] -> String -> String
Sign a -> String
(Int -> Sign a -> String -> String)
-> (Sign a -> String)
-> ([Sign a] -> String -> String)
-> Show (Sign a)
forall a. Show a => Int -> Sign a -> String -> String
forall a. Show a => [Sign a] -> String -> String
forall a. Show a => Sign a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Sign a] -> String -> String
$cshowList :: forall a. Show a => [Sign a] -> String -> String
show :: Sign a -> String
$cshow :: forall a. Show a => Sign a -> String
showsPrec :: Int -> Sign a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> Sign a -> String -> String
Show, ReadPrec [Sign a]
ReadPrec (Sign a)
Int -> ReadS (Sign a)
ReadS [Sign a]
(Int -> ReadS (Sign a))
-> ReadS [Sign a]
-> ReadPrec (Sign a)
-> ReadPrec [Sign a]
-> Read (Sign a)
forall a. Read a => ReadPrec [Sign a]
forall a. Read a => ReadPrec (Sign a)
forall a. Read a => Int -> ReadS (Sign a)
forall a. Read a => ReadS [Sign a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Sign a]
$creadListPrec :: forall a. Read a => ReadPrec [Sign a]
readPrec :: ReadPrec (Sign a)
$creadPrec :: forall a. Read a => ReadPrec (Sign a)
readList :: ReadS [Sign a]
$creadList :: forall a. Read a => ReadS [Sign a]
readsPrec :: Int -> ReadS (Sign a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Sign a)
Read)

sneg :: Sign a -> Sign a
sneg (Pos x :: a
x) = a -> Sign a
forall a. a -> Sign a
Not a
x
sneg (Not x :: a
x) = a -> Sign a
forall a. a -> Sign a
Pos a
x

type NetList = Array Int (S (Sign Int))

instance Functor Sign where
  fmap :: (a -> b) -> Sign a -> Sign b
fmap f :: a -> b
f (Pos x :: a
x) = b -> Sign b
forall a. a -> Sign a
Pos (a -> b
f a
x)
  fmap f :: a -> b
f (Not x :: a
x) = b -> Sign b
forall a. a -> Sign a
Not (a -> b
f a
x)


showS :: S String -> String
showS :: S String -> String
showS (Bool b :: Bool
b)     = "Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
b
showS (Or [x :: String
x,y :: String
y])   = "Or " 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]
++ ',' Char -> String -> String
forall a. a -> [a] -> [a]
: String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
showS (Xor [x :: String
x,y :: String
y])  = "Xor " 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]
++ ',' Char -> String -> String
forall a. a -> [a] -> [a]
: String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
showS (VarBool v :: String
v)  = "VarBool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
v
showS (DelayBool x :: String
x y :: String
y) = "DelayBool (" 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]
++ ")"
showS _               = String -> String
forall a. HasCallStack => String -> a
error "showS"

showN :: NetList -> String
showN :: NetList -> String
showN = Array Int String -> String
showA (Array Int String -> String)
-> (NetList -> Array Int String) -> NetList -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S (Sign Int) -> String) -> NetList -> Array Int String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (S String -> String
showS (S String -> String)
-> (S (Sign Int) -> S String) -> S (Sign Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sign Int -> String) -> S (Sign Int) -> S String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sign Int -> String
forall a. Show a => a -> String
show)

showA :: Array Int String -> String
showA :: Array Int String -> String
showA a :: Array Int String
a = "array " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Array Int String -> (Int, Int)
forall i e. Array i e -> (i, i)
bounds Array Int String
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [" 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 "," (((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i,s :: String
s) -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i 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]
++ ")")
                                         (Array Int String -> [(Int, String)]
forall i e. Ix i => Array i e -> [(i, e)]
assocs Array Int String
a)))
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"

showAll :: (NetList, a) -> String
showAll (n :: NetList
n,p :: a
p) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NetList -> String
showN NetList
n 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
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

net_ :: Checkable a => String -> a -> IO ()
net_ :: String -> a -> IO ()
net_ file :: String
file a :: a
a = do
  (NetList, Sign Int)
p <- a -> IO (NetList, Sign Int)
forall a. Checkable a => a -> IO (NetList, Sign Int)
net a
a
  String -> String -> IO ()
writeFile String
file ((NetList, Sign Int) -> String
forall a. Show a => (NetList, a) -> String
showAll (NetList, Sign Int)
p)

net :: Checkable a => a -> IO (NetList, Sign Int)
net :: a -> IO (NetList, Sign Int)
net a :: a
a =
  do (props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
     let top :: Signal Bool
top = case [Signal Bool]
props of
                [x :: Signal Bool
x] -> Signal Bool
x
                xs :: [Signal Bool]
xs  -> [Signal Bool] -> Signal Bool
andl [Signal Bool]
xs
     let (tab :: [(Int, S (Sign Int))]
tab, Object top' :: Sign Int
top') = Struct Symbol -> ([(Int, S (Sign Int))], Struct (Sign Int))
forall (f :: * -> *).
Sequent f =>
f Symbol -> ([(Int, S (Sign Int))], f (Sign Int))
table (Signal Bool -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct Signal Bool
top)
     (NetList, Sign Int) -> IO (NetList, Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, Int) -> [(Int, S (Sign Int))] -> NetList
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (0, [(Int, S (Sign Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, S (Sign Int))]
tabInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [(Int, S (Sign Int))]
tab, Sign Int
top')


table :: Sequent f => f Symbol -> ([(Int,S (Sign Int))], f (Sign Int))
table :: f Symbol -> ([(Int, S (Sign Int))], f (Sign Int))
table str :: f Symbol
str =
  (forall s. ST s ([(Int, S (Sign Int))], f (Sign Int)))
-> ([(Int, S (Sign Int))], f (Sign Int))
forall a. (forall s. ST s a) -> a
runST
  ( do STRef s Int
ref   <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef 0
       STRef s [(Int, S (Sign Int))]
table <- [(Int, S (Sign Int))] -> ST s (STRef s [(Int, S (Sign Int))])
forall a s. a -> ST s (STRef s a)
newSTRef []

       let define :: S (Sign Int) -> ST s (Sign Int)
define sym :: S (Sign Int)
sym = do
             [(Int, S (Sign Int))]
tab <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
             case S (Sign Int)
sym of
               And xs :: [Sign Int]
xs -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Or ((Sign Int -> Sign Int) -> [Sign Int] -> [Sign Int]
forall a b. (a -> b) -> [a] -> [b]
map Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg [Sign Int]
xs) ST s (Sign Int) -> (Sign Int -> ST s (Sign Int)) -> ST s (Sign Int)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign Int -> ST s (Sign Int))
-> (Sign Int -> Sign Int) -> Sign Int -> ST s (Sign Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg
               Or xs :: [Sign Int]
xs  -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Or [Sign Int]
xs
               Xor xs :: [Sign Int]
xs -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Xor [Sign Int]
xs
--                          v <- new
--                          writeSTRef table ((v,x):tab)
--                          return (Not v)
               Inv x :: Sign Int
x  -> Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg Sign Int
x)
               x :: S (Sign Int)
x      -> do Int
v <- ST s Int
new
                            STRef s [(Int, S (Sign Int))] -> [(Int, S (Sign Int))] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [(Int, S (Sign Int))]
table ((Int
v,S (Sign Int)
x)(Int, S (Sign Int))
-> [(Int, S (Sign Int))] -> [(Int, S (Sign Int))]
forall a. a -> [a] -> [a]
:[(Int, S (Sign Int))]
tab)
                            Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sign Int
forall a. a -> Sign a
Pos Int
v)

           bin :: ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin f :: [Sign Int] -> S (Sign Int)
f [x :: Sign Int
x]      = Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign Int
x
           bin f :: [Sign Int] -> S (Sign Int)
f (x :: Sign Int
x:y :: Sign Int
y:xs :: [Sign Int]
xs) = do
               Int
v <- ST s Int
new
               [(Int, S (Sign Int))]
tab <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
               STRef s [(Int, S (Sign Int))] -> [(Int, S (Sign Int))] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [(Int, S (Sign Int))]
table ((Int
v, [Sign Int] -> S (Sign Int)
f [Sign Int
x,Sign Int
y]) (Int, S (Sign Int))
-> [(Int, S (Sign Int))] -> [(Int, S (Sign Int))]
forall a. a -> [a] -> [a]
: [(Int, S (Sign Int))]
tab)
               ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
f (Int -> Sign Int
forall a. a -> Sign a
Pos Int
vSign Int -> [Sign Int] -> [Sign Int]
forall a. a -> [a] -> [a]
:[Sign Int]
xs)

           new :: ST s Int
new = do
             Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
ref
             STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
ref (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)
             Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

       f (Sign Int)
str' <- (S (Sign Int) -> ST s (Sign Int))
-> f Symbol -> ST s (f (Sign Int))
forall (f :: * -> *) v s.
Sequent f =>
(S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ S (Sign Int) -> ST s (Sign Int)
define f Symbol
str
       [(Int, S (Sign Int))]
tab  <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
       ([(Int, S (Sign Int))], f (Sign Int))
-> ST s ([(Int, S (Sign Int))], f (Sign Int))
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, S (Sign Int))]
tab, f (Sign Int)
str')
  )

netlistST_ :: Sequent f => (S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ :: (S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ define :: S v -> ST s v
define symbols :: f Symbol
symbols =
  do TableST s (S Symbol) v
tab <- ST s (TableST s (S Symbol) v)
forall s a b. ST s (TableST s a b)
tableST

     let gather :: Symbol -> ST s v
gather (Symbol sym :: Ref (S Symbol)
sym) =
           do Maybe v
visited <- TableST s (S Symbol) v -> Ref (S Symbol) -> ST s (Maybe v)
forall s a b. TableST s a b -> Ref a -> ST s (Maybe b)
findST TableST s (S Symbol) v
tab Ref (S Symbol)
sym
              case Maybe v
visited of
                Just v :: v
v  -> do v -> ST s v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
                Nothing -> (v -> ST s v) -> ST s v
forall a s. (a -> ST s a) -> ST s a
fixST ((v -> ST s v) -> ST s v) -> (v -> ST s v) -> ST s v
forall a b. (a -> b) -> a -> b
$ \v :: v
v -> do
                              TableST s (S Symbol) v -> Ref (S Symbol) -> v -> ST s ()
forall s a b. TableST s a b -> Ref a -> b -> ST s ()
extendST TableST s (S Symbol) v
tab Ref (S Symbol)
sym v
v
                              S v
s <- (Symbol -> ST s v) -> S Symbol -> ST s (S v)
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap Symbol -> ST s v
gather (Ref (S Symbol) -> S Symbol
forall a. Ref a -> a
deref Ref (S Symbol)
sym)
                              S v -> ST s v
define S v
s

      in (Symbol -> ST s v) -> f Symbol -> ST s (f v)
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap Symbol -> ST s v
gather f Symbol
symbols


{-
isLow  (Bool False) = True
isLow  (Inv s)      = isHigh (unsymbol s)
isLow  _            = False
isHigh (Bool True)  = True
isHigh (Inv s)      = isLow (unsymbol s)
isHigh _            = False
-}