Extraction: new compile.mli file

Makefile.in

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

src/mlw/ocaml_printer.ml

@@ -38,7 +38,8 @@ type info = {
 
 module Print = struct
 
-  open ML
+  open Mltree
+  open Compile.ML
 
   let ocaml_keywords =
     ["and"; "as"; "assert"; "asr"; "begin";

src/mlw/pdriver.ml

@@ -224,7 +224,7 @@ type filename_generator = ?fname:string -> Pmodule.pmodule -> string
 
 type printer =
   printer_args -> ?old:in_channel -> ?fname:string -> flat:bool ->
-  Pmodule.pmodule -> Compile.ML.decl Pp.pp
+  Pmodule.pmodule -> Mltree.decl Pp.pp
 
 type reg_printer = Pp.formatted * filename_generator * printer
 

src/mlw/pdriver.mli

@@ -39,7 +39,7 @@ val load_driver : Env.env -> string -> string list -> driver
 
 type printer =
   printer_args -> ?old:in_channel -> ?fname:string -> flat:bool ->
-  Pmodule.pmodule -> Compile.ML.decl Pp.pp
+  Pmodule.pmodule -> Mltree.decl Pp.pp
 
 type filename_generator = ?fname:string -> Pmodule.pmodule -> string
 

src/tools/why3extract.ml

@@ -183,7 +183,7 @@ let extract_to =
         if not (Ident.Hid.mem memo name) then begin
           Ident.Hid.add memo name ();
           let mdecls = match decl with
-            | None   -> (translate_module m).ML.mod_decl
+            | None   -> (translate_module m).Mltree.mod_decl
             | Some d -> Translate.pdecl_m m d in
           print_mdecls ?fname m mdecls
         end
@@ -271,7 +271,7 @@ let toextract = ref []
 let find_decl mm id =
   let m = find_module_id mm id in
   let m = translate_module m in
-  Ident.Mid.find id m.ML.mod_known
+  Ident.Mid.find id m.Mltree.mod_known
 
 let rec visit mm id =
   if not (Ident.Hid.mem visited id) then begin
@@ -301,7 +301,7 @@ let flat_extraction mm = function
   | Module (path, m) ->
     let m = find_module_path mm path m in (* FIXME: catch Not_found here *)
     let m = translate_module m in
-    Ident.Mid.iter (fun id _ -> visit mm id) m.ML.mod_known;
+    Ident.Mid.iter (fun id _ -> visit mm id) m.Mltree.mod_known;
     mm
   | Symbol (path, m, s) ->
     let m = find_module_path mm path m in
@@ -318,7 +318,7 @@ let () =
     | Flat ->
       let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
       let visit_m _ m = let tm = translate_module m in
-        Ident.Mid.iter (fun id _ -> visit mm id) tm.ML.mod_known in
+        Ident.Mid.iter (fun id _ -> visit mm id) tm.Mltree.mod_known in
       Mstr.iter visit_m mm;
       let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
       let cout = match opt_output with
@@ -332,7 +332,7 @@ let () =
       let extract fmt 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 d = Ident.Mid.find id m.Mltree.mod_known in
         pr pargs ~flat:true pm fmt d in
       List.iter (extract fmt) (List.rev !toextract);
       if cout <> stdout then close_out cout