bunch of small cleanups (#2015)

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

@@ -22,7 +22,7 @@ import Prelude hiding ((<$>), (<>))
 -- @""@, i.e., two copies of it, as this is how Coq escapes double quote
 -- characters.
 escapeStringLit :: String -> String
-escapeStringLit = concat . map (\c -> if c == '"' then "\"\"" else [c])
+escapeStringLit = concatMap (\c -> if c == '"' then "\"\"" else [c])
 
 text :: String -> Doc ann
 text = pretty
@@ -99,11 +99,11 @@ ppTerm p e =
   case e of
     Lambda bs t ->
       parensIf (p > PrecLambda) $
-      (text "fun" <+> ppBinders bs <+> text "=>" <+> ppTerm PrecLambda t)
+      text "fun" <+> ppBinders bs <+> text "=>" <+> ppTerm PrecLambda t
     Fix ident binders returnType body ->
       parensIf (p > PrecLambda) $
-      (text "fix" <+> text ident <+> ppBinders binders <+> text ":"
-             <+> ppTerm PrecNone returnType <+> text ":=" <+> ppTerm PrecLambda body)
+      text "fix" <+> text ident <+> ppBinders binders <+> text ":"
+        <+> ppTerm PrecNone returnType <+> text ":=" <+> ppTerm PrecLambda body
     Pi bs t ->
       parensIf (p > PrecLambda) $
       ppPi bs <+> ppTerm PrecLambda t
@@ -156,24 +156,28 @@ ppTerm p e =
 ppDecl :: Decl -> Doc ann
 ppDecl decl = case decl of
   Axiom nm ty ->
-    (nest 2 $
-     hsep ([text "Axiom", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+    nest 2 (
+      hsep [text "Axiom", text nm, text ":", ppTerm PrecNone ty, period]
+    ) <> hardline
   Parameter nm ty ->
-    (nest 2 $
-     hsep ([text "Parameter", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+    nest 2 (
+     hsep [text "Parameter", text nm, text ":", ppTerm PrecNone ty, period]
+    ) <> hardline
   Variable nm ty ->
-    (nest 2 $
-     hsep ([text "Variable", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+    nest 2 (
+      hsep [text "Variable", text nm, text ":", ppTerm PrecNone ty, period]
+    ) <> hardline
   Comment s ->
     text "(*" <+> text s <+> text "*)" <> hardline
   Definition nm bs mty body ->
-    (nest 2 $
-     vsep
-     [ hsep ([text "Definition", text nm] ++
-            map ppBinder bs ++
-            [ppMaybeTy mty, text ":="])
-     , ppTerm PrecNone body <> period
-     ]) <> hardline
+    nest 2 (
+      vsep
+      [ hsep ([text "Definition", text nm] ++
+             map ppBinder bs ++
+             [ppMaybeTy mty, text ":="])
+      , ppTerm PrecNone body <> period
+      ]
+    ) <> hardline
   InductiveDecl ind -> ppInductive ind
   Section nm ds ->
     vsep $ concat
@@ -186,12 +190,11 @@ ppDecl decl = case decl of
 ppConstructor :: Constructor -> Doc ann
 ppConstructor (Constructor {..}) =
   nest 2 $
-  hsep ([ text "|"
-        , text constructorName
-        , text ":"
-        , ppTerm PrecNone constructorType
-        ]
-       )
+  hsep [ text "|"
+       , text constructorName
+       , text ":"
+       , ppTerm PrecNone constructorType
+       ]
 
 ppInductive :: Inductive -> Doc ann
 ppInductive (Inductive {..}) =

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

@@ -38,56 +38,6 @@ import           Verifier.SAW.Translation.Coq.SpecialTreatment
 import qualified Verifier.SAW.Translation.Coq.Term             as TermTranslation
 import           Verifier.SAW.TypedTerm
 import           Verifier.SAW.Cryptol (Env)
---import Verifier.SAW.Term.Pretty
--- import qualified Verifier.SAW.UntypedAST as Un
-
---import Debug.Trace
-
--- showFTermF :: FlatTermF Term -> String
--- showFTermF = show . Unshared . FTermF
-
--- mkCoqIdent :: String -> String -> Ident
--- mkCoqIdent coqModule coqIdent = mkIdent (mkModuleName [coqModule]) coqIdent
-
-{-
-traceFTermF :: String -> FlatTermF Term -> a -> a
-traceFTermF ctx tf = traceTerm ctx (Unshared $ FTermF tf)
-
-traceTerm :: String -> Term -> a -> a
-traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a
--}
-
--- translateBinder ::
---   TermTranslationMonad m =>
---   (Ident, Term) -> m (Coq.Ident, Coq.Term)
--- translateBinder (ident, term) =
---   (,)
---   <$> pure (translateIdent ident)
---   <*> translateTerm term
-
--- dropModuleName :: String -> String
--- dropModuleName s =
---   case elemIndices '.' s of
---   [] -> s
---   indices ->
---     let lastIndex = last indices in
---     drop (lastIndex + 1) s
-
--- unqualifyTypeWithinConstructor :: Coq.Term -> Coq.Term
--- unqualifyTypeWithinConstructor = go
---   where
---     go (Coq.Pi bs t)  = Coq.Pi bs (go t)
---     go (Coq.App t as) = Coq.App (go t) as
---     go (Coq.Var v)    = Coq.Var (dropModuleName v)
---     go t              = error $ "Unexpected term in constructor: " ++ show t
-
--- | This is a convenient helper for when you want to add some bindings before
--- translating a term.
--- translateTermLocallyBinding :: ModuleTranslationMonad m => [String] -> Term -> m Coq.Term
--- translateTermLocallyBinding bindings term =
---   withLocalEnvironment $ do
---   modify $ over environment (bindings ++)
---   translateTerm term
 
 text :: String -> Doc ann
 text = pretty
@@ -148,9 +98,9 @@ translateCryptolModule ::
   [String] ->
   CryptolModule ->
   IO (Either (TranslationError Term) (Doc ann))
-translateCryptolModule sc env nm configuration globalDecls m =
-  fmap (fmap (Coq.ppDecl . Coq.Section nm)) $
-  CMT.translateCryptolModule sc env configuration globalDecls m
+translateCryptolModule sc env nm configuration globalDecls m = do
+  translated <- CMT.translateCryptolModule sc env configuration globalDecls m
+  return $ Coq.ppDecl . Coq.Section (escapeIdent nm) <$> translated
 
 -- | Extract out the 'String' name of a declaration in a SAW core module
 moduleDeclName :: ModuleDecl -> Maybe String

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

@@ -731,7 +731,7 @@ ppTerm opts = ppTermWithNames opts emptySAWNamingEnv
 
 -- | Pretty-print a term, but only to a maximum depth
 ppTermDepth :: Int -> Term -> SawDoc
-ppTermDepth depth t = ppTerm (depthPPOpts depth) t
+ppTermDepth depth = ppTerm (depthPPOpts depth)
 
 -- | Like 'ppTerm', but also supply a context of bound names, where the most
 -- recently-bound variable is listed first in the context