From e86ea2b51a9f10a0065416e6ec0f49f649129d83 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 23 Apr 2012 15:14:14 +0000 Subject: correct abort in Function when a proof of inversion fails git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15239 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/invfun.ml | 49 ++++++++++++++++++++-------------------------- toplevel/backtrack.ml | 2 +- toplevel/vernacentries.ml | 13 ++++++------ toplevel/vernacentries.mli | 12 +----------- 4 files changed, 29 insertions(+), 47 deletions(-) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e4695792be..b92a8daf39 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1023,6 +1023,7 @@ let do_save () = Lemmas.save_named false *) let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = + let previous_state = States.freeze () in let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in try @@ -1064,22 +1065,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_correct_id is valid since we are constructing the lemma + (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_correct_id f_id) + i*) + let lem_id = mk_correct_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove correctness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id))) - } - + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with correctness_lemma = Some lem_cst} ) funs; let lemmas_types_infos = @@ -1116,34 +1116,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_complete_id is valid since we are constructing the lemma + (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_complete_id f_id) + i*) + let lem_id = mk_complete_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove completeness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id))) - } + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with completeness_lemma = Some lem_cst} ) funs; with e -> (* In case of problem, we reset all the lemmas *) - (*i The next call to mk_correct_id is valid since we are erasing the lemmas - Ensures by: obvious - i*) - let first_lemma_id = - let f_id = id_of_label (con_label funs.(0)) in - - mk_correct_id f_id - in - (try Backtrack.reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); + Pfedit.delete_all_proofs (); + States.unfreeze previous_state; raise e diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index a84550a5d3..24a056d738 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -167,7 +167,7 @@ let reset_initial () = let init_label = Lib.first_command_label in if Lib.current_command_label () = init_label then () else begin - if Pfedit.refining() then Pfedit.delete_all_proofs (); + Pfedit.delete_all_proofs (); Lib.reset_label init_label; Stack.clear history; Stack.push diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3652e2a6b0..22ac6e90c1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -745,14 +745,13 @@ let vernac_chdir = function (********************) (* State management *) -let abort_refine f x = - if Pfedit.refining() then delete_all_proofs (); - f x - (* used to be: error "Must save or abort current goal first" *) +let vernac_write_state file = + Pfedit.delete_all_proofs (); + States.extern_state file -let vernac_write_state file = abort_refine States.extern_state file - -let vernac_restore_state file = abort_refine States.intern_state file +let vernac_restore_state file = + Pfedit.delete_all_proofs (); + States.intern_state file (************) (* Commands *) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 66aa6c20a5..a9d384ea03 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -23,13 +23,6 @@ val show_node : unit -> unit in the context of the current goal, as for instance in pcoq *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env -(*i - -(** this function is used to analyse the extra arguments in search commands. - It is used in pcoq. *) (*i anciennement: inside_outside i*) -val interp_search_restriction : search_restriction -> dir_path list * bool -i*) - type pcoq_hook = { start_proof : unit -> unit; solve : int -> unit; @@ -44,10 +37,7 @@ type pcoq_hook = { val set_pcoq_hook : pcoq_hook -> unit -(** This function makes sure that the function given in argument is preceded - by a command aborting all proofs if necessary. - It is used in pcoq. *) -val abort_refine : ('a -> unit) -> 'a -> unit;; +(** The main interpretation function of vernacular expressions *) val interp : Vernacexpr.vernac_expr -> unit -- cgit v1.2.3