SAWScript: Add an extra global environment for "let rebindable".

This makes the new "let rebindable" functionality work, fixing the
test05 and test14 cases of test1646, and finally closes #1646.

Author: sauclovian-g

intTests/test1646/test05.log.good

@@ -1,3 +1,3 @@
  Loading file "test05.saw"
  x=a
- x=a
+ x=b

intTests/test1646/test05.saw

@@ -1,5 +1,4 @@
 // The second f call will print x=b.
-// XXX currently it prints x=a
 
 let rebindable x = "a";
 

intTests/test1646/test14.log.good

@@ -1,6 +1,6 @@
  Loading file "test14.saw"
  x=a
- x=a
- test14.saw:12:5-12:6: Warning: Redeclaration of x
- test14.saw:9:16-9:17: Warning: Previous declaration was here
- x=a
+ x=b
+ test14.saw:11:5-11:6: Warning: Redeclaration of x
+ test14.saw:8:16-8:17: Warning: Previous declaration was here
+ x=b

intTests/test1646/test14.saw

@@ -1,5 +1,4 @@
 // The second f call should print x=b. So should the third.
-// XXX: currently all print x=a.
 
 let rebindable x = "a";
 

intTests/test1646/test15.log.good

@@ -1,5 +1,8 @@
  <stdin>:1:5-1:6: Warning: Redeclaration of y
  <stdin>:1:16-1:17: Warning: Previous declaration was here
+x : rebindable Int
+y : rebindable Int
+
 abc : ProofScript ()
 abstract_symbolic : Term -> Term
 add_cryptol_defs : [String] -> Simpset -> Simpset
@@ -345,5 +348,4 @@ write_smtlib2_w4 : String -> Term -> TopLevel ()
 yices : ProofScript ()
 z3 : ProofScript ()
 
-x : Int
 y : Int

saw-central/src/SAWCentral/Builtins.hs

@@ -1705,10 +1705,21 @@ envCmd = do
   opts <- getOptions
   avail <- gets rwPrimsAvail
   SV.Environ varenv _tyenv <- gets rwEnviron
-  let printItem (x, (_pos, _lc, _rb, ty, _v, _doc)) =
+  rbenv <- gets rwRebindables
+
+  -- print rebindables first if there are any
+  unless (Map.null rbenv) $ do
+      io $ printOutLn opts Info $ "Rebindable globals:"
+      io $ printOutLn opts Info $ ""
+      let printRB (x, (_pos, ty, _v)) = do
+              let str = x <> " : rebindable " <> PPS.pShowText ty
+              printOutLn opts Info $ Text.unpack str
+      io $ mapM_ printRB $ Map.assocs rbenv
+
+  let printItem (x, (_pos, _lc, ty, _v, _doc)) =
           printOutLn opts Info $ Text.unpack (x <> " : " <> PPS.pShowText ty)
       -- Print only the visible objects
-      keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail
+      keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail
       -- Insert a blank line in the output where there's a scope boundary
       printScope mItems = case mItems of
           Nothing -> printOutLn opts Info ""

saw-central/src/SAWCentral/Value.hs

@@ -746,14 +746,25 @@ evaluateTypedTerm _sc (TypedTerm tp _) =
 -- TopLevel Monad --------------------------------------------------------------
 
 -- | Type names for the interpreter environment components.
-type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable,
+--
+-- Note: because no builtins are rebindable, the rebindable
+-- environment doesn't have lifecycle or help text fields. There is,
+-- currently at least, no way to populate those for non-builtins.
+type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle,
                                  SS.Schema, Value, Maybe [Text])
 type TyEnv = ScopedMap SS.Name (SS.PrimitiveLifecycle, SS.NamedType)
 
--- | Type for the full interpreter environment.
+type RebindableEnv = Map SS.Name (SS.Pos, SS.Schema, Value)
+
+-- | 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.
 --
---   There's one environment that maps variable names to values,
---   and one that maps type names to types.
+--   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
@@ -877,6 +888,7 @@ data TopLevelRW =
 --    rwValueInfo  :: Map SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable,
 --                                 SS.Schema, Value, Maybe [Text])
     rwEnviron :: Environ
+  , rwRebindables :: RebindableEnv
 
     -- | The type environment: a map from type names to:
     --      - the lifecycle setting (experimental/current/deprecated/etc)
@@ -1213,7 +1225,22 @@ extendEnv pos name rb ty doc v = do
 
      -- Update the SAWScript environment.
      Environ varenv tyenv <- gets rwEnviron
