-
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