Merge branch 'master' into bugfix-global-infer-performance

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 =