{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}

{- |

Combinators for generating verification conditions for programs.

-}
module Language.Verification.Conditions
  (
  -- * Types
    Assignment(..)
  , AnnSeq(..)
  , Triplet

  -- * Generating Verification Conditions
  , skipVCs
  , assignVCs
  , sequenceVCs
  , ifVCs
  , multiIfVCs
  , whileVCs

  -- * Combinators
  , subAssignment
  , chainSub
  , joinAnnSeq
  , JoinAnnSeq(..)
  , joiningAnnSeq
  , emptyAnnSeq
  , propAnnSeq
  , cmdAnnSeq

  -- * Propositions
  , module Language.Expression.Prop
  ) where

import           Data.List                  (intersperse)
import           Data.Semigroup             (Semigroup(..))
import           Data.Monoid                (Endo (..))

import           Control.Monad.Writer       (MonadWriter (tell))

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

--------------------------------------------------------------------------------
--  Exposed Types
--------------------------------------------------------------------------------

-- | An assignment of a particular expression to a particular variable.
data Assignment expr var where
  Assignment :: var a -> expr var a -> Assignment expr var

instance (Pretty1 var, Pretty2 expr) => Pretty (Assignment expr var) where
  prettysPrec :: Int -> Assignment expr var -> ShowS
prettysPrec Int
p (Assignment var a
v expr var a
e) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> var a -> ShowS
forall k (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
10 var a
v 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 -> expr var a -> ShowS
forall k k (op :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
(Pretty2 op, Pretty1 t) =>
Int -> op t a -> ShowS
prettys2Prec Int
10 expr var a
e

-- | An annotated sequence. Consists of runs of assignments, with other commands
-- separated by annotations.
data AnnSeq expr var cmd
  = JustAssign [Assignment expr var]
  -- ^ Just a series of assignments without annotations
  | CmdAssign cmd [Assignment expr var]
  -- ^ A command followed by a series of assignments
  | Annotation (AnnSeq expr var cmd) (Prop (expr var) Bool) (AnnSeq expr var cmd)
  -- ^ An initial sequence, followed by an annotation, then another sequence
  deriving (a -> AnnSeq expr var b -> AnnSeq expr var a
(a -> b) -> AnnSeq expr var a -> AnnSeq expr var b
(forall a b. (a -> b) -> AnnSeq expr var a -> AnnSeq expr var b)
-> (forall a b. a -> AnnSeq expr var b -> AnnSeq expr var a)
-> Functor (AnnSeq expr var)
forall a b. a -> AnnSeq expr var b -> AnnSeq expr var a
forall a b. (a -> b) -> AnnSeq expr var a -> AnnSeq expr var b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
a -> AnnSeq expr var b -> AnnSeq expr var a
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
(a -> b) -> AnnSeq expr var a -> AnnSeq expr var b
<$ :: a -> AnnSeq expr var b -> AnnSeq expr var a
$c<$ :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
a -> AnnSeq expr var b -> AnnSeq expr var a
fmap :: (a -> b) -> AnnSeq expr var a -> AnnSeq expr var b
$cfmap :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
(a -> b) -> AnnSeq expr var a -> AnnSeq expr var b
Functor, AnnSeq expr var a -> Bool
(a -> m) -> AnnSeq expr var a -> m
(a -> b -> b) -> b -> AnnSeq expr var a -> b
(forall m. Monoid m => AnnSeq expr var m -> m)
-> (forall m a. Monoid m => (a -> m) -> AnnSeq expr var a -> m)
-> (forall m a. Monoid m => (a -> m) -> AnnSeq expr var a -> m)
-> (forall a b. (a -> b -> b) -> b -> AnnSeq expr var a -> b)
-> (forall a b. (a -> b -> b) -> b -> AnnSeq expr var a -> b)
-> (forall b a. (b -> a -> b) -> b -> AnnSeq expr var a -> b)
-> (forall b a. (b -> a -> b) -> b -> AnnSeq expr var a -> b)
-> (forall a. (a -> a -> a) -> AnnSeq expr var a -> a)
-> (forall a. (a -> a -> a) -> AnnSeq expr var a -> a)
-> (forall a. AnnSeq expr var a -> [a])
-> (forall a. AnnSeq expr var a -> Bool)
-> (forall a. AnnSeq expr var a -> Int)
-> (forall a. Eq a => a -> AnnSeq expr var a -> Bool)
-> (forall a. Ord a => AnnSeq expr var a -> a)
-> (forall a. Ord a => AnnSeq expr var a -> a)
-> (forall a. Num a => AnnSeq expr var a -> a)
-> (forall a. Num a => AnnSeq expr var a -> a)
-> Foldable (AnnSeq expr var)
forall a. Eq a => a -> AnnSeq expr var a -> Bool
forall a. Num a => AnnSeq expr var a -> a
forall a. Ord a => AnnSeq expr var a -> a
forall m. Monoid m => AnnSeq expr var m -> m
forall a. AnnSeq expr var a -> Bool
forall a. AnnSeq expr var a -> Int
forall a. AnnSeq expr var a -> [a]
forall a. (a -> a -> a) -> AnnSeq expr var a -> a
forall m a. Monoid m => (a -> m) -> AnnSeq expr var a -> m
forall b a. (b -> a -> b) -> b -> AnnSeq expr var a -> b
forall a b. (a -> b -> b) -> b -> AnnSeq expr var a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Eq a =>
a -> AnnSeq expr var a -> Bool
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Num a =>
AnnSeq expr var a -> a
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Ord a =>
AnnSeq expr var a -> a
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) m.
Monoid m =>
AnnSeq expr var m -> m
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> Bool
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> Int
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> [a]
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
(a -> a -> a) -> AnnSeq expr var a -> a
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) m a.
Monoid m =>
(a -> m) -> AnnSeq expr var a -> m
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) b a.
(b -> a -> b) -> b -> AnnSeq expr var a -> b
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
(a -> b -> b) -> b -> AnnSeq expr var a -> b
product :: AnnSeq expr var a -> a
$cproduct :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Num a =>
AnnSeq expr var a -> a
sum :: AnnSeq expr var a -> a
$csum :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Num a =>
AnnSeq expr var a -> a
minimum :: AnnSeq expr var a -> a
$cminimum :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Ord a =>
AnnSeq expr var a -> a
maximum :: AnnSeq expr var a -> a
$cmaximum :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Ord a =>
AnnSeq expr var a -> a
elem :: a -> AnnSeq expr var a -> Bool
$celem :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
Eq a =>
a -> AnnSeq expr var a -> Bool
length :: AnnSeq expr var a -> Int
$clength :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> Int
null :: AnnSeq expr var a -> Bool
$cnull :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> Bool
toList :: AnnSeq expr var a -> [a]
$ctoList :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
AnnSeq expr var a -> [a]
foldl1 :: (a -> a -> a) -> AnnSeq expr var a -> a
$cfoldl1 :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
(a -> a -> a) -> AnnSeq expr var a -> a
foldr1 :: (a -> a -> a) -> AnnSeq expr var a -> a
$cfoldr1 :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a.
(a -> a -> a) -> AnnSeq expr var a -> a
foldl' :: (b -> a -> b) -> b -> AnnSeq expr var a -> b
$cfoldl' :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) b a.
(b -> a -> b) -> b -> AnnSeq expr var a -> b
foldl :: (b -> a -> b) -> b -> AnnSeq expr var a -> b
$cfoldl :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) b a.
(b -> a -> b) -> b -> AnnSeq expr var a -> b
foldr' :: (a -> b -> b) -> b -> AnnSeq expr var a -> b
$cfoldr' :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
(a -> b -> b) -> b -> AnnSeq expr var a -> b
foldr :: (a -> b -> b) -> b -> AnnSeq expr var a -> b
$cfoldr :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) a b.
(a -> b -> b) -> b -> AnnSeq expr var a -> b
foldMap' :: (a -> m) -> AnnSeq expr var a -> m
$cfoldMap' :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) m a.
Monoid m =>
(a -> m) -> AnnSeq expr var a -> m
foldMap :: (a -> m) -> AnnSeq expr var a -> m
$cfoldMap :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) m a.
Monoid m =>
(a -> m) -> AnnSeq expr var a -> m
fold :: AnnSeq expr var m -> m
$cfold :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) m.
Monoid m =>
AnnSeq expr var m -> m
Foldable, Functor (AnnSeq expr var)
Foldable (AnnSeq expr var)
Functor (AnnSeq expr var)
-> Foldable (AnnSeq expr var)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    AnnSeq expr var (f a) -> f (AnnSeq expr var a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b))
-> (forall (m :: * -> *) a.
    Monad m =>
    AnnSeq expr var (m a) -> m (AnnSeq expr var a))
