pretty-printer #9

Merged
gasche merged 11 commits from pretty-printer into master 2020-06-05 09:05:57 +02:00
Owner

The pretty printer for F keeps trace of the "levels" implicitly. Inspired by http://gallium.inria.fr/blog/a-toy-type-language-1/

The pretty printer for F keeps trace of the "levels" implicitly. Inspired by http://gallium.inria.fr/blog/a-toy-type-language-1/
gasche reviewed 2020-05-27 11:59:27 +02:00
@ -30,0 +13,4 @@
let rec print_type ty =
tyquant ty
and tyquant = function
Collaborator

I would have a preference for print_type_quant to clarify the namespace, and in particular be able to call print_type_atom from the term printers. (Maybe we can drop the print_* suffix for all functions.)

I would have a preference for `print_type_quant` to clarify the namespace, and in particular be able to call `print_type_atom` from the term printers. (Maybe we can drop the `print_*` suffix for all functions.)
@ -121,0 +84,4 @@
let rec print_term t =
abs t
and abs = function
Collaborator

Possible naming proposals: toplevel or binder.

Possible naming proposals: `toplevel` or `binder`.
Collaborator

Actually, thinking about it more, I think that abs is also perfectly fine. It is the "level of things like abs".

Actually, thinking about it more, I think that `abs` is also perfectly fine. It is the "level of things like `abs`".
@ -150,0 +107,4 @@
print_type ty1 ^^
string " = " ^^
abs t2
| Proj (i, t) ->
Collaborator

I would propose to have Proj and Inj at their own level, below (so that we get inj 2 (fun x -> x) rather than inj 2 fun x -> x), and that their own sub-terms be printed at app level (to force inj 2 (proj 1 x) rather than inj 2 proj 1 x).

I would propose to have `Proj` and `Inj` at their own level, below (so that we get `inj 2 (fun x -> x)` rather than `inj 2 fun x -> x`), and that their own sub-terms be printed at `app` level (to force `inj 2 (proj 1 x)` rather than `inj 2 proj 1 x`).
@ -153,3 +118,2 @@
else
parens (print_term t)
print_inj ty1 i (abs t2)
| Match (ty, t, brs) ->
Collaborator

I think Match could go to the level atom.

I think `Match` could go to the level `atom`.
gasche reviewed 2020-05-27 13:54:33 +02:00
gasche left a comment
Collaborator

More comments! I have looked at all the code now.

More comments! I have looked at all the code now.
@ -56,0 +45,4 @@
and typrod = function
| TyProduct tys ->
surround_separate_map 2 0 (lbrace ^^ rbrace)
lbrace star rbrace atom tys
Collaborator

With our surrounded/closed syntax for n-ary sums and products, they should both go in atom, it is never useful or natural to parenthesize them.

With our surrounded/closed syntax for n-ary sums and products, they should both go in `atom`, it is never useful or natural to parenthesize them.
@ -56,0 +52,4 @@
and atom = function
| TyVar x ->
print_tyvar x
| ty ->
Collaborator

I find it useful in practice to do a complete list of the unhandled constructors here: (TyProd _ | TySum _ | TyForall _ | TyMu _ | ...) as ty -> . The point is to get an exhaustivity warning if we later add a new constructor to the type, and be forced to think about where to add it in the hiearchy. With the current design, all pattern-matchings in the type printer are "fragile", so that does not happen.

I find it useful in practice to do a complete list of the unhandled constructors here: `(TyProd _ | TySum _ | TyForall _ | TyMu _ | ...) as ty -> `. The point is to get an exhaustivity warning if we later add a new constructor to the type, and be forced to think about where to add it in the hiearchy. With the current design, all pattern-matchings in the type printer are "fragile", so that does not happen.
@ -142,0 +93,4 @@
| Let (x, t1, t2) ->
print_let_in
(string x)
(abs t1)
Collaborator

I think it is clearer to call print_term here, because there is no level requirement at all for this term (it is enclosed by keywords on both sides). It is equivalent to the current code, as abs is the toplevel, but it is less clear and it could change in the future.

