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

Coq realization infrastructure thanks to Andrei's help

parent 9f15e991
...@@ -33,7 +33,7 @@ type prelude_map = prelude Mid.t ...@@ -33,7 +33,7 @@ type prelude_map = prelude Mid.t
type 'a pp = formatter -> 'a -> unit type 'a pp = formatter -> 'a -> unit
type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp type printer = Env.env -> prelude -> prelude_map -> ?realize:bool -> ?old:in_channel -> task pp
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17 let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
...@@ -50,7 +50,7 @@ let lookup_printer s = ...@@ -50,7 +50,7 @@ let lookup_printer s =
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers [] let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let () = register_printer "(null)" (fun _ _ _ ?old:_ _ _ -> ()) let () = register_printer "(null)" (fun _ _ _ ?realize:_ ?old:_ _ _ -> ())
(** Syntax substitutions *) (** Syntax substitutions *)
......
...@@ -31,7 +31,7 @@ type prelude_map = prelude Mid.t ...@@ -31,7 +31,7 @@ type prelude_map = prelude Mid.t
type 'a pp = Format.formatter -> 'a -> unit type 'a pp = Format.formatter -> 'a -> unit
type printer = Env.env -> prelude -> prelude_map -> ?old:in_channel -> task pp type printer = Env.env -> prelude -> prelude_map -> ?realize:bool -> ?old:in_channel -> task pp
val register_printer : string -> printer -> unit val register_printer : string -> printer -> unit
......
...@@ -103,7 +103,7 @@ val used_symbols : theory Mid.t -> theory Mid.t ...@@ -103,7 +103,7 @@ val used_symbols : theory Mid.t -> theory Mid.t
a map from symbol names to their theories of origin *) a map from symbol names to their theories of origin *)
val local_decls : task -> theory Mid.t -> decl list val local_decls : task -> theory Mid.t -> decl list
(** takes the result of [used_symbols] adn returns (** takes the result of [used_symbols] and returns
the list of declarations that are not imported the list of declarations that are not imported
with those theories or derived thereof *) with those theories or derived thereof *)
......
...@@ -280,7 +280,7 @@ let prepare_task drv task = ...@@ -280,7 +280,7 @@ let prepare_task drv task =
let task = update_task drv task in let task = update_task drv task in
List.fold_left apply task transl List.fold_left apply task transl
let print_task_prepared ?old drv fmt task = let print_task_prepared ?realize ?old drv fmt task =
let p = match drv.drv_printer with let p = match drv.drv_printer with
| None -> raise NoPrinter | None -> raise NoPrinter
| Some p -> p | Some p -> p
...@@ -288,15 +288,15 @@ let print_task_prepared ?old drv fmt task = ...@@ -288,15 +288,15 @@ let print_task_prepared ?old drv fmt task =
let printer = let printer =
lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
in in
fprintf fmt "@[%a@]@?" (printer ?old) task fprintf fmt "@[%a@]@?" (printer ?realize ?old) task
let print_task ?old drv fmt task = let print_task ?realize ?old drv fmt task =
let task = prepare_task drv task in let task = prepare_task drv task in
print_task_prepared ?old drv fmt task print_task_prepared ?realize ?old drv fmt task
let print_theory ?old drv fmt th = let print_theory ?old drv fmt th =
let task = Task.use_export None th in let task = Task.use_export None th in
print_task ?old drv fmt task print_task ~realize:true ?old drv fmt task
let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task = let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
let buf = Buffer.create 1024 in let buf = Buffer.create 1024 in
......
...@@ -45,6 +45,7 @@ val call_on_buffer : ...@@ -45,6 +45,7 @@ val call_on_buffer :
val print_task : val print_task :
?realize : bool ->
?old : in_channel -> ?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit driver -> Format.formatter -> Task.task -> unit
...@@ -64,6 +65,7 @@ val prove_task : ...@@ -64,6 +65,7 @@ val prove_task :
val prepare_task : driver -> Task.task -> Task.task val prepare_task : driver -> Task.task -> Task.task
val print_task_prepared : val print_task_prepared :
?realize : bool ->
?old : in_channel -> ?old : in_channel ->
driver -> Format.formatter -> Task.task -> unit driver -> Format.formatter -> Task.task -> unit
......
...@@ -248,7 +248,7 @@ let print_task_old pr thpr fmt task = ...@@ -248,7 +248,7 @@ let print_task_old pr thpr fmt task =
fprintf fmt "%a@." (print_list nothing (print_decl info)) decls fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
let () = register_printer "alt-ergo-old" let () = register_printer "alt-ergo-old"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task_old pr thpr fmt task) print_task_old pr thpr fmt task)
...@@ -261,7 +261,7 @@ let print_decls = ...@@ -261,7 +261,7 @@ let print_decls =
Trans.on_tagged_ls meta_ac (fun ac -> Trans.on_tagged_ls meta_ac (fun ac ->
Printer.sprint_decls (print ac)) Printer.sprint_decls (print ac))
let print_task _env pr thpr ?old:_ fmt task = let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *) (* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *) (* forget_all ident_printer; *)
print_prelude fmt pr; print_prelude fmt pr;
......
...@@ -28,12 +28,12 @@ open Term ...@@ -28,12 +28,12 @@ open Term
open Decl open Decl
open Printer open Printer
let black_list = [ "at"; "cofix"; "exists2"; "fix"; "IF"; "mod"; "Prop";
"return"; "Set"; "Type"; "using"; "where"]
let iprinter = let iprinter =
let bl = [ "at"; "cofix"; "exists2"; "fix"; "IF"; "mod"; "Prop";
"return"; "Set"; "Type"; "using"; "where"]
in
let isanitize = sanitizer char_to_alpha char_to_alnumus in let isanitize = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bl ~sanitizer:isanitize create_ident_printer black_list ~sanitizer:isanitize
let forget_all () = forget_all iprinter let forget_all () = forget_all iprinter
...@@ -101,7 +101,7 @@ let print_pr fmt pr = ...@@ -101,7 +101,7 @@ let print_pr fmt pr =
type info = { type info = {
info_syn : syntax_map; info_syn : syntax_map;
realization : bool; realization : (Theory.theory * ident_printer) Mid.t option;
} }
(** Types *) (** Types *)
...@@ -348,7 +348,7 @@ let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params = ...@@ -348,7 +348,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 then "Definition" else "Parameter") fprintf fmt "%s" (if info.realization <> None then "Definition" else "Parameter")
(* (*
...@@ -507,7 +507,7 @@ let print_type_decl ~old info fmt (ts,def) = ...@@ -507,7 +507,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 (realization ~old ~def:true) (info.realization <> None)
| 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
...@@ -554,7 +554,7 @@ let print_logic_decl ~old info fmt (ls,ld) = ...@@ -554,7 +554,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 (realization ~old ~def:true) (info.realization <> None)
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"
...@@ -613,7 +613,7 @@ let print_ind_decl info fmt d = ...@@ -613,7 +613,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 then if info.realization <> None then
fprintf fmt "Lemma" fprintf fmt "Lemma"
else else
fprintf fmt "Axiom" fprintf fmt "Axiom"
...@@ -625,14 +625,14 @@ let print_proof ~old info fmt = function ...@@ -625,14 +625,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 realization ~old fmt (info.realization <> None)
| 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 then print_context ~old fmt if info.realization <> None 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
...@@ -659,25 +659,54 @@ let print_decl ~old info fmt d = match d.d_node with ...@@ -659,25 +659,54 @@ let print_decl ~old info fmt d = match d.d_node with
let print_decls ~old info fmt dl = let print_decls ~old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
let print_task _env pr thpr ?old fmt task = let init_printer th =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
let pr = create_ident_printer black_list ~sanitizer:isanitize in
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
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 =
if realize = Some true then
let used = Task.used_theories task in
(* 2 cases: goal is clone T with [] or goal is a real goal *)
let used = match task with
| None -> assert false
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
Mid.remove th.Theory.th_name used
| _ -> used
in
let symbols = Task.used_symbols used in
(* build the printers for each theories *)
let printers = Mid.map init_printer used in
let decls = Task.local_decls task symbols in
let symbols =
Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers))
symbols
in
Some symbols, decls
else
None, Task.task_decls task
in
let info = { let info = {
info_syn = get_syntax_map task; info_syn = get_syntax_map task;
realization = false; realization = realization;
} in }
in
let old = match old with let old = match old with
| None -> None | None -> None
| Some ch -> Some(ref NoWhere,ch) | Some ch -> Some(ref NoWhere,ch)
in in
print_decls ~old info fmt (Task.task_decls task) print_decls ~old info fmt decls
let () = register_printer "coq" print_task let () = register_printer "coq" print_task
(* specific printer for realization of theories *) (* specific printer for realization of theories *)
(* OBSOLETE (* OBSOLETE
......
...@@ -331,6 +331,6 @@ let print_task pr thpr fmt task = ...@@ -331,6 +331,6 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "cvc3" let () = register_printer "cvc3"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
...@@ -407,7 +407,7 @@ let print_goal info fmt g = ...@@ -407,7 +407,7 @@ let print_goal info fmt g =
fprintf fmt "# (no goal at all ??)@\n"; fprintf fmt "# (no goal at all ??)@\n";
fprintf fmt "1 in [0,0]@\n" fprintf fmt "1 in [0,0]@\n"
let print_task env pr thpr ?old:_ fmt task = let print_task env pr thpr ?realize:_ ?old:_ fmt task =
forget_all ident_printer; forget_all ident_printer;
let info = get_info env task in let info = get_info env task in
print_prelude fmt pr; print_prelude fmt pr;
......
...@@ -179,7 +179,7 @@ let print_task pr thpr fmt task = ...@@ -179,7 +179,7 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "simplify" let () = register_printer "simplify"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
...@@ -242,6 +242,6 @@ let print_task pr thpr fmt task = ...@@ -242,6 +242,6 @@ let print_task pr thpr fmt task =
fprintf fmt "@\n)@." fprintf fmt "@\n)@."
let () = register_printer "smtv1" let () = register_printer "smtv1"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
...@@ -338,7 +338,7 @@ let print_task_old pr thpr fmt task = ...@@ -338,7 +338,7 @@ let print_task_old pr thpr fmt task =
fprintf fmt "%a@." (print_list nothing (print_decl info)) decls fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
let () = register_printer "smtv2" let () = register_printer "smtv2"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task_old pr thpr fmt task) print_task_old pr thpr fmt task)
...@@ -357,7 +357,7 @@ let print_decls = ...@@ -357,7 +357,7 @@ let print_decls =
Trans.on_meta Discriminate.meta_lsinst (fun dls -> Trans.on_meta Discriminate.meta_lsinst (fun dls ->
Printer.sprint_decls (print dls)) Printer.sprint_decls (print dls))
let print_task _env pr thpr ?old:_ fmt task = let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is taboo *) (* In trans-based p-printing [forget_all] is taboo *)
(* forget_all ident_printer; *) (* forget_all ident_printer; *)
print_prelude fmt pr; print_prelude fmt pr;
......
...@@ -147,7 +147,7 @@ let print_task pr thpr fmt task = ...@@ -147,7 +147,7 @@ let print_task pr thpr fmt task =
(print_decl info) fmt (Task.task_decls task)) (print_decl info) fmt (Task.task_decls task))
let () = register_printer "tptp" let () = register_printer "tptp"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
...@@ -372,7 +372,7 @@ let print_tdecl fmt td = match td.td_node with ...@@ -372,7 +372,7 @@ let print_tdecl fmt td = match td.td_node with
fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n" fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
m.meta_name (print_list comma print_meta_arg) al m.meta_name (print_list comma print_meta_arg) al
let print_task_old _env pr thpr ?old:_ fmt task = let print_task_old _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;
...@@ -386,7 +386,7 @@ let print_tdecls = ...@@ -386,7 +386,7 @@ let print_tdecls =
print_tdecl fmt td in print_tdecl fmt td in
Printer.sprint_tdecls print Printer.sprint_tdecls print
let print_task _env pr thpr ?old:_ fmt task = let print_task _env pr thpr ?realize:_ ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *) (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *) (* forget_all (); *)
print_prelude fmt pr; print_prelude fmt pr;
......
...@@ -331,6 +331,6 @@ let print_task pr thpr fmt task = ...@@ -331,6 +331,6 @@ let print_task pr thpr fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls) ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
let () = register_printer "yices" let () = register_printer "yices"
(fun _env pr thpr ?old:_ fmt task -> (fun _env pr thpr ?realize:_ ?old:_ fmt task ->
forget_all ident_printer; forget_all ident_printer;
print_task pr thpr fmt task) print_task pr thpr fmt task)
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