-> Traversable (AnnSeq expr var)
(a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
AnnSeq expr var (m a) -> m (AnnSeq expr var a)
forall (f :: * -> *) a.
Applicative f =>
AnnSeq expr var (f a) -> f (AnnSeq expr var a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *).
Functor (AnnSeq expr var)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *).
Foldable (AnnSeq expr var)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (m :: * -> *)
       a.
Monad m =>
AnnSeq expr var (m a) -> m (AnnSeq expr var a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (f :: * -> *)
       a.
Applicative f =>
AnnSeq expr var (f a) -> f (AnnSeq expr var a)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (m :: * -> *) a
       b.
Monad m =>
(a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (f :: * -> *) a
       b.
Applicative f =>
(a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b)
sequence :: AnnSeq expr var (m a) -> m (AnnSeq expr var a)
$csequence :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (m :: * -> *)
       a.
Monad m =>
AnnSeq expr var (m a) -> m (AnnSeq expr var a)
mapM :: (a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b)
$cmapM :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (m :: * -> *) a
       b.
Monad m =>
(a -> m b) -> AnnSeq expr var a -> m (AnnSeq expr var b)
sequenceA :: AnnSeq expr var (f a) -> f (AnnSeq expr var a)
$csequenceA :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (f :: * -> *)
       a.
Applicative f =>
AnnSeq expr var (f a) -> f (AnnSeq expr var a)
traverse :: (a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b)
$ctraverse :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *) (f :: * -> *) a
       b.
Applicative f =>
(a -> f b) -> AnnSeq expr var a -> f (AnnSeq expr var b)
$cp2Traversable :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *).
Foldable (AnnSeq expr var)
$cp1Traversable :: forall (expr :: (* -> *) -> * -> *) (var :: * -> *).
Functor (AnnSeq expr var)
Traversable)

