Merge pull request #1330 from msaaltink/print-sharing-control

Print sharing control

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

@@ -99,12 +99,13 @@ type SawDoc = Doc SawStyle
 data PPOpts = PPOpts { ppBase :: Int
                      , ppColor :: Bool
                      , ppShowLocalNames :: Bool
-                     , ppMaxDepth :: Maybe Int }
+                     , ppMaxDepth :: Maybe Int
+                     , ppMinSharing :: Int }
 
 -- | Default options for pretty-printing
 defaultPPOpts :: PPOpts
 defaultPPOpts = PPOpts { ppBase = 10, ppColor = False,
-                         ppShowLocalNames = True, ppMaxDepth = Nothing }
+                         ppShowLocalNames = True, ppMaxDepth = Nothing, ppMinSharing = 2 }
 
 -- | Options for printing with a maximum depth
 depthPPOpts :: Int -> PPOpts
@@ -575,16 +576,18 @@ shouldMemoizeTerm t =
 -- let-bindings for the entries in the memoization table. If the flag is true,
 -- compute a global table, otherwise compute a local table.
 ppTermWithMemoTable :: Prec -> Bool -> Term -> PPM SawDoc
-ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where
+ppTermWithMemoTable prec global_p trm = do
+     min_occs <- ppMinSharing <$> ppOpts <$> ask
+     ppLets (occ_map_elems min_occs) [] where
 
   -- Generate an occurrence map for trm, filtering out terms that only occur
   -- once, that are "too small" to memoize, and, for the global table, terms
   -- that are not closed
-  occ_map_elems =
+  occ_map_elems min_occs =
     IntMap.assocs $
     IntMap.filter
     (\(t,cnt) ->
-      cnt > 1 && shouldMemoizeTerm t &&
+      cnt >= min_occs && shouldMemoizeTerm t &&
       (if global_p then looseVars t == emptyBitSet else True)) $
     scTermCount global_p trm
 

src/SAWScript/Interpreter.hs

@@ -620,6 +620,11 @@ set_color b = do
   let b' = b && useColor opts
   putTopLevelRW rw { rwPPOpts = (rwPPOpts rw) { ppOptsColor = b' } }
 
+set_min_sharing :: Int -> TopLevel ()
+set_min_sharing b = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwPPOpts = (rwPPOpts rw) { ppOptsMinSharing = b } }
+
 print_value :: Value -> TopLevel ()
 print_value (VString s) = printOutLnTop Info (Text.unpack s)
 print_value (VTerm t) = do
@@ -811,6 +816,12 @@ primitives = Map.fromList
     Current
     [ "Select whether to pretty-print SAWCore terms using color." ]
 
+  , prim "set_min_sharing"     "Int -> TopLevel ()"
+    (pureVal set_min_sharing)
+    Current
+    [ "Set the number times a subterm must be shared for it to be"
+    ,  "let-bound in printer output." ]
+
   , prim "set_timeout"         "Int -> ProofScript ()"
     (pureVal set_timeout)
     Experimental

src/SAWScript/Value.hs

@@ -208,10 +208,11 @@ data PPOpts = PPOpts
   , ppOptsAscii :: Bool
   , ppOptsBase :: Int
   , ppOptsColor :: Bool
+  , ppOptsMinSharing :: Int
   }
 
 defaultPPOpts :: PPOpts
-defaultPPOpts = PPOpts False False 10 False
+defaultPPOpts = PPOpts False False 10 False 2
 
 cryptolPPOpts :: PPOpts -> C.PPOpts
 cryptolPPOpts opts =
@@ -225,6 +226,7 @@ sawPPOpts opts =
   SAWCorePP.defaultPPOpts
     { SAWCorePP.ppBase = ppOptsBase opts
     , SAWCorePP.ppColor = ppOptsColor opts
+    , SAWCorePP.ppMinSharing = ppOptsMinSharing opts
     }
 
 quietEvalOpts :: C.EvalOpts