Code extraction: extraction of record type declarations

src/mlw/compile.ml

@@ -193,29 +193,40 @@ module Translate = struct
   let its_args ts = ts.its_ts.ts_args
   let itd_name td = td.itd_its.its_ts.ts_name
 
+  let drecord_fields {itd_its = its; itd_fields = fl} =
+    List.map (fun ({rs_cty = rsc} as rs) ->
+      (List.exists (pv_equal (Opt.get rs.rs_field)) its.its_mfields),
+      rs.rs_name,
+      if rs_ghost rs then ML.tunit else ity rsc.cty_result) fl
+
   let ddata_constructs = (* point-free *)
     List.map (fun ({rs_cty = rsc} as rs) ->
-        rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
+      rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
 
   (** Question pour Jean-Christophe et Andreï :
-       est-ce que vous pouriez m'expliquer le champ itd_fields,
-       utilisé dans une déclaration de type ? *)
+       est-ce que vous pouriez m'expliquer le champ [itd_fields],
+       utilisé dans une définition de type ([its_defn]) ?
+       MIS-À-JOUR : je viens de coder l'extraction d'une définition
+         d'un type enregistrement et je comprends maintenant que che
+         champ est utilisé pour stocker les champs d'une définition de
+         type enregistrement. Je veux toujours savoir s'il y a des
+         cas particulaires d'utilisation, en particulier vis-à-vis du
+         champ [itd_constructors] *)
 
   (* type declarations/definitions *)
   let tdef itd =
     let s = itd.itd_its in
     let id = itd_name itd in
     let args = its_args s in
-    begin match s.its_def, itd.itd_constructors with
-      | None, [] ->
-         (* let args = its_args s in *)
+    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
+      | None, [], [] ->
          ML.Dtype [id, type_args args, ML.Dabstract]
-      | None, cl ->
-         (* let args = its_args s in *)
+      | None, cl, [] ->
          ML.Dtype [id, type_args args, ML.Ddata (ddata_constructs cl)]
-      | Some t, _ ->
+      | None, _, _ ->
+         ML.Dtype [id, type_args args, ML.Drecord (drecord_fields itd)]
+      | Some t, _, _ ->
          ML.Dtype [id, type_args args, ML.Dalias (ity t)]
-      (* | _ -> (\* TODO *\) assert false *)
     end
 
   (* program declarations *)
@@ -260,6 +271,6 @@ end
 
 (*
  * Local Variables:
- * compile-command: "make -C ../.."
+ * compile-command: "make -C ../.. -j3"
  * End:
  *)

src/mlw/ocaml_printer.ml

@@ -112,8 +112,8 @@ module Print = struct
     print_enode fmt e.e_node
 
   let print_type_decl fmt (id, args, tydef) =
-    let print_constr fmt (id, constrs) =
-      match constrs with
+    let print_constr fmt (id, cs_args) =
+      match cs_args with
       | [] ->
          fprintf fmt "@[<hov 4>| %a@]"
                  print_ident id (* FIXME: first letter must be uppercase
@@ -123,14 +123,21 @@ module Print = struct
                  print_ident id (* FIXME: print_uident *)
                  (print_list star (print_ty ~paren:false)) l
     in
+    let print_field fmt (is_mutable, id, ty) =
+      fprintf fmt "%s%a: %a;"
+              (if is_mutable then "mutable " else "")
+              print_ident id
+              (print_ty ~paren:false) ty
+    in
     let print_def fmt = function
       | Dabstract ->
          ()
       | Ddata csl ->
          fprintf fmt " =@\n%a" (print_list newline print_constr) csl
+      | Drecord fl ->
+         fprintf fmt " = {@\n%a@\n}" (print_list newline print_field) fl
       | Dalias ty ->
          fprintf fmt " =@ %a" (print_ty ~paren:false) ty
-      | _ -> (* TODO *) assert false
     in
     fprintf fmt "@[<hov 2>%s %a%a%a@]"
             (if true then "type" else "and") (* FIXME: mutual recursive types *)
@@ -161,3 +168,9 @@ let extract_module fmt m =
   let mdecls = Translate.module_ m in
   print_list nothing Print.print_decl fmt mdecls;
   fprintf fmt "@."
+
+(*
+ * Local Variables:
+ * compile-command: "make -C ../.. -j3"
+ * End:
+ *)

tests/test_extraction_mario.mlw

 module M
 
   use import int.Int
+  use import seq.Seq
 
-  let f (y: int) (x: int) : int
+  let function f (y: int) (x: int) : int
     requires { x >= 0 }
     ensures  { result >= 0 }
   = x
 
-  let g (x: int) : int
+  let g (ghost z: int) (x: int) : int
     requires { x > 0 }
     ensures  { result > 0 }
   = let y = x in
@@ -23,6 +24,13 @@ module M
 
   type list_int = list int
 
+  type cursor 'a = {
+    collection : list 'a;
+    index      : int;
+    mutable index2     : int;
+    ghost mutable v : seq 'a;
+  }
+
 end
 
 (*