Commit 4ccdc0b8 authored by MARCHE Claude's avatar MARCHE Claude

embryon de realisation en Coq

parent 86720958
......@@ -111,14 +111,24 @@ let print_prelude fmt pl =
let println fmt s = fprintf fmt "%s@\n" s in
print_list nothing println fmt pl
let print_prelude_of_theories th_used fmt pm =
List.iter (fun th ->
let prel = Mid.find_default th.th_name [] pm in
print_prelude fmt prel) th_used
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
| { td_node = Clone (th,sm) } when is_empty_sm sm -> th::acc
| _ -> acc) [] task
in
List.iter (fun th ->
let prel = Mid.find_default th.th_name [] pm in
print_prelude fmt prel) th_used
print_prelude_of_theories th_used fmt pm
let print_prelude_for_theory th fmt pm =
let th_used = List.fold_left (fun acc -> function
| { td_node = Clone (th,sm) } when is_empty_sm sm -> th::acc
| _ -> acc) [] th.th_decls
in
print_prelude_of_theories th_used fmt pm
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol
......
......@@ -43,6 +43,7 @@ val list_printers : unit -> string list
val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp
val print_prelude_for_theory : theory -> prelude_map pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
......
......@@ -92,6 +92,7 @@ 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 false
let opt_loadpath = ref []
let opt_driver = ref None
let opt_output = ref None
......@@ -139,6 +140,8 @@ 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.Set opt_coq_realization,
" produce a Coq realization of 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),
......@@ -420,6 +423,13 @@ 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 env _drv fname m (tname,_,t,_glist) =
let th = try Mnm.find t m with Not_found ->
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
Coq.print_theory env [] Ident.Mid.empty std_formatter th
let do_input env drv = function
| None, _ when !opt_parse_only || !opt_type_only ->
()
......@@ -434,6 +444,8 @@ let do_input env drv = function
close_in cin;
if !opt_type_only then
()
else if !opt_coq_realization then
Queue.iter (do_coq_realize_theory env drv fname m) tlist
else 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
......
......@@ -94,6 +94,7 @@ let print_pr fmt pr =
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
realization : bool;
}
(** Types *)
......@@ -326,13 +327,55 @@ let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params =
if need_context then fprintf fmt "Unset Contextual Implicit.@\n"
end
let print_type_decl info fmt (ts,def) =
let definition fmt info =
fprintf fmt "%s" (if info.realization then "Definition" else "Parameter")
let proof_begin = "(* YOU MAY EDIT THE PROOF BELOW *)"
let proof_end = "(* DO NOT EDIT BELOW *)"
let print_empty_proof ?(def=false) fmt =
fprintf fmt "%s@\n" proof_begin;
if not def then fprintf fmt "intuition.@\n";
fprintf fmt "@\n";
fprintf fmt "%s.@\n" (if def then "Defined" else "Qed");
fprintf fmt "%s@\n@\n" proof_end
let print_next_proof ?def ch fmt =
try
while true do
let s = input_line ch in
if s = proof_begin then
begin
fprintf fmt "%s@\n" proof_begin;
while true do
let s = input_line ch in
fprintf fmt "%s@\n" s;
if s = proof_end then raise Exit
done
end
done
with
| End_of_file -> print_empty_proof ?def fmt
| Exit -> fprintf fmt "@\n"
let realization ?old ?def fmt info =
if info.realization then
begin match old with
| None -> print_empty_proof ?def fmt
| Some ch -> print_next_proof ?def ch fmt
end
else
fprintf fmt "@\n"
let print_type_decl ?old info fmt (ts,def) =
if is_ts_tuple ts then () else
match def with
| Tabstract -> begin match ts.ts_def with
| None ->
fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
fprintf fmt "@[<hov 2>%a %a : %aType.@]@\n%a"
definition info
print_ts ts print_params_list ts.ts_args
(realization ?old ~def:true) info
| Some ty ->
fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
print_ts ts (print_arrow_list print_tv_binder) ts.ts_args
......@@ -359,7 +402,7 @@ let print_ls_type ?(arrow=false) info fmt ls =
| None -> fprintf fmt "Prop"
| Some ty -> print_ty info fmt ty
let print_logic_decl info fmt (ls,ld) =
let print_logic_decl ?old info fmt (ls,ld) =
let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ls in
begin
match ld with
......@@ -373,11 +416,13 @@ let print_logic_decl info fmt (ls,ld) =
(print_expr info) e;
List.iter forget_var vl
| None ->
fprintf fmt "@[<hov 2>Parameter %a: %a%a@ %a.@]@\n"
fprintf fmt "@[<hov 2>%a %a: %a%a@ %a.@]@\n%a"
definition info
print_ls ls
print_params all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
(realization ?old ~def:true) info
end;
print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n"
......@@ -400,46 +445,29 @@ let print_ind_decl info fmt d =
if not (Sid.mem (fst d).ls_name info.info_rem) then
(print_ind_decl info fmt d; forget_tvs ())
let print_pkind fmt = function
| Paxiom -> fprintf fmt "Axiom"
let print_pkind info fmt = function
| Paxiom ->
if info.realization then
fprintf fmt "Lemma"
else
fprintf fmt "Axiom"
| Plemma -> fprintf fmt "Lemma"
| Pgoal -> fprintf fmt "Theorem"
| Pskip -> assert false (* impossible *)
let proof_begin = "(* YOU MAY EDIT THE PROOF BELOW *)"
let proof_end = "(* DO NOT EDIT BELOW *)"
let print_empty_proof fmt =
fprintf fmt "%s@\n" proof_begin;
fprintf fmt "intuition.@\n";
fprintf fmt "@\n";
fprintf fmt "Qed.@\n";
fprintf fmt "%s@\n" proof_end
let print_next_proof ch fmt =
try
while true do
let s = input_line ch in
if s = proof_begin then
begin
fprintf fmt "%s@\n" proof_begin;
while true do
let s = input_line ch in
fprintf fmt "%s@\n" s;
if s = proof_end then raise Exit
done
end
done
with
| End_of_file -> print_empty_proof fmt
| Exit -> ()
let print_proof ?old fmt = function
| Paxiom | Pskip -> ()
let print_proof ?old info fmt = function
| Plemma | Pgoal ->
match old with
begin match old with
| None -> print_empty_proof fmt
| Some ch -> print_next_proof ch fmt
end
| Paxiom ->
if info.realization then
begin match old with
| None -> print_empty_proof fmt
| Some ch -> print_next_proof ch fmt
end
| Pskip -> ()
let print_decl ?old info fmt d = match d.d_node with
| Dtype tl -> print_list nothing (print_type_decl info) fmt tl
......@@ -452,11 +480,11 @@ let print_decl ?old info fmt d = match d.d_node with
fprintf fmt "(* DO NOT EDIT BELOW *)@\n@\@\n";
*)
let params = f_ty_freevars Stv.empty f in
fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a@\n"
print_pkind k
fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
(print_pkind info) k
print_pr pr
print_params params
(print_fmla info) f (print_proof ?old) k;
(print_fmla info) f (print_proof ?old info) k;
forget_tvs ()
let print_decls ?old info fmt dl =
......@@ -468,7 +496,9 @@ let print_task _env pr thpr ?old fmt task =
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task } in
info_rem = get_remove_set task;
realization = false;
} in
print_decls ?old info fmt (Task.task_decls task)
let () = register_printer "coq" print_task
......@@ -476,6 +506,37 @@ let () = register_printer "coq" print_task
(* specific printer for realization of theories *)
open Theory
let print_tdecl ?old info fmt d = match d.td_node with
| Decl d -> print_decl ?old info fmt d
| Use _ -> ()
| Meta _ -> ()
| Clone _ -> ()
let print_tdecls ?old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_tdecl ?old info)) dl
let print_theory _env pr thpr ?old fmt th =
forget_all ();
print_prelude fmt pr;
print_prelude_for_theory th fmt thpr;
(* TODO
let info = {
info_syn = get_syntax_map th;
info_rem = get_remove_set th} in
*)
let info = {
info_syn = Mid.empty;
info_rem = Mid.empty;
realization = true;
}
in
print_tdecls ?old info fmt th.th_decls
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. "
......
......@@ -44,7 +44,7 @@ theory TestSplit
logic bb int
goal G : aa 0 /\ bb 1 -> false
goal G : aa 0 && bb 1 -> false
end
......@@ -116,3 +116,14 @@ end
theory TestRealize
type t
logic f t : t
logic p t t
axiom A : forall x:t. p (f x) x
end
\ No newline at end of file
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