{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.WeakestPreconditions.Append where
import Data.SBV
import Data.SBV.Control
import Prelude hiding ((++))
import qualified Prelude as P
import Data.SBV.List ((++))
import qualified Data.SBV.List as L
import Data.SBV.Tools.WeakestPreconditions
import GHC.Generics (Generic)
data AppS a = AppS { forall a. AppS a -> SList a
xs :: SList a
, forall a. AppS a -> SList a
ys :: SList a
, forall a. AppS a -> SList a
ts :: SList a
, forall a. AppS a -> SList a
zs :: SList a
}
deriving ((forall x. AppS a -> Rep (AppS a) x)
-> (forall x. Rep (AppS a) x -> AppS a) -> Generic (AppS a)
forall x. Rep (AppS a) x -> AppS a
forall x. AppS a -> Rep (AppS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (AppS a) x -> AppS a
forall a x. AppS a -> Rep (AppS a) x
$cfrom :: forall a x. AppS a -> Rep (AppS a) x
from :: forall x. AppS a -> Rep (AppS a) x
$cto :: forall a x. Rep (AppS a) x -> AppS a
to :: forall x. Rep (AppS a) x -> AppS a
Generic, Bool -> SBool -> AppS a -> AppS a -> AppS a
(Bool -> SBool -> AppS a -> AppS a -> AppS a)
-> (forall b.
(Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a)
-> Mergeable (AppS a)
forall b.
(Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a
forall a. SymVal a => Bool -> SBool -> AppS a -> AppS a -> AppS a
forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS 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 -> AppS a -> AppS a -> AppS a
symbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a
$cselect :: forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a
select :: forall b.
(Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a
Mergeable)
data AppC a = AppC [a] [a] [a] [a]
instance {-# OVERLAPS #-} (SymVal a, Show a) => Show (AppS a) where
show :: AppS a -> String
show (AppS SList a
xs SList a
ys SList a
ts SList a
zs) = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
xs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ys String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ts = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ts String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", zs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ SList a -> String
forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
zs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ 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 (AppC a) where
show :: AppC a -> String
show (AppC [a]
xs [a]
ys [a]
ts [a]
zs) = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ [a] -> String
forall a. Show a => a -> String
show [a]
xs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ [a] -> String
forall a. Show a => a -> String
show [a]
ys String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ts = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ [a] -> String
forall a. Show a => a -> String
show [a]
ts String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", zs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ [a] -> String
forall a. Show a => a -> String
show [a]
zs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
"}"
instance Queriable IO (AppS Integer) (AppC Integer) where
create :: QueryT IO A
create = SList Integer
-> SList Integer -> SList Integer -> SList Integer -> A
forall a. SList a -> SList a -> SList a -> SList a -> AppS a
AppS (SList Integer
-> SList Integer -> SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SList Integer -> SList Integer -> A)
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 -> SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SList Integer -> A)
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 (SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer) -> QueryT IO (SList Integer -> A)
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 (SList Integer -> A)
-> QueryT IO (SList Integer) -> QueryT IO A
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_
project :: A -> QueryT IO (AppC Integer)
project (AppS SList Integer
xs SList Integer
ys SList Integer
ts SList Integer
zs) = [Integer] -> [Integer] -> [Integer] -> [Integer] -> AppC Integer
forall a. [a] -> [a] -> [a] -> [a] -> AppC a
AppC ([Integer] -> [Integer] -> [Integer] -> [Integer] -> AppC Integer)
-> QueryT IO [Integer]
-> QueryT IO ([Integer] -> [Integer] -> [Integer] -> AppC 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] -> [Integer] -> AppC Integer)
-> QueryT IO [Integer]
-> QueryT IO ([Integer] -> [Integer] -> AppC 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] -> [Integer] -> AppC Integer)
-> QueryT IO [Integer] -> QueryT IO ([Integer] -> AppC 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
ts QueryT IO ([Integer] -> AppC Integer)
-> QueryT IO [Integer] -> QueryT IO (AppC 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
zs
embed :: AppC Integer -> QueryT IO A
embed (AppC [Integer]
xs [Integer]
ys [Integer]
ts [Integer]
zs) = A -> QueryT IO A
forall a. a -> QueryT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (A -> QueryT IO A) -> A -> QueryT IO A
forall a b. (a -> b) -> a -> b
$ SList Integer
-> SList Integer -> SList Integer -> SList Integer -> A
forall a. SList a -> SList a -> SList a -> SList a -> AppS a
AppS ([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] -> SList Integer
forall a. SymVal a => a -> SBV a
literal [Integer]
ts) ([Integer] -> SList Integer
forall a. SymVal a => a -> SBV a
literal [Integer]
zs)
type A = AppS Integer
algorithm :: Stmt A
algorithm :: Stmt A
algorithm = [Stmt A] -> Stmt A
forall st. [Stmt st] -> Stmt st
Seq [ (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \A
st -> A
st{zs = []}
, (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
xs :: forall a. AppS a -> SList a
xs :: SList Integer
xs} -> A
st{ts = xs}
, String -> Invariant A -> Stmt A
forall {a}.
SymVal a =>
String -> Invariant (AppS a) -> Stmt (AppS a)
loop String
"xs" (\AppS{SList Integer
xs :: forall a. AppS a -> SList a
xs :: SList Integer
xs, SList Integer
zs :: forall a. AppS a -> SList a
zs :: SList Integer
zs, SList Integer
ts :: forall a. AppS a -> SList a
ts :: SList Integer
ts} -> SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ts)
, (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
ys :: forall a. AppS a -> SList a
ys :: SList Integer
ys} -> A
st{ts = ys}
, String -> Invariant A -> Stmt A
forall {a}.
SymVal a =>
String -> Invariant (AppS a) -> Stmt (AppS a)
loop String
"ys" (\AppS{SList Integer
xs :: forall a. AppS a -> SList a
xs :: SList Integer
xs, SList Integer
ys :: forall a. AppS a -> SList a
ys :: SList Integer
ys, SList Integer
zs :: forall a. AppS a -> SList a
zs :: SList Integer
zs, SList Integer
ts :: forall a. AppS a -> SList a
ts :: SList Integer
ts} -> SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ts)
]
where loop :: String -> Invariant (AppS a) -> Stmt (AppS a)
loop String
w Invariant (AppS a)
inv = String
-> Invariant (AppS a)
-> Maybe (Measure (AppS a))
-> Invariant (AppS a)
-> Stmt (AppS a)
-> Stmt (AppS a)
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While (String
"walk over " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
w)
Invariant (AppS a)
inv
(Measure (AppS a) -> Maybe (Measure (AppS a))
forall a. a -> Maybe a
Just (\AppS{SList a
ts :: forall a. AppS a -> SList a
ts :: SList a
ts} -> [SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList a
ts]))
(\AppS{SList a
ts :: forall a. AppS a -> SList a
ts :: SList a
ts} -> SBool -> SBool
sNot (SList a -> SBool
forall a. SymVal a => SList a -> SBool
L.null SList a
ts))
(Stmt (AppS a) -> Stmt (AppS a)) -> Stmt (AppS a) -> Stmt (AppS a)
forall a b. (a -> b) -> a -> b
$ [Stmt (AppS a)] -> Stmt (AppS a)
forall st. [Stmt st] -> Stmt st
Seq [ (AppS a -> AppS a) -> Stmt (AppS a)
forall st. (st -> st) -> Stmt st
Assign ((AppS a -> AppS a) -> Stmt (AppS a))
-> (AppS a -> AppS a) -> Stmt (AppS a)
forall a b. (a -> b) -> a -> b
$ \st :: AppS a
st@AppS{SList a
ts :: forall a. AppS a -> SList a
ts :: SList a
ts, SList a
zs :: forall a. AppS a -> SList a
zs :: SList a
zs} -> AppS a
st{zs = zs `L.snoc` L.head ts}
, (AppS a -> AppS a) -> Stmt (AppS a)
forall st. (st -> st) -> Stmt st
Assign ((AppS a -> AppS a) -> Stmt (AppS a))
-> (AppS a -> AppS a) -> Stmt (AppS a)
forall a b. (a -> b) -> a -> b
$ \st :: AppS a
st@AppS{SList a
ts :: forall a. AppS a -> SList a
ts :: SList a
ts} -> AppS a
st{ts = L.tail ts }
]
imperativeAppend :: Program A
imperativeAppend :: Program A
imperativeAppend = Program { setup :: Symbolic ()
setup = () -> Symbolic ()
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, precondition :: Invariant A
precondition = SBool -> Invariant A
forall a b. a -> b -> a
const SBool
sTrue
, program :: Stmt A
program = Stmt A
algorithm
, postcondition :: Invariant A
postcondition = Invariant A
postcondition
, stability :: Stable A
stability = Stable A
noChange
}
where
postcondition :: A -> SBool
postcondition :: Invariant A
postcondition AppS{SList Integer
xs :: forall a. AppS a -> SList a
xs :: SList Integer
xs, SList Integer
ys :: forall a. AppS a -> SList a
ys :: SList Integer
ys, SList Integer
zs :: forall a. AppS a -> SList a
zs :: SList Integer
zs} = SList Integer
zs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys
noChange :: Stable A
noChange = [String -> (A -> SList Integer) -> A -> A -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" A -> SList Integer
forall a. AppS a -> SList a
xs, String -> (A -> SList Integer) -> A -> A -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"ys" A -> SList Integer
forall a. AppS a -> SList a
ys]
correctness :: IO (ProofResult (AppC Integer))
correctness :: IO (ProofResult (AppC Integer))
correctness = WPConfig -> Program A -> IO (ProofResult (AppC Integer))
forall st res.
(Show res, Mergeable st, Queriable IO st res) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose=True} Program A
imperativeAppend