Do not require parentheses for fun/assume/assert

[gebner]

This PR changes the parser to require fewer parentheses:

1. When using lambdas as last function argument: foo fun x -> x + 1
2. Around assume and assert arguments: assert 1 < 2 (Like we already do in Pulse.)

I'm doing an everest run right now.

[gebner]

I'm doing an everest run right now.

And it finished successfully.

[mtzguido]

Hi Gabriel, this looks great, but I'm concerned about the following warnings:

Warning: 29 states have shift/reduce conflicts.
Warning: 3 states have reduce/reduce conflicts.
Warning: 363 shift/reduce conflicts were arbitrarily resolved.
Warning: 3 reduce/reduce conflicts were arbitrarily resolved.
Warning: 227 end-of-stream conflicts were arbitrarily resolved.

In master this is:

Warning: 5 states have shift/reduce conflicts.
Warning: 6 shift/reduce conflicts were arbitrarily resolved.
Warning: 227 end-of-stream conflicts were arbitrarily resolved.

Would be good if we can rework the grammar a bit to remove the conflicts, but in general I really like this feature (we discussed it today too and agreed it's good)

Also, would be nice if we can ditch the parenthesis in formulas like p /\ (forall x. q x).

[TWal]

There are also unnecessary parenthesis in expressions like p /\ (let x = ... in ...) and p /\ (match x with ...), similar to the forall example!

[gebner]

I managed to fix the reduce/reduce conflicts:

Warning: 16 states have shift/reduce conflicts.
Warning: 33 shift/reduce conflicts were arbitrarily resolved.
Warning: 233 end-of-stream conflicts were arbitrarily resolved.

However, there are a few new shift/reduce conflicts: these are of the form fun x -> t $op s for some binary operator $op. The grammar is ambiguous here and does not specify whether the $op should be inside the fun outside. If I read the menhir documentation correctly, then these conflicts should all be resolved in favor of shifting, i.e., greedily parsing the fun---which seems very natural here.

I haven't used parser generators in decades, so this is mostly guesswork and I'd love to hear from someone more experienced. AFAICT, there are two ways to disambiguate conflicts:

1. Using a sequence of nonterminals that correspond to the precedence hierarchy (i.e., disambiguating the grammar). We use this for tmIff/tmImplies/tmConjunction/...
2. Using precedence declarations, where you specify precedence and associativity declaratively at the beginning of the file using %nonassoc/%left/%right statements. However, this only seems to disambiguate productions in the same nonterminal in my limited testing. We use this in tmEqWith (?).

Unfortunately, I don't see how either one would help with this change.

[gebner]

FWIW, I'm also getting these warnings:

File "fstar-lib/FStar_Parser_Parse.mly", line 125, characters 60-70:
Warning: the token LBRACK_BAR is unused.
File "fstar-lib/FStar_Parser_Parse.mly", line 319, characters 0-15:
Warning: symbol decoratableDecl is unreachable from any of the start symbol(s).
File "fstar-lib/FStar_Parser_Parse.mly", line 302, characters 0-16:
Warning: symbol noDecorationDecl is unreachable from any of the start symbol(s).

Is it safe to remove those unused nonterminals?

EDIT: I just saw that they are used in pulse.

[gebner]

There are also unnecessary parenthesis in expressions like p /\ (let x = ... in ...) and p /\ (match x with ...), similar to the forall example!

I also think that these parens are unnecessary, but I'm not sure what the best way to go here is. Would you expect the following to work?

Seq.length let x = Seq.create 1 42 in Seq.append x x

I tried moving let to tmNoEqWith instead, but that breaks quite a bit.

[gebner]

I just did another everest run with the changes to forall/exists, and I can confirm that there are no regressions.

[mtzguido]

Check world CI: https://github.com/FStarLang/FStar/actions/runs/10705049189