Commit 10e54f43 authored by Andrei Paskevich's avatar Andrei Paskevich

Merge branch 'autodereference'

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.
parents 25315953 67c1adfb
......@@ -5,13 +5,15 @@ prelude "#include <stdint.h>"
prelude "#include <stdio.h>"
prelude "#include <assert.h>"
module ref.Ref
module Ref
syntax type ref "%1"
syntax val ref "%1"
syntax val contents "%1"
end
module ref.Ref
syntax val (!_) "%1"
syntax val (:=) "%1 = %2"
syntax val contents "%1"
end
module mach.int.Unsigned
......
......@@ -48,10 +48,13 @@ theory list.Length
syntax function length "List.length %1"
end
module ref.Ref
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -69,6 +69,17 @@ end
(* WhyML *)
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
module stack.Stack
syntax type t "(%1 Stack.t)"
syntax val create "Stack.create"
......
......@@ -68,10 +68,13 @@ theory list.Combine
syntax function combine "List.combine %1 %2"
end
module ref.Ref
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val ref "ref %1"
end
module ref.Ref
syntax val (!_) "!%1"
syntax val (:=) "%1 := %2"
end
......
......@@ -24,23 +24,23 @@ end
module Simple
use int.Int
use ref.Ref
use ref.Refint
use Square
let isqrt (x:int) : int
requires { x >= 0 }
ensures { isqrt_spec x result }
= let count = ref 0 in
let sum = ref 1 in
while !sum <= x do
invariant { !count >= 0 }
invariant { x >= sqr !count }
invariant { !sum = sqr (!count+1) }
variant { x - !count }
count := !count + 1;
sum := !sum + 2 * !count + 1
= let ref count = 0 in
let ref sum = 1 in
while sum <= x do
invariant { count >= 0 }
invariant { x >= sqr count }
invariant { sum = sqr (count+1) }
variant { x - count }
count += 1;
sum += 2 * count + 1
done;
!count
count
let main ()
ensures { result = 4 }
......@@ -62,32 +62,32 @@ module NewtonMethod
ensures { isqrt_spec x result }
= if x = 0 then 0 else
if x <= 3 then 1 else
let y = ref x in
let z = ref ((1 + x) / 2) in
while !z < !y do
variant { !y }
invariant { !z > 0 }
invariant { !y > 0 }
invariant { !z = div (div x !y + !y) 2 }
invariant { x < sqr (!y + 1) }
invariant { x < sqr (!z + 1) }
y := !z;
z := (x / !z + !z) / 2;
let ref y = x in
let ref z = (1 + x) / 2 in
while z < y do
variant { y }
invariant { z > 0 }
invariant { y > 0 }
invariant { z = div (div x y + y) 2 }
invariant { x < sqr (y + 1) }
invariant { x < sqr (z + 1) }
y <- z;
z <- (x / z + z) / 2;
(* A few hints to prove preservation of the last invariant *)
assert { x < sqr (!z + 1)
by let a = div x !y in
x < a * !y + !y
so a + !y <= 2 * !z + 1
so sqr (a + !y + 1) <= sqr (2 * !z + 2)
so 4 * (sqr (!z + 1) - x)
= sqr (2 * !z + 2) - 4 * x
>= sqr (a + !y + 1) - 4 * x
> sqr (a + !y + 1) - 4 * (a * !y + !y)
= sqr (a + 1 - !y)
assert { x < sqr (z + 1)
by let a = div x y in
x < a * y + y
so a + y <= 2 * z + 1
so sqr (a + y + 1) <= sqr (2 * z + 2)
so 4 * (sqr (z + 1) - x)
= sqr (2 * z + 2) - 4 * x
>= sqr (a + y + 1) - 4 * x
> sqr (a + y + 1) - 4 * (a * y + y)
= sqr (a + 1 - y)
>= 0 }
done;
assert { !y * !y <= div x !y * !y
by !y <= div x !y };
!y
assert { y * y <= div x y * y
by y <= div x y };
y
end
......@@ -25,7 +25,7 @@
(defconst why3-font-lock-keywords-1
(list
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "pure" "returns" "raises" "reads" "writes" "alias" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "partial" "raise" "return" "break" "continue" "try" "with" "theory" "uses" "module" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "partial" "raise" "ref" "return" "break" "continue" "try" "with" "theory" "uses" "module" "fun" "at" "old" "true" "false" "forall" "exists" "label" "by" "so" "meta")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -10,7 +10,7 @@ check,clone,coinductive,constant,continue,diverges,do,done,downto,%
else,end,ensures,exception,exists,export,false,for,forall,fun,%
function,ghost,goal,if,import,in,inductive,invariant,label,lemma,%
let,loop,match,meta,module,mutable,not,old,%
predicate,private,pure,raise,raises,reads,rec,requires,result,return,%
predicate,private,pure,raise,raises,reads,rec,ref,requires,result,return,%
returns,scope,so,then,theory,to,true,try,type,use,val,variant,while,%
with,writes},%
string=[b]",%
......
This diff is collapsed.
......@@ -30,13 +30,14 @@ val dity_bool : dity
val dity_unit : dity
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
type dref = bool list * bool
(** Patterns *)
type dpattern = private {
dp_pat : pre_pattern;
dp_dity : dity;
dp_vars : dity Mstr.t;
dp_vars : (dity * bool) Mstr.t;
dp_loc : Loc.position option;
}
......@@ -101,7 +102,7 @@ type dexpr = private {
}
and dexpr_node =
| DEvar of string * dvty
| DEvar of string * dvty * dref
| DEsym of prog_symbol
| DEconst of Number.constant * dity
| DEapp of dexpr * dexpr
......@@ -123,7 +124,7 @@ and dexpr_node =
| DEoptexn of preid * dity * mask * dexpr
| DEassert of assertion_kind * term later
| DEpure of term later * dity
| DEvar_pure of string * dvty
| DEvar_pure of string * dvty * dref
| DEls_pure of lsymbol * bool
| DEpv_pure of pvsymbol
| DEabsurd
......@@ -189,6 +190,9 @@ type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
val undereference : dexpr -> dexpr
(* raises Not_found if the argument is not auto-dereferenced *)
(** Final stage *)
val expr : ?keep_loc:bool -> ?ughost:bool -> dexpr -> expr
......
......@@ -372,7 +372,7 @@ let e_attr_copy { e_attrs = attrs; e_loc = loc } e =
let loc = if e.e_loc = None then loc else e.e_loc in
{ e with e_attrs = attrs; e_loc = loc }
let proxy_attr = create_attribute "whyml_proxy_symbol"
let proxy_attr = create_attribute "mlw:proxy_symbol"
let proxy_attrs = Sattr.singleton proxy_attr
let rec e_attr_push ?loc l e = match e.e_node with
......
......@@ -391,7 +391,7 @@ let exec_print _ args =
let built_in_modules =
[
["bool"],"Bool", [],
["why3"; "Bool"],"Bool", [],
[ "True", eval_true ;
"False", eval_false ;
] ;
......@@ -505,14 +505,16 @@ let built_in_modules =
"set", exec_matrix_set ;
"copy", exec_matrix_copy ;
] ;
["ref"],"Ref",
[], (* ? *)
["why3"; "Ref"],"Ref", [],
["ref", exec_ref_make ;
Ident.op_prefix "!", exec_ref_get;
"mk ref", exec_ref_make ;
"contents", exec_ref_get ;
] ;
["ref"],"Ref", [],
[Ident.op_prefix "!", exec_ref_get;
Ident.op_infix ":=", exec_ref_set;
] ;
["debug"],"Debug",
[],
["debug"],"Debug", [],
["print", exec_print ] ;
]
......
......@@ -527,8 +527,6 @@ let create_let_decl ld =
| LDvar ({pv_vs = {vs_name = {id_loc = loc}}},e) ->
if not (ity_closed e.e_ity) then
Loc.errorm ?loc "Top-level variables must have monomorphic type";
if match e.e_node with Eexec _ -> false | _ -> true then
Loc.errorm ?loc "Top-level computations must carry a specification";
[], [], []
| LDrec rdl ->
let add_rd sm d = Mrs.add d.rec_rsym d.rec_sym sm in
......
......@@ -686,7 +686,8 @@ and exec_call env rs args ity_result =
let env = add_local_funs locals env in
begin
match d.c_node with
| Capp _ -> assert false (* TODO ? *)
| Capp (rs',pvl) ->
exec_call env rs' (pvl @ args) ity_result
| Cpur _ -> assert false (* TODO ? *)
| Cany -> raise CannotCompute
| Cfun body ->
......
......@@ -71,6 +71,12 @@ let same_overload r1 r2 =
| FixedRes t1, FixedRes t2 -> ity_equal t1 t2
| _ -> false (* two NoOver's are not the same *)
let ref_attr = Ident.create_attribute "mlw:reference_var"
let has_ref s =
let has v = Sattr.mem ref_attr v.pv_vs.vs_name.id_attrs in
List.exists has s.rs_cty.cty_args
exception IncompatibleNotation of string
let merge_ps chk x vo vn =
......@@ -87,12 +93,14 @@ let merge_ps chk x vo vn =
(* but we can merge two compatible symbols *)
| RS r1, RS r2 ->
if rs_equal r1 r2 then vo else
if has_ref r1 || has_ref r2 then vn else
if not (same_overload r1 r2) then vn else
if ity_equal (fsty r1) (fsty r2) then vn else
OO (Srs.add r2 (Srs.singleton r1))
(* or add a compatible symbol to notation *)
| OO s1, RS r2 ->
if Srs.mem r2 s1 then vo else
if has_ref r2 then vn else
let r1 = Srs.choose s1 in
if not (same_overload r1 r2) then vn else
let ty = fsty r2 in
......@@ -398,6 +406,33 @@ let unit_module =
let td = create_alias_decl (id_fresh "unit") [] ity_unit in
close_module (List.fold_left add uc (create_type_decl [td]))
let itd_ref =
let tv = create_tvsymbol (id_fresh "a") in
let attrs = Sattr.singleton (create_attribute "model_trace:") in
let pj = create_pvsymbol (id_fresh ~attrs "contents") (ity_var tv) in
create_plain_record_decl ~priv:false ~mut:true (id_fresh "ref")
[tv] [true, pj] [] []
let its_ref = itd_ref.itd_its
let rs_ref_cons = List.hd itd_ref.itd_constructors
let rs_ref_proj = List.hd itd_ref.itd_fields
let ts_ref = its_ref.its_ts
let ls_ref_cons = ls_of_rs rs_ref_cons
let ls_ref_proj = ls_of_rs rs_ref_proj
let rs_ref_ld, rs_ref =
let cty = rs_ref_cons.rs_cty in
let ityl = List.map (fun v -> v.pv_ity) cty.cty_args in
let_sym (id_fresh "ref") (c_app rs_ref_cons [] ityl cty.cty_result)
let ref_module =
let add uc d = add_pdecl_raw ~warn:false uc d in
let uc = empty_module dummy_env (id_fresh "Ref") ["why3";"Ref"] in
let uc = List.fold_left add uc (create_type_decl [itd_ref]) in
let uc = use_export uc builtin_module (* needed for "=" *) in
close_module (add uc (create_let_decl rs_ref_ld))
let create_module env ?(path=[]) n =
let m = empty_module env n path in
let m = use_export m builtin_module in
......@@ -408,6 +443,8 @@ let create_module env ?(path=[]) n =
let add_use uc d = Sid.fold (fun id uc ->
if id_equal id ts_func.ts_name then
use_export uc highord_module
else if id_equal id ts_ref.ts_name then
use_export uc ref_module
else match is_ts_tuple_id id with
| Some n -> use_export uc (tuple_module n)
| None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc
......@@ -1187,6 +1224,7 @@ end)
let mlw_language_builtin =
let builtin s =
if s = unit_module.mod_theory.th_name.id_string then unit_module else
if s = ref_module.mod_theory.th_name.id_string then ref_module else
if s = builtin_theory.th_name.id_string then builtin_module else
if s = highord_theory.th_name.id_string then highord_module else
if s = bool_theory.th_name.id_string then bool_module else
......
......@@ -48,6 +48,8 @@ type overload =
val overload_of_rs : rsymbol -> overload
val ref_attr : Ident.attribute
exception IncompatibleNotation of string
(** {2 Module} *)
......@@ -138,6 +140,15 @@ val bool_module : pmodule
val unit_module : pmodule
val highord_module : pmodule
val tuple_module : int -> pmodule
val ref_module : pmodule
val its_ref : itysymbol
val ts_ref : tysymbol
val rs_ref : rsymbol
val rs_ref_cons : rsymbol
val rs_ref_proj : rsymbol
val ls_ref_cons : lsymbol
val ls_ref_proj : lsymbol
(** {2 WhyML language} *)
......
......@@ -85,6 +85,7 @@
"raises", RAISES;
"reads", READS;
"rec", REC;
"ref", REF;
"requires", REQUIRES;
"return", RETURN;
"returns", RETURNS;
......@@ -222,6 +223,8 @@ rule token = parse
{ DOT }
| ".."
{ DOTDOT }
| "&"
{ AMP }
| "|"
{ BAR }
| "<"
......
This diff is collapsed.
......@@ -31,6 +31,7 @@ type pty =
| PTtyvar of ident
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTref of pty list
| PTarrow of pty * pty
| PTscope of qualid * pty
| PTparen of pty
......@@ -73,6 +74,7 @@ and term_desc =
| Tfalse
| Tconst of Number.constant
| Tident of qualid
| Tasref of qualid
| Tidapp of qualid * term list
| Tapply of term * term
| Tinfix of term * ident * term
......@@ -120,11 +122,13 @@ type expr = {
}
and expr_desc =
| Eref
| Etrue
| Efalse
| Econst of Number.constant
(* lambda-calculus *)
| Eident of qualid
| Easref of qualid
| Eidapp of qualid * expr list
| Eapply of expr * expr
| Einfix of expr * ident * expr
......@@ -136,7 +140,7 @@ and expr_desc =
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
| Eassign of (expr * qualid * expr) list
| Eassign of (expr * qualid option * expr) list
(* control *)
| Esequence of expr * expr
| Eif of expr * expr * expr
......
This diff is collapsed.
......@@ -13,15 +13,11 @@
module Ref
type ref 'a = { mutable contents [@model_trace:] : 'a }
use export why3.Ref.Ref
function (!) (x: ref 'a) : 'a = x.contents
let function (!) (r: ref 'a) = r.contents
let ref (v: 'a) ensures { result = { contents = v } } = { contents = v }
let (!) (r:ref 'a) ensures { result = !r } = r.contents
let (:=) (r:ref 'a) (v:'a) ensures { !r = v } = r.contents <- v
let (:=) (ref r:'a) (v:'a) ensures { r = v } = r <- v
end
......@@ -34,11 +30,11 @@ module Refint
use int.Int
use export Ref
let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1
let decr (r: ref int) ensures { !r = old !r - 1 } = r := !r - 1
let incr (ref r: int) ensures { r = old r + 1 } = r <- r + 1
let decr (ref r: int) ensures { r = old r - 1 } = r <- r - 1
let (+=) (r: ref int) (v: int) ensures { !r = old !r + v } = r := !r + v
let (-=) (r: ref int) (v: int) ensures { !r = old !r - v } = r := !r - v
let ( *= ) (r: ref int) (v: int) ensures { !r = old !r * v } = r := !r * v
let (+=) (ref r: int) (v: int) ensures { r = old r + v } = r <- r + v
let (-=) (ref r: int) (v: int) ensures { r = old r - v } = r <- r - v
let ( *= ) (ref r: int) (v: int) ensures { r = old r * v } = r <- r * v
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment