Commit f796cd6d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Switch to an always-on realization mode for Coq.

There are hardly any change to the code. It now just looks whether
dependencies are marked as realized. The old no-realization mode is
equivalent to marking no theory as realized, while the old realization
mode amounts to marking all of the theories as realized. Now, the finer
granularity make any intermediate state reachable. This is just a proof
of concept, so the actual set of realized theories is hard-coded.
parent 2af41451
...@@ -102,24 +102,21 @@ let print_pr fmt pr = ...@@ -102,24 +102,21 @@ let print_pr fmt pr =
type info = { type info = {
info_syn : syntax_map; info_syn : syntax_map;
realization : (Theory.theory * ident_printer) Mid.t option; symbol_printers : (Theory.theory * ident_printer) Mid.t;
realization : bool;
} }
let print_path = print_list (constant_string ".") string let print_path = print_list (constant_string ".") string
let print_id fmt id = string fmt (id_unique iprinter id) let print_id fmt id = string fmt (id_unique iprinter id)
let print_id_real info fmt id = match info.realization with let print_id_real info fmt id =
| Some m -> try let th,ipr = Mid.find id info.symbol_printers in
begin
try let th,ipr = Mid.find id m in
fprintf fmt "%a.%s.%s" fprintf fmt "%a.%s.%s"
print_path th.Theory.th_path print_path th.Theory.th_path
th.Theory.th_name.id_string th.Theory.th_name.id_string
(id_unique ipr id) (id_unique ipr id)
with Not_found -> print_id fmt id with Not_found -> print_id fmt id
end
| None -> print_id fmt id
let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
...@@ -369,7 +366,7 @@ let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params = ...@@ -369,7 +366,7 @@ let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params =
end end
let definition fmt info = let definition fmt info =
fprintf fmt "%s" (if info.realization <> None then "Definition" else "Parameter") fprintf fmt "%s" (if info.realization then "Definition" else "Parameter")
(* (*
...@@ -528,7 +525,7 @@ let print_type_decl ~old info fmt (ts,def) = ...@@ -528,7 +525,7 @@ let print_type_decl ~old info fmt (ts,def) =
fprintf fmt "@[<hov 2>%a %a : %aType.@]@\n%a" fprintf fmt "@[<hov 2>%a %a : %aType.@]@\n%a"
definition info definition info
print_ts ts print_params_list ts.ts_args print_ts ts print_params_list ts.ts_args
(realization ~old ~def:true) (info.realization <> None) (realization ~old ~def:true) info.realization
| Some ty -> | Some ty ->
fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n" fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
print_ts ts (print_list space print_tv_binder) ts.ts_args print_ts ts (print_list space print_tv_binder) ts.ts_args
...@@ -575,7 +572,7 @@ let print_logic_decl ~old info fmt (ls,ld) = ...@@ -575,7 +572,7 @@ let print_logic_decl ~old info fmt (ls,ld) =
print_params all_ty_params print_params all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args (print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
(realization ~old ~def:true) (info.realization <> None) (realization ~old ~def:true) info.realization
end; end;
print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params; print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n" fprintf fmt "@\n"
...@@ -634,7 +631,7 @@ let print_ind_decl info fmt d = ...@@ -634,7 +631,7 @@ let print_ind_decl info fmt d =
let print_pkind info fmt = function let print_pkind info fmt = function
| Paxiom -> | Paxiom ->
if info.realization <> None then if info.realization then
fprintf fmt "Lemma" fprintf fmt "Lemma"
else else
fprintf fmt "Axiom" fprintf fmt "Axiom"
...@@ -646,14 +643,14 @@ let print_proof ~old info fmt = function ...@@ -646,14 +643,14 @@ let print_proof ~old info fmt = function
| Plemma | Pgoal -> | Plemma | Pgoal ->
realization ~old fmt true realization ~old fmt true
| Paxiom -> | Paxiom ->
realization ~old fmt (info.realization <> None) realization ~old fmt info.realization
| Pskip -> () | Pskip -> ()
let print_proof_context ~old info fmt = function let print_proof_context ~old info fmt = function
| Plemma | Pgoal -> | Plemma | Pgoal ->
print_context ~old fmt print_context ~old fmt
| Paxiom -> | Paxiom ->
if info.realization <> None then print_context ~old fmt if info.realization then print_context ~old fmt
| Pskip -> () | Pskip -> ()
let print_decl ~old info fmt d = match d.d_node with let print_decl ~old info fmt d = match d.d_node with
...@@ -686,14 +683,28 @@ let init_printer th = ...@@ -686,14 +683,28 @@ let init_printer th =
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local; Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr pr
let print_task env pr thpr realize ?old fmt task = (* TODO: change into a less intrusive coding, e.g. a driver meta, and
make the lookup a bit more efficient along the way *)
let realized_theories = [
["int"; "Abs"];
["int"; "ComputerDivision"];
["int"; "EuclideanDivision"];
["int"; "Int"];
["int"; "MinMax"];
["real"; "Abs"];
["real"; "FromInt"];
["real"; "MinMax"];
["real"; "Real"];
["real"; "Square"];
]
let print_task _env pr thpr realize ?old fmt task =
forget_all (); forget_all ();
print_prelude fmt pr; print_prelude fmt pr;
print_th_prelude task fmt thpr; print_th_prelude task fmt thpr;
let realization,decls = let symbol_printers,decls =
if realize then
let used = Task.used_theories task in let used = Task.used_theories task in
let used = Mid.filter (fun _ th -> th.Theory.th_path <> []) used in let used = Mid.filter (fun _ th -> List.mem (th.Theory.th_path@[th.Theory.th_name.id_string]) realized_theories) used in
(* 2 cases: goal is clone T with [] or goal is a real goal *) (* 2 cases: goal is clone T with [] or goal is a real goal *)
let used = match task with let used = match task with
| None -> assert false | None -> assert false
...@@ -704,10 +715,12 @@ let print_task env pr thpr realize ?old fmt task = ...@@ -704,10 +715,12 @@ let print_task env pr thpr realize ?old fmt task =
Mid.remove th.Theory.th_name used Mid.remove th.Theory.th_name used
| _ -> used | _ -> used
in in
(*
(* output the Require commands *) (* output the Require commands *)
List.iter List.iter
(fprintf fmt "Add Rec LoadPath \"%s\".@\n") (fprintf fmt "Add Rec LoadPath \"%s\".@\n")
(Env.get_loadpath env); (Env.get_loadpath env);
*)
Mid.iter Mid.iter
(fun id th -> fprintf fmt "Require %a.%s.@\n" (fun id th -> fprintf fmt "Require %a.%s.@\n"
print_path th.Theory.th_path id.id_string) print_path th.Theory.th_path id.id_string)
...@@ -720,13 +733,12 @@ let print_task env pr thpr realize ?old fmt task = ...@@ -720,13 +733,12 @@ let print_task env pr thpr realize ?old fmt task =
Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers)) Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers))
symbols symbols
in in
Some symbols, decls symbols, decls
else
None, Task.task_decls task
in in
let info = { let info = {
info_syn = get_syntax_map task; info_syn = get_syntax_map task;
realization = realization; symbol_printers = symbol_printers;
realization = realize;
} }
in in
let old = match old with let old = match old with
......
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