    -----------------------------------------------------------------------------
    -- |
    -- 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       #-}
    {-# LANGUAGE TypeFamilies          #-}

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

    -- | 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 = " 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)

    -- | 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 = " 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
    "}"

    -- | 'Queriable' instance for the program state
    instance Queriable IO (AppS Integer) where
      type QueryResult (AppS Integer) = AppC Integer
      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 (QueryResult A)
    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 :: QueryResult A -> 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)

    -- | 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 = [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            }
                                     ]

    -- | A program is the algorithm, together with its pre- and post-conditions.
    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  -- no precondition
                               , program :: Stmt A
    program       = Stmt A
    algorithm
                               , postcondition :: Invariant A
    postcondition = Invariant A
    postcondition
                               , stability :: Stable A
    stability     = Stable A
    noChange
                               }
      where -- We must append properly!
            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

            -- Program should never change values of @xs@ and @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

    -- | 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 = WPConfig -> Program A -> IO (ProofResult (AppC 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} Program A
    imperativeAppend