Update cryptol submodule and adapt to changes.

The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
GaloisInc · Mar 3, 2021 · bae01f6 · bae01f6
1 parent 9004724
commit bae01f6
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 6 deletions.
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -24,7 +24,7 @@ import Data.Traversable (for)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
-import Cryptol.ModuleSystem.Env (ModuleEnv)
+import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
 import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
 import qualified Cryptol.ModuleSystem.Renamer as MR
@@ -33,6 +33,7 @@ import qualified Cryptol.Parser as CP
 import Cryptol.Parser.Position (emptyRange, getLoc)
 import Cryptol.TypeCheck (tcExpr)
 import Cryptol.TypeCheck.Monad (InferOutput(..), inpVars, inpTSyns)
+import Cryptol.TypeCheck.Solver.SMT (withSolver)
 import Cryptol.Utils.Ident (interactiveName)
 import Cryptol.Utils.Logger (quietLogger)
 import Cryptol.Utils.PP
@@ -64,7 +65,9 @@ getTypedTermOfCExp fileReader sc cenv expr =
   do let ?fileReader = fileReader
      let env = eModuleEnv cenv
      let minp = ModuleInput True (pure defaultEvalOpts) B.readFile env
-     mres <- runModuleM minp $
+     mres <-
+       withSolver (meSolverConfig env) $ \s ->
+       runModuleM (minp s) $
        do npe <- interactive (noPat expr) -- eliminate patterns
 
           -- resolve names

diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs
@@ -435,7 +435,8 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
 
       cryptolAbstractNamesSAW :: [SAWScript.LName] -> Cryptol.Expr Cryptol.PName -> Cryptol.Expr Cryptol.PName
       cryptolAbstractNamesSAW names expr =
-         Cryptol.EFun (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
+         Cryptol.EFun Cryptol.emptyFunDesc
+         (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
 
       cryptolApplyFunctionSAW :: SAWScript.LName -> [SAWScript.LName] -> Cryptol.Expr Cryptol.PName
       cryptolApplyFunctionSAW function args =

diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -22,6 +22,7 @@ import Cryptol.ModuleSystem.Name
 import Cryptol.Utils.Ident (unpackIdent)
 import Cryptol.Utils.Logger (quietLogger)
 import qualified Cryptol.TypeCheck.AST as AST
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP
 
 -- | Parse a Cryptol module into a list of declarations
@@ -31,7 +32,9 @@ getDeclsCryptol path = do
    let evalOpts = EvalOpts quietLogger defaultPPOpts
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
-   (result, warnings) <- M.loadModuleByPath path minp
+   (result, warnings) <-
+     SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
+     M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
       case result of
+6 −5		cryptol-remote-api/cryptol-eval-server/Main.hs
+6 −1		src/Cryptol/Backend/Monad.hs
+4 −3		src/Cryptol/ModuleSystem/Base.hs
+8 −0		src/Cryptol/ModuleSystem/Monad.hs
+9 −3		src/Cryptol/ModuleSystem/Renamer.hs
+1 −1		src/Cryptol/Parser.y
+18 −3		src/Cryptol/Parser/AST.hs
+2 −2		src/Cryptol/Parser/Names.hs
+23 −13		src/Cryptol/Parser/NoPat.hs
+2 −2		src/Cryptol/Parser/ParserUtils.hs
+5 −2		src/Cryptol/REPL/Command.hs
+2 −0		src/Cryptol/TypeCheck.hs
+16 −6		src/Cryptol/TypeCheck/Error.hs
+14 −9		src/Cryptol/TypeCheck/Infer.hs
+1 −0		src/Cryptol/TypeCheck/InferTypes.hs
+3 −3		src/Cryptol/TypeCheck/Instantiate.hs
+1 −1		src/Cryptol/TypeCheck/Kind.hs
+46 −13		src/Cryptol/TypeCheck/Monad.hs
+22 −19		src/Cryptol/TypeCheck/Solver/SMT.hs
+24 −10		src/Cryptol/TypeCheck/Type.hs
+4 −4		tests/issues/T146.icry.stdout
+4 −0		tests/issues/issue1024.icry
+27 −0		tests/issues/issue1024.icry.stdout
+5 −0		tests/issues/issue1024a.cry
+5 −0		tests/issues/issue1024b.cry
+2 −2		tests/issues/issue290v2.icry.stdout
+5 −0		tests/issues/issue567.icry
+27 −0		tests/issues/issue567.icry.stdout
+2 −2		tests/issues/issue723.icry.stdout
+8 −8		tests/regression/specialize.icry.stdout
+4 −4		tests/regression/tc-errors.icry.stdout
+7 −4		utils/CryHtml.hs
+7 −2		cryptol-saw-core/css/Main.hs
+29 −3		cryptol-saw-core/saw/Cryptol.sawcore
+9 −1		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+9 −6		cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs