From f7bb9487146af501f255b5a90d8c737a8c12c81c Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Sun, 17 May 2020 17:31:43 -0700
Subject: [PATCH] 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.
---
 src/SAWScript/Prover/ABC.hs   | 7 ++-----
 src/SAWScript/Prover/RME.hs   | 5 +----
 src/SAWScript/Prover/SBV.hs   | 7 +------
 src/SAWScript/Prover/What4.hs | 6 +-----
 4 files changed, 5 insertions(+), 20 deletions(-)

diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs
index 50e9820731..a7a8bad4d2 100644
--- a/src/SAWScript/Prover/ABC.hs
+++ b/src/SAWScript/Prover/ABC.hs
@@ -4,7 +4,6 @@ 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
 
@@ -12,7 +11,7 @@ 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
index 6ee3f784e7..c4f8f0a5d5 100644
--- 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
index 83dd7b8347..4b5095970e 100644
--- 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
index 772ec75c54..1945a97e11 100644
--- 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)