-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.TP.Kernel
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Kernel of the TP prover API.
-----------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.TP.Kernel (
         Proposition,  Proof(..)
       , axiom
       , lemma,          lemmaWith
       , inductiveLemma, inductiveLemmaWith
       , internalAxiom
       , TPProofContext (..), smtProofStep, HasInductionSchema(..)
       ) where

import Control.Monad.Trans  (liftIO, MonadIO)

import Data.List  (intercalate)
import Data.Maybe (catMaybes)

import Data.SBV.Core.Data     hiding (None)
import Data.SBV.Trans.Control hiding (getProof)
import Data.SBV.Core.Symbolic (MonadSymbolic)

import Data.SBV.SMT.SMT
import Data.SBV.Core.Model
import Data.SBV.Provers.Prover

import Data.SBV.TP.Utils

import Data.Time (NominalDiffTime)
import Data.SBV.Utils.TDiff

import Data.Dynamic

import Type.Reflection (typeRep)

import qualified Data.SBV.List as SL (nil, (.:))

-- | A proposition is something SBV is capable of proving/disproving in TP.
type Proposition a = ( QNot a
                     , QuantifiedBool a
                     , QSaturate Symbolic a
                     , Skolemize (NegatesTo a)
                     , Satisfiable (Symbolic (SkolemsTo (NegatesTo a)))
                     , Constraint  Symbolic  (SkolemsTo (NegatesTo a))
                     , Typeable a
                     )

-- | An inductive proposition is a proposition that has an induction scheme associated with it.
type Inductive a = (HasInductionSchema a, Proposition a)

-- | A class of values that has an associated induction schema. SBV manages this internally.
class HasInductionSchema a where
  inductionSchema :: a -> ProofObj

-- | Induction schema for integers. Note that this is good for proving properties over naturals really.
-- There are other instances that would apply to all integers, but this one is really the most useful
-- in practice.
instance HasInductionSchema (Forall nm Integer -> SBool) where
   inductionSchema :: (Forall nm Integer -> SBool) -> ProofObj
inductionSchema Forall nm Integer -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger" SBool
ax
     where pf :: SBV Integer -> SBool
pf = Forall nm Integer -> SBool
p (Forall nm Integer -> SBool)
-> (SBV Integer -> Forall nm Integer) -> SBV Integer -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall
           ax :: SBool
ax =   [SBool] -> SBool
sAnd [SBV Integer -> SBool
pf SBV Integer
0, (Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBool
pf SBV Integer
i) SBool -> SBool -> SBool
.=> SBV Integer -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1))]
              SBool -> SBool -> SBool
.=> (Forall Any Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) -> SBV Integer -> SBool
pf SBV Integer
i)

-- | Induction schema for integers with one extra argument
instance SymVal at => HasInductionSchema (Forall nm Integer -> Forall an at -> SBool) where
   inductionSchema :: (Forall nm Integer -> Forall an at -> SBool) -> ProofObj
inductionSchema Forall nm Integer -> Forall an at -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger1" SBool
ax
     where pf :: SBV Integer -> SBV at -> SBool
pf SBV Integer
i SBV at
a = Forall nm Integer -> Forall an at -> SBool
p (SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV Integer
i) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a)
           ax :: SBool
ax     = [SBool] -> SBool
sAnd [ (Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\           (Forall SBV at
a) -> SBV Integer -> SBV at -> SBool
pf SBV Integer
0 SBV at
a)
                         , (Forall Any Integer -> Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBool
pf SBV Integer
i SBV at
a) SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1) SBV at
a)]
                    SBool -> SBool -> SBool
.=>    (Forall Any Integer -> Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) -> SBV Integer -> SBV at -> SBool
pf SBV Integer
i SBV at
a)

-- | Induction schema for integers with two extra arguments
instance (SymVal at, SymVal bt) => HasInductionSchema (Forall nm Integer -> Forall an at -> Forall bn bt -> SBool) where
   inductionSchema :: (Forall nm Integer -> Forall an at -> Forall bn bt -> SBool)
