Coq section

saw-core-coq/src/Language/Coq/AST.hs

@@ -73,5 +73,6 @@ data Decl
   | Parameter Ident Type
   | Variable Ident Type
   | InductiveDecl Inductive
+  | Section Ident [Decl]
   | Snippet String
   deriving (Show)

saw-core-coq/src/Language/Coq/Pretty.hs

@@ -163,6 +163,12 @@ ppDecl decl = case decl of
      , ppTerm PrecNone body <> period
      ]) <> hardline
   InductiveDecl ind -> ppInductive ind
+  Section nm ds ->
+    vsep $ concat
+     [ [ hsep [text "Section", text nm, period] ]
+     , map (indent 2 . ppDecl) ds
+     , [ hsep [text "End", text nm, period] ]
+     ]
   Snippet s -> text s
 
 ppConstructor :: Constructor -> Doc ann

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

@@ -135,18 +135,19 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
+  Coq.Ident {- ^ Section name -} ->
   TranslationConfiguration ->
   -- | List of already translated global declarations
   [String] ->
   CryptolModule ->
   Either (TranslationError Term) (Doc ann)
-translateCryptolModule configuration globalDecls m =
+translateCryptolModule nm configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration
               globalDecls
               m
   in
-  vcat . map Coq.ppDecl <$> decls
+  Coq.ppDecl . Coq.Section nm <$> decls
 
 moduleDeclName :: ModuleDecl -> String
 moduleDeclName (TypeDecl (DataType { dtName })) = identName dtName

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

@@ -136,6 +136,7 @@ namedDecls = concatMap filterNamed
     filterNamed (Coq.Definition n _ _ _)                      = [n]
     filterNamed (Coq.InductiveDecl (Coq.Inductive n _ _ _ _)) = [n]
     filterNamed (Coq.Snippet _)                               = []
+    filterNamed (Coq.Section _ ds)                            = namedDecls ds
 
 -- | Retrieve the names of all local and global declarations from the
 -- translation state.
@@ -616,7 +617,7 @@ translateTermUnshared t = withLocalTranslationState $ do
               modify $ set sharedNames IntMap.empty
               modify $ set nextSharedName "var__0"
               translateTermLet (ecType n)
-          modify $ over topLevelDeclarations $ (Coq.Parameter renamed tp :)
+          modify $ over topLevelDeclarations $ (Coq.Variable renamed tp :)
           Coq.Var <$> pure renamed
 
     -- Constants with a body

saw-core/src/Verifier/SAW/Term/Pretty.hs

@@ -547,11 +547,17 @@ scTermCount doBinders t0 = execState (go [t0]) IntMap.empty
         argsAndSubterms (unwrapTermF -> App f arg) = arg : argsAndSubterms f
         argsAndSubterms h =
           case unwrapTermF h of
-            Lambda _ t1 _ | not doBinders -> [t1]
-            Pi _ t1 _     | not doBinders -> [t1]
-            Constant{}                    -> []
-            FTermF (Primitive _)          -> []
-            tf                            -> Fold.toList tf
+            Lambda _ t1 _ | not doBinders  -> [t1]
+            Pi _ t1 _     | not doBinders  -> [t1]
+            Constant{}                     -> []
+            FTermF (Primitive _)           -> []
+            FTermF (DataTypeApp _ ps xs)   -> ps ++ xs
+            FTermF (CtorApp _ ps xs)       -> ps ++ xs
+            FTermF (RecursorType _ ps m _) -> ps ++ [m]
+            FTermF (Recursor crec)         -> recursorParams crec ++
+                                              [recursorMotive crec] ++
+                                              map fst (Map.elems (recursorElims crec))
+            tf                             -> Fold.toList tf
 
 -- | Return true if the printing of the given term should be memoized; we do not
 -- want to memoize the printing of terms that are "too small"

src/SAWScript/Prover/Exporter.hs

@@ -479,7 +479,8 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
         withImportCryptolPrimitivesForSAWCore $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
-  case Coq.translateCryptolModule configuration cryptolPreludeDecls cm of
+  let nm = takeBaseName inputFile
+  case Coq.translateCryptolModule nm configuration cryptolPreludeDecls cm of
     Left e -> putStrLn $ show e
     Right cmDoc ->
       writeFile outputFile