GitLab

this avoids handling LEFTPAR_STAR_RIGHTPAR in the parser

The pattern-matching construct in the logic is now systematically named
"Tcase" in constructors (Ptree.Tmatch -> Tcase). The one in the
programs (supporting exceptions) is now systematically named "Ematch"
(Expr.Ecase -> Ematch, Dexpr.DEcase -> DEmatch). They are now homogeneous
with the other constructors: Term.Tcase, Dterm.DTcase, Ptree.Ematch,
Mltree.Ematch. Smart constructor Expr.e_case was renamed accordingly.

Also update of ce/bench

Changed the parser to automatically add model_trace labels during parsing.
Removed model labels in bench for counterexamples.

The feature is not yet fully implemented (e.g. escape characters).

Forces aliasing between the arguments, external reads and the
result (denoted "result"). Cannot be used for exceptional results.
Currently, is only used for "any" and "val", and is silently ignored
otherwise.

This allows why3doc to generate anchors for operator definitions,
including "(*)".

This allows why3doc to generate anchors for operator definitions,
including "(*)".

command "search" and transformations taking idents as arguments now can
support qualified idents and infix symbols.

For example, "search (+) (*)" returns the distributivity axioms

FIXME: "search Int.(+)" fails, probably missing namespaced for
imported modules

Type declarations for records (incuding the private records) can
now be followed by a "witness": a set of values for the record
fields that must satisfy the type invariant (if any). The fields
must be initialized with pure terminating program expressions.
The current syntax, proposed by Martin, is

    type t 'a = { f: ty1; g: ty2 }
      invariant { J[f,g] }
      by { f = e1; g = e2 }

The generated proof obligation is the VC for

    let g = e2 in let f = e1 in assert { J[f,g] }

In absence of an explicit witness, an existential proof obligation
"exists f,g. J[f,g]" is produced.

Without an argument, break and continue refer to the innermost loop.
A label put over an expression sequence starting with a loop, can be
used as an optional argument for break and continue:

  label L in
  [ghost] ["tag"] [M.begin]
    while true do
      ...
      break L
      ...
    done;
    [...]
  [end] [: unit]

In the square brackets are listed the constructions allowed between
the label declaration and the loop expression.

Just as abstract blocks, "white-box blocks" are program expressions
with an additional contract attached to their execution place.
Contrary to abstract blocks, whiteboxes do not hide their contents
from the outer computation. In most cases, you would not need
whiteboxes at all, as the same effect can be achieved by adding
assertions. Their utility comes from their syntax: the added
contract clauses bind to the expression and do not require
additional semicolons, begin-end's, let-in's or try-with's.

Compare:

    let x = <expr> in assert { P x }; x
to  <expr> ensures { P result }
or  <expr> returns { x -> P x }

    if ... then begin let x = <expr> in assert { P x }; x end; ...
to  if ... then <expr> ensures { P result }; ...

    try <expr> with E x -> assert { P x }; raise E x; end
to  <expr> raises { E x -> P x }

Internally, whiteboxes are just abstract blocks (zero-argument
anonymous functions executed in-place) with the label "vc:white_box"
on top. The user never needs to write this label explicitly though.

This makes the syntax cleaner and brings us closer to OCaml.

One incompatibility with the previous grammar is that "ghost"
binds stronger than the left arrow of assignment, and thus
ghost assignments have to be written as "ghost (x.f <- v)".

This is unavoidable, because assignment has to be weaker than
the tuple comma (think "x.f, y.g <- y.g, x.f" or "a[i] <- u,v"),
and "ghost" has to be stronger than comma, for consistency with
our patterns and our return types.

The "return" construction is weaker than comma, for "return a,b".
It is also weaker than assignment, though "return x.f <- b" does
not make much sense either way.

This change does not concern type expressions, where a tuple
type must always have its clothes^Wparentheses on: (int, int).
It might be nice to write "constant pair: int, bool", but on
the other hand this would break casts like "42: int, true".

- requires a lot more testing
- support in extraction missing (exception raised)
- interaction with "syntax literal" remains to investigate

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

  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.

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.