search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

TPT: Unbalanced parenthesis in forall quantifiers #300

Closed ldcouto closed 9 years ago

ldcouto commented 9 years ago

An extra parenthesis is appended at the end of the quantified expression.

Minimum example:

values 
b = forall x in set {} @ false

Yields:

definition "b = +|(forall x in @set {} @ false)) : @bool|+"
declare b_def [eval,evalp]
ldcouto commented 9 years ago

Did some sniffing around and in ThmExpVisitor there's a line adding a parenthesis to endBrackets:

very long link

I think that's the problem but I don't know why it's there so I'm leaving it to @richardpayne for now.

richardpaynea55 commented 9 years ago

Fixed, the set bind version wasn't adding the opening parenthesis for the expression. Now generates:

definition "b = +|(forall x in @set {} @ (false)) : @bool|+" declare b_def [eval,evalp]

which parses fine in Isabelle

ldcouto commented 9 years ago

Ignore the test reference. It's actually for another issue and numbers are difficult for me.