instance (Pretty2 expr, Pretty1 var, Pretty cmd) => Pretty (AnnSeq expr var cmd) where
  prettysPrec :: Int -> AnnSeq expr var cmd -> ShowS
prettysPrec Int
_ (JustAssign [Assignment expr var]
as)
    = Endo String -> ShowS
forall a. Endo a -> a -> a
appEndo (Endo String -> ShowS)
-> ([Assignment expr var] -> Endo String)
-> [Assignment expr var]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Endo String] -> Endo String
forall a. Monoid a => [a] -> a
mconcat
    ([Endo String] -> Endo String)
-> ([Assignment expr var] -> [Endo String])
-> [Assignment expr var]
-> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Endo String -> [Endo String] -> [Endo String]
forall a. a -> [a] -> [a]
intersperse (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (String -> ShowS
showString String
"; "))
    ([Endo String] -> [Endo String])
-> ([Assignment expr var] -> [Endo String])
-> [Assignment expr var]
-> [Endo String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assignment expr var -> Endo String)
-> [Assignment expr var] -> [Endo String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo String)
-> (Assignment expr var -> ShowS)
-> Assignment expr var
-> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Assignment expr var -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10)
    ([Assignment expr var] -> ShowS) -> [Assignment expr var] -> ShowS
forall a b. (a -> b) -> a -> b
$ [Assignment expr var]
as

  prettysPrec Int
_ (CmdAssign cmd
cmd [Assignment expr var]
as)
    =  Endo String -> ShowS
forall a. Endo a -> a -> a
appEndo (Endo String -> ShowS)
-> ([Assignment expr var] -> Endo String)
-> [Assignment expr var]
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Endo String] -> Endo String
forall a. Monoid a => [a] -> a
mconcat
      ([Endo String] -> Endo String)
-> ([Assignment expr var] -> [Endo String])
-> [Assignment expr var]
-> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Endo String -> [Endo String] -> [Endo String]
forall a. a -> [a] -> [a]
intersperse (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (String -> ShowS
showString String
"; "))
      ([Endo String] -> [Endo String])
-> ([Assignment expr var] -> [Endo String])
-> [Assignment expr var]
-> [Endo String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (Int -> cmd -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 cmd
cmd) Endo String -> [Endo String] -> [Endo String]
forall a. a -> [a] -> [a]
:)
      ([Endo String] -> [Endo String])
