Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Translate Constant term bodies in a top-level name scope.
Browse files Browse the repository at this point in the history
Fixes #18.
  • Loading branch information
Brian Huffman committed Oct 9, 2020
1 parent 689afdc commit 54b5e47
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion src/Verifier/SAW/Translation/Coq/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 54b5e47

Please sign in to comment.