getting rid of old references

src/programs/pgm_types.ml

@@ -32,6 +32,8 @@ let create_mtsymbol name args model =
   Hts.add mutable_types ts mt;
   mt
 
+let is_mutable_type = Hts.mem mutable_types
+
 exception NotMutable
 
 let get_mtsymbol ts = 

src/programs/pgm_types.mli

@@ -25,6 +25,8 @@ exception NotMutable
 val get_mtsymbol : tysymbol -> mtsymbol
   (** raises [NotMutable] if [ts] is not a mutable type *)
 
+val is_mutable_type : tysymbol -> bool
+
 val ts_arrow : tysymbol
     
 (* program types *)

src/programs/pgm_typing.ml

@@ -207,17 +207,19 @@ let expected_type e ty =
 
 let pure_type env = Typing.dty env.denv
 
-let check_reference_type uc loc ty =
-  let ty_ref = dty_app (find_ts uc "ref", [create_type_var loc]) in
-  if not (Denv.unify ty ty_ref) then
-    errorm ~loc "this expression has type %a, but is expected to be a reference"
-      print_dty ty
+let check_mutable_type loc = function
+  | Denv.Tyapp (ts, _) when is_mutable_type ts -> 
+      ()
+  | ty ->
+      errorm ~loc 
+	"this expression has type %a, but is expected to have a mutable type"
+	print_dty ty
 
 let dreference env = function
-  | Qident id when Typing.mem_var id.id env.denv ->
+  | Qident id when Mstr.mem id.id env.locals ->
       (* local variable *)
-      let ty = Typing.find_var id.id env.denv in
-      check_reference_type env.uc id.id_loc ty;
+      let ty = Mstr.find id.id env.locals in
+      check_mutable_type id.id_loc ty;
       DRlocal id.id
   | qid ->
       let loc = Typing.qloc qid in
@@ -329,7 +331,7 @@ and dexpr_desc env loc = function
   | Pgm_ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals ->
       (* local variable *)
       let tyv = Mstr.find x env.locals in
-      DElocal (x, tyv), dpurify tyv
+      DElocal (x, tyv), tyv
   | Pgm_ptree.Eident p ->
       begin try
 	(* global variable *)
@@ -641,13 +643,6 @@ let make_logic_app gl loc ty ls el =
   in
   make [] el
 
