Remove 'rewritingSharedContext' and related code.

Author: brianhuffman

otherTests/saw-core/Tests.hs

@@ -20,7 +20,6 @@ import Data.Proxy
 import Tests.CacheTests
 import Tests.Parser
 import Tests.SharedTerm
-import Tests.Rewriter
 import Tests.Functor
 
 main :: IO ()
@@ -41,7 +40,6 @@ tests =
    testGroup "SAWCore"
    [ testGroup "SharedTerm" sharedTermTests
    , testGroup "Parser" parserTests
-   , testGroup "Rewriter" rewriter_tests
    , testGroup "Cache" cacheTests
    , testGroup "Functor" functorTests
    ]

otherTests/saw-core/Tests/Rewriter.hs

@@ -52,9 +52,7 @@ module SAWCore.Rewriter
   , rewriteSharedTermTypeSafe
   -- * Matching
   , scMatch
-  -- * SharedContext
-  , rewritingSharedContext
-
+  -- * Miscellaneous
   , replaceTerm
   , hoistIfs
   ) where
@@ -865,40 +863,6 @@ rewriteSharedTermTypeSafe sc ss t0 =
         Nothing -> apply rules t
         Just tb -> rewriteAll =<< runTermBuilder tb (scGlobalDef sc) (scTermF sc)
 
--- | Generate a new SharedContext that normalizes terms as it builds them.
---   Rule annotations are ignored.
-rewritingSharedContext :: SharedContext -> Simpset a -> SharedContext
-rewritingSharedContext sc ss = sc'
-  where
-    sc' = sc { scTermF = rewriteTop }
-
-    rewriteTop :: TermF Term -> IO Term
-    rewriteTop tf =
-      case asPairRedex t of
-        Just t' -> return t'
-        Nothing ->
-          case asRecordRedex t of
-            Just t' -> return t'
-            Nothing -> apply (Net.match_term ss t) t
-      where t = Unshared tf
-
-    apply :: [Either (RewriteRule a) Conversion] ->
-             Term -> IO Term
-    apply [] (Unshared tf) = scTermF sc tf
-    apply [] STApp{ stAppTermF = tf } = scTermF sc tf
-    apply (Left (RewriteRule c l r _ _shallow _ann) : rules) t =
-      case firstOrderMatch c l t of
-        Nothing -> apply rules t
-        Just inst
-          | l == r ->
-            do putStrLn $ "rewritingSharedContext: skipping reflexive rule: " ++ scPrettyTerm PPS.defaultOpts l
-               apply rules t
-          | otherwise -> scInstantiateExt sc' inst r
-    apply (Right conv : rules) t =
-      case runConversion conv t of
-        Nothing -> apply rules t
-        Just tb -> runTermBuilder tb (scGlobalDef sc) (scTermF sc')
-
 
 -- FIXME: is there some way to have sensable term replacement in the presence of loose variables
 --  and/or under binders?

saw-core/src/SAWCore/Rewriter.hs

@@ -102,11 +102,10 @@ import qualified SAWCentral.Yosys as Yo (YosysIR)
 import qualified SAWCentral.Yosys.State as Yo (YosysSequential)
 import qualified SAWCentral.Yosys.Theorem as Yo (YosysImport, YosysTheorem)
 
-import SAWCore.Conversion
-import SAWCore.Module (Def(..), emptyModule, moduleDefs)
-import SAWCore.Name (mkModuleName, Name(..))
+import SAWCore.Module (emptyModule)
+import SAWCore.Name (mkModuleName)
 import SAWCore.Prim (rethrowEvalError)
-import SAWCore.Rewriter (emptySimpset, rewritingSharedContext, scSimpset)
+import SAWCore.Rewriter (emptySimpset)
 import SAWCore.SharedTerm
 import qualified CryptolSAWCore.CryptolEnv as CEnv
 
@@ -1009,31 +1008,11 @@ buildTopLevelEnv :: AIGProxy
                  -> IO (BuiltinContext, TopLevelRO, TopLevelRW)
 buildTopLevelEnv proxy opts scriptArgv =
     do let mn = mkModuleName ["SAWScript"]
-       sc0 <- mkSharedContext
+       sc <- mkSharedContext
        let ?fileReader = BS.readFile
-       CryptolSAW.scLoadPreludeModule sc0
-       CryptolSAW.scLoadCryptolModule sc0
-       scLoadModule sc0 (emptyModule mn)
-       cryptol_mod <- scFindModule sc0 $ mkModuleName ["Cryptol"]
-       let convs = natConversions
-                   ++ bvConversions
-                   ++ vecConversions
-                   ++ [ tupleConversion
-                      , recordConversion
-                      , remove_ident_coerce
-                      , remove_ident_unsafeCoerce
-                      ]
-           cryptolDefs = filter defPred $ moduleDefs cryptol_mod
-           defPred d =
-             case nameInfo (defName d) of
-               ModuleIdentifier ident -> ident `Set.member` includedDefs
-               ImportedName{} -> False
-           includedDefs = Set.fromList
-                          [ "Cryptol.ecDemote"
-                          , "Cryptol.seq"
-                          ]
-       simps <- scSimpset sc0 cryptolDefs [] convs
-       let sc = rewritingSharedContext sc0 simps
+       CryptolSAW.scLoadPreludeModule sc
+       CryptolSAW.scLoadCryptolModule sc
+       scLoadModule sc (emptyModule mn)
        ss <- basic_ss sc
        currDir <- getCurrentDirectory
        mb_cache <- lookupEnv "SAW_SOLVER_CACHE_PATH" >>= \case

saw-script/src/SAWScript/Interpreter.hs

@@ -990,7 +990,6 @@ test-suite saw-core-tests
     Tests.CacheTests
     Tests.Functor
     Tests.Parser
-    Tests.Rewriter
     Tests.SharedTerm