pretty-printer #9
Loading…
Reference in New Issue
No description provided.
Delete Branch "pretty-printer"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The pretty printer for F keeps trace of the "levels" implicitly. Inspired by http://gallium.inria.fr/blog/a-toy-type-language-1/
@ -30,0 +13,4 @@
let rec print_type ty =
tyquant ty
and tyquant = function
I would have a preference for
print_type_quant
to clarify the namespace, and in particular be able to callprint_type_atom
from the term printers. (Maybe we can drop theprint_*
suffix for all functions.)@ -121,0 +84,4 @@
let rec print_term t =
abs t
and abs = function
Possible naming proposals:
toplevel
orbinder
.Actually, thinking about it more, I think that
abs
is also perfectly fine. It is the "level of things likeabs
".@ -150,0 +107,4 @@
print_type ty1 ^^
string " = " ^^
abs t2
| Proj (i, t) ->
I would propose to have
Proj
andInj
at their own level, below (so that we getinj 2 (fun x -> x)
rather thaninj 2 fun x -> x
), and that their own sub-terms be printed atapp
level (to forceinj 2 (proj 1 x)
rather thaninj 2 proj 1 x
).@ -153,3 +118,2 @@
else
parens (print_term t)
print_inj ty1 i (abs t2)
| Match (ty, t, brs) ->
I think
Match
could go to the levelatom
.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
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 ->
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)
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, asabs
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)
same comment as for
Let
above@ -164,0 +127,4 @@
and app = function
| TyApp (t1, ty2) ->
atom t1 ^^
we don't need
atom
here,app
is fine (and would correspond to the previous code). This is important to getfoo [bar] [baz]
when type-applying several times in a row.@ -164,0 +132,4 @@
print_type ty2 ^^
rbracket
| App (t1, t2) ->
atom t1 ^^
Same comment as for
TyAbs
. This is important to getf 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
If we want to avoid the printing
Inj 2 Inj 3 p
, we also need levels here, withinj
at its own level and then everything else inatom
.I updated the printer as suggested in the comments
@ -142,0 +86,4 @@
print_let_in
(string x)
(print_term t1)
(print_term t2)
(I would use
print_term
for the first subterm andprint_term_abs
for the second.)@ -164,0 +124,4 @@
| App (t1, t2) ->
print_term_app t1 ^^
space ^^
print_term_app t2
the second term should be one level below
Approved, see minor comments to fix before merging.
@ -175,1 +156,3 @@
match pat with
print_pinj pat
and print_pinj = function
print_pattern_inj
@ -186,1 +170,3 @@
print_term_aux 2 t
print_tuple print_pattern ps
| PInj _ as pat ->
print_pattern pat
I think that parentheses are needed here.
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 upstreammaster
branch, so you can send a PR here againstupstream
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 exampleupstream-olivier
for your own fork on gitlab.inria.fr.)(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.)