extraction drivers

parent c8fc11e7
......@@ -395,7 +395,7 @@ clean::
########
MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_dtree mlw_dty mlw_typing mlw_ocaml mlw_main
mlw_dtree mlw_dty mlw_typing mlw_driver mlw_ocaml mlw_main
MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
......
......@@ -65,3 +65,15 @@ theory int.ComputerDivision
syntax function mod "(Num.mod_num %1 %2)"
end
(* WhyML *)
(*
module ref.Ref
syntax type ref "(%1 Pervasives.ref)"
syntax function contents "(%1).Pervasives.contents"
syntax val ref "(Pervasives.ref %1)"
syntax val (!) "(%1).Pervasives.contents"
syntax val (:=) "((%1) := (%2))"
end
*)
......@@ -115,7 +115,7 @@ let check_syntax s len =
in
iter_group regexp_arg_pos arg s
let check_syntax_typed ls s =
let check_syntax_logic ls s =
let len = List.length ls.ls_args in
let ret = ls.ls_value <> None in
let nfv = Stv.cardinal (ls_ty_freevars ls) in
......@@ -227,12 +227,14 @@ let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
let meta_realized = register_meta "realized" [MTstring; MTstring]
~desc:"TODO??"
let check_syntax_type ts s = check_syntax s (List.length ts.ts_args)
let syntax_type ts s =
check_syntax s (List.length ts.ts_args);
check_syntax_type ts s;
create_meta meta_syntax_type [MAts ts; MAstr s]
let syntax_logic ls s =
check_syntax_typed ls s;
check_syntax_logic ls s;
create_meta meta_syntax_logic [MAls ls; MAstr s]
let remove_prop pr =
......
......@@ -60,6 +60,9 @@ val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
val remove_prop : prsymbol -> tdecl
val check_syntax_type: tysymbol -> string -> unit
val check_syntax_logic: lsymbol -> string -> unit
type syntax_map = string Mid.t
(* [syntax_map] maps the idents of removed props to "" *)
......
......@@ -26,7 +26,7 @@ type driver
val load_driver : Env.env -> string -> string list -> driver
(** loads a driver from a file
@param env TODO
@param env environment to interpret theories
@param string driver file name
@param string list additional driver files containing only theories
*)
......
......@@ -81,8 +81,13 @@ type file = {
f_rules : theory_rules list;
}
type global_extract =
| EPrelude of string
| EPrinter of string
| EBlacklist of string list
type file_extract = {
fe_global : (loc * global) list;
fe_global : (loc * global_extract) list;
fe_th_rules : theory_rules list;
fe_mo_rules : module_rules list;
}
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val parse_file:
(string -> Lexing.lexbuf) -> Lexing.lexbuf -> Driver_ast.file
val parse_file_extract:
(string -> Lexing.lexbuf) -> Lexing.lexbuf -> Driver_ast.file_extract
......@@ -119,7 +119,7 @@ rule token = parse
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
let parse_file input_lexbuf lexbuf =
let parse_file_gen parse input_lexbuf lexbuf =
let s = Stack.create () in
Stack.push lexbuf s;
let rec multifile lex_dumb =
......@@ -137,5 +137,8 @@ rule token = parse
| _ -> tok in
let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
Loc.transfer_loc lexbuf lex_dumb;
with_location (Driver_parser.file multifile) lex_dumb
with_location (parse multifile) lex_dumb
let parse_file = parse_file_gen Driver_parser.file
let parse_file_extract = parse_file_gen Driver_parser.file_extract
}
......@@ -180,7 +180,7 @@ file_extract:
list0_global_theory_module:
| /* epsilon */ { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
| global list0_global_theory_module
| global_extract list0_global_theory_module
{ {$2 with fe_global = (loc_i 1, $1) :: ($2.fe_global)} }
| theory list0_global_theory_module
{ {$2 with fe_th_rules = $1 :: ($2.fe_th_rules)} }
......@@ -188,6 +188,12 @@ list0_global_theory_module:
{ {$2 with fe_mo_rules = $1 :: ($2.fe_mo_rules)} }
;
global_extract:
| PRELUDE STRING { EPrelude $2 }
| PRINTER STRING { EPrinter $2 }
| BLACKLIST list1_string_list { EBlacklist $2 }
;
module_:
| MODULE tqualid list0_mrule END
{ { mor_name = $2; mor_rules = $3 } }
......
......@@ -103,7 +103,7 @@ let opt_memlimit = ref None
let opt_command = ref None
let opt_task = ref None
let opt_realize = ref false
let opt_extract = ref false
let opt_extract = ref None
let opt_bisect = ref false
let opt_print_libdir = ref false
......@@ -179,9 +179,9 @@ let option_list = Arg.align [
" same as -o";
"--realize", Arg.Set opt_realize,
" Realize selected theories from the library";
"-E", Arg.Set opt_extract,
" Generate OCaml code for selected theories/modules from the library";
"--extract", Arg.Set opt_extract,
"-E", Arg.String (fun s -> opt_extract := Some s),
"<driver> Generate code for selected theories/modules";
"--extract", Arg.String (fun s -> opt_extract := Some s),
" same as -E";
"--bisect", Arg.Set opt_bisect,
" Reduce the set of needed axioms which prove a goal, \
......@@ -306,7 +306,7 @@ let () = try
end;
if !opt_output <> None
&& !opt_driver = None && !opt_prover = None && not !opt_extract then begin
&& !opt_driver = None && !opt_prover = None && !opt_extract = None then begin
eprintf
"Option '-o'/'--output' requires a prover, a driver, or option '-E'.@.";
exit 1
......@@ -329,7 +329,7 @@ let () = try
opt_print_theory := true
end;
if !opt_extract && !opt_output = None then begin
if !opt_extract <> None && !opt_output = None then begin
eprintf
"Option '-E'/'--extract' require a directory to output the result.@.";
exit 1
......@@ -534,34 +534,35 @@ let extract_to ?fname th extract =
extract file ?old (formatter_of_out_channel cout);
close_out cout
let do_extract_theory env ?fname tname th =
let do_extract_theory edrv ?fname tname th =
let extract file ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
Mlw_ocaml.extract_theory env ?old ?fname fmt th
Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
in
extract_to ?fname th extract
let do_extract_module env ?fname tname m =
let do_extract_module edrv ?fname tname m =
let extract file ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
Mlw_ocaml.extract_module env ?old ?fname fmt m
Mlw_ocaml.extract_module edrv ?old ?fname fmt m
in
extract_to ?fname m.Mlw_module.mod_theory extract
let do_global_extract env (tname,p,t,_) =
let do_global_extract edrv (tname,p,t,_) =
let lib = edrv.Mlw_driver.drv_lib in
try
let lib = Mlw_main.library_of_env env in
let mm, thm = Env.read_lib_file lib p in
try
let m = Mstr.find t mm in
do_extract_module env tname m
do_extract_module edrv tname m
with Not_found ->
let th = Mstr.find t thm in
do_extract_theory env tname th
do_extract_theory edrv tname th
with Env.LibFileNotFound _ | Not_found -> try
let format = Util.def_option "why" !opt_parser in
let env = Env.env_of_library lib in
let th = Env.read_theory ~format env p t in
do_extract_theory env tname th
do_extract_theory edrv tname th
with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
eprintf "Theory/module '%s' not found.@." tname;
exit 1
......@@ -582,35 +583,36 @@ let do_extract_module_from env fname mm thm (tname,_,t,_) =
eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
exit 1
let do_local_extract env fname cin tlist =
let do_local_extract edrv fname cin tlist =
let lib = edrv.Mlw_driver.drv_lib in
if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then begin
let lib = Mlw_main.library_of_env env in
let mm, thm = Mlw_main.read_channel lib [] fname cin in
if Queue.is_empty tlist then begin
let do_m t m thm =
do_extract_module env ~fname t m; Mstr.remove t thm in
do_extract_module edrv ~fname t m; Mstr.remove t thm in
let thm = Mstr.fold do_m mm thm in
Mstr.iter (fun t th -> do_extract_theory env ~fname t th) thm
Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
end else
Queue.iter (do_extract_module_from env fname mm thm) tlist
Queue.iter (do_extract_module_from edrv fname mm thm) tlist
end else begin
let env = Env.env_of_library lib in
let m = Env.read_channel ?format:!opt_parser env fname cin in
if Queue.is_empty tlist then
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_extract_theory env ~fname t th in
let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_extract_theory_from env fname m) tlist
Queue.iter (do_extract_theory_from edrv fname m) tlist
end
let total_annot_tokens = ref 0
let total_program_tokens = ref 0
let do_input env drv = function
let do_input env drv edrv = function
| None, _ when !opt_parse_only || !opt_type_only ->
()
| None, tlist when !opt_extract ->
Queue.iter (do_global_extract env) tlist
| None, tlist when edrv <> None ->
Queue.iter (do_global_extract (Util.of_option edrv)) tlist
| None, tlist ->
Queue.iter (do_global_theory env drv) tlist
| Some f, tlist ->
......@@ -632,8 +634,8 @@ let do_input env drv = function
Format.printf "File %s: %d tokens in annotations@." f a;
Format.printf "File %s: %d tokens in programs@." f p
end
end else if !opt_extract then begin
do_local_extract env fname cin tlist;
end else if edrv <> None then begin
do_local_extract (Util.of_option edrv) fname cin tlist;
close_in cin
end else begin
let m = Env.read_channel ?format:!opt_parser env fname cin in
......@@ -650,12 +652,27 @@ let do_input env drv = function
Queue.iter (do_local_theory env drv fname m) tlist
end
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"))
let load_driver env (s,ef) =
let file = driver_file s in
load_driver env file ef
let load_driver_extract env s =
let file = driver_file s in
let lib = Mlw_main.library_of_env env in
Mlw_driver.load_driver lib file []
let () =
try
let env = Env.create_env !opt_loadpath in
let drv =
Util.option_map (fun (f,ef) -> load_driver env f ef) !opt_driver in
Queue.iter (do_input env drv) opt_queue;
let drv = Util.option_map (load_driver env) !opt_driver in
let edrv = Util.option_map (load_driver_extract env) !opt_extract in
Queue.iter (do_input env drv edrv) opt_queue;
if !opt_token_count then
Format.printf "Total: %d annot/%d programs, ratio = %.3f@."
!total_annot_tokens !total_program_tokens
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Util
open Ident
open Ty
open Term
open Decl
open Theory
open Task
open Printer
open Trans
open Driver_ast
open Call_provers
type driver = {
drv_lib : Mlw_typing.mlw_library;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
}
let load_file file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let to_close = Stack.create () in
Stack.push c to_close;
let input_lexer filename =
let c = open_in filename in
Stack.push c to_close;
let lb = Lexing.from_channel c in
Loc.set_file filename lb;
lb
in
let f = Driver_lexer.parse_file_extract input_lexer lb in
Stack.iter close_in to_close;
f
exception Duplicate of string
exception UnknownType of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
let load_driver lib file extra_files =
let prelude = ref [] in
let printer = ref None in
let blacklist = Queue.create () in
let set_or_raise loc r v error = match !r with
| Some _ -> raise (Loc.Located (loc, Duplicate error))
| None -> r := Some v
in
let add_to_list r v = (r := v :: !r) in
let add_global (loc, g) = match g with
| EPrelude s -> add_to_list prelude s
| EPrinter s -> set_or_raise loc printer s "printer"
| EBlacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
in
let f = load_file file in
List.iter add_global f.fe_global;
let thprelude = ref Mid.empty in
let syntax_map = ref Mid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try ns_find_pr th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
in
let find_ls th (loc,q) = try ns_find_ls th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
in
let find_ts th (loc,q) = try ns_find_ts th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
in
let find_fs th q =
let ls = find_ls th q in
if ls.ls_value = None then raise (FSymExpected ls) else ls in
let find_ps th q =
let ls = find_ls th q in
if ls.ls_value <> None then raise (PSymExpected ls) else ls in
let add_syntax id s = syntax_map := Mid.add id s !syntax_map in
let add_local th = function
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (_,q,s) ->
let ts = find_ts th q in
check_syntax_type ts s;
add_syntax ts.ts_name s
| Rsyntaxfs (_,q,s) ->
let fs = find_fs th q in
check_syntax_logic fs s;
add_syntax fs.ls_name s
| Rsyntaxps (_,q,s) ->
let ps = find_ps th q in
check_syntax_logic ps s;
add_syntax ps.ls_name s
| Rremovepr (_,q) ->
ignore (find_pr th q)
| Rmeta (_,s,al) ->
let convert = function
| PMAts q -> MAts (find_ts th q)
| PMAfs q -> MAls (find_fs th q)
| PMAps q -> MAls (find_ps th q)
| PMApr q -> MApr (find_pr th q)
| PMAstr s -> MAstr s
| PMAint i -> MAint i
in
let m = lookup_meta s in
ignore (create_meta m (List.map convert al))
in
let add_local th (loc,rule) =
try add_local th rule with e -> raise (Loc.Located (loc,e))
in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th =
try Env.read_theory ~format:"why" (Env.env_of_library lib) f id
with e -> raise (Loc.Located (loc,e))
in
qualid := q;
List.iter (add_local th) trl
in
let add_module _ =
assert false (*TODO*)
in
List.iter add_theory f.fe_th_rules;
List.iter add_module f.fe_mo_rules;
List.iter (fun f ->
let fe = load_file f in
List.iter add_theory fe.fe_th_rules;
List.iter add_module fe.fe_mo_rules)
extra_files;
{
drv_lib = lib;
drv_printer = !printer;
drv_prelude = List.rev !prelude;
drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_syntax = !syntax_map;
}
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Why3
type driver = private {
drv_lib : Mlw_typing.mlw_library;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
}
val load_driver :
Mlw_typing.mlw_library -> string -> string list -> driver
(** loads a driver from a file
@param env environment to interpret theories and modules
@param string driver file name
@param string list additional drivers containing only theories/modules *)
......@@ -217,7 +217,8 @@ let print_constr info ty fmt (cs,_) =
let print_type_decl info fmt ts = match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>type %a%a@]"
fprintf fmt
"@[<hov 2>type %a%a (* to be defined (uninterpreted type) *)@]"
print_tv_args ts.ts_args (print_ts info) ts
| Some ty ->
fprintf fmt "@[<hov 2>type %a%a =@ %a@]"
......@@ -451,14 +452,15 @@ let print_param_decl info fmt ls =
forget_tvs ()
end
let print_logic_decl info fst fmt (ls,ld) =
let print_logic_decl info isrec fst fmt (ls,ld) =
if has_syntax info ls.ls_name then
fprintf fmt "(* symbol %a is overridden by driver *)"
(print_lident info) ls.ls_name
else begin
let vl,e = open_ls_defn ld in
fprintf fmt "@[<hov 2>%s %a %a : %a =@ %a@]"
(if fst then "let rec" else "and") (print_ls info) ls
(if fst then if isrec then "let rec" else "let" else "and")
(print_ls info) ls
(print_list space (print_vs_arg info)) vl
(print_ls_type info) ls.ls_value (print_defn info) e;
forget_vars vl;
......@@ -486,8 +488,12 @@ let logic_decl info fmt d = match d.d_node with
| Decl.Dparam ls ->
print_param_decl info fmt ls;
fprintf fmt "@\n@\n"
| Dlogic [ls,_ as ld] ->
let isrec = Sid.mem ls.ls_name d.d_syms in
print_logic_decl info isrec true fmt ld;
fprintf fmt "@\n@\n"
| Dlogic ll ->
print_list_next newline (print_logic_decl info) fmt ll;
print_list_next newline (print_logic_decl info true) fmt ll;
fprintf fmt "@\n@\n"
| Dind (s, il) ->
print_list_next newline (print_ind_decl info s) fmt il;
......@@ -508,18 +514,9 @@ let logic_decl info fmt td = match td.td_node with
(** Theories *)
let ocaml_driver env =
try
let file = Filename.concat Config.datadir "drivers/ocaml.drv" in
let drv = Driver.load_driver env file [] in
Driver.syntax_map drv
with e ->
eprintf "cannot find driver 'ocaml'@.";
raise e
let extract_theory env ?old ?fname fmt th =
let extract_theory drv ?old ?fname fmt th =
ignore (old); ignore (fname);
let sm = ocaml_driver env in
let sm = drv.Mlw_driver.drv_syntax in
let info = {
info_syn = sm;
current_theory = th;
......@@ -739,9 +736,9 @@ let pdecl info fmt pd = match pd.pd_node with
(** Modules *)
let extract_module env ?old ?fname fmt m =
let extract_module drv ?old ?fname fmt m =
ignore (old); ignore (fname);
let sm = ocaml_driver env in
let sm = drv.Mlw_driver.drv_syntax in
let th = m.mod_theory in
let info = {
info_syn = sm;
......
......@@ -27,10 +27,10 @@ val debug: Debug.flag
val extract_filename: ?fname:string -> Theory.theory -> string
val extract_theory:
Env.env -> ?old:Pervasives.in_channel -> ?fname:string ->
Mlw_driver.driver -> ?old:Pervasives.in_channel -> ?fname:string ->
Format.formatter -> Theory.theory -> unit
val extract_module:
Env.env -> ?old:Pervasives.in_channel -> ?fname:string ->
Mlw_driver.driver -> ?old:Pervasives.in_channel -> ?fname:string ->
Format.formatter -> Mlw_module.modul -> unit
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