interpreter: Now that the Cryptol is scoped, it needs to be in Environ.

That causes it to get closed in along with the SAWScript environments
in lambdas and do-blocks. Otherwise, the Cryptol-level values for
SAWScript function arguments mysteriously disappear except (due to
implementation quirks) when they're associated with the last argument
of a function.

Note that the SAWCore environment really properly speaking needs a
similar treatment, but we can't currently. The result is that in
obscure cases (e.g. test03.saw in test2304) uses of the same variable
name in what should be distinct places cause a duplicate definition
error.

For the moment, we're going to hope that these cases are all
sufficiently obscure that nobody trips on them, and track the issue in

Author: sauclovian-g

intTests/test2304/test04.log.good

@@ -3,11 +3,5 @@
   \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P)
  ("b",\(u1218 : isort 0) ->
   \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P)
- Stack trace:
-   (builtin) in h
-   test04.saw:11:6-11:9 (at top level)
-Cryptol error:
-[error] at test04.saw:3:38--3:39
-    Type not in scope: x
-
-FAILED
+ ("c",\(u1218 : isort 0) ->
+  \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P)

intTests/test2304/test05.log.good

@@ -1,9 +1,7 @@
  Loading file "test05.saw"
- Stack trace:
-   (builtin) in f
-   test05.saw:5:9-5:14 (at top level)
-Cryptol error:
-[error] at test05.saw:1:39--1:40
-    Type not in scope: x
-
-FAILED
+ ("a",\(u1218 : isort 0) ->
+  \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P)
+ ("b",\(u1218 : isort 0) ->
+  \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P)
+ ("c",\(u1218 : isort 0) ->
+  \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P)

saw-central/src/SAWCentral/Builtins.hs

@@ -1706,7 +1706,7 @@ envCmd :: TopLevel ()
 envCmd = do
   opts <- getOptions
   avail <- gets rwPrimsAvail
-  SV.Environ varenv _tyenv <- gets rwEnviron
+  SV.Environ varenv _tyenv _cryenv <- gets rwEnviron
   rbenv <- gets rwRebindables
 
   -- print rebindables first if there are any
@@ -2093,28 +2093,30 @@ cryptol_prims = CryptolModule Map.empty <$> Map.fromList <$> traverse parsePrim
     parsePrim :: (Text, Ident, Text) -> TopLevel (C.Name, TypedTerm)
     parsePrim (n, i, s) = do
       sc <- getSharedContext
-      rw <- getTopLevelRW
-      let SV.CryptolScopeStack (cenv :| cenvs) = rwCryptol rw
+      SV.Environ varenv tyenv cryenv <- gets rwEnviron
+      let SV.CryptolScopeStack (cenv :| cenvs) = cryenv
       unless (null cenvs) $ do
           fail "cryptol_prims is an import operation and may not be done in a nested block"
       let mname = C.packModName ["Prims"]
       let ?fileReader = StrictBS.readFile
       (n', cenv') <- io $ CEnv.declareName cenv mname n
       s' <- io $ CEnv.parseSchema cenv' (noLoc s)
       t' <- io $ scGlobalDef sc i
