diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
tree | 9b221c283c2971f7ac151397231059e1d239e723 /plugins/funind | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 55 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 42 |
4 files changed, 53 insertions, 49 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 1d1e4a2a..33d77568 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1371,7 +1371,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto false (false,5) [] (Some []) + Eauto.gen_eauto (false,5) [] (Some []) ] gls @@ -1449,7 +1449,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = ( tclCOMPLETE( Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 123399d5..06abb8ce 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = - Genarg.create_arg "function_rec_definition_loc" + Genarg.create_arg None "function_rec_definition_loc" VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> [ diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0b04a572..95ca86c2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -588,15 +588,15 @@ let rec reflexivity_with_destruct_cases g = ) in (tclFIRST - [ reflexivity; - tclTHEN (tclPROGRESS discr_inject) (destruct_case ()); + [ observe_tac "reflexivity_with_destruct_cases : reflexivity" reflexivity; + observe_tac "reflexivity_with_destruct_cases : destruct_case" ((destruct_case ())); (* We reach this point ONLY if the same value is matched (at least) two times along binding path. In this case, either we have a discriminable hypothesis and we are done, either at least an injectable one and we do the injection before continuing *) - tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases + observe_tac "reflexivity_with_destruct_cases : others" (tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases) ]) g @@ -752,6 +752,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 @@ -793,22 +794,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 = @@ -845,34 +845,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 - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); + Pfedit.delete_all_proofs (); + States.unfreeze previous_state; raise e diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 55ebd31b..3355300e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -48,7 +48,8 @@ open Genarg let compute_renamed_type gls c = - rename_bound_vars_as_displayed [] (pf_type_of gls c) + rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] + (pf_type_of gls c) let qed () = Lemmas.save_named true let defined () = Lemmas.save_named false @@ -232,18 +233,19 @@ let rec (find_call_occs : int -> int -> constr -> constr -> | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function") | Var(id) -> (fun l -> expr), [] - | Meta(_) -> error "find_call_occs : Meta" - | Evar(_) -> error "find_call_occs : Evar" + | Meta(_) -> error "Found a metavariable. Can not treat such a term" + | Evar(_) -> error "Found an evar. Can not treat such a term" | Sort(_) -> (fun l -> expr), [] | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b - | Prod(_,_,_) -> error "find_call_occs : Prod" + | Prod(na,t,b) -> + error "Found a product. Can not treat such a term" | Lambda(na,t,b) -> begin match find_call_occs nb_arg (succ nb_lam) f b with | _, [] -> (* Lambda are authorized as long as they do not contain recursives calls *) (fun l -> expr),[] - | _ -> error "find_call_occs : Lambda" + | _ -> error "Found a lambda which body contains a recursive call. Such terms are not allowed" end | LetIn(na,v,t,b) -> begin @@ -254,7 +256,7 @@ let rec (find_call_occs : int -> int -> constr -> constr -> ((fun l -> mkLetIn(na,v,t,cf l)),l) | (cf,(_::_ as l)),(_,[]) -> ((fun l -> mkLetIn(na,cf l,t,b)), l) - | _ -> error "find_call_occs : LetIn" + | _ -> error "Found a letin with recursive calls in both variable value and body. Such terms are not allowed." end | Const(_) -> (fun l -> expr), [] | Ind(_) -> (fun l -> expr), [] @@ -263,8 +265,8 @@ let rec (find_call_occs : int -> int -> constr -> constr -> (match find_call_occs nb_arg nb_lam f a with cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) | _ -> (fun l -> expr),[]) - | Fix(_) -> error "find_call_occs : Fix" - | CoFix(_) -> error "find_call_occs : CoFix";; + | Fix(_) -> error "Found a local fixpoint. Can not treat such a term" + | CoFix(_) -> error "Found a local cofixpoint : CoFix";; let coq_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" @@ -896,6 +898,20 @@ let build_and_l l = let conj_constr = coq_conj () in let mk_and p1 p2 = Term.mkApp(and_constr,[|p1;p2|]) in + let rec is_well_founded t = + match kind_of_term t with + | Prod(_,_,t') -> is_well_founded t' + | App(_,_) -> + let (f,_) = decompose_app t in + eq_constr f (well_founded ()) + | _ -> assert false + in + let compare t1 t2 = + let b1,b2= is_well_founded t1,is_well_founded t2 in + if (b1&&b2) || not (b1 || b2) then 0 + else if b1 && not b2 then 1 else -1 + in + let l = List.sort compare l in let rec f = function | [] -> failwith "empty list of subgoals!" | [p] -> p,tclIDTAC,1 @@ -1006,7 +1022,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) e_assumption; Eauto.eauto_with_bases - false (true,5) [Evd.empty,delayed_force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] @@ -1378,6 +1393,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = + let previous_label = Lib.current_command_label () in let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) @@ -1429,7 +1445,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly "Cannot create equation Lemma" ; -(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) stop := true; end end; @@ -1461,10 +1476,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); -(* anomaly "Cannot create termination Lemma" *) + (try ignore (Backtrack.backto previous_label) with _ -> ()); + (* anomaly "Cannot create termination Lemma" *) raise e end - - - |