GitLab

We only destruct n-tuples, unit types, and singleton records
without invariants. We only inline projection-like functions
for these types.

also, rename asym_label to asym_split and keep_on_simp_label
to keep_on_simp.

Record fields labeled with label model_trace:@hide_field will be not
shown in counterexample.

Previously, "." was automatically appended to names stored in
model_trace label when creating variables corresponding to record
fields in eval_match and when projecting record fields in the
transformation intro_projections_counterexmp. Now, this is not done
and "." must be given in model_trace label of the projection or
record field.

The reason is that for SPARK, character different from "." (e.g., "'"
needs to be sometimes appended.

Do not append '.' to the name of the variable representing field access
if the field name is empty string (that is, if the field name should be
ignored in counterexample).

were added to original labels.

When eval_match creates new terms from original terms, all labels of
the original terms are copied to the new terms. The exception are
labels of the form "model_trace:*". These labels are not copied if both
original terms and new terms contain this label.

In wp, eval_match is used to replace record fields with simple variables
of the same type. Originally, all labels from the variable that field
was accessed were copied to new variables representing fields of this
variable. Therefore also "model_trace:var_name" label was copied and thus
the field had name "var_name" in the counterexample.

This commit solves this problem by appending names of the fields to
"model_trace:*" label of new variables representing record fields.

  This is to prevent quantified records from being decomposed by
  eval_match. e.g, assert { forall x:t. ... } was previously
  transformed to assert { forall x1:t1, x2:t2, x3:t3. ... } if x was
  a record type with fields x1,x2,x3. This changed the
  instantiation pattern, which could be harmful.

In pattern compilation, we only need to know the full list of
constructors for a given type, whenever
1. we want to check that a symbol used in a pattern is indeed
   a constructor;
2. we want to check for non-exhaustive matching and return an
   example of a non-covered pattern, if any.
Thus, we need to give Pattern.compile access to the current
known_map whenever we check new declarations in Decl or Mlw_decl.
However, once we have checked the patterns, we do not need the
full constructor lists just to compile the match expressions.
Just knowing the number of constructors (provided in ls_constr)
is enough to detect non-exhaustive matching during compilation.

+ rename Debug.Opt to Debug.Args to avoid conflicts

+ create AUTHORS file
+ fix the linking exception in LICENSE
+ update the "About" in IDE
+ remove the trailing whitespace
+ inflate my scores at Ohloh

Indeed their inlining causes an exponential growth of the formulas for all
the provers that are relying on the "eliminate_if" transformation.

- put abstract types and aliases in Dtype of tysymbol
- put (recursive) algebraic types in Ddata of (ts,constr list) list
- put abstract function/predicate symbols in Dparam of lsymbol
- put defined logic symbols in Dlogic of (ls,ls_definition) list

Thanks to Johannes Kanig for this useful suggestion.