-> ProofObj
inductionSchema Forall nm Integer -> Forall an at -> Forall bn bt -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger2" SBool
ax
     where pf :: SBV Integer -> SBV at -> SBV bt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b = Forall nm Integer -> Forall an at -> Forall bn bt -> SBool
p (SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV Integer
i) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b)
           ax :: SBool
ax       = [SBool] -> SBool
sAnd [ (Forall Any at -> Forall Any bt -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\           (Forall SBV at
a) (Forall SBV bt
b) -> SBV Integer -> SBV at -> SBV bt -> SBool
pf SBV Integer
0 SBV at
a SBV bt
b)
                           , (Forall Any Integer -> Forall Any at -> Forall Any bt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b) SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1) SBV at
a SBV bt
b)]
                      SBool -> SBool -> SBool
.=>    (Forall Any Integer -> Forall Any at -> Forall Any bt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) -> SBV Integer -> SBV at -> SBV bt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b)

-- | Induction schema for integers with three extra arguments
instance (SymVal at, SymVal bt, SymVal ct) => HasInductionSchema (Forall nm Integer -> Forall an at -> Forall bn bt -> Forall cn ct -> SBool) where
   inductionSchema :: (Forall nm Integer
 -> Forall an at -> Forall bn bt -> Forall cn ct -> SBool)
-> ProofObj
inductionSchema Forall nm Integer
-> Forall an at -> Forall bn bt -> Forall cn ct -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger3" SBool
ax
     where pf :: SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c = Forall nm Integer
-> Forall an at -> Forall bn bt -> Forall cn ct -> SBool
p (SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV Integer
i) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c)
           ax :: SBool
ax         = [SBool] -> SBool
sAnd [ (Forall Any at -> Forall Any bt -> Forall Any ct -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\           (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV Integer
0 SBV at
a SBV bt
b SBV ct
c)
                             , (Forall Any Integer
 -> Forall Any at -> Forall Any bt -> Forall Any ct -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c) SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1) SBV at
a SBV bt
b SBV ct
c)]
                        SBool -> SBool -> SBool
.=>    (Forall Any Integer
 -> Forall Any at -> Forall Any bt -> Forall Any ct -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c)

-- | Induction schema for integers with four extra arguments
instance (SymVal at, SymVal bt, SymVal ct, SymVal dt) => HasInductionSchema (Forall nm Integer -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> SBool) where
   inductionSchema :: (Forall nm Integer
 -> Forall an at
 -> Forall bn bt
 -> Forall cn ct
 -> Forall dn dt
 -> SBool)
-> ProofObj
inductionSchema Forall nm Integer
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger4" SBool
ax
     where pf :: SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d = Forall nm Integer
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> SBool
p (SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV Integer
i) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c) (SBV dt -> Forall dn dt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV dt
d)
           ax :: SBool
ax           = [SBool] -> SBool
sAnd [ (Forall Any at
 -> Forall Any bt -> Forall Any ct -> Forall Any dt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\           (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV Integer
0 SBV at
a SBV bt
b SBV ct
c SBV dt
d)
                               , (Forall Any Integer
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d) SBool -> SBool -> SBool
.=> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1) SBV at
a SBV bt
b SBV ct
c SBV dt
d)]
                          SBool -> SBool -> SBool
.=>    (Forall Any Integer
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> SBV Integer -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d)

-- | Induction schema for integers with five extra arguments
instance (SymVal at, SymVal bt, SymVal ct, SymVal dt, SymVal et) => HasInductionSchema (Forall nm Integer -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> Forall en et -> SBool) where
   inductionSchema :: (Forall nm Integer
 -> Forall an at
 -> Forall bn bt
 -> Forall cn ct
 -> Forall dn dt
 -> Forall en et
 -> SBool)
-> ProofObj
inductionSchema Forall nm Integer
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> Forall en et
-> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
"inductInteger5" SBool
ax
     where pf :: SBV Integer
-> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e = Forall nm Integer
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> Forall en et
-> SBool
p (SBV Integer -> Forall nm Integer
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV Integer
i) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c) (SBV dt -> Forall dn dt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV dt
d) (SBV et -> Forall en et
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV et
e)
           ax :: SBool
ax             = [SBool] -> SBool
sAnd [ (Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\           (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> SBV Integer
-> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV Integer
0 SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)
                                 , (Forall Any Integer
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> (SBV Integer
i SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
0 SBool -> SBool -> SBool
.=> SBV Integer
-> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e) SBool -> SBool -> SBool
.=> SBV Integer
-> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf (SBV Integer
i SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
1) SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)]
                            SBool -> SBool -> SBool
.=>    (Forall Any Integer
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV Integer
i) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> SBV Integer
-> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV Integer
i SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)

-- | Induction schema for lists.
instance SymVal x => HasInductionSchema (Forall nm [x] -> SBool) where
   inductionSchema :: (Forall nm [x] -> SBool) -> ProofObj
inductionSchema Forall nm [x] -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x])) SBool
ax
     where pf :: SBV [x] -> SBool
pf = Forall nm [x] -> SBool
p (Forall nm [x] -> SBool)
-> (SBV [x] -> Forall nm [x]) -> SBV [x] -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall
           ax :: SBool
ax =   [SBool] -> SBool
sAnd [SBV [x] -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil, (Forall Any x -> Forall Any [x] -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) -> SBV [x] -> SBool
pf SBV [x]
xs SBool -> SBool -> SBool
.=> SBV [x] -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs))]
              SBool -> SBool -> SBool
.=> (Forall Any [x] -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) -> SBV [x] -> SBool
pf SBV [x]
xs)

-- | Induction schema for lists with one extra argument
instance (SymVal x, SymVal at) => HasInductionSchema (Forall nm [x] -> Forall an at -> SBool) where
   inductionSchema :: (Forall nm [x] -> Forall an at -> SBool) -> ProofObj
inductionSchema Forall nm [x] -> Forall an at -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"1") SBool
ax
     where pf :: SBV [x] -> SBV at -> SBool
pf SBV [x]
xs SBV at
a = Forall nm [x] -> Forall an at -> SBool
p (SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV [x]
xs) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a)
           ax :: SBool
ax      = [SBool] -> SBool
sAnd [ (Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\                       (Forall SBV at
a) -> SBV [x] -> SBV at -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil SBV at
a)
                          , (Forall Any x -> Forall Any [x] -> Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) (Forall SBV at
a) -> SBV [x] -> SBV at -> SBool
pf SBV [x]
xs SBV at
a SBool -> SBool -> SBool
.=> SBV [x] -> SBV at -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs) SBV at
a)]
                     SBool -> SBool -> SBool
.=>    (Forall Any [x] -> Forall Any at -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) (Forall SBV at
a) -> SBV [x] -> SBV at -> SBool
pf SBV [x]
xs SBV at
a)

-- | Induction schema for lists with two extra arguments
instance (SymVal x, SymVal at, SymVal bt) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> SBool) where
   inductionSchema :: (Forall nm [x] -> Forall an at -> Forall bn bt -> SBool)
-> ProofObj
inductionSchema Forall nm [x] -> Forall an at -> Forall bn bt -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"2") SBool
ax
     where pf :: SBV [x] -> SBV at -> SBV bt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b = Forall nm [x] -> Forall an at -> Forall bn bt -> SBool
p (SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV [x]
xs) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b)
           ax :: SBool
ax        = [SBool] -> SBool
sAnd [ (Forall Any at -> Forall Any bt -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\                       (Forall SBV at
a) (Forall SBV bt
b) -> SBV [x] -> SBV at -> SBV bt -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil SBV at
a SBV bt
b)
                            , (Forall Any x
 -> Forall Any [x] -> Forall Any at -> Forall Any bt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) -> SBV [x] -> SBV at -> SBV bt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBool -> SBool -> SBool
.=> SBV [x] -> SBV at -> SBV bt -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs) SBV at
a SBV bt
b)]
                       SBool -> SBool -> SBool
