Pretty-printing saw-core syntax results in way too many line-breaks

[brianhuffman]

Pretty-printing a large saw-core term invariably gives you output that looks something like this:

                        in Prelude.either x@3 x@5 (Prelude.CompM x@4)
                             (\(x_left0 : x@3) ->
                                Prelude.sawLet Prelude.Nat
                                  (Prelude.CompM (Prelude.Vec 64 Prelude.Bool))
                                  0
                                  (\(z' : Prelude.Nat) ->
                                     Prelude.sawLet Prelude.Bool
                                       (Prelude.CompM
                                          (Prelude.Vec 64 Prelude.Bool))
                                       Prelude.True
                                       (\(z'' : Prelude.Bool) ->
                                          let { x@6 = Prelude.Vec 64
                                                        Prelude.Bool
                                              }
                                           in Prelude.sawLet x@6
                                                (Prelude.CompM x@6)
                                                0x0000000000000000
                                                (\(z''' : x@6) ->
                                                   Prelude.sawLet Prelude.Bool
                                                     (Prelude.CompM
                                                        (Prelude.Vec 64
                                                           Prelude.Bool))
                                                     Prelude.True
                                                     (\(z'''' : Prelude.Bool) ->
                                                        Prelude.sawLet
                                                          Prelude.Nat
                                                          (Prelude.CompM
                                                             (Prelude.Vec 64
                                                                Prelude.Bool))
                                                          0
                                                          (\(z'''''
                                                               : Prelude.Nat) ->
                                                             let { x@7 = Prelude.Vec
                                                                           1
                                                                           Prelude.Bool
                                                                 }
                                                              in Prelude.sawLet
                                                                   x@7
                                                                   (Prelude.CompM
                                                                      (Prelude.Vec
                                                                         64
                                                                         Prelude.Bool))
                                                                   0b1
                                                                   (\(z''''''
                                                                        : x@7) ->
                                                                      Prelude.sawLet
                                                                        Prelude.Bool
                                                                        (Prelude.CompM
                                                                           (Prelude.Vec
                                                                              64
                                                                              Prelude.Bool))
                                                                        Prelude.True
                                                                        (\(z'''''''
                                                                             : Prelude.Bool) ->
                                                                           Prelude.sawLet
                                                                             Prelude.Bool
                                                                             (Prelude.CompM
                                                                                (Prelude.Vec
                                                                                   64
                                                                                   Prelude.Bool))
                                                                             Prelude.False
                                                                             (\(z''''''''
                                                                                  : Prelude.Bool) ->
                                                                                Prelude.sawLet
                                                                                  Prelude.Bool
                                                                                  (Prelude.CompM
                                                                                     (Prelude.Vec
                                                                                        64
                                                                                        Prelude.Bool))
                                                                                  Prelude.True
                                                                                  (\(z'''''''''
                                                                                       : Prelude.Bool) ->
                                                                                     Prelude.sawLet
                                                                                       Prelude.Bool
                                                                                       (Prelude.CompM
                                                                                          (Prelude.Vec
                                                                                             64
                                                                                             Prelude.Bool))
                                                                                       Prelude.True
                                                                                       (\(z''''''''''
                                                                                            : Prelude.Bool) ->
                                                                                          Prelude.returnM
                                                                                            (Prelude.Vec
                                                                                               64
                                                                                               Prelude.Bool)
                                                                                            0x0000000000000000)))))))))))

After the first few lines, once the indentation starts to get large, the prettyprinter decides to put only one identifier or token per line, as if that's supposed to make it easier to read. It prints out so many newlines that quite often a pretty-printed term will exceed the maximum size of my terminal's scrollback buffer.

We need to change the default page width and ribbon width settings for the saw-core prettyprinter, so that we don't get such garbage output.

[kquick]

Also note that Prettyprinter has the group and flatAlt functions that might be helpful in this regard.

[brianhuffman]

I believe we're using group etc. in basically the way we want; it's just that with the default layout configuration, as soon as anything exceeds 80 columns it starts putting linebreaks everywhere they can possibly go. Changing the default layout configuration should take care of this problem.

[brianhuffman]

Layout options are specified in four (!) different places in the code that I can find:

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

Lines 683 to 688 in 87ab2f3

	renderSawDoc :: PPOpts -> SawDoc -> String
	renderSawDoc ppOpts doc =
	Text.Lazy.unpack (renderLazy (style (layoutPretty layoutOpts doc)))
	where
	layoutOpts = LayoutOptions (AvailablePerLine 80 0.8)
	style = if ppColor ppOpts then reAnnotateS colorStyle else unAnnotateS

saw-script/src/SAWScript/Position.hs

Lines 41 to 43 in 87ab2f3

	renderDoc :: PP.Doc ann -> String
	renderDoc doc = PP.renderString (PP.layoutPretty opts doc)
	where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)

saw-script/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

Lines 1166 to 1168 in 87ab2f3

	renderDoc :: Doc ann -> String
	renderDoc doc = renderString (layoutPretty opts doc)
	where opts = LayoutOptions (AvailablePerLine 80 0.8)

saw-script/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

Lines 4164 to 4166 in 87ab2f3

	error ("Unhandled expression form: " ++
	(renderString (layoutSmart opts (mbLift $ fmap (ppApp (const $ pretty ("_" :: String))) mb_e))))
	where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)

I don't think all of these are used for pretty-printing saw-core terms, but we should still reconsider all of these.

[eddywestbrook]

Ooh, yeah, that's a little embarrassing. :) Agreed, those should all definitely use a single layout function defined in Pretty.hs.

[brianhuffman]

Yeah, any that are used for printing saw-core terms should use a default layout defined in Pretty.hs. Layout configurations used for printing other types might be better off using defaultLayoutOptions from the prettyprinter library, unless we have a specific reason to prefer something else.

[brianhuffman]

Since saw-core terms so regularly exceed the 80-column width, I'm thinking that we might rather just set the page width to something astronomically large, and then just set the ribbon width to something less than 80. This way we'll get output shaped like this:

******
 ******
  ******
   ******
    ******
     ******
      ******
       ******
        ******

instead of like this

******
 ******
  ******
   *****
    ****
     ***
      **
       *
        *
         *
          *
           *