-let is_ts_ref gl ts =
-  try ts_equal ts (find_ts gl "ref") with Not_found -> false
-
-let is_reference_type gl ty  = match ty.ty_node with
-  | Ty.Tyapp (ts, _) -> is_ts_ref gl ts
-  | _ -> false
-
 (* same thing, but for an abritrary expression f (not an application)
    f [e1; e2; ...; en]
 -> let x1 = e1 in ... let xn = en in (...((f x1) x2)... xn)
@@ -1055,7 +1050,7 @@ let mk_true  loc gl = mk_bool_constant loc gl (find_ls gl "True")
 let rec check_type ?(noref=false) gl loc ty = match ty.ty_node with
   | Ty.Tyapp (ts, tyl) when ts_equal ts ts_arrow ->
       List.iter (check_type gl loc) tyl
-  | Ty.Tyapp (ts, _) when noref && is_ts_ref gl ts ->
+  | Ty.Tyapp (ts, _) when noref && is_mutable_type ts ->
       errorm ~loc "inner reference types are not allowed"
   | Ty.Tyapp (_, tyl) ->
       List.iter (check_type ~noref:true gl loc) tyl
@@ -1446,9 +1441,9 @@ let rec polymorphic_pure_type ty = match ty.ty_node with
   | Ty.Tyvar _ -> true
   | Ty.Tyapp (_, tyl) -> List.exists polymorphic_pure_type tyl
 
-let cannot_be_generalized gl = function
-  | Tpure { ty_node = Ty.Tyapp (ts, [ty]) } when is_ts_ref gl ts ->
-      polymorphic_pure_type ty
+let cannot_be_generalized = function
+  | Tpure { ty_node = Ty.Tyapp (ts, tyl) } when is_mutable_type ts ->
+      List.for_all polymorphic_pure_type tyl
   | Tpure { ty_node = Ty.Tyvar _ } ->
       true
   | Tpure _ | Tarrow _ ->
@@ -1514,7 +1509,7 @@ let rec decl ~wp env penv lmod uc = function
       let tyv = dtype_v denv tyv in
       let tyv = itype_v uc Mstr.empty tyv in
       let tyv = type_v Mvs.empty tyv in
-      if cannot_be_generalized uc tyv then errorm ~loc "cannot be generalized";
+      if cannot_be_generalized tyv then errorm ~loc "cannot be generalized";
       let ps, uc = add_global loc id.id tyv uc in
       let uc = add_global_if_pure uc ps in
       add_decl (Dparam (ps, tyv)) uc (* TODO: is it really needed? *)

src/programs/pgm_wp.ml

@@ -51,13 +51,6 @@ let wp_implies = f_implies_simp
 let find_ts uc s = ns_find_ts (get_namespace (theory_uc uc)) [s]
 let find_ls uc s = ns_find_ls (get_namespace (theory_uc uc)) [s]
 
-let is_ts_ref uc ts =
-  try ts_equal ts (find_ts uc "ref") with Not_found -> false
-
-let is_ref_ty uc ty = match ty.ty_node with
-  | Tyapp (ts, _) -> is_ts_ref uc ts
-  | _ -> false
-
 let is_arrow_ty ty = match ty.ty_node with
   | Tyapp (ts, _) -> ts_equal ts ts_arrow
   | _ -> false
@@ -110,21 +103,17 @@ and erase_label_term env lab t = match t.t_node with
   | _ ->
       t_map (erase_label_term env lab) (erase_label env lab) t
 
-let unref_ty env ty = match ty.ty_node with
-  | Tyapp (ts, [ty]) when is_ts_ref env ts -> ty
-  | _ -> assert false
-
-(* replace !r by v everywhere in formula f *)
 let rec unref env r v f =
   f_map (unref_term env r v) (unref env r v) f
 
-and unref_term env r v t = match t.t_node with
-  (* | Tapp (ls, [u]) when ls_equal ls (find_ls env "prefix !") -> *)
-  (*     let rt = E.reference_of_term u in *)
-  (*     if E.ref_equal rt r then t_var v else t *)
-  | Tapp (ls, _) when ls_equal ls (find_ls env "old") ->
+and unref_term env r v t = match r, t.t_node with
+  | R.Rglobal {p_ls=ls1}, Tapp (ls2, _) when ls_equal ls1 ls2 ->
+      t_var v
+  | R.Rlocal {pv_vs=vs1}, Tvar vs2 when vs_equal vs1 vs2 ->
+      t_var v
+  | _, Tapp (ls, _) when ls_equal ls (find_ls env "old") ->
       assert false
-  | Tapp (ls, _) when ls_equal ls (find_ls env "at") -> 
+  | _, Tapp (ls, _) when ls_equal ls (find_ls env "at") -> 
       (* do not recurse in at(...) *)
       t
   | _ ->
@@ -134,7 +123,7 @@ and unref_term env r v t = match t.t_node with
 let quantify ?(all=false) env ef f =
   (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
   let quantify1 r f =
-    let ty = unref_ty env (R.type_of r) in
+    let ty = R.type_of r in
     let v = create_vsymbol (id_clone (R.name_of r)) ty in
     let f = unref env r v f in
     wp_forall v f

tests/test-pgm-jcf.mlw

@@ -12,11 +12,21 @@ let rec f91 (n:int) : int variant { 101-n } =
     n - 10
   { (n <= 100 and result = 91) or (n >= 101 and result = n - 10) }
 
-  mutable type t 'a model 'a
+  mutable type ref 'a model 'a
 
-  let f (r : t int) =
+  parameter get : r:ref 'a -> {} 'a reads r { result=r }
+
+  parameter set : r:ref 'a -> v:'a -> {} unit writes r { r=v }
+
+  let incr (r : ref int) =
+    {}
+    set r (get r + 1)
+    { r = old r + 1 }
+
+  let f (r : ref int) =
     { r = 0 }
-    if (*r*)0 <= 1 then 1 else 2
+    incr r;
+    get r
     { result = 1 }
 
 end

theories/programs.why

@@ -6,11 +6,6 @@ theory Prelude
   type unit = ()
   logic ignore 'a : unit
 
-  type arrow 'a 'b 
-
-  type  ref 'a
-  logic (!) (ref 'a) : 'a
-
   type  label
   logic at  'a label : 'a
   logic old 'a       : 'a