{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Tools.Induction (
InductionResult(..), InductionStep(..), induct, inductWith
) where
import Data.SBV
import Data.SBV.Control
import Data.List (intercalate)
import Control.Monad (when)
data InductionStep = Initiation (Maybe String)
| Consecution (Maybe String)
| PartialCorrectness
instance Show InductionStep where
show :: InductionStep -> String
show (Initiation Maybe String
Nothing) = String
"initiation"
show (Initiation (Just String
s)) = String
"initiation for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
show (Consecution Maybe String
Nothing) = String
"consecution"
show (Consecution (Just String
s)) = String
"consecution for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
show InductionStep
PartialCorrectness = String
"partial correctness"
data InductionResult a = Failed InductionStep a
| Proven
instance Show a => Show (InductionResult a) where
show :: InductionResult a -> String
show InductionResult a
Proven = String
"Q.E.D."
show (Failed InductionStep
s a
e) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"Failed while establishing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InductionStep -> String
forall a. Show a => a -> String
show InductionStep
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
, String
"Counter-example to inductiveness:"
, String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (a -> String
forall a. Show a => a -> String
show a
e)]
]
induct :: (Show res, Queriable IO st, res ~ QueryResult st)
=> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct :: forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct = SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith SMTConfig
defaultSMTCfg
inductWith :: (Show res, Queriable IO st, res ~ QueryResult st)
=> SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith :: forall res st.
(Show res, Queriable IO st, res ~ QueryResult st) =>
SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith SMTConfig
cfg Bool
chatty Symbolic ()
setup st -> SBool
initial st -> [st]
trans [(String, st -> SBool)]
strengthenings st -> SBool
inv st -> (SBool, SBool)
goal =
String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving initiation"
(\st
s -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
inv st
s)
(InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Initiation Maybe String
forall a. Maybe a
Nothing))
(IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ [(String, st -> SBool)]
-> IO (InductionResult res) -> IO (InductionResult res)
strengthen [(String, st -> SBool)]
strengthenings
(IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving consecution"
(\st
s -> [SBool] -> SBool
sAnd (st -> SBool
inv st
s SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [st -> SBool
st st
s | (String
_, st -> SBool
st) <- [(String, st -> SBool)]
strengthenings]) SBool -> SBool -> SBool
.=> (st -> SBool) -> [st] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll st -> SBool
inv (st -> [st]
trans st
s))
(InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Consecution Maybe String
forall a. Maybe a
Nothing))
(IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
"Proving partial correctness"
(\st
s -> let (SBool
term, SBool
result) = st -> (SBool, SBool)
goal st
s in st -> SBool
inv st
s SBool -> SBool -> SBool
.&& SBool
term SBool -> SBool -> SBool
.=> SBool
result)
(InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed InductionStep
PartialCorrectness)
(String -> IO ()
msg String
"Done" IO () -> IO (InductionResult res) -> IO (InductionResult res)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InductionResult res -> IO (InductionResult res)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return InductionResult res
forall a. InductionResult a
Proven)
where msg :: String -> IO ()
msg = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
chatty (IO () -> IO ()) -> (String -> IO ()) -> String -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn
try :: String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try String
m st -> SBool
p res -> InductionResult res
wrap IO (InductionResult res)
cont = do String -> IO ()
msg String
m
Maybe res
res <- (st -> SBool) -> IO (Maybe res)
check st -> SBool
p
case Maybe res
res of
Just res
ex -> InductionResult res -> IO (InductionResult res)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InductionResult res -> IO (InductionResult res))
-> InductionResult res -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ res -> InductionResult res
wrap res
ex
Maybe res
Nothing -> IO (InductionResult res)
cont
check :: (st -> SBool) -> IO (Maybe res)
check st -> SBool
p = SMTConfig -> Symbolic (Maybe res) -> IO (Maybe res)
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith SMTConfig
cfg (Symbolic (Maybe res) -> IO (Maybe res))
-> Symbolic (Maybe res) -> IO (Maybe res)
forall a b. (a -> b) -> a -> b
$ do
Symbolic ()
setup
Query (Maybe res) -> Symbolic (Maybe res)
forall a. Query a -> Symbolic a
query (Query (Maybe res) -> Symbolic (Maybe res))
-> Query (Maybe res) -> Symbolic (Maybe res)
forall a b. (a -> b) -> a -> b
$ do st
st <- QueryT IO st
forall (m :: * -> *) a. Queriable m a => QueryT m a
create
SBool -> QueryT IO ()
forall a. QuantifiedBool a => a -> QueryT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (st -> SBool
p st
st)
CheckSatResult
cs <- Query CheckSatResult
checkSat
case CheckSatResult
cs of
CheckSatResult
Unk -> String -> Query (Maybe res)
forall a. HasCallStack => String -> a
error String
"Solver said unknown"
DSat{} -> String -> Query (Maybe res)
forall a. HasCallStack => String -> a
error String
"Solver returned a delta-sat result"
CheckSatResult
Unsat -> Maybe res -> Query (Maybe res)
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe res
forall a. Maybe a
Nothing
CheckSatResult
Sat -> do IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
msg String
"Failed:"
res
ex <- st -> QueryT IO (QueryResult st)
forall (m :: * -> *) a.
Queriable m a =>
a -> QueryT m (QueryResult a)
project st
st
IO () -> QueryT IO ()
forall a. IO a -> Query a
io (IO () -> QueryT IO ()) -> IO () -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
msg (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ res -> String
forall a. Show a => a -> String
show res
ex
Maybe res -> Query (Maybe res)
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe res -> Query (Maybe res)) -> Maybe res -> Query (Maybe res)
forall a b. (a -> b) -> a -> b
$ res -> Maybe res
forall a. a -> Maybe a
Just res
ex
strengthen :: [(String, st -> SBool)]
-> IO (InductionResult res) -> IO (InductionResult res)
strengthen [] IO (InductionResult res)
cont = IO (InductionResult res)
cont
strengthen ((String
nm, st -> SBool
st):[(String, st -> SBool)]
sts) IO (InductionResult res)
cont = String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try (String
"Proving strengthening initiation : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
(\st
s -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
st st
s)
(InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Initiation (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)))
(IO (InductionResult res) -> IO (InductionResult res))
-> IO (InductionResult res) -> IO (InductionResult res)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
try (String
"Proving strengthening consecution: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
(\st
s -> st -> SBool
st st
s SBool -> SBool -> SBool
.=> (st -> SBool) -> [st] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll st -> SBool
st (st -> [st]
trans st
s))
(InductionStep -> res -> InductionResult res
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Consecution (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)))
([(String, st -> SBool)]
-> IO (InductionResult res) -> IO (InductionResult res)
strengthen [(String, st -> SBool)]
sts IO (InductionResult res)
cont)