-     let varenv' = ScopedMap.insert name (pos, SS.Current, rb, ty, v, doc) varenv
+     rbenv <- gets rwRebindables
+     let (varenv', rbenv') = case rb of
+           SS.ReadOnlyVar ->
+             -- If we replace a rebindable variable at the top level with a
+             -- readonly one, the readonly version in varenv will hide it
+             -- ever after. We ought to remove it from rbenv; however, it's
+             -- not easy to know here whether we're at the top level or not.
+             -- FUTURE: maybe this will become easier in the long run.
+             let ve' = ScopedMap.insert name (pos, SS.Current, ty, v, doc) varenv in
+             (ve', rbenv)
+           SS.RebindableVar ->
+             -- The typechecker restricts this to happen only at the
+             -- top level and only if any existing variable is already
+             -- rebindable, so we don't have to update varenv.
+             let re' = M.insert name (pos, ty, v) rbenv in
+             (varenv, re')
 
      -- Mirror the value into the Cryptol environment if appropriate.
      ce <- gets rwCryptol
@@ -1237,7 +1264,11 @@ extendEnv pos name rb ty doc v = do
            pure ce
 
      -- Drop the new bits into place.
-     modify (\rw -> rw { rwCryptol = ce', rwEnviron = Environ varenv' tyenv })
+     modify (\rw -> rw {
+         rwCryptol = ce',
+         rwEnviron = Environ varenv' tyenv,
+         rwRebindables = rbenv'
+     })
 
 extendEnvMulti :: [(SS.Pos, SS.Name, SS.Rebindable, SS.Schema, Maybe [Text], Environ -> Value)] -> TopLevel ()
 extendEnvMulti bindings = do
@@ -1262,10 +1293,19 @@ extendEnvMulti bindings = do
                      VLambda{} -> v
                      _ ->
                          panic "extendEnvMulti" [
-                             "Non-lambda value: " <> Text.pack (show v)
+                             "Non-lambda value: " <> Text.pack (show v),
+                             "Source position: " <> Text.pack (show pos)
+                         ]
+                 v'' = case rb of
+                     SS.ReadOnlyVar -> v'
+                     SS.RebindableVar ->
+                         -- "rec" declarations can't be rebindable
+                         panic "extendEnvMulti" [
+                             "Rebindable variable: " <> name,
+                             "Source position: " <> Text.pack (show pos)
                          ]
              in
-             ScopedMap.insert name (pos, SS.Current, rb, ty, v', doc) tmpenv
+             ScopedMap.insert name (pos, SS.Current, ty, v'', doc) tmpenv
          varenv' = foldr insert varenv bindings
          environ' = Environ varenv' tyenv
 

saw-script/src/SAWScript/Interpreter.hs

@@ -510,22 +510,30 @@ interpretExpr expr =
       SS.Var pos x -> do
           avail <- gets rwPrimsAvail
           Environ varenv _tyenv <- gets rwEnviron
-          case ScopedMap.lookup x varenv of
-            Nothing ->
-                -- This should be rejected by the typechecker, so panic
-                panic "interpretExpr" [
-                    "Read of unknown variable " <> x
-                ]
-            Just (_defpos, lc, _rebindable, _ty, v, _doc)
-              | Set.member lc avail -> do
-                   let v' = injectPositionIntoMonadicValue pos v
-                       v'' = insertRefChain pos x v'
-                   return v''
-              | otherwise ->
-                   -- This case is also rejected by the typechecker
-                   panic "interpretExpr" [
-                       "Read of inaccessible variable " <> x
-                   ]
+          rbenv <- gets rwRebindables
+          let info = case ScopedMap.lookup x varenv of
+                  Nothing ->
+                      -- Try the rebindable environment
+                      case Map.lookup x rbenv of
+                          Nothing -> Nothing
+                          Just (_defpos, _ty, v) -> Just (Current, v)
+                  Just (_defpos, lc, _ty, v, _doc) -> Just (lc, v)
+          case info of
+              Nothing ->
+                  -- This should be rejected by the typechecker; panic
+                  panic "interpretExpr" [
+                      "Read of unknown variable " <> x
+                  ]
+              Just (lc, v)
+                | Set.member lc avail -> do
+                      let v' = injectPositionIntoMonadicValue pos v
+                          v'' = insertRefChain pos x v'
+                      return v''
+                | otherwise ->
+                      -- This case is also rejected by the typechecker
+                      panic "interpretExpr" [
+                           "Read of inaccessible variable " <> x
+                      ]
       SS.Lambda _pos mname pat e -> do
           env <- gets rwEnviron
           return $ VLambda env mname pat e
@@ -912,9 +920,15 @@ interpretTopStmt printBinds stmt = do
   --    - shouldn't have to flatten the environments
   --    - shouldn't be typechecking one statement at a time regardless
   Environ varenv tyenv <- liftTopLevel $ gets rwEnviron
-  let varenv' = Map.map (\(pos, lc, rb, ty, _v, _doc) -> (pos, lc, rb, ty)) $ ScopedMap.flatten varenv
+  rbenv <- liftTopLevel $ gets rwRebindables
+
+  let varenv' = Map.map (\(pos, lc, ty, _v, _doc) -> (pos, lc, SS.ReadOnlyVar, ty)) $ ScopedMap.flatten varenv
+      rbenv' = Map.map (\(pos, ty, _v) -> (pos, SS.Current, SS.RebindableVar, ty)) rbenv
+      -- If anything appears in both, favor the real environment
+      varenv'' = Map.union varenv' rbenv'
+
   let tyenv' = ScopedMap.flatten tyenv
-  stmt' <- processTypeCheck $ checkStmt avail varenv' tyenv' ctx stmt
+  stmt' <- processTypeCheck $ checkStmt avail varenv'' tyenv' ctx stmt
 
   case stmt' of
 
@@ -995,6 +1009,7 @@ interpretMain :: TopLevel ()
 interpretMain = do
   avail <- gets rwPrimsAvail
   Environ varenv tyenv <- gets rwEnviron
+  rbenv <- gets rwRebindables
   let pos = SS.PosInternal "entry"
       -- We need the type to be "TopLevel a", not just "TopLevel ()".
       -- There are several (old) tests in the test suite whose main
@@ -1004,11 +1019,19 @@ interpretMain = do
       tyRet = SS.TyVar pos "a"
       tyMonadic = SS.tBlock pos (SS.tContext pos SS.TopLevel) tyRet
       tyExpected = SS.Forall [(pos, "a")] tyMonadic
-  case ScopedMap.lookup "main" varenv of
+  let main = case ScopedMap.lookup "main" varenv of
+          Just (_defpos, lc, tyFound, v, _doc) -> Just (lc, tyFound, v)
+          -- Having main be rebindable doesn't make much sense, but
+          -- it's easier to have this code than to spend time
+          -- explaining that it's not allowed.
+          Nothing -> case Map.lookup "main" rbenv of
+              Nothing -> Nothing
+              Just (_defpos, tyFound, v) -> Just (Current, tyFound, v)
+  case main of
     Nothing ->
       -- Don't fail or complain if there's no main.
       return ()
-    Just (_defpos, Current, _rebindable, tyFound, v, _doc) -> case tyFound of
+    Just (Current, tyFound, v) -> case tyFound of
         SS.Forall _ (SS.TyCon _ SS.BlockCon [_, _]) ->
             -- XXX shouldn't have to do this
             let tyenv' = ScopedMap.flatten tyenv in
@@ -1026,7 +1049,7 @@ interpretMain = do
             -- If the type is something entirely random, like a Term or a
             -- String or something, just ignore it.
             return ()
-    Just (_defpos, lc, _rebindable, _ty, _v, _doc) ->
+    Just (lc, _ty, _v) ->
       -- There is no way for things other than primitives to get marked
       -- experimental or deprecated, so this isn't possible. If we allow
       -- users to deprecate their own functions in the future, change
@@ -1093,6 +1116,7 @@ buildTopLevelEnv proxy opts scriptArgv =
 
        let rw0 = TopLevelRW
                    { rwEnviron = primEnviron opts bic
+                   , rwRebindables = Map.empty
                    , rwCryptol    = ce0
                    , rwPosition = SS.Unknown
                    , rwStackTrace = Trace.empty
@@ -6455,7 +6479,7 @@ primNamedTypeEnv = fmap extract primTypes
 primValueEnv ::
    Options ->
    BuiltinContext ->
-   Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Rebindable, SS.Schema, Value, Maybe [Text])
+   Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Schema, Value, Maybe [Text])
 primValueEnv opts bic = Map.mapWithKey extract primitives
   where
       header = [
@@ -6476,7 +6500,7 @@ primValueEnv opts bic = Map.mapWithKey extract primitives
           header <> tag p <> name n p <> primitiveDoc p
       extract n p =
           let pos = SS.PosInternal "<<builtin>>" in
-          (pos, primitiveLife p, SS.ReadOnlyVar, primitiveType p,
+          (pos, primitiveLife p, primitiveType p,
            (primitiveFn p) opts bic, Just $ doc n p)
 
 primEnviron :: Options -> BuiltinContext -> Environ

saw-script/src/SAWScript/REPL/Command.hs

@@ -44,7 +44,7 @@ import SAWScript.Token (Token)
 
 import Cryptol.Parser (ParseError())
 
-import Control.Monad (guard, void)
+import Control.Monad (guard, unless, void)
 
 import Data.Char (isSpace,isPunctuation,isSymbol)
 import Data.Function (on)
@@ -77,7 +77,7 @@ import SAWScript.Interpreter (interpretTopStmt)
 import qualified SAWScript.Lexer (lexSAW)
 import qualified SAWScript.Parser (parseStmtSemi, parseExpression, parseSchemaPattern)
 import SAWCentral.TopLevel (TopLevelRW(..))
-import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable)
+import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable, Rebindable(..))
 
 
 -- Commands --------------------------------------------------------------------
@@ -205,11 +205,16 @@ typeOfCmd str
      rw <- getTopLevelRW
      decl' <- do
        let primsAvail = rwPrimsAvail rw
+           -- XXX it should not be necessary to do this munging
            Environ varenv tyenv = rwEnviron rw
-           squash (defpos, lc, rb, ty, _val, _doc) = (defpos, lc, rb, ty)
+           squash (defpos, lc, ty, _val, _doc) = (defpos, lc, ReadOnlyVar, ty)
            varenv' = Map.map squash $ ScopedMap.flatten varenv
            tyenv' = ScopedMap.flatten tyenv
-       let (errs_or_results, warns) = checkDecl primsAvail varenv' tyenv' decl
+           rbenv = rwRebindables rw
+           rbsquash (defpos, ty, _val) = (defpos, Current, RebindableVar, ty)
+           rbenv' = Map.map rbsquash rbenv
+           varenv'' = Map.union varenv' rbenv'
+       let (errs_or_results, warns) = checkDecl primsAvail varenv'' tyenv' decl
        let issueWarning (msgpos, msg) =
              -- XXX the print functions should be what knows how to show positions...
              putStrLn (show msgpos ++ ": Warning: " ++ msg)
@@ -243,11 +248,16 @@ searchCmd str
      -- for deprecated functions that take Terms.
 
      let primsAvail = rwPrimsAvail rw
+         -- XXX it should not be necessary to do this munging
          Environ varenv tyenv = rwEnviron rw
-         squash (pos, lc, rb, ty, _val, _doc) = (pos, lc, rb, ty)
+         rbenv = rwRebindables rw
+         squash (pos, lc, ty, _val, _doc) = (pos, lc, ReadOnlyVar, ty)
          varenv' = Map.map squash $ ScopedMap.flatten varenv
          tyenv' = ScopedMap.flatten tyenv
-         (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv' tyenv' pat
+         rbsquash (pos, ty, _val) = (pos, Current, RebindableVar, ty)
+         rbenv' = Map.map rbsquash rbenv
+         varenv'' = Map.union varenv' rbenv'
+         (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv'' tyenv' pat
      let issueWarning (msgpos, msg) =
            -- XXX the print functions should be what knows how to show positions...
            putStrLn (show msgpos ++ ": Warning: " ++ msg)
@@ -343,13 +353,24 @@ quitCmd  = stop
 envCmd :: REPL ()
 envCmd = do
   rw <- getTopLevelRW
-  let avail = rwPrimsAvail rw
-      Environ varenv _tyenv = rwEnviron rw
-      say (x, (_pos, _lc, _rb, ty, _v, _doc)) = do
+  let Environ varenv _tyenv = rwEnviron rw
+      rbenv = rwRebindables rw
+      avail = rwPrimsAvail rw
+
+  -- print the rebindable globals first, if any
+  unless (Map.null rbenv) $ do
+      let rbsay (x, (_pos, ty, _v)) = do
+              let ty' = PPS.pShowText ty
+              TextIO.putStrLn (x <> " : rebindable " <> ty')
+      io $ mapM_ rbsay $ Map.assocs rbenv
+      io $ TextIO.putStrLn ""
+
+  -- print the normal environment
+  let say (x, (_pos, _lc, ty, _v, _doc)) = do
           let ty' = PPS.pShowText ty
           TextIO.putStrLn (x <> " : " <> ty')
       -- Print only the visible objects
-      keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail
+      keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail
       -- Insert a blank line in the output where there's a scope boundary
       printScope mItems = case mItems of
           Nothing -> TextIO.putStrLn ""
@@ -383,11 +404,14 @@ helpCmd cmd
   | null cmd = io (mapM_ putStrLn (genHelp commandList))
   | otherwise =
     do rw <- getTopLevelRW
+       -- Note: there's no rebindable builtins and thus no way to
+       -- attach help text to anything rebindable, so we can ignore
+       -- the rebindables.
        let Environ varenv _tyenv = rwEnviron rw
        case ScopedMap.lookup (Text.pack cmd) varenv of
-         Just (_pos, _lc, _rb, _ty, _v, Just doc) ->
+         Just (_pos, _lc, _ty, _v, Just doc) ->
            io $ mapM_ TextIO.putStrLn doc
-         Just (_pos, _lc, _rb, _ty, _v, Nothing) -> do
+         Just (_pos, _lc, _ty, _v, Nothing) -> do
            io $ putStrLn $ "// No documentation is available."
            typeOfCmd cmd
          Nothing ->