Update saw-remote-api with Simpset changes.

TODO! We currently are allowing users to create simpsets from
raw terms, and probably we should only let `Theorem` values
be turned into rewrite rules.

saw-remote-api/src/SAWServer.hs

@@ -52,10 +52,9 @@ import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModu
 import SAWScript.Options (defaultOptions)
 import SAWScript.Position (Pos(..))
 import SAWScript.Prover.Rewrite (basic_ss)
-import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts)
+import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts, SAWSimpset)
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
-import Verifier.SAW.Rewriter (Simpset)
 import qualified Cryptol.Utils.Ident as Cryptol
 
 import qualified Argo
@@ -275,7 +274,7 @@ data CrucibleSetupTypeRepr :: Type -> Type where
 
 data ServerVal
   = VTerm TypedTerm
-  | VSimpset Simpset
+  | VSimpset SAWSimpset
   | VType Cryptol.Schema
   | VCryptolModule CryptolModule -- from SAW, includes Term mappings
   | VJVMClass JSS.Class
@@ -305,7 +304,7 @@ class IsServerVal a where
 instance IsServerVal TypedTerm where
   toServerVal = VTerm
 
-instance IsServerVal Simpset where
+instance IsServerVal SAWSimpset where
   toServerVal = VSimpset
 
 instance IsServerVal Cryptol.Schema where
@@ -402,7 +401,7 @@ getLLVMMethodSpecIR n =
        VLLVMMethodSpecIR ir -> return ir
        _other -> Argo.raise (notAnLLVMMethodSpecIR n)
 
-getSimpset :: ServerName -> Argo.Command SAWState Simpset
+getSimpset :: ServerName -> Argo.Command SAWState SAWSimpset
 getSimpset n =
   do v <- getServerVal n
      case v of

saw-remote-api/src/SAWServer/ProofScript.hs

@@ -154,7 +154,7 @@ makeSimpset params = do
         v <- getServerVal n
         case v of
           VSimpset ss' -> return (merge ss ss')
-          VTerm t -> return (addSimp (ttTerm t) ss)
+          VTerm t -> return (addSimp (ttTerm t) Nothing ss) -- TODO! making rewrite rules from terms!
           _ -> Argo.raise (notASimpset n)
   ss <- foldM add emptySimpset (ssElements params)
   setServerVal (ssResult params) ss