-      putTopLevelRW $ rw { rwCryptol = SV.CryptolScopeStack (cenv' :| cenvs) }
+      let cryenv' = SV.CryptolScopeStack (cenv' :| cenvs)
+      modify (\rw -> rw { rwEnviron = SV.Environ varenv tyenv cryenv' })
       return (n', TypedTerm (TypedTermSchema s') t')
 
 cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CryptolModule
 cryptol_load fileReader path = do
   sc <- getSharedContext
-  rw <- getTopLevelRW
-  let SV.CryptolScopeStack (ce :| ces) = rwCryptol rw
+  SV.Environ varenv tyenv cryenv <- gets rwEnviron
+  let SV.CryptolScopeStack (ce :| ces) = cryenv
   unless (null ces) $ do
       fail "cryptol_load is an import operation and is not permitted in nested blocks"
   let ?fileReader = fileReader
   (m, ce') <- io $ CEnv.loadCryptolModule sc ce path
-  putTopLevelRW $ rw { rwCryptol = SV.CryptolScopeStack (ce' :| ces) }
+  let cryenv' = SV.CryptolScopeStack (ce' :| ces)
+  modify (\rw -> rw { rwEnviron = SV.Environ varenv tyenv cryenv' })
   return m
 
 -- XXX: This is kind of a top-level style operation; should it be
@@ -2124,35 +2126,37 @@ cryptol_load fileReader path = do
 -- of the environment closed in with lambdas and do-blocks, so that's
 -- probably a bad idea.)
 cryptol_add_path :: FilePath -> TopLevel ()
-cryptol_add_path path =
-  do rw <- getTopLevelRW
-     let SV.CryptolScopeStack (ce :| ces) = rwCryptol rw
+cryptol_add_path path = do
+     SV.Environ varenv tyenv cryenv <- gets rwEnviron
+     let SV.CryptolScopeStack (ce :| ces) = cryenv
      let me = CEnv.eModuleEnv ce
      let me' = me { C.meSearchPath = path : C.meSearchPath me }
      let ce' = ce { CEnv.eModuleEnv = me' }
-     let rw' = rw { rwCryptol = SV.CryptolScopeStack (ce' :| ces) }
-     putTopLevelRW rw'
+     let cryenv' = SV.CryptolScopeStack (ce' :| ces)
+     modify (\rw -> rw { rwEnviron = SV.Environ varenv tyenv cryenv' })
 
 cryptol_add_prim :: Text -> Text -> TypedTerm -> TopLevel ()
-cryptol_add_prim mnm nm trm =
-  do rw <- getTopLevelRW
-     let SV.CryptolScopeStack (env :| envs) = rwCryptol rw
+cryptol_add_prim mnm nm trm = do
+     SV.Environ varenv tyenv cryenv <- gets rwEnviron
+     let SV.CryptolScopeStack (env :| envs) = cryenv
      let prim_name =
            C.PrimIdent (C.textToModName mnm) nm
      let env' =
            env { CEnv.ePrims =
                    Map.insert prim_name (ttTerm trm) (CEnv.ePrims env) }
-     putTopLevelRW (rw { rwCryptol = SV.CryptolScopeStack (env' :| envs) })
+     let cryenv' = SV.CryptolScopeStack (env' :| envs)
+     modify (\rw -> rw { rwEnviron = SV.Environ varenv tyenv cryenv' })
 
 cryptol_add_prim_type :: Text -> Text -> TypedTerm -> TopLevel ()
-cryptol_add_prim_type mnm nm tp =
-  do rw <- getTopLevelRW
-     let SV.CryptolScopeStack (env :| envs) = rwCryptol rw
+cryptol_add_prim_type mnm nm tp = do
+     SV.Environ varenv tyenv cryenv <- gets rwEnviron
+     let SV.CryptolScopeStack (env :| envs) = cryenv
      let prim_name =
            C.PrimIdent (C.textToModName mnm) nm
      let env' = env { CEnv.ePrimTypes =
                         Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes env) }
-     putTopLevelRW (rw { rwCryptol = SV.CryptolScopeStack (env' :| envs) })
+     let cryenv' = SV.CryptolScopeStack (env' :| envs)
+     modify (\rw -> rw { rwEnviron = SV.Environ varenv tyenv cryenv' })
 
 -- | Call 'Cryptol.importSchema' using a 'CEnv.CryptolEnv'
 importSchemaCEnv :: SharedContext -> CEnv.CryptolEnv -> Cryptol.Schema ->

saw-central/src/SAWCentral/Value.hs

@@ -754,26 +754,28 @@ type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle,
 --        builtin types that aren't special cases in the AST appear)
 type TyEnv = ScopedMap SS.Name (SS.PrimitiveLifecycle, SS.NamedType)
 
+-- | The Cryptol environment. We maintain a stack of Cryptol
+--   environments and push/pop them as we enter and leave scopes;
+--   otherwise the Cryptol environment doesn't track SAWScript scopes
+--   and horribly confusing wrong things happen.
+newtype CryptolScopeStack = CryptolScopeStack (NonEmpty CEnv.CryptolEnv)
+
 -- | Type for the ordinary interpreter environment.
 --
 --   There's one environment that maps variable names to values, and
---   one that maps type names to types. Both get closed in with
---   lambdas and do-blocks at the appropriate times.
+--   one that maps type names to types. A third handles the Cryptol
+--   domain. All three get closed in with lambdas and do-blocks at the
+--   appropriate times.
 --
 --   Note that rebindable variables are sold separately. This is so
 --   they don't get closed in; references to rebindable variables
 --   always retrieve the most recent version.
 data Environ = Environ {
     eVarEnv :: VarEnv,
-    eTyEnv :: TyEnv
+    eTyEnv :: TyEnv,
+    eCryptol :: CryptolScopeStack
 }
 
--- | The Cryptol environment. We maintain a stack of Cryptol
---   environments and push/pop them as we enter and leave scopes;
---   otherwise the Cryptol environment doesn't track SAWScript scopes
---   and horribly confusing wrong things happen.
-newtype CryptolScopeStack = CryptolScopeStack (NonEmpty CEnv.CryptolEnv)
-
 -- | The extra environment for rebindable globals.
 --
 --   Note: because no builtins are rebindable, there are no lifecycle
@@ -784,28 +786,27 @@ type RebindableEnv = Map SS.Name (SS.Pos, SS.Schema, Value)
 -- | Enter a scope.
 pushScope :: TopLevel ()
 pushScope = do
-    Environ varenv tyenv <- gets rwEnviron
-    cryenv <- gets rwCryptol
+    Environ varenv tyenv cryenv <- gets rwEnviron
     let varenv' = ScopedMap.push varenv
         tyenv' = ScopedMap.push tyenv
         cryenv' = cryptolPush cryenv
-    modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv', rwCryptol = cryenv' })
+    modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' })
 
 -- | Leave a scope. This will panic if you try to leave the last scope;
 --   pushes and pops should be matched.
 popScope  :: TopLevel ()
 popScope = do
-    Environ varenv tyenv <- gets rwEnviron
-    cryenv <- gets rwCryptol
+    Environ varenv tyenv cryenv <- gets rwEnviron
     let varenv' = ScopedMap.pop varenv
         tyenv' = ScopedMap.pop tyenv
         cryenv' = cryptolPop cryenv
-    modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv', rwCryptol = cryenv' })
+    modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' })
 
 
 getCryptolEnv :: TopLevel CEnv.CryptolEnv
 getCryptolEnv = do
-    CryptolScopeStack (e :| _) <- gets rwCryptol
+    Environ _varenv _tyenv cryenv <- gets rwEnviron
+    let CryptolScopeStack (e :| _) = cryenv
     return e
 
 cryptolPush :: CryptolScopeStack -> CryptolScopeStack
@@ -857,9 +858,6 @@ data TopLevelRW =
     rwEnviron :: Environ
   , rwRebindables :: RebindableEnv
 
-    -- | The Cryptol naming environment.
-  , rwCryptol    :: CryptolScopeStack
-
     -- | The current execution position. This is only valid when the
     --   interpreter is calling out into saw-central to execute a
     --   builtin. Within the interpreter, the current position is
@@ -1176,7 +1174,7 @@ extendEnv pos name rb ty doc v = do
          modname = T.packModName [name]
 
      -- Update the SAWScript environment.
-     Environ varenv tyenv <- gets rwEnviron
+     Environ varenv tyenv cryenv <- gets rwEnviron
      rbenv <- gets rwRebindables
      let (varenv', rbenv') = case rb of
            SS.ReadOnlyVar ->
@@ -1195,7 +1193,7 @@ extendEnv pos name rb ty doc v = do
              (varenv, re')
 
      -- Mirror the value into the Cryptol environment if appropriate.
-     CryptolScopeStack (ce :| ces) <- gets rwCryptol
+     let CryptolScopeStack (ce :| ces) = cryenv
      ce' <-
        case v of
          VTerm t ->
@@ -1214,19 +1212,19 @@ extendEnv pos name rb ty doc v = do
               pure $ CEnv.bindTypedTerm (ident, tt) ce
          _ ->
            pure ce
+     let cryenv' = CryptolScopeStack (ce' :| ces)
 
      -- Drop the new bits into place.
      modify (\rw -> rw {
-         rwCryptol = CryptolScopeStack (ce' :| ces),
-         rwEnviron = Environ varenv' tyenv,
+         rwEnviron = Environ varenv' tyenv cryenv',
          rwRebindables = rbenv'
      })
 
 extendEnvMulti :: [(SS.Pos, SS.Name, SS.Rebindable, SS.Schema, Maybe [Text], Environ -> Value)] -> TopLevel ()
 extendEnvMulti bindings = do
 
      -- Update the SAWScript environment.
-     Environ varenv tyenv <- gets rwEnviron
+     Environ varenv tyenv cryenv <- gets rwEnviron
 
      -- Insert all the bindings at once, and feed the final resulting
      -- interpreter environment into each value. This circular
@@ -1259,7 +1257,7 @@ extendEnvMulti bindings = do
              in
              ScopedMap.insert name (pos, SS.Current, ty, v'', doc) tmpenv
          varenv' = foldr insert varenv bindings
-         environ' = Environ varenv' tyenv
+         environ' = Environ varenv' tyenv cryenv
 
      -- Drop the new bits into place.
      modify (\rw -> rw { rwEnviron = environ' })
@@ -1269,10 +1267,10 @@ extendEnvMulti bindings = do
 addTypedef :: SS.Name -> SS.Type -> TopLevel ()
 addTypedef name ty = do
     avail <- gets rwPrimsAvail
-    Environ varenv tyenv <- gets rwEnviron
+    Environ varenv tyenv cryenv <- gets rwEnviron
     let ty' = SS.substituteTyVars avail tyenv ty
         tyenv' = ScopedMap.insert name (SS.Current, SS.ConcreteType ty') tyenv
-    modify (\rw -> rw { rwEnviron = Environ varenv tyenv' })
+    modify (\rw -> rw { rwEnviron = Environ varenv tyenv' cryenv })
 
 typedTermOfString :: SharedContext -> String -> IO TypedTerm
 typedTermOfString sc str =