.=>    (Forall Any [x] -> Forall Any at -> Forall Any bt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) -> SBV [x] -> SBV at -> SBV bt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b)

-- | Induction schema for lists with three extra arguments
instance (SymVal x, SymVal at, SymVal bt, SymVal ct) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> SBool) where
   inductionSchema :: (Forall nm [x]
 -> Forall an at -> Forall bn bt -> Forall cn ct -> SBool)
-> ProofObj
inductionSchema Forall nm [x]
-> Forall an at -> Forall bn bt -> Forall cn ct -> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"3") SBool
ax
     where pf :: SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c = Forall nm [x]
-> Forall an at -> Forall bn bt -> Forall cn ct -> SBool
p (SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV [x]
xs) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c)
           ax :: SBool
ax          = [SBool] -> SBool
sAnd [ (Forall Any at -> Forall Any bt -> Forall Any ct -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\                       (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil SBV at
a SBV bt
b SBV ct
c)
                              , (Forall Any x
 -> Forall Any [x]
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBool -> SBool -> SBool
.=> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs) SBV at
a SBV bt
b SBV ct
c)]
                         SBool -> SBool -> SBool
.=>    (Forall Any [x]
 -> Forall Any at -> Forall Any bt -> Forall Any ct -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c)

-- | Induction schema for lists with four extra arguments
instance (SymVal x, SymVal at, SymVal bt, SymVal ct, SymVal dt) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> SBool) where
   inductionSchema :: (Forall nm [x]
 -> Forall an at
 -> Forall bn bt
 -> Forall cn ct
 -> Forall dn dt
 -> SBool)
-> ProofObj
inductionSchema Forall nm [x]
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"4") SBool
ax
     where pf :: SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d = Forall nm [x]
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> SBool
p (SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV [x]
xs) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c) (SBV dt -> Forall dn dt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV dt
d)
           ax :: SBool
ax            = [SBool] -> SBool
sAnd [ (Forall Any at
 -> Forall Any bt -> Forall Any ct -> Forall Any dt -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\                       (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil SBV at
a SBV bt
b SBV ct
c SBV dt
d)
                                , (Forall Any x
 -> Forall Any [x]
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d SBool -> SBool -> SBool
.=> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs) SBV at
a SBV bt
b SBV ct
c SBV dt
d)]
                           SBool -> SBool -> SBool
.=>    (Forall Any [x]
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d)

-- | Induction schema for lists with five extra arguments
instance (SymVal x, SymVal at, SymVal bt, SymVal ct, SymVal dt, SymVal et) => HasInductionSchema (Forall nm [x] -> Forall an at -> Forall bn bt -> Forall cn ct -> Forall dn dt -> Forall en et -> SBool) where
   inductionSchema :: (Forall nm [x]
 -> Forall an at
 -> Forall bn bt
 -> Forall cn ct
 -> Forall dn dt
 -> Forall en et
 -> SBool)
-> ProofObj
inductionSchema Forall nm [x]
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> Forall en et
-> SBool
p = Proof SBool -> ProofObj
forall a. Proof a -> ProofObj
proofOf (Proof SBool -> ProofObj) -> Proof SBool -> ProofObj
forall a b. (a -> b) -> a -> b
$ String -> SBool -> Proof SBool
forall a. Proposition a => String -> a -> Proof a
internalAxiom (String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep [x] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[x]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"5") SBool
ax
     where pf :: SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e = Forall nm [x]
-> Forall an at
-> Forall bn bt
-> Forall cn ct
-> Forall dn dt
-> Forall en et
-> SBool
p (SBV [x] -> Forall nm [x]
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV [x]
xs) (SBV at -> Forall an at
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV at
a) (SBV bt -> Forall bn bt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV bt
b) (SBV ct -> Forall cn ct
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV ct
c) (SBV dt -> Forall dn dt
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV dt
d) (SBV et -> Forall en et
forall (nm :: Symbol) a. SBV a -> Forall nm a
Forall SBV et
e)
           ax :: SBool
