{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}

module Language.While.Test where

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

import           Language.While.Hoare
import           Language.While.Hoare.Prover
import           Language.While.Syntax
import           Language.While.Syntax.Sugar

import           Data.SBV                    (SMTConfig (..), defaultSMTCfg)

testCommandAnn :: Command String (PropAnn String ())
testCommandAnn :: Command String (PropAnn String ())
testCommandAnn =
  String
"Q" String
-> WhileExpr String AlgReal -> Command String (PropAnn String ())
forall l a. l -> WhileExpr l AlgReal -> Command l a
.=. WhileExpr String AlgReal
0   Command String (PropAnn String ())
-> Command String (PropAnn String ())
-> Command String (PropAnn String ())
forall l a. Command l a -> Command l a -> Command l a
\\ (HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== WhileExpr String AlgReal
"x") Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&& HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"Q" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== WhileExpr String AlgReal
0)) Prop (HFree WhileOp (WhileVar String)) Bool
-> Command String (PropAnn String ())
-> Command String (PropAnn String ())
forall l. WhileProp l Bool -> AnnCommand l () -> AnnCommand l ()
^^^
  HFree WhileOp (WhileVar String) Bool
-> Command String (PropAnn String ())
-> Command String (PropAnn String ())
forall l a. WhileExpr l Bool -> Command l a -> Command l a
CWhile (WhileExpr String AlgReal
"Y" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.<= WhileExpr String AlgReal
"R")
  ((HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"x" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== (WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
+ WhileExpr String AlgReal
"Y" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
* WhileExpr String AlgReal
"Q"))) Prop (HFree WhileOp (WhileVar String)) Bool
-> Command String (PropAnn String ())
-> Command String (PropAnn String ())
forall l. WhileProp l Bool -> AnnCommand l () -> AnnCommand l ()
^^^
   (  String
"R" String
-> WhileExpr String AlgReal -> Command String (PropAnn String ())
forall l a. l -> WhileExpr l AlgReal -> Command l a
.=. WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
- WhileExpr String AlgReal
"Y"
   Command String (PropAnn String ())
-> Command String (PropAnn String ())
-> Command String (PropAnn String ())
forall l a. Command l a -> Command l a -> Command l a
\\ String
"Q" String
-> WhileExpr String AlgReal -> Command String (PropAnn String ())
forall l a. l -> WhileExpr l AlgReal -> Command l a
.=. WhileExpr String AlgReal
"Q" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
+ WhileExpr String AlgReal
1
   ))

testPrecond :: WhileProp String Bool
testPrecond :: Prop (HFree WhileOp (WhileVar String)) Bool
testPrecond = HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== WhileExpr String AlgReal
"x")

testPostcond :: WhileProp String Bool
testPostcond :: Prop (HFree WhileOp (WhileVar String)) Bool
testPostcond =
  HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"x" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.== (WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
+ WhileExpr String AlgReal
"Y" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> WhileExpr String AlgReal
forall a. Num a => a -> a -> a
* WhileExpr String AlgReal
"Q")) Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *).
Prop expr Bool -> Prop expr Bool -> Prop expr Bool
*&&
  HFree WhileOp (WhileVar String) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
forall (expr :: * -> *) a. expr a -> Prop expr a
expr (WhileExpr String AlgReal
"R" WhileExpr String AlgReal
-> WhileExpr String AlgReal -> HFree WhileOp (WhileVar String) Bool
forall l.
WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l Bool
.< WhileExpr String AlgReal
"Y")

testConfig :: SMTConfig
testConfig :: SMTConfig
testConfig = SMTConfig
defaultSMTCfg { verbose :: Bool
verbose = Bool
False }

testVcs :: Maybe [WhileProp String Bool]
testVcs :: Maybe [Prop (HFree WhileOp (WhileVar String)) Bool]
testVcs = Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
-> Command String (PropAnn String ())
-> Maybe [Prop (HFree WhileOp (WhileVar String)) Bool]
forall l a.
VerifiableVar (WhileVar l) =>
WhileProp l Bool
-> WhileProp l Bool -> AnnCommand l a -> Maybe [WhileProp l Bool]
generateVCs Prop (HFree WhileOp (WhileVar String)) Bool
testPrecond Prop (HFree WhileOp (WhileVar String)) Bool
testPostcond Command String (PropAnn String ())
testCommandAnn

test :: IO (Either (VerifierError (WhileVar String)) Bool)
test :: IO (Either (VerifierError (WhileVar String)) Bool)
test = SMTConfig
-> Verifier (WhileVar String) Bool
-> IO (Either (VerifierError (WhileVar String)) Bool)
forall (v :: * -> *) a.
VerifiableVar v =>
SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)
runVerifierWith SMTConfig
testConfig (Verifier (WhileVar String) Bool
 -> IO (Either (VerifierError (WhileVar String)) Bool))
-> Verifier (WhileVar String) Bool
-> IO (Either (VerifierError (WhileVar String)) Bool)
forall a b. (a -> b) -> a -> b
$ (Query (WhileVar String) SBool
 -> () -> Verifier (WhileVar String) Bool)
-> ()
-> Query (WhileVar String) SBool
-> Verifier (WhileVar String) Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Query (WhileVar String) SBool
-> () -> Verifier (WhileVar String) Bool
forall (v :: * -> *).
VerifiableVar v =>
Query v SBool -> VarEnv v -> Verifier v Bool
query () (Query (WhileVar String) SBool -> Verifier (WhileVar String) Bool)
-> Query (WhileVar String) SBool -> Verifier (WhileVar String) Bool
forall a b. (a -> b) -> a -> b
$
  Prop (HFree WhileOp (WhileVar String)) Bool
-> Prop (HFree WhileOp (WhileVar String)) Bool
-> Command String (PropAnn String ())
-> Query (WhileVar String) SBool
forall l a.
(VerifiableVar (WhileVar l), VarSym (WhileVar l) ~ SBV) =>
WhileProp l Bool
-> WhileProp l Bool -> AnnCommand l a -> Query (WhileVar l) SBool
checkPartialHoare Prop (HFree WhileOp (WhileVar String)) Bool
testPrecond Prop (HFree WhileOp (WhileVar String)) Bool
testPostcond Command String (PropAnn String ())
testCommandAnn