Code extraction : wip

src/mlw/compile.ml

@@ -48,6 +48,7 @@
 
 open Ident
 open Ity
+open Ty
 open Term
 
 module ML = struct
@@ -124,7 +125,11 @@ module ML = struct
   let create_expr e_node e_ity e_effect =
     { e_node = e_node; e_ity = e_ity; e_effect = e_effect }
 
-(* TODO add here some smart constructors for ML expressions *)
+  (* TODO add here some smart constructors for ML expressions *)
+  let ml_let id e1 e2 =
+    Elet (id, e1, e2)
+
+  let tunit = Ttuple []
 
 end
 
@@ -137,16 +142,40 @@ module Translate = struct
   open Pmodule (* for the type of modules *)
   open Pdecl   (* for the type of program declarations *)
 
+  (* types *)
+  let rec type_ ty =
+    match ty.ty_node with
+    | Tyvar tvs ->
+       ML.Tvar tvs.tv_name
+    | Tyapp (ts, tyl) when is_ts_tuple ts ->
+       ML.Ttuple (List.map type_ tyl)
+    | Tyapp (ts, tyl) ->
+       ML.Tapp (ts.ts_name, List.map type_ tyl)
+
+  let vsty vs =
+    vs.vs_name, type_ vs.vs_ty
+
   (** programs *)
 
   let pv_name pv = pv.pv_vs.vs_name
 
+  let pvty pv =
+    if pv.pv_ghost then (pv_name pv, ML.tunit)
+    else vsty pv.pv_vs
+
+  (* function arguments *)
+  let args = (* point-free *)
+    List.map pvty
+
   (* expressions *)
   let rec expr e =
     match e.e_node with
     | Evar pvs ->
        let pv_id = pv_name pvs in
        ML.create_expr (ML.Eident pv_id) e.e_ity e.e_effect
+    | Elet (LDvar (pvs, e1), e2) ->
+       let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
+       ML.create_expr ml_let e.e_ity e.e_effect
     | _ -> assert false (* TODO *)
 
   (* program declarations *)
@@ -154,8 +183,8 @@ module Translate = struct
     match pd.pd_node with
     | PDlet (LDvar (_, _)) ->
        []
-    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cfun e})) ->
-       [ML.Dlet (false, [rsn, [], expr e])]
+    | PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
+       [ML.Dlet (false, [rsn, args cty.cty_args, expr e])]
     | PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
        Format.printf "LDsym Capp--> %s@." rsn.id_string;
        []
@@ -186,3 +215,9 @@ module Translate = struct
     List.concat (List.map mdecl m.mod_units)
 
 end
+
+(*
+ * Local Variables:
+ * compile-command: "make -C ../.."
+ * End:
+ *)

src/mlw/ocaml_printer.ml

@@ -34,14 +34,57 @@ module Print = struct
      "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
      "raise";]
 
-  let iprinter =
+  let iprinter, aprinter =
     let isanitize = sanitizer char_to_alpha char_to_alnumus in
-    create_ident_printer ocaml_keywords ~sanitizer:isanitize
+    let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
+    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
+    create_ident_printer ocaml_keywords ~sanitizer:lsanitize
 
   let print_ident fmt id =
     let s = id_unique iprinter id in
     fprintf fmt "%s" s
 
+  (* let print_lident = print_qident ~sanitizer:Strings.uncapitalize *)
+  (* let print_uident = print_qident ~sanitizer:Strings.capitalize *)
+
+  let print_tv fmt tv =
+    fprintf fmt "'%s" (id_unique aprinter tv)
+
+  let star fmt () = fprintf fmt " *@ "
+
+  let rec print_ty fmt = function
+    | Tvar id ->
+       print_tv fmt id
+    | Ttuple [] ->
+       fprintf fmt "unit"
+    | Ttuple tl ->
+       fprintf fmt "%a" (print_list star print_ty) tl
+    | Tapp (ts, []) ->
+       print_ident fmt ts
+    | Tapp (ts, [ty]) ->
+       fprintf fmt "%a@ %a" print_ty ty print_ident ts
+    | Tapp (ts, tl) ->
+       fprintf fmt "(%a)@ %a"
+               (print_list comma print_ty) tl
+               print_ident ts
+
+  let print_vsty fmt (v, ty) =
+    fprintf fmt "%a:@ %a" print_ident v print_ty ty
+
+  let print_vs_arg fmt vs =
+    fprintf fmt "@[(%a)@]" print_vsty vs
+
+  let rec print_ty fmt = function
+    | Tvar id ->
+       print_tv fmt id
+    | Ttuple [] ->
+       fprintf fmt "unit"
+    | Ttuple tl ->
+       fprintf fmt "%a" (print_list star print_ty) tl
+    | Tapp (ts, []) ->
+       print_ident fmt ts
+    | _ -> assert false (* TODO *)
+
   let print_path =
     print_list dot pp_print_string (* point-free *)
 
@@ -58,16 +101,22 @@ module Print = struct
   let rec print_enode fmt = function
     | Eident id ->
        print_ident fmt id
+    | Elet (id, e1, e2) ->
+       fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
+               print_ident id
+               print_expr e1
+               print_expr e2
     | _ -> assert false (* TODO *)
 
-  let print_expr fmt e =
+  and print_expr fmt e =
     print_enode fmt e.e_node
 
   let print_decl fmt = function
-    | Dlet (isrec, [id, _, e]) ->
-       fprintf fmt "@[<hov 2>%s %a =@ %a@]"
+    | Dlet (isrec, [id, vl, e]) ->
+       fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
                (if isrec then "let rec" else "let")
                print_ident id
+               (print_list space print_vs_arg) vl
                print_expr e;
        fprintf fmt "@\n@\n"
     | _ -> assert false (* TODO *)

tests/test_extraction_mario.mlw

+module M
+
+  use import int.Int
+
+  let f (y: int) (x: int) : int
+    requires { x >= 0 }
+    ensures  { result >= 0 }
+  = x
+
+  let g (x: int) : int
+    requires { x > 0 }
+    ensures  { result > 0 }
+  = let y = x in
+    y
+
+end
+
+(*
+ * Local Variables:
+ * compile-command: "../bin/why3extract -D ../drivers/c.drv -o extract test_extraction_mario.mlw"
+ * End:
+ *)
\ No newline at end of file