-> ([Assignment expr var] -> [Endo String])
-> [Assignment expr var]
-> [Endo String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assignment expr var -> Endo String)
-> [Assignment expr var] -> [Endo String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo String)
-> (Assignment expr var -> ShowS)
-> Assignment expr var
-> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Assignment expr var -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10)
      ([Assignment expr var] -> ShowS) -> [Assignment expr var] -> ShowS
forall a b. (a -> b) -> a -> b
$ [Assignment expr var]
as

  prettysPrec Int
_ (Annotation AnnSeq expr var cmd
l Prop (expr var) Bool
p AnnSeq expr var cmd
r)
    = Int -> AnnSeq expr var cmd -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 AnnSeq expr var cmd
l
    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 -> Prop (expr var) Bool -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 Prop (expr var) Bool
p
    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 -> AnnSeq expr var cmd -> ShowS
forall a. Pretty a => Int -> a -> ShowS
prettysPrec Int
10 AnnSeq expr var cmd
r

--------------------------------------------------------------------------------
--  Combinators
--------------------------------------------------------------------------------

-- | Substitutes variables in the given proposition based on the given
-- assignment.
subAssignment
  :: (HMonad expr, VerifiableVar v)
  => Assignment expr v -> Prop (expr v) a -> Prop (expr v) a
subAssignment :: Assignment expr v -> Prop (expr v) a -> Prop (expr v) a
subAssignment (Assignment v a
targetVar expr v a
newExpr) = (forall b. expr v b -> expr v b)
-> Prop (expr v) a -> Prop (expr v) a
forall u (h :: (u -> *) -> u -> *) (t :: u -> *) (t' :: u -> *)
       (a :: u).
HFunctor h =>
(forall (b :: u). t b -> t' b) -> h t a -> h t' a
hmap (expr v b -> (forall b. v b -> expr v b) -> expr v b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k)
       (t' :: k -> *).
HBind h =>
h t a -> (forall (b :: k). t b -> h t' b) -> h t' a
^>>= expr v a -> v a -> v b -> expr v b
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) a b.
(HPointed expr, VerifiableVar v, Eq (VarKey v)) =>
expr v a -> v a -> v b -> expr v b
subVar expr v a
newExpr v a
targetVar)


-- | Chains substitutions, substituting using each assignment in the given list
-- in turn.
chainSub
  :: (HMonad expr, VerifiableVar v)
  => Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub :: Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (expr v) Bool
prop []       = Prop (expr v) Bool
prop
chainSub Prop (expr v) Bool
prop (Assignment expr v
a : [Assignment expr v]
as) = Assignment expr v -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) a.
(HMonad expr, VerifiableVar v) =>
Assignment expr v -> Prop (expr v) a -> Prop (expr v) a
subAssignment Assignment expr v
a (Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *).
(HMonad expr, VerifiableVar v) =>
Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (expr v) Bool
prop [Assignment expr v]
as)


