syntax for record type declarations

src/parser/parser.pre.mly

@@ -920,6 +920,28 @@ program_decl:
     { Dmodel_type (false, $3, $4, $5) }
 | MUTABLE TYPE lident type_args model
     { Dmodel_type (true, $3, $4, $5) }
+| TYPE lident labels type_args EQUAL 
+  LEFTBRC list1_field_decl opt_semicolon RIGHTBRC
+    { Drecord_type (add_lab $2 $3, $4, $7) }
+;
+
+list1_field_decl:
+| field_decl                            { [$1] }
+| list1_field_decl SEMICOLON field_decl { $3 :: $1 }
+;
+
+field_decl:
+| opt_mutable ident COLON pure_type { $1, $2, $4 }
+;
+
+opt_mutable:
+| /* epsilon */ { false }
+| MUTABLE       { true  }
+;
+
+opt_semicolon:
+| /* epsilon */ {}
+| SEMICOLON     {}
 ;
 
 use_module:

src/parser/ptree.ml

@@ -221,6 +221,8 @@ and expr_desc =
 
 and triple = pre * expr * post
 
+type is_mutable = bool
+
 type program_decl =
   | Dlet    of ident * expr
   | Dletrec of (ident * binder list * variant option * triple) list
@@ -230,7 +232,8 @@ type program_decl =
   (* modules *)
   | Duse    of qualid * imp_exp * (*as:*) ident option
   | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
