module Lava.Verification
( Option(..)
, verify
, verifyWith
, ProofResult(..)
, verifyDir
, checkVerifyDir
)
where
import Lava.Signal
import Lava.Netlist
import Lava.Generic
import Lava.Sequent
import Lava.Property
import Lava.Error
import Lava.LavaDir
import Data.List
( intersperse
, isPrefixOf
, nub
)
import System.IO
( openFile
, IOMode(..)
, hPutStr
, hClose
)
import Lava.IOBuffering
( noBuffering
)
import Data.IORef
import System.Process (system)
import System.Exit (ExitCode(..))
verifyDir :: FilePath
verifyDir :: FilePath
verifyDir = "Verify"
data Option
= Name String
| ShowTime
| Sat Int
| NoBacktracking
| Depth Int
| Increasing
| RestrictStates
deriving (Option -> Option -> Bool
(Option -> Option -> Bool)
-> (Option -> Option -> Bool) -> Eq Option
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Option -> Option -> Bool
$c/= :: Option -> Option -> Bool
== :: Option -> Option -> Bool
$c== :: Option -> Option -> Bool
Eq, Int -> Option -> ShowS
[Option] -> ShowS
Option -> FilePath
(Int -> Option -> ShowS)
-> (Option -> FilePath) -> ([Option] -> ShowS) -> Show Option
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Option] -> ShowS
$cshowList :: [Option] -> ShowS
show :: Option -> FilePath
$cshow :: Option -> FilePath
showsPrec :: Int -> Option -> ShowS
$cshowsPrec :: Int -> Option -> ShowS
Show)
defaultOptions :: [Option]
defaultOptions :: [Option]
defaultOptions =
[Option
Increasing]
defaultValues :: [Option]
defaultValues :: [Option]
defaultValues =
[FilePath -> Option
Name "circuit", Int -> Option
Sat 1, Int -> Option
Depth 1]
sameOption :: Option -> Option -> Bool
sameOption :: Option -> Option -> Bool
sameOption opt1 :: Option
opt1 opt2 :: Option
opt2 = Option -> FilePath
tag Option
opt1 FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== Option -> FilePath
tag Option
opt2
where
tag :: Option -> FilePath
tag = [FilePath] -> FilePath
forall a. [a] -> a
head ([FilePath] -> FilePath)
-> (Option -> [FilePath]) -> Option -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
words (FilePath -> [FilePath])
-> (Option -> FilePath) -> Option -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Option -> FilePath
forall a. Show a => a -> FilePath
show
searchOptVal :: Read a => [Option] -> (a -> Option) -> a
searchOptVal :: [Option] -> (a -> Option) -> a
searchOptVal options :: [Option]
options what :: a -> Option
what = [Option] -> a
forall p. Read p => [Option] -> p
search ([Option]
options [Option] -> [Option] -> [Option]
forall a. [a] -> [a] -> [a]
++ [Option]
defaultValues)
where
opt' :: Option
opt' = a -> Option
what a
forall a. HasCallStack => a
undefined
search :: [Option] -> p
search [] = Error -> p
forall a. Error -> a
wrong Error
Lava.Error.Internal_OptionNotFound
search (opt :: Option
opt:opts :: [Option]
opts)
| Option -> Option -> Bool
sameOption Option
opt Option
opt' = FilePath -> p
forall a. Read a => FilePath -> a
read (FilePath -> [FilePath]
words (Option -> FilePath
forall a. Show a => a -> FilePath
show Option
opt) [FilePath] -> Int -> FilePath
forall a. [a] -> Int -> a
!! 1)
| Bool
otherwise = [Option] -> p
search [Option]
opts
searchOptBool :: [Option] -> Option -> Bool
searchOptBool :: [Option] -> Option -> Bool
searchOptBool options :: [Option]
options what :: Option
what = Option
what Option -> [Option] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Option]
options
verify :: Checkable a => a -> IO ProofResult
verify :: a -> IO ProofResult
verify a :: a
a = [Option] -> a -> IO ProofResult
forall a. Checkable a => [Option] -> a -> IO ProofResult
verifyWith [Option]
defaultOptions a
a
verifyWith :: Checkable a => [Option] -> a -> IO ProofResult
verifyWith :: [Option] -> a -> IO ProofResult
verifyWith options :: [Option]
options a :: a
a =
do IO ()
checkVerifyDir
IO ()
noBuffering
(props :: [Signal Bool]
props,model :: Model -> [[FilePath]]
model) <- a -> IO ([Signal Bool], Model -> [[FilePath]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[FilePath]])
properties a
a
(states :: [State]
states,pins :: Int
pins) <- FilePath -> [Signal Bool] -> IO ([State], Int)
writeDefinitions FilePath
defsFile [Signal Bool]
props
ProofResult
res <- FilePath -> [State] -> Int -> [Option] -> IO ProofResult
proveAll FilePath
defsFile [State]
states Int
pins [Option]
options
if ProofResult
res ProofResult -> ProofResult -> Bool
forall a. Eq a => a -> a -> Bool
== ProofResult
Falsifiable
then FilePath -> (Model -> [[FilePath]]) -> IO ()
displayModel FilePath
outFile Model -> [[FilePath]]
model
else () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res
where
defsFile :: FilePath
defsFile = FilePath
verifyDir FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
nameOpt FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ".defs"
outFile :: FilePath
outFile = FilePath
verifyDir FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/prover.out"
nameOpt :: FilePath
nameOpt = [Option] -> (FilePath -> Option) -> FilePath
forall a. Read a => [Option] -> (a -> Option) -> a
searchOptVal [Option]
options FilePath -> Option
Name
proveAll :: FilePath -> [State] -> Int -> [Option] -> IO ProofResult
proveAll :: FilePath -> [State] -> Int -> [Option] -> IO ProofResult
proveAll defsFile :: FilePath
defsFile states :: [State]
states quests :: Int
quests options :: [Option]
options =
case [[([FilePath], Bool, [(Int, Int)], [(Int, Int)])]]
actions of
[[]] ->
do FilePath -> IO ()
putStrLn "Nothing to prove! ... Valid."
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
Valid
[[(labels :: [FilePath]
labels, ini :: Bool
ini, assumps :: [(Int, Int)]
assumps, obligs :: [(Int, Int)]
obligs)]] ->
do [FilePath]
-> Bool -> [(Int, Int)] -> [(Int, Int)] -> IO ProofResult
forall a.
Show a =>
[FilePath] -> Bool -> [(Int, a)] -> [(Int, a)] -> IO ProofResult
proveUnit [FilePath]
labels Bool
ini [(Int, Int)]
assumps [(Int, Int)]
obligs
_ ->
do [[([FilePath], Bool, [(Int, Int)], [(Int, Int)])]]
-> IO ProofResult
forall a.
Show a =>
[[([FilePath], Bool, [(Int, a)], [(Int, a)])]] -> IO ProofResult
tryAll [[([FilePath], Bool, [(Int, Int)], [(Int, Int)])]]
actions
where
depths :: [Int]
depths
| Bool
incrOpt Bool -> Bool -> Bool
&& Bool -> Bool
not ([State] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [State]
states) = [Int
depthOpt ..]
| Bool
otherwise = [Int
depthOpt]
steps :: a -> [([FilePath], Bool, [a], [a])]
steps d :: a
d
| [State] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [State]
states = [ ([], Bool
True, [], [1]) ]
| Bool
otherwise = [ (["base " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
d], Bool
True, [], [1..a
d])
, (["step " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
d], Bool
False, [1..a
d], [a
da -> a -> a
forall a. Num a => a -> a -> a
+1])
]
pins :: ([FilePath], b, [a], [a])
-> b -> [([FilePath], b, [(a, b)], [(a, b)])]
pins (labels :: [FilePath]
labels, ini :: b
ini, assumps :: [a]
assumps, obligs :: [a]
obligs) n :: b
n
| b
n b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = [ ([FilePath]
labels, b
ini, (a -> (a, b)) -> [a] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (b -> a -> (a, b)
forall b a. b -> a -> (a, b)
pin 1) [a]
assumps, (a -> (a, b)) -> [a] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (b -> a -> (a, b)
forall b a. b -> a -> (a, b)
pin 1) [a]
obligs) ]
| Bool
otherwise = [ ( [FilePath]
labels [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ["pin " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> FilePath
forall a. Show a => a -> FilePath
show b
p]
, b
ini
, [ b -> a -> (a, b)
forall b a. b -> a -> (a, b)
pin b
p a
ass | a
ass <- [a]
assumps, b
p <- [1..b
n] ]
[(a, b)] -> [(a, b)] -> [(a, b)]
forall a. [a] -> [a] -> [a]
++ [ b -> a -> (a, b)
forall b a. b -> a -> (a, b)
pin b
p' a
obl | a
obl <- [a]
obligs, b
p' <- [1..b
pb -> b -> b
forall a. Num a => a -> a -> a
-1] ]
, [ b -> a -> (a, b)
forall b a. b -> a -> (a, b)
pin b
p a
obl | a
obl <- [a]
obligs ]
)
| b
p <- [1..b
n]
]
where
pin :: b -> a -> (a, b)
pin p :: b
p a :: a
a = (a
a, b
p)
actions :: [[([FilePath], Bool, [(Int, Int)], [(Int, Int)])]]
actions =
[ (([FilePath], Bool, [Int], [Int])
-> [([FilePath], Bool, [(Int, Int)], [(Int, Int)])])
-> [([FilePath], Bool, [Int], [Int])]
-> [([FilePath], Bool, [(Int, Int)], [(Int, Int)])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([FilePath], Bool, [Int], [Int])
-> Int -> [([FilePath], Bool, [(Int, Int)], [(Int, Int)])]
forall b b a.
(Eq b, Num b, Enum b, Show b) =>
([FilePath], b, [a], [a])
-> b -> [([FilePath], b, [(a, b)], [(a, b)])]
`pins` Int
quests) (Int -> [([FilePath], Bool, [Int], [Int])]
forall a.
(Num a, Show a, Enum a) =>
a -> [([FilePath], Bool, [a], [a])]
steps Int
d) | Int
d <- [Int]
depths ]
nameOpt :: FilePath
nameOpt = [Option] -> (FilePath -> Option) -> FilePath
forall a. Read a => [Option] -> (a -> Option) -> a
searchOptVal [Option]
options FilePath -> Option
Name
depthOpt :: Int
depthOpt = [Option] -> (Int -> Option) -> Int
forall a. Read a => [Option] -> (a -> Option) -> a
searchOptVal [Option]
options Int -> Option
Depth
incrOpt :: Bool
incrOpt = [Option] -> Option -> Bool
searchOptBool [Option]
options Option
Increasing
restrOpt :: Bool
restrOpt = [Option] -> Option -> Bool
searchOptBool [Option]
options Option
RestrictStates
tryAll :: [[([FilePath], Bool, [(Int, a)], [(Int, a)])]] -> IO ProofResult
tryAll [] =
do ProofResult -> IO ProofResult
forall b. Show b => b -> IO b
result ProofResult
Indeterminate
tryAll ([] : rest :: [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
rest) =
do ProofResult -> IO ProofResult
forall b. Show b => b -> IO b
result ProofResult
Valid
tryAll (((labels :: [FilePath]
labels, ini :: Bool
ini, assumps :: [(Int, a)]
assumps, obligs :: [(Int, a)]
obligs) : tries :: [([FilePath], Bool, [(Int, a)], [(Int, a)])]
tries) : rest :: [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
rest) =
do ProofResult
r <- [FilePath] -> Bool -> [(Int, a)] -> [(Int, a)] -> IO ProofResult
forall a.
Show a =>
[FilePath] -> Bool -> [(Int, a)] -> [(Int, a)] -> IO ProofResult
proveUnit [FilePath]
labels Bool
ini [(Int, a)]
assumps [(Int, a)]
obligs
case ProofResult
r of
Valid -> [[([FilePath], Bool, [(Int, a)], [(Int, a)])]] -> IO ProofResult
tryAll ([([FilePath], Bool, [(Int, a)], [(Int, a)])]
tries [([FilePath], Bool, [(Int, a)], [(Int, a)])]
-> [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
-> [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
forall a. a -> [a] -> [a]
: [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
rest)
Falsifiable | Bool -> Bool
not Bool
ini -> [[([FilePath], Bool, [(Int, a)], [(Int, a)])]] -> IO ProofResult
tryAll [[([FilePath], Bool, [(Int, a)], [(Int, a)])]]
rest
| Bool
ini -> ProofResult -> IO ProofResult
forall b. Show b => b -> IO b
result ProofResult
Falsifiable
Indeterminate -> ProofResult -> IO ProofResult
forall b. Show b => b -> IO b
result ProofResult
Indeterminate
result :: b -> IO b
result r :: b
r =
do FilePath -> IO ()
putStrLn "--"
FilePath -> IO ()
putStrLn ("Result: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> FilePath
forall a. Show a => a -> FilePath
show b
r FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ".")
b -> IO b
forall (m :: * -> *) a. Monad m => a -> m a
return b
r
proveUnit :: [FilePath] -> Bool -> [(Int, a)] -> [(Int, a)] -> IO ProofResult
proveUnit labels :: [FilePath]
labels ini :: Bool
ini assumps :: [(Int, a)]
assumps obligs :: [(Int, a)]
obligs =
do FilePath -> IO () -> [FilePath] -> [Option] -> IO ProofResult
proveFile FilePath
mainFile IO ()
create [FilePath]
labels [Option]
options
where
create :: IO ()
create =
do IO ()
writeHeader
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
[ FilePath -> FilePath -> Int -> IO ()
instantiateFile FilePath
defsFile FilePath
mainFile Int
t
| Int
t <- [Int]
times
]
[FilePath] -> IO ()
appendAssumptions
([FilePath] -> IO ()) -> [FilePath] -> IO ()
forall a b. (a -> b) -> a -> b
$ [ (Int, a) -> FilePath
forall a a. (Show a, Show a) => (a, a) -> FilePath
quest (Int, a)
ass
| (Int, a)
ass <- [(Int, a)]
assumps
]
[FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [ "~" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
init Int
t
| Int
t <- [Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
times
]
[FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ( if Bool
ini then [Integer -> FilePath
forall a. Show a => a -> FilePath
init 1]
else
if Bool
restrOpt then [FilePath]
restrictStates
else []
)
[FilePath] -> IO ()
appendObligations
([FilePath] -> IO ()) -> [FilePath] -> IO ()
forall a b. (a -> b) -> a -> b
$ [ (Int, a) -> FilePath
forall a a. (Show a, Show a) => (a, a) -> FilePath
quest (Int, a)
obl
| (Int, a)
obl <- [(Int, a)]
obligs
]
IO ()
appendFooter
mainFile :: FilePath
mainFile =
FilePath
verifyDir FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
clean (FilePath
nameOpt FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ".prov" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ("." FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++) [FilePath]
labels)
clean :: ShowS
clean (' ':s :: FilePath
s) = '_'Char -> ShowS
forall a. a -> [a] -> [a]
:ShowS
clean FilePath
s
clean (c :: Char
c:s :: FilePath
s) = Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:ShowS
clean FilePath
s
clean [] = []
times :: [Int]
times =
[Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub [ Int
t | (t :: Int
t, p :: a
p) <- [(Int, a)]
assumps [(Int, a)] -> [(Int, a)] -> [(Int, a)]
forall a. [a] -> [a] -> [a]
++ [(Int, a)]
obligs ]
init :: a -> FilePath
init t :: a
t =
"init_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
t
quest :: (a, a) -> FilePath
quest (t :: a
t, p :: a
p) =
"quest_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
t FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "_n" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
p
writeHeader :: IO ()
writeHeader = FilePath -> FilePath -> IO ()
writeFile FilePath
mainFile (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
[ "/* Generated by Lava 2000 */"
, "/* options: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [Option] -> FilePath
forall a. Show a => a -> FilePath
show [Option]
options FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " */"
, ""
, "AND("
, ""
]
appendAssumptions :: [FilePath] -> IO ()
appendAssumptions [] = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
appendAssumptions ass :: [FilePath]
ass = FilePath -> FilePath -> IO ()
appendFile FilePath
mainFile (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
[ ""
, "/* assumptions */"
, ""
] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ",") [FilePath]
ass
appendObligations :: [FilePath] -> IO ()
appendObligations obs :: [FilePath]
obs = FilePath -> FilePath -> IO ()
appendFile FilePath
mainFile (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
[ ""
, "big_question <-> AND("
, "/* proof obligations */"
, ""
] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ",") [FilePath]
obs
appendFooter :: IO ()
appendFooter = FilePath -> FilePath -> IO ()
appendFile FilePath
mainFile (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
[ ""
, "/* the big question */"
, "TRUE)) -> big_question"
, ""
]
restrictStates :: [FilePath]
restrictStates =
[ Int -> Int -> [State] -> FilePath
forall a a. (Show a, Show a) => a -> a -> [State] -> FilePath
notEqual (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (Int
t'Int -> Int -> Int
forall a. Num a => a -> a -> a
-1) [State]
states | Int
t <- [Int]
times, Int
t' <- [Int]
times, Int
t' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
t ]
notEqual :: a -> a -> [State] -> FilePath
notEqual t :: a
t t' :: a
t' states :: [State]
states =
"OR(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse ", " [ "~(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
t FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
eq FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
t' FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
| (eq :: FilePath
eq,s :: FilePath
s) <- [State]
states ])
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
data ProofResult
= Valid
| Falsifiable
| Indeterminate
deriving (ProofResult -> ProofResult -> Bool
(ProofResult -> ProofResult -> Bool)
-> (ProofResult -> ProofResult -> Bool) -> Eq ProofResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofResult -> ProofResult -> Bool
$c/= :: ProofResult -> ProofResult -> Bool
== :: ProofResult -> ProofResult -> Bool
$c== :: ProofResult -> ProofResult -> Bool
Eq, Int -> ProofResult -> ShowS
[ProofResult] -> ShowS
ProofResult -> FilePath
(Int -> ProofResult -> ShowS)
-> (ProofResult -> FilePath)
-> ([ProofResult] -> ShowS)
-> Show ProofResult
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [ProofResult] -> ShowS
$cshowList :: [ProofResult] -> ShowS
show :: ProofResult -> FilePath
$cshow :: ProofResult -> FilePath
showsPrec :: Int -> ProofResult -> ShowS
$cshowsPrec :: Int -> ProofResult -> ShowS
Show)
proveFile :: FilePath -> IO () -> [String] -> [Option] -> IO ProofResult
proveFile :: FilePath -> IO () -> [FilePath] -> [Option] -> IO ProofResult
proveFile file :: FilePath
file before :: IO ()
before labels :: [FilePath]
labels options :: [Option]
options =
do FilePath -> IO ()
putStr ( "Proving:"
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse "," (ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (" " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++) [FilePath]
labels))
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
)
IO ()
before
FilePath -> IO ()
putStr "... "
FilePath
lavadir <- IO FilePath
getLavaDir
ExitCode
x <- FilePath -> IO ExitCode
system ( FilePath
lavadir
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/Scripts/prover.wrapper "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
file
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
opts
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " -model first"
)
let res :: ProofResult
res = case ExitCode
x of
ExitSuccess -> ProofResult
Valid
ExitFailure 1 -> ProofResult
Indeterminate
ExitFailure _ -> ProofResult
Falsifiable
FilePath -> IO ()
putStrLn (ProofResult -> FilePath
forall a. Show a => a -> FilePath
show ProofResult
res FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ".")
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res
where
satOpt :: Int
satOpt = [Option] -> (Int -> Option) -> Int
forall a. Read a => [Option] -> (a -> Option) -> a
searchOptVal [Option]
options Int -> Option
Sat
noBackOpt :: Bool
noBackOpt = [Option] -> Option -> Bool
searchOptBool [Option]
options Option
NoBacktracking
timeOpt :: Bool
timeOpt = [Option] -> Option -> Bool
searchOptBool [Option]
options Option
ShowTime
opts :: FilePath
opts = (if Bool
timeOpt then "-showTime " else "")
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ("-t " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
satOpt FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " ")
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
noBackOpt then "" else "-b")
writeDefinitions :: FilePath -> [Signal Bool] -> IO ([State],Int)
writeDefinitions :: FilePath -> [Signal Bool] -> IO ([State], Int)
writeDefinitions file :: FilePath
file props :: [Signal Bool]
props =
do Handle
han <- FilePath -> IOMode -> IO Handle
openFile FilePath
file IOMode
WriteMode
IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0
IORef [State]
sts <- [State] -> IO (IORef [State])
forall a. a -> IO (IORef a)
newIORef []
let new :: IO Timed
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
IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
var Integer
n'
Timed -> IO Timed
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Timed
Now ("w" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
n'))
define :: a -> S Timed -> IO ()
define v :: a
v s :: S Timed
s =
do Handle -> FilePath -> IO ()
hPutStr Handle
han (FilePath
def FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ";\n")
case S Timed
s of
DelayBool x :: Timed
x y :: Timed
y -> State -> IO ()
state ("<->",Timed -> FilePath
the Timed
y)
DelayInt x :: Timed
x y :: Timed
y -> State -> IO ()
state ("=",Timed -> FilePath
the Timed
y)
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
def :: FilePath
def =
case S Timed
s of
Bool True -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "TRUE"
Bool False -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "FALSE"
Inv x -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> Timed -> FilePath
forall a. Show a => FilePath -> a -> FilePath
op1 "~" Timed
x
And xs -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [Timed] -> ShowS
forall a. Show a => FilePath -> FilePath -> [a] -> ShowS
opl "AND" "," [Timed]
xs "TRUE"
Or xs -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [Timed] -> ShowS
forall a. Show a => FilePath -> FilePath -> [a] -> ShowS
opl "OR" "," [Timed]
xs "FALSE"
Xor xs -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [Timed] -> ShowS
forall a. Show a => FilePath -> FilePath -> [a] -> ShowS
opl "XOR" "," [Timed]
xs "FALSE"
Int n -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n
Neg x -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> Timed -> FilePath
forall a. Show a => FilePath -> a -> FilePath
op1 "-" Timed
x
Div x y -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> Timed -> Timed -> FilePath
forall a a. (Show a, Show a) => FilePath -> a -> a -> FilePath
op2 "/" Timed
x Timed
y
Mod x y -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> Timed -> Timed -> FilePath
forall a a. (Show a, Show a) => FilePath -> a -> a -> FilePath
op2 "%" Timed
x Timed
y
Plus xs -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [Timed] -> ShowS
forall a. Show a => FilePath -> FilePath -> [a] -> ShowS
opl "" "+" [Timed]
xs "0"
Times xs -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [Timed] -> ShowS
forall a. Show a => FilePath -> FilePath -> [a] -> ShowS
opl "" "*" [Timed]
xs "1"
Gte x y -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath -> Timed -> Timed -> FilePath
forall a a. (Show a, Show a) => FilePath -> a -> a -> FilePath
op2 ">=" Timed
x Timed
y
Equal xs -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [Timed] -> FilePath
forall a. Show a => [a] -> FilePath
equal [Timed]
xs
If x y z -> Timed -> FilePath -> ShowS
forall a. Show a => a -> FilePath -> ShowS
iff Timed
x (FilePath -> a -> Timed -> FilePath
forall a a. (Show a, Show a) => FilePath -> a -> a -> FilePath
op2 "=" a
v Timed
y) (FilePath -> a -> Timed -> FilePath
forall a a. (Show a, Show a) => FilePath -> a -> a -> FilePath
op2 "=" a
v Timed
z)
VarBool s -> ShowS
prop ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Timed -> FilePath
forall a. Show a => a -> FilePath
op0 (FilePath -> Timed
Now FilePath
s)
VarInt s -> ShowS
arit ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Timed -> FilePath
forall a. Show a => a -> FilePath
op0 (FilePath -> Timed
Now FilePath
s)
DelayBool x y -> Timed -> FilePath -> ShowS
forall a. Show a => a -> FilePath -> ShowS
iff Timed
ini (ShowS
prop (Timed -> FilePath
forall a. Show a => a -> FilePath
op0 Timed
x)) (ShowS
prop (Timed -> FilePath
forall a. Show a => a -> FilePath
op0 (Timed -> Timed
pre Timed
y)))
DelayInt x y -> Timed -> FilePath -> ShowS
forall a. Show a => a -> FilePath -> ShowS
iff Timed
ini (ShowS
arit (Timed -> FilePath
forall a. Show a => a -> FilePath
op0 Timed
x)) (ShowS
arit (Timed -> FilePath
forall a. Show a => a -> FilePath
op0 (Timed -> Timed
pre Timed
y)))
prop :: ShowS
prop form :: FilePath
form =
"(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
v FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " <-> (" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
form FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
arit :: ShowS
arit expr :: FilePath
expr =
"(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
v FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " = (" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
expr FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
iff :: a -> FilePath -> ShowS
iff c :: a
c x :: FilePath
x y :: FilePath
y =
"(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
op0 a
c FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
x FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ") & (~"
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
op0 a
c FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
y FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
state :: State -> IO ()
state s :: State
s =
do [State]
xs <- IORef [State] -> IO [State]
forall a. IORef a -> IO a
readIORef IORef [State]
sts
IORef [State] -> [State] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef [State]
sts (State
sState -> [State] -> [State]
forall a. a -> [a] -> [a]
:[State]
xs)
op0 :: a -> FilePath
op0 v :: a
v = a -> FilePath
forall a. Show a => a -> FilePath
show a
v
op1 :: FilePath -> a -> FilePath
op1 op :: FilePath
op v :: a
v = FilePath
op FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
v
op2 :: FilePath -> a -> a -> FilePath
op2 op :: FilePath
op v :: a
v w :: a
w = "(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
v FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
op FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
w FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
opl :: FilePath -> FilePath -> [a] -> ShowS
opl fun :: FilePath
fun con :: FilePath
con [] nul :: FilePath
nul = FilePath
nul
opl fun :: FilePath
fun con :: FilePath
con [x :: a
x] nul :: FilePath
nul = a -> FilePath
forall a. Show a => a -> FilePath
show a
x
opl fun :: FilePath
fun con :: FilePath
con xs :: [a]
xs nul :: FilePath
nul =
FilePath
fun FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "(" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse FilePath
con ((a -> FilePath) -> [a] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map a -> FilePath
forall a. Show a => a -> FilePath
show [a]
xs)) FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
equal :: [a] -> FilePath
equal (x :: a
x:y :: a
y:xs :: [a]
xs) =
(a -> FilePath
forall a. Show a => a -> FilePath
show a
x FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
y) FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " & " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> FilePath
equal (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)
equal _ = "TRUE"
~(Compound vs :: [Struct Timed]
vs) <- IO Timed
-> (Timed -> S Timed -> IO ())
-> Struct Symbol
-> IO (Struct Timed)
forall (f :: * -> *) v.
Sequent f =>
IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistIO IO Timed
new Timed -> S Timed -> IO ()
forall a. Show a => a -> S Timed -> IO ()
define ([Signal Bool] -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct [Signal Bool]
props)
let quests :: [Indexed]
quests = [ Timed -> Int -> Indexed
Index Timed
quest Int
i | Int
i <- [1..] ]
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Handle -> FilePath -> IO ()
hPutStr Handle
han (Indexed -> FilePath
forall a. Show a => a -> FilePath
show Indexed
q FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " <-> " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Timed -> FilePath
forall a. Show a => a -> FilePath
show Timed
v FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ";\n")
| (q :: Indexed
q, Object v :: Timed
v) <- [Indexed]
quests [Indexed] -> [Struct Timed] -> [(Indexed, Struct Timed)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Struct Timed]
vs
]
Handle -> IO ()
hClose Handle
han
[State]
states <- IORef [State] -> IO [State]
forall a. IORef a -> IO a
readIORef IORef [State]
sts
([State], Int) -> IO ([State], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([State]
states, [Struct Timed] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Struct Timed]
vs)
type State
= (String, String)
data Timed
= Now String
| Pre String
instance Show Timed where
show :: Timed -> FilePath
show (Now a :: FilePath
a) = FilePath
a FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "$now"
show (Pre a :: FilePath
a) = FilePath
a FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "$pre"
the :: Timed -> FilePath
the (Now a :: FilePath
a) = FilePath
a
the (Pre a :: FilePath
a) = FilePath
a
pre :: Timed -> Timed
pre (Now a :: FilePath
a) = FilePath -> Timed
Pre FilePath
a
ini :: Timed
ini = FilePath -> Timed
Now "init"
quest :: Timed
quest = FilePath -> Timed
Now "quest"
data Indexed
= Index Timed Int
instance Show Indexed where
show :: Indexed -> FilePath
show (Index a :: Timed
a n :: Int
n) = Timed -> FilePath
forall a. Show a => a -> FilePath
show Timed
a FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "_n" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n
displayModel :: FilePath -> (Model -> [[String]]) -> IO ()
displayModel :: FilePath -> (Model -> [[FilePath]]) -> IO ()
displayModel file :: FilePath
file showModel :: Model -> [[FilePath]]
showModel =
do FilePath
s <- FilePath -> IO FilePath
readFile FilePath
file
let (first :: FilePath
first : model :: [FilePath]
model) = FilePath -> [FilePath]
lines FilePath
s
if "# counter model" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
first
then do let inps :: [State]
inps = [FilePath] -> [State]
inputs [FilePath]
model
table :: Model
table = [State] -> Model -> Model
makeTable [State]
inps []
repr :: [[FilePath]]
repr = Model -> [[FilePath]]
showModel Model
table
FilePath -> IO ()
putStr ([FilePath] -> FilePath
unlines (([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map [FilePath] -> FilePath
showInput [[FilePath]]
repr))
else () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
inputs :: [FilePath] -> [State]
inputs [] = []
inputs (l :: FilePath
l:ls :: [FilePath]
ls) =
case FilePath -> [FilePath]
words FilePath
l of
[v :: FilePath
v@('i':_), "=", val :: FilePath
val] -> (FilePath
v, FilePath
val) State -> [State] -> [State]
forall a. a -> [a] -> [a]
: [State]
rest
[v :: FilePath
v@('i':_)] -> (FilePath
v, "high") State -> [State] -> [State]
forall a. a -> [a] -> [a]
: [State]
rest
['~':v :: FilePath
v@('i':_)] -> (FilePath
v, "low") State -> [State] -> [State]
forall a. a -> [a] -> [a]
: [State]
rest
_ -> [State]
rest
where
rest :: [State]
rest = [FilePath] -> [State]
inputs [FilePath]
ls
makeTable :: [State] -> Model -> Model
makeTable [] table :: Model
table =
Model
table
makeTable ((v :: FilePath
v,val :: FilePath
val):inps :: [State]
inps) table :: Model
table =
[State] -> Model -> Model
makeTable [State]
inps (FilePath -> Int -> FilePath -> Model -> Model
forall a.
Eq a =>
a -> Int -> FilePath -> [(a, [FilePath])] -> [(a, [FilePath])]
extend FilePath
name (FilePath -> Int
forall a. Read a => FilePath -> a
read FilePath
time) FilePath
val Model
table)
where
n :: Int
n = FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
v
name :: FilePath
name = Int -> ShowS
forall a. Int -> [a] -> [a]
take (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- FilePath -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
time Int -> Int -> Int
forall a. Num a => a -> a -> a
- 2) FilePath
v
time :: FilePath
time = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isDigit ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath
v
isDigit :: Char -> Bool
isDigit d :: Char
d = '0' Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
d Bool -> Bool -> Bool
&& Char
d Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= '9'
extend :: a -> Int -> FilePath -> [(a, [FilePath])] -> [(a, [FilePath])]
extend name :: a
name time :: Int
time val :: FilePath
val [] =
a -> Int -> FilePath -> [(a, [FilePath])] -> [(a, [FilePath])]
extend a
name Int
time FilePath
val [(a
name, [])]
extend name :: a
name time :: Int
time val :: FilePath
val (entry :: (a, [FilePath])
entry@(name' :: a
name',vals :: [FilePath]
vals):table :: [(a, [FilePath])]
table)
| a
name a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
name' = (a, [FilePath])
updated (a, [FilePath]) -> [(a, [FilePath])] -> [(a, [FilePath])]
forall a. a -> [a] -> [a]
: [(a, [FilePath])]
table
| Bool
otherwise = (a, [FilePath])
entry (a, [FilePath]) -> [(a, [FilePath])] -> [(a, [FilePath])]
forall a. a -> [a] -> [a]
: a -> Int -> FilePath -> [(a, [FilePath])] -> [(a, [FilePath])]
extend a
name Int
time FilePath
val [(a, [FilePath])]
table
where
updated :: (a, [FilePath])
updated = (a
name', Int -> [FilePath] -> [FilePath]
forall a. (Eq a, Num a) => a -> [FilePath] -> [FilePath]
make (Int
time Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [FilePath]
vals [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
val] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ Int -> [FilePath] -> [FilePath]
forall a. Int -> [a] -> [a]
drop Int
time [FilePath]
vals)
make :: a -> [FilePath] -> [FilePath]
make 0 xs :: [FilePath]
xs = []
make n :: a
n [] = a -> [FilePath] -> [FilePath]
make a
n ["?"]
make n :: a
n (x :: FilePath
x:xs :: [FilePath]
xs) = FilePath
x FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: a -> [FilePath] -> [FilePath]
make (a
na -> a -> a
forall a. Num a => a -> a -> a
-1) [FilePath]
xs
showInput :: [FilePath] -> FilePath
showInput [x :: FilePath
x] = FilePath
x
showInput xs :: [FilePath]
xs = "<" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
intersperse "," [FilePath]
xs) FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ">"
instantiateFile :: FilePath -> FilePath -> Int -> IO ()
instantiateFile :: FilePath -> FilePath -> Int -> IO ()
instantiateFile from :: FilePath
from to :: FilePath
to t :: Int
t =
do FilePath -> FilePath -> IO ()
appendFile FilePath
to ("/* time instance " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
t FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " */\n")
FilePath -> IO ExitCode
system ( "sed "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "-e 's/$now/_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
t FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/g' "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "-e 's/$pre/_t" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "/g' "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ "-e 's/;/,/g' "
FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " < " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
from FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ " >> " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
to
)
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkVerifyDir :: IO ()
checkVerifyDir :: IO ()
checkVerifyDir =
do FilePath -> IO ExitCode
system ("mkdir -p " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
verifyDir)
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()