mutables types (work in progress)

share/emacs/why.el

@@ -29,7 +29,7 @@
    ;; Note: comment font-lock is guaranteed by suitable syntax entries
    ;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
    '("{\\([^}]*\\)}" . font-lock-type-face)
-   `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
+   `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model")) . font-lock-builtin-face)
    `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
    ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
    )

src/parser/denv.ml

@@ -50,6 +50,8 @@ and type_var = {
   type_var_loc : loc option;
 }
 
+let tvsymbol_of_type_var tv = tv.tvsymbol
+
 let rec print_dty fmt = function
   | Tyvar { type_val = Some t } ->
       print_dty fmt t
@@ -58,10 +60,9 @@ let rec print_dty fmt = function
   | Tyapp (s, []) ->
       fprintf fmt "%s" s.ts_name.id_string
   | Tyapp (s, [t]) ->
-      fprintf fmt "%a %s" print_dty t s.ts_name.id_string
+      fprintf fmt "%s %a" s.ts_name.id_string print_dty t
   | Tyapp (s, l) ->
-      fprintf fmt "(%a) %s"
-	(print_list comma print_dty) l s.ts_name.id_string
+      fprintf fmt "%s %a" s.ts_name.id_string (print_list comma print_dty) l
 
 let create_ty_decl_var =
   let t = ref 0 in

src/parser/denv.mli

@@ -95,3 +95,6 @@ val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
 
 val specialize_fmla : loc:Ptree.loc -> type_var Htv.t -> fmla -> dfmla
 
+(** exported for programs *)
+
+val tvsymbol_of_type_var : type_var -> tvsymbol

src/programs/pgm_types.ml

@@ -8,6 +8,50 @@ open Term
 open Decl
 module E = Pgm_effect
 
+(* mutable types *)
+
+type mtsymbol = {
+  mt_name  : ident;
+  mt_args  : tvsymbol list;
+  mt_model : ty option;
+  mt_abstr : tysymbol;
+}
+
+let mt_equal = (==)
+
+let mutable_types = Hts.create 17
+
+let create_mtsymbol name args model = 
+  let id = id_register name in
+  let ts = create_tysymbol name args None in
+  let mt = 
+    { mt_name  = id;
+      mt_args  = args;
+      mt_model = model; 
+      mt_abstr = ts; }
+  in
+  Hts.add mutable_types ts mt;
+  mt
+
+exception NotMutable
+
+let get_mtsymbol ts = 
+  try Hts.find mutable_types ts with Not_found -> raise NotMutable
+
+let model_type ty = match ty.ty_node with
+  | Tyapp (ts, tyl) when Hts.mem mutable_types ts ->
+      let mt = Hts.find mutable_types ts in
+      begin match mt.mt_model with
+	| None -> 
+	    ty
+	| Some ty ->
+	    let add mtv tv ty = Mtv.add tv ty mtv in
+	    let mtv = List.fold_left2 add Mtv.empty mt.mt_args tyl in
+	    ty_inst mtv ty
+      end
+  | Tyvar _ | Tyapp _ -> 
+      raise NotMutable
+
 (* types *)
 
 type effect = Pgm_effect.t
@@ -21,8 +65,8 @@ type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
 type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
 
 type type_v =
-  | Tpure of Ty.ty
-  | Tarrow of binder list * type_c
+  | Tpure    of Ty.ty
+  | Tarrow   of binder list * type_c
 
 and type_c =
   { c_result_type : type_v;
@@ -42,16 +86,18 @@ let make_arrow_type tyl ty =
   let arrow ty1 ty2 = Ty.ty_app ts_arrow [ty1; ty2] in
   List.fold_right arrow tyl ty
 
-let rec uncurry_type = function
-  | Tpure ty ->
+let rec uncurry_type ?(logic=false) = function
+  | Tpure ty when not logic ->
       [], ty
+  | Tpure ty ->
+      [], begin try model_type ty with NotMutable -> ty end
   | Tarrow (bl, c) ->
       let tyl1 = List.map (fun (v,_) -> v.vs_ty) bl in
-      let tyl2, ty = uncurry_type c.c_result_type in
-      tyl1 @ tyl2, ty (* TODO: improve? *)
+      let tyl2, ty = uncurry_type ~logic c.c_result_type in
+      tyl1 @ tyl2, ty (* TODO: improve efficiency? *)
 
-let purify v =
-  let tyl, ty = uncurry_type v in
+let purify ?(logic=false) v =
+  let tyl, ty = uncurry_type ~logic v in
   make_arrow_type tyl ty
 
 (* symbols *)
@@ -68,20 +114,6 @@ let create_psymbol id v =
 
 type esymbol = lsymbol
 
-type mtsymbol = {
-  mt_name  : ident;
-  mt_args  : tvsymbol list;
-  mt_model : ty option;
-}
-
-let create_mtsymbol name args model = { 
-  mt_name  = id_register name;
-  mt_args  = args;
-  mt_model = model; 
-}
-
-let mt_equal = (==)
-
 (* misc. functions *)
 
 let v_result ty = create_vsymbol (id_fresh "result") ty

src/programs/pgm_types.mli

@@ -7,7 +7,25 @@ open Theory
 open Term
 open Decl
 
-(* types *)
+(* mutable type symbols *)
+
+type mtsymbol = private {
+  mt_name  : ident;
+  mt_args  : tvsymbol list;
+  mt_model : ty option;
+  mt_abstr : tysymbol;
+}
+
+val create_mtsymbol : preid -> tvsymbol list -> ty option -> mtsymbol
+
+val mt_equal : mtsymbol -> mtsymbol -> bool
+
+exception NotMutable
+
+val get_mtsymbol : tysymbol -> mtsymbol
+  (** raises [NotMutable] if [ts] is not a mutable type *)
+
+(* program types *)
 
 type effect = Pgm_effect.t
 type reference = Pgm_effect.reference
@@ -20,8 +38,8 @@ type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
 type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
 
 type type_v = private
-  | Tpure of Ty.ty
-  | Tarrow of binder list * type_c
+  | Tpure    of Ty.ty
+  | Tarrow   of binder list * type_c
 
 and type_c =
   { c_result_type : type_v;
@@ -34,7 +52,7 @@ and binder = Term.vsymbol * type_v
 val tpure : Ty.ty -> type_v
 val tarrow : binder list -> type_c -> type_v
 
-(* symbols *)
+(* program symbols *)
 
 type psymbol = private {
   p_ls : lsymbol;
@@ -43,23 +61,16 @@ type psymbol = private {
 
 val create_psymbol : preid -> type_v -> psymbol
 
-type esymbol = lsymbol
-
-type mtsymbol = private {
-  mt_name  : ident;
-  mt_args  : tvsymbol list;
-  mt_model : ty option;
-}
-
-val create_mtsymbol : preid -> tvsymbol list -> ty option -> mtsymbol
+(* exception symbols *)
 
-val mt_equal : mtsymbol -> mtsymbol -> bool
+type esymbol = lsymbol
 
 (* program types -> logic types *)
 
 val ts_arrow : tysymbol
 
-val purify : type_v -> ty
+val purify : ?logic:bool -> type_v -> ty
+  (** when [logic] is [true], mutable types are turned into their models *)
 
 (* operations on program types *)
 

src/programs/pgm_typing.ml

@@ -176,12 +176,32 @@ let expected_type e ty =
 
 let pure_type env = Typing.dty env.denv
 
-let rec dpurify env = function
-  | DTpure ty ->
+let dmodel_type = function
+  | Tyapp (ts, tyl) as ty ->
+      let mt = get_mtsymbol ts in
+      begin match mt.mt_model with
+	| None -> 
+	    ty
+	| Some ty ->
+	    let h = Htv.create 17 in
+	    List.iter2 (Htv.add h) mt.mt_args tyl;
+	    let rec inst ty = match ty.ty_node with
+	      | Ty.Tyvar tv -> Htv.find h tv
+	      | Ty.Tyapp (ts, tyl) -> Denv.Tyapp (ts, List.map inst tyl)
+	    in
+	    inst ty
+      end
+  | Tyvar _ as ty -> 
+      ty
+
+let rec dpurify ?(logic=false) = function
+  | DTpure ty when not logic ->
       ty
+  | DTpure ty ->
+      begin try dmodel_type ty with NotMutable -> ty end
   | DTarrow (bl, c) ->
-      dcurrying (List.map (fun (_,ty) -> dpurify env ty) bl)
-	(dpurify env c.dc_result_type)
+      dcurrying (List.map (fun (_,ty) -> dpurify ~logic ty) bl)
+	(dpurify c.dc_result_type)
 
 let check_reference_type uc loc ty =
   let ty_ref = dty_app (find_ts uc "ref", [create_type_var loc]) in
@@ -239,7 +259,7 @@ let add_local_top env x tyv =
   { env with locals = Mstr.add x tyv env.locals }
 
 let add_local env x tyv =
-  let ty = dpurify env tyv in
+  let ty = dpurify ~logic:true tyv in
   { env with locals = Mstr.add x tyv env.locals;
              denv = add_pure_var x ty env }
 
@@ -256,7 +276,7 @@ and dtype_c env c =
   { dc_result_type = ty;
     dc_effect      = deffect env c.Pgm_ptree.pc_effect;
     dc_pre         = dfmla env.denv c.Pgm_ptree.pc_pre;
-    dc_post        = dpost env (dpurify env ty) c.Pgm_ptree.pc_post;
+    dc_post        = dpost env (dpurify ty) c.Pgm_ptree.pc_post;
   }
 
 and dbinder env ({id=x; id_loc=loc} as id, v) =
@@ -304,13 +324,13 @@ 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 env tyv
+      DElocal (x, tyv), dpurify tyv
   | Pgm_ptree.Eident p ->
       begin try
 	(* global variable *)
 	let x = Typing.string_list_of_qualid [] p in
 	let s, tyv = specialize_global loc x env.uc in
-	DEglobal (s, tyv), dpurify env tyv
+	DEglobal (s, tyv), dpurify tyv
       with Not_found ->
 	let s,tyl,ty = Typing.specialize_lsymbol p (theory_uc env.uc) in
 	let ty = match ty with
@@ -472,7 +492,7 @@ and dexpr_desc env loc = function
       e1.dexpr_desc, ty
   | Pgm_ptree.Eany c ->
       let c = dtype_c env c in
-      DEany c, dpurify env c.dc_result_type
+      DEany c, dpurify c.dc_result_type
 
 and dletrec env dl =
   (* add all functions into environment *)
@@ -565,7 +585,7 @@ and type_c gl env c =
 
 and binder gl env (x, tyv) =
   let tyv = type_v gl env tyv in
-  let v = create_vsymbol (id_user x.id x.id_loc) (purify tyv) in
+  let v = create_vsymbol (id_user x.id x.id_loc) (purify ~logic:true tyv) in
   let env = Mstr.add x.id v env in
   env, (v, tyv)
 
@@ -1305,6 +1325,19 @@ let cannot_be_generalized gl = function
   | Tpure _ | Tarrow _ ->
       false
 
+let check_type_vars ~loc vars ty =
+  let h = Htv.create 17 in
+  List.iter (fun v -> Htv.add h v ()) vars;
+  let rec check ty = match ty.ty_node with
+    | Ty.Tyvar v when not (Htv.mem h v) -> 
+	errorm ~loc "unbound type variable '%s" v.tv_name.id_string
+    | Ty.Tyvar _ ->
+	()
+    | Ty.Tyapp (_, tyl) ->
+	List.iter check tyl
+  in
+  check ty
+
 let find_module penv lmod q id = match q with
   | [] ->
       (* local module *)
@@ -1394,8 +1427,27 @@ let rec decl ~wp env penv lmod uc = function
       let uc = List.fold_left (decl ~wp env penv lmod) uc dl in
       begin try close_namespace uc import (Some id.id)
       with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
-  | Pgm_ptree.Dmutable_type _ ->
-      assert false (*TODO*)
+  | Pgm_ptree.Dmutable_type (id, args, model) ->
+      let loc = id.id_loc in
+      let id = id_user id.id loc in
+      let denv = Typing.create_denv (theory_uc uc) in
+      let args = 
+	List.map 
+	  (fun x -> tvsymbol_of_type_var (Typing.find_user_type_var x.id denv))
+	  args
+      in
+      let model = 
+	option_map 
+	  (fun ty -> let dty = Typing.dty denv ty in Denv.ty_of_dty dty)
+	  model 
+      in
+      option_iter (check_type_vars ~loc args) model;
+      let mt = create_mtsymbol id args model in
+      let uc = 
+	let d = Decl.create_ty_decl [mt.mt_abstr, Decl.Tabstract] in
+	Pgm_module.add_logic_decl d uc 
+      in
+      add_mtsymbol mt uc
 
 (*
 Local Variables:

tests/test-pgm-jcf.mlw

@@ -3,14 +3,19 @@ module P
 
   { use import programs.Prelude }
 
-  use module import pervasives.Ref 
-
-  let test () =
-    { true }
-    let r = ref 0 in
-    set r 1;
-    !r
-    { result > 0 }
+  use module import pervasives.Ref
+
+  let test (r : ref int) = 
+    { !r = 0 }
+    set r 1 
+    { !r = 1 }
+
+  mutable type t model int
+
+  let f (x : t) =
+    { x = 0 }
+    if x = 1 then ()
+    { x = 1 }
 
 end