no more particular case for field access in programs (rollback on commit 852ed2a9)

src/parser/parser.pre.mly

@@ -1030,9 +1030,9 @@ expr:
      mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [t]) }
 | expr LARROW expr
     { match $1.expr_desc with
-        | Eaccess (e1, x) -> 
-            mk_expr (Eassign (e1, x, $3))
-	| Eapply (e11, e12) -> begin match e11.expr_desc with
+        | Eapply (e11, e12) -> begin match e11.expr_desc with
+            | Eident x ->
+                mk_expr (Eassign (e12, x, $3))
             | Eapply ({ expr_desc = Eident (Qident x) }, e11)
       	      when x.id = mixfix "[]" ->
                 mk_mixfix3 "[]<-" e11 e12 $3
@@ -1132,7 +1132,7 @@ expr_dot:
 
 expr_sub:
 | expr_dot DOT lqualid_rich
-   { mk_expr (Eaccess ($1, $3)) }
+   { mk_expr (mk_apply (mk_expr_i 3 (Eident $3)) [$1]) }
 | LEFTPAR expr RIGHTPAR
     { $2 }
 | BEGIN expr END

src/parser/ptree.ml

@@ -211,7 +211,6 @@ and expr_desc =
   | Eletrec of (ident * binder list * variant option * triple) list * expr
   | Etuple of expr list
   | Erecord of (qualid * expr) list
-  | Eaccess of expr * qualid
   | Eassign of expr * qualid * expr
   (* control *)
   | Esequence of expr * expr

src/programs/pgm_ttree.ml

@@ -111,7 +111,6 @@ and dexpr_desc =
   | DEfun of dubinder list * dtriple
   | DElet of ident * dexpr * dexpr
   | DEletrec of drecfun list * dexpr
-  | DEaccess of dexpr * Term.lsymbol * int option
   | DEassign of dexpr * Term.lsymbol * int * dexpr
 
   | DEsequence of dexpr * dexpr
@@ -198,6 +197,7 @@ type iexpr = {
 
 and iexpr_desc =
   | IElogic of Term.term (* pure *)
+      * Term.Svs.t (* local impure variables *) * Spv.t (* globals *)
   | IElocal of ivsymbol
   | IEglobal of psymbol * type_v
   | IEapply of iexpr * ivsymbol
@@ -206,7 +206,6 @@ and iexpr_desc =
   | IEfun of ibinder list * itriple
   | IElet of ivsymbol * iexpr * iexpr
   | IEletrec of irecfun list * iexpr
-  | IEaccess of ivsymbol * Term.lsymbol * R.t option
 
   | IEif of iexpr * iexpr * iexpr
   | IEloop of loop_annotation * iexpr

src/programs/pgm_types.ml

@@ -603,13 +603,11 @@ and E : sig
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    (* globals : Spv.t; *)
   }
 
   val empty : t
 
   val add_read  : R.t -> t -> t
-  (* val add_glob  : T.pvsymbol -> t -> t *)
   val add_write : R.t -> t -> t
   val add_raise : T.esymbol -> t -> t
   val add_var   : T.pvsymbol -> t -> t (* add all regions for x, in reads *)
@@ -641,19 +639,17 @@ end = struct
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    (* globals: Spv.t; *)
   }
 
   let empty = {
     reads = Sreg.empty;
     writes = Sreg.empty;
     raises = Sexn.empty;
-    (* globals = Spv.empty; *) }
+  }
 
   let add_read  r t = { t with reads  = Sreg.add r t.reads  }
   let add_write r t = { t with writes = Sreg.add r t.writes }
   let add_raise e t = { t with raises = Sexn.add e t.raises }
-  (* let add_glob  pv t = { t with globals = Spv.add pv t.globals } *)
   let add_var pv ef = Sreg.fold add_read pv.pv_regions ef
 
   let remove s t =

src/programs/pgm_types.mli

@@ -189,13 +189,11 @@ and E : sig
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    (* globals: Spv.t; *)
   }
 
   val empty : t
 
   val add_read  : R.t -> t -> t
-  (* val add_glob  : T.pvsymbol -> t -> t *)
   val add_write : R.t -> t -> t
   val add_raise : T.esymbol -> t -> t
   val add_var   : T.pvsymbol -> t -> t

src/programs/pgm_typing.ml

@@ -495,28 +495,6 @@ and dexpr_desc ~ghost env loc = function
       in
       let d = List.fold_left2 constructor d fl tyl in
       d.dexpr_desc, ty
-  | Ptree.Eaccess (e1, q) ->
-      let e1 = dexpr ~ghost env e1 in
-      let x = Typing.string_list_of_qualid [] q in
-      let ls =
-	try ns_find_ls (get_namespace (impure_uc env.uc)) x
-	with Not_found -> errorm ~loc "unbound record field %a" print_qualid q
-      in
-      new_regions_vars ();
-      let ty2 = match specialize_lsymbol ~loc (Htv.create 17) ls with
-	| [ty1], Some ty2 -> expected_type e1 ty1; ty2
-	| _ -> assert false
-      in
-      begin match Typing.is_projection (impure_uc env.uc) ls with
-	| Some (ts, _, i)  ->
-	    let mt = get_mtsymbol ts in
-	    let j = 
-	      try Some (mutable_field mt.mt_effect i) with Not_found -> None
-	    in
-	    DEaccess (e1, ls, j), ty2
-	| _ ->
-	    errorm ~loc "unbound record field %a" print_qualid q
-      end
   | Ptree.Eassign (e1, q, e2) ->
       let e1 = dexpr ~ghost env e1 in
       let e2 = dexpr ~ghost env e2 in
@@ -536,15 +514,15 @@ and dexpr_desc ~ghost env loc = function
       begin match Typing.is_projection (impure_uc env.uc) ls with
 	| Some (ts, _, i)  ->
 	    let mt = get_mtsymbol ts in
-	    let j = 
-	      try mutable_field mt.mt_effect i 
+	    let j =
+	      try mutable_field mt.mt_effect i
 	      with Not_found -> errorm ~loc "not a mutable field"
 	    in
 	    DEassign (e1, ls, j, e2), dty_unit env.uc
 	| None ->
 	    errorm ~loc "unbound record field %a" print_qualid q
       end
- 
+
   | Ptree.Esequence (e1, e2) ->
       let e1 = dexpr ~ghost env e1 in
       expected_type e1 (dty_unit env.uc);
@@ -918,26 +896,28 @@ let mk_t_if gl f =
   ls(x1,x2,...,xn)
 *)
 let make_logic_app gl loc ty ls el =
-  let rec make args = function
+  let rec make lvars gvars args = function
     | [] ->
         begin match ls.ls_value with
           | Some _ ->
               let t = fs_app ls (List.rev args) (purify ty) in
-              IElogic t
-          | None -> IElogic (mk_t_if gl (ps_app ls (List.rev args)))
+              IElogic (t, lvars, gvars)
+          | None ->
+	      IElogic (mk_t_if gl (ps_app ls (List.rev args)), lvars, gvars)
         end
-    | ({ iexpr_desc = IElogic t }, _) :: r ->
-        make (t :: args) r
+    | ({ iexpr_desc = IElogic (t, lvt, gvt) }, _) :: r ->
+        make (Svs.union lvars lvt) (Spv.union gvars gvt) (t :: args) r
     | ({ iexpr_desc = IElocal v }, _) :: r ->
-        make (t_var v.i_pure :: args) r
+        make (Svs.add v.i_impure lvars) gvars (t_var v.i_pure :: args) r
     | ({ iexpr_desc = IEglobal ({ ps_kind = PSvar v }, _) }, _) :: r ->
-        make (t_var v.pv_pure :: args) r
+        make lvars (Spv.add v gvars) (t_var v.pv_pure :: args) r
     | (e, _) :: r ->
         let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in
-        let d = mk_iexpr loc ty (make (t_var v.i_pure :: args) r) in
+	let lvars = Svs.add v.i_impure lvars in
+        let d = mk_iexpr loc ty (make lvars gvars (t_var v.i_pure :: args) r) in
         IElet (v, e, d)
   in
