{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor      #-}
{-# LANGUAGE DeriveTraversable  #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE TypeFamilies       #-}

module Language.While.Hoare where

import Control.Monad.Writer

import           Language.While.Syntax

import           Language.Expression.Prop
import           Language.Expression.Pretty
import           Language.Verification
import           Language.Verification.Conditions

type WhileProp l = Prop (WhileExpr l)

data PropAnn l a = PropAnn (WhileProp l Bool) a

type AnnCommand l a = Command l (PropAnn l a)

instance (Pretty l, Pretty a) => Pretty (PropAnn l a) where
  prettysPrec :: Int -> PropAnn l a -> ShowS
prettysPrec Int
_ (PropAnn WhileProp l Bool
prop a
ann) = Int -> WhileProp l Bool -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 WhileProp l Bool
prop ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" , " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 a
ann

type MonadGen l = WriterT [WhileProp l Bool] Maybe

--------------------------------------------------------------------------------
--  Exposed Functions
--------------------------------------------------------------------------------

-- | Generate verification conditions to prove that the given Hoare partial
-- correctness triple holds.
generateVCs
  :: (VerifiableVar (WhileVar l))
  => WhileProp l Bool -> WhileProp l Bool -> AnnCommand l a
  -> Maybe [WhileProp l Bool]
generateVCs :: WhileProp l Bool
-> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
generateVCs WhileProp l Bool
precond WhileProp l Bool
postcond AnnCommand l a
cmd =
  WriterT [WhileProp l Bool] Maybe () -> Maybe [WhileProp l Bool]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT [WhileProp l Bool] Maybe () -> Maybe [WhileProp l Bool])
-> WriterT [WhileProp l Bool] Maybe () -> Maybe [WhileProp l Bool]
forall a b. (a -> b) -> a -> b
$ Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> WriterT [WhileProp l Bool] Maybe ()
forall l a.
VerifiableVar (WhileVar l) =>
Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs' (WhileProp l Bool
precond, WhileProp l Bool
postcond, AnnCommand l a
cmd)


generateVCs'
  :: (VerifiableVar (WhileVar l))
  => Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a) -> MonadGen l ()
generateVCs' :: Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs' (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, AnnCommand l a
cmd) = case AnnCommand l a
cmd of
  CAnn (PropAnn Prop (HFree WhileOp (WhileVar l)) Bool
prop a
_) AnnCommand l a
command ->
    Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
forall l a.
VerifiableVar (WhileVar l) =>
Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs' ((Prop (HFree WhileOp (WhileVar l)) Bool
prop Prop (HFree WhileOp (WhileVar l)) Bool
-> Prop (HFree WhileOp (WhileVar l)) Bool
-> Prop (HFree WhileOp (WhileVar l)) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (HFree WhileOp (WhileVar l)) Bool
precond), Prop (HFree WhileOp (WhileVar l)) Bool
postcond, AnnCommand l a
command)

  c :: AnnCommand l a
c@(CSeq AnnCommand l a
_ AnnCommand l a
_) -> do
    AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
s <- Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
-> WriterT
     [Prop (HFree WhileOp (WhileVar l)) Bool]
     Maybe
     (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c)
    WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe [()]
-> MonadGen l ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe [()]
 -> MonadGen l ())
-> WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe [()]
-> MonadGen l ()
forall a b. (a -> b) -> a -> b
$ (Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> MonadGen l ())
-> Triplet
     (HFree WhileOp)
     (WhileVar l)
     (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
-> WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe [()]
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
       a.
(HMonad expr, MonadGenVCs expr v m, VerifiableVar v) =>
(Triplet expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
sequenceVCs Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
forall l a.
VerifiableVar (WhileVar l) =>
Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs' (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
s)

  AnnCommand l a
CSkip -> Triplet (HFree WhileOp) (WhileVar l) () -> MonadGen l ()
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (m :: * -> *).
(HMonad expr, MonadGenVCs expr var m) =>
Triplet expr var () -> m ()
skipVCs (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, ())

  CAssign l
loc WhileExpr l AlgReal
e ->
    Triplet
  (HFree WhileOp)
  (WhileVar l)
  (Assignment (HFree WhileOp) (WhileVar l))
-> MonadGen l ()
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *).
(HMonad expr, MonadGenVCs expr v m, VerifiableVar v) =>
Triplet expr v (Assignment expr v) -> m ()
assignVCs (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, (WhileVar l AlgReal
-> WhileExpr l AlgReal -> Assignment (HFree WhileOp) (WhileVar l)
forall k (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment (l -> WhileVar l AlgReal
forall l. l -> WhileVar l AlgReal
WhileVar l
loc) WhileExpr l AlgReal
e))

  CIf WhileExpr l Bool
cond AnnCommand l a
c1 AnnCommand l a
c2 ->
    WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe ((), ())
-> MonadGen l ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe ((), ())
 -> MonadGen l ())
-> WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe ((), ())
-> MonadGen l ()
forall a b. (a -> b) -> a -> b
$ (Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> MonadGen l ())
-> (WhileExpr l Bool -> Prop (HFree WhileOp (WhileVar l)) Bool)
-> Triplet
     (HFree WhileOp)
     (WhileVar l)
     (WhileExpr l Bool, AnnCommand l a, AnnCommand l a)
-> WriterT [Prop (HFree WhileOp (WhileVar l)) Bool] Maybe ((), ())
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
       a cond.
(HMonad expr, MonadGenVCs expr v m) =>
(Triplet expr v cmd -> m a)
-> (cond -> Prop (expr v) Bool)
-> Triplet expr v (cond, cmd, cmd)
-> m (a, a)
ifVCs Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
forall l a.
VerifiableVar (WhileVar l) =>
Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs' WhileExpr l Bool -> Prop (HFree WhileOp (WhileVar l)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, (WhileExpr l Bool
cond, AnnCommand l a
c1, AnnCommand l a
c2))

  CWhile WhileExpr l Bool
cond (CAnn (PropAnn Prop (HFree WhileOp (WhileVar l)) Bool
invariant a
_) AnnCommand l a
body) ->
    (Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> MonadGen l ())
-> (WhileExpr l Bool -> Prop (HFree WhileOp (WhileVar l)) Bool)
-> Prop (HFree WhileOp (WhileVar l)) Bool
-> Triplet
     (HFree WhileOp) (WhileVar l) (WhileExpr l Bool, AnnCommand l a)
-> MonadGen l ()
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) (m :: * -> *) cmd
       cond.
(HMonad expr, MonadGenVCs expr v m) =>
(Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Prop (expr v) Bool
-> Triplet expr v (cond, cmd)
-> m ()
whileVCs Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
forall l a.
VerifiableVar (WhileVar l) =>
Triplet (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> MonadGen l ()
generateVCs'
      WhileExpr l Bool -> Prop (HFree WhileOp (WhileVar l)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr
      Prop (HFree WhileOp (WhileVar l)) Bool
invariant
      (Prop (HFree WhileOp (WhileVar l)) Bool
precond, Prop (HFree WhileOp (WhileVar l)) Bool
postcond, (WhileExpr l Bool
cond, AnnCommand l a
body))

  -- If this falls through, the command is not sufficiently annotated
  AnnCommand l a
_ -> MonadGen l ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero

--------------------------------------------------------------------------------
--  Internal
--------------------------------------------------------------------------------

-- | Split the command into all the top-level sequenced commands, interspersed
-- with annotations. Returns 'Nothing' if the command's sequences are not
-- sufficiently annotated.
splitSeq :: AnnCommand l a -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq :: AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq = \case
  CSeq AnnCommand l a
c1 (CAnn (PropAnn WhileProp l Bool
midcond a
_) AnnCommand l a
c2) ->
    do AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 <- AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c1
       AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a2 <- AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c2
       AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)))
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall a b. (a -> b) -> a -> b
$ AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> WhileProp l Bool
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
Annotation AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 WhileProp l Bool
midcond AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a2
  CSeq AnnCommand l a
c1 (CAssign l
loc WhileExpr l AlgReal
e) ->
    do AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 <- AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c1
       AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` [Assignment (HFree WhileOp) (WhileVar l)]
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign [WhileVar l AlgReal
-> WhileExpr l AlgReal -> Assignment (HFree WhileOp) (WhileVar l)
forall k (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment (l -> WhileVar l AlgReal
forall l. l -> WhileVar l AlgReal
WhileVar l
loc) WhileExpr l AlgReal
e]
  CSeq AnnCommand l a
c1 AnnCommand l a
c2 ->
    do AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 <- AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c1
       AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a2 <- AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall l a.
AnnCommand l a
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
splitSeq AnnCommand l a
c2
       AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a1 AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
a2
  CAssign l
loc WhileExpr l AlgReal
e -> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)))
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall a b. (a -> b) -> a -> b
$ [Assignment (HFree WhileOp) (WhileVar l)]
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign [WhileVar l AlgReal
-> WhileExpr l AlgReal -> Assignment (HFree WhileOp) (WhileVar l)
forall k (var :: k -> *) (a :: k) (expr :: (k -> *) -> k -> *).
var a -> expr var a -> Assignment expr var
Assignment (l -> WhileVar l AlgReal
forall l. l -> WhileVar l AlgReal
WhileVar l
loc) WhileExpr l AlgReal
e]
  AnnCommand l a
c -> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
 -> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)))
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
-> Maybe (AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a))
forall a b. (a -> b) -> a -> b
$ AnnCommand l a
-> [Assignment (HFree WhileOp) (WhileVar l)]
-> AnnSeq (HFree WhileOp) (WhileVar l) (AnnCommand l a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
cmd -> [Assignment expr var] -> AnnSeq expr var cmd
CmdAssign AnnCommand l a
c []