From 54b5e47fc75feba772654e6b8977a527a52daf4f Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 8 Oct 2020 18:56:28 -0700
Subject: [PATCH] Translate Constant term bodies in a top-level name scope.

Fixes #18.
---
 src/Verifier/SAW/Translation/Coq/Term.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Verifier/SAW/Translation/Coq/Term.hs b/src/Verifier/SAW/Translation/Coq/Term.hs
index 6cbb393c..2f6dbdd3 100644
--- 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