Code extraction (wip)

Preparing for the new command line.

drivers/ocaml-no-arith.drv

@@ -43,6 +43,10 @@ theory list.List
   syntax function Cons "%1 :: %2"
 end
 
+theory list.Length
+  syntax function length "List.length %1"
+end
+
 theory list.Mem
   syntax predicate mem "List.mem %1 %2"
 end

src/mlw/compile.ml

@@ -197,9 +197,83 @@ module ML = struct
   let iter_deps_its_defn f its_d =
     Opt.iter (iter_deps_typedef f) its_d.its_def
 
+  let iter_deps_args f =
+    List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg)
+
+  let rec iter_deps_xbranch f (xs, _, e) =
+    f xs.xs_name;
+    iter_deps_expr f e
+
+  and iter_deps_pat_list f patl =
+    List.iter (iter_deps_pat f) patl
+
+  and iter_deps_pat f = function
+    | Pwild | Pident _ -> ()
+    | Papp (ls, patl) ->
+      f ls.ls_name;
+      iter_deps_pat_list f patl
+    | Ptuple patl -> iter_deps_pat_list f patl
+    | Por (p1, p2) ->
+      iter_deps_pat f p1;
+      iter_deps_pat f p2
+    | Pas (p, _) -> iter_deps_pat f p
+
+  and iter_deps_expr f e = match e.e_node with
+    | Econst _ | Evar _ | Eabsurd -> ()
+    | Eapp (rs, exprl) ->
+      f rs.rs_name; List.iter (iter_deps_expr f) exprl
+    | Efun _ -> assert false
+    | Elet (Lvar (_, e1), e2) ->
+      iter_deps_expr f e1;
+      iter_deps_expr f e2
+    | Elet (Lsym (_, ty_result, args, e1), e2) ->
+      iter_deps_ty f ty_result;
+      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
+      iter_deps_expr f e1;
+      iter_deps_expr f e2
+    | Elet ((Lrec rdef), e) ->
+      List.iter
+        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
+           f rs.rs_name; iter_deps_args f args;
+           iter_deps_expr f e; iter_deps_ty f res) rdef;
+      iter_deps_expr f e
+    | Ematch (e, branchl) ->
+      iter_deps_expr f e;
+      List.iter (fun (p, e) -> iter_deps_pat f p; iter_deps_expr f e) branchl
+    | Eif (e1, e2, e3) ->
+      iter_deps_expr f e1;
+      iter_deps_expr f e2;
+      iter_deps_expr f e3
+    | Eblock exprl ->
+      List.iter (iter_deps_expr f) exprl
+    | Ewhile (e1, e2) ->
+      iter_deps_expr f e1;
+      iter_deps_expr f e2
+    | Efor (_, _, _, _, e) ->
+      iter_deps_expr f e
+    | Eraise (xs, None) ->
+      f xs.xs_name
+    | Eraise (xs, Some e) ->
+      f xs.xs_name;
+      iter_deps_expr f e
+    | Etry (e, xbranchl) ->
+      iter_deps_expr f e;
+      List.iter (iter_deps_xbranch f) xbranchl
+    | Eassign assingl ->
+      List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
+
   let iter_deps f = function
     | Dtype its_dl ->
       List.iter (iter_deps_its_defn f) its_dl
+    | Dlet (Lsym (_rs, ty_result, args, e)) ->
+      iter_deps_ty f ty_result;
+      iter_deps_args f args;
+      iter_deps_expr f e
+    | Dlet (Lrec rdef) ->
+      List.iter
+        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
+           f rs.rs_name; iter_deps_args f args;
+           iter_deps_expr f e; iter_deps_ty f res) rdef
     | _ -> assert false (*TODO*)
 
   let mk_expr e_node e_ity e_effect =
@@ -268,15 +342,11 @@ module Translate = struct
   let type_args = (* point-free *)
     List.map (fun x -> x.tv_name)
 
-  let filter_ghost_params p def l =
-    let rec filter_ghost_params_cps l k =
-      match l with
-      | [] -> k []
-      | e :: r ->
-        filter_ghost_params_cps r
-          (fun fr -> k (if p e then (def e) :: fr else fr))
-    in
-    filter_ghost_params_cps l (fun x -> x)
+  let rec filter_ghost_params p def = function
+    | [] -> []
+    | pv :: l ->
+      if p pv then def pv :: (filter_ghost_params p def l)
+      else filter_ghost_params p def l
 
   let filter2_ghost_params p def al l =
     let rec filter2_ghost_params_cps l k =
@@ -371,10 +441,6 @@ module Translate = struct
       ML.mk_expr (ML.Eapp (rsc, args)) (ML.C cty_app) cty_app.cty_effect in
     ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C cty_app) cty_app.cty_effect
 
-  let app pvl =
-    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
-    filter_ghost_params pv_not_ghost def pvl
-
   (* function arguments *)
   let filter_params args =
     let args = List.map pvty args in
@@ -386,6 +452,21 @@ module Translate = struct
     | args -> let args = filter_params args in
       if args = [] then [ML.mk_var_unit ()] else args
 
