Commit eeeb58d9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Preserve realization headers in Coq printer.

parent aafbd002
...@@ -518,8 +518,9 @@ let read_deprecated_script ch in_context = ...@@ -518,8 +518,9 @@ let read_deprecated_script ch in_context =
let read_old_script = let read_old_script =
let axm = Str.regexp "\\(Axiom\\|Parameter\\)[ ]+\\([^ :(.]+\\)" in let axm = Str.regexp "\\(Axiom\\|Parameter\\)[ ]+\\([^ :(.]+\\)" in
let prelude = Str.regexp "(\\* This file is generated by Why3.*\\*)" in
fun ch -> fun ch ->
let skip_to_empty = ref true in let skip_to_empty = ref false in
let last_empty_line = ref 0 in let last_empty_line = ref 0 in
let sc = ref [] in let sc = ref [] in
try try
...@@ -538,6 +539,9 @@ let read_old_script = ...@@ -538,6 +539,9 @@ let read_old_script =
skip_to_empty := true) else skip_to_empty := true) else
if s = "(* Why3 goal *)" then if s = "(* Why3 goal *)" then
(sc := read_old_proof ch :: !sc; skip_to_empty := true) else (sc := read_old_proof ch :: !sc; skip_to_empty := true) else
if Str.string_match prelude s 0 then
(sc := Info "Why3 prelude" :: !sc;
skip_to_empty := true) else
if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then
(sc := read_deprecated_script ch true; raise End_of_file) else (sc := read_deprecated_script ch true; raise End_of_file) else
if s = "(* YOU MAY EDIT THE PROOF BELOW *)" then if s = "(* YOU MAY EDIT THE PROOF BELOW *)" then
...@@ -955,8 +959,6 @@ let print_decls ~old info fmt dl = ...@@ -955,8 +959,6 @@ let print_decls ~old info fmt dl =
let print_task printer_args ~realize ~ssreflect ?old fmt task = let print_task printer_args ~realize ~ssreflect ?old fmt task =
(* eprintf "Task:%a@.@." Pretty.print_task task; *) (* eprintf "Task:%a@.@." Pretty.print_task task; *)
forget_all (); forget_all ();
print_prelude fmt printer_args.prelude;
print_th_prelude task fmt printer_args.th_prelude;
(* find theories that are both used and realized from metas *) (* find theories that are both used and realized from metas *)
let realized_theories = let realized_theories =
Task.on_meta meta_realized_theory (fun mid args -> Task.on_meta meta_realized_theory (fun mid args ->
...@@ -983,8 +985,7 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task = ...@@ -983,8 +985,7 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task =
upd_realized_theories task upd_realized_theories task
| _ -> assert false in | _ -> assert false in
let realized_theories = upd_realized_theories task in let realized_theories = upd_realized_theories task in
let realized_theories' = let realized_theories' = Mid.map fst realized_theories in
Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in let realized_symbols = Task.used_symbols realized_theories' in
let local_decls = Task.local_decls task realized_symbols in let local_decls = Task.local_decls task realized_symbols in
(* eprintf "local_decls:%i@." (List.length local_decls); *) (* eprintf "local_decls:%i@." (List.length local_decls); *)
...@@ -1010,6 +1011,10 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task = ...@@ -1010,6 +1011,10 @@ let print_task printer_args ~realize ~ssreflect ?old fmt task =
let old = ref (match old with let old = ref (match old with
| None -> [] | None -> []
| Some ch -> read_old_script ch) in | Some ch -> read_old_script ch) in
ignore (output_till_statement fmt old "Why3 prelude");
print_prelude fmt printer_args.prelude;
print_th_prelude task fmt printer_args.th_prelude;
Mid.iter (fun _ (_, s) -> fprintf fmt "Require %s.@\n" s) realized_theories;
print_decls ~old info fmt local_decls; print_decls ~old info fmt local_decls;
output_remaining fmt !old output_remaining fmt !old
......
Supports Markdown
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