diff options
| -rw-r--r-- | contrib/funind/indfun.ml | 21 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 81 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 1137 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.mli | 13 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 3 |
5 files changed, 508 insertions, 747 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index c1c835b92..fde269549 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -101,7 +101,8 @@ let prepare_body (name,annot,args,types,body) rt = (fun_args,rt') -let generate_principle fix_rec_l recdefs interactive_proof parametrize continue_proof = +let generate_principle fix_rec_l recdefs interactive_proof parametrize + (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) = let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -127,13 +128,17 @@ let generate_principle fix_rec_l recdefs interactive_proof parametrize continue let _ = Util.list_map_i (fun i x -> - New_arg_principle.generate_new_structural_principle + let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in + let princ_type = + (Global.lookup_constant princ).Declarations.const_type + in + New_arg_principle.generate_functional_principle interactive_proof - (destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp))) + princ_type None funs_kn i - (continue_proof i funs_kn) + (continue_proof 0 [|funs_kn.(i)|]) ) 0 fix_rec_l @@ -161,7 +166,7 @@ let register_struct is_rec fixpoint_exprl = let generate_correction_proof_wf tcc_lemma_ref is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.constant array) (_:int) : Tacmach.tactic = + (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = Recdef.prove_principle tcc_lemma_ref is_mes f_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -266,7 +271,7 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body = -let do_generate_principle fixpoint_exprl = +let do_generate_principle interactive_proof fixpoint_exprl = let recdefs = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with @@ -329,9 +334,9 @@ let do_generate_principle fixpoint_exprl = generate_principle fixpoint_exprl recdefs - false + interactive_proof true - (New_arg_principle.prove_princ_for_struct); + (New_arg_principle.prove_princ_for_struct interactive_proof); true in diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index f182c7997..5e4a95b10 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -48,6 +48,43 @@ TACTIC EXTEND newfuninv ] END + + +TACTIC EXTEND newfunind + ["new" "functional" "induction" constr(c) ] -> + [ + let f,args = decompose_app c in + let fname = + match kind_of_term f with + | Const c' -> + id_of_label (con_label c') + | _ -> Util.error "Must be used with a function" + in + fun g -> + let princ_name = + ( + Indrec.make_elimination_ident + fname + (Tacticals.elimination_sort_of_goal g) + ) + in + let princ = const_of_id princ_name in + let args_as_induction_constr = + List.map (fun c -> Tacexpr.ElimOnConstr c) (args@[c]) + in + let princ' = Some (mkConst princ,Rawterm.NoBindings) in + Tactics.new_induct args_as_induction_constr princ' Genarg.IntroAnonymous g +(* Tacticals.tclTHEN *) +(* (Hiddentac.h_reduce *) +(* (Rawterm.Pattern (List.map (fun e -> ([],e)) (frealargs@[c]))) *) +(* Tacticals.onConcl *) +(* ) *) +(* (Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings)) *) +(* g *) + ] +END + +(* TACTIC EXTEND newfunind ["new" "functional" "induction" constr(c) ] -> [ @@ -116,6 +153,10 @@ TACTIC EXTEND newfunind g ] END +*) + + + VERNAC ARGUMENT EXTEND rec_annotation2 [ "{" "struct" ident(id) "}"] -> [ Struct id ] @@ -173,5 +214,41 @@ END VERNAC COMMAND EXTEND GenFixpoint ["GenFixpoint" rec_definitions2(recsl)] -> - [ do_generate_principle recsl] - END + [ do_generate_principle false recsl] +END + +VERNAC COMMAND EXTEND IGenFixpoint + ["IGenFixpoint" rec_definitions2(recsl)] -> + [ do_generate_principle true recsl] +END + +VERNAC COMMAND EXTEND NewFunctionalScheme + ["New" "Functional" "Scheme" ident(name) ident_list(funs) "using" ident(scheme)] -> + [ + let id_to_constr id = + Tacinterp.constr_of_id (Global.env ()) id + in + let funs = + Array.of_list (List.map id_to_constr funs) + in + let scheme = id_to_constr scheme in + let scheme_type = Typing.type_of (Global.env ()) Evd.empty scheme in + New_arg_principle.generate_functional_principle false + scheme_type + (Some name) + (Array.map destConst funs) + 0 + (New_arg_principle.prove_princ_for_struct false 0 (Array.map destConst funs)) + + + +(* let res = New_arg_principle.compute_new_princ_type_from_rel *) +(* funs *) +(* scheme_type *) +(* in *) + +(* Pp.msgnl (str "result := "++Printer.pr_lconstr res++fnl ()) *) + + ] +END + diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml index 03eacea27..7696059e8 100644 --- a/contrib/funind/new_arg_principle.ml +++ b/contrib/funind/new_arg_principle.ml @@ -14,8 +14,14 @@ open Tacticals open Tactics open Indfun_common + (* let msgnl = Pp.msgnl *) +let observe strm = + if Tacinterp.get_debug () <> Tactic_debug.DebugOff + then Pp.msgnl strm + else () + let observe_tac s tac g = if Tacinterp.get_debug () <> Tactic_debug.DebugOff then Recdef.do_observe_tac s tac g @@ -174,194 +180,67 @@ let my_reflexivity : tactic = | _ -> tclFAIL 0 (str "") end g -let exactify_proof rec_pos ptes_to_fix : tactic = - let not_as_constant = Coqlib.build_coq_not () in - let or_as_ind = Coqlib.build_coq_or () in - let eq_not = eq_constr not_as_constant in - let eq_or = eq_constr or_as_ind in - let tac_res tac: tactic = - fun g -> - match kind_of_term (pf_concl g) with - | Prod _ -> tclTHEN intro tac g - | App(f,_) -> - if eq_not f - then tclTHEN (intro_force true) (tclABSTRACT None (Cctac.cc_tactic [])) - (* Equality.discr_tac None *) g - else if eq_or f - then - tclSOLVE - [tclTHEN simplest_left tac; - tclTHEN simplest_right tac - ] g - else - begin - match rec_pos with - | Some rec_pos -> - begin - match kind_of_term f with - | Var id -> - begin - try - let fix_id = Idmap.find id ptes_to_fix in - let fix = mkVar (fix_id) in - tclTHEN - (rewrite_until_var rec_pos) - (Eauto.e_resolve_constr fix) - g - with Not_found -> - (* Pp.msgnl (str "No fix found for "++ *) - (* pr_lconstr_env (pf_env g) f); *) - tclFAIL 0 (str "No such fix found") g - end - | _ -> - tclCOMPLETE - (Eauto. gen_eauto false (false,5) [] (Some [])) - (* (string_of_pp (pr_lconstr_env (pf_env g) f)) *) - g - end - | None -> - tclCOMPLETE (Eauto. gen_eauto false (false,5) [] (Some [])) g - - end - | _ -> tclFAIL 0 (str "Not a good term") g - in - let rec exactify_proof g = - tclFIRST - [ - tclSOLVE [my_reflexivity]; - tclSOLVE [Eauto.e_assumption]; - tclSOLVE [Tactics.reflexivity ]; - tac_res exactify_proof; - tclCOMPLETE - ( - tclREPEAT - ( - tclPROGRESS - (tclTHEN - (rew_all LR) - (Eauto. gen_eauto false (false,5) [] (Some [])) - ) - ) - ) - ] g - in - observe_tac "exactify_proof with " exactify_proof - +let eauto g = + tclFIRST + [ + Eauto.e_assumption + ; + h_exact (Coqlib.build_coq_I ()); + tclTHEN + (rew_all LR) + (Eauto. gen_eauto false (false,5) [] (Some [])) + ] + g -let reduce_fname fnames : tactic = - let do_reduce : tactic = reduce - (Rawterm.Lazy - { Rawterm.rBeta = true; - Rawterm.rIota = true; - Rawterm.rZeta = true; - Rawterm.rDelta = false; - Rawterm.rConst = List.map (fun f -> EvalConstRef f) fnames - } + + +let conclude fixes g = +(* let clear_fixes = *) +(* let l = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *) +(* h_clear false l *) +(* in *) + match kind_of_term (pf_concl g) with + | App(pte,args) -> + let tac = + if isVar pte + then + try + let idxs,body,this_fix_id,new_type = Idmap.find (destVar pte) fixes + in + let idx = idxs - 1 in + tclTHEN + (rewrite_until_var idx) + (* If we have an IH then with use the fixpoint *) + (Eauto.e_resolve_constr (mkVar this_fix_id)) + (* And left the generated subgoals to eauto *) + with Not_found -> (* this is not a pte *) + tclIDTAC + else tclIDTAC + in + tclTHENSEQ [tac; (* clear_fixes; *) eauto] g + | _ -> eauto g + + +let finalize_proof interactive_proof fixes hyps fnames term = + tclORELSE + ( + tclFIRST + (List.map + (fun id -> tclTHEN (Eauto.e_resolve_constr (mkVar id)) + (tclCOMPLETE (conclude fixes))) hyps + ) ) - onConcl - in - let refold : tactic = - reduce - (Rawterm.Fold (List.map mkConst fnames)) - onConcl - - in - fun g -> -(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) -(* then msgnl (str "reduce_fname"); *) - tclTHENSEQ - [do_reduce; - refold ; - (tclREPEAT (tclPROGRESS (rew_all LR))) - ] - g + (if interactive_proof then tclIDTAC else tclFAIL 0 (str "")) + + -let h_exact ?(with_rew_all=false) c :tactic = - observe_tac "h_exact " (exact_check c ) - - -let finalize_proof rec_pos fixes (hyps:identifier list) = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then - Pp.msgnl (str "rec hyps are : " ++ - prlist_with_sep spc Ppconstr.pr_id hyps); - let exactify_proof = exactify_proof rec_pos fixes in - - let exactify_proof_with_id id : tactic = - let do_exactify_proof_with_id = - fun g -> - let res = - tclTHEN - (Eauto.e_resolve_constr (mkVar id)) - (tclTRY exactify_proof) - - in - tclTHEN - res - ((h_exact (Coqlib.build_coq_I ()))) - g - in - fun g -> observe_tac "exactify_proof_with_id" do_exactify_proof_with_id g - in - let apply_one_hyp hyp acc = - tclORELSE - ( exactify_proof_with_id hyp) - acc - in - let apply_one_hyp_with_rewall hyp acc = - tclORELSE - (tclTHEN - (rew_all RL) - (exactify_proof_with_id hyp) - ) - - acc - in - let apply_hyps = - tclTRYD( - (List.fold_right - apply_one_hyp - hyps - (List.fold_right - apply_one_hyp_with_rewall - hyps - (tclFAIL 0 (str "No rec hyps found ") ) - ) - )) - in - let finalize_proof fnames t : tactic = - let change_tac tac g = - match kind_of_term ( pf_concl g) with - | App(p,args) -> - let nargs = Array.length args in - begin - tclTHENS - (try Equality.replace (args.(nargs -1)) t - with _ -> - tclFAIL 0 (str "") - ) - [tac; - tclTRY (tclTHEN (reduce_fname fnames) ( (Tactics.reflexivity))) - ] - g - end - | _ -> assert false - in - fun g -> -(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) -(* then *) -(* msgnl (str "finalize with body "++ Printer.pr_lconstr t ++ *) -(* str " on goal "++ Printer.pr_goal (sig_it g)); *) - (change_tac apply_hyps) g - in - finalize_proof -let do_prove_princ_for_struct - (rec_pos:int option) (fnames:constant list) - (ptes:identifier list) (fixes:identifier Idmap.t) (hyps: identifier list) +let do_prove_princ_for_struct interactive_proof + (* (rec_pos:int option) *) (fnames:constant list) + (ptes:identifier list) (fixes:(int*constr*identifier*constr) Idmap.t) (hyps: identifier list) (term:constr) : tactic = let finalize_proof term = - finalize_proof rec_pos fixes hyps fnames term + finalize_proof (* rec_pos *) interactive_proof fixes hyps fnames term in let rec do_prove_princ_for_struct do_finalize term g = (* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) @@ -400,7 +279,7 @@ let do_prove_princ_for_struct | Const _ -> do_finalize term g | _ -> - warning "Applied binders not yet implemented"; + msg_warning (str "Applied binders not yet implemented: "++ Printer.pr_lconstr_env (pf_env g) term) ; tclFAIL 0 (str "TODO") g end | Fix _ | CoFix _ -> @@ -450,395 +329,207 @@ let is_pte_type t = let is_pte (_,_,t) = is_pte_type t -let prove_princ_for_struct fun_num f_names nparams : tactic = - let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in - let fbody = - match (Global.lookup_constant f_names.(fun_num)).const_body with - | Some b -> - let body = force b in - Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) - body - | None -> error ( "Cannot define a principle over an axiom ") - in - let rec_arg_num,fbody = - match kind_of_term fbody with - | Fix((idxs,fix_num),(_,_,ca)) -> - begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end - | b -> None,fbody - in - let f_real_args = nb_lam fbody - nparams in - let test_goal_for_hyps g = - let goal_nb_prod = nb_prod (pf_concl g) in - goal_nb_prod = f_real_args - in - let test_goal_for_args g = - let goal_nb_prod = nb_prod (pf_concl g) in - goal_nb_prod < 1 - in - let rec intro_params tac params n : tactic = - if n = 0 - then tac params - else - tclTHEN - (intro) - (fun g -> - let (id,_,_) = pf_last_hyp g in - intro_params tac (id::params) (n-1) g - ) - in - let rec intro_pte tac ptes : tactic = - tclTHEN - intro - (fun g -> - let (id,_,_) as pte = pf_last_hyp g in - if is_pte pte - then intro_pte tac (id::ptes) g - else - tclTHENSEQ - [ h_generalize [(mkVar id)]; - clear [id]; - tac ptes - ] - g - ) - in - let rec intro_hyps tac hyps : tactic = - fun g -> - if test_goal_for_hyps g - then tac hyps g - else - tclTHEN - intro - (fun g' -> - let (id,_,_) = pf_last_hyp g' in - intro_hyps tac (id::hyps) g' - ) - g - in - let do_fix ptes tac : tactic = - match rec_arg_num with - | None -> tac (Idmap.empty) - | Some fix_arg_num -> - fun g -> - let this_fix_id = (fresh_id (pf_ids_of_hyps g) "fix___") in - let ptes_to_fix = - List.fold_left2 - (fun acc pte fix -> - Idmap.add pte fix acc - ) - Idmap.empty - ptes - [this_fix_id] - in - tclTHEN - (h_mutual_fix this_fix_id (fix_arg_num +1) []) - (tac ptes_to_fix) - g - in - let rec intro_args tac args : tactic = - fun g -> - if test_goal_for_args g - then tac args g - else - tclTHEN - intro - (fun g' -> - let (id,_,_) = pf_last_hyp g' in - intro_args tac (id::args) g' - ) - g - in - let intro_tacs tac : tactic = - fun g -> -(* msgnl (str "introducing params"); *) - intro_params - (fun params -> -(* msgnl (str "introducing properties"); *) - intro_pte - (fun ptes -> -(* msgnl (str "introducing rec hyps"); *) - intro_hyps - (fun hyps -> -(* msgnl (str "creating fixes"); *) - do_fix ptes - (fun ptes_to_fix -> -(* msgnl (str "introducing args"); *) - intro_args - (fun args -> -(* tclTHEN *) -(* (reduce_fname (Array.to_list f_names)) *) - (tac params ptes ptes_to_fix hyps args)) - [] - ) - ) - [] +exception Not_Rec + +let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : tactic = + fun goal -> + observe (str "Proving principle for "++ str (string_of_int fun_num) ++ str "th function : " ++ + Printer.pr_lconstr (mkConst fnames.(fun_num))); + let princ_type = pf_concl goal in + let princ_info = compute_elim_sig princ_type in + let get_body const = + match (Global.lookup_constant const ).const_body with + | Some b -> + let body = force b in + Tacred.cbv_norm_flags + (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (Global.env ()) + (Evd.empty) + body + | None -> error ( "Cannot define a principle over an axiom ") + in + let fbody = get_body fnames.(fun_num) in + let params : identifier list ref = ref [] in + let predicates : identifier list ref = ref [] in + let args : identifier list ref = ref [] in + let branches : identifier list ref = ref [] in + let pte_to_fix = ref Idmap.empty in + let fbody_with_params = ref None in + let intro_with_remembrance ref number : tactic = + tclTHEN + ( tclDO number intro ) + (fun g -> + let last_n = list_chop number (pf_hyps g) in + ref := List.map (fun (id,_,_) -> id) (fst last_n)@ !ref; + tclIDTAC g + ) + in + let rec partial_combine body params = + match kind_of_term body,params with + | Lambda (x,t,b),param::params -> + partial_combine (subst1 param b) params + | Fix(infos),_ -> + body,params, Some (infos) + | _ -> body,params,None + in + let build_pte_to_fix (offset:int) params predicates + ((idxs,fix_num),(na,typearray,ca)) (avoid,_) = +(* let true_params,_ = list_chop offset params in *) + let true_params = List.rev params in + let avoid = ref avoid in + let res = list_fold_left_i + (fun i acc id -> + let this_fix_id = fresh_id !avoid "fix___" in + avoid := this_fix_id::!avoid; +(* let this_body = substl (List.rev fnames_as_constr) ca.(i) in *) + let this_body = substl (List.rev (Array.to_list all_funs)) ca.(i) in + let new_type = prod_applist typearray.(i) true_params + and new_body = Reductionops.nf_beta (applist(this_body,true_params)) in + let fix_info = idxs.(i) - offset + 1,new_body,this_fix_id ,new_type in + pte_to_fix := Idmap.add id fix_info !pte_to_fix; + fix_info::acc + ) + 0 + [] + (List.rev predicates) + in + !avoid,List.rev res + in + let mk_fixes : tactic = + fun g -> + let body_p,params',fix_infos = + partial_combine fbody (List.rev_map mkVar !params) + in + fbody_with_params := Some body_p; + let offset = List.length params' in + let not_real_param,true_params = + list_chop + ((List.length !params ) - offset) + !params + in + params := true_params; args := not_real_param; + observe (str "mk_fixes : params are "++ + prlist_with_sep spc + (fun id -> Printer.pr_lconstr (mkVar id)) + !params + ); + let new_avoid,infos = + option_fold_right + (build_pte_to_fix + offset + (List.map mkVar !params) + (List.rev !predicates) ) - [] - ) - [] - nparams - g - in - let apply_fbody g params args = -(* msgnl (str "applying fbody"); *) - let args' = List.rev_map mkVar args in - let f_args = - List.fold_left (fun acc p -> (mkVar p)::acc) args' params - in - let app_f = applist(subst1 (mkConst f_names.(fun_num)) fbody,f_args) in -(* Pp.msgnl (pr_lconstr_env (pf_env g) app_f); *) - pf_nf_betaiota g app_f - in - let prepare_goal_tac tac : tactic = - intro_tacs - (fun params ptes ptes_to_fix hyps args g -> - let app_f = apply_fbody g params args in -(* msgnl (str "proving"); *) - match rec_arg_num with - Some rec_arg_num -> - let actual_args = - List.fold_left (fun y x -> x::y) - (List.rev args) - params + fix_infos + ((pf_ids_of_hyps g),[]) + in + let pre_info,infos = list_chop fun_num infos in + match pre_info,infos with + | [],[] -> tclIDTAC g + | _,(idx,_,fix_id,_)::infos' -> + let other_fix_info = + List.map (fun (idx,_,fix_id,fix_typ) -> fix_id,idx,fix_typ) (pre_info@infos') in - let to_replace = - applist(mkConst f_names.(fun_num),List.map mkVar actual_args) in - - tclTHENS - (Equality.replace - to_replace - app_f - ) - [ - tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f; - let id = List.nth (List.rev args) (rec_arg_num ) in - (tclTHENSEQ - [(h_simplest_case (mkVar id)); - tclTRY Tactics.intros_reflexivity - ] - ) -(* Tactics.reflexivity) *) - ] - g - | None -> - tclTHEN - (reduce_fname (Array.to_list f_names)) - (tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f) + tclORELSE + (h_mutual_fix fix_id idx other_fix_info) + (tclFAIL 1000 (str "bad index" ++ str (string_of_int idx) ++ + str "offset := " ++ + (str (string_of_int offset)))) g - -(* tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g *) - ) - in - prepare_goal_tac (fun g -> do_prove_princ_for_struct rec_arg_num g) - - - -(* let case_eq term : tactic = *) -(* fun g -> *) -(* let type_of_term = pf_type_of g term in *) -(* let eq_proof_term = *) -(* let refl_equal_term = Lazy.force refl_equal in *) -(* mkApp(refl_equal_term,[|type_of_t;t|]) *) -(* in *) -(* let ba_fun ba = *) -(* tclDO ba.nassums h_intro *) -(* in *) -(* tclTHENSEQ *) -(* [ *) -(* h_generalize [eq_proof_term]; *) -(* pattern_option [[-1],term] None; *) -(* case_then_using Genarg.IntroAnonymous ba_fun term None ([],[]) term *) -(* ] *) -(* g *) - - -(* let heq_id = id_of_string "Heq" *) - -(* let do_prove_princ_for_struct *) -(* predicates_ids ptes_to_fix branches_ids params_ids args_ids rec_arg_num = *) -(* let rec do_prove_princ_for_struct eqs_id term = *) -(* match kind_of_term term with *) -(* | Case(_,_,t,_) -> *) -(* tclTHEN *) -(* (case_eq t) *) -(* (fun g -> *) -(* let heq = fresh_id (pf_ids_of_hyps g) heq in *) -(* tclTHEN *) -(* (h_intro heq) *) -(* (fun g' -> *) -(* let new_t_value = *) -(* match kind_of_term (pf_type_of g' (mkVar heq)) with *) -(* | App(_,[|_;_;value|]) -> value *) -(* | _ -> anomaly "should have been an equality" *) -(* in *) -(* let type_of_t = pf_type_of g' t in *) -(* let term_as_fun = *) -(* mkLambda(Anonymous,type_of_t, *) -(* replace_term term (mkRel 1) term *) -(* ) *) -(* in *) -(* let new_term = *) -(* pf_nf_betaiota g' (mkApp(term_as_fun,new_t_value)) *) -(* in do_prove_princ_for_struct (heq::eqs_id) new_term g' *) -(* ) *) -(* ) *) -(* | Lambda(n,t,b) -> *) -(* begin *) -(* match kind_of_term( pf_concl g) with *) -(* | Prod _ -> *) + | _,[] -> anomaly "Not a valid information" + in + let do_prove pte_to_fix args : tactic = + fun g -> + match kind_of_term (pf_concl g) with + | App(pte,pte_args) when isVar pte -> + begin + let pte = destVar pte in + try + let (_idx,_new_body,_this_fix_id,_new_type) = + try Idmap.find pte pte_to_fix with _ -> raise Not_Rec + in + let nparams = List.length !params in + let args_as_constr = List.map mkVar args in + let rec_num,new_body = + let idx' = list_index pte !predicates - 1 in + let f = fnames.(idx') in + let body_with_params = match !fbody_with_params with Some f -> f | _ -> anomaly "" + in + let name_of_f = Name ( id_of_label (con_label f)) in + let ((rec_nums,_),(na,_,bodies)) = destFix body_with_params in + let idx'' = list_index name_of_f (Array.to_list na) - 1 in + let body = substl (List.rev (Array.to_list all_funs)) bodies.(idx'') in + let body = Reductionops.nf_beta (applist(body,(List.rev_map mkVar !params))) in + rec_nums.(idx'') - nparams ,body + in + let applied_body = + Reductionops.nf_beta + (applist(new_body,List.rev args_as_constr)) + in + let do_prove = + do_prove_princ_for_struct + interactive_proof + (Array.to_list fnames) + !predicates + pte_to_fix + !branches + applied_body + in + let replace_and_prove = + tclTHENS + (fun g -> + observe (str "replacing " ++ + Printer.pr_lconstr_env (pf_env g) (array_last pte_args) ++ + str " with " ++ + Printer.pr_lconstr_env (pf_env g) applied_body ++ + str " rec_arg_num is " ++ str (string_of_int rec_num) + ); + Equality.replace (array_last pte_args) applied_body g + ) + [ + do_prove; + try + let id = List.nth (List.rev args_as_constr) (rec_num) in + observe (str "choosen var := "++ Printer.pr_lconstr id); + (tclTHENSEQ + [(h_simplest_case id); + Tactics.intros_reflexivity + ]) + with _ -> tclIDTAC + + ] + in (* tclTHEN *) -(* intro *) -(* (fun g' -> *) -(* let (id,_,_) = pf_last_hyp g' in *) -(* let new_term = pf_nf_betaiota g' (mkApp(term,[|mkVar id|])) *) -(* in *) -(* do_prove_princ_for_struct do_finalize eqs_id new_term g' *) -(* ) *) -(* | _ -> *) -(* do_finalize eqs_id term *) -(* end *) -(* | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize eqs_id t *) -(* | Fix _ | CoFix _ -> *) -(* error ( "Anonymous local (co)fixpoints are not handled yet") *) -(* | LetIn (Name id,v,t,b) -> *) -(* do_prove_princ_for_struct do_finalize (subst1 v b) g *) -(* | LetIn(Anonymous,_,_,b) -> *) -(* do_prove_princ_for_struct do_finalize (pop b) g *) -(* | Prod _ -> assert false *) -(* | *) -(* in *) -(* do_prove_princ_for_struct [] *) - - - - -(* let fresh_id_from_name avoid na = *) -(* match get_name avoid na with *) -(* | Name id -> id *) -(* | _ -> assert false *) - - -(* let fresh_ids (acces_fun: 'a -> name) (l: 'a list)(avoid : identifier list) = *) -(* let rev_ids,avoid = *) -(* List.fold_left *) -(* (fun (rev_ids,avoid) e -> *) -(* let old_name = acces_fun e in *) -(* let new_id = fresh_id_from_name avoid old_name in *) -(* new_id::rev_ids,new_id::avoid *) -(* ) *) -(* ([],avoid) *) -(* l *) -(* in *) -(* List.rev rev_ids,avoid *) - -(* let fst' (x,_,_) = x *) - -(* let prove_princ_for_struct fun_num f_names nparams : tactic = *) -(* fun g -> *) -(* let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in *) -(* let fbody = *) -(* match (Global.lookup_constant f_names.(fun_num)).const_body with *) -(* | Some b -> *) -(* let body = force b in *) -(* Tacred.cbv_norm_flags *) -(* (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) *) -(* (Global.env ()) *) -(* (Evd.empty) *) -(* body *) -(* | None -> error ( "Cannot define a principle over an axiom ") *) -(* in *) -(* let rec_arg_num,fbody = *) -(* match kind_of_term fbody with *) -(* | Fix((idxs,fix_num),(_,_,ca)) -> *) -(* begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end *) -(* | b -> None,fbody *) -(* in *) -(* let goal_info = compute_elim_sig (mkRel 0,Rawterm.NoBindings) (pf_concl g) in *) -(* let params_ids,to_avoid = fresh_ids fst' goal_info.Tactics.params [] in *) -(* let predicates_ids,to_avoid = fresh_ids fst' goal_info.predicates to_avoid in *) -(* let branches_ids,to_avoid = fresh_ids fst' goal_info.branches to_avoid in *) -(* let first_intros : tactic = *) -(* tclMAP h_intro (params_ids@predicates_ids@branches_ids) *) -(* in *) -(* let fix_id,to_avoid,fix_tac = *) -(* match rec_arg_num with *) -(* | None -> None,to_avoid,first_intros *) -(* | Some fix_arg_num -> *) -(* let this_fix_id = (fresh_id to_avoid "fix___") in *) -(* Some this_fix_id,this_fix_id::to_avoid, *) -(* tclTHEN *) -(* first_intros *) -(* (h_mutual_fix this_fix_id (fix_arg_num +1) []) *) -(* in *) -(* let ptes_to_fix = *) -(* List.fold_left2 *) -(* (fun acc pte fix -> *) -(* Idmap.add pte fix acc *) -(* ) *) -(* Idmap.empty *) -(* predicates_ids *) -(* [fix_id] *) -(* in *) -(* let args_ids,to_avoid = fresh_ids fst' goal_info.args to_avoid in *) -(* let (tac_replace,term : tactic*constr) = *) -(* let eqs_rhs = *) -(* let fbody_with_funs = *) -(* substl (List.rev_map mkConst (Array.to_list f_names)) fbody *) -(* in *) -(* applist (fbody_with_funs, (List.map mkVar (params_ids@args_ids))) *) -(* in *) -(* match rec_arg_num with *) -(* | Some rec_arg_num -> *) -(* let eqs_lhs = *) -(* applist(mkConst f_names.(fun_num),List.map mkVar args_ids) *) -(* in *) -(* tclTHENS *) -(* (Equality.replace eqs_lhs eqs_rhs) *) -(* [ *) -(* tclIDTAC (\* The proof continue in this branche *\) *) -(* ; *) -(* (\* Not in this one *\) *) -(* let id = List.nth (List.rev args_ids) (rec_arg_num ) in *) -(* tclCOMPLETE *) -(* (tclTHENSEQ *) -(* [(h_simplest_case (mkVar id)); *) -(* Tactics.intros_reflexivity *) -(* ]) *) -(* ],eqs_rhs *) -(* | None -> *) -(* unfold_in_concl *) -(* (Array.to_list (Array.map (fun x -> [],EvalConstRef x) f_names)), *) -(* eqs_rhs *) -(* in *) -(* tclTHENSEQ *) -(* [ *) -(* fix_tac; *) -(* tclMAP h_intro args_ids; *) -(* tac_replace; *) -(* do_prove_princ_for_struct *) -(* predicates_ids *) -(* ptes_to_fix *) -(* branches_ids *) -(* params_ids *) -(* args_ids *) -(* rec_arg_num *) -(* term *) -(* ] *) - - - - - - - - - - - - + (observe_tac "doing replacement" replace_and_prove) + g + with Not_Rec -> + let fname = destConst (fst (decompose_app (array_last pte_args))) in + tclTHEN + (unfold_in_concl [([],Names.EvalConstRef fname)]) + (observe_tac "" (fun g' -> + do_prove_princ_for_struct + interactive_proof + (Array.to_list fnames) + !predicates + pte_to_fix + !branches + (array_last (snd (destApp (pf_concl g')))) + g' + )) + g + end + | _ -> assert false + in + tclTHENSEQ + [ + (fun g -> observe_tac "introducing params" (intro_with_remembrance params princ_info.nparams) g); + (fun g -> observe_tac "introducing predicate" (intro_with_remembrance predicates princ_info.npredicates) g); + (fun g -> observe_tac "introducing branches" (intro_with_remembrance branches princ_info.nbranches) g); + (fun g -> observe_tac "declaring fix(es)" mk_fixes g); + (fun g -> observe_tac "introducing args" (intro_with_remembrance args princ_info.nargs) g); + (fun g -> observe_tac "proving" (fun g -> do_prove !pte_to_fix !args g) g) + ] + goal @@ -847,24 +538,56 @@ let prove_princ_for_struct fun_num f_names nparams : tactic = + + - + exception Toberemoved_with_rel of int*constr exception Toberemoved -let prov_pte_prefix = "_____PTE" - - - -let is_pte_id = - let pref_length = String.length prov_pte_prefix in - function id -> - String.sub (string_of_id id) 0 pref_length = prov_pte_prefix - -let compute_new_princ_type_from_rel replace - (rel_as_kn:mutual_inductive) = +let compute_new_princ_type_from_rel rel_to_fun princ_type = + let princ_type_info = compute_elim_sig princ_type in + let env = Global.env () in + let type_sort = (Termops.new_sort_in_family InType) in + let change_predicate_sort (x,_,t) = + let args,_ = decompose_prod t in + let real_args = + if princ_type_info.indarg_in_concl + then List.tl args + else args + in + x,None,compose_prod real_args (mkSort type_sort) + in + let new_predicates = List.map change_predicate_sort princ_type_info.predicates in + let env_with_params_and_predicates = + Environ.push_rel_context + new_predicates + (Environ.push_rel_context + princ_type_info.params + env + ) + in + let rel_as_kn = + fst (match princ_type_info.indref with + | Some (Libnames.IndRef ind) -> ind + | _ -> failwith "Not a valid predicate" + ) + in + let pre_princ = + it_mkProd_or_LetIn + ~init: + (it_mkProd_or_LetIn + ~init:(option_fold_right + mkProd_or_LetIn + princ_type_info.indarg + princ_type_info.concl + ) + princ_type_info.args + ) + princ_type_info.branches + in let is_dom c = match kind_of_term c with | Ind((u,_)) -> u = rel_as_kn @@ -879,7 +602,7 @@ let compute_new_princ_type_from_rel replace in let dummy_var = mkVar (id_of_string "________") in let mk_replacement i args = - mkApp(replace.(i),Array.map pop (array_get_start args)) + mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in let rec has_dummy_var t = fold_constr @@ -887,53 +610,63 @@ let compute_new_princ_type_from_rel replace false t in - let rec compute_new_princ_type env pre_princ : types*(constr list) = -(* let _tim1 = Sys.time() in *) + let rec compute_new_princ_type remove env pre_princ : types*(constr list) = let (new_princ_type,_) as res = match kind_of_term pre_princ with | Rel n -> begin - match Environ.lookup_rel n env with + try match Environ.lookup_rel n env with | _,_,t when is_dom t -> raise Toberemoved - | _ -> pre_princ,[] + | _ -> pre_princ,[] with Not_found -> assert false end | Prod(x,t,b) -> - compute_new_princ_type_for_binder mkProd env x t b + compute_new_princ_type_for_binder remove mkProd env x t b | Lambda(x,t,b) -> - compute_new_princ_type_for_binder mkLambda env x t b + compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> let var_to_be_removed = destRel (array_last args) in let num = get_fun_num f in raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement num args)) | App(f,args) -> + let is_pte = + match kind_of_term f with + | Rel n -> + is_pte (Environ.lookup_rel n env) + | _ -> false + in + let args = + if is_pte && remove + then array_get_start args + else args + in let new_args,binders_to_remove = - Array.fold_right (compute_new_princ_type_with_acc env) + Array.fold_right (compute_new_princ_type_with_acc remove env) args ([],[]) in - let new_f,binders_to_remove_from_f = compute_new_princ_type env f in + let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in mkApp(new_f,Array.of_list new_args), list_union_eq eq_constr binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin env x v t b + compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in (* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) (* then *) -(* msgnl (str "compute_new_princ_type for "++ *) +(* Pp.msgnl (str "compute_new_princ_type for "++ *) (* pr_lconstr_env env pre_princ ++ *) (* str" is "++ *) (* pr_lconstr_env env new_princ_type); *) res - and compute_new_princ_type_for_binder bind_fun env x t b = + and compute_new_princ_type_for_binder remove bind_fun env x t b = begin try - let new_t,binders_to_remove_from_t = compute_new_princ_type env t in + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_x : name = get_name (ids_of_context env) x in let new_env = Environ.push_rel (x,None,t) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type new_env b in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b else @@ -948,21 +681,21 @@ let compute_new_princ_type_from_rel replace with | Toberemoved -> (* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [dummy_var] 1 b) in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [c] n b) in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end - and compute_new_princ_type_for_letin env x v t b = + and compute_new_princ_type_for_letin remove env x v t b = begin try - let new_t,binders_to_remove_from_t = compute_new_princ_type env t in - let new_v,binders_to_remove_from_v = compute_new_princ_type env v in + let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in + let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in let new_x : name = get_name (ids_of_context env) x in let new_env = Environ.push_rel (x,Some v,t) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type new_env b in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b else @@ -977,174 +710,115 @@ let compute_new_princ_type_from_rel replace with | Toberemoved -> (* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [dummy_var] 1 b) in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [c] n b) in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end - and compute_new_princ_type_with_acc env e (c_acc,to_remove_acc) = - let new_e,to_remove_from_e = compute_new_princ_type env e + and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = + let new_e,to_remove_from_e = compute_new_princ_type remove env e in new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc in - compute_new_princ_type +(* Pp.msgnl (Printer.pr_lconstr_env env_with_params_and_predicates pre_princ); *) + let pre_res,_ = + compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in + it_mkProd_or_LetIn + ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates) + princ_type_info.params + + -let change_property_sort nparam toSort princ princName = - let params,concl = decompose_prod_n nparam princ in - let hyps,_ = decompose_prod concl in - let rec f l = - match l with - [] -> assert false - | (nme,typ)::l' -> - if is_pte_type typ then (nme,typ)::(f l') - else [] in - let args' = List.rev (f (List.rev hyps)) in - let args = - List.map - (function nme,typ -> - let arg,_ = decompose_prod typ in - nme, compose_prod arg (mkSort toSort) - ) args' - in - let nargs = List.length args + nparam in - let princName' = - Nametab.locate_constant - (snd (Libnames.qualid_of_reference (Libnames.Ident (Util.dummy_loc,princName)))) - in - let res = - compose_lam - params - (compose_lam args - (mkApp (mkConst princName',Array.init nargs - (fun i -> mkRel (nargs -i))))) +let change_property_sort toSort princ princName = + let princ_info = compute_elim_sig princ in + let change_sort_in_predicate (x,v,t) = + (x,None, + let args,_ = decompose_prod t in + compose_prod args (mkSort toSort) + ) in - res - -let prov_pte_prefix = "_____PTE" + let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in + let init = + let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in + mkApp(princName_as_constr, + Array.init nargs + (fun i -> mkRel (nargs - i ))) + in + it_mkLambda_or_LetIn + ~init: + (it_mkLambda_or_LetIn ~init + (List.map change_sort_in_predicate princ_info.predicates) + ) + princ_info.params + -let generate_new_structural_principle +let generate_functional_principle interactive_proof - old_princ new_princ_name funs i proof_tac + old_princ_type new_princ_name funs i proof_tac = let type_sort = (Termops.new_sort_in_family InType) in let f = funs.(i) in (* First we get the type of the old graph principle *) - let old_princ_type = (Global.lookup_constant old_princ).const_type - in - (* We split it into arguments and conclusion *) - let old_princ_hyps,old_princ_concl = decompose_prod old_princ_type in - (* We split the conclusion which must looks like - P x1 .... xn - *) - let p,pargs = decompose_app old_princ_concl in - if pargs = [] - then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme"); - (* The principle must as least have P as an argument *) - if old_princ_hyps = [] - then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme"); - (* The last argument of old_princ looks like: - (R_f x1 ... xn) - *) - let (_,r_app) = List.hd old_princ_hyps in - let rel,rel_args = decompose_app r_app in - if rel_args = [] || not (isInd rel) - then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme"); - let (mutr_as_kn,r_num) = destInd rel in - (* we can the compute the new_principle type *) - let mutr_def = Global.lookup_mind mutr_as_kn in - let mutr_nparams = mutr_def.mind_nparams in - let mutr_params,old_princ_type' = - decompose_prod_n mutr_nparams old_princ_type - in - let env_with_param = - Environ.push_rel_context - (List.map (fun (n,t) -> (n,None,t)) mutr_params) - (Global.env ()) - in - let pte_context,pte_prod,old_princ_type'' = - let rec f (acc_context,acc_prod) avoid c = - try - let (n,t,c') = destProd c - in - if is_pte_type t - then - let t' = - let args,concl = decompose_prod t in compose_prod args (mkSort type_sort) - in - let pte_id = fresh_id avoid prov_pte_prefix in - f ((Name pte_id,None,t)::acc_context,(n,t')::acc_prod) (pte_id::avoid) c' - else acc_context,acc_prod,c - with Invalid_argument _ -> acc_context,acc_prod,c - in - f ([],[]) (ids_of_context env_with_param) old_princ_type' - in - let env_with_ptes = Environ.push_rel_context pte_context env_with_param in -(* let tim1 = Sys.time () in *) - let new_principle_type,_ = - compute_new_princ_type_from_rel + let mutr_nparams = (compute_elim_sig old_princ_type).nparams in + (* First we get the type of the old graph principle *) + let new_principle_type = + compute_new_princ_type_from_rel (Array.map mkConst funs) - mutr_as_kn - env_with_ptes - old_princ_type'' - in + old_princ_type + in (* let tim2 = Sys.time () in *) (* Pp.msgnl (str ("Time to compute type: ") ++ str (string_of_float (tim2 -. tim1))) ; *) - let new_principle_type = - compose_prod mutr_params - (compose_prod pte_prod new_principle_type) - in (* msgnl (str "new principle type :"++ pr_lconstr new_principle_type); *) - let new_princ_name = - match new_princ_name with + let new_princ_name = + match new_princ_name with | Some (id) -> id - | None -> + | None -> let id_of_f = id_of_label (con_label f) in Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in - let hook _ _ = + let hook _ _ = let id_of_f = id_of_label (con_label f) in - let register_with_sort fam_sort = - let s = Termops.new_sort_in_family fam_sort in - let name = Indrec.make_elimination_ident id_of_f fam_sort in - let value = - change_property_sort mutr_nparams s new_principle_type new_princ_name - in - let ce = + let register_with_sort fam_sort = + let s = Termops.new_sort_in_family fam_sort in + let name = Indrec.make_elimination_ident id_of_f fam_sort in + let value = + change_property_sort s new_principle_type new_princ_name + in +(* Pp.msgnl (str "new principle := " ++ Printer.pr_lconstr value); *) + let ce = { const_entry_body = value; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() + const_entry_boxed = Options.boxed_definitions() } in ignore( - Declare.declare_constant - name - (Entries.DefinitionEntry ce, + Declare.declare_constant + name + (Entries.DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme) ) ) in - register_with_sort InProp; - register_with_sort InSet + register_with_sort InSet; + register_with_sort InProp in begin - Command.start_proof + Command.start_proof new_princ_name - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type hook ; - try + try (* let tim1 = Sys.time () in *) - Pfedit.by (proof_tac mutr_nparams); + Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); (* let tim2 = Sys.time () in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float (tim2 -. tim1))); *) - - if Tacinterp.get_debug () = Tactic_debug.DebugOff && not interactive_proof - then - Options.silently Command.save_named false; + let do_save = Tacinterp.get_debug () = Tactic_debug.DebugOff && not interactive_proof in + if do_save then Options.silently Command.save_named false (* let tim3 = Sys.time () in *) @@ -1152,17 +826,16 @@ let generate_new_structural_principle with | e -> - if Tacinterp.get_debug () = Tactic_debug.DebugOff - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end - else - msg_warning - ( - Cerrors.explain_exn e - ) - + msg_warning + ( + Cerrors.explain_exn e + ); + if Tacinterp.get_debug () = Tactic_debug.DebugOff + then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end end + diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli index 12325668c..eedc1d9dc 100644 --- a/contrib/funind/new_arg_principle.mli +++ b/contrib/funind/new_arg_principle.mli @@ -1,9 +1,9 @@ -val generate_new_structural_principle : +val generate_functional_principle : (* do we accept interactive proving *) bool -> (* induction principle on rel *) - Names.constant -> + Term.types -> (* Name of the new principle *) (Names.identifier) option -> (* the compute functions to use *) @@ -13,11 +13,16 @@ val generate_new_structural_principle : (* The tactic to use to make the proof w.r the number of params *) - (int -> Tacmach.tactic) -> + (Term.constr array -> int -> Tacmach.tactic) -> unit (* val my_reflexivity : Tacmach.tactic *) -val prove_princ_for_struct : int -> Names.constant array -> int -> Tacmach.tactic +val prove_princ_for_struct : + bool -> + int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic + + +val compute_new_princ_type_from_rel : Term.constr array -> Term.types -> Term.types diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 5bf0744d5..f97354845 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1111,7 +1111,8 @@ let (com_eqn : identifier -> Command.save_named true);; -let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle : unit = +let recursive_definition is_mes f type_of_f r rec_arg_num eq + generate_induction_principle : unit = let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_rel (Name f,None,function_type) (Global.env()) in let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in |