-  make [] el
+  make Svs.empty Spv.empty [] el
 
 (* same thing, but for an abritrary expression f (not an application)
    f [e1; e2; ...; en]
@@ -1013,7 +993,7 @@ open Pretty
 let print_iregion = R.print
 
 let rec print_iexpr fmt e = match e.iexpr_desc with
-  | IElogic t ->
+  | IElogic (t, _, _) ->
       print_term fmt t
   | IElocal v ->
       fprintf fmt "<local %a>" print_vs v.i_impure
@@ -1055,8 +1035,8 @@ let rec iexpr gl env e =
 
 and iexpr_desc gl env loc ty = function
   | DEconstant c ->
-      IElogic (t_const c)
-  | DElocal (x, _tyv) ->
+      IElogic (t_const c, Svs.empty, Spv.empty)
+  | DElocal (x, _) ->
       IElocal (Mstr.find x env.i_impures)
   | DEglobal (s, tv, htv) ->
       let ts = mtv_of_htv htv in
@@ -1065,9 +1045,9 @@ and iexpr_desc gl env loc ty = function
   | DElogic ls ->
       begin match ls.ls_args, ls.ls_value with
         | [], Some _ ->
-            IElogic (fs_app ls [] (purify ty))
+            IElogic (fs_app ls [] (purify ty), Svs.empty, Spv.empty)
         | [], None ->
-            IElogic (mk_t_if gl (ps_app ls []))
+            IElogic (mk_t_if gl (ps_app ls []), Svs.empty, Spv.empty)
         | al, _ ->
             errorm ~loc "function symbol %s is expecting %d arguments"
               ls.ls_name.id_string (List.length al)
@@ -1097,43 +1077,28 @@ and iexpr_desc gl env loc ty = function
       let env, dl = iletrec gl env dl in
       let e1 = iexpr gl env e1 in
       IEletrec (dl, e1)
-  | DEaccess (e1, ls, j) ->
-      let e1 = iexpr gl env e1 in
-      let x1 = create_ivsymbol (id_fresh "x") e1.iexpr_type in
-      let r = match e1.iexpr_type.ty_node, j with
-	| Ty.Tyapp (ts, tyl), Some j -> 
-	    let mt = get_mtsymbol ts in
-            let r = regions_tyapp mt.mt_effect mt.mt_regions tyl in
-            Some (List.nth r j)
-	| Ty.Tyapp _, None ->
-	    None
-	| Ty.Tyvar _, _ -> 
-	    assert false
-      in
-      IElet (x1, e1, mk_iexpr loc ty (
-      IEaccess (x1, ls, r)))
   | DEassign (e1, ls, j, e2) ->
-      (* e1.f <- e2 is syntactic sugar for 
+      (* e1.f <- e2 is syntactic sugar for
          let x1 = e1 in let x2 = e2 in any {} writes f { x1.f = x2 } *)
       let e1 = iexpr gl env e1 in
       let e2 = iexpr gl env e2 in
       let x1 = create_ivsymbol (id_fresh "x") e1.iexpr_type in
       let x2 = create_ivsymbol (id_fresh "x") e2.iexpr_type in
       let r = match e1.iexpr_type.ty_node with
-	| Ty.Tyapp (ts, tyl) -> 
+	| Ty.Tyapp (ts, tyl) ->
 	    let mt = get_mtsymbol ts in
             let r = regions_tyapp mt.mt_effect mt.mt_regions tyl in
             List.nth r j
-	| Ty.Tyvar _ -> 
+	| Ty.Tyvar _ ->
 	    assert false
       in
       let ef = { ie_reads = []; ie_writes = [r]; ie_raises = [] } in
-      let q = 
+      let q =
 	let ls = (get_psymbol ls).ps_pure in
 	t_equ (fs_app ls [t_var x1.i_pure] x2.i_pure.vs_ty) (t_var x2.i_pure)
       in
       let q = (create_vsymbol (id_fresh "result") ty, q), [] in
-      let c = { 
+      let c = {
 	ic_result_type = ITpure ty; ic_effect = ef;
 	ic_pre = t_true; ic_post = q }
       in
@@ -1233,8 +1198,12 @@ and iletrec gl env dl =
       | Some (phi, r) ->
           let p, e, q = t in
           let phi0 = create_ivsymbol (id_fresh "variant") (t_type phi) in
-          let e_phi = { iexpr_desc = IElogic phi; iexpr_type = t_type phi;
-                        iexpr_loc = e.iexpr_loc } in
+          let e_phi = {
+	    iexpr_desc = IElogic (phi, Svs.empty, Spv.empty);
+         	    (* FIXME: vars(phi) *)
+	    iexpr_type = t_type phi;
+            iexpr_loc = e.iexpr_loc }
+	  in
           let e = { e with iexpr_desc = IElet (phi0, e_phi, e) } in
           Some (phi0, phi, r), (p, e, q)
     in
@@ -1492,8 +1461,11 @@ let rec expr gl env e =
     expr_type_v = v; expr_effect = ef; expr_loc = loc }
 
 and expr_desc gl env loc ty = function
-  | IElogic t ->
+  | IElogic (t, lvars, gvars) ->
       let ef, t = term_effect E.empty t in
+      let add_lvar v ef = let v = Mvs.find v env in E.add_var v ef in
+      let ef = Svs.fold add_lvar lvars ef in
+      let ef = Spv.fold E.add_var gvars ef in
       Elogic t, tpure ty, ef
   | IElocal vs ->
       let vs = Mvs.find vs.i_impure env in
@@ -1545,12 +1517,6 @@ and expr_desc gl env loc ty = function
       let add_effect ef (_,_,_,_,ef') = E.union ef ef' in
       let ef = List.fold_left add_effect e1.expr_effect dl in
       Eletrec (dl, e1), e1.expr_type_v, ef
-  | IEaccess (i, ls, r) ->
-      let ef = option_apply E.empty (fun r -> E.add_read r E.empty) r in
-      let ls = (get_psymbol ls).ps_pure in
-      let v = Mvs.find i.i_impure env in
-      let t = fs_app ls [t_var v.pv_pure] (purify ty) in
-      Elogic t, tpure ty, ef
 
   | IEif (e1, e2, e3) ->
       let e1 = expr gl env e1 in

src/programs/pgm_wp.ml

@@ -260,34 +260,6 @@ let quantify env rm sreg f =
     in
     Sreg.fold add sreg Mtv.empty
   in
-  (* s: v -> v' and vv': pv -> v', update_v *)
-  (****
-  let mreg, s, vv' =
-    let add pv (mreg, s, vv') = match pv.pv_effect.vs_ty.ty_node with
-      | Ty.Tyapp (ts, _) ->
-          let mt = get_mtsymbol ts in
-          if mt.mt_singleton then begin (* singleton type *)
-            assert (Sreg.cardinal pv.pv_regions = 1);
-            let r = Sreg.choose pv.pv_regions in
-            (* a better name for r' *)
-            let r' = create_vsymbol (id_clone pv.pv_name) (purify r.R.r_ty) in
-            let mreg = Mreg.add r r' mreg in
-            let ty = pv.pv_pure.vs_ty in
-            let v' = create_vsymbol (id_clone pv.pv_name) ty in
-            let cs = find_constructor env mt.mt_pure in
-            let update = fs_app cs [t_var r'] ty in
-            let vv' = Mpv.add pv (v', update) vv' in
-            mreg, Mvs.add pv.pv_pure v' s, vv'
-          end else begin
-            eprintf "pv = %a@." print_pvsymbol pv;
-            failwith "WP: update not yet implemented" (* assert false *)
-          end
-      | Ty.Tyvar _ ->
-          assert false
-    in
-    Spv.fold add vars (mreg, Mvs.empty, Mpv.empty)
-  in
-  ****)
   let vv' =
     let add pv s =
       let v = pv.pv_pure in
@@ -309,19 +281,12 @@ let quantify env rm sreg f =
   Mtv.fold quantify_r mreg f
 
 let wp_close_state env rm ef f =
-  let sreg =
-    (* Spv.fold (fun pv s -> Sreg.union pv.pv_regions s) *)
-    (*   ef.E.globals *) (Sreg.union ef.E.reads ef.E.writes)
-  in
+  let sreg = Sreg.union ef.E.reads ef.E.writes in
   quantify env rm sreg f
 
 let wp_close rm ef f =
   let sreg = ef.E.writes in
-  let sreg =
-    (* Spv.fold (fun pv s -> Sreg.union pv.pv_regions s) *)
-    (*   ef.E.globals *) (Sreg.union ef.E.reads sreg)
-  in
-  (* eprintf "wp_close: ef=%a@." E.print ef; *)
+  let sreg = Sreg.union ef.E.reads sreg in
   (* all program variables involving these regions *)
   let vars =
     let add r s =
@@ -332,7 +297,6 @@ let wp_close rm ef f =
   let quantify_v v f = wp_forall v.pv_pure f in
   Spv.fold quantify_v vars f
 
-
 (* let quantify ?(all=false) env rm ef f = *)
 (*   let r = quantify ~all env rm ef f in *)
 (*   eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@] ==>@\n%a@]@." *)

tests/test-pgm-jcf.mlw

-
 module M
 
   use import int.Int