-  | Dmodel_type of bool * ident * ident list * pty option
+  | Dmodel_type of is_mutable * ident * ident list * pty option
+  | Drecord_type of ident * ident list * (is_mutable * ident * pty) list
 
 type module_ = {
   mod_name   : ident;

src/programs/pgm_module.ml

@@ -13,6 +13,7 @@ type namespace = {
   ns_pr : psymbol   Mnm.t;  (* program symbols *)
   ns_ex : esymbol   Mnm.t;  (* exceptions*)
   ns_mt : mtsymbol  Mnm.t;  (* mutable types *)
+  ns_rt : rtsymbol  Mnm.t;  (* record types *)
   ns_ns : namespace Mnm.t;  (* inner namespaces *)
 }
 
@@ -20,6 +21,7 @@ let empty_ns = {
   ns_pr = Mnm.empty;
   ns_ex = Mnm.empty;
   ns_mt = Mnm.empty;
+  ns_rt = Mnm.empty;
   ns_ns = Mnm.empty;
 }
 
@@ -38,6 +40,7 @@ let rec merge_ns chk ns1 ns2 =
   { ns_pr = ns_union p_equal  chk ns1.ns_pr ns2.ns_pr;
     ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
     ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
+    ns_rt = ns_union rt_equal chk ns1.ns_rt ns2.ns_rt;
     ns_ns = Mnm.union fusion      ns1.ns_ns ns2.ns_ns; }
 
 let nm_add chk x ns m = Mnm.change x (function
@@ -51,10 +54,12 @@ let ns_add eq chk x v m = Mnm.change x (function
 let pr_add = ns_add p_equal
 let ex_add = ns_add ls_equal
 let mt_add = ns_add mt_equal
+let rt_add = ns_add rt_equal
 
 let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
 let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
 let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
+let add_rt chk x rt ns = { ns with ns_rt = rt_add chk x rt ns.ns_rt }
 let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
 
 let rec ns_find get_map ns = function
@@ -65,6 +70,7 @@ let rec ns_find get_map ns = function
 let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
 let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
 let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
+let ns_find_rt = ns_find (fun ns -> ns.ns_rt)
 let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
 
 (* modules under construction *)
@@ -138,6 +144,14 @@ let add_mtsymbol mt uc =
   in
   add_symbol add_mt mt.mt_name mt uc
 
+let add_rtsymbol rt uc =
+  (* added in the logic as an abstract type *)
+  let uc = 
+    let d = Decl.create_ty_decl [rt.rt_abstr, Decl.Tabstract] in
+    add_logic_decl d uc 
+  in
+  add_symbol add_rt rt.rt_name rt uc
+
 let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)
 
 let create_module n =

src/programs/pgm_module.mli

@@ -10,6 +10,7 @@ type namespace = private {
   ns_pr : psymbol   Mnm.t;  (* program symbols *)
   ns_ex : esymbol   Mnm.t;  (* exception symbols *)
   ns_mt : mtsymbol  Mnm.t;  (* mutable types *)
+  ns_rt : rtsymbol  Mnm.t;  (* record types *)
   ns_ns : namespace Mnm.t;  (* inner namespaces *)
 }
 
@@ -48,6 +49,7 @@ exception ClashSymbol of string
 val add_psymbol : psymbol -> uc -> uc
 val add_esymbol : esymbol -> uc -> uc
 val add_mtsymbol : mtsymbol -> uc -> uc
+val add_rtsymbol : rtsymbol -> uc -> uc
 val add_decl : Pgm_ttree.decl -> uc -> uc
 val add_logic_decl : Decl.decl -> uc -> uc
 

src/programs/pgm_types.ml

@@ -7,7 +7,7 @@ open Theory
 open Term
 open Decl
 
-(* model types *)
+(* model type symbols *)
 
 type mtsymbol = {
   mt_name   : ident;
@@ -46,6 +46,59 @@ exception NotModelType
 let get_mtsymbol ts = 
   try Hts.find model_types ts with Not_found -> raise NotModelType
 
+(* record type symbols ***************************************************)
+
+type rt_field = {
+  rf_name   : ident;
+  rf_region : tvsymbol option;
+  rf_type   : ty;
+}
+
+type rtsymbol = {
+  rt_name  : ident;
+  rt_args  : tvsymbol list;
+  rt_abstr : tysymbol;
+  rt_fields: rt_field Mstr.t; 
+}
+
+let record_types = Hts.create 17
+
+let create_rtsymbol name args fields = 
+  let id = id_register name in
+  let args = ref args in
+  let m = 
+    List.fold_left
+      (fun m (mut, id, ty) -> 
+	 let id = id_register id in
+	 if mut then begin
+	   let tv = create_tvsymbol (id_fresh "r") in
+	   args := tv :: !args; 
+	   Mstr.add id.id_string (id, Some tv, ty) m
+	 end else
+	   Mstr.add id.id_string (id, None, ty) m)
+      Mstr.empty fields
+  in
+  let ts = create_tysymbol name !args None in
+  let create_field (id, reg, ty) = 
+    { rf_name   = id;
+      rf_region = reg;
+      rf_type   = ty;
+    }
+  in
+  let m = Mstr.map create_field m in
+  let rt = 
+    { rt_name   = id;
+      rt_args   = !args;
+      rt_abstr  = ts;
+      rt_fields = m; }
+  in
+  Hts.add record_types ts rt;
+  rt
+
+let rt_equal : rtsymbol -> rtsymbol -> bool = (==)
+
+(* model type *************************************************************)
+
 let rec model_type ty = match ty.ty_node with
   | Tyapp (ts, tyl) ->
       let tyl = List.map model_type tyl in
@@ -65,7 +118,7 @@ let rec model_type ty = match ty.ty_node with
   | Tyvar _ ->
       ty
 
-(* types *)
+(* builtin logic symbols ************************************************)
 
 let ts_exn = Ty.create_tysymbol (id_fresh "exn") [] None
 let ty_exn = Ty.ty_app ts_exn []

src/programs/pgm_types.mli

@@ -30,6 +30,28 @@ val get_mtsymbol : tysymbol -> mtsymbol
 val is_mutable_ts : tysymbol -> bool
 val is_mutable_ty : ty       -> bool
 
+(* record type symbols *)
+
+type rt_field = private {
+  rf_name   : ident;
+  rf_region : tvsymbol option;
+  rf_type   : ty;
+}
+
+type rtsymbol = private {
+  rt_name   : ident;
+  rt_args   : tvsymbol list;
+  rt_abstr  : tysymbol;
+  rt_fields : rt_field Mstr.t; 
+}
+
+val create_rtsymbol : 
+  preid -> tvsymbol list -> (bool * preid * ty) list -> rtsymbol
+
+val rt_equal : rtsymbol -> rtsymbol -> bool
+
+(* builtin logic symbols for programs *)
+
 val ts_arrow : tysymbol
 val make_arrow_type : ty list -> ty -> ty
 
@@ -39,6 +61,7 @@ val ty_exn : ty
 (* val ts_label : tysymbol *)
 
 (* program types *)
+
 module rec T : sig
 
   type pre = Term.fmla

src/programs/pgm_typing.ml

@@ -1656,11 +1656,23 @@ let rec decl ~wp env penv ltm lmod uc = function
       in
       option_iter (check_type_vars ~loc args) model;
       let mt = create_mtsymbol ~mut 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
+  | Ptree.Drecord_type (id, args, fl) ->
+      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 field (m, id, ty) = 
+	let ty = let dty = Typing.dty denv ty in Denv.ty_of_dty dty in
+	m, id_user id.id id.id_loc, ty
+      in
+      let fields = List.map field fl in
+      let rt = create_rtsymbol id args fields in
+      add_rtsymbol rt uc
 
 (*
 Local Variables:

tests/test-pgm-jcf.mlw

 module P
 
   use import int.Int
-  use import module stdlib.Ref
-  use import module stdlib.Array
 
-  abstract type t 'a model 'a
-  parameter t : x:'a -> {} t 'a { result=x }
-
-  let f () = {} (1, t 2) { true }
-
-  parameter c : ghost int
-
-  axiom a : c = 1
-
-  let gid (x:int) = {} ghost (c + x) { result=c+x }
-
-  let foo (x:int) = {} (x, ghost x) { let a,b = result in a=x and b=x }
-
-  (* FIXME : make c a first parameter of gid => then to type gid c y inside
-     ghost we should not insert unghost *)
-
-  let g (x : int) (y : ghost int) =
-    let z = ghost (1 + gid y) in
-    assert { z = 2 + y };
-    x + 1
+  type t 'a = { a : int; mutable b : int; }
 
 end