GitLab

metas are stored in a new field pd_metas aside the field pd_pure

+ add 'minInt and 'maxInt attributes for range types
+ add 'eb and 'sb attributes for float types
+ make ieee_float realization compatible with Coq 8.4

* 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.

Since this might break some cases relying on opaqueness of
type variables occuring only in return types, opaqueness
annotations are now allowed there as well.

This reverts commit b65dd4ae.

still allowed in the API (so far)

this is still work in progress and no testing was done so far.

Highlights of this commit:

- "(ghost 42, 15)" is now a non-ghost expression that can be returned
  from a function and/or matched against a "(ghost x, y)" pattern.
  Only the tuple constructor and direct pattern matching are magical:
  "let z = (ghost 42, 15) in ..." still makes z ghost, and therefore
  "snd (ghost 42, 15)" is ghost, too.

- "if c then e1 else ghost e2" and "let z = e1 in ghost e2" are now
  non-ghost expressions with a ghost result. This means that e1 may
  have visible effects. Of course, if e2 raises exceptions, the whole
  expression is ghostified. Contamination is still done when possible,
  that is, when the contaminated expression has no visible effects.

- "let ghost x = e1 in e2" no longer ghostifies e1.

- "let f (ghost x) = ... in f e1" no longer ghostifies e1.

- new syntax: variables in program patterns may be marked ghost.
  In particular: "let x, ghost y = ...".

- new syntax: the function result type may be written as a partially
  ghost tuple: "val f ... : ghost int" or "any (int, ghost bool)".
  The ghostness annotation is required for top-level and recursive
  functions.

- exceptions can carry partially ghost tuples (API only, WIP)

but forbid writing into these "confined" regions

this should not be problematic as long as these fields do not occur
in the invariants (actual or refined). In other words, a value of
a private type exists no matter what is stored in the field.

Also, admit non-private mutable types without actual mutable fields.
It is actually impossible to create a write effect for such types,
and the only consequence of being mutable is that they are assigned
a region, and so every value of such type can be tracked individually.
One use case for this is a non-private record with an invariant,
which either has fields with mutable types or has type parameters
that we wish to instantiate with mutable types. If we modify these
mutable components, this may break the record's invariant. Now, if
the record itself is immutable (and thus has no associated region),
then we must reestablish the invariant immediately, otherwise we
lose track of the value. Even if this extra flexibility does not
prove useful in the end, it seems to be harmless.

Also, admit type definitions of the form
  type t 'a = (private|abstract)? mutable? {} invariant*
which define private empty records (even if not declared private).

Also, "type t 'a" is now equivalent to "type t 'a = private {}".

pure functions are always ghost, accept mutable values,
and are required to produce pure results

the previous commit loses information when the target type symbol
is an existing type alias. This commit preserves symbol-to-symbol
instances.

this removes the ugly hack of creating an ad-hoc type alias symbol
for substitutions like "clone T with type t 'a = list (int, 'a)".

If a type symbol "t1 'a 'b 'c" is instantiated into a type of the
form "t2 'a 'b 'c", then the metas that mention the type symbol "t1"
are preserved, and "t1" is replaced with "t2". Otherwise, all such
metas disappear in the cloned theory.