GitLab

This reverts the enforcing part of a44cccbb.

x.{f} is allowed and can be used for unary applications
M.{f} is not allowed, use {M.f} instead

It is confusing to use the keyword "label" to define an exception.
Also, the "label L in ..." binds too far and the break point is
not clearly defined.

We do need some syntactic sugar for
  exception X t in try <expr> with X r -> r
(at the very least "break" and "continue"), but labels are not it.

In the surface language, the loop index is always int in
the loop invariant and all annotations and pure terms inside
the loop. If you want to access the original range-typed index,
use "let copy_i = i in" in the program code before your assertion.
Of course, you cannot do that for the loop invariant, which is
what we want.

  Reason for that change: interpret correctly both
  (1) A by B -> C and (2) A -> B by C
  Case (2) is common, and we expect by to take precendence,
  so that A is the context for the proof of B.
  Case (1) is rarer, and is troublesome if by take precendence
  cause (A by B) -> C is almost certainly not what the user
  intended to write. Putting precendence of by/so at the same level as
  the arrow fix this

At this moment, there is no semantics change. This commit only
provides dedicated grammar rules for negated numerals, so that
we do not have to recognize them later.

In this way, someone who puts a part of his function
in an abstract block will not have broken "return"s.

Useful to break out of the loops:

  label Break in
  while ... do
    label Continue in
    ... raise Break ...
    ... raise Continue ...
  done

When a label is put over a non-unit expression,
raise acts as return:

  label Return in
  if ... then raise Return 42; 0

Also, "return <expr>" returns from the innermost function.
This includes abstract blocks, too, so if you want to return
across an abstract block, you should rather use a label at
the top of the main function. TODO/FIXME: maybe we should
let "return" pass across abstract blocks by default, to
avoid surprises?

One shortcoming of the labels-as-exceptions is that they cannot
be used to transmit tuples with ghost elements, nor return ghost
values from non-ghost expressions. A local exception with an
explicit mask should be used instead. Similarly, to return
a partially ghost value from a function, it must have have
its mask explicitly written (which is a good practice anyway).
We cannot know the mask of an expr before we construct it,
but in order to construct it, we need to create the local
exceptions first.

Another caveat is that while it is possible to catch an exception
generated by a label, you should avoid to do so. We only declare
the local exception if the expression under the label _raises_
the exception, and thus the following code will not typecheck:

  label X in (try raise X with X -> () end)

Indeed, the expression in the parentheses does not raise X,
and so we do not declare a local exception X for this label,
and so the program contains an undeclared exception symbol.

current syntax is

    exception Return (int, ghost bool) in
    ...
    try
      ...
      raise Return (5, false)
      ...
    with
      Return (i, b) -> ...
    ...

These exceptions can carry mutable and non-monomorphic values.
They can be raised from local functions defined in the scope
of the exception declaration.

Aesthetics is a harsh mistress.

The current syntax is "{| <term> |}", which is shorter than
"pure { <term> }", and does not require a keyword. Better
alternatives are welcome.

As for type inference, we infer the type pf the term under Epure
without binding destructible type variables in the program.
In particular,
  let ghost fn x = {| x + 1 |}
will not typecheck. Indeed, even if we detect that the result
is [int], the type of the formal parameter [x[ is not inferred
in the process, and thus stays at ['xi].

Another problem is related to the fact that variable and function
namespaces are not yet separated when we perform type inference.
Thus both fuctions
  let ghost fn (x: int) = let x a = a in {| x + 5 |}
and
  let ghost fn (x: int) = let x a = a in {| x 5 |}
will not typecheck, since the type of [x] is ['a -> 'a] when
we infer the type for the Epure term, but it becomes [int],
when we construct the final program expression. Probably,
the only reasonable solution is to keep variables and
functions in the same namespace, so that [x] simply can
not be used in annotations after being redefined as a
program function.

Refinement code requires private types to reside in
separate program declarations. So we split type decls
into chunks where all non-free types are declared
separately and only constructible (Ddata) types are
kept together. The code preserves the original order
wherever possible.

Also, export ls_of_rs and fd_of_rs from Expr: these are
used everywhere in src/mlw anyway.

Also, remove some range/float-related "assert false".

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.

use "begin <spec> <expr_seq> end" instead. The word "abstract" is
now only used to declare a private type whose fields are all ghost.