GitLab

displayed in any case (even if the debug flag whyml_wp is not given).

Conflicts:
	src/core/model_parser.ml

maps Why3 type int to OCaml type int
this is of course unsafe, unless one has proved absence of overflows

This commits enable the possibility to use variants
with different types/well-founded relations for
mutually recursive functions. This is useful if the
termination of sub-groups of those functions requires
a finer termination argument.

Example use case:
Suppose for example the following mutually recursive
function structure:

type t = A (list t)
let rec f (x:t) (...other args...)
  variant { x , other variants }
= ... f x (...different args...)...
with g (l:list t) (...other args...)
  variant { l }
= ...

The global termination argument is structural descent
trough the type t. However, as it is not enough for f
which perform a non-structural recursive calls, we add
other variants. Such variants were forbidden under the
previous behavior because f and g variants were
considered incompatible: As x and l have different
types, it was impossible to write the lexicographic
comparison of both n-uplets (even when completing g's
list).

The new behavior for mutual recursive calls is the
following: We first scan both variants to find the
longest compatible common prefix, e.g prefixes for
which types and relations are the same. Additionally,
we allow the last elements of such prefix to have
different types if their well-founded relation is
structural descent. Then, we generate a lexicographic
descent obligation on those prefixes only.

We still enforce that in a mutually recursive group,
the first component of each variant must corresponds
to the same well-founded relation. This event is much
more likely to be symptomatic of an error, as functions
with such fully mismatched variants cannot call each
other anyway. Moreover, one can always break them in
different recursive groups.

by wp displayed in counter-example only if the debug flag whyml_wp is
given.

Label model_trace:x is automatically added to every element with name x that has a model label and does not have a model_trace:y label.

Setting whether counter-example should be get in why3ide is done by in GUI - instead of setting this using command-line option.

              when one of the field is empty.

              (Thx Jean-Christophe)