• 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
..
alt_ergo.drv Loading commit data...
alt_ergo_common.drv Loading commit data...
alt_ergo_fp.drv Loading commit data...
alt_ergo_model.drv Loading commit data...
alt_ergo_smt2.drv Loading commit data...
beagle.drv Loading commit data...
c.drv Loading commit data...
cakeml.drv Loading commit data...
coq-common.gen Loading commit data...
coq-realize.drv Loading commit data...
coq-ssreflect.drv Loading commit data...
coq.drv Loading commit data...
cvc3.drv Loading commit data...
cvc4-realize.drv Loading commit data...
cvc4.drv Loading commit data...
cvc4_14.drv Loading commit data...
cvc4_15.drv Loading commit data...
cvc4_15_counterexample.drv Loading commit data...
cvc4_16.drv Loading commit data...
cvc4_16_counterexample.drv Loading commit data...
cvc4_bv.gen Loading commit data...
discrimination.gen Loading commit data...
eprover.drv Loading commit data...
gappa.drv Loading commit data...
iprover.drv Loading commit data...
isabelle-2017.gen Loading commit data...
isabelle-2018.gen Loading commit data...
isabelle-common.gen Loading commit data...
isabelle2017-realize.drv Loading commit data...
isabelle2017.drv Loading commit data...
isabelle2018-realize.drv Loading commit data...
isabelle2018.drv Loading commit data...
mathematica.drv Loading commit data...
mathsat.drv Loading commit data...
metis.drv Loading commit data...
metitarski.drv Loading commit data...
no-bv.gen Loading commit data...
ocaml-unsafe-int.drv Loading commit data...
ocaml64.drv Loading commit data...
polypaver.drv Loading commit data...
princess.drv Loading commit data...
psyche.drv Loading commit data...
pvs-common.gen Loading commit data...
pvs-realize.drv Loading commit data...
pvs.drv Loading commit data...
safeprover.drv Loading commit data...
simplify.drv Loading commit data...
smt-libv2-bv-realization.gen Loading commit data...
smt-libv2-bv.gen Loading commit data...
smt-libv2-floats-gnatprove.gen Loading commit data...
smt-libv2-floats-int_via_bv.gen Loading commit data...
smt-libv2-floats-int_via_real.gen Loading commit data...
smt-libv2-floats.gen Loading commit data...
smt-libv2-gnatprove.gen Loading commit data...
smt-libv2.drv Loading commit data...
smt-libv2.gen Loading commit data...
spass.drv Loading commit data...
spass_types.drv Loading commit data...
tptp-tff0.drv Loading commit data...
tptp-tff1.drv Loading commit data...
tptp.gen Loading commit data...
vampire.drv Loading commit data...
verit.drv Loading commit data...
why3.drv Loading commit data...
why3_smt.drv Loading commit data...
why3_tptp.drv Loading commit data...
yices-smt2.drv Loading commit data...
yices.drv Loading commit data...
z3.drv Loading commit data...
z3_432.drv Loading commit data...
z3_440.drv Loading commit data...
z3_440_counterexample.drv Loading commit data...
z3_bv.gen Loading commit data...
z3_smtv1.drv Loading commit data...
zenon.drv Loading commit data...
zenon_modulo.drv Loading commit data...