GitLab

* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.

Change in syntax
* use

  type t = < range 1 2 >   (* integers from 1 to 2 *)
  type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)

  the two projections :
  t'int
  t''real

  and the predicate :
  t''isFinite

* Restrict the use of "'" in whyml:
  Users are not allowed to introduce names where a quote symbol
  is followed by a letter. Thus, the following identifiers are
  valid:

  t'
  toto'0''
  toto'_phi

  whereas toto'phi is not.

Note: we do not yet support negative numbers in range declaration
and casting of a literal.

also, remove the useless ?constr parameter of create_psymbol

- hide the closure variable
- split t_app_beta into t_func_app_beta, which returns terms,
  and t_pred_app_beta which returns formulas

Also:
- check for non-recursivity in t_open_lambda
- implement t_is_lambda via t_open_lambda (less efficient,
  but the correct code without opening would be horrendous)
- drop t_app_lambda, subsumed by t_[func|pred]_app_beta
- support nested lambdas in t_[func|pred]_app_beta

Two points for discussion:

- t_lambda accepts both terms and formulas for the body.
  Thus, t_open_lambda, t_app_lambda, and t_app_beta can all
  return a term or a formula, depending on what is inside
  the lambda term. The caller should not forget to check.
  We could, in principle, always return a term (bool-typed
  when needed), which would exclude a possible run-time error,
  but then a caller who expects a formula, would have to
  recognize the results of the form [if f then True else False],
  before blindly attaching [== True] to them. Maybe still worth it:
  it's better if a forgotten check leads to an inefficient formula
  than to a type-checking error.

- t_lambda takes a preid which will be the binding variable in the
  produced epsilon. This permits us to give names to our lambdas
  if we want it (what for?) and to give locations to intermediate
  terms inside the epsilon. Overall, it's not very useful and can
  probably be removed.

feel free to revert, if you think we might want to make again the
distinction between t_equal and t_equal_alpha in future or just
don't feel like breaking the API.

also, ensure that t_label_copy does not lose information

The rationale for this change is that the major case of term duplication
is a transformation that changes only some parts of a term, leaving the
rest intact. This case can be handled with the help of Term.t_label_copy
(which must be called anyway, to preserve labels): if the two terms are
"similar", i.e. composed from the identical components, we return the
original and drop the copy. The duplication of unrelated terms is more
rare, because of bound variables which are mostly unique.

Decls and tasks are still h-consed, however, to permit memoization.

On the same example of BWare the gain is quite visible:

why3-replayer : hcons

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

why3-replayer : no hcons

106.81user 7.86system 1:59.32elapsed 96%CPU (0avgtext+0avgdata 1656908maxresident)k

we still keep bv_vars in the binders, so calculating the set
of free variables only has to descend to the topmost binders.
The difference on an example from BWare is quite striking:

/usr/bin/time why3-replayer : with t_vars

505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k

/usr/bin/time why3-replayer : without t_vars

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

Not only we take 2/3 of memory, but we also gain in speed (less work
for the GC, most probably).

This patch should be tested on big WhyML examples,
since src/whyml/mlw_*.ml are big users of t_vars.

Thanks to Guillaume for the suggestion.

Also:

- Make [Highord.pred 'a] an alias for [Highord.func 'a bool],
rename [Highorg.(@!)] to [(@)], remove [Highorg.(@?)], remove
the quantifiers [\!] and [\?] and only leave [\] which is the
only true lambda now;

- Allow mixing bool and Prop in logic, Dterm will introduce
coercions where necessary (trying to minimize the number of
if-then-else in the term context).

the term evaluation.