ax              = [SBool] -> SBool
sAnd [ (Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\                       (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV [x]
forall a. SymVal a => SList a
SL.nil SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)
                                  , (Forall Any x
 -> Forall Any [x]
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV x
x) (Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e SBool -> SBool -> SBool
.=> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf (SBV x
x SBV x -> SBV [x] -> SBV [x]
forall a. SymVal a => SBV a -> SList a -> SList a
SL..: SBV [x]
xs) SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)]
                             SBool -> SBool -> SBool
.=>    (Forall Any [x]
 -> Forall Any at
 -> Forall Any bt
 -> Forall Any ct
 -> Forall Any dt
 -> Forall Any et
 -> SBool)
-> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool (\(Forall SBV [x]
xs) (Forall SBV at
a) (Forall SBV bt
b) (Forall SBV ct
c) (Forall SBV dt
d) (Forall SBV et
e) -> SBV [x] -> SBV at -> SBV bt -> SBV ct -> SBV dt -> SBV et -> SBool
pf SBV [x]
xs SBV at
a SBV bt
b SBV ct
c SBV dt
d SBV et
e)

-- | Accept the given definition as a fact. Usually used to introduce definitial axioms,
-- giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions,
-- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to
-- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.
axiom :: Proposition a => String -> a -> TP (Proof a)
axiom :: forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
nm a
p = do SMTConfig
cfg <- TP SMTConfig
getTPConfig
                TPUnique
u   <- TP TPUnique
tpGetNextUnique
                Int
_   <- IO Int -> TP Int
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TP Int) -> IO Int -> TP Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
True String
"Axiom" Int
0 (String -> [ProofObj] -> TPProofContext
TPProofOneShot String
nm [])
                let Proof ProofObj
iax = String -> a -> Proof a
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
nm a
p
                Proof a -> TP (Proof a)
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof a -> TP (Proof a)) -> Proof a -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj
iax { isUserAxiom = True, uniqId = u })

-- | Internal axiom generator; so we can keep truck of TP's trusted axioms, vs. user given axioms.
internalAxiom :: Proposition a => String -> a -> Proof a
internalAxiom :: forall a. Proposition a => String -> a -> Proof a
internalAxiom String
nm a
p = ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj -> Proof a) -> ProofObj -> Proof a
forall a b. (a -> b) -> a -> b
$ ProofObj { dependencies :: [ProofObj]
dependencies = []
                                      , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                                      , getObjProof :: SBool
getObjProof  = String -> SBool -> SBool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
p)
                                      , getProp :: Dynamic
getProp      = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
p
                                      , proofName :: String
proofName    = String
nm
                                      , uniqId :: TPUnique
uniqId       = TPUnique
TPInternal
                                      , isCached :: Bool
isCached     = Bool
False
                                      }

-- | Prove a lemma, using the given configuration
lemmaWith :: Proposition a => SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith cfg :: SMTConfig
cfg@SMTConfig{tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
printStats :: Bool
printStats :: TPOptions -> Bool
printStats}} String
nm a
inputProp [ProofObj]
by = String -> TP (Proof a) -> TP (Proof a)
forall a. Typeable a => String -> TP (Proof a) -> TP (Proof a)
withProofCache String
nm (TP (Proof a) -> TP (Proof a)) -> TP (Proof a) -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ do
                 TPState
tpSt <- TP TPState
getTPState
                 TPUnique
