GitLab

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.

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.

A symbol is now considered overloadable if it satisfies
the following conditions:
  - it has at least one parameter
  - it is non-ghost and has fully visible result
  - all of its parameters are non-ghost and have the same type
  - its result is either of the same type as its parameters
    or it is a monomorphic immutable type.

An overloadable symbol can be combined with other symbols of the
same arity and overloading kind. Otherwise, the new symbol shadows
the previously defined ones.

This generalisation allows us to overload symbols such as "size"
or "length", and also symbols of arbitraty non-zero arity.

I am reluctant to generalize this any further, because then we
won't have reasonable destructible signatures for type inference.

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.

This allows to import an existing scope to the current namespace.
Not sure if we need this in the surface language, though.

This is a prototype version that requires no additional annotation.
In addition to the existing rules of scoping:

  - it is forbidden to declare two symbols with the same name
    in the same scope ("everything can be unambiguously named"),

  - it is allowed to shadow an earlier declaration with a newer one,
    if they belong to different scopes (e.g., via import),

we define one new rule:

  - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
    but (1) both of them are either
      - binary relations: t -> t -> bool,
      - binary operators: t -> t -> t, or
      - unary operators:  t -> t
    and (2) their argument types are not the same,
    then rs_old remains visible in the current scope.
    Both symbols should take non-ghost arguments and
    return non-ghost results, but effects are allowed.
    The name itself is not taken into account, hence
    it is possible to overload "div", "mod", or "fact".

Clause (1) allows us to perform type inference for a family of rsymbols,
using an appropriate generalized signature.

Clause (2) removes guaranteed ambiguities: we treat this case as
the user's intention to redefine the symbol for a given type.

Type inference failures are still possible: either due to
polymorphism (['a -> 'a] combines with [int -> int] and
will fail with the "ambiguous notation" error), or due
to inability to infer the precise types of arguments.
Explicit type annotations and/or use of qualified names
for disambiguation should always allow to bypass the errors.

Binary operations on Booleans are treated as relations, not as
operators. Thus, (+) on bool will not combine with (+) on int.

This overloading only concerns programs: in logic, the added rule
does not apply, and the old symbols get shadowed by the new ones.

In this setting, modules never export families of overloaded symbols:
it is impossible to "use import" a single module, and have access to
several rsymbols for (=) or (+).

The new "overloading" rule prefers to silently discard the previous
binding when it cannot be combined with the new one. This allows us
to be mostly backward compatible with existing programs (except for
the cases where type inference fails, as discussed above).

This rule should be enough to have several equalities for different
program types or overloaded arithmetic operations for bounded integers.
These rsymbols should not be defined as let-functions: in fact, it is
forbidden now to redefine equality in logic, and the bounded integers
should be all coerced into mathematical integers anyway.

I would like to be able to overload mixfix operators too, but
there is no reasonable generalized signature for them: compare
"([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
with "([]) : monomap -> key -> elt". If we restrict the overloading
to symbols with specific names, we might go with "'a -> 'b -> 'c" for
type inference (and even "'a -> 'b" for some prefix operators, such
as "!" or "?"). To discuss.

As we have to implement the "HERE" and "PARENT" qualifiers anyway,
allowing this shadowing lets us accept more programs without
compromising the "everything is unambigously nameable" invariant.

Exported [close_record_invariant] function from pdecl.ml so
that it can also be used in pmodule.ml

Rejecting when the refinement type does not present an invariant
and the refined type does.

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

Generation of type invariants VC (wip).

Somes experiments around the generation of type invariants implication.

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

A good example is worth a thousand words:

module Sig
  type t = private mutable {}

  val f (t: t) : int
    writes { t }
end

module Impl
  use import int.Int

  type t = { mutable size: int }

  let f (t: t) : int
    writes  { t }
    ensures { result = (old t).size }
    ensures { t.size = (old t).size + 1 }
  = let x = t.size in t.size <- t.size + 1;
    x

  clone Sig with type t = t, val f = f
end

In order for this clone to succeed, we need to add the field
[size] to the [writes] of the cloned val [f].
In the general case, we add all of the new mutable fields of
a refinement type to [writes] clause of the cloned function
(even if their values are not changed by the function execution).

FIXME: fix the case in which the type to be refined is already
declared with some mutable fields.

Code refactoring.

Check if the refinement record type possesses all the fields
(same name, same type, same ghost status) included in the
refined type.