record updates

bench/typing/bad/record8.why

+theory Records
+  type t = {| a:int; b:int |}
+  goal g1 : 
+    let t = {| a = 1; b = 2 |} in
+    let t = {| t with a = () |} in
+    true
+end

bench/typing/bad/record9.why

+theory Records
+  type t = {| a:int; b:int |}
+  type t2 = {| c:int; d:int |}
+  goal g1 : 
+    let t = {| a = 1; b = 2 |} in
+    let t = {| t with d = 3 |} in
+    true
+end

src/parser/parser.pre.mly

@@ -624,6 +624,8 @@ lexpr_sub:
    { mk_pp (PPtuple ($2 :: $4)) }
 | LEFTREC list1_field_value opt_semicolon RIGHTREC
    { mk_pp (PPrecord (List.rev $2)) }
+| LEFTREC lexpr_arg WITH list1_field_value opt_semicolon RIGHTREC
+   { mk_pp (PPupdate ($2, List.rev $4)) }
 | lexpr_arg LEFTSQ lexpr RIGHTSQ
    { mk_pp (PPapp (Qident (mk_id (misfix "[]") (loc ())), [$1; $3])) }
 | lexpr_arg LEFTSQ lexpr OP1 lexpr RIGHTSQ

src/parser/ptree.ml

@@ -82,6 +82,7 @@ and pp_desc =
   | PPcast of lexpr * pty
   | PPtuple of lexpr list
   | PPrecord of (qualid * lexpr) list
+  | PPupdate of lexpr * (qualid * lexpr) list
 
 (*s Declarations. *)
 

src/parser/typing.ml

@@ -519,8 +519,7 @@ and dterm_node ~localize loc env = function
         p, e
       in
       let bl = List.map branch bl in
-      let ty = (snd (List.hd bl)).dt_ty in
-      Tmatch (t1, bl), ty
+      Tmatch (t1, bl), tb
   | PPnamed (x, e1) ->
       let e1 = dterm ~localize env e1 in
       Tnamed (x, e1), e1.dt_ty
@@ -611,6 +610,39 @@ and dterm_node ~localize loc env = function
         | None -> errorm ~loc "some record fields are missing") fl tyl
       in
       Tapp (cs,al), Util.of_option ty
+  | PPupdate (e,fl) ->
+      let n = ref (-1) in
+      let q = Queue.create () in
+      let e = dterm ~localize env e in
+      let _,cs,fl = list_fields env.uc fl in
+      (* prepare the pattern *)
+      let tyl,ty = Denv.specialize_lsymbol ~loc cs in
+      unify_raise ~loc e.dt_ty (Util.of_option ty);
+      let pl = List.map2 (fun f ty -> match f with
+        | Some _ ->
+            { dp_node = 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 = Pvar i ; dp_ty = ty }) fl tyl
+      in
+      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 al = List.map2 (fun f ty -> match f with
+        | Some (_,e) ->
+            let loc = e.pp_loc in
+            let e = dterm ~localize env e in
+            unify_raise ~loc:loc e.dt_ty ty;
+            e
+        | None ->
+            let (x,xty) = Queue.take q in
+            unify_raise ~loc xty ty;
+            { dt_node = Tvar x ; dt_ty = ty }) fl tyl
+      in
+      let t = { dt_node = Tapp (cs,al) ; dt_ty = Util.of_option ty } in
+      Tmatch (e,[p,t]), t.dt_ty
   | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
       error ~loc TermExpected
 
@@ -682,7 +714,8 @@ and dfmla_node ~localize loc env = function
       let t1 = dterm ~localize env e1 in
       let ty1 = t1.dt_ty in
       let branch (p, e) =
-        let env, p = dpat_list env ty1 p in p, dfmla ~localize env e
+        let env, p = dpat_list env ty1 p in
+        p, dfmla ~localize env e
       in
       Fmatch (t1, List.map branch bl)
   | PPnamed (x, f1) ->
@@ -695,7 +728,7 @@ and dfmla_node ~localize loc env = function
       let s, tyl = specialize_psymbol x env.uc in
       let tl = dtype_args s.ls_name loc env tyl [] in
       Fapp (s, tl)
-  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ ->
+  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ | PPupdate _ ->
       error ~loc PredicateExpected
 
 and dpat_list env ty p =

tests/test-jcf.why

@@ -12,8 +12,8 @@ theory Records
   end
 
   goal g1 :
-    let t = {| b = Cons True Nil; a = 1; |} in
-    match t with
+    let t = {| b = Cons True Nil; a = 1.0; |} in
+    match {| t with a = 1 |} with
     | {| R.b = Cons x _ |} -> x = True
     | {| a = a |} -> a = 1
     end