+  let filter_params_cty p def pvl cty_args =
+    if List.length pvl <> List.length cty_args then
+      raise (Invalid_argument "Different size lists.@.");
+    let rec loop = function
+      | [], [] -> []
+      | pv :: l1, arg :: l2 ->
+        if p pv && p arg then def pv :: loop (l1, l2)
+        else loop (l1, l2)
+      | _ -> assert false
+    in loop (pvl, cty_args)
+
+  let app pvl cty_args =
+    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
+    filter_params_cty pv_not_ghost def pvl cty_args
+
   let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff =
     let i_expr, from_expr, to_expr =
       let int_ity = ML.ity_int in let eff_e = eff_empty in
@@ -480,13 +561,12 @@ module Translate = struct
       ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
     | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
       (* partial application *)
-      let pvl = app pvl in
+      let pvl = app pvl rsf.rs_cty.cty_args in
       let eapp =
         ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
       let ein  = expr info ein in
       let res  = ity cty.cty_result in
-      let args =
-        if filter_params cty.cty_args = [] then [ML.mk_var_unit ()] else [] in
+      let args = params cty.cty_args in
       let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
       ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
     | Elet (LDrec rdefl, ein) ->
@@ -512,7 +592,7 @@ module Translate = struct
       (* partial application of constructors *)
       mk_eta_expansion rs pvl cty
     | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
-      let pvl = app pvl in
+      let pvl = app pvl rs.rs_cty.cty_args in
       ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
     | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
       let args = params cty.cty_args in
@@ -527,7 +607,7 @@ module Translate = struct
       let e1 = expr info e1 in
       let pl = List.map (ebranch info) pl in
       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
-    | Eassert _ ->
+    | Eassert _ -> (* ML.mk_expr ML.Ehole ML.ity_unit eff *)
       ML.mk_unit
     | Eif (e1, e2, e3) ->
       let e1 = expr info e1 in

src/mlw/ocaml_printer.ml

@@ -125,8 +125,8 @@ module Print = struct
       print_list2 sep sep_m print1 print2 fmt (r1, r2)
     | _ -> ()
 
-  let print_rs info fmt rs =
-    fprintf fmt "%a" (print_lident info) rs.rs_name
+  let print_rs fmt rs =
+    fprintf fmt "%a" print_ident rs.rs_name
 
   (** Types *)
 
@@ -194,9 +194,9 @@ module Print = struct
     | Pwild ->
        fprintf fmt "_"
     | Pident id ->
-       print_ident fmt id
+       (print_lident info) fmt id
     | Pas (p, id) ->
-       fprintf fmt "%a as %a" (print_pat info) p print_ident id
+       fprintf fmt "%a as %a" (print_pat info) p (print_lident info) id
     | Por (p1, p2) ->
        fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
     | Ptuple pl ->
@@ -211,7 +211,7 @@ module Print = struct
         | []  -> print_papp info ls fmt pl
         | pjl ->
           fprintf fmt "@[<hov 2>{ %a}@]"
