Code extraction : wip

Makefile.in

@@ -177,7 +177,7 @@ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer dri
              parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
 
 LIB_MLW = ity expr dexpr pdecl eval_match vc pmodule \
-          pinterp pdriver cprinter compile
+          pinterp pdriver cprinter compile ocaml_printer
 
 LIB_PARSER = ptree glob typing parser lexer
 

src/mlw/compile.ml

@@ -48,6 +48,7 @@
 
 open Ident
 open Ity
+open Term
 
 module ML = struct
 
@@ -79,8 +80,9 @@ module ML = struct
     | Xexit             (* Pervasives.Exit *)
 
   type expr = {
-    e_node : expr_node;
-    e_ity  : ity;
+    e_node   : expr_node;
+    e_ity    : ity;
+    e_effect : effect;
   }
 
   and expr_node =
@@ -119,6 +121,68 @@ module ML = struct
         (* TODO add return type? *)
     | Dexn  of ident * ty option
 
+  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 *)
 
 end
+
+(** Translation from Mlw to ML *)
+
+module Translate = struct
+
+  open Expr    (* Mlw expressions *)
+
+  open Pmodule (* for the type of modules *)
+  open Pdecl   (* for the type of program declarations *)
+
+  (** programs *)
+
+  let pv_name pv = pv.pv_vs.vs_name
+
+  (* 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
+    | _ -> assert false (* TODO *)
+
+  (* program declarations *)
+  let pdecl pd =
+    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}, {c_node = Capp _})) ->
+       Format.printf "LDsym Capp--> %s@." rsn.id_string;
+       []
+    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
+       Format.printf "LDsym Cpur--> %s@." rsn.id_string;
+       []
+    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
+       Format.printf "LDsym Cany--> %s@." rsn.id_string;
+       []
+    | PDlet (LDrec _) ->
+       []
+    | PDpure ->
+       []
+    | _ -> (* TODO *) assert false
+
+  (* unit module declarations *)
+  let mdecl = function
+    | Udecl pd ->
+       pdecl pd
+    | Uuse _ ->
+       []
+    | Uscope _ ->
+       []
+    | _ -> (* TODO *) assert false
+
+  (* modules *)
+  let module_ m =
+    List.concat (List.map mdecl m.mod_units)
+
+end

src/mlw/compile_ml.ml

-(********************************************************************)
-(*                                                                  *)
-(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
-(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
-(*                                                                  *)
-(*  This software is distributed under the terms of the GNU Lesser  *)
-(*  General Public License version 2.1, with the special exception  *)
-(*  on linking described in file LICENSE.                           *)
-(*                                                                  *)
-(********************************************************************)
-
-(*
-  - option to extract into a single file
-
-  - no more why3extract.cma
-    use driver preludes instead
-
-  - 2 drivers for nums and zarith
-
-  - no delcaration at all for a module -> no file produced
-    (e.g. ref.Ref)
-
-  - suggest a command line to compile the extracted code
-    (for instance in a comment)
-
-  - drivers for val now may use %1, %2, etc. (though not mandatory)
-    Capp f x y
-      "..." -> "..." x y
-      "...%1..." -> "...x..." y
-      "..(*%1*)..." -> "...(*x*)..." y
-      "..%1..%3.." -> (fun z -> "..x..z..")  (y ignored)
-
-  - extract file f.mlw into OCaml file f.ml, with sub-modules
-
-  - "use (im|ex)port" -> "open"
-    but OCaml's open is not transitive, so requires some extra work
-    to figure out all the opens
-
-  - if a WhyML module M is extracted to something that is a signature,
-    then extract "module type B_sig = ..." (as well as "module B = ...")
-
-  - use a black list in printer to avoid clash with Pervasives symbols
-    (e.g. ref, (!), etc.)
-
-*)

src/mlw/ocaml_printer.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(** Printer for extracted OCaml code *)
+
+open Compile
+open Format
+open Pmodule
+open Theory
+open Ident
+open Printer
+open Pp
+
+module Print = struct
+
+  open ML
+
+  let ocaml_keywords =
+    ["and"; "as"; "assert"; "asr"; "begin";
+     "class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
+     "exception"; "external"; "false"; "for"; "fun"; "function";
+     "functor"; "if"; "in"; "include"; "inherit"; "initializer";
+     "land"; "lazy"; "let"; "lor"; "lsl"; "lsr"; "lxor"; "match";
+     "method"; "mod"; "module"; "mutable"; "new"; "object"; "of";
+     "open"; "or"; "private"; "rec"; "sig"; "struct"; "then"; "to";
+     "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
+     "raise";]
+
+  let iprinter =
+    let isanitize = sanitizer char_to_alpha char_to_alnumus in
+    create_ident_printer ocaml_keywords ~sanitizer:isanitize
+
+  let print_ident fmt id =
+    let s = id_unique iprinter id in
+    fprintf fmt "%s" s
+
+  let print_path =
+    print_list dot pp_print_string (* point-free *)
+
+  let print_path_id fmt = function
+    | [], id -> print_ident fmt id
+    | p, id  -> fprintf fmt "%a.%a" print_path p print_ident id
+
+  let print_theory_name fmt th =
+    print_path_id fmt (th.th_path, th.th_name)
+
+  let print_module_name fmt m =
+    print_theory_name fmt m.mod_theory
+
+  let rec print_enode fmt = function
+    | Eident id ->
+       print_ident fmt id
+    | _ -> assert false (* TODO *)
+
+  let 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@]"
+               (if isrec then "let rec" else "let")
+               print_ident id
+               print_expr e;
+       fprintf fmt "@\n@\n"
+    | _ -> assert false (* TODO *)
+
+end
+
+let extract_module fmt m =
+  fprintf fmt
+    "(* This file has been generated from Why3 module %a *)@\n@\n"
+    Print.print_module_name m;
+  let mdecls = Translate.module_ m in
+  print_list nothing Print.print_decl fmt mdecls;
+  fprintf fmt "@."

src/tools/why3extract.ml

@@ -13,6 +13,8 @@ open Format
 open Why3
 open Stdlib
 open Pmodule
+(* open Compile (\* intermediate ML AST *\) *)
+open Ocaml_printer
 
 let usage_msg = sprintf
   "Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
@@ -128,14 +130,22 @@ let extract_to =
 let rec use_iter f l =
   List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
 
+let test_extract fmt m =
+  print_module fmt m;
+  fprintf fmt "@\n@\n";
+  (* Translate.module_ m *)
+  extract_module fmt m
+
 let rec do_extract_module ?fname m =
+  test_extract (Format.formatter_of_out_channel stdout) m;
   let extract_use m' =
     let fname =
       if m'.mod_theory.Theory.th_path = [] then fname else None
     in
     do_extract_module ?fname m'
   in
-  use_iter extract_use m.mod_units;
+  (* for now, do not do a recursive extraction *)
+  (* use_iter extract_use m.mod_units; *)
   extract_to ?fname m
 
 let do_global_extract (_,p,t) =