Unnecessary parentheses in pretty printing of abstractions

[jgroote]

Issue migrated from trac ticket # 1131

component: Core: Print Library | priority: minor

2013-02-14 22:17:46: @wiegerw created the issue

---

Currently too many parentheses are used when printing abstractions in certain contexts. For example:

forall n: Bool. n => (forall k: Bool. k => n)

It looks like the function print_expression needs to be specialized for abstractions (and possibly some other operators too).

[jgroote]

2013-06-06 15:50:47: @jkeiren

[jgroote]

2013-08-19 11:58:47: @jkeiren

[jgroote]

2014-09-03 16:48:55: @wiegerw

[jgroote]

2016-11-17 10:38:35: @wiegerw changed title from pretty printing of abstractions needs improvement to Unnecessary parentheses in pretty printing of abstractions

[jgroote]

2017-05-04 14:16:15: @wiegerw

[tneele]

I do not find the provided example very convincing. The precedence of the forall operator is lower than the implication operator (ie, the implication binds stronger. The fact that the forall k occurs on the right-hand side of the implication is essential for the fact that forall n: Bool. n => forall k: Bool. k => n can only be interpreted in one way.

However, commit 2f4a60ce74d43 introduced some new unnecessary parentheses. For example, in the expression (a && a) && a, the parentheses are not necessary.

[wiegerw]

The change in commit 07bc09d should solve the problem with unnecessary parentheses in the expression (a && a) && a. Perhaps there are more operators with the wrong associativity annotations. The problem is that information about associativity is only partially available in the dparser grammar.