GitLab

Black on red was not readable. Colors to be decided.

As a side effect, this also modifies reflection.ml accordingly.

fixes issue #57

a new theory relations.WellFounded is introduced for this purpose
(and must be imported whenever one wants to make use of a custom
relation for a variant)

it defines, inductively, a notion of accessibility for a given
predicate R (x is accessible whenever all elements smaller than x for R
are alreay accessible)

whenever one has to prove that a variant decreases, a new VC is also
generated, to show that the old value of the variant is accessible
for the order relation

note: accessibility being defined inductively, proving well-foundedness
is out of reach of SMT solvers; but at least this is sound now

Also, move some model-related labelling from Parser to Vc.

a branch is typed *after* unifying the type of the pattern with the
type of the matched value

fixes issue #124 (return type and coercions)

done in both logic and programs