{-|
Module      : Language.Contract.Proof
Description : Theorem prover for type checking.
Copyright   : (c) Xie Ruifeng, 2020
License     : AGPL-3
Maintainer  : krantz.xrf@outlook.com
Stability   : experimental
Portability : portable
-}
module Language.Contract.Proof
  ( pattern Falsified
  , pattern Proven
  , isFalsified
  , tryProve
  , naiveTryProve
  ) where

import Data.List
import Data.SBV.Trans
import Numeric.Natural

import Control.Monad.Reader
import Control.Monad.Trans.Maybe

import Language.Contract.AST
import Language.Contract.Pretty

data Var
  = VBool SBool
  | VNat SInteger
  | VUnit
  | VFunc (Var -> Var)

asNat :: Var -> SInteger
asNat :: Var -> SInteger
asNat ~(VNat n :: SInteger
n) = SInteger
n

asBool :: Var -> SBool
asBool :: Var -> SBool
asBool ~(VBool b :: SBool
b) = SBool
b

asFunc :: Var -> Var -> Var
asFunc :: Var -> Var -> Var
asFunc ~(VFunc f :: Var -> Var
f) = Var -> Var
f

freeVar :: (MonadFail m, MonadSymbolic m) => Natural -> Type -> m Var
freeVar :: Natural -> Type -> m Var
freeVar n :: Natural
n TBoolean = SBool -> Var
VBool (SBool -> Var) -> m SBool -> m Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m SBool
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
free (Natural -> String
makeVarName Natural
n)
freeVar n :: Natural
n TNatural = SInteger -> Var
VNat (SInteger -> Var) -> m SInteger -> m Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m SInteger
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
free (Natural -> String
makeVarName Natural
n)
freeVar _ TUnit = Var -> m Var
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var
VUnit
freeVar _ _ = String -> m Var
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Function type not supported in SBV."

iteVar :: Var -> Var -> Var -> Var
iteVar :: Var -> Var -> Var -> Var
iteVar ~(VBool b :: SBool
b) t :: Var
t f :: Var
f = case (Var
t, Var
f) of
  (VNat x :: SInteger
x, ~(VNat y :: SInteger
y)) -> SInteger -> Var
VNat (SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b SInteger
x SInteger
y)
  (VBool x :: SBool
x, ~(VBool y :: SBool
y)) -> SBool -> Var
VBool (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b SBool
x SBool
y)
  (_, _) -> Var
VUnit

makeBoolTerm :: [Var] -> Term -> SBool
makeBoolTerm :: [Var] -> Term -> SBool
makeBoolTerm vs :: [Var]
vs = Var -> SBool
asBool (Var -> SBool) -> (Term -> Var) -> Term -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> Term -> Var
makeTerm [Var]
vs

constrainPremise :: MonadIO m => [Var] -> Term -> SymbolicT m ()
constrainPremise :: [Var] -> Term -> SymbolicT m ()
constrainPremise vs :: [Var]
vs = SBool -> SymbolicT m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> SymbolicT m ())
-> (Term -> SBool) -> Term -> SymbolicT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> Term -> SBool
makeBoolTerm [Var]
vs

