GitLab

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.

Translate a chain of equivalences A <-> B <-> C into a conjunction
(A <-> B) /\ (B <-> C). Implication is weaker than equivalence when
it occurs to the left of it, and is forbidden at the right hand side.
In other words, A -> B <-> C <-> D is allowed and translated into
A -> ((B <-> C) /\ (C <-> D)), and A <-> B -> C is not allowed,
and requires explicit parentheses.

All infix operations in the weakest priority group (those containing
at least one of the characters '=', '<', '>', or '~') are considered
non-associative and the chains (t1 OP t2 OP t3) are translated into
conjunctions (t1 OP t2 /\ t2 OP t3).

This does not concern implication '->' and equivalence '<->'
which are right-associative. like the rest of propositional
connectives.

we are not going to use exceptions as first-class values any time soon

In logic, a lambda-term is written (fun (x y : int) -> term).
Also, local function definitions (let f x = t1 in t2) are allowed
and translated as (let f = fun x -> t1 in t2).

- move common lexing functions to util/lexlib.mll
- move and rename Typing.create_user_tv to Ty.tv_of_string

Will be supported in programs as soon, as we enable lambdas.