GitLab

Bench reestablished

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, comment out a seemingly useless invariant in
examples/topological_sorting.mlw detected by the new check.

This is important for the "loose" fields: mutable components of
a private type which can be modified without a direct write into
the containing object. These subcomponents can be modified by
abstract functions, and these modifications are actually visible,
since a refinement of a private type can make ghost fields non-ghost.

Example taken from the VOCaL project:
  let make (dummy [@ocaml:optional]: option 'a) (n: int63) (x: 'a) : t 'a
    ...

  let init (dummy [@ocaml:named]: 'a) (n: int63) (f: int63 -> 'a) : t 'a
  = let a = make None n dummy in
    ...

Now the resulting OCaml code is as follows:
  let init ~dummy:(dummy: 'a) (n: int) (f: (int) -> 'a) : 'a t =
    let a = make  n dummy in
    ...

both constructor and projection names are now added to the mod_known from
Mltree.pmodule, pointing to the type declarations in which they are introduced.

- even for range types fitting 31-bit signed integers the user must provide a
driver in order to get them extracted to OCaml's type 'int'

- range types that fit in 31-bit signed integers are mapped to OCaml's type int
  (both literals and for loops)
- a for loop on a type that is mapped to 'int' in the OCaml driver is
  translated to an OCaml for loop

Since we are going to authorize "any" and "val" to have aliases
between the argument and the results, we should only reset the
unknown regions -- and these are easier to compute inside create_cty.

Also, reset regions in local exceptions in Dexpr.cty_of_spec.

Type variables that appear in the result types of "pure"
or logical functions are "spoiled" and cannot be instantiated
with mutable types. Abstract program functions ("val") are assumed
to not spoil type variables, and no explicit effect annotation is
provided for this effect. Constructors, projections, and function
application do not spoil type variables.

This effect prevent unsoundness that results from instantiating
[constant magic : 'a] with a mutable type in a program. It is,
however, less precise than tracking of magic values using
pure type variables. For example, the following program
does typecheck with pure type variables but not with the
spoil effects.

  use seq.Seq

  type ref_hist 'a = {
          mutable contents : 'a;
    ghost mutable history  : Seq.seq {'a}
  }

  let (:=) (r : ref_hist 'a) (v : 'a) =
    r.history <- Seq.cons (pure { r.contents }) r.history;
    r.contents <- v

  let test (r : ref_hist (ref_hist unit)) =
    r := r.contents

Indeed, (:=) spoils 'a, and precludes it from being instantiated
with a mutable type in "test".