search

MonoidalAttackTrees / ILL-Impl

Implementation of a term assignment for intuitionistic linear logic
0 stars 0 forks source link

Property Parens in Pretty Printer #14

Closed heades closed 8 years ago

heades commented 8 years ago

The output to the pretty printer will not be correct for some inputs due to parenthesization.

For example, prettyType applied to "Lolly (Lolly I I) I" will out put "I -o I -o I", which is actually, "I -o (I -o I)", but the correct output should be "(I -o I) -o I" which is semantically different.

So proper parens to be accounted for.

heades commented 8 years ago

Checkout the following for how to do this:

https://github.com/heades/gradual-typing/blob/master/impl/Pretty.hs

tattymennis commented 8 years ago

Work in progress.

tattymennis commented 8 years ago

I addressed proper parens for Lolly (if first arg is another Lolly, parenthesize), App (if first arg is another App, parenthesize), adjusted Lam (from bound var to . parenthesize).

heades commented 8 years ago

You said:

App (if first arg is another App, parenthesize)

This is not needed, because (t1 t2) t3 = t1 t2 t3, because application is left associative.

If the first argument to an application is not an application or unit, then it needs to be parenthesized.