ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Marked Pretty Printer #146

Open xich opened 8 years ago

xich commented 8 years ago

At HIW this year, David Christiansen talked about a pretty printer library with annotations, and mostly showed some of the cool things you could do with it. Video:

https://www.youtube.com/watch?v=m7BBCcIDXSg&list=PLnqUlCo055hVfNkQHP7z43r10yNo-mc7B&index=10

This is very similar to Hughes/PJ pretty-printer with 'marking' that Andy cooked up for HERMIT (which we still use). I know at some point @RyanGlScott used the marking for the Android interface to draw arrows between occurrences and bindings, etc.

Then I went to look at the marked-pretty repo, and noticed that Ryan converted it at some point to be based on (match API of?) Trevor Elliott's pretty package. The thing is, pretty implements a Hughes/PJ pretty printer with annotations here:

https://hackage.haskell.org/package/pretty-1.1.3.2/docs/Text-PrettyPrint-Annotated-HughesPJ.html

So my question is, does marked-pretty do something pretty doesn't? Could we just switch to pretty and have one less package to maintain? Could the rendering code we use be integrated back into pretty, or some package built on pretty?

People are currently excited about building this sort of pretty printer into GHC/ghci:

https://ghc.haskell.org/trac/ghc/ticket/8809#comment:12

Perhaps jumping on that bandwagon would be good so we could influence the ghci implementation and then use it for the new HERMIT shell?

RyanGlScott commented 8 years ago

Well, one practical reason is that pretty-1.1.3 won't be bundled with GHC until 8.0, I'm guessing (GHC 7.10 ships with pretty-1.1.2). Other than that, I think we could replace marked-pretty with pretty at some point, although I'd have to look closer to see if it truly is a drop-in replacement. The marking mechanism which marked-pretty uses is:

data MDoc a
  = Empty
  | NilAbove (MDoc a)
  | TextBeside !(TextDetails a) {-# UNPACK #-} !Int (MDoc a)
  | Nest {-# UNPACK #-} !Int (MDoc a)
  | Union (MDoc a) (MDoc a)
  | NoDoc
  | Beside (MDoc a) Bool (MDoc a)
  | Above (MDoc a) Bool (MDoc a)

data TextDetails a = Chr  {-# UNPACK #-} !Char
                   | Str  String
                   | PStr String
                   | Mark a

Whereas in pretty-1.1.3, it's:

data Doc a
  = Empty
  | NilAbove (Doc a)
  | TextBeside !(AnnotDetails a) (Doc a)
  | Nest {-# UNPACK #-} !Int (Doc a)
  | Union (Doc a) (Doc a)
  | NoDoc
  | Beside (Doc a) Bool (Doc a)
  | Above (Doc a) Bool (Doc a)

data AnnotDetails a = AnnotStart
                    | NoAnnot !TextDetails {-# UNPACK #-} !Int
                    | AnnotEnd a
andygill commented 8 years ago

Yes - it looks like it would work.

RyanGlScott commented 8 years ago

I was skeptical at first if this would work, since we use fullRender in HERMIT at the moment, and it has the wrong type signature to work with AnnotDetails:

fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc b -> a

but I had completely overlooked the more general analog, fullRenderAnn:

fullRenderAnn :: Mode -> Int -> Float -> (AnnotDetails b -> a -> a) -> a -> Doc b -> a

I also hadn't noticed that TextDetails was moved into AnnotDetails, so this means that fullRenderAnn provides a completely drop-in replacement for fullRender! Yay!