Merge pull request #28 from GaloisInc/prettyprinter

Convert from `ansi-wl-pprint` package to `prettyprinter`.

saw-core-coq.cabal

@@ -15,14 +15,14 @@ description:
 
 library
   build-depends:
-    ansi-wl-pprint,
     base == 4.*,
     cryptol,
     cryptol-saw-core,
     containers,
     interpolate,
     lens,
     mtl,
+    prettyprinter,
     saw-core,
     text,
     vector

src/Language/Coq/Pretty.hs

@@ -11,54 +11,64 @@ Portability : portable
 
 module Language.Coq.Pretty where
 
-import Text.PrettyPrint.ANSI.Leijen
+import Prettyprinter
+
 import Language.Coq.AST
 import Prelude hiding ((<$>), (<>))
 
+text :: String -> Doc ann
+text = pretty
+
+string :: String -> Doc ann
+string = pretty
+
+integer :: Integer -> Doc ann
+integer = pretty
+
 -- TODO: import SAWCore pretty-printer?
-tightSepList :: Doc -> [Doc] -> Doc
-tightSepList _ [] = empty
+tightSepList :: Doc ann -> [Doc ann] -> Doc ann
+tightSepList _ [] = mempty
 tightSepList _ [d] = d
 tightSepList s (d:l) = d <> s <+> tightSepList s l
 
-looseSepList :: Doc -> [Doc] -> Doc
-looseSepList _ [] = empty
+looseSepList :: Doc ann -> [Doc ann] -> Doc ann
+looseSepList _ [] = mempty
 looseSepList _ [d] = d
 looseSepList s (d:l) = d <+> s <+> looseSepList s l
 
-commaSepList, starSepList, semiSepList :: [Doc] -> Doc
+commaSepList, starSepList, semiSepList :: [Doc ann] -> Doc ann
 commaSepList = tightSepList comma
 starSepList = looseSepList (text "*")
 semiSepList = tightSepList semi
 
-period :: Doc
+period :: Doc ann
 period = text "."
 
-ppIdent :: Ident -> Doc
+ppIdent :: Ident -> Doc ann
 ppIdent = text
 
-ppBinder :: Binder -> Doc
+ppBinder :: Binder -> Doc ann
 ppBinder (Binder x Nothing)  = ppIdent x
 ppBinder (Binder x (Just t)) = parens (ppIdent x <+> colon <+> ppTerm PrecNone t)
 
-ppPiBinder :: PiBinder -> Doc
+ppPiBinder :: PiBinder -> Doc ann
 ppPiBinder (PiBinder Nothing t)  = ppTerm PrecApp t <+> text "->"
 ppPiBinder (PiBinder (Just x) t) =
   text "forall" <+> parens (ppIdent x <+> colon <+> ppTerm PrecNone t) <> comma
 
-ppBinders :: [Binder] -> Doc
+ppBinders :: [Binder] -> Doc ann
 ppBinders = hsep . map ppBinder
 
-ppMaybeTy :: Maybe Type -> Doc
-ppMaybeTy Nothing = empty
+ppMaybeTy :: Maybe Type -> Doc ann
+ppMaybeTy Nothing = mempty
 ppMaybeTy (Just ty) = colon <+> ppTerm PrecNone ty
 
-ppSort :: Sort -> Doc
+ppSort :: Sort -> Doc ann
 ppSort Prop = text "Prop"
 ppSort Set = text "Set"
 ppSort Type = text "Type"
 
-ppPi :: [PiBinder] -> Doc
+ppPi :: [PiBinder] -> Doc ann
 ppPi bs = hsep (map ppPiBinder bs)
 
 data Prec
@@ -68,10 +78,10 @@ data Prec
   | PrecAtom
   deriving (Eq, Ord)
 
-parensIf :: Bool -> Doc -> Doc
+parensIf :: Bool -> Doc ann -> Doc ann
 parensIf p d = if p then parens d else d
 
-ppTerm :: Prec -> Term -> Doc
+ppTerm :: Prec -> Term -> Doc ann
 ppTerm p e =
   case e of
     Lambda bs t ->
@@ -86,8 +96,10 @@ ppTerm p e =
       ppPi bs <+> ppTerm PrecLambda t
     Let x bs mty t body ->
       parensIf (p > PrecLambda) $
-      text "let" <+> ppIdent x <+> ppBinders bs <+> ppMaybeTy mty <+>
-      text ":=" <+> ppTerm PrecNone t <+> text "in" </> ppTerm PrecLambda body
+      fillSep
+      [ text "let" <+> ppIdent x <+> ppBinders bs <+> ppMaybeTy mty <+>
+        text ":=" <+> ppTerm PrecNone t <+> text "in"
+      , ppTerm PrecLambda body ]
     If c t f ->
       parensIf (p > PrecLambda) $
       text "if" <+> ppTerm PrecNone c <+>
@@ -113,7 +125,7 @@ ppTerm p e =
     Ltac s ->
       text "ltac:" <> parens (string s)
 
-ppDecl :: Decl -> Doc
+ppDecl :: Decl -> Doc ann
 ppDecl decl = case decl of
   Axiom nm ty ->
     (nest 2 $
@@ -122,14 +134,16 @@ ppDecl decl = case decl of
     text "(*" <+> text s <+> text "*)" <> hardline
   Definition nm bs mty body ->
     (nest 2 $
-     hsep ([text "Definition", text nm] ++
-          map ppBinder bs ++
-          [ppMaybeTy mty, text ":="]) <$>
-     ppTerm PrecNone body <> period) <> hardline
+     vsep
+     [ hsep ([text "Definition", text nm] ++
+            map ppBinder bs ++
+            [ppMaybeTy mty, text ":="])
+     , ppTerm PrecNone body <> period
+     ]) <> hardline
   InductiveDecl ind -> ppInductive ind
   Snippet s -> text s
 