-            (print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
+            (print_list2 semi equal print_rs (print_pat info)) (pjl, pl)
 
   and print_papp info ls fmt = function
     | []  -> fprintf fmt "%a"      (print_uident info) ls.ls_name
@@ -260,21 +260,25 @@ module Print = struct
     | _, _, tl when is_rs_tuple rs ->
       fprintf fmt "@[(%a)@]"
         (print_list comma (print_expr info)) tl
-    | _, _, [] ->
-      print_ident fmt rs.rs_name
     | _,  _, [t1] when isfield ->
-      fprintf fmt "%a.%a" (print_expr info) t1 print_ident rs.rs_name
+      fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
     | _, _, tl when isconstructor () ->
       let pjl = get_record info rs in
-      if pjl = [] then
-        fprintf fmt "@[<hov 2>%a (%a)@]"
-          print_ident rs.rs_name (print_list comma (print_expr info)) tl
-      else
-        fprintf fmt "@[<hov 2>{ %a}@]"
-          (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
+      begin match pjl, tl with
+        | [], [] ->
+          (print_uident info) fmt rs.rs_name
+        | [], tl ->
+          fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
+            (print_list comma (print_expr info)) tl
+        | pjl, tl ->
+          fprintf fmt "@[<hov 2>{ %a}@]"
+            (print_list2 semi equal print_rs (print_expr info)) (pjl, tl)
+      end
+    | _, _, [] ->
+      (print_lident info) fmt rs.rs_name
     | _, _, tl ->
-      fprintf fmt "@[<hov 2>%a %a@]"
-        print_ident rs.rs_name (print_list space (print_expr ~paren:true info)) tl
+      fprintf fmt "@[<hov 2>%a %a@]" (print_lident info) rs.rs_name
+        (print_list space (print_expr ~paren:true info)) tl
 
   and print_let_def info fmt = function
     | Lvar (pv, e) ->
@@ -333,8 +337,8 @@ module Print = struct
     | Eassign al ->
       let assign fmt (rho, rs, pv) =
         fprintf fmt "%a.%a <-@ %a"
-          print_ident (pv_name rho) print_ident rs.rs_name
-          print_ident (pv_name pv) in
+          (print_lident info) (pv_name rho) (print_lident info) rs.rs_name
+          (print_lident info) (pv_name pv) in
       begin match al with
       | [] -> assert false | [a] -> assign fmt a
       | al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end
@@ -427,7 +431,7 @@ module Print = struct
                (print_list star (print_ty ~paren:false info)) 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 info) ty in
+        (print_lident info) id (print_ty ~paren:false info) ty in
     let print_def fmt = function
       | None ->
         ()
@@ -453,10 +457,10 @@ module Print = struct
       print_list_next newline (print_type_decl info) fmt dl;
       fprintf fmt "@\n"
     | Dexn (xs, None) ->
-       fprintf fmt "exception %a@\n" print_ident xs.xs_name
+       fprintf fmt "exception %a@\n" (print_uident info) xs.xs_name
     | Dexn (xs, Some t) ->
       fprintf fmt "@[<hov 2>exception %a of %a@]@\n"
-        print_ident xs.xs_name (print_ty ~paren:true info) t
+        (print_uident info) xs.xs_name (print_ty ~paren:true info) t
 end
 
 let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d =

src/tools/why3extract.ml

@@ -38,7 +38,7 @@ let opt_rec_single = ref Single
 type flat_modular = Flat | Modular
 let opt_modu_flat = ref Flat
 
-let is_uppercase c = c = Char.uppercase c
+let is_uppercase c = c = Char.uppercase_ascii c
 
 let add_opt_file x =
   let invalid_path () = Format.eprintf "invalid path: %s@." x; exit 1 in
@@ -95,12 +95,25 @@ let () =
     Whyconf.Args.exit_with_usage option_list usage_msg
   end
 
-(* FIXME: accept --mono without -o and use to standard output *)
-let opt_output = !opt_output
-
 let opt_rec_single = !opt_rec_single
 let opt_modu_flat  = !opt_modu_flat
 
+(* FIXME: accept --mono without -o and use to standard output *)
+let opt_output = match opt_modu_flat, !opt_output with
+  | Modular, None ->
+    eprintf "Output directory (-o) is required for modular extraction.@.";
+    exit 1
+  | Modular, Some s when not (Sys.file_exists s) ->
+    eprintf "Option '-o' should be given an existing directory as argument.@.";
+    exit 1
+  | Modular, Some s when not (Sys.is_directory s) ->
+    eprintf "Option '-o' should be given a directory as argument.@.";
+    exit 1
+  | Flat, Some s when Sys.is_directory s ->
+    eprintf "Option '-o' should not be given a directory as argument.@.";
+    exit 1
+  | Modular, Some _ | Flat, None | Flat, Some _ -> !opt_output
+
 let driver_file s =
   if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
   else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
@@ -255,17 +268,20 @@ let find_decl mm id =
 
 let rec visit mm id =
   if not (Ident.Hid.mem visited id) then begin
-    let d = find_decl mm id in
-    ML.iter_deps (visit mm) d;
-    Ident.Hid.add visited id ();
-    toextract := id :: !toextract
+    try
+      let d = find_decl mm id in
+      (* Can I change these the two lines (* *) ? *)
+      Ident.Hid.add visited id (); (* *)
+      ML.iter_deps (visit mm) d;   (* *)
+      toextract := id :: !toextract
+    with Not_found -> ()
   end
 
 let visit mm id =
   if opt_rec_single = Recursive then visit mm id
   else toextract := id :: !toextract
 
-let flat_extraction target = match Opt.get target with (* FIXME *)
+let flat_extraction target = match Opt.get target with
   | File _ -> ()
   (*  let format = !opt_parser in
       read_mlw_file ?format env fname *)
@@ -284,23 +300,22 @@ let flat_extraction target = match Opt.get target with (* FIXME *)
 let () =
   try
     match opt_modu_flat with
-    | Modular ->
-      Queue.iter do_input opt_queue
+    | Modular -> Queue.iter do_input opt_queue
     | Flat ->
       Queue.iter flat_extraction opt_queue;
       let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
       let mm = Mstr.empty in
+      let cout = match opt_output with
+          | None -> stdout
+          | Some file -> open_out file in
+      let fmt = formatter_of_out_channel cout in
       let extract id =
         let pm = find_module_id mm id in
         let m = translate_module pm in
         let d = Ident.Mid.find id m.ML.mod_known in
-        let cout = match opt_output with
-          | None -> stdout
-          | Some file -> open_out file in
-        let fmt = formatter_of_out_channel cout in
-        pr pargs false pm fmt d;
-        if cout <> stdout then close_out cout in
-      List.iter extract (List.rev !toextract)
+        pr pargs ~flat:true pm fmt d in
+      List.iter extract (List.rev !toextract);
+      if cout <> stdout then close_out cout
 
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "%a@." Exn_printer.exn_printer e;