-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.WeakestPreconditions.Append
-- Copyright : Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proof of correctness of an imperative list-append algorithm, using weakest
-- preconditions. Illustrates the use of SBV's symbolic lists together with
-- the WP algorithm.
-----------------------------------------------------------------------------

{-# 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)

-- * Program state

-- | The state of the length program, paramaterized over the element type @a@
data AppS a = AppS { forall a. AppS a -> SList a
xs :: SList a  -- ^ The first input list
                   , forall a. AppS a -> SList a
ys :: SList a  -- ^ The second input list
                   , forall a. AppS a -> SList a
ts :: SList a  -- ^ Temporary variable
                   , forall a. AppS a -> SList a
zs :: SList a  -- ^ Output
                   }
                   deriving (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
$cto :: forall a x. Rep (AppS a) x -> AppS a
$cfrom :: forall a x. AppS a -> Rep (AppS a) x
Generic, 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
select :: forall b.
(Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a
$cselect :: forall a b.
(SymVal a, Ord b, SymVal b, Num b) =>
[AppS a] -> AppS a -> SBV b -> AppS a
symbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a
$csymbolicMerge :: forall a. SymVal a => Bool -> SBool -> AppS a -> AppS a -> AppS a
Mergeable)

-- | The concrete counterpart of 'AppS'. Again, we can't simply use the duality between
-- @SBV a@ and @a@ due to the difference between @SList a@ and @[a]@.
data AppC a = AppC [a] [a] [a] [a]

-- | Show instance for 'AppS'. The above deriving clause would work just as well,
-- but we want it to be a little prettier here, and hence the @OVERLAPS@ directive.
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 = " forall a. [a] -> [a] -> [a]
P.++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
xs forall a. [a] -> [a] -> [a]
P.++ String
", ys = " forall a. [a] -> [a] -> [a]
P.++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ys forall a. [a] -> [a] -> [a]
P.++ String
", ts = " forall a. [a] -> [a] -> [a]
P.++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
ts forall a. [a] -> [a] -> [a]
P.++ String
", zs = " forall a. [a] -> [a] -> [a]
P.++ forall {a}. (Show a, SymVal a) => SBV a -> String
sh SList a
zs forall a. [a] -> [a] -> [a]
P.++ String
"}"
    where sh :: SBV a -> String
sh SBV a
v = forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"<symbolic>" forall a. Show a => a -> String
show (forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
v)

-- | Show instance, a bit more prettier than what would be derived:
instance Show a => Show (AppC a) where
  show :: AppC a -> String
show (AppC [a]
xs [a]
ys [a]
ts [a]
zs) = String
"{xs = " forall a. [a] -> [a] -> [a]
P.++ forall a. Show a => a -> String
show [a]
xs forall a. [a] -> [a] -> [a]
P.++ String
", ys = " forall a. [a] -> [a] -> [a]
P.++ forall a. Show a => a -> String
show [a]
ys forall a. [a] -> [a] -> [a]
P.++ String
", ts = " forall a. [a] -> [a] -> [a]
P.++ forall a. Show a => a -> String
show [a]
ts forall a. [a] -> [a] -> [a]
P.++ String
", zs = " forall a. [a] -> [a] -> [a]
P.++ forall a. Show a => a -> String
show [a]
zs forall a. [a] -> [a] -> [a]
P.++ String
"}"

-- | 'Queriable' instance for the program state
instance Queriable IO (AppS Integer) (AppC Integer) where
  create :: QueryT IO A
create                     = forall a. SList a -> SList a -> SList a -> SList a -> AppS a
AppS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => Query (SBV a)
freshVar_   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Query (SBV a)
freshVar_   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => Query (SBV a)
freshVar_   forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = forall a. [a] -> [a] -> [a] -> [a] -> AppC a
AppC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SBV a -> Query a
getValue SList Integer
xs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Query a
getValue SList Integer
ys forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Query a
getValue SList Integer
ts forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SList a -> SList a -> SList a -> SList a -> AppS a
AppS (forall a. SymVal a => a -> SBV a
literal [Integer]
xs) (forall a. SymVal a => a -> SBV a
literal [Integer]
ys) (forall a. SymVal a => a -> SBV a
literal [Integer]
ts) (forall a. SymVal a => a -> SBV a
literal [Integer]
zs)

-- | Helper type synonym
type A = AppS Integer

-- * The algorithm

-- | The imperative append algorithm:
--
-- @
--    zs = []
--    ts = xs
--    while not (null ts)
--      zs = zs ++ [head ts]
--      ts = tail ts
--    ts = ys
--    while not (null ts)
--      zs = zs ++ [head ts]
--      ts = tail ts
-- @
algorithm :: Stmt A
algorithm :: Stmt A
algorithm = forall st. [Stmt st] -> Stmt st
Seq [ forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \A
st          -> A
st{zs :: SList Integer
zs = []}
                , forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
xs :: SList Integer
xs :: forall a. AppS a -> SList a
xs} -> A
st{ts :: SList Integer
ts = SList Integer
xs}
                , forall {a}.
SymVal a =>
String -> Invariant (AppS a) -> Stmt (AppS a)
loop String
"xs" (\AppS{SList Integer
xs :: SList Integer
xs :: forall a. AppS a -> SList a
xs, SList Integer
zs :: SList Integer
zs :: forall a. AppS a -> SList a
zs, SList Integer
ts :: SList Integer
ts :: forall a. AppS a -> SList a
ts} -> SList Integer
xs forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ts)
                , forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
ys :: SList Integer
ys :: forall a. AppS a -> SList a
ys} -> A
st{ts :: SList Integer
ts = SList Integer
ys}
                , forall {a}.
SymVal a =>
String -> Invariant (AppS a) -> Stmt (AppS a)
loop String
"ys" (\AppS{SList Integer
xs :: SList Integer
xs :: forall a. AppS a -> SList a
xs, SList Integer
ys :: SList Integer
ys :: forall a. AppS a -> SList a
ys, SList Integer
zs :: SList Integer
zs :: forall a. AppS a -> SList a
zs, SList Integer
ts :: SList Integer
ts :: forall a. AppS a -> SList a
ts} -> SList Integer
xs forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs 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 = forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While (String
"walk over " forall a. [a] -> [a] -> [a]
P.++ String
w)
                           Invariant (AppS a)
inv
                           (forall a. a -> Maybe a
Just (\AppS{SList a
ts :: SList a
ts :: forall a. AppS a -> SList a
ts} -> [forall a. SymVal a => SList a -> SInteger
L.length SList a
ts]))
                           (\AppS{SList a
ts :: SList a
ts :: forall a. AppS a -> SList a
ts} -> SBool -> SBool
sNot (forall a. SymVal a => SList a -> SBool
L.null SList a
ts))
                           forall a b. (a -> b) -> a -> b
$ forall st. [Stmt st] -> Stmt st
Seq [ forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: AppS a
st@AppS{SList a
ts :: SList a
ts :: forall a. AppS a -> SList a
ts, SList a
zs :: SList a
zs :: forall a. AppS a -> SList a
zs} -> AppS a
st{zs :: SList a
zs = SList a
zs forall a. SymVal a => SList a -> SBV a -> SList a
`L.snoc` forall a. SymVal a => SList a -> SBV a
L.head SList a
ts}
                                 , forall st. (st -> st) -> Stmt st
Assign forall a b. (a -> b) -> a -> b
$ \st :: AppS a
st@AppS{SList a
ts :: SList a
ts :: forall a. AppS a -> SList a
ts}     -> AppS a
st{ts :: SList a
ts = forall a. SymVal a => SList a -> SList a
L.tail SList a
ts            }
                                 ]

-- | A program is the algorithm, together with its pre- and post-conditions.
imperativeAppend :: Program A
imperativeAppend :: Program A
imperativeAppend = Program { setup :: Symbolic ()
setup         = forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           , precondition :: A -> SBool
precondition  = forall a b. a -> b -> a
const SBool
sTrue  -- no precondition
                           , program :: Stmt A
program       = Stmt A
algorithm
                           , postcondition :: A -> SBool
postcondition = A -> SBool
postcondition
                           , stability :: Stable A
stability     = Stable A
noChange
                           }
  where -- We must append properly!
        postcondition :: A -> SBool
        postcondition :: A -> SBool
postcondition AppS{SList Integer
xs :: SList Integer
xs :: forall a. AppS a -> SList a
xs, SList Integer
ys :: SList Integer
ys :: forall a. AppS a -> SList a
ys, SList Integer
zs :: SList Integer
zs :: forall a. AppS a -> SList a
zs} = SList Integer
zs forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
xs forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys

        -- Program should never change values of @xs@ and @ys@
        noChange :: Stable A
noChange = [forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" forall a. AppS a -> SList a
xs, forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"ys" forall a. AppS a -> SList a
ys]

-- * Correctness

-- | We check that @zs@ is @xs ++ ys@ upon termination.
--
-- >>> correctness
-- Total correctness is established.
-- Q.E.D.
correctness :: IO (ProofResult (AppC Integer))
correctness :: IO (ProofResult (AppC Integer))
correctness = forall st res.
(Show res, Mergeable st, Queriable IO st res) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose :: Bool
wpVerbose=Bool
True} Program A
imperativeAppend