u    <- TP TPUnique
tpGetNextUnique
                 IO (Proof a) -> TP (Proof a)
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Proof a) -> TP (Proof a)) -> IO (Proof a) -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ Bool -> IO (Maybe UTCTime)
forall (m :: * -> *). MonadIO m => Bool -> m (Maybe UTCTime)
getTimeStampIf Bool
printStats IO (Maybe UTCTime)
-> (Maybe UTCTime -> IO (Proof a)) -> IO (Proof a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SMTConfig -> SymbolicT IO (Proof a) -> IO (Proof a)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
cfg (SymbolicT IO (Proof a) -> IO (Proof a))
-> (Maybe UTCTime -> SymbolicT IO (Proof a))
-> Maybe UTCTime
-> IO (Proof a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPState -> TPUnique -> Maybe UTCTime -> SymbolicT IO (Proof a)
forall {m :: * -> *} {a}.
(ExtractIO m, MonadSymbolic (QueryT m),
 QSaturate (SymbolicT m) a) =>
TPState -> TPUnique -> Maybe UTCTime -> SymbolicT m (Proof a)
go TPState
tpSt TPUnique
u
  where go :: TPState -> TPUnique -> Maybe UTCTime -> SymbolicT m (Proof a)
go TPState
tpSt TPUnique
u Maybe UTCTime
mbStartTime = do a -> SymbolicT m ()
forall (m :: * -> *) a.
(Monad m, MonadIO m, SolverContext m, QSaturate m a) =>
a -> m ()
qSaturateSavingObservables a
inputProp
                                   (ProofObj -> SymbolicT m ()) -> [ProofObj] -> SymbolicT m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SBool -> SymbolicT m ()
forall a. QuantifiedBool a => a -> SymbolicT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT m ())
-> (ProofObj -> SBool) -> ProofObj -> SymbolicT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofObj -> SBool
getObjProof) [ProofObj]
by
                                   QueryT m (Proof a) -> SymbolicT m (Proof a)
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
query (QueryT m (Proof a) -> SymbolicT m (Proof a))
-> QueryT m (Proof a) -> SymbolicT m (Proof a)
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO (Proof a))
-> QueryT m (Proof a)
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m,
 Proposition a) =>
SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg TPState
tpSt String
"Lemma" Int
0 (String -> [ProofObj] -> TPProofContext
TPProofOneShot String
nm [ProofObj]
by) Maybe SBool
forall a. Maybe a
Nothing a
inputProp [] (Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> IO (Proof a)
forall {m :: * -> *} {a}.
MonadIO m =>
Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> m (Proof a)
good Maybe UTCTime
mbStartTime TPUnique
u)

        -- What to do if all goes well
        good :: Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> m (Proof a)
good Maybe UTCTime
mbStart TPUnique
u (Int, Maybe NominalDiffTime)
d = do Maybe NominalDiffTime
mbElapsed <- Maybe UTCTime -> m (Maybe NominalDiffTime)
forall (m :: * -> *).
MonadIO m =>
Maybe UTCTime -> m (Maybe NominalDiffTime)
getElapsedTime Maybe UTCTime
mbStart
                              IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishTP SMTConfig
cfg (String
"Q.E.D." String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> String
concludeModulo [ProofObj]
by) (Int, Maybe NominalDiffTime)
d ([NominalDiffTime] -> IO ()) -> [NominalDiffTime] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Maybe NominalDiffTime] -> [NominalDiffTime]
forall a. [Maybe a] -> [a]
catMaybes [Maybe NominalDiffTime
mbElapsed]
                              Proof a -> m (Proof a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof a -> m (Proof a)) -> Proof a -> m (Proof a)
forall a b. (a -> b) -> a -> b
$ ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj -> Proof a) -> ProofObj -> Proof a
forall a b. (a -> b) -> a -> b
$ ProofObj { dependencies :: [ProofObj]
dependencies = [ProofObj]
by
                                                      , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                                                      , getObjProof :: SBool
getObjProof  = String -> SBool -> SBool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
inputProp)
                                                      , getProp :: Dynamic
getProp      = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
inputProp
                                                      , proofName :: String
proofName    = String
nm
                                                      , uniqId :: TPUnique
uniqId       = TPUnique
u
                                                      , isCached :: Bool
isCached     = Bool
False
                                                      }

-- | Prove a given statement, using auxiliaries as helpers. Using the default solver.
lemma :: Proposition a => String -> a -> [ProofObj] -> TP (Proof a)
lemma :: forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
nm a
f [ProofObj]
by = do SMTConfig
cfg <- TP SMTConfig
getTPConfig
                   SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