makeTerm :: [Var] -> Term -> Var
makeTerm :: [Var] -> Term -> Var
makeTerm _  Unit = Var
VUnit
makeTerm vs :: [Var]
vs (Lambda _ _ t :: Term
t) = (Var -> Var) -> Var
VFunc ((Var -> Var) -> Var) -> (Var -> Var) -> Var
forall a b. (a -> b) -> a -> b
$ \x :: Var
x -> [Var] -> Term -> Var
makeTerm (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
vs) Term
t
makeTerm vs :: [Var]
vs (App f :: Term
f x :: Term
x) = Var -> Var -> Var
asFunc ([Var] -> Term -> Var
makeTerm [Var]
vs Term
f) ([Var] -> Term -> Var
makeTerm [Var]
vs Term
x)
makeTerm vs :: [Var]
vs (Assert _ t :: Term
t) = [Var] -> Term -> Var
makeTerm [Var]
vs Term
t
makeTerm vs :: [Var]
vs (Atom n :: Natural
n) = [Var]
vs [Var] -> Natural -> Var
forall i a. Integral i => [a] -> i -> a
`genericIndex` Natural
n
makeTerm vs :: [Var]
vs (If b :: Term
b t :: Term
t f :: Term
f) = Var -> Var -> Var -> Var
iteVar ([Var] -> Term -> Var
makeTerm [Var]
vs Term
b) ([Var] -> Term -> Var
makeTerm [Var]
vs Term
t) ([Var] -> Term -> Var
makeTerm [Var]
vs Term
f)
makeTerm vs :: [Var]
vs (Succ n :: Term
n) = SInteger -> Var
VNat (SInteger -> Var) -> (Var -> SInteger) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ 1) (SInteger -> SInteger) -> (Var -> SInteger) -> Var -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> SInteger
asNat (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ [Var] -> Term -> Var
makeTerm [Var]
vs Term
n
makeTerm vs :: [Var]
vs (Pred n :: Term
n) = SInteger -> Var
VNat (SInteger -> Var) -> (Var -> SInteger) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
subtract 1 (SInteger -> SInteger) -> (Var -> SInteger) -> Var -> SInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> SInteger
asNat (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ [Var] -> Term -> Var
makeTerm [Var]
vs Term
n
makeTerm vs :: [Var]
vs (IsZero n :: Term
n) = SBool -> Var
VBool (SBool -> Var) -> (Var -> SBool) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== 0) (SInteger -> SBool) -> (Var -> SInteger) -> Var -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> SInteger
asNat (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$ [Var] -> Term -> Var
makeTerm [Var]
vs Term
n
makeTerm _  (Natural n :: Natural
n) = SInteger -> Var
VNat (SInteger -> Var) -> SInteger -> Var
forall a b. (a -> b) -> a -> b
$ Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Integer -> SInteger) -> Integer -> SInteger
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n
makeTerm _  (Boolean b :: Bool
b) = SBool -> Var
VBool (SBool -> Var) -> SBool -> Var
forall a b. (a -> b) -> a -> b
$ Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
b

-- |A falsified theorem.
pattern Falsified :: ThmResult
pattern $mFalsified :: forall r. ThmResult -> (Void# -> r) -> (Void# -> r) -> r
Falsified <- ThmResult (isFalsified -> True)

-- |Is this theorem falsified?
isFalsified :: SMTResult -> Bool
isFalsified :: SMTResult -> Bool
isFalsified (Satisfiable _ _) = Bool
True
isFalsified (SatExtField _ _) = Bool
True
isFalsified _ = Bool
False

-- |A proven theorem.
pattern Proven :: ThmResult
pattern $mProven :: forall r. ThmResult -> (Void# -> r) -> (Void# -> r) -> r
Proven <- ThmResult (Unsatisfiable _ _)

-- |Try prove with sbv.
tryProve :: MonadIO m => [Type] -> [Term] -> Term -> m (Maybe ThmResult)
tryProve :: [Type] -> [Term] -> Term -> m (Maybe ThmResult)
tryProve bindings :: [Type]
bindings premises :: [Term]
premises target :: Term
target =
  let prove' :: SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult
prove' = SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult
forall (m :: * -> *) a. MProvable m a => a -> m ThmResult
prove :: SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult
  in IO (Maybe ThmResult) -> m (Maybe ThmResult)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe ThmResult) -> m (Maybe ThmResult))
-> IO (Maybe ThmResult) -> m (Maybe ThmResult)
forall a b. (a -> b) -> a -> b
$ MaybeT IO ThmResult -> IO (Maybe ThmResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO ThmResult -> IO (Maybe ThmResult))
-> MaybeT IO ThmResult -> IO (Maybe ThmResult)
forall a b. (a -> b) -> a -> b
$ SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult
prove' (SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult)
-> SymbolicT (MaybeT IO) SBool -> MaybeT IO ThmResult
forall a b. (a -> b) -> a -> b
$ do
  [Var]
vars <- [(Natural, Type)]
-> ((Natural, Type) -> SymbolicT (MaybeT IO) Var)
-> SymbolicT (MaybeT IO) [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Natural] -> [Type] -> [(Natural, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Type]
bindings) ((Natural -> Type -> SymbolicT (MaybeT IO) Var)
-> (Natural, Type) -> SymbolicT (MaybeT IO) Var
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Natural -> Type -> SymbolicT (MaybeT IO) Var
forall (m :: * -> *).
(MonadFail m, MonadSymbolic m) =>
Natural -> Type -> m Var
freeVar)
  [Var]
-> (Var -> SymbolicT (MaybeT IO) ()) -> SymbolicT (MaybeT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var]
vars ((Var -> SymbolicT (MaybeT IO) ()) -> SymbolicT (MaybeT IO) ())
-> (Var -> SymbolicT (MaybeT IO) ()) -> SymbolicT (MaybeT IO) ()
forall a b. (a -> b) -> a -> b
$ \case
    VNat x :: SInteger
x -> SBool -> SymbolicT (MaybeT IO) ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 0)
    _ -> () -> SymbolicT (MaybeT IO) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  (Term -> SymbolicT (MaybeT IO) ())
-> [Term] -> SymbolicT (MaybeT IO) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Var] -> Term -> SymbolicT (MaybeT IO) ()
forall (m :: * -> *). MonadIO m => [Var] -> Term -> SymbolicT m ()
constrainPremise [Var]
vars) [Term]
premises
  SBool -> SymbolicT (MaybeT IO) SBool
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Var] -> Term -> SBool
makeBoolTerm [Var]
vars Term
target)

-- |Use the naive theorem prover.
naiveTryProve :: (MonadFail m, MonadIO m) => [Type] -> [Term] -> Term -> m ()
naiveTryProve :: [Type] -> [Term] -> Term -> m ()
naiveTryProve _ _ (Boolean True) = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn "Q.E.D. (Trivial)")
naiveTryProve _ [] _ = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn "Falsified") m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Falsified"
naiveTryProve _ premise :: [Term]
premise _ | Bool -> Term
Boolean Bool
False Term -> [Term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
premise
  = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn "Q.E.D. (Vacuous)")
naiveTryProve _ premise :: [Term]
premise t :: Term
t | Term
t Term -> [Term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
premise = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn "Q.E.D.")
naiveTryProve _ _ _ = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn "Unknown")