Conditional rules

[bodeveix]

This PR extends the syntax of rules to add optional equational constraints of the form:

rule <term> when <term> ≡ <term> ↪ <term>
rule <term> when <term> «[op] <term> ↪ <term>

• In the first form, the compared terms must be flat, i.e. of the form f $p1 ... $pn to avoid cyclic dependencies between files.

• In the second form, the compared terms are restricted to pattern variables. The condition is satisfied if the valeur of the first is a sub term of the value of the second one by crossing only op arguments. Subterm conditions could be expressed using the first form, but it would need defining a sub term relation for each operator.

Remarks:

• It would be possible to let the comparison instantiate some pattern variables.
• Static type checking of the constraint is not done