Commit d51f735c authored by MARCHE Claude's avatar MARCHE Claude

realisation en Coq marche mais sans regle de syntaxe

parent 4ccdc0b8
......@@ -148,7 +148,7 @@ let syntax_logic ls s =
let remove_prop pr =
create_meta meta_remove_prop [MApr pr]
let get_syntax_map task =
let get_syntax_map, get_syntax_map_of_theory =
let add_ts m = function
| [MAts ts; MAstr s] ->
Mid.add_new ts.ts_name s (KnownTypeSyntax ts) m
......@@ -159,10 +159,17 @@ let get_syntax_map task =
Mid.add_new ls.ls_name s (KnownLogicSyntax ls) m
| _ -> assert false
in
let m = Mid.empty in
let m = Task.on_meta meta_syntax_logic add_ls m task in
let m = Task.on_meta meta_syntax_type add_ts m task in
m
(fun task ->
let m = Mid.empty in
let m = Task.on_meta meta_syntax_logic add_ls m task in
let m = Task.on_meta meta_syntax_type add_ts m task in
m),
(fun theory ->
let m = Mid.empty in
let m = Theory.on_meta meta_syntax_logic add_ls m theory in
let m = Theory.on_meta meta_syntax_type add_ts m theory in
m)
let get_remove_set task =
let add_ts s = function
......
......@@ -56,6 +56,8 @@ val remove_prop : prsymbol -> tdecl
val get_syntax_map : task -> string Mid.t
val get_remove_set : task -> Sid.t
val get_syntax_map_of_theory : theory -> string Mid.t
val query_syntax : string Mid.t -> ident -> string option
val syntax_arguments : string -> 'a pp -> 'a list pp
......
......@@ -114,8 +114,8 @@ let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_meta = option_apply Mmeta.empty (fun t -> t.task_meta)
let find_clone_tds task th = cm_find (task_clone task) th
let find_meta_tds task t = mm_find (task_meta task) t
let find_clone_tds task (th : theory) = cm_find (task_clone task) th
let find_meta_tds task (t : meta) = mm_find (task_meta task) t
(* constructors with checks *)
......
......@@ -713,6 +713,32 @@ let clone_meta tdt sm = match tdt.td_node with
mk_tdecl (Meta (t, List.map cl_marg al))
| _ -> invalid_arg "clone_meta"
(** access to meta *)
(*
let theory_meta = option_apply Mmeta.empty (fun t -> t.task_meta)
let find_meta_tds th (t : meta) = mm_find (theory_meta th) t
let on_meta meta fn acc theory =
let add td acc = match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> assert false
in
let tds = find_meta_tds theory meta in
Stdecl.fold add tds.tds_set acc
*)
let on_meta meta fn acc theory =
let tdecls = theory.th_decls in
List.fold_left
(fun acc td ->
match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> acc)
acc tdecls
(** Base theories *)
......
......@@ -182,6 +182,8 @@ val clone_meta : tdecl -> symbol_map -> tdecl
(* [clone_meta td_meta sm] produces from [td_meta]
* a new Meta tdecl instantiated with respect to [sm]]. *)
val on_meta: meta-> ('a -> meta_arg list -> 'a) -> 'a -> theory -> 'a
(** Base theories *)
val builtin_theory : theory
......
......@@ -135,11 +135,11 @@ let edit_proof () =
let (_debug,editor,file,driver,callback,goal) =
Queue.pop proof_edition_queue in
Mutex.unlock queue_lock;
let backup = file ^ ".bak" in
let old =
if Sys.file_exists file
then
begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some(open_in backup)
end
......
......@@ -92,7 +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_coq_realization = ref None
let opt_loadpath = ref []
let opt_driver = ref None
let opt_output = ref None
......@@ -140,8 +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";
"--coq-realize", Arg.String (fun s -> opt_coq_realization := Some s),
" 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),
......@@ -423,12 +423,24 @@ 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 do_coq_realize_theory env _drv oldf 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 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 ->
......@@ -444,15 +456,18 @@ 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
let do_th _ (t,th) = do_theory env drv fname t th glist in
Ident.Mid.iter do_th (Mnm.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
else
match !opt_coq_realization with
| Some 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 (Mnm.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_local_theory env drv fname m) tlist
let () =
try
......
......@@ -358,16 +358,16 @@ let print_next_proof ?def ch fmt =
| End_of_file -> print_empty_proof ?def fmt
| Exit -> fprintf fmt "@\n"
let realization ?old ?def fmt info =
let realization ~old ?def fmt info =
if info.realization then
begin match old with
| None -> print_empty_proof ?def fmt
| None -> assert false; 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) =
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
......@@ -375,7 +375,7 @@ let print_type_decl ?old info fmt (ts,def) =
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
(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
......@@ -392,9 +392,9 @@ let print_type_decl ?old info fmt (ts,def) =
csl;
fprintf fmt "@\n"
let print_type_decl info fmt d =
let print_type_decl ~old info fmt d =
if not (Sid.mem (fst d).ts_name info.info_rem) then
(print_type_decl info fmt d; forget_tvs ())
(print_type_decl ~old info fmt d; forget_tvs ())
let print_ls_type ?(arrow=false) info fmt ls =
if arrow then fprintf fmt " ->@ ";
......@@ -402,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 ?old 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
......@@ -422,15 +422,15 @@ let print_logic_decl ?old info fmt (ls,ld) =
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
(realization ~old ~def:true) info
end;
print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n"
let print_logic_decl info fmt d =
let print_logic_decl ~old info fmt d =
if not (Sid.mem (fst d).ls_name info.info_rem) then
(print_logic_decl info fmt d; forget_tvs ())
(print_logic_decl ~old info fmt d; forget_tvs ())
let print_ind info fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) f
......@@ -455,7 +455,7 @@ let print_pkind info fmt = function
| Pgoal -> fprintf fmt "Theorem"
| Pskip -> assert false (* impossible *)
let print_proof ?old info fmt = function
let print_proof ~old info fmt = function
| Plemma | Pgoal ->
begin match old with
| None -> print_empty_proof fmt
......@@ -469,9 +469,9 @@ let print_proof ?old info fmt = function
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
| Dlogic ll -> print_list nothing (print_logic_decl info) fmt ll
let print_decl ~old info fmt d = match d.d_node with
| Dtype tl -> print_list nothing (print_type_decl ~old info) fmt tl
| Dlogic ll -> print_list nothing (print_logic_decl ~old info) fmt ll
| Dind il -> print_list nothing (print_ind_decl info) fmt il
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
| Dprop (k,pr,f) ->
......@@ -484,11 +484,11 @@ let print_decl ?old info fmt d = match d.d_node with
(print_pkind info) k
print_pr pr
print_params params
(print_fmla info) f (print_proof ?old info) k;
(print_fmla info) f (print_proof ~old info) k;
forget_tvs ()
let print_decls ?old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ?old info)) dl
let print_decls ~old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
let print_task _env pr thpr ?old fmt task =
forget_all ();
......@@ -499,7 +499,7 @@ let print_task _env pr thpr ?old fmt task =
info_rem = get_remove_set task;
realization = false;
} in
print_decls ?old info fmt (Task.task_decls task)
print_decls ~old info fmt (Task.task_decls task)
let () = register_printer "coq" print_task
......@@ -510,16 +510,16 @@ let () = register_printer "coq" print_task
open Theory
let print_tdecl ?old info fmt d = match d.td_node with
| Decl d -> print_decl ?old info fmt d
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_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 =
let print_theory _env pr thpr ~old fmt th =
forget_all ();
print_prelude fmt pr;
print_prelude_for_theory th fmt thpr;
......@@ -529,12 +529,12 @@ let print_theory _env pr thpr ?old fmt th =
info_rem = get_remove_set th} in
*)
let info = {
info_syn = Mid.empty;
info_syn = Mid.empty (* get_syntax_map_of_theory th *);
info_rem = Mid.empty;
realization = true;
}
in
print_tdecls ?old info fmt th.th_decls
print_tdecls ~old info fmt th.th_decls
(*
......
......@@ -124,6 +124,10 @@ theory TestRealize
logic p t t
axiom P_sym: forall x y:t. p x y <-> p y x
axiom A : forall x:t. p (f x) x
lemma B : forall x:t. p x (f 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