forall a.
Proposition a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith SMTConfig
cfg String
nm a
f [ProofObj]
by

-- | Prove a given statement, using the induction schema for the proposition. Using the default solver.
inductiveLemma :: Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma :: forall a. Inductive a => String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemma String
nm a
f [ProofObj]
by = do SMTConfig
cfg <- TP SMTConfig
getTPConfig
                            SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
forall a.
Inductive a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemmaWith SMTConfig
cfg String
nm a
f [ProofObj]
by

-- | Prove a given statement, using the induction schema for the proposition. Using the default solver.
inductiveLemmaWith :: Inductive a => SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemmaWith :: forall a.
Inductive a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
inductiveLemmaWith SMTConfig
cfg String
nm a
f [ProofObj]
by = SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
forall a.
Proposition a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith SMTConfig
cfg String
nm a
f (a -> ProofObj
forall a. HasInductionSchema a => a -> ProofObj
inductionSchema a
f ProofObj -> [ProofObj] -> [ProofObj]
forall a. a -> [a] -> [a]
: [ProofObj]
by)

-- | Capture the general flow of a proof-step. Note that this is the only point where we call the backend solver
-- in a TP proof.
smtProofStep :: (SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m, Proposition a)
   => SMTConfig                              -- ^ config
   -> TPState                                -- ^ TPState
   -> String                                 -- ^ tag
   -> Int                                    -- ^ level
   -> TPProofContext                         -- ^ the context in which we're doing the proof
   -> Maybe SBool                            -- ^ Assumptions under which we do the check-sat. If there's one we'll push/pop
   -> a                                      -- ^ what we want to prove
   -> [(String, SVal)]                       -- ^ Values to display in case of failure
   -> ((Int, Maybe NominalDiffTime) -> IO r) -- ^ what to do when unsat, with the tab amount and time elapsed (if asked)
   -> m r
smtProofStep :: forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m,
 Proposition a) =>
SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep cfg :: SMTConfig
cfg@SMTConfig{Bool
verbose :: Bool
verbose :: SMTConfig -> Bool
verbose, tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
printStats :: TPOptions -> Bool
printStats :: Bool
printStats}} TPState
tpState String
tag Int
level TPProofContext
ctx Maybe SBool
mbAssumptions a
prop [(String, SVal)]
disps (Int, Maybe NominalDiffTime) -> IO r
unsat = do

        case Maybe SBool
mbAssumptions of
           Maybe SBool
Nothing  -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; smtProofStep: No context value to push."]
                          m r
check
           Just SBool
asm -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; smtProofStep: Pushing in the context: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBool -> String
forall a. Show a => a -> String
show SBool
asm]
                          m r -> m r
forall (m :: * -> *) a. (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain SBool
asm
                                                   m r
check

 where check :: m r
check = do
           Int
tab <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> m Int) -> IO Int -> m Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
verbose String
tag Int
level TPProofContext
ctx

           -- It's tempting to skolemize here.. But skolemization creates fresh constants
           -- based on the name given, and they mess with all else. So, don't skolemize!
           SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
