search

jonsterling / tt

secret project
17 stars 1 forks source link

Implement pretty printing #6

Closed ghost closed 6 years ago

ghost commented 6 years ago

Here is a quick and dirty pretty printer. It hasn't been tested much so it probably has some bugs.

Example session below:

utop # open TT;;
utop # Tm.pp_chk (Pretty.Supply.mk ()) 2 Format.str_formatter (Tm.Lam (Tm.Bind.Mk (Tm.Up (Tm.App (Tm.V (Tm.Idx.Mk 0), (Tm.Lam (Tm.Bind.Mk Tm.Bool)))))));;
- : unit = ()
utop # Format.flush_str_formatter ();;
- : string = "λa. ⇑(a (λb. bool))"
ghost commented 6 years ago

By the way, you probably want to still derive show so you can have something to display the raw AST form. Maybe it would be better to name these functions something other than pp_.

ghost commented 6 years ago

Also, if you aren't familiar with the weird box formatting notation there are some explanations here (scroll down to "Printing to stdout: using printf") along with an example. The docs for the Format module also cover some of it in more detail.

jonsterling commented 6 years ago

This is really cool! I'm sorry that I didn't see this, now I appear to have created some merge conflicts 😦

jonsterling commented 6 years ago

I'm still not certain if I'm done moving the syntax around yet, btw. But I think it's at least in a better state than it was.

ghost commented 6 years ago

Yeah, no worries about the merge conflicts. If you want to wait a little while on this so you can experiment with the syntax more that's fine. Let me know when you think it's ready. Alternatively, you should have commit rights for this (on my repo I guess) so feel free to modify it.

Also some of this was kind of tentative anyway since I wasn't really sure how you wanted the concrete syntax to look.