Skip to content

Commit

Permalink
Merge pull request #106 from GaloisInc/prettyprinter
Browse files Browse the repository at this point in the history
Switch from ansi-wl-pprint to the prettyprinter package.
  • Loading branch information
brianhuffman authored Nov 24, 2020
2 parents ab87ce3 + 056ac76 commit 296bc6d
Show file tree
Hide file tree
Showing 6 changed files with 142 additions and 111 deletions.
1 change: 0 additions & 1 deletion saw-core-what4/saw-core-what4.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ Description:

library
build-depends:
ansi-wl-pprint,
base == 4.*,
bv-sized >= 1.0.0,
containers,
Expand Down
4 changes: 2 additions & 2 deletions saw-core/saw-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ library

build-depends:
base == 4.*,
ansi-wl-pprint,
array,
bytestring,
containers,
Expand All @@ -41,6 +40,8 @@ library
panic,
parameterized-utils,
pretty,
prettyprinter >= 1.7.0,
prettyprinter-ansi-terminal >= 1.1.2,
random,
rme,
template-haskell,
Expand Down Expand Up @@ -118,7 +119,6 @@ test-suite test-sawcore
, time
, unordered-containers
, vector
, ansi-wl-pprint
, QuickCheck >= 2.7
, tasty
, tasty-ant-xml >= 1.1.0
Expand Down
20 changes: 10 additions & 10 deletions saw-core/src/Verifier/SAW/FiniteValue.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ import Data.Map (Map)
import qualified Data.Map as Map
import Numeric.Natural (Natural)

import Prettyprinter hiding (Doc)

import qualified Verifier.SAW.Recognizer as R
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST
import Verifier.SAW.Term.Pretty

import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))

-- | Finite types that can be encoded as bits for a SAT/SMT solver.
data FiniteType
= FTBit
Expand Down Expand Up @@ -102,24 +102,24 @@ instance Show FirstOrderValue where
commaSep ss = foldr (.) id (intersperse (showString ",") ss)
showField (field, v) = showString field . showString " = " . shows v

ppFiniteValue :: PPOpts -> FiniteValue -> Doc
ppFiniteValue :: PPOpts -> FiniteValue -> SawDoc
ppFiniteValue opts fv = ppFirstOrderValue opts (toFirstOrderValue fv)

ppFirstOrderValue :: PPOpts -> FirstOrderValue -> Doc
ppFirstOrderValue :: PPOpts -> FirstOrderValue -> SawDoc
ppFirstOrderValue opts = loop
where
loop fv = case fv of
FOVBit b
| b -> text "True"
| otherwise -> text "False"
FOVInt i -> integer i
FOVIntMod _ i -> integer i
| b -> pretty "True"
| otherwise -> pretty "False"
FOVInt i -> pretty i
FOVIntMod _ i -> pretty i
FOVWord _w i -> ppNat opts i
FOVVec _ xs -> brackets (sep (punctuate comma (map loop xs)))
FOVArray{} -> text $ show $ firstOrderTypeOf fv
FOVArray{} -> viaShow $ firstOrderTypeOf fv
FOVTuple xs -> parens (sep (punctuate comma (map loop xs)))
FOVRec xs -> braces (sep (punctuate comma (map ppField (Map.toList xs))))
where ppField (f,x) = pretty f <+> char '=' <+> loop x
where ppField (f,x) = pretty f <+> pretty '=' <+> loop x


-- | Smart constructor
Expand Down
3 changes: 1 addition & 2 deletions saw-core/src/Verifier/SAW/Module.hs
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,6 @@ import qualified Data.Map.Strict as Map
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import GHC.Generics (Generic)
import Text.PrettyPrint.ANSI.Leijen (Doc)

import qualified Language.Haskell.TH.Syntax as TH

Expand Down Expand Up @@ -468,7 +467,7 @@ allModuleCtors modmap = concatMap moduleCtors (HMap.elems modmap)


-- | Pretty-print a 'Module'
ppModule :: PPOpts -> Module -> Doc
ppModule :: PPOpts -> Module -> SawDoc
ppModule opts m =
ppPPModule opts (PPModule (moduleImportNames m) (map toDecl $ moduleDecls m))
where
Expand Down
Loading

0 comments on commit 296bc6d

Please sign in to comment.