Make checkpoint somewhat less broken. This change causes the

`NameSeeds` value used internally by Cryptol to be carried forward
across checkpoints.  This prevents internal nonce values from being
reused, which, in turn, avoids errors about registering duplicate
names.

It is unclear if this is the correct long-term fix, but it allows
checkpoint to work more reliably when importing Cryptol modules
or using `let {{ ... }}` constructs.

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -16,6 +16,7 @@ module Verifier.SAW.CryptolEnv
   , loadCryptolModule
   , bindCryptolModule
   , lookupCryptolModule
+  , combineCryptolEnv
   , importModule
   , bindTypedTerm
   , bindType
@@ -342,6 +343,15 @@ genTermEnv sc modEnv cryEnv0 = do
 
 --------------------------------------------------------------------------------
 
+
+combineCryptolEnv :: CryptolEnv -> CryptolEnv -> IO CryptolEnv
+combineCryptolEnv chkEnv newEnv =
+  do let newMEnv = eModuleEnv newEnv
+     let chkMEnv = eModuleEnv chkEnv
+     let menv' = chkMEnv{ ME.meNameSeeds = ME.meNameSeeds newMEnv }
+     return chkEnv{ eModuleEnv = menv' }
+
+
 checkNotParameterized :: T.Module -> IO ()
 checkNotParameterized m =
   when (T.isParametrizedModule m) $

src/SAWScript/Value.hs

@@ -568,15 +568,39 @@ io f = (TopLevel_ (liftIO f))
       do pos <- getPosition
          rethrow (SS.TopLevelException pos ("Error in x86 code: " ++ s))
 
+
+
+
+combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW
+combineRW (TopLevelCheckpoint chk) rw =
+  do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw)
+     return chk{ rwCryptol = cenv' }
+
+-- | Represents the mutable state of the TopLevel monad
+--   that can later be restored.
+newtype TopLevelCheckpoint =
+  TopLevelCheckpoint TopLevelRW
+
+makeCheckpoint :: TopLevel TopLevelCheckpoint
+makeCheckpoint =
+  do rw <- getTopLevelRW
+     return (TopLevelCheckpoint rw)
+
+restoreCheckpoint :: TopLevelCheckpoint -> TopLevel ()
+restoreCheckpoint chk =
+  do rw <- getTopLevelRW
+     rw' <- io (combineRW chk rw)
+     putTopLevelRW rw'
+
 -- | Capture the current state of the TopLevel monad
 --   and return an action that, if invoked, resets
 --   the state back to that point.
 checkpoint :: TopLevel (() -> TopLevel ())
 checkpoint =
-  do rw <- getTopLevelRW
+  do chk <- makeCheckpoint
      return $ \_ ->
        do printOutLnTop Info "Restoring state from checkpoint"
-          putTopLevelRW rw
+          restoreCheckpoint chk
 
 throwTopLevel :: String -> TopLevel a
 throwTopLevel msg = do