-ppConstructor :: Constructor -> Doc
+ppConstructor :: Constructor -> Doc ann
 ppConstructor (Constructor {..}) =
   nest 2 $
   hsep ([ text "|"
@@ -139,7 +153,7 @@ ppConstructor (Constructor {..}) =
         ]
        )
 
-ppInductive :: Inductive -> Doc
+ppInductive :: Inductive -> Doc ann
 ppInductive (Inductive {..}) =
   (vsep
    ([ nest 2 $

src/Verifier/SAW/Translation/Coq.hs

@@ -25,7 +25,7 @@ module Verifier.SAW.Translation.Coq (
 import           Control.Monad.Reader                          hiding (fail)
 import           Data.String.Interpolate                       (i)
 import           Prelude                                       hiding (fail)
-import           Text.PrettyPrint.ANSI.Leijen                  hiding ((<$>))
+import           Prettyprinter
 
 import qualified Language.Coq.AST                              as Coq
 import qualified Language.Coq.Pretty                           as Coq
@@ -90,9 +90,12 @@ traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a
 --   modify $ over environment (bindings ++)
 --   translateTerm term
 
+text :: String -> Doc ann
+text = pretty
+
 -- | Eventually, different modules may want different preambles.  For now,
 -- we hardcode a sufficient set of imports for all our purposes.
-preamblePlus :: TranslationConfiguration -> Doc -> Doc
+preamblePlus :: TranslationConfiguration -> Doc ann -> Doc ann
 preamblePlus (TranslationConfiguration {..}) extraImports = text [i|
 From Coq          Require Import Lists.List.
 From Coq          Require Import String.
@@ -105,16 +108,16 @@ From CryptolToCoq Require Import #{vectorModule}.
 Import ListNotations.
 |]
 
-preamble :: TranslationConfiguration -> Doc
+preamble :: TranslationConfiguration -> Doc ann
 preamble configuration = preamblePlus configuration $ vcat []
 
 translateTermAsDeclImports ::
-  TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) Doc
+  TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann)
 translateTermAsDeclImports configuration name t = do
   doc <- TermTranslation.translateDefDoc configuration Nothing [] name t
-  return (preamble configuration <$$> hardline <> doc)
+  return $ vcat [preamble configuration, hardline <> doc]
 
-translateSAWModule :: TranslationConfiguration -> Module -> Doc
+translateSAWModule :: TranslationConfiguration -> Module -> Doc ann
 translateSAWModule configuration m =
   let name = show $ translateModuleName (moduleName m)
   in
@@ -129,7 +132,7 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) Doc
+  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
 translateCryptolModule configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration

src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -29,7 +29,7 @@ import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
 import           Control.Monad.State                           hiding (fail)
 import           Prelude                                       hiding (fail)
-import           Text.PrettyPrint.ANSI.Leijen                  hiding ((<$>))
+import           Prettyprinter                                 (Doc)
 
 import qualified Language.Coq.AST                              as Coq
 import qualified Language.Coq.Pretty                           as Coq
@@ -170,7 +170,7 @@ liftTermTranslationMonad n = do
     Right (a, _) -> do
       return a
 
-translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc
+translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc ann
 translateDecl configuration modname decl =
   case decl of
   TypeDecl td -> do

src/Verifier/SAW/Translation/Coq/Term.hs

@@ -35,7 +35,7 @@ import           Data.List                                     (intersperse, sor
 import           Data.Maybe                                    (fromMaybe)
 import qualified Data.Set                                      as Set
 import           Prelude                                       hiding (fail)
-import           Text.PrettyPrint.ANSI.Leijen                  hiding ((<$>))
+import           Prettyprinter
 
 import qualified Data.Vector                                   as Vector (reverse)
 import qualified Language.Coq.AST                              as Coq
@@ -530,24 +530,26 @@ translateTermToDocWith ::
   Maybe ModuleName ->
   [String] ->
   [String] ->
-  (Coq.Term -> Doc) ->
+  (Coq.Term -> Doc ann) ->
   Term ->
-  Either (TranslationError Term) Doc
+  Either (TranslationError Term) (Doc ann)
 translateTermToDocWith configuration mn globalDecls localEnv f t = do
   (term, state) <-
     runTermTranslationMonad configuration mn globalDecls localEnv (translateTermLet t)
   let decls = view localDeclarations state
-  return
-    $ ((vcat . intersperse hardline . map Coq.ppDecl . reverse) decls)
-    <$$> (if null decls then empty else hardline)
-    <$$> f term
+  return $
+    vcat $
+    [ (vcat . intersperse hardline . map Coq.ppDecl . reverse) decls
+    , if null decls then mempty else hardline
+    , f term
+    ]
 
 translateDefDoc ::
   TranslationConfiguration ->
   Maybe ModuleName ->
   [String] ->
   Coq.Ident -> Term ->
-  Either (TranslationError Term) Doc
+  Either (TranslationError Term) (Doc ann)
 translateDefDoc configuration mn globalDecls name =
   translateTermToDocWith configuration mn globalDecls [name]
   (\ term -> Coq.ppDecl (mkDefinition name term))