From d45a35444a6e115c6b0b194a7072ae73bf1ccc5b Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 28 Sep 2021 12:29:17 -0700 Subject: [PATCH 1/2] When exporting a Cryptol module to Coq, wrap the module in a section, and translate `primitive` declarations into section `Variable` declarations instead of using top-level parameters. --- saw-core-coq/src/Language/Coq/AST.hs | 1 + saw-core-coq/src/Language/Coq/Pretty.hs | 6 ++++++ saw-core-coq/src/Verifier/SAW/Translation/Coq.hs | 5 +++-- saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs | 3 ++- src/SAWScript/Prover/Exporter.hs | 3 ++- 5 files changed, 14 insertions(+), 4 deletions(-) diff --git a/saw-core-coq/src/Language/Coq/AST.hs b/saw-core-coq/src/Language/Coq/AST.hs index e70f780f11..51ef098116 100644 --- a/saw-core-coq/src/Language/Coq/AST.hs +++ b/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) diff --git a/saw-core-coq/src/Language/Coq/Pretty.hs b/saw-core-coq/src/Language/Coq/Pretty.hs index c3d04bd471..e80c4ab651 100644 --- a/saw-core-coq/src/Language/Coq/Pretty.hs +++ b/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 diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs index 34dfc2d7b6..7efef1fc85 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs +++ b/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 diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs index 8911e46e66..581ab83704 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/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 diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index a20009627b..780ca6aa8e 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/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 From 020b09abf6abf7e108a759a565d46e7474a058b8 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 28 Sep 2021 12:30:51 -0700 Subject: [PATCH 2/2] When pretty printing terms skip counting more terms that will not be included in the eventual printed term. This avoids more instances where terms become "let" bound that appear not to be referenced in the printed term. --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index af3eed6832..758c1d5a8b 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/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"