We store in every lsymbol a new integer field ls_constr,
equal to zero if the lsymbol is not a constructor, and equal
to the number of constructors of the lsymbol's type otherwise.
It is allowed to declare or define an lsymbol with ls_constr > 0
as an ordinary function (otherwise algebraic type elimination
wouldn't work - though we might still check this in theories),
but it is forbidden to use a wrong ls_constr in algebraic type
definitions.

The ghostness of a match expression is now determined as follows:

If at least one branch expression is ghost,
  then the match is ghost;
else if there is only one branch,
  then the match is not ghost;
else if the matched expression is ghost,
  then the match is ghost;
else if at least one pattern matches a ghost field
        against a constructor with ls_constr > 1
  then the match is ghost;
else
  the match is not ghost.

We do just enough to recognize obvious non-ghost cases, and
make no attempt to handle redundant matches or to detect
exhaustive or-patterns in subpatterns.

In programs, but also in pure theories, it is not safe to compare
arbitrary types. For example, if we have a record with ghost fields,
a comparison may produce different results before and after ghost
code elimination. Even for pure types like 'map' or 'set', it is
unlikely that the result of logical equality will be the same as
the result of OCaml structural equality on the implemented type.

This commit makes the first step towards fixing this issue.
We proceed in the following way:

1. Every lsymbol (pure function or predicate symbol) carries
   a subset of type variables of its signature, called "opaque
   type variables". By marking a type variable 'a opaque in an
   lsymbol's signature, the user guarantees that this lsymbol
   can be implemented without ever comparing values of type 'a.
   In other words, this is a promise not to break into a type
   variable.

   The corresponding syntax is: "predicate safe (x y : ~'a)".

   All type variables in undefined symbols are non-opaque,
   unless annotated otherwise. Non-opaque is the default
   to keep the change conservative.

   Opacity of type variables in defined symbols is inferred
   from the definition. If the definition violates a given
   opacity annotation, an exception is raised. Notice that
   we only check definitions in _theory_ declarations. One
   can define an lsymbol in a _task_ in a way that violates
   opacity. We cannot forbid it, because various elimination
   transformations would replace safe operations (such as
   matching) with equalities. This is not a problem, since in
   the pure logical realm of provers opacity is not required
   One exception would be Coq, whose transformation chain must
   never perform such operations.

   All type variables in inductive predicates are non-opaque.
   Indeed, we can redefine equality via an inductive predicate.
   [TODO: find safe forms of inductive definitions and implement
   more reasonable restrictions.]

   All type variables in constructors and field symbols are opaque.

   It is forbidden to instantiate an opacity-preserving symbol
   with an opacity-breaking one in a clone substitution.

2. Similar type variable tracking is implemented for program symbols.
   Type variables in the signature of a "val" are non-opaque unless
   annotated otherwise. Opacity of type variables in defined symbols
   is inferred from the definition, and an exception is raised, if
   a given annotation is violated.

   The internal mechanism of tracking is different: the "eff_compar"
   field in effects contains the type variables that occur under
   equality or any other opacity-breaking operation. In this respect,
   our API is inconsistent between lsymbols and psymbols: the former
   asks for the opaque tvsymbols, the latter requires us to fill the
   spec with "comparison effects" for the non-opaque ones. [TODO:
   add the "~opaque" argument to create_psymbol and make the WhyML
   core fill the effect under the hood.]

   Every time an lsymbol or a psymbol is applied in a program,
   we check the substitution into its signature's type variables.
   If a non-opaque type variable is instantiated with a program type,
   an exception is raised. [TODO: be more precise and reject only
   types with ghost and model components - being mutable, private,
   or carrying an invariant doesn't conflict with equality.]

   Notice that we do not allow to compare program types even in
   the ghost code. This is not needed if we only consider the
   problems of the code extraction, but _might_ be necessary,
   if we also want to protect Coq realisations (see below).

This commit fixes the immediate problem of breaking the ghost
guarantees when equality or some other opacity-breaking lsymbol
is applied in a program to a type with ghost or "model" parts.

This leaves the problem of code extraction for programs that
compare complex types such as maps or sets (Coq driver is
affected by this, too, I guess). The next step is to provide
annotations for problematic type constructors. A declaration
"type ~map 'a 'b" would mean "logical equality on this type
is likely to be different from the structural equality on any
implementation of this type - therefore do not apply equality
to it: neither in programs (because this can't be implemented),
nor in pure functions (because they are extracted, too, and
because this can't be realized with Leibniz equality in Coq)."
[TODO: discuss and implement.]

[TODO: mb choose better term for "opaque" and notation for ~'a.]

the Set signature is moved to a separate Extset module,
instead of being included into Extmap.S. The module hierarchy
becomes simpler, we don't shadow  OCaml standard modules anymore,
and the bug #15270 is fixed, too.

export Why3's extended hash tables as Stdlib.XHashtbl
in order to keep OCaml's Hashtbl accessible. Unlike Stdlib.Map
which fully covers the OCaml's interface, Stdlib.XHashtbl does
not provide polymorphic hash tables.

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