{-# LANGUAGE FlexibleContexts #-}
{-# 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 Nothing) = "initiation"
show (Initiation (Just s :: String
s)) = "initiation for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
show (Consecution Nothing) = "consecution"
show (Consecution (Just s :: String
s)) = "consecution for strengthening " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s
show PartialCorrectness = "partial correctness"
data InductionResult a = Failed InductionStep a
| Proven
instance Show a => Show (InductionResult a) where
show :: InductionResult a -> String
show Proven = "Q.E.D."
show (Failed s :: InductionStep
s e :: a
e) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [ "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]
++ "."
, "Counter-example to inductiveness:"
, String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [" " 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)
=> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
induct :: 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) =>
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)
=> SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith :: SMTConfig
-> Bool
-> Symbolic ()
-> (st -> SBool)
-> (st -> [st])
-> [(String, st -> SBool)]
-> (st -> SBool)
-> (st -> (SBool, SBool))
-> IO (InductionResult res)
inductWith cfg :: SMTConfig
cfg chatty :: Bool
chatty setup :: Symbolic ()
setup initial :: st -> SBool
initial trans :: st -> [st]
trans strengthenings :: [(String, st -> SBool)]
strengthenings inv :: st -> SBool
inv goal :: st -> (SBool, SBool)
goal =
String
-> (st -> SBool)
-> (res -> InductionResult res)
-> IO (InductionResult res)
-> IO (InductionResult res)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try "Proving initiation"
(\s :: 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)
forall a.
(Queriable IO st a, Show a) =>
[(String, st -> SBool)]
-> IO (InductionResult a) -> IO (InductionResult a)
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)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try "Proving consecution"
(\s :: st
s -> [SBool] -> SBool
sAnd (st -> SBool
inv st
s SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [st -> SBool
st st
s | (_, st :: 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)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try "Proving partial correctness"
(\s :: st
s -> let (term :: SBool
term, result :: 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 "Done" IO () -> IO (InductionResult res) -> IO (InductionResult res)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InductionResult res -> IO (InductionResult res)
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 -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try m :: String
m p :: a -> SBool
p wrap :: t -> b
wrap cont :: IO b
cont = do String -> IO ()
msg String
m
Maybe t
res <- (a -> SBool) -> IO (Maybe t)
forall a a.
(Queriable IO a a, Show a) =>
(a -> SBool) -> IO (Maybe a)
check a -> SBool
p
case Maybe t
res of
Just ex :: t
ex -> b -> IO b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> IO b) -> b -> IO b
forall a b. (a -> b) -> a -> b
$ t -> b
wrap t
ex
Nothing -> IO b
cont
check :: (a -> SBool) -> IO (Maybe a)
check p :: a -> SBool
p = SMTConfig -> Symbolic (Maybe a) -> IO (Maybe a)
forall a. SMTConfig -> Symbolic a -> IO a
runSMTWith SMTConfig
cfg (Symbolic (Maybe a) -> IO (Maybe a))
-> Symbolic (Maybe a) -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ do
Symbolic ()
setup
Query (Maybe a) -> Symbolic (Maybe a)
forall a. Query a -> Symbolic a
query (Query (Maybe a) -> Symbolic (Maybe a))
-> Query (Maybe a) -> Symbolic (Maybe a)
forall a b. (a -> b) -> a -> b
$ do a
st <- QueryT IO a
forall (m :: * -> *) a b. Queriable m a b => QueryT m a
create
SBool -> QueryT IO ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> QueryT IO ()) -> SBool -> QueryT IO ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (a -> SBool
p a
st)
CheckSatResult
cs <- Query CheckSatResult
checkSat
case CheckSatResult
cs of
Unk -> String -> Query (Maybe a)
forall a. HasCallStack => String -> a
error "Solver said unknown"
Unsat -> Maybe a -> Query (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
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 "Failed:"
a
ex <- a -> QueryT IO a
forall (m :: * -> *) a b. Queriable m a b => a -> QueryT m b
project a
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
$ a -> String
forall a. Show a => a -> String
show a
ex
Maybe a -> Query (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Query (Maybe a)) -> Maybe a -> Query (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
ex
strengthen :: [(String, st -> SBool)]
-> IO (InductionResult a) -> IO (InductionResult a)
strengthen [] cont :: IO (InductionResult a)
cont = IO (InductionResult a)
cont
strengthen ((nm :: String
nm, st :: st -> SBool
st):sts :: [(String, st -> SBool)]
sts) cont :: IO (InductionResult a)
cont = String
-> (st -> SBool)
-> (a -> InductionResult a)
-> IO (InductionResult a)
-> IO (InductionResult a)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try ("Proving strengthening initation : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
(\s :: st
s -> st -> SBool
initial st
s SBool -> SBool -> SBool
.=> st -> SBool
st st
s)
(InductionStep -> a -> InductionResult a
forall a. InductionStep -> a -> InductionResult a
Failed (Maybe String -> InductionStep
Initiation (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)))
(IO (InductionResult a) -> IO (InductionResult a))
-> IO (InductionResult a) -> IO (InductionResult a)
forall a b. (a -> b) -> a -> b
$ String
-> (st -> SBool)
-> (a -> InductionResult a)
-> IO (InductionResult a)
-> IO (InductionResult a)
forall a t b.
(Queriable IO a t, Show t) =>
String -> (a -> SBool) -> (t -> b) -> IO b -> IO b
try ("Proving strengthening consecution: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm)
(\s :: 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 -> a -> InductionResult a
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 a) -> IO (InductionResult a)
strengthen [(String, st -> SBool)]
sts IO (InductionResult a)
cont)