Commit 1c9adfcf authored by MARCHE Claude's avatar MARCHE Claude

extraction: finished the common part

Dummy C printer added
parent 588d33ed
......@@ -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
pinterp pdriver cprinter
LIB_PARSER = ptree glob typing parser lexer
......
printer "c"
let fg ?fname m =
let n = m.Pmodule.mod_theory.Theory.th_name.Ident.id_string in
match fname with
| None -> n ^ ".c"
| Some f -> f ^ "__" ^ n ^ ".c"
open Format
let pr args ?old fmt m =
ignore(args);
ignore(old);
ignore(m);
fprintf fmt "#include <stdio.h>\n\
\n\
int main() {\n\
printf \"Extraction from WhyML to C not yet implemented\\n\";\n\
return 1;\n\
}\n\
"
let () = Pdriver.register_printer "c" ~desc:"printer for C code" fg pr
......@@ -218,9 +218,11 @@ let load_driver env file extra_files =
open Stdlib
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type printer = printer_args -> ?old:in_channel -> Pmodule.pmodule Pp.pp
type reg_printer = Pp.formatted * printer
type reg_printer = Pp.formatted * filename_generator * printer
let printers : reg_printer Hstr.t = Hstr.create 17
......@@ -228,18 +230,11 @@ exception KnownPrinter of string
exception UnknownPrinter of string
exception NoPrinter
let register_printer ~desc s p =
let register_printer ~desc s fg p =
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s (desc, p)
let lookup_printer s =
try snd (Hstr.find printers s)
with Not_found -> raise (UnknownPrinter s)
let list_printers () =
Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) printers []
Hstr.replace printers s (desc, fg, p)
let extract_module ?old drv fmt m =
let lookup_printer drv =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
......@@ -251,10 +246,20 @@ let extract_module ?old drv fmt m =
blacklist = drv.drv_blacklist;
syntax = drv.drv_syntax;
converter = drv.drv_converter;
} in
}
in
try
let (_,fg,p) = Hstr.find printers p in (fg,printer_args,p)
with Not_found -> raise (UnknownPrinter p)
let list_printers () =
Hstr.fold (fun k (desc,_,_) acc -> (k,desc)::acc) printers []
(*
let extract_module ?old drv fmt m =
let printer = lookup_printer p printer_args in
Format.fprintf fmt "@[%a@]@?" (printer ?old) m
*)
(* exception report *)
......
......@@ -39,11 +39,15 @@ val load_driver : Env.env -> string -> string list -> driver
type printer = printer_args -> ?old:in_channel -> Pmodule.pmodule Pp.pp
val register_printer : desc:Pp.formatted -> string -> printer -> unit
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
val lookup_printer : string -> printer
val register_printer : desc:Pp.formatted -> string -> filename_generator -> printer -> unit
val lookup_printer : driver -> filename_generator * printer_args * printer
val list_printers : unit -> (string * Pp.formatted) list
(*
val extract_module : ?old:in_channel ->
driver -> Format.formatter -> Pmodule.pmodule -> unit
*)
......@@ -12,7 +12,7 @@
open Format
open Why3
open Stdlib
open Theory
open Pmodule
let usage_msg = sprintf
"Usage: %s [options] -D <driver> -o <dir> [[file|-] [-T <theory>]...]..."
......@@ -27,6 +27,7 @@ let add_opt_file x =
Queue.push (Some x, tlist) opt_queue;
opt_input := Some tlist
(* TODO : rename theory into module, -T into -M *)
let add_opt_theory x =
let l = Strings.split '.' x in
let p, t = match List.rev l with
......@@ -99,8 +100,9 @@ let opt_driver =
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let extract_to ?fname:string m =
let file = Filename.concat opt_output (assert false (*Mlw_ocaml.extract_filename ?fname th *)) in
let extract_to ?fname m =
let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
let file = Filename.concat opt_output (fg ?fname m) in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
......@@ -109,41 +111,36 @@ let extract_to ?fname:string m =
end else None in
let cout = open_out file in
let fmt = formatter_of_out_channel cout in
let tname = m.Pmodule.mod_theory.th_name.Ident.id_string in
let tname = m.mod_theory.Theory.th_name.Ident.id_string in
Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
Pdriver.extract_module ?old opt_driver fmt m;
pr ?old pargs fmt m;
close_out cout
let extract_to =
let visited = Ident.Hid.create 17 in
fun ?fname m ->
let name = m.Pmodule.mod_theory.Theory.th_name in
let name = m.mod_theory.Theory.th_name in
if not (Ident.Hid.mem visited name) then begin
Ident.Hid.add visited name ();
extract_to ?fname m
end
let use_iter f th =
List.iter (fun d -> match d.td_node with Use t -> f t | _ -> ()) th.th_decls
let rec use_iter f l =
List.iter (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
let (* rec *) do_extract_module ?fname m =
extract_to ?fname m;
assert false
(* TODO: extract also used modules ? Or let each extraction function decide what "used" parts should be extracted ?
let extract_use th' =
let fname = if th'.th_path = [] then fname else None in
match
try Some (Mlw_module.restore_module th') with Not_found -> None
with
| Some m' -> do_extract_module ?fname m'
| None -> do_extract_theory ?fname th' in
use_iter extract_use m.Mlw_module.mod_theory
*)
let rec do_extract_module ?fname 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;
extract_to ?fname m
let do_global_extract (_,p,t) =
let env = opt_driver.Pdriver.drv_env in
let m = Pmodule.read_module env p t in
let m = read_module env p t in
do_extract_module m
......@@ -158,7 +155,7 @@ let do_local_extract fname cin tlist =
let env = opt_driver.Pdriver.drv_env in
let format = !opt_parser in
let mm =
Env.read_channel ?format Pmodule.mlw_language env fname cin in
Env.read_channel ?format mlw_language env fname cin in
if Queue.is_empty tlist then
let do_m _ m = do_extract_module ~fname m in
Mstr.iter do_m mm
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment