refactored the saw-core-coq translator so that all the local variable…

… information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927
GaloisInc · Sep 1, 2023 · 599a177 · 599a177
1 parent b74252b
commit 599a177
Show file tree

Hide file tree

Showing 4 changed files with 275 additions and 226 deletions.
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
@@ -121,7 +121,7 @@ translateTermAsDeclImports configuration name t tp = do
   doc <-
     TermTranslation.translateDefDoc
       configuration
-      (TermTranslation.TranslationReader Nothing)
+      Nothing
       [] name t tp
   return $ vcat [preamble configuration, hardline <> doc]
 

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
@@ -3,7 +3,7 @@
 
 module Verifier.SAW.Translation.Coq.CryptolModule where
 
-import           Control.Lens                       (over, set, view)
+import           Control.Lens                       (over, view)
 import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
@@ -27,9 +27,7 @@ translateTypedTermMap defs = forM defs translateAndRegisterEntry
     translateAndRegisterEntry (name, t, tp) = do
       let nameStr = unpackIdent (nameIdent name)
       decl <-
-        TermTranslation.withLocalTranslationState $
-        do modify $ set TermTranslation.localEnvironment [nameStr]
-           t_trans <- TermTranslation.translateTerm t
+        do t_trans <- TermTranslation.translateTerm t
            tp_trans <- TermTranslation.translateTerm tp
            return $ TermTranslation.mkDefinition nameStr t_trans tp_trans
       modify $ over TermTranslation.globalDeclarations (nameStr :)
@@ -55,7 +53,7 @@ translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) =
        (reverse . view TermTranslation.topLevelDeclarations . snd <$>
         TermTranslation.runTermTranslationMonad
         configuration
-        (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+        Nothing -- TODO: this should be Just no?
         globalDecls
         []
         (translateTypedTermMap defs))
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
@@ -42,14 +42,14 @@ import Verifier.SAW.Translation.Coq.Monad
 -- import Debug.Trace
 
 type ModuleTranslationMonad m =
-  M.TranslationMonad TermTranslation.TranslationReader () m
+  M.TranslationMonad (Maybe ModuleName) () m
 
 runModuleTranslationMonad ::
   M.TranslationConfiguration -> Maybe ModuleName ->
   (forall m. ModuleTranslationMonad m => m a) ->
   Either (M.TranslationError Term) (a, ())
 runModuleTranslationMonad configuration modName =
-  M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) ()
+  M.runTranslationMonad configuration modName ()
 
 dropPi :: Coq.Term -> Coq.Term
 dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r
@@ -93,22 +93,22 @@ translateDataType (DataType {..}) =
     translateNamed name = do
       let inductiveName = name
       (inductiveParameters, inductiveIndices) <-
-        liftTermTranslationMonad $ do
-        ps <- TermTranslation.translateParams dtParams
-        ixs <- TermTranslation.translateParams dtIndices
+        liftTermTranslationMonad $
+        TermTranslation.translateParams dtParams $ \ps ->
+        TermTranslation.translateParams dtIndices $ \ixs ->
         -- Translating the indices of a data type should never yield
         -- Inhabited constraints, so the result of calling
         -- `translateParams dtIndices` above should only return Binders and not
         -- any ImplicitBinders. Moreover, `translateParams` always returns
         -- Binders where the second field is `Just t`, where `t` is the type.
-        let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg
+        let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg in
         let bs = map (\case Coq.Binder s (Just t) ->
                               Coq.PiBinder (Just s) t
                             Coq.Binder _ Nothing ->
                               errorBecause "encountered a Binder without a Type"
                             Coq.ImplicitBinder{} ->
                               errorBecause "encountered an implicit binder")
-                     ixs
+                     ixs in
         return (ps, bs)
       let inductiveSort = TermTranslation.translateSort dtSort
       inductiveConstructors <- mapM (translateCtor inductiveParameters) dtCtors