GitLab

Merge typing.ml and remove ref that is now apparently a keyword.

Auto-dereferencing references:

    let &x = ... in                     let (x: ref ...) = ... in
    f x;                    ---->       f x.contents;
    x <- ...                            x.contents <- ...

  -- recommended sugar:

    let ref x = ...          ==>        let &x = ref ...

  The & marker adds the typing constraint (x: ref ...)

  Top-level "let/val ref" and "let/val &" are allowed.

  Auto-dereferencing works in logic, but such variables
  cannot be introduced inside logical terms.

Extension to pattern matching:

    match e with                        match e with
    | (x,&y) -> y           ---->       | (x,(y: ref ...)) -> y.contents
    end                                 end

Extension to function parameters and reference passing:

    let incr (&x: ref int) =            let incr (x: ref int) =
      x <- x + 1                          x.contents <- x.contents + 1
                            ---->
    let f () =                          let f () =
      let ref x = 0 in                    let x = ref 0 in
      incr x;                             incr x;
      x                                   x.contents

  -- recommended sugar:

    let incr (ref x: int)    ==>        let incr (&x: ref int)

  The type annotation is not required. Let-functions with such
  formal parameters also prevent the actual argument from
  auto-dereferencing when used in logic. Pure logical symbols
  cannot be declared with such parameters.

  Auto-dereference suppression does not work in the middle of
  a relation chain: in "0 < x :< 17", x will be dereferenced
  even if (:<) expects a ref-parameter on the left.

Caller-side suppression of auto-dereference:

    let f () =                          let f () =
      let ref x = 0 in      ---->         let x = ref 0 in
      g &x                                g x

  The & marker can only be attached to a variable. Works in logic.

Ref-binders and &-binders in variable declarations, patterns,
and function parameters do not require importing ref.Ref.
Any example that does not use references inside data structures
can be rewritten by using ref-binders, without importing ref.Ref.

Explicit use of type symbol "ref", program function "ref",
or field "contents" require importing ref.Ref or why3.Ref.Ref.
Operations (:=) and (!) require importing ref.Ref.

Operation (:=) is fully subsumed by direct assignment (<-).

TODO: find good terminology for documentation. We want to avoid
confusion with regular OCaml-style references.

fix #219 Use snapshot of printers to display messages. Improve error.

Closes #219

See merge request !49

The snapshots using duplicate_ident_printer are there to avoid editing the
printer during display of error.
This also improves the error messages for transformation apply by adding
an error exception.

fix #220 : print for ind constr now only prints the constructor

Closes #220

See merge request !46

Also, fix a problem of search on constructor

1.2.0+git meaning 'the git dev master branch for upcoming release 1.2.0'

Ideally, the name should contain the hash of the last commit, and
the branch name. Is there any Make guru in the room?

Also, make let-functions with reference parameters
inhibit auto-dereference in logic.

We now use the information inside attributes to correctly associate a
label to each counterexamples. The information is carried inside
attributes which are preserved/collected during ce transformations and
printing to smt2.
The collection filled during the printing of the task is reused during the
printing of counterexamples to add "at label" where needed.

This is solved by collecting names of constructors with no arguments
during printing.

These projections are necessary because records have changed from
old system to new system. Previously, a record was never abstract.
Subsequently, we could always give value to its fields independently.
Now, when a record (or algebraic type, not handled by this commit) is
abstract, we use the function defined for its fields as projections.
So, we need to have several projections per constant in order to represent
those as values.

This patch is also a first step to the necessary cleaning of ce treatment
code.

congruence transformation

See merge request !20