Remove unnecessary calls to mkTypedTerm.

This is a step toward fixing #718. The use of mkTypedTerm is redundant in these cases in the SAWScript.Prover modules, as the computed schema in all cases is only used to check that the return type is Bool, and the prior calls to `propToPredicate` already ensure that.
GaloisInc · May 19, 2020 · f7bb948 · f7bb948
1 parent eeef9a1
commit f7bb948
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 20 deletions.
diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs
@@ -4,15 +4,14 @@ module SAWScript.Prover.ABC (proveABC) where
 import qualified Data.AIG as AIG
 
 import           Verifier.SAW.SharedTerm
-import           Verifier.SAW.TypedTerm
 import           Verifier.SAW.FiniteValue
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
 import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
 import SAWScript.Prover.Rewrite(rewriteEqs)
 import SAWScript.Prover.Util
-         (liftCexBB, bindAllExts, checkBooleanSchema)
+         (liftCexBB, bindAllExts)
 
 -- | Bit-blast a proposition and check its validity using ABC.
 proveABC ::
@@ -23,9 +22,7 @@ proveABC ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveABC proxy sc goal =
   do t0 <- propToPredicate sc goal
-     TypedTerm schema t <-
-        (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc)
-     checkBooleanSchema schema
+     t <- bindAllExts sc t0 >>= rewriteEqs sc
      BBSim.withBitBlastedPred proxy sc mempty t $
       \be lit0 shapes ->
          do let lit = AIG.not lit0

diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs
@@ -7,7 +7,6 @@ import Verifier.SAW.FiniteValue
 
 import qualified Verifier.SAW.Simulator.RME as RME
 import qualified Verifier.SAW.Simulator.RME.Base as RME
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
@@ -22,9 +21,7 @@ proveRME ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveRME sc goal =
   do t0 <- propToPredicate sc goal
-     TypedTerm schema t <-
-        bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc
-     checkBooleanSchema schema
+     t <- bindAllExts sc t0 >>= rewriteEqs sc
      tp <- scWhnf sc =<< scTypeOf sc t
      let (args, _) = asPiList tp
          argNames = map fst args

diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs
@@ -20,14 +20,11 @@ import qualified Verifier.SAW.Simulator.SBV as SBVSim
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPi, asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Rewrite(rewriteEqs)
-import SAWScript.Prover.Util(checkBooleanSchema)
-
 
 
 -- | Bit-blast a proposition and check its validity using SBV.
@@ -93,10 +90,8 @@ prepNegatedSBV sc unints goal =
      let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
      exts <- filterM nonFun (getAllExts t0)
 
-     TypedTerm schema t' <-
-         scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc
+     t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-     checkBooleanSchema schema
      (labels, lit) <- SBVSim.sbvSolve sc mempty unints t'
      let lit' = liftM SBV.svNot lit
      return (t', labels, lit')

diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
@@ -13,13 +13,11 @@ import           Data.Maybe (catMaybes)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
 
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPi)
 
 import           SAWScript.Proof(Prop, propToPredicate)
 import           SAWScript.Prover.Rewrite(rewriteEqs)
 import           SAWScript.Prover.SolverStats
-import           SAWScript.Prover.Util
 
 import Data.Parameterized.Nonce
 
@@ -119,10 +117,8 @@ prepWhat4 sym sc unints t0 = do
   let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
   exts <- filterM nonFun (getAllExts t0)
 
-  TypedTerm schema t' <-
-      scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc
+  t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-  checkBooleanSchema schema
   (argNames, lit) <- W.w4Solve sym sc mempty unints t'
   return (t', argNames, lit)