saw-core-coq: fix and document the local translation state (#1328)

5a37203 introduced a subtle bug in the
translation of Cryptol modules to Coq.  In this commit, it was decided that all
'TranslationState' should be restored when calling `withLocalLocalEnvironment'.

Historically, 'withLocalLocalEnvironment' was only supposed to restore the
value of the 'localEnvironment' field of the translation state, hence its name.
The translation state has grown since, and includes many fields that ought to
be restored after a local (sub-)term translation.  Unfortunately, the
translation state also contains fields that are meant to monotonically
accumulate global data through the translation.

Those fields are thus being erased incorrectly due to the changes made.  This
commit revert those changes, making it painfully explicit which fields of the
state are to be restored or preserved so that future refactorings will have to
make a decision.

In the process, I also renamed the confusing 'localDeclarations' into
'topLevelDeclarations', since it captures declarations that appear in the
processed file (so more local than the "global", "ambient" standard library
declarations), but the name made it sound like these were more local.

saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v

@@ -583,8 +583,11 @@ Definition ecRotR : forall (m : @Num), forall (ix : Type), forall (a : Type), @P
 Definition ecCat : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a :=
   @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @seq n a -> @seq (@tcAdd (@TCNum m) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.append m n a) (fun (a : Type) => @SAWCorePrelude.streamAppend a m)).
 
-Definition ecSplitAt : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a) :=
-  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a)) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> prod (@SAWCoreVectorsAsCoqVectors.Vec m a) (@seq n a)) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => pair (@SAWCorePrelude.take a m n xs) (@SAWCorePrelude.drop a m n xs)) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => pair (@SAWCorePrelude.streamTake a m xs) (@SAWCorePrelude.streamDrop a m xs))).
+Definition ecTake : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a :=
+  @CryptolPrimitivesForSAWCore.Num_rect (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.take a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamTake a m xs)) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCInf) n) a -> @SAWCorePrelude.Stream a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCorePrelude.Stream a) => xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => xs)).
+
+Definition ecDrop : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a :=
+  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @seq n a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.drop a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamDrop a m xs)).
 
 Definition ecJoin : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m (@seq n a) -> @seq (@tcMul m n) a :=
   fun (m : @Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : @Num) => forall (n : @Num), forall (a : Type), @seq m1 (@seq n a) -> @seq (@tcMul m1 n) a) (fun (m1 : @SAWCoreScaffolding.Nat) => @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m1 (@seq n a) -> @seq (@tcMul (@TCNum m1) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.join m1 n a)) (@finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Stream (@seq n a) -> @seq (@tcMul (@TCInf) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.natCase (fun (n' : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec n' a) -> @seq (@SAWCorePrelude.if0Nat (@Num) n' (@TCNum 0) (@TCInf)) a) (fun (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec 0 a)) => @SAWCoreVectorsAsCoqVectors.EmptyVec a) (fun (n' : @SAWCoreScaffolding.Nat) (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n') a)) => @SAWCorePrelude.streamJoin a n' s) n)) m.

saw-core-coq/src/Verifier/SAW/Translation/Coq.hs

@@ -113,7 +113,11 @@ Import ListNotations.
 translateTermAsDeclImports ::
   TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann)
 translateTermAsDeclImports configuration name t = do
-  doc <- TermTranslation.translateDefDoc configuration Nothing [] name t
+  doc <-
+    TermTranslation.translateDefDoc
+      configuration
+      (TermTranslation.TranslationReader Nothing)
+      [] name t
   return $ vcat [preamble configuration, hardline <> doc]
 
 translateSAWModule :: TranslationConfiguration -> Module -> Doc ann
@@ -131,7 +135,11 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) (Doc ann)
 translateCryptolModule configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration

saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs

@@ -8,10 +8,10 @@ import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
 
-import           Cryptol.ModuleSystem.Name
-import           Cryptol.Utils.Ident
+import           Cryptol.ModuleSystem.Name          (Name, nameIdent)
+import           Cryptol.Utils.Ident                (unpackIdent)
 import qualified Language.Coq.AST                   as Coq
-import           Verifier.SAW.Term.Functor
+import           Verifier.SAW.Term.Functor          (Term)
 import           Verifier.SAW.Translation.Coq.Monad
 import qualified Verifier.SAW.Translation.Coq.Term  as TermTranslation
 import           Verifier.SAW.TypedTerm
@@ -23,21 +23,28 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
     translateAndRegisterEntry (name, symbol) = do
       let t = ttTerm symbol
       let nameStr = unpackIdent (nameIdent name)
-      term <- TermTranslation.withLocalLocalEnvironment $ do
+      term <- TermTranslation.withLocalTranslationState $ do
         modify $ set TermTranslation.localEnvironment [nameStr]
         TermTranslation.translateTerm t
       let decl = TermTranslation.mkDefinition nameStr term
       modify $ over TermTranslation.globalDeclarations (nameStr :)
       return decl
 
+-- | Translates a Cryptol Module into a list of Coq declarations.  This is done
+-- by going through the term map corresponding to the module, translating all
+-- terms, and accumulating the translated declarations of all top-level
+-- declarations encountered.
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl]
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) [Coq.Decl]
 translateCryptolModule configuration globalDecls (CryptolModule _ tm) =
-  case TermTranslation.runTermTranslationMonad
-       configuration
-       Nothing
-       globalDecls
-       []
-       (translateTypedTermMap tm) of
-  Left e -> Left e
-  Right (_, st) -> Right (reverse (view TermTranslation.localDeclarations st))
+  reverse . view TermTranslation.topLevelDeclarations . snd
+  <$> TermTranslation.runTermTranslationMonad
+      configuration
+      (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+      globalDecls
+      []
+      (translateTypedTermMap tm)

saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs

@@ -17,6 +17,7 @@ module Verifier.SAW.Translation.Coq.Monad
   , TranslationConfigurationMonad
   , TranslationMonad
   , TranslationError(..)
+  , WithTranslationConfiguration(..)
   , runTranslationMonad
   ) where
 
@@ -77,19 +78,32 @@ data TranslationConfiguration = TranslationConfiguration
   -- - SAWCoreVectorsAsSSReflectSeqs
   }
 
-type TranslationConfigurationMonad m =
-  ( MonadReader TranslationConfiguration m
+-- | The functional dependency of 'MonadReader' makes it not compositional, so
+-- we have to jam together different structures that want to be in the 'Reader'
+-- into a single datatype.  This type allows adding extra configuration on top
+-- of the translation configuration.
+data WithTranslationConfiguration r = WithTranslationConfiguration
+  { translationConfiguration :: TranslationConfiguration
+  , otherConfiguration :: r
+  }
+
+-- | Some computations will rely solely on access to the configuration, so we
+-- provide it separately.
+type TranslationConfigurationMonad r m =
+  ( MonadReader (WithTranslationConfiguration r) m
   )
 
-type TranslationMonad s m =
+type TranslationMonad r s m =
   ( Except.MonadError (TranslationError Term)  m
-  , TranslationConfigurationMonad m
+  , TranslationConfigurationMonad r m
   , MonadState s m
   )
 
 runTranslationMonad ::
   TranslationConfiguration ->
+  r ->
   s ->
-  (forall m. TranslationMonad s m => m a) ->
+  (forall m. TranslationMonad r s m => m a) ->
   Either (TranslationError Term) (a, s)
-runTranslationMonad configuration state m = runStateT (runReaderT m configuration) state
+runTranslationMonad configuration r s m =
+  runStateT (runReaderT m (WithTranslationConfiguration configuration r)) s

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -24,10 +24,8 @@ Portability : portable
 
 module Verifier.SAW.Translation.Coq.SAWModule where
 
-import           Control.Lens                                  (makeLenses, view)
 import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
-import           Control.Monad.State                           hiding (fail)
 import           Prelude                                       hiding (fail)
 import           Prettyprinter                                 (Doc)
 
@@ -36,26 +34,22 @@ import qualified Language.Coq.Pretty                           as Coq
 import           Verifier.SAW.Module
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Term.Functor
-import           Verifier.SAW.Translation.Coq.Monad
+import qualified Verifier.SAW.Translation.Coq.Monad            as M
 import           Verifier.SAW.Translation.Coq.SpecialTreatment
 import qualified Verifier.SAW.Translation.Coq.Term             as TermTranslation
+import Verifier.SAW.Translation.Coq.Monad
 
 -- import Debug.Trace
 
-data ModuleTranslationState = ModuleTranslationState
-  { _currentModule  :: Maybe ModuleName
-  }
-  deriving (Show)
-makeLenses ''ModuleTranslationState
-
-type ModuleTranslationMonad m = TranslationMonad ModuleTranslationState m
+type ModuleTranslationMonad m =
+  M.TranslationMonad TermTranslation.TranslationReader () m
 
 runModuleTranslationMonad ::
-  TranslationConfiguration -> Maybe ModuleName ->
+  M.TranslationConfiguration -> Maybe ModuleName ->
   (forall m. ModuleTranslationMonad m => m a) ->
-  Either (TranslationError Term) (a, ModuleTranslationState)
-runModuleTranslationMonad configuration modname =
-  runTranslationMonad configuration (ModuleTranslationState modname)
+  Either (M.TranslationError Term) (a, ())
+runModuleTranslationMonad configuration modName =
+  M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) ()
 
 dropPi :: Coq.Term -> Coq.Term
 dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r
@@ -162,15 +156,19 @@ liftTermTranslationMonad ::
   (forall n. TermTranslation.TermTranslationMonad   n => n a) ->
   (forall m. ModuleTranslationMonad m => m a)
 liftTermTranslationMonad n = do
-  configuration <- ask
-  cur_mod <- view currentModule <$> get
-  let r = TermTranslation.runTermTranslationMonad configuration cur_mod [] [] n
+  configuration <- asks translationConfiguration
+  configReader <- asks otherConfiguration
+  let r = TermTranslation.runTermTranslationMonad configuration configReader [] [] n
   case r of
     Left  e      -> Except.throwError e
     Right (a, _) -> do
       return a
 
-translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc ann
+translateDecl ::
+  M.TranslationConfiguration ->
+  Maybe ModuleName ->
+  ModuleDecl ->
+  Doc ann
 translateDecl configuration modname decl =
   case decl of
   TypeDecl td -> do

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -25,7 +25,7 @@ Portability : portable
 module Verifier.SAW.Translation.Coq.SpecialTreatment where
 
 import           Control.Lens                       (_1, _2, over)
-import           Control.Monad.Reader               (ask)
+import           Control.Monad.Reader               (asks)
 import qualified Data.Map                           as Map
 import           Data.String.Interpolate            (i)
 import qualified Data.Text                          as Text
@@ -70,10 +70,10 @@ translateModuleName mn =
   Map.findWithDefault mn mn moduleRenamingMap
 
 findSpecialTreatment ::
-  TranslationConfigurationMonad m =>
+  TranslationConfigurationMonad r m =>
   Ident -> m IdentSpecialTreatment
 findSpecialTreatment ident = do
-  configuration <- ask
+  configuration <- asks translationConfiguration
   let moduleMap =
         Map.findWithDefault Map.empty (identModule ident) (specialTreatmentMap configuration)
   let defaultTreatment =