Commit f7f65b21 authored by MARCHE Claude's avatar MARCHE Claude

an embryo of Coq realization

(standalone executable why3realize)
parent 842acbfc
......@@ -25,6 +25,8 @@ why3.conf
/dep.pdf
/distrib
/META
/why3regtests.err
/why3regtests.out
# /bench/
/bench/programs/good/booleans/
......@@ -42,6 +44,9 @@ why3.conf
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
/bin/why3ml.byte
/bin/why3ml.opt
/bin/why3ml
......
......@@ -272,6 +272,37 @@ install_no_local::
install_local: bin/why3
##################
# Why realize binary
##################
byte: bin/why3realize.byte
opt: bin/why3realize.opt
bin/why3realize.opt: src/why3.cmxa src/realize.cmx
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3realize.byte: src/why3.cma src/realize.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
bin/why3realize: bin/why3realize.@OCAMLBEST@
ln -sf why3realize.@OCAMLBEST@ $@
src/realize.cmo: src/why3.cma
src/realize.cmx: src/why3.cmxa
clean::
rm -f src/realize.cm[iox] src/realize.annot src/realize.o
rm -f bin/realize.byte bin/realize.opt bin/realize
install_no_local::
cp -f bin/why3realize.@OCAMLBEST@ $(BINDIR)/why3realize
install_local: bin/why3realize
########
# Whyml
########
......
......@@ -332,3 +332,13 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
"%a is not a predicate symbol" Pretty.print_ls ls
| e -> raise e)
let print_theory ?old drv fmt th =
let task = Task.use_export None th in
print_task ?old drv fmt task
......@@ -70,3 +70,9 @@ val prove_task_prepared :
driver -> Task.task -> Call_provers.pre_prover_call
(***)
val print_theory :
?old : in_channel ->
driver -> Format.formatter -> Theory.theory -> unit
(** produce a realization of the given theory using the given driver *)
......@@ -92,7 +92,6 @@ let add_opt_meta meta =
let opt_config = ref None
let opt_parser = ref None
let opt_prover = ref None
let opt_coq_realization = ref None
let opt_loadpath = ref []
let opt_driver = ref None
let opt_output = ref None
......@@ -144,9 +143,6 @@ let option_list = Arg.align [
"<prover> Prove or print (with -o) the selected goals";
"--prover", Arg.String (fun s -> opt_prover := Some s),
" same as -P";
"--coq-realize", Arg.String (fun s -> opt_coq_realization := Some s),
" <file> produce, in given file, a Coq realization of the theory given \
using -T";
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> Select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
......@@ -482,55 +478,12 @@ let do_local_theory env drv fname m (tname,_,t,glist) =
in
do_theory env drv fname tname th glist
let do_coq_realize_theory_raw env _drv oldf th =
let old =
if Sys.file_exists oldf
then
begin
let backup = oldf ^ ".bak" in
Sys.rename oldf backup;
Some(open_in backup)
end
else None
in
let ch = open_out oldf in
let fmt = formatter_of_out_channel ch in
Queue.iter
(Coq.print_theory ?old env [] Ident.Mid.empty fmt) th
let do_coq_realize_theory env _drv oldf fname m (tname,_,t,_ths) =
eprintf "[Coq realization] theory '%s' of file '%s'.@." tname fname;
let th = try Mstr.find t m with Not_found ->
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
let old =
if Sys.file_exists oldf
then
begin
let backup = oldf ^ ".bak" in
Sys.rename oldf backup;
Some(open_in backup)
end
else None
in
let ch = open_out oldf in
let fmt = formatter_of_out_channel ch in
Coq.print_theory ?old env [] Ident.Mid.empty fmt th
let do_input env drv = function
| None, _ when !opt_parse_only || !opt_type_only ->
()
| None, tlist ->
begin
match !opt_coq_realization with
| Some f ->
eprintf "[Coq realization] output file: %s@." f;
(*
Queue.iter (do_coq_realize_theory_raw env drv f) tlist
*)
| None -> Queue.iter (do_global_theory env drv) tlist
end
Queue.iter (do_global_theory env drv) tlist
| Some f, tlist ->
let fname, cin = match f with
| "-" -> "stdin", stdin
......@@ -541,18 +494,13 @@ let do_input env drv = function
if !opt_type_only then
()
else
match !opt_coq_realization with
| Some f ->
eprintf "[Coq realization] output file: %s@." f;
Queue.iter (do_coq_realize_theory env drv f fname m) tlist
| None ->
if Queue.is_empty tlist then
let glist = Queue.create () in
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_theory env drv fname t th glist in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
if Queue.is_empty tlist then
let glist = Queue.create () in
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_theory env drv fname t th glist in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
let () =
try
......
......@@ -679,6 +679,7 @@ let () = register_printer "coq" print_task
(* specific printer for realization of theories *)
(* OBSOLETE
open Theory
......@@ -712,6 +713,7 @@ let print_theory _env pr thpr ?old fmt th =
print_tdecls ~old info fmt th.th_decls;
produce_remaining_contexts_and_proofs ~old fmt
*)
(*
Local Variables:
......
......@@ -17,5 +17,7 @@
(* *)
(**************************************************************************)
(* OBSOLETE
val print_theory : Env.env -> Printer.prelude -> Printer.prelude_map ->
?old:Pervasives.in_channel -> Format.formatter -> Theory.theory -> unit
*)
open Why3
open Format
(* produce a realization of a theory *)
let do_theory _env drv _path thname th =
let oldf = thname ^ ".v" in
let old =
if Sys.file_exists oldf
then
begin
let backup = oldf ^ ".bak" in
Sys.rename oldf backup;
Some(open_in backup)
end
else None
in
eprintf "[Coq realization] realizing theory '%s' in file '%s'.@." thname oldf;
let ch = open_out oldf in
let fmt = formatter_of_out_channel ch in
fprintf fmt "(* Coq file produced by why3realize *)@\n@\n";
Driver.print_theory ?old drv fmt th;
fprintf fmt "@.";
close_out ch
let rdot = (Str.regexp "\\.")
let do_global_theory env drv t =
let l = Str.split rdot t in
let p, t = match List.rev l with
| [] -> assert false
| [_] ->
eprintf "Theory name must be qualified.@.";
exit 1
| t::p -> List.rev p, t
in
let th = try Env.find_theory env p t with Env.TheoryNotFound _ ->
eprintf "Theory '%s' not found.@." t;
exit 1
in
do_theory env drv p t th
(* command-line options *)
let usage_msg = sprintf
"Usage: %s [options] <theory>"
(Filename.basename Sys.argv.(0))
let opt_loadpath = ref []
let add_loadpath s = opt_loadpath := s :: !opt_loadpath
let opt_theory = ref None
let add_opt_theory t =
match !opt_theory with
| None -> opt_theory := Some t
| Some _ -> eprintf "%s@." usage_msg; exit 2
let option_list = Arg.align [
"-L", Arg.String add_loadpath,
"<dir> Add <dir> to the library search path";
"--library", Arg.String add_loadpath,
" same as -L";
"-I", Arg.String add_loadpath,
" same as -L (obsolete)";
]
(* parsing command-line options *)
let () =
try
Arg.parse option_list add_opt_theory usage_msg
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(* main program *)
let () =
match !opt_theory with
| None -> eprintf "%s@." usage_msg; exit 2
| Some th ->
try
let config = Whyconf.read_config None in
let main = Whyconf.get_main config in
let env =
Env.create_env_of_loadpath (!opt_loadpath @ Whyconf.loadpath main)
in
let coq =
try Util.Mstr.find "coq" (Whyconf.get_provers config)
with Not_found ->
eprintf "Driver for Coq not found@.";
exit 2
in
let drv = Driver.load_driver env coq.Whyconf.driver in
do_global_theory env drv th
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
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