record update in programs; match on mutable types

parent 0c8cbaa1
module M
use import int.Int
type t 'a = {| a: 'a; b: bool; c: 'a |}
let test1 (x: t bool) =
{| x with a = 0 |}
end
module M
use import int.Int
type t 'a = {| a: 'a; b: bool; c: 'a |}
let test1 (x: t bool) =
{| x with a = 0; c = True |}
end
......@@ -1146,6 +1146,8 @@ expr_sub:
{ mk_expr (Etuple ($2 :: $4)) }
| LEFTREC list1_field_expr opt_semicolon RIGHTREC
{ mk_expr (Erecord (List.rev $2)) }
| LEFTREC expr_arg WITH list1_field_expr opt_semicolon RIGHTREC
{ mk_expr (Eupdate ($2, List.rev $4)) }
| BEGIN END
{ mk_expr (Etuple []) }
| expr_arg LEFTSQ expr RIGHTSQ
......
......@@ -211,6 +211,7 @@ and expr_desc =
| Eletrec of (ident * binder list * variant option * triple) list * expr
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
| Eassign of expr * qualid * expr
(* control *)
| Esequence of expr * expr
......
......@@ -625,6 +625,15 @@ and dterm_node ~localize loc uc env = function
let p = { dp_node = Papp (cs,pl) ; dp_ty = e.dt_ty } in
(* prepare the result *)
let tyl,ty = Denv.specialize_lsymbol ~loc cs in
let set_pat_var_ty f tyf = match f with
| Some _ ->
()
| None ->
let _, xty as v = Queue.take q in
assert (Denv.unify xty tyf);
Queue.push v q
in
List.iter2 set_pat_var_ty fl tyl;
let al = List.map2 (fun f ty -> match f with
| Some (_,e) ->
let loc = e.pp_loc in
......@@ -632,8 +641,7 @@ and dterm_node ~localize loc uc env = function
unify_raise ~loc:loc e.dt_ty ty;
e
| None ->
let (x,xty) = Queue.take q in
unify_raise ~loc xty ty;
let (x, _) = Queue.take q in
{ dt_node = Tvar x ; dt_ty = ty }) fl tyl
in
let t = { dt_node = Tapp (cs,al) ; dt_ty = Util.of_option ty } in
......
o get rid of types Pgm_ttree.{ipattern, pattern} (use logical patterns instead)
o bug in test-pgm-jcf: scope
o freshness analysis
......@@ -6,14 +8,14 @@ o freshness analysis
o no `old' in loop invariants
o use of old in loop invariant should be reported as an error (correctly)
o {| e with x1 = e1; ...; xn = en |}
o syntactic sugar for postcondition:
{ pat | q } stands for { let pat = result in q }
particular case { x | ... } to use x instead of result
but also { a,b | ... }, etc.
Andrei: bad idea
o automatically add a label pre_f at entrance of each function f
and then replace (old t) by (at t pre_f)
(so that there is no more 'old' in the abstract syntax)
......
......@@ -177,6 +177,7 @@ type label = Term.vsymbol
type irec_variant = ivsymbol * Term.term * Term.lsymbol option
(* FIXME: get rid of ipattern *)
type ipattern = {
ipat_pat : Term.pattern; (* program variables *)
ipat_node : ipat_node;
......@@ -242,7 +243,7 @@ type pattern = {
ppat_node : ppat_node;
}
and ppat_node =
and ppat_node =
| Pwild
| Pvar of pvsymbol
| Papp of Term.lsymbol * pattern list
......
......@@ -473,7 +473,7 @@ and dexpr_desc ~ghost env loc = function
let constructor d f tyf = match f with
| Some (_, f) ->
let f = dexpr ~ghost env f in
assert (Denv.unify f.dexpr_type tyf);
expected_type f tyf;
let ty = create_type_var loc in
assert (Denv.unify d.dexpr_type (tyapp ts_arrow [tyf; ty]));
create (DEapply (d, f)) ty
......@@ -486,6 +486,60 @@ and dexpr_desc ~ghost env loc = function
in
let d = List.fold_left2 constructor d fl tyl in
d.dexpr_desc, ty
| Ptree.Eupdate (e1, fl) ->
let e1 = dexpr ~ghost env e1 in
let _, cs, fl = Typing.list_fields (impure_uc env.uc) fl in
let tyl, ty = Denv.specialize_lsymbol ~loc cs in
let ty = of_option ty in
expected_type e1 ty;
let n = ref (-1) in
let q = Queue.create () in
(* prepare the pattern *)
let pl = List.map2 (fun f ty -> match f with
| Some _ ->
{ dp_node = Denv.Pwild ; dp_ty = ty }
| None ->
let x = incr n; "x:" ^ string_of_int !n in
let i = { id = x ; id_lab = []; id_loc = loc } in
Queue.add (x,ty) q;
{ dp_node = Denv.Pvar i ; dp_ty = ty }) fl tyl
in
let p = { dp_node = Denv.Papp (cs,pl) ; dp_ty = ty } in
(* prepare the result *)
new_regions_vars ();
let tyl, ty = specialize_lsymbol ~loc (Htv.create 17) cs in
let ty = of_option ty in
(* unify pattern variable types with expected types *)
let set_pat_var_ty f tyf = match f with
| Some _ ->
()
| None ->
let _, xty as v = Queue.take q in
assert (Denv.unify xty tyf);
Queue.push v q
in
List.iter2 set_pat_var_ty fl tyl;
let create d ty = { dexpr_desc = d; dexpr_type = ty; dexpr_loc = loc } in
let apply t f tyf = match f with
| Some (_,e) ->
let e = dexpr ~ghost env e in
expected_type e tyf;
let ty = create_type_var loc in
assert (Denv.unify t.dexpr_type (tyapp ts_arrow [tyf; ty]));
create (DEapply (t, e)) ty
| None ->
let x, _ = Queue.take q in
let v = create (DElocal (x, tyf)) tyf in
let ty = create_type_var loc in
assert (Denv.unify t.dexpr_type (tyapp ts_arrow [tyf; ty]));
create (DEapply (t, v)) ty
in
let t =
let ps = get_psymbol cs in
create (DElogic ps.ps_pure) (dcurrying tyl ty)
in
let t = List.fold_left2 apply t fl tyl in
DEmatch (e1, [p, t]), ty
| Ptree.Eassign (e1, q, e2) ->
let e1 = dexpr ~ghost env e1 in
let e2 = dexpr ~ghost env e2 in
......@@ -1563,8 +1617,6 @@ and expr_desc gl env loc ty = function
in
d, tpure ty, ef
| IEmatch (i, bl) ->
if is_mutable_ty i.i_impure.vs_ty then
errorm ~loc "cannot match over a reference";
let v = Mvs.find i.i_impure env in
let branch ef (p, e) =
let env, p = pattern env p in
......
theory Test
use import bool.Bool
type t 'a = {| a: 'a; b: bool; c: 'a |}
goal G: forall x: t bool.
{| x with a = 0 |}.a = 0
end
theory Order
type t
logic (<=) t t
......
......@@ -3,35 +3,26 @@ module M
use import int.Int
use import module ref.Ref
parameter r : ref int
type t 'a = {| a: 'a; b: bool; c: 'a |}
let test1 () =
let x = ref 0 in
let f (y: int) = {} x := !x + y { !x = old !x + y } in
f 2;
assert { !x = 2 }
let rec test2 () =
{ }
r := 0
{ !r = 0 }
let test1 (x: t (ref int)) =
{}
let y = {| x with a = 0; c = 0 |} in
x = y
{ result = True }
(***
use import option.Option
parameter clear (o : option (ref int)) :
{} unit writes (match o with Some r -> r end).contents { !r = 0 }
let test4 () =
let r = ref 0 in
let a = (r, 0) in
incr_fst a;
assert { !(fst a) = 1 }
***)
(* BUG: x escapes its scope (in the postcondition) => should be an error *)
(* let scope (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 } *)
let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !a = 0 }
let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end
(* let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !a = 0 } *)
(* let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end *)
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