Shared term pretty printers now take a PPOpts argument with a number-…

…base.

Fixes #93.

src/SAWScript/Builtins.hs

@@ -425,14 +425,36 @@ trivial = StateT $ \goal -> do
         FTermF (CtorApp "Prelude.True" []) -> return ()
         _ -> fail "trivial: not a trivial goal"
 
+getTopLevelPPOpts :: TopLevel PPOpts
+getTopLevelPPOpts = do
+  rw <- getTopLevelRW
+  return defaultPPOpts { ppBase = SV.ppOptsBase (rwPPOpts rw) }
+
+show_term :: SharedTerm SAWCtx -> TopLevel String
+show_term t = do
+  opts <- getTopLevelPPOpts
+  return (scPrettyTerm opts t)
+
+print_term :: SharedTerm SAWCtx -> TopLevel ()
+print_term t = do
+  opts <- getTopLevelPPOpts
+  io $ putStrLn (scPrettyTerm opts t)
+
+print_term_depth :: Int -> SharedTerm SAWCtx -> TopLevel ()
+print_term_depth d t = do
+  opts <- getTopLevelPPOpts
+  io $ print (ppTermDepth opts d t)
+
 printGoal :: ProofScript s ()
 printGoal = StateT $ \goal -> do
-  io $ putStrLn (scPrettyTerm (ttTerm (goalTerm goal)))
+  opts <- getTopLevelPPOpts
+  io $ putStrLn (scPrettyTerm opts (ttTerm (goalTerm goal)))
   return ((), goal)
 
 printGoalDepth :: Int -> ProofScript SAWCtx ()
 printGoalDepth n = StateT $ \goal -> do
-  io $ print (ppTermDepth n (ttTerm (goalTerm goal)))
+  opts <- getTopLevelPPOpts
+  io $ print (ppTermDepth opts n (ttTerm (goalTerm goal)))
   return ((), goal)
 
 printGoalConsts :: ProofScript SAWCtx ()

src/SAWScript/ImportAIG.hs

@@ -65,7 +65,7 @@ bitblastSharedTerm sc v (asBitvectorType -> Just w) = do
   modify (V.++ inputs)
 bitblastSharedTerm _ _ tp = throwTP $ show $
   text "Could not parse AIG input type:" <$$>
-  indent 2 (scPrettyTermDoc tp)
+  indent 2 (scPrettyTermDoc defaultPPOpts tp)
 
 parseAIGResultType :: SharedContext s
                    -> SharedTerm s -- ^ Term for type

src/SAWScript/Interpreter.hs

@@ -367,7 +367,7 @@ buildTopLevelEnv opts =
                    , rwTypes    = primTypeEnv
                    , rwDocs     = primDocEnv
                    , rwCryptol  = ce0
-                   , rwPPOpts   = defaultPPOpts
+                   , rwPPOpts   = SAWScript.Value.defaultPPOpts
                    }
        return (bic, ro0, rw0)
 
@@ -529,11 +529,11 @@ primitives = Map.fromList
     [ "Print the value of the given expression." ]
 
   , prim "print_term"          "Term -> TopLevel ()"
-    (pureVal ((putStrLn . scPrettyTerm) :: SharedTerm SAWCtx -> IO ()))
+    (pureVal print_term)
     [ "Pretty-print the given term in SAWCore syntax." ]
 
   , prim "print_term_depth"    "Int -> Term -> TopLevel ()"
-    (pureVal ((\d -> print . ppTermDepth d) :: Int -> SharedTerm SAWCtx -> IO ()))
+    (pureVal print_term_depth)
     [ "Pretty-print the given term in SAWCore syntax up to a given depth." ]
 
   , prim "dump_file_AST"       "String -> TopLevel ()"
@@ -555,7 +555,7 @@ primitives = Map.fromList
     [ "Return the type of the given term." ]
 
   , prim "show_term"           "Term -> String"
-    (pureVal (scPrettyTerm :: SharedTerm SAWCtx -> String))
+    (funVal1 show_term)
     [ "Pretty-print the given term in SAWCore syntax, yielding a String." ]
 
   , prim "check_term"          "Term -> TopLevel ()"

src/SAWScript/JavaMethodSpec.hs

@@ -445,7 +445,7 @@ runValidation prover params sc results = do
        g <- io $ scImplies sc (pvcAssumptions pvc) =<< vcGoal sc vc
        when (verb >= 2) $ io $ do
          putStr $ "Checking " ++ vcName vc
-         when (verb >= 5) $ putStr $ " (" ++ scPrettyTerm g ++ ")"
+         when (verb >= 5) $ putStr $ " (" ++ scPrettyTerm defaultPPOpts g ++ ")"
          putStrLn ""
        prover vs g
     else do
@@ -458,7 +458,7 @@ runValidation prover params sc results = do
         print $ pvcStaticErrors pvc
       when (verb >= 5) $ io $ do
         putStrLn $ "Calling prover to disprove " ++
-                 scPrettyTerm (pvcAssumptions pvc)
+                 scPrettyTerm defaultPPOpts (pvcAssumptions pvc)
       prover vs g
 
 data VerifyState = VState {

src/SAWScript/JavaMethodSpecIR.hs

@@ -140,7 +140,7 @@ data BehaviorSpec = BS {
 ppLogicExpr :: LogicExpr -> Doc
 ppLogicExpr (LogicExpr t args) =
   vcat $
-  parens (scPrettyTermDoc t) :
+  parens (scPrettyTermDoc defaultPPOpts t) :
   map (text . ppJavaExpr) args
 
 ppMixedExpr :: MixedExpr -> Doc

src/SAWScript/LLVMMethodSpec.hs

@@ -785,7 +785,7 @@ runValidation prover params sc esd results = do
         putStrLn $ "Checking " ++ vsName
         print $ pvcStaticErrors pvc
         putStrLn $ "Calling prover to disprove " ++
-                 scPrettyTerm (pvcAssumptions pvc)
+                 scPrettyTerm defaultPPOpts (pvcAssumptions pvc)
       prover vs g
 
 data VerifyState = VState {

src/SAWScript/PathVC.hs

@@ -32,7 +32,7 @@ ppPathVC pvc =
   vcat [ text "Path VC:"
        , nest 2 $
          vcat [ text "Assumptions:"
-              , scPrettyTermDoc (pvcAssumptions pvc)
+              , scPrettyTermDoc defaultPPOpts (pvcAssumptions pvc)
               ]
        , nest 2 $ vcat $
          text "Static errors:" :

src/SAWScript/Value.hs

@@ -46,7 +46,8 @@ import SAWScript.SAWCorePrimitives( concretePrimitives )
 
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Rewriter ( Simpset )
-import Verifier.SAW.SharedTerm
+import Verifier.SAW.SharedTerm hiding (PPOpts(..), defaultPPOpts)
+import qualified Verifier.SAW.SharedTerm as SharedTerm (PPOpts(..), defaultPPOpts)
 
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import qualified Cryptol.Eval.Value as C
@@ -190,7 +191,7 @@ showsSatResult opts r =
     showMulti s (eqn : eqns) = showString s . showEqn eqn . showMulti ", " eqns
 
 showsPrecValue :: PPOpts -> Int -> Value -> ShowS
-showsPrecValue opts p v =
+showsPrecValue opts _p v =
   case v of
     VBool True -> showString "true"
     VBool False -> showString "false"
@@ -204,14 +205,14 @@ showsPrecValue opts p v =
                        showString n . showString "=" . showsPrecValue opts 0 fv
 
     VLambda {} -> showString "<<function>>"
-    VTerm t -> showsPrec p (ttTerm t)
+    VTerm t -> showString (scPrettyTerm opts' (ttTerm t))
     VType sig -> showString (pretty sig)
     VReturn {} -> showString "<<monadic>>"
     VBind {} -> showString "<<monadic>>"
     VTopLevel {} -> showString "<<TopLevel>>"
     VSimpset {} -> showString "<<simpset>>"
     VProofScript {} -> showString "<<proof script>>"
-    VTheorem (Theorem t) -> showString "Theorem " . showParen True (showString (scPrettyTerm (ttTerm t)))
+    VTheorem (Theorem t) -> showString "Theorem " . showParen True (showString (scPrettyTerm opts' (ttTerm t)))
     VJavaSetup {} -> showString "<<Java Setup>>"
     VLLVMSetup {} -> showString "<<LLVM Setup>>"
     VJavaMethodSpec ms -> shows (JIR.ppMethodSpec ms)
@@ -225,6 +226,8 @@ showsPrecValue opts p v =
     VSatResult r -> showsSatResult opts r
     VUninterp u -> showString "Uninterp: " . shows u
     VAIG _ -> showString "<<AIG>>"
+  where
+    opts' = SharedTerm.defaultPPOpts { SharedTerm.ppBase = ppOptsBase opts }
 
 instance Show Value where
     showsPrec p v = showsPrecValue defaultPPOpts p v

src/SAWScript/VerificationCheck.hs

@@ -40,7 +40,7 @@ type CounterexampleFn s = (SharedTerm s -> IO CValue) -> IO Doc
 vcCounterexample :: SharedContext s -> VerificationCheck s -> CounterexampleFn s
 vcCounterexample _ (AssertionCheck nm n) _ =
   return $ text ("Assertion " ++ nm ++ " is unsatisfied:") <+>
-           scPrettyTermDoc n
+           scPrettyTermDoc defaultPPOpts n
 vcCounterexample sc (EqualityCheck nm impNode specNode) evalFn =
   do ln <- evalFn impNode
      sn <- evalFn specNode
@@ -63,11 +63,11 @@ vcCounterexample sc (EqualityCheck nm impNode specNode) evalFn =
 ppCheck :: VerificationCheck s -> Doc
 ppCheck (AssertionCheck nm tm) =
   hsep [ text (nm ++ ":")
-       , scPrettyTermDoc tm
+       , scPrettyTermDoc defaultPPOpts tm
        ]
 ppCheck (EqualityCheck nm tm tm') =
   hsep [ text (nm ++ ":")
-       , scPrettyTermDoc tm
+       , scPrettyTermDoc defaultPPOpts tm
        , text ":="
-       , scPrettyTermDoc tm'
+       , scPrettyTermDoc defaultPPOpts tm'
        ]