-- | Joins two annotations together without a Hoare annotation in between. Fails
-- if this would place two non-assignment commands after each other, because
-- these need an annotation.
joinAnnSeq :: AnnSeq expr var cmd -> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
joinAnnSeq :: AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
joinAnnSeq (JustAssign [Assignment expr var]
xs) (JustAssign [Assignment expr var]
ys) = AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd))
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall a b. (a -> b) -> a -> b
$ [Assignment expr var] -> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign ([Assignment expr var]
xs [Assignment expr var]
-> [Assignment expr var] -> [Assignment expr var]
forall a. [a] -> [a] -> [a]
++ [Assignment expr var]
ys)
joinAnnSeq (CmdAssign cmd
cmd [Assignment expr var]
xs) (JustAssign [Assignment expr var]
ys) = AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd))
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall a b. (a -> b) -> a -> b
$ cmd -> [Assignment expr var] -> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
cmd -> [Assignment expr var] -> AnnSeq expr var cmd
CmdAssign cmd
cmd ([Assignment expr var]
xs [Assignment expr var]
-> [Assignment expr var] -> [Assignment expr var]
forall a. [a] -> [a] -> [a]
++ [Assignment expr var]
ys)
joinAnnSeq AnnSeq expr var cmd
s (JustAssign []) = AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (m :: * -> *) a. Monad m => a -> m a
return AnnSeq expr var cmd
s
joinAnnSeq (JustAssign []) AnnSeq expr var cmd
s = AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (m :: * -> *) a. Monad m => a -> m a
return AnnSeq expr var cmd
s
joinAnnSeq (Annotation AnnSeq expr var cmd
l Prop (expr var) Bool
p AnnSeq expr var cmd
r) AnnSeq expr var cmd
r' = AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
Annotation AnnSeq expr var cmd
l Prop (expr var) Bool
p (AnnSeq expr var cmd -> AnnSeq expr var cmd)
-> Maybe (AnnSeq expr var cmd) -> Maybe (AnnSeq expr var cmd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
joinAnnSeq AnnSeq expr var cmd
r AnnSeq expr var cmd
r'
joinAnnSeq AnnSeq expr var cmd
l' (Annotation AnnSeq expr var cmd
l Prop (expr var) Bool
p AnnSeq expr var cmd
r) = (\AnnSeq expr var cmd
l'' -> AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
Annotation AnnSeq expr var cmd
l'' Prop (expr var) Bool
p AnnSeq expr var cmd
r) (AnnSeq expr var cmd -> AnnSeq expr var cmd)
-> Maybe (AnnSeq expr var cmd) -> Maybe (AnnSeq expr var cmd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
joinAnnSeq AnnSeq expr var cmd
l' AnnSeq expr var cmd
l
joinAnnSeq AnnSeq expr var cmd
_ AnnSeq expr var cmd
_ = Maybe (AnnSeq expr var cmd)
forall a. Maybe a
Nothing


emptyAnnSeq :: AnnSeq expr var cmd
emptyAnnSeq :: AnnSeq expr var cmd
emptyAnnSeq = [Assignment expr var] -> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
[Assignment expr var] -> AnnSeq expr var cmd
JustAssign []

propAnnSeq :: Prop (expr var) Bool -> AnnSeq expr var cmd
propAnnSeq :: Prop (expr var) Bool -> AnnSeq expr var cmd
propAnnSeq Prop (expr var) Bool
p = AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> Prop (expr var) Bool
-> AnnSeq expr var cmd
-> AnnSeq expr var cmd
Annotation AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq Prop (expr var) Bool
p AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq

cmdAnnSeq :: cmd -> AnnSeq expr var cmd
cmdAnnSeq :: cmd -> AnnSeq expr var cmd
cmdAnnSeq cmd
c = cmd -> [Assignment expr var] -> AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
cmd -> [Assignment expr var] -> AnnSeq expr var cmd
CmdAssign cmd
c []


-- | 'JoinAnnSeq' forms a 'Monoid' out of 'AnnSeq' by propagating failure to
-- join arising from 'joinAnnSeq'.
newtype JoinAnnSeq expr var cmd = JoinAnnSeq { JoinAnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
tryJoinAnnSeq :: Maybe (AnnSeq expr var cmd) }

joiningAnnSeq :: AnnSeq expr var cmd -> JoinAnnSeq expr var cmd
joiningAnnSeq :: AnnSeq expr var cmd -> JoinAnnSeq expr var cmd
joiningAnnSeq = Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
JoinAnnSeq (Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd)
-> (AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd))
-> AnnSeq expr var cmd
-> JoinAnnSeq expr var cmd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall a. a -> Maybe a
Just

instance Semigroup (JoinAnnSeq expr var cmd) where
  JoinAnnSeq (Just AnnSeq expr var cmd
x) <> :: JoinAnnSeq expr var cmd
-> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd
<> JoinAnnSeq (Just AnnSeq expr var cmd
y) = Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
JoinAnnSeq (AnnSeq expr var cmd
x AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
-> AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
`joinAnnSeq` AnnSeq expr var cmd
y)
  JoinAnnSeq expr var cmd
_ <> JoinAnnSeq expr var cmd
_ = Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
JoinAnnSeq Maybe (AnnSeq expr var cmd)
forall a. Maybe a
Nothing

instance Monoid (JoinAnnSeq expr var cmd) where
  mempty :: JoinAnnSeq expr var cmd
mempty = Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
Maybe (AnnSeq expr var cmd) -> JoinAnnSeq expr var cmd
JoinAnnSeq (AnnSeq expr var cmd -> Maybe (AnnSeq expr var cmd)
forall a. a -> Maybe a
Just AnnSeq expr var cmd
forall (expr :: (* -> *) -> * -> *) (var :: * -> *) cmd.
AnnSeq expr var cmd
emptyAnnSeq)
  mappend :: JoinAnnSeq expr var cmd
-> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd
mappend = JoinAnnSeq expr var cmd
-> JoinAnnSeq expr var cmd -> JoinAnnSeq expr var cmd
forall a. Semigroup a => a -> a -> a
(<>)

