GitLab

In programs, but also in pure theories, it is not safe to compare
arbitrary types. For example, if we have a record with ghost fields,
a comparison may produce different results before and after ghost
code elimination. Even for pure types like 'map' or 'set', it is
unlikely that the result of logical equality will be the same as
the result of OCaml structural equality on the implemented type.

This commit makes the first step towards fixing this issue.
We proceed in the following way:

1. Every lsymbol (pure function or predicate symbol) carries
   a subset of type variables of its signature, called "opaque
   type variables". By marking a type variable 'a opaque in an
   lsymbol's signature, the user guarantees that this lsymbol
   can be implemented without ever comparing values of type 'a.
   In other words, this is a promise not to break into a type
   variable.

   The corresponding syntax is: "predicate safe (x y : ~'a)".

   All type variables in undefined symbols are non-opaque,
   unless annotated otherwise. Non-opaque is the default
   to keep the change conservative.

   Opacity of type variables in defined symbols is inferred
   from the definition. If the definition violates a given
   opacity annotation, an exception is raised. Notice that
   we only check definitions in _theory_ declarations. One
   can define an lsymbol in a _task_ in a way that violates
   opacity. We cannot forbid it, because various elimination
   transformations would replace safe operations (such as
   matching) with equalities. This is not a problem, since in
   the pure logical realm of provers opacity is not required
   One exception would be Coq, whose transformation chain must
   never perform such operations.

   All type variables in inductive predicates are non-opaque.
   Indeed, we can redefine equality via an inductive predicate.
   [TODO: find safe forms of inductive definitions and implement
   more reasonable restrictions.]

   All type variables in constructors and field symbols are opaque.

   It is forbidden to instantiate an opacity-preserving symbol
   with an opacity-breaking one in a clone substitution.

2. Similar type variable tracking is implemented for program symbols.
   Type variables in the signature of a "val" are non-opaque unless
   annotated otherwise. Opacity of type variables in defined symbols
   is inferred from the definition, and an exception is raised, if
   a given annotation is violated.

   The internal mechanism of tracking is different: the "eff_compar"
   field in effects contains the type variables that occur under
   equality or any other opacity-breaking operation. In this respect,
   our API is inconsistent between lsymbols and psymbols: the former
   asks for the opaque tvsymbols, the latter requires us to fill the
   spec with "comparison effects" for the non-opaque ones. [TODO:
   add the "~opaque" argument to create_psymbol and make the WhyML
   core fill the effect under the hood.]

   Every time an lsymbol or a psymbol is applied in a program,
   we check the substitution into its signature's type variables.
   If a non-opaque type variable is instantiated with a program type,
   an exception is raised. [TODO: be more precise and reject only
   types with ghost and model components - being mutable, private,
   or carrying an invariant doesn't conflict with equality.]

   Notice that we do not allow to compare program types even in
   the ghost code. This is not needed if we only consider the
   problems of the code extraction, but _might_ be necessary,
   if we also want to protect Coq realisations (see below).

This commit fixes the immediate problem of breaking the ghost
guarantees when equality or some other opacity-breaking lsymbol
is applied in a program to a type with ghost or "model" parts.

This leaves the problem of code extraction for programs that
compare complex types such as maps or sets (Coq driver is
affected by this, too, I guess). The next step is to provide
annotations for problematic type constructors. A declaration
"type ~map 'a 'b" would mean "logical equality on this type
is likely to be different from the structural equality on any
implementation of this type - therefore do not apply equality
to it: neither in programs (because this can't be implemented),
nor in pure functions (because they are extracted, too, and
because this can't be realized with Leibniz equality in Coq)."
[TODO: discuss and implement.]

[TODO: mb choose better term for "opaque" and notation for ~'a.]

Also, ghost fields in algerbraic types are now accepted in programs.

As of now, "function", "predicate", "inductive", "val", "let", "fun",
and constructors in algebraic type declarations all accept the same
syntax for parameters. In "function", "predicate", "inductive", "val",
and constructors in algebraic type declarations, binders without
colons are treated as type expressions:

    function f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    function f (_: int) (_: list bool) (_: (int,real)) (ghost _: bool)

In "let" and "fun", single unqualified idents are treated as parameter
names whose types are to be inferred, other binders without colons are
treated as type expressions:

    let f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    let f (int: ?) (_: list bool) (_: (int,real)) (ghost bool: ?)

Anonymous binders ("_") are accepted only if their type is specified.

[<file.why>|<project directory> [<file.why> ...]]

In a chain "e1 op1 e2 op2 e3 op3 e4", each relation symbol is either:

- an infix symbol "=" or "<>", or

- a binary symbol whose value type is Bool.bool or Prop (for lsymbols)
  and whose arguments' types are not Bool.bool.

In other words, we interpret a chain as a conjunction only if there
is no possibility(*) to interpret it as a superposition. The exception
is only made for "=" and "<>", which are _always_ considered as
chainable, even if they are redefined with some bogus type signatures.
Notice that redefining "<>" has no effect whatsoever, since "<>" is
always treated as negated "=".

As for the evaluation order, the chain above would be equivalent to:
    let x2 = e2 in
    (e1 op1 x2) &&
        let x3 = e3 in
        (x2 op2 x3) &&
            (x3 op3 e4)
This is due to the fact that lazy conjunctions are evaluated from
left to right, function arguments are evaluated from right to left,
and no expression should be evaluated twice.

[*] well, not really, since we consider symbols ('a -> 'b -> bool)
as chainable, even though such chains could be interpreted as
superpositions(**). We could treat such symbols as unchainable,
but that would make equality and disequality doubly special cases,
and I don't like it. We'll see if the current conditions are not
enough.

[**] what also bothers me is dynamic types of locally defined
infix symbols, which can be type variables or Bool.bool depending
on the order of operations in Mlw_typing. Currently, I can't come
up with any example of bad behaviour -- we are somewhat saved by
not being able to write "let (==) = ... in ...").

because otherwise they are likely to be missed

remove the keyword "cloned" from drivers, since it becomes
the default and only behaviour (the same for prelude strings).

Also, remove obsolete Printer.print_prelude_for_theory.

File "why3/modules/array.mlw", line 141, characters 2-26:
warning: cloned theory map.MapPermut does not contain any abstract symbol; it should be used instead

Note that warn_clone_not_abstract is not called from clone_export so that
the location of the declaration can be passed.

these return the newly created symbol, saving us a pattern matching
in let_defn.

Now, there are three kinds of types used in WhyML API:
  ity -- the type of first-order values, "i" stands for "individual"
  aty -- the type of higher-order values, "a" stands for "arrow"
  vty -- the sum of the previous two, "v" stands for "value"

We should probably rename the VTvalue constructor, since it carries
an ity, and not a vty. And I would gladly rename ity to something
more appropriate, too.

Instead, we now store the ghostness boolean directly
in pvsymbols, pssymbols, ppatterns, and exprs. We thus
remove one level of indirection, and vty_value becomes
a one-field record which we remove in the next commit.

This simplifies semantics, makes a lot of checks unnecessary,
and makes us compatible with OCaml.