Add new pretty-printer precedence level for comma-separated lists.

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

@@ -114,28 +114,19 @@ depthAllowed _ _ = True
 
 -- | Precedence levels, each of which corresponds to a parsing nonterminal
 data Prec
-  = PrecNone   -- ^ Nonterminal 'Term'
-  | PrecLambda -- ^ Nonterminal 'LTerm'
-  | PrecProd   -- ^ Nonterminal 'ProductTerm'
-  | PrecApp    -- ^ Nonterminal 'AppTerm'
-  | PrecArg    -- ^ Nonterminal 'AtomTerm'
+  = PrecCommas -- ^ Nonterminal @sepBy(Term, \',\')@
+  | PrecTerm   -- ^ Nonterminal @Term@
+  | PrecLambda -- ^ Nonterminal @LTerm@
+  | PrecProd   -- ^ Nonterminal @ProdTerm@
+  | PrecApp    -- ^ Nonterminal @AppTerm@
+  | PrecArg    -- ^ Nonterminal @AtomTerm@
+  deriving (Eq, Ord)
 
 -- | Test if the first precedence "contains" the second, meaning that terms at
 -- the latter precedence level can be printed in the context of the former
 -- without parentheses.
---
--- NOTE: we write this explicitly here, instead of generating it from an 'Ord'
--- instance, so that readers of this code understand it and know what it is.
 precContains :: Prec -> Prec -> Bool
-precContains _ PrecArg = True
-precContains PrecArg _ = False
-precContains _ PrecApp = True
-precContains PrecApp _ = False
-precContains _ PrecProd = True
-precContains PrecProd _ = False
-precContains _ PrecLambda = True
-precContains PrecLambda _ = False
-precContains PrecNone PrecNone = True
+precContains x y = x <= y
 
 -- | Optionally print parentheses around a document, iff the incoming, outer
 -- precedence (listed first) contains (as in 'precContains') the required
@@ -346,7 +337,7 @@ ppLetBlock defs body =
 
 -- | Pretty-print pairs as "(x, y)"
 ppPair :: Prec -> SawDoc -> SawDoc -> SawDoc
-ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> pretty ',', y]))
+ppPair prec x y = ppParensPrec prec PrecCommas (group (vcat [x <> pretty ',', y]))
 
 -- | Pretty-print pair types as "x * y"
 ppPairType :: Prec -> SawDoc -> SawDoc -> SawDoc
@@ -426,7 +417,7 @@ ppFlatTermF prec tf =
     Primitive ec  -> annotate PrimitiveStyle <$> ppBestName (ecName ec)
     UnitValue     -> return "(-empty-)"
     UnitType      -> return "#(-empty-)"
-    PairValue x y -> ppPair prec <$> ppTerm' PrecLambda x <*> ppTerm' PrecNone y
+    PairValue x y -> ppPair prec <$> ppTerm' PrecTerm x <*> ppTerm' PrecCommas y
     PairType x y  -> ppPairType prec <$> ppTerm' PrecApp x <*> ppTerm' PrecProd y
     PairLeft t    -> ppProj "1" <$> ppTerm' PrecArg t
     PairRight t   -> ppProj "2" <$> ppTerm' PrecArg t
@@ -438,7 +429,7 @@ ppFlatTermF prec tf =
     RecursorApp d params p_ret cs_fs ixs arg ->
       do params_pp <- mapM (ppTerm' PrecArg) params
          p_ret_pp <- ppTerm' PrecArg p_ret
-         fs_pp <- mapM (ppTerm' PrecNone . snd) cs_fs
+         fs_pp <- mapM (ppTerm' PrecTerm . snd) cs_fs
          ixs_pp <- mapM (ppTerm' PrecArg) ixs
          arg_pp <- ppTerm' PrecArg arg
          return $
@@ -449,14 +440,14 @@ ppFlatTermF prec tf =
              cs_fs fs_pp]
             ++ ixs_pp ++ [arg_pp])
     RecordType alist ->
-      ppRecord True <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecNone t) alist
+      ppRecord True <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecTerm t) alist
     RecordValue alist ->
-      ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecNone t) alist
+      ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecTerm t) alist
     RecordProj e fld -> ppProj fld <$> ppTerm' PrecArg e
     Sort s -> return $ viaShow s
     NatLit i -> ppNat <$> (ppOpts <$> ask) <*> return (toInteger i)
     ArrayValue _ args   ->
-      ppArrayValue <$> mapM (ppTerm' PrecNone) (V.toList args)
+      ppArrayValue <$> mapM (ppTerm' PrecTerm) (V.toList args)
     StringLit s -> return $ viaShow s
     ExtCns cns -> annotate ExtCnsStyle <$> ppBestName (ecName cns)
 
@@ -618,7 +609,7 @@ ppWithBoundCtx [] m = (mempty ,) <$> m
 ppWithBoundCtx ((x,tp):ctx) m =
   (\tp_d (x', (ctx_d, ret)) ->
     (parens (ppTypeConstraint (pretty x') tp_d) <+> ctx_d, ret))
-  <$> ppTerm' PrecNone tp <*> withBoundVarM x (ppWithBoundCtx ctx m)
+  <$> ppTerm' PrecTerm tp <*> withBoundVarM x (ppWithBoundCtx ctx m)
 
 -- | Pretty-print a term, also adding let-bindings for all subterms that occur
 -- more than once at the same binding level
@@ -635,7 +626,7 @@ ppTermInCtx :: PPOpts -> [LocalName] -> Term -> SawDoc
 ppTermInCtx opts ctx trm =
   runPPM opts emptySAWNamingEnv $
   flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $
-  ppTermWithMemoTable PrecNone True trm
+  ppTermWithMemoTable PrecTerm True trm
 
 renderSawDoc :: PPOpts -> SawDoc -> String
 renderSawDoc ppOpts doc =
@@ -656,7 +647,7 @@ scPrettyTermInCtx opts ctx trm =
   renderSawDoc opts $
   runPPM opts emptySAWNamingEnv $
   flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $
-  ppTermWithMemoTable PrecNone False trm
+  ppTermWithMemoTable PrecTerm False trm
 
 
 -- | Pretty-print a term and render it to a string
@@ -672,7 +663,7 @@ showTerm t = scPrettyTerm defaultPPOpts t
 -- more than once at the same binding level
 ppTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> SawDoc
 ppTermWithNames opts ne trm =
-  runPPM opts ne $ ppTermWithMemoTable PrecNone True trm
+  runPPM opts ne $ ppTermWithMemoTable PrecTerm True trm
 
 showTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> String
 showTermWithNames opts ne trm =
@@ -706,10 +697,10 @@ ppPPModule opts (PPModule importNames decls) =
        ppWithBoundCtx dtIndices (return $ viaShow dtSort) <*>
        mapM (\(ctorName,ctorType) ->
               ppTypeConstraint (ppIdent ctorName) <$>
-              ppTerm' PrecNone ctorType)
+              ppTerm' PrecTerm ctorType)
        dtCtors)
     ppDecl (PPDefDecl defIdent defType defBody) =
-      ppDef (ppIdent defIdent) <$> ppTerm' PrecNone defType <*>
+      ppDef (ppIdent defIdent) <$> ppTerm' PrecTerm defType <*>
       case defBody of
-        Just body -> Just <$> ppTerm' PrecNone body
+        Just body -> Just <$> ppTerm' PrecTerm body
         Nothing -> return Nothing