• 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.
    10e54f43
Name
Last commit
Last update
..
mach Loading commit data...
algebra.mlw Loading commit data...
appmap.mlw Loading commit data...
appset.mlw Loading commit data...
array.mlw Loading commit data...
bag.mlw Loading commit data...
bintree.mlw Loading commit data...
bool.mlw Loading commit data...
bv.mlw Loading commit data...
cursor.mlw Loading commit data...
debug.mlw Loading commit data...
exn.mlw Loading commit data...
floating_point.mlw Loading commit data...
for_drivers.mlw Loading commit data...
function.mlw Loading commit data...
graph.mlw Loading commit data...
hashtbl.mlw Loading commit data...
ieee_float.mlw Loading commit data...
impmap.mlw Loading commit data...
impset.mlw Loading commit data...
int.mlw Loading commit data...
io.mlw Loading commit data...
list.mlw Loading commit data...
map.mlw Loading commit data...
matrix.mlw Loading commit data...
null.mlw Loading commit data...
number.mlw Loading commit data...
ocaml.mlw Loading commit data...
option.mlw Loading commit data...
pigeon.mlw Loading commit data...
pqueue.mlw Loading commit data...
python.mlw Loading commit data...
queue.mlw Loading commit data...
random.mlw Loading commit data...
real.mlw Loading commit data...
ref.mlw Loading commit data...
regexp.mlw Loading commit data...
relations.mlw Loading commit data...
seq.mlw Loading commit data...
set.mlw Loading commit data...
stack.mlw Loading commit data...
string.mlw Loading commit data...
sum.mlw Loading commit data...
tptp.mlw Loading commit data...
tree.mlw Loading commit data...
witness.mlw Loading commit data...