--------------------------------------------------------------------------------
--  Generating verification conditions
--------------------------------------------------------------------------------

type MonadGenVCs expr var = MonadWriter [Prop (expr var) Bool]

type Triplet expr var a = (Prop (expr var) Bool, Prop (expr var) Bool, a)

-- | Generates verification conditions for a skip statement.
skipVCs
  :: (HMonad expr, MonadGenVCs expr var m)
  => Triplet expr var () -> m ()
skipVCs :: Triplet expr var () -> m ()
skipVCs (Prop (expr var) Bool
precond, Prop (expr var) Bool
postcond, ()) = [Prop (expr var) Bool] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Prop (expr var) Bool
precond Prop (expr var) Bool
-> Prop (expr var) Bool -> Prop (expr var) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> Prop (expr var) Bool
postcond]


-- | Generates verification conditions for an assignment.
assignVCs
  :: (HMonad expr, MonadGenVCs expr v m, VerifiableVar v)
  => Triplet expr v (Assignment expr v) -> m ()
assignVCs :: Triplet expr v (Assignment expr v) -> m ()
assignVCs (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond, Assignment expr v
assignment) = do
  let postcond' :: Prop (expr v) Bool
postcond' = Assignment expr v -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) a.
(HMonad expr, VerifiableVar v) =>
Assignment expr v -> Prop (expr v) a -> Prop (expr v) a
subAssignment Assignment expr v
assignment Prop (expr v) Bool
postcond
  [Prop (expr v) Bool] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Prop (expr v) Bool
precond Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> Prop (expr v) Bool
postcond']


-- | Generates verification conditions for a sequence of commands.
sequenceVCs
  :: (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 expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
sequenceVCs Triplet expr v cmd -> m a
cmdVCs (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond, AnnSeq expr v cmd
annSeq) =
  case AnnSeq expr v cmd
annSeq of
    -- A sequence of assignments can be verified by checking the precondition
    -- implies the postcondition, after substitutions are performed by the
    -- assignments.
    JustAssign [Assignment expr v]
as -> do
      [Prop (expr v) Bool] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Prop (expr v) Bool
precond Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *).
(HMonad expr, VerifiableVar v) =>
Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (expr v) Bool
postcond [Assignment expr v]
as]
      [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

    -- A command followed by a sequence of assignments can be verified by
    -- substituting based on the assignments in the postcondition, then verifying
    -- the command with the new postcondition and original precondition.
    CmdAssign cmd
cmd [Assignment expr v]
as ->
      let postcond' :: Prop (expr v) Bool
postcond' = Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
forall (expr :: (* -> *) -> * -> *) (v :: * -> *).
(HMonad expr, VerifiableVar v) =>
Prop (expr v) Bool -> [Assignment expr v] -> Prop (expr v) Bool
chainSub Prop (expr v) Bool
postcond [Assignment expr v]
as
      in (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []) (a -> [a]) -> m a -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Triplet expr v cmd -> m a
cmdVCs (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond', cmd
cmd)

    -- To verify @{P} C_1 ; {R} C_2 {Q}@, verify @{P} C_1 {R}@ and @{R} C_2 {Q}@.
    Annotation AnnSeq expr v cmd
l Prop (expr v) Bool
midcond AnnSeq expr v cmd
r -> do
      [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) ([a] -> [a] -> [a]) -> m [a] -> m ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Triplet expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
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 expr v cmd -> m a
cmdVCs (Prop (expr v) Bool
precond, Prop (expr v) Bool
midcond, AnnSeq expr v cmd
l)
           m ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Triplet expr v cmd -> m a)
-> Triplet expr v (AnnSeq expr v cmd) -> m [a]
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 expr v cmd -> m a
cmdVCs (Prop (expr v) Bool
midcond, Prop (expr v) Bool
postcond, AnnSeq expr v cmd
r)


-- | Generates verification conditions for a two-branch if command.
ifVCs
  :: (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 expr v cmd -> m a)
-> (cond -> Prop (expr v) Bool)
-> Triplet expr v (cond, cmd, cmd)
-> m (a, a)
ifVCs Triplet expr v cmd -> m a
cmdVCs cond -> Prop (expr v) Bool
condToProp (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond, (cond
cond, cmd
cmd1, cmd
cmd2)) = do
  let condProp :: Prop (expr v) Bool
