• 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.
Last commit
Last update
bash Loading commit data...
emacs Loading commit data...
images Loading commit data...
lang Loading commit data...
latex Loading commit data...
vim Loading commit data...
whyitp Loading commit data...
zsh Loading commit data...
provers-detection-data.conf Loading commit data...
strategies.conf Loading commit data...
why3session.dtd Loading commit data...