{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE TypeFamilies     #-}

module Language.While.Hoare.Prover where

import           Data.SBV                (SBV)

import           Language.Expression.Prop
import           Language.Verification

import           Language.While.Hoare
import           Language.While.Syntax


checkPartialHoare
  :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV)
  => WhileProp l Bool
  -> WhileProp l Bool
  -> AnnCommand l a
  -> Query (WhileVar l) (SBV Bool)
checkPartialHoare :: WhileProp l Bool
-> WhileProp l Bool
-> AnnCommand l a
-> Query (WhileVar l) (SBV Bool)
checkPartialHoare WhileProp l Bool
precond WhileProp l Bool
postcond AnnCommand l a
cmd =
  do [WhileProp l Bool]
vcs <- case WhileProp l Bool
-> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
forall l a.
VerifiableVar (WhileVar l) =>
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 of
              Just [WhileProp l Bool]
x  -> [WhileProp l Bool] -> Query (WhileVar l) [WhileProp l Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return [WhileProp l Bool]
x
              Maybe [WhileProp l Bool]
Nothing -> String -> Query (WhileVar l) [WhileProp l Bool]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Command not sufficiently annotated"

     let bigVC :: WhileProp l Bool
bigVC = (WhileProp l Bool -> WhileProp l Bool -> WhileProp l Bool)
-> WhileProp l Bool -> [WhileProp l Bool] -> WhileProp l Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr WhileProp l Bool -> WhileProp l Bool -> WhileProp l Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
(*&&) (Bool -> WhileProp l Bool
forall (expr :: * -> *). Bool -> Prop expr Bool
plit Bool
True) [WhileProp l Bool]
vcs

     WhileProp l Bool -> Query (WhileVar l) (SBV Bool)
forall (expr :: (* -> *) -> * -> *) (v :: * -> *) b.
(HMonad expr, HTraversable expr, VerifiableVar v,
 Exception (VerifierError v), HFoldableAt SBV expr,
 VarSym v ~ SBV) =>
Prop (expr v) b -> Query v (SBV b)
evalPropSimple WhileProp l Bool
bigVC

provePartialHoare
  :: (VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV, VarEnv (WhileVar l) ~ ())
  => WhileProp l Bool
  -> WhileProp l Bool
  -> AnnCommand l a
  -> IO (Either (VerifierError (WhileVar l)) Bool)
provePartialHoare :: WhileProp l Bool
-> WhileProp l Bool
-> AnnCommand l a
-> IO (Either (VerifierError (WhileVar l)) Bool)
provePartialHoare WhileProp l Bool
precond WhileProp l Bool
postcond AnnCommand l a
cmd =
  Verifier (WhileVar l) Bool
-> IO (Either (VerifierError (WhileVar l)) Bool)
forall (v :: * -> *) a.
VerifiableVar v =>
Verifier v a -> IO (Either (VerifierError v) a)
runVerifier (Verifier (WhileVar l) Bool
 -> IO (Either (VerifierError (WhileVar l)) Bool))
-> (Query (WhileVar l) (SBV Bool) -> Verifier (WhileVar l) Bool)
-> Query (WhileVar l) (SBV Bool)
-> IO (Either (VerifierError (WhileVar l)) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Query (WhileVar l) (SBV Bool) -> () -> Verifier (WhileVar l) Bool)
-> ()
-> Query (WhileVar l) (SBV Bool)
-> Verifier (WhileVar l) Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Query (WhileVar l) (SBV Bool) -> () -> Verifier (WhileVar l) Bool
forall (v :: * -> *).
VerifiableVar v =>
Query v (SBV Bool) -> VarEnv v -> Verifier v Bool
query () (Query (WhileVar l) (SBV Bool)
 -> IO (Either (VerifierError (WhileVar l)) Bool))
-> Query (WhileVar l) (SBV Bool)
-> IO (Either (VerifierError (WhileVar l)) Bool)
forall a b. (a -> b) -> a -> b
$ WhileProp l Bool
-> WhileProp l Bool
-> AnnCommand l a
-> Query (WhileVar l) (SBV Bool)
forall l a.
(VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV) =>
WhileProp l Bool
-> WhileProp l Bool
-> AnnCommand l a
-> Query (WhileVar l) (SBV Bool)
checkPartialHoare WhileProp l Bool
precond WhileProp l Bool
postcond AnnCommand l a
cmd