condProp = cond -> Prop (expr v) Bool
condToProp cond
cond
  (a -> a -> (a, a)) -> m (a -> a -> (a, a))
forall (m :: * -> *) a. Monad m => a -> m a
return (,) m (a -> a -> (a, a)) -> m a -> m (a -> (a, a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Triplet expr v cmd -> m a
cmdVCs ((Prop (expr v) Bool
precond Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool
condProp), Prop (expr v) Bool
postcond, cmd
cmd1)
             m (a -> (a, a)) -> m a -> m (a, a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Triplet expr v cmd -> m a
cmdVCs ((Prop (expr v) Bool
precond Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *). Prop expr Bool -> Prop expr Bool
pnot Prop (expr v) Bool
condProp), Prop (expr v) Bool
postcond, cmd
cmd2)


-- | Generates verification conditions for a multi-branch if-then-else-...
-- command.
multiIfVCs
  :: (HMonad expr, Monad m)
  => (Triplet expr v cmd -> m ())
  -> (cond -> Prop (expr v) Bool)
  -> Triplet expr v [(Maybe cond, cmd)] -> m ()
multiIfVCs :: (Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Triplet expr v [(Maybe cond, cmd)]
-> m ()
multiIfVCs Triplet expr v cmd -> m ()
cmdVCs cond -> Prop (expr v) Bool
condToProp (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond, [(Maybe cond, cmd)]
branches) = Prop (expr v) Bool -> [(Maybe cond, cmd)] -> m ()
go Prop (expr v) Bool
precond [(Maybe cond, cmd)]
branches
  where
    go :: Prop (expr v) Bool -> [(Maybe cond, cmd)] -> m ()
go Prop (expr v) Bool
precond' ((Maybe cond
branchCond, cmd
branchCmd) : [(Maybe cond, cmd)]
rest) =
      case Maybe cond
branchCond of
        Just cond
bc -> do
          let bc' :: Prop (expr v) Bool
bc' = cond -> Prop (expr v) Bool
condToProp cond
bc
          Triplet expr v cmd -> m ()
cmdVCs ((Prop (expr v) Bool
precond' Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool
bc'), Prop (expr v) Bool
postcond, cmd
branchCmd)
          Prop (expr v) Bool -> [(Maybe cond, cmd)] -> m ()
go (Prop (expr v) Bool
precond' Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *). Prop expr Bool -> Prop expr Bool
pnot Prop (expr v) Bool
bc') [(Maybe cond, cmd)]
rest
        Maybe cond
Nothing -> do
          Triplet expr v cmd -> m ()
cmdVCs (Prop (expr v) Bool
precond', Prop (expr v) Bool
postcond, cmd
branchCmd)
    go Prop (expr v) Bool
_ [] = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Generates verification conditions for a while loop.
whileVCs
  :: (HMonad expr, MonadGenVCs expr v m)
  => (Triplet expr v cmd -> m ())
  -> (cond -> Prop (expr v) Bool)
  -> Prop (expr v) Bool -- ^ Loop invariant
  -> Triplet expr v (cond, cmd) -> m ()
whileVCs :: (Triplet expr v cmd -> m ())
-> (cond -> Prop (expr v) Bool)
-> Prop (expr v) Bool
-> Triplet expr v (cond, cmd)
-> m ()
whileVCs Triplet expr v cmd -> m ()
cmdVCs cond -> Prop (expr v) Bool
condToProp Prop (expr v) Bool
invariant (Prop (expr v) Bool
precond, Prop (expr v) Bool
postcond, (cond
cond, cmd
body)) = do
  let condProp :: Prop (expr v) Bool
condProp = cond -> Prop (expr v) Bool
condToProp cond
cond
  -- Assert that the invariant is maintained over the loop body
  Triplet expr v cmd -> m ()
cmdVCs ((Prop (expr v) Bool
invariant Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool
condProp), Prop (expr v) Bool
invariant, cmd
body)
  -- Assert that the invariant is implied by precondition, and at the end of the
  -- loop the invariant implies the postcondition
  [Prop (expr v) Bool] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Prop (expr v) Bool
precond Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> Prop (expr v) Bool
invariant, (Prop (expr v) Bool
invariant Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *). Prop expr Bool -> Prop expr Bool
pnot Prop (expr v) Bool
condProp) Prop (expr v) Bool -> Prop (expr v) Bool -> Prop (expr v) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*-> Prop (expr v) Bool
postcond]