{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.WeakestPreconditions.Length where
import Data.SBV
import Data.SBV.Control
import qualified Data.SBV.List as L
import Data.SBV.Tools.WeakestPreconditions
import GHC.Generics (Generic)
data LenS a = LenS { forall a. LenS a -> SList a
xs :: SList a
, forall a. LenS a -> SList a
ys :: SList a
, forall a. LenS a -> SInteger
l :: SInteger
}
deriving ((forall x. LenS a -> Rep (LenS a) x)
-> (forall x. Rep (LenS a) x -> LenS a) -> Generic (LenS a)
forall x. Rep (LenS a) x -> LenS a
forall x. LenS a -> Rep (LenS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LenS a) x -> LenS a
forall a x. LenS a -> Rep (LenS a) x
$cfrom :: forall a x. LenS a -> Rep (LenS a) x
from :: forall x. LenS a -> Rep (LenS a) x
$cto :: forall a x. Rep (LenS a) x -> LenS a
to :: forall x. Rep (LenS a) x -> LenS a
Generic, Bool -> SBool -> LenS a -> LenS a -> LenS a
(Bool -> SBool -> LenS a -> LenS a -> LenS a)
-> (forall b.
(Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a)
-> Mergeable (LenS a)
forall b.
(Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
forall a. SymVal a => Bool -> SBool -> LenS a -> LenS a -> LenS a
forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b. (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: forall a. SymVal a => Bool -> SBool -> LenS a -> LenS a -> LenS a
symbolicMerge :: Bool -> SBool -> LenS a -> LenS a -> LenS a
$cselect :: forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
select :: forall b.
(Ord b, SymVal b, Num b) =>
[LenS a] -> LenS a -> SBV b -> LenS a
Mergeable)
data LenC a = LenC [a] [a] Integer
instance (SymVal a, Show a) => Show (LenS a) where
show :: LenS a -> String
show (LenS SList a
xs SList a
ys SInteger
l) = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ys String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", l = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SInteger -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SInteger
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
where sh :: SBV a -> String
sh SBV a
v = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<symbolic>" a -> String
forall a. Show a => a -> String
show (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
v)
instance Show a => Show (LenC a) where
show :: LenC a -> String
show (LenC [a]
xs [a]
ys Integer
l) = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
ys String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", l = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
instance Queriable IO (LenS Integer) where
type QueryResult (LenS Integer) = LenC Integer
create :: QueryT IO S
create = SList Integer -> SList Integer -> SInteger -> S
forall a. SList a -> SList a -> SInteger -> LenS a
LenS (SList Integer -> SList Integer -> SInteger -> S)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SInteger -> S)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO (SList Integer)
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SList Integer -> SInteger -> S)
-> QueryT IO (SList Integer) -> QueryT IO (SInteger -> S)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO (SList Integer)
forall a. SymVal a => Query (SBV a)
freshVar_ QueryT IO (SInteger -> S) -> QueryT IO SInteger -> QueryT IO S
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO SInteger
forall a. SymVal a => Query (SBV a)
freshVar_
project :: S -> QueryT IO (QueryResult S)
project (LenS SList Integer
xs SList Integer
ys SInteger
l) = [Integer] -> [Integer] -> Integer -> LenC Integer
forall a. [a] -> [a] -> Integer -> LenC a
LenC ([Integer] -> [Integer] -> Integer -> LenC Integer)
-> QueryT IO [Integer]
-> QueryT IO ([Integer] -> Integer -> LenC Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SList Integer -> QueryT IO [Integer]
forall a. SymVal a => SBV a -> Query a
getValue SList Integer
xs QueryT IO ([Integer] -> Integer -> LenC Integer)
-> QueryT IO [Integer] -> QueryT IO (Integer -> LenC Integer)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SList Integer -> QueryT IO [Integer]
forall a. SymVal a => SBV a -> Query a
getValue SList Integer
ys QueryT IO (Integer -> LenC Integer)
-> QueryT IO Integer -> QueryT IO (LenC Integer)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SInteger -> QueryT IO Integer
forall a. SymVal a => SBV a -> Query a
getValue SInteger
l
embed :: QueryResult S -> QueryT IO S
embed (LenC [Integer]
xs [Integer]
ys Integer
l) = S -> QueryT IO S
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (S -> QueryT IO S) -> S -> QueryT IO S
forall a b. (a -> b) -> a -> b
$ SList Integer -> SList Integer -> SInteger -> S
forall a. SList a -> SList a -> SInteger -> LenS a
LenS ([Integer] -> SList Integer
forall a. SymVal a => a -> SBV a
literal [Integer]
xs) ([Integer] -> SList Integer
forall a. SymVal a => a -> SBV a
literal [Integer]
ys) (Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
l)
type S = LenS Integer
algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
algorithm :: Invariant S -> Maybe (Measure S) -> Stmt S
algorithm Invariant S
inv Maybe (Measure S)
msr = [Stmt S] -> Stmt S
forall st. [Stmt st] -> Stmt st
Seq [ (S -> S) -> Stmt S
forall st. (st -> st) -> Stmt st
Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SList Integer
xs :: forall a. LenS a -> SList a
xs :: SList Integer
xs} -> S
st{ys = xs, l = 0}
, String
-> Invariant S
-> Maybe (Measure S)
-> Invariant S
-> Stmt S
-> Stmt S
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While String
"! (null ys)"
Invariant S
inv
Maybe (Measure S)
msr
(\LenS{SList Integer
ys :: forall a. LenS a -> SList a
ys :: SList Integer
ys} -> SBool -> SBool
sNot (SList Integer -> SBool
forall a. SymVal a => SList a -> SBool
L.null SList Integer
ys))
(Stmt S -> Stmt S) -> Stmt S -> Stmt S
forall a b. (a -> b) -> a -> b
$ [Stmt S] -> Stmt S
forall st. [Stmt st] -> Stmt st
Seq [ (S -> S) -> Stmt S
forall st. (st -> st) -> Stmt st
Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SInteger
l :: forall a. LenS a -> SInteger
l :: SInteger
l} -> S
st{l = l + 1 }
, (S -> S) -> Stmt S
forall st. (st -> st) -> Stmt st
Assign ((S -> S) -> Stmt S) -> (S -> S) -> Stmt S
forall a b. (a -> b) -> a -> b
$ \st :: S
st@LenS{SList Integer
ys :: forall a. LenS a -> SList a
ys :: SList Integer
ys} -> S
st{ys = L.tail ys}
]
]
pre :: S -> SBool
pre :: Invariant S
pre S
_ = SBool
sTrue
post :: S -> SBool
post :: Invariant S
post LenS{SList Integer
xs :: forall a. LenS a -> SList a
xs :: SList Integer
xs, SInteger
l :: forall a. LenS a -> SInteger
l :: SInteger
l} = SInteger
l SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
xs
noChange :: Stable S
noChange :: Stable S
noChange = [String -> (S -> SList Integer) -> S -> S -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" S -> SList Integer
forall a. LenS a -> SList a
xs]
imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S
imperativeLength :: Invariant S -> Maybe (Measure S) -> Program S
imperativeLength Invariant S
inv Maybe (Measure S)
msr = Program { setup :: Symbolic ()
setup = () -> Symbolic ()
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, precondition :: Invariant S
precondition = Invariant S
pre
, program :: Stmt S
program = Invariant S -> Maybe (Measure S) -> Stmt S
algorithm Invariant S
inv Maybe (Measure S)
msr
, postcondition :: Invariant S
postcondition = Invariant S
post
, stability :: Stable S
stability = Stable S
noChange
}
invariant :: Invariant S
invariant :: Invariant S
invariant LenS{SList Integer
xs :: forall a. LenS a -> SList a
xs :: SList Integer
xs, SList Integer
ys :: forall a. LenS a -> SList a
ys :: SList Integer
ys, SInteger
l :: forall a. LenS a -> SInteger
l :: SInteger
l} = SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
xs SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
ys
measure :: Measure S
measure :: Measure S
measure LenS{SList Integer
ys :: forall a. LenS a -> SList a
ys :: SList Integer
ys} = [SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
ys]
correctness :: IO ()
correctness :: IO ()
correctness = ProofResult (LenC Integer) -> IO ()
forall a. Show a => a -> IO ()
print (ProofResult (LenC Integer) -> IO ())
-> IO (ProofResult (LenC Integer)) -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< WPConfig -> Program S -> IO (ProofResult (LenC Integer))
forall st res.
(Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose=True} (Invariant S -> Maybe (Measure S) -> Program S
imperativeLength Invariant S
invariant (Measure S -> Maybe (Measure S)
forall a. a -> Maybe a
Just Measure S
measure))