Merge pull request #21 from GaloisInc/issue18

Translate Constant term bodies in a top-level name scope.
GaloisInc · Oct 9, 2020 · 2c7b485 · 2c7b485
2 parents 689afdc + 54b5e47
commit 2c7b485
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/src/Verifier/SAW/Translation/Coq/Term.hs b/src/Verifier/SAW/Translation/Coq/Term.hs
@@ -484,7 +484,14 @@ translateTermUnshared t = withLocalLocalEnvironment $ do
       if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
         then Coq.Var <$> pure renamed
         else do
-        b <- go env body
+        b <-
+          -- Translate body in a top-level name scope
+          withLocalLocalEnvironment $
+          do modify $ set localEnvironment []
+             modify $ set unavailableIdents reservedIdents
+             modify $ set sharedNames IntMap.empty
+             modify $ set nextSharedName "var__0"
+             translateTermLet body
         modify $ over localDeclarations $ (mkDefinition renamed b :)
         Coq.Var <$> pure renamed