Wrong type-checking with mutually recursive definitions

[claudemarche]

With the attached file MutualDef.zip, Alt-Ergo version 2.4.2 type-checker wrongly complains with

[Error]File "/home/cmarche/MutualDef.ae", line 10, characters 33-34:
Typing Error: this expression should have type prop

Similar definitions without mutual recursion are accepted normally.

[hra687261]

Apparently it is not treated as a mutually recursive function definition but as a normal definition, so instead of:

f(x) = f_body
and g(y) = g_body

it is seen as:

f(x) = (f_body and g(y) = g_body)

with g and y as uninterpreted symbols. Which is why f_body is expected to be of type prop.
Which is annoying, because by looking at the parser their doesn't seem to be support for parsing mutually recursive functions. Although it shouldn't be too hard to add.

[claudemarche]

Indeed, I didn't realized it was a parsing problem at first!

Since Alt-Ergo supports mutually recursive ATDs, it is expected that it supports also mutually recursive definitions.

A possible solution to avoid the parsing ambiguity is to use another keyword than and, say with like in Coq or WhyML. Or do not use and for logical connective, but /\.

[hra687261]

Fixed by #549.
So to add support for mutually-recursive definitions without adding a new keyword and without introducing ambiguity, it was decided that the syntax would look like this from now on:

function f (...): ... = ...
and function g(...): ... = ...
and predicate p(...) = ...

[Halbaroth]

Fixed by #550 for future Dolmen front-end.