• Andrei Paskevich's avatar
    Merge branch 'autodereference' · 10e54f43
    Andrei Paskevich authored
    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.
ocaml-unsafe-int.drv 6.99 KB