prop)

           (Maybe NominalDiffTime
mbT, CheckSatResult
r) <- Bool
-> m CheckSatResult -> m (Maybe NominalDiffTime, CheckSatResult)
forall (m :: * -> *) a.
MonadIO m =>
Bool -> m a -> m (Maybe NominalDiffTime, a)
timeIf Bool
printStats m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

           TPState -> (TPStats -> TPStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
TPState -> (TPStats -> TPStats) -> m ()
updStats TPState
tpState (\TPStats
s -> TPStats
s{noOfCheckSats = noOfCheckSats s + 1})

           case Maybe NominalDiffTime
mbT of
             Maybe NominalDiffTime
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
             Just NominalDiffTime
t  -> TPState -> (TPStats -> TPStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
TPState -> (TPStats -> TPStats) -> m ()
updStats TPState
tpState (\TPStats
s -> TPStats
s{solverElapsed = solverElapsed s + t})

           case CheckSatResult
r of
             CheckSatResult
Unk    -> m r
forall {b}. m b
unknown
             CheckSatResult
Sat    -> m r
forall {b}. m b
cex
             DSat{} -> m r
forall {b}. m b
cex
             CheckSatResult
Unsat  -> IO r -> m r
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO r -> m r) -> IO r -> m r
forall a b. (a -> b) -> a -> b
$ (Int, Maybe NominalDiffTime) -> IO r
unsat (Int
tab, Maybe NominalDiffTime
mbT)

       die :: a
die = String -> a
forall a. HasCallStack => String -> a
error String
"Failed"

       fullNm :: String
fullNm = case TPProofContext
ctx of
                  TPProofOneShot       String
s [ProofObj]
_    -> String
s
                  TPProofStep    Bool
True  String
s [String]
_ [String]
ss -> String
"assumptions for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ss)
                  TPProofStep    Bool
False String
s [String]
_ [String]
ss ->                       String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ss)

       unknown :: m b
unknown = do SMTReasonUnknown
r <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                    IO b -> m b
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO b -> m b) -> IO b -> m b
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fullNm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
                                String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Solver reported: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
r
                                IO b
forall {a}. a
die

       -- What to do if the proof fails
       cex :: m b
cex = do
         IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fullNm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

         SMTResult
res <- case TPProofContext
ctx of
                  TPProofStep{} -> do ((String, SVal) -> m ()) -> [(String, SVal)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> SVal -> m ()) -> (String, SVal) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => String -> SVal -> m ()
sObserve) [(String, SVal)]
disps
                                      SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                  TPProofOneShot String
_ [ProofObj]
by ->
                     -- When trying to get a counter-example not in query mode, we
                     -- do a skolemized sat call, which gets better counter-examples.
                     -- We only include the those facts that are user-given axioms. This
                     -- way our counter-example will be more likely to be relevant
                     -- to the proposition we're currently proving. (Hopefully.)
                     -- Remember that we first have to negate, and then skolemize!
                     do SatResult SMTResult
res <- IO SatResult -> m SatResult
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SatResult -> m SatResult) -> IO SatResult -> m SatResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
cfg (Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult)
-> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
                                           a -> SymbolicT IO ()
forall (m :: * -> *) a.
(Monad m, MonadIO m, SolverContext m, QSaturate m a) =>
a -> m ()
qSaturateSavingObservables a
prop
                                           (SBool -> SymbolicT IO ()) -> [SBool] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain [SBool
getObjProof | ProofObj{Bool
isUserAxiom :: ProofObj -> Bool
isUserAxiom :: Bool
isUserAxiom, SBool
getObjProof :: ProofObj -> SBool
getObjProof :: SBool
getObjProof} <- [ProofObj]
by, Bool
isUserAxiom] :: Symbolic ()
                                           ((String, SVal) -> SymbolicT IO ())
-> [(String, SVal)] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> SVal -> SymbolicT IO ())
-> (String, SVal) -> SymbolicT IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SVal -> SymbolicT IO ()
forall (m :: * -> *). MonadSymbolic m => String -> SVal -> m ()
sObserve) [(String, SVal)]
disps
                                           SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a)))
-> SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a b. (a -> b) -> a -> b
$ NegatesTo a -> SkolemsTo (NegatesTo a)
forall a.
(Skolemize a, Constraint Symbolic (SkolemsTo a), Skolemize a) =>
a -> SkolemsTo a
skolemize (a -> NegatesTo a
forall a. QNot a => a -> NegatesTo a
qNot a
prop)
                        SMTResult -> m SMTResult
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SMTResult
res

         IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ ThmResult -> IO ()
forall a. Show a => a -> IO ()
print (ThmResult -> IO ()) -> ThmResult -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTResult -> ThmResult
ThmResult SMTResult
res

         m b
forall {a}. a
die