I think it is clearer to call `print_term` here, because there is no level requirement at all for this term (it is enclosed by keywords on both sides). It is equivalent to the current code, as `abs` is the toplevel, but it is less clear and it could change in the future.
@ -149,1 +99,3 @@
parens (print_term t)
print_let_in
(print_tuple string xs)
(abs t1)
Collaborator

same comment as for Let above

same comment as for `Let` above
@ -164,0 +127,4 @@
and app = function
| TyApp (t1, ty2) ->
atom t1 ^^
Collaborator

we don't need atom here, app is fine (and would correspond to the previous code). This is important to get foo [bar] [baz] when type-applying several times in a row.

we don't need `atom` here, `app` is fine (and would correspond to the previous code). This is important to get `foo [bar] [baz]` when type-applying several times in a row.
@ -164,0 +132,4 @@
print_type ty2 ^^
rbracket
| App (t1, t2) ->
atom t1 ^^
Collaborator

Same comment as for TyAbs. This is important to get f x y z.

Same comment as for `TyAbs`. This is important to get `f x y z`.
@ -181,6 +165,3 @@ and print_pattern pat =
print_inj tys i (print_pattern pat)
| PTuple ps ->
print_tuple print_pattern ps
Collaborator

If we want to avoid the printing Inj 2 Inj 3 p, we also need levels here, with inj at its own level and then everything else in atom.

If we want to avoid the printing `Inj 2 Inj 3 p`, we also need levels here, with `inj` at its own level and then everything else in `atom`.
Author
Owner

I updated the printer as suggested in the comments

I updated the printer as suggested in the comments
gasche reviewed 2020-05-28 15:13:55 +02:00
@ -142,0 +86,4 @@
print_let_in
(string x)
(print_term t1)
(print_term t2)
Collaborator

(I would use print_term for the first subterm and print_term_abs for the second.)

(I would use `print_term` for the first subterm and `print_term_abs` for the second.)
@ -164,0 +124,4 @@
| App (t1, t2) ->
print_term_app t1 ^^
space ^^
print_term_app t2
Collaborator

the second term should be one level below

the second term should be one level below
gasche approved these changes 2020-06-04 16:33:58 +02:00
gasche left a comment
Collaborator

Approved, see minor comments to fix before merging.

Approved, see minor comments to fix before merging.
@ -175,1 +156,3 @@
match pat with
print_pinj pat
and print_pinj = function
Collaborator

print_pattern_inj

`print_pattern_inj`
@ -186,1 +170,3 @@
print_term_aux 2 t
print_tuple print_pattern ps
| PInj _ as pat ->
print_pattern pat
Collaborator

I think that parentheses are needed here.

I think that parentheses are needed here.
gasche closed this pull request 2020-06-05 09:05:57 +02:00
Collaborator

Merged, thanks!

When you have time, we should prepare a similar PR against the upstream branch (the master branch of François' repository, git@gitlab.inria.fr:fpottier/inferno.git ).

I created an upstream branch in our repository that tracks the upstream master branch, so you can send a PR here against upstream if you want a review.

To actually submit the PR to François, you will need to sign up on gitlab.inria.fr, and create a fork of the repository there, if you have not already done this, to submit the PR from that fork. (On your local directory you could add two remotes, upstream for François' repository on gitlab.inria.fr, and for example upstream-olivier for your own fork on gitlab.inria.fr.)

Merged, thanks! When you have time, we should prepare a similar PR against the upstream branch (the `master` branch of François' repository, git@gitlab.inria.fr:fpottier/inferno.git ). I created an `upstream` branch in our repository that tracks the upstream `master` branch, so you can send a PR here against `upstream` if you want a review. To actually submit the PR to François, you will need to sign up on gitlab.inria.fr, and create a fork of the repository there, if you have not already done this, to submit the PR from that fork. (On your local directory you could add two remotes, `upstream` for François' repository on gitlab.inria.fr, and for example `upstream-olivier` for your own fork on gitlab.inria.fr.)
Collaborator

(I would recommend having a single commit with all pretty-printer changes, and keeping the link to the blog post in your PR description, which I think is helpful.)

(I would recommend having a single commit with all pretty-printer changes, and keeping the link to the blog post in your PR description, which I think is helpful.)
Sign in to join this conversation.
No reviewers
No Label
No Milestone
No Assignees
2 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Olivier/inferno-experimental#9
No description provided.