diff options
Diffstat (limited to 'contrib/funind/new_arg_principle.ml')
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 1770 |
1 files changed, 1770 insertions, 0 deletions
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml new file mode 100644 index 00000000..8ef23c48 --- /dev/null +++ b/contrib/funind/new_arg_principle.ml @@ -0,0 +1,1770 @@ +open Printer +open Util +open Term +open Termops +open Names +open Declarations +open Pp +open Entries +open Hiddentac +open Evd +open Tacmach +open Proof_type +open Tacticals +open Tactics +open Indfun_common + + +let msgnl = Pp.msgnl + +let do_observe () = + Tacinterp.get_debug () <> Tactic_debug.DebugOff + + +let observe strm = + if do_observe () + then Pp.msgnl strm + else () + +let observennl strm = + if do_observe () + then begin Pp.msg strm;Pp.pp_flush () end + else () + + + + +let do_observe_tac s tac g = + try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v + with e -> + let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + msgnl (str "observation "++str s++str " raised exception " ++ + Cerrors.explain_exn e ++ str "on goal " ++ goal ); + raise e;; + + +let observe_tac s tac g = + if do_observe () + then do_observe_tac s tac g + else tac g + + +let tclTRYD tac = + if !Options.debug || do_observe () + then (fun g -> try do_observe_tac "" tac g with _ -> tclIDTAC g) + else tac + + +let list_chop ?(msg="") n l = + try + list_chop n l + with Failure (msg') -> + failwith (msg ^ msg') + + +let make_refl_eq type_of_t t = + let refl_equal_term = Lazy.force refl_equal in + mkApp(refl_equal_term,[|type_of_t;t|]) + + +type static_fix_info = + { + idx : int; + name : identifier; + types : types + } + +type static_infos = + { + fixes_ids : identifier list; + ptes_to_fixes : static_fix_info Idmap.t + } + +type 'a dynamic_info = + { + nb_rec_hyps : int; + rec_hyps : identifier list ; + eq_hyps : identifier list; + info : 'a + } + +let finish_proof dynamic_infos g = + observe_tac "finish" + h_assumption + g + + +let refine c = + Tacmach.refine_no_check c + +let thin l = + Tacmach.thin_no_check l + + +let cut_replacing id t tac :tactic= + tclTHENS (cut t) + [ tclTHEN (thin_no_check [id]) (introduction_no_check id); + tac + ] + +let intro_erasing id = tclTHEN (thin [id]) (introduction id) + + + +let rec_hyp_id = id_of_string "rec_hyp" + +let is_trivial_eq t = + match kind_of_term t with + | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> + eq_constr t1 t2 + | _ -> false + + +let rec incompatible_constructor_terms t1 t2 = + let c1,arg1 = decompose_app t1 + and c2,arg2 = decompose_app t2 + in + (not (eq_constr t1 t2)) && + isConstruct c1 && isConstruct c2 && + ( + not (eq_constr c1 c2) || + List.exists2 incompatible_constructor_terms arg1 arg2 + ) + +let is_incompatible_eq t = + match kind_of_term t with + | App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) -> + incompatible_constructor_terms t1 t2 + | _ -> false + +let change_hyp_with_using hyp_id t tac = + fun g -> + let prov_id = pf_get_new_id hyp_id g in + tclTHENLIST + [ + forward (Some tac) (Genarg.IntroIdentifier prov_id) t; + thin [hyp_id]; + h_rename prov_id hyp_id + ] g + +exception TOREMOVE + + +let prove_trivial_eq h_id context (type_of_term,term) = + let nb_intros = List.length context in + tclTHENLIST + [ + tclDO nb_intros intro; (* introducing context *) + (fun g -> + let context_hyps = + fst (list_chop ~msg:"prove_trivial_eq : " nb_intros (pf_ids_of_hyps g)) + in + let context_hyps' = + (mkApp(Lazy.force refl_equal,[|type_of_term;term|])):: + (List.map mkVar context_hyps) + in + let to_refine = applist(mkVar h_id,List.rev context_hyps') in + refine to_refine g + ) + ] + + +let isAppConstruct t = + if isApp t + then isConstruct (fst (destApp t)) + else false + + +let nf_betaoiotazeta = Reductionops.local_strong Reductionops.whd_betaiotazeta + +let remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 = + let rel_num = destRel t2 in + + let nb_kept = List.length context - rel_num + and nb_popped = rel_num - 1 + in + + (* We remove the equation *) + let new_end_of_type = pop end_of_type in + + let lt_relnum,ge_relnum = + list_chop + ~msg:("removing useless variable "^(string_of_int rel_num)^" :") + nb_popped + context + in + (* we rebuilt the type of hypothesis after the rel to remove *) + let hyp_type_lt_relnum = + it_mkProd_or_LetIn ~init:new_end_of_type lt_relnum + in + (* we replace Rel 1 by t1 *) + let new_hyp_type_lt_relnum = subst1 t1 hyp_type_lt_relnum in + (* we resplit the type of hyp_type *) + let new_lt_relnum,new_end_of_type = + Sign.decompose_prod_n_assum nb_popped new_hyp_type_lt_relnum + in + (* and rebuilt new context of hyp *) + let new_context = new_lt_relnum@(List.tl ge_relnum) in + let new_typ_of_hyp = + nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type new_context) + in + let prove_simpl_eq = + tclTHENLIST + [ + tclDO (nb_popped + nb_kept) intro; + (fun g' -> + let new_hyps_ids = pf_ids_of_hyps g' in + let popped_ids,others = + list_chop ~msg:"removing useless variable pop :" + nb_popped new_hyps_ids in + let kept_ids,_ = + list_chop ~msg: " removing useless variable kept : " + nb_kept others + in + let rev_to_apply = + (mkApp(Lazy.force refl_equal,[|Typing.type_of env sigma t1;t1|])):: + ((List.map mkVar popped_ids)@ + (t1:: + (List.map mkVar kept_ids))) + in + let to_refine = applist(mkVar hyp_id,List.rev rev_to_apply) in + refine to_refine g' + ) + ] + in + let simpl_eq_tac = change_hyp_with_using hyp_id new_typ_of_hyp + (observe_tac "prove_simpl_eq" prove_simpl_eq) + in + let new_end_of_type = nf_betaoiotazeta new_end_of_type in + (new_context,new_end_of_type,simpl_eq_tac),new_typ_of_hyp, + (str " removing useless variable " ++ str (string_of_int rel_num) ) + + +let decompose_eq env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 = + let c1,args1 = destApp t1 + and c2,args2 = destApp t2 + in + (* This tactic must be used after is_incompatible_eq *) + assert (eq_constr c1 c2); + (* we remove this equation *) + let new_end_of_type = pop end_of_type in + let new_eqs = + array_map2_i + (fun i arg1 arg2 -> + let new_eq = + let type_of_arg = Typing.type_of env sigma arg1 in + mkApp(Lazy.force eq,[|type_of_arg;arg1;arg2|]) + in + Anonymous,None,lift i new_eq + ) + args1 + args2 + in + let nb_new_eqs = Array.length new_eqs in + (* we add the new equation *) + let new_end_of_type = lift nb_new_eqs new_end_of_type in + let local_context = + List.rev (Array.to_list new_eqs) in + let new_end_of_type = it_mkProd_or_LetIn ~init:new_end_of_type local_context in + let new_typ_of_hyp = + nf_betaoiotazeta (it_mkProd_or_LetIn ~init:new_end_of_type context) + in + let prove_pattern_simplification = + let context_length = List.length context in + tclTHENLIST + [ + tclDO (context_length + nb_new_eqs) intro ; + (fun g -> + let new_eqs,others = + list_chop ~msg:"simplifying pattern : new_eqs" nb_new_eqs (pf_hyps g) + in + let context_hyps,_ = list_chop ~msg:"simplifying pattern : context_hyps" + context_length others in + let eq_args = + List.rev_map + (fun (_,_, eq) -> let _,args = destApp eq in args.(1),args.(2)) + new_eqs + in + let lhs_args,rhs_args = List.split eq_args in + let lhs_eq = applist(c1,lhs_args) + and rhs_eq = applist(c1,rhs_args) + in + let type_of_eq = pf_type_of g lhs_eq in + let eq_to_assert = + mkApp(Lazy.force eq,[|type_of_eq;lhs_eq;rhs_eq|]) + in + let prove_new_eq = + tclTHENLIST [ + tclMAP + (fun (id,_,_) -> + (* The tclTRY here is used when trying to rewrite + on Set + eg (@cons A x l)=(@cons A x' l') generates 3 eqs + A=A -> x=x' -> l = l' ... + + *) + tclTRY (Equality.rewriteLR (mkVar id)) + ) + new_eqs; + reflexivity + ] + in + let new_eq_id = pf_get_new_id (id_of_string "H") g in + let create_new_eq = + forward + (Some (observe_tac "prove_new_eq" (prove_new_eq))) + (Genarg.IntroIdentifier new_eq_id) + eq_to_assert + in + let to_refine = + applist ( + mkVar hyp_id, + List.rev ((mkVar new_eq_id):: + (List.map (fun (id,_,_) -> mkVar id) context_hyps))) + in + tclTHEN + (observe_tac "create_new_eq" create_new_eq ) + (observe_tac "refine in decompose_eq " (refine to_refine)) + g + ) + ] + in + let simpl_eq_tac = + change_hyp_with_using hyp_id new_typ_of_hyp (observe_tac "prove_pattern_simplification " prove_pattern_simplification) + in + (context,nf_betaoiotazeta new_end_of_type,simpl_eq_tac),new_typ_of_hyp, + str "simplifying an equation " + +let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = + if not (noccurn 1 end_of_type) + then (* if end_of_type depends on this term we don't touch it *) + begin + observe (str "Not treating " ++ pr_lconstr t ); + failwith "NoChange"; + end; + let res,new_typ_of_hyp,msg = + if not (isApp t) then failwith "NoChange"; + let f,args = destApp t in + if not (eq_constr f (Lazy.force eq)) then failwith "NoChange"; + let t1 = args.(1) + and t2 = args.(2) + in + if isRel t2 && closed0 t1 then (* closed_term = x with x bound in context *) + begin + remove_useless_rel env sigma hyp_id (context:Sign.rel_context) t end_of_type t1 t2 + end + else if isAppConstruct t1 && isAppConstruct t2 (* C .... = C .... *) + then decompose_eq env sigma hyp_id context t end_of_type t1 t2 + else failwith "NoChange" + in + observe (str "In " ++ Ppconstr.pr_id hyp_id ++ + msg ++ fnl ()++ + str "old_typ_of_hyp :=" ++ + Printer.pr_lconstr_env + env + (it_mkProd_or_LetIn ~init:end_of_type ((x,None,t)::context)) + ++ fnl () ++ + str "new_typ_of_hyp := "++ + Printer.pr_lconstr_env env new_typ_of_hyp ++ fnl ()); + (res:'a*'b*'c) + + + + +let is_property static_info t_x = + if isApp t_x + then + let pte,args = destApp t_x in + if isVar pte && array_for_all closed0 args + then Idmap.mem (destVar pte) static_info.ptes_to_fixes + else false + else false + +let isLetIn t = + match kind_of_term t with + | LetIn _ -> true + | _ -> false + + +let h_reduce_with_zeta = + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + +(* +let rewrite_until_var arg_num : tactic = + let constr_eq = Lazy.force eq in + let replace_if_unify arg (pat,cl,id,lhs) : tactic = + fun g -> + try + let (evd,matched) = + Unification.w_unify_to_subterm + (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env + in + let cl' = {cl with Clenv.env = evd } in + let c2 = Clenv.clenv_nf_meta cl' lhs in + (Equality.replace matched c2) g + with _ -> tclFAIL 0 (str "") g + in + let rewrite_on_step equalities : tactic = + fun g -> + match kind_of_term (pf_concl g) with + | App(_,args) when (not (test_var args arg_num)) -> +(* tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *) + tclFIRST (List.map (replace_if_unify args.(arg_num)) equalities) g + | _ -> + raise (Util.UserError("", (str "No more rewrite" ++ + pr_lconstr_env (pf_env g) (pf_concl g)))) + in + fun g -> + let equalities = + List.filter + ( + fun (_,_,id_t) -> + match kind_of_term id_t with + | App(f,_) -> eq_constr f constr_eq + | _ -> false + ) + (pf_hyps g) + in + let f (id,_,ctype) = + let c = mkVar id in + let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in + let clause_type = Clenv.clenv_type eqclause in + let f,args = decompose_app (clause_type) in + let rec split_last_two = function + | [c1;c2] -> (c1, c2) + | x::y::z -> + split_last_two (y::z) + | _ -> + error ("The term provided is not an equivalence") + in + let (c1,c2) = split_last_two args in + (c2,eqclause,id,c1) + in + let matching_hyps = List.map f equalities in + tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g + +*) + + +let rewrite_until_var arg_num eq_ids : tactic = + let test_var g = + let _,args = destApp (pf_concl g) in + isVar args.(arg_num) + in + let rec do_rewrite eq_ids g = + if test_var g + then tclIDTAC g + else + match eq_ids with + | [] -> anomaly "Cannot find a way to prove recursive property"; + | eq_id::eq_ids -> + tclTHEN + (tclTRY (Equality.rewriteRL (mkVar eq_id))) + (do_rewrite eq_ids) + g + in + do_rewrite eq_ids + +let prove_rec_hyp eq_hyps fix_info = + tclTHEN + (rewrite_until_var (fix_info.idx - 1) eq_hyps) + (fun g -> + let _,pte_args = destApp (pf_concl g) in + let rec_hyp_proof = + mkApp(mkVar fix_info.name,array_get_start pte_args) + in + refine rec_hyp_proof g + ) + + + + + +let rec_pte_id = id_of_string "Hrec" +let clean_hyp_with_heq static_infos eq_hyps hyp_id env sigma = + let coq_False = Coqlib.build_coq_False () in + let coq_True = Coqlib.build_coq_True () in + let coq_I = Coqlib.build_coq_I () in + let rec scan_type context type_of_hyp : tactic = + if isLetIn type_of_hyp then + let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in + let reduced_type_of_hyp = nf_betaoiotazeta real_type_of_hyp in + (* length of context didn't change ? *) + let new_context,new_typ_of_hyp = + Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp + in + tclTHENLIST + [ + h_reduce_with_zeta + (Tacticals.onHyp hyp_id) + ; + scan_type new_context new_typ_of_hyp + + ] + else if isProd type_of_hyp + then + begin + let (x,t_x,t') = destProd type_of_hyp in + if is_property static_infos t_x then + begin + let pte,pte_args = (destApp t_x) in + let fix_info = Idmap.find (destVar pte) static_infos.ptes_to_fixes in + let popped_t' = pop t' in + let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in + let prove_new_type_of_hyp = + let context_length = List.length context in + tclTHENLIST + [ + tclDO context_length intro; + (fun g -> + let context_hyps_ids = + fst (list_chop ~msg:"rec hyp : context_hyps" + context_length (pf_ids_of_hyps g)) + in + let rec_pte_id = pf_get_new_id rec_pte_id g in + let to_refine = + applist(mkVar hyp_id, + List.rev_map mkVar (rec_pte_id::context_hyps_ids) + ) + in + tclTHENLIST + [ + forward + (Some (prove_rec_hyp eq_hyps fix_info)) + (Genarg.IntroIdentifier rec_pte_id) + t_x; + refine to_refine + ] + g + ) + ] + in + tclTHENLIST + [ + observe_tac "hyp rec" + (change_hyp_with_using hyp_id real_type_of_hyp prove_new_type_of_hyp); + scan_type context popped_t' + ] + end + else if eq_constr t_x coq_False then + begin + observe (str "Removing : "++ Ppconstr.pr_id hyp_id++ + str " since it has False in its preconds " + ); + raise TOREMOVE; (* False -> .. useless *) + end + else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) + else if eq_constr t_x coq_True (* Trivial => we remove this precons *) + then + let _ = + observe (str "In "++Ppconstr.pr_id hyp_id++ + str " removing useless precond True" + ) + in + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn ~init:popped_t' context + in + let prove_trivial = + let nb_intro = List.length context in + tclTHENLIST [ + tclDO nb_intro intro; + (fun g -> + let context_hyps = + fst (list_chop ~msg:"removing True : context_hyps "nb_intro (pf_ids_of_hyps g)) + in + let to_refine = + applist (mkVar hyp_id, + List.rev (coq_I::List.map mkVar context_hyps) + ) + in + refine to_refine g + ) + ] + in + tclTHENLIST[ + change_hyp_with_using hyp_id real_type_of_hyp (observe_tac "prove_trivial" prove_trivial); + scan_type context popped_t' + ] + else if is_trivial_eq t_x + then (* t_x := t = t => we remove this precond *) + let popped_t' = pop t' in + let real_type_of_hyp = + it_mkProd_or_LetIn ~init:popped_t' context + in + let _,args = destApp t_x in + tclTHENLIST + [ + change_hyp_with_using + hyp_id + real_type_of_hyp + (observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1)))); + scan_type context popped_t' + ] + else + begin + try + let new_context,new_t',tac = change_eq env sigma hyp_id context x t_x t' in + tclTHEN + tac + (scan_type new_context new_t') + with Failure "NoChange" -> + (* Last thing todo : push the rel in the context and continue *) + scan_type ((x,None,t_x)::context) t' + end + end + else + tclIDTAC + in + try + scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] + with TOREMOVE -> + thin [hyp_id],[] + + +let clean_goal_with_heq static_infos continue_tac dyn_infos = + fun g -> + let env = pf_env g + and sigma = project g + in + let tac,new_hyps = + List.fold_left ( + fun (hyps_tac,new_hyps) hyp_id -> + let hyp_tac,new_hyp = + clean_hyp_with_heq static_infos dyn_infos.eq_hyps hyp_id env sigma + in + (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps + ) + (tclIDTAC,[]) + dyn_infos.rec_hyps + in + let new_infos = + { dyn_infos with + rec_hyps = new_hyps; + nb_rec_hyps = List.length new_hyps + } + in + tclTHENLIST + [ + tac ; + (continue_tac new_infos) + ] + g + +let heq_id = id_of_string "Heq" + +let treat_new_case static_infos nb_prod continue_tac term dyn_infos = + fun g -> + let heq_id = pf_get_new_id heq_id g in + let nb_first_intro = nb_prod - 1 - dyn_infos.nb_rec_hyps in + tclTHENLIST + [ + (* We first introduce the variables *) + tclDO nb_first_intro (intro_avoiding dyn_infos.rec_hyps); + (* Then the equation itself *) + introduction_no_check heq_id; + (* Then the new hypothesis *) + tclMAP introduction_no_check dyn_infos.rec_hyps; + observe_tac "after_introduction" (fun g' -> + (* We get infos on the equations introduced*) + let new_term_value_eq = pf_type_of g' (mkVar heq_id) in + (* compute the new value of the body *) + let new_term_value = + match kind_of_term new_term_value_eq with + | App(f,[| _;_;args2 |]) -> args2 + | _ -> + observe (pr_gls g' ++ fnl () ++ str "last hyp is" ++ + pr_lconstr_env (pf_env g') new_term_value_eq + ); + assert false + in + let fun_body = + mkLambda(Anonymous, + pf_type_of g' term, + replace_term term (mkRel 1) dyn_infos.info + ) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + let new_infos = + {dyn_infos with + info = new_body; + eq_hyps = heq_id::dyn_infos.eq_hyps + } + in + clean_goal_with_heq static_infos continue_tac new_infos g' + ) + ] + g + +let do_prove_princ_for_struct + (interactive_proof:bool) + (fnames:constant list) + static_infos +(* (ptes:identifier list) *) +(* (fixes:(int*constr*identifier*constr) Idmap.t) *) +(* (hyps: identifier list) *) +(* (term:constr) *) + dyn_infos + : tactic = +(* let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *) + let rec do_prove_princ_for_struct_aux do_finalize dyn_infos : tactic = + fun g -> +(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) + match kind_of_term dyn_infos.info with + | Case(_,_,t,_) -> + let g_nb_prod = nb_prod (pf_concl g) in + let type_of_term = pf_type_of g t in + let term_eq = + make_refl_eq type_of_term t + in + tclTHENSEQ + [ + h_generalize (term_eq::List.map mkVar dyn_infos.rec_hyps); + thin dyn_infos.rec_hyps; + pattern_option [[-1],t] None; + h_simplest_case t; + (fun g' -> + let g'_nb_prod = nb_prod (pf_concl g') in + let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + static_infos + nb_instanciate_partial + (do_prove_princ_for_struct do_finalize) + t + dyn_infos) + g' + ) + + ] g + | Lambda(n,t,b) -> + begin + match kind_of_term( pf_concl g) with + | Prod _ -> + tclTHEN + intro + (fun g' -> + let (id,_,_) = pf_last_hyp g' in + let new_term = + pf_nf_betaiota g' + (mkApp(dyn_infos.info,[|mkVar id|])) + in + let new_infos = {dyn_infos with info = new_term} in + do_prove_princ_for_struct do_finalize new_infos g' + ) g + | _ -> + do_finalize dyn_infos g + end + | Cast(t,_,_) -> + do_prove_princ_for_struct do_finalize {dyn_infos with info = t} g + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + do_finalize dyn_infos g + | App(_,_) -> + let f,args = decompose_app dyn_infos.info in + begin + match kind_of_term f with + | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in + do_prove_princ_for_struct_args do_finalize new_infos g + | Const c when not (List.mem c fnames) -> + let new_infos = + { dyn_infos with + info = (f,args) + } + in + do_prove_princ_for_struct_args do_finalize new_infos g + | Const _ -> + do_finalize dyn_infos g + | _ -> +(* observe *) +(* (str "Applied binders not yet implemented: in "++ fnl () ++ *) +(* pr_lconstr_env (pf_env g) term ++ fnl () ++ *) +(* pr_lconstr_env (pf_env g) f ++ spc () ++ str "is applied") ; *) + tclFAIL 0 (str "TODO : Applied binders not yet implemented") g + end + | Fix _ | CoFix _ -> + error ( "Anonymous local (co)fixpoints are not handled yet") + + | Prod _ -> assert false + | LetIn _ -> + let new_infos = + { dyn_infos with + info = nf_betaoiotazeta dyn_infos.info + } + in + + tclTHENLIST + [tclMAP + (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) + dyn_infos.rec_hyps; + h_reduce_with_zeta Tacticals.onConcl; + do_prove_princ_for_struct do_finalize new_infos + ] g + | _ -> + errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *) +(* pr_lconstr_env (pf_env g) term *) + ) + and do_prove_princ_for_struct do_finalize dyn_infos g = +(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) + do_prove_princ_for_struct_aux do_finalize dyn_infos g + and do_prove_princ_for_struct_args do_finalize dyn_infos (* f_args' args *) :tactic = + fun g -> +(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) +(* then msgnl (str "do_prove_princ_for_struct_args with " ++ *) +(* pr_lconstr_env (pf_env g) f_args' *) +(* ); *) + let (f_args',args) = dyn_infos.info in + let tac = + match args with + | [] -> + do_finalize {dyn_infos with info = f_args'} + | arg::args -> + let do_finalize dyn_infos = + let new_arg = dyn_infos.info in + tclTRYD + (do_prove_princ_for_struct_args + do_finalize + {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} + ) + in + do_prove_princ_for_struct do_finalize + {dyn_infos with info = arg } + in + tclTRYD(tac ) g + in + let do_finish_proof dyn_infos = + clean_goal_with_heq + static_infos + finish_proof dyn_infos + in + observe_tac "do_prove_princ_for_struct" + (do_prove_princ_for_struct do_finish_proof dyn_infos) + +let is_pte_type t = + isSort (snd (decompose_prod t)) + +let is_pte (_,_,t) = is_pte_type t + +exception Not_Rec + + + +let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in + let instanciate_one_hyp hid = + tclORELSE + ( (* we instanciate the hyp if possible *) +(* tclTHENLIST *) +(* [h_generalize [mkApp(mkVar hid,args)]; *) +(* intro_erasing hid] *) + fun g -> + let prov_hid = pf_get_new_id hid g in + tclTHENLIST[ + forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); + thin [hid]; + h_rename prov_hid hid + ] g + ) + ( (* + if not then we are in a mutual function block + and this hyp is a recursive hyp on an other function. + + We are not supposed to use it while proving this + principle so that we can trash it + + *) + (fun g -> + observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); + thin [hid] g + ) + ) + in + (* if no args then no instanciation ! *) + if args_id = [] + then + tclTHENLIST [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + do_prove hyps + ] + else + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps; + tclMAP instanciate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty + in + let remaining_hyps = + List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps + in + do_prove remaining_hyps g + ) + ] + + +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 : " ++ *) +(* 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 pte_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 new_type = prod_applist typearray.(i) true_params in + let new_type_args,_ = decompose_prod new_type in + let nargs = List.length new_type_args in + let pte_args = + (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *) + let f = applist((* all_funs *)mkConst fnames.(i),true_params) in + let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) in + (Array.to_list (Array.init nargs (fun i -> mkRel(nargs - i))))@[app_f] + in + let app_pte = applist(mkVar pte_id,pte_args) in + let new_type = compose_prod new_type_args app_pte in + let fix_info = + { + idx = idxs.(i) - offset + 1; + name = this_fix_id; + types = new_type + } + in + pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix; + fix_info::acc + ) + 0 + [] + 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 -> pr_lconstr (mkVar id)) *) +(* !params *) +(* ); *) + let new_avoid,infos = + option_fold_right + (build_pte_to_fix + offset + (List.map mkVar !params) + (List.rev !predicates) + ) + 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 + | _,this_fix_info::infos' -> + let other_fix_info = + List.map + (fun fix_info -> fix_info.name,fix_info.idx,fix_info.types) + (pre_info@infos') + in + tclORELSE + (h_mutual_fix this_fix_info.name this_fix_info.idx other_fix_info) + (tclFAIL 1000 (str "bad index" ++ + str (string_of_int this_fix_info.idx) ++ + str "offset := " ++ + (str (string_of_int offset)))) + g + | _,[] -> anomaly "Not a valid information" + in + let do_prove ptes_to_fixes args branches : tactic = + fun g -> + let static_infos = + { + ptes_to_fixes = ptes_to_fixes; + fixes_ids = + Idmap.fold + (fun _ fix_info acc -> fix_info.name::acc) + ptes_to_fixes [] + } + in + match kind_of_term (pf_concl g) with + | App(pte,pte_args) when isVar pte -> + begin + let pte = destVar pte in + try + if not (Idmap.mem pte ptes_to_fixes) then raise Not_Rec; + 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 (List.rev !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 branches applied_body = + do_prove_princ_for_struct + interactive_proof + (Array.to_list fnames) + static_infos + branches + applied_body + in + let replace_and_prove = + tclTHENS + (fun g -> +(* observe (str "replacing " ++ *) +(* pr_lconstr_env (pf_env g) (array_last pte_args) ++ *) +(* str " with " ++ *) +(* 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 + ) + [ + clean_goal_with_heq + static_infos do_prove + { + nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = applied_body; + eq_hyps = []; + } ; + try + let id = List.nth (List.rev args_as_constr) (rec_num) in + (* observe (str "choosen var := "++ pr_lconstr id); *) + (tclTHENSEQ + [(h_simplest_case id); + Tactics.intros_reflexivity + ]) + with _ -> tclIDTAC + + ] + in + (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' -> + let body = array_last (snd (destApp (pf_concl g'))) in + let dyn_infos = + { nb_rec_hyps = List.length branches; + rec_hyps = branches; + info = body; + eq_hyps = [] + } + in + let do_prove = + do_prove_princ_for_struct + interactive_proof + (Array.to_list fnames) + static_infos + in + clean_goal_with_heq static_infos + do_prove dyn_infos 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 -> + let nb_prod_g = nb_prod (pf_concl g) in + tclTHENLIST [ + tclDO nb_prod_g intro; + (fun g' -> + let args = + fst (list_chop ~msg:"args" nb_prod_g (pf_ids_of_hyps g')) + in + let do_prove_on_branches branches : tactic = + observe_tac "proving" (do_prove !pte_to_fix args branches) + in + observe_tac "instanciating rec hyps" + (instanciate_hyps_with_args do_prove_on_branches !branches (List.rev args)) + g' + ) + ] + g + ) + ] + goal + + + + + + + + + + + + + + + + + + + + + + + +exception Toberemoved_with_rel of int*constr +exception Toberemoved + +let compute_new_princ_type_from_rel rel_to_fun sorts 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 i (x,_,t) = + let new_sort = sorts.(i) in + 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 new_sort) + in + let new_predicates = + list_map_i + change_predicate_sort + 0 + 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 + | Construct((u,_),_) -> u = rel_as_kn + | _ -> false + in + let get_fun_num c = + match kind_of_term c with + | Ind(_,num) -> num + | Construct((_,num),_) -> num + | _ -> assert false + in + let dummy_var = mkVar (id_of_string "________") in + let mk_replacement c i args = + let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in +(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) + res + in + let rec has_dummy_var t = + fold_constr + (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t)) + false + t + 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 + try match Environ.lookup_rel n env with + | _,_,t when is_dom t -> raise Toberemoved + | _ -> pre_princ,[] with Not_found -> assert false + end + | Prod(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 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 pre_princ 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 remove env) + args + ([],[]) + in + let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in + applist(new_f, 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 remove env x v t b + | _ -> pre_princ,[] + in +(* observennl ( *) +(* match kind_of_term pre_princ with *) +(* | Prod _ -> *) +(* str "compute_new_princ_type for "++ *) +(* pr_lconstr_env env pre_princ ++ *) +(* str" is "++ *) +(* pr_lconstr_env env new_princ_type ++ fnl () *) +(* | _ -> str "" *) +(* ); *) + res + + 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 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 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 + ( + bind_fun(new_x,new_t,new_b), + list_union_eq + eq_constr + binders_to_remove_from_t + (List.map pop binders_to_remove_from_b) + ) + + 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 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 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 remove env x v t b = + begin + try + 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 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 + ( + mkLetIn(new_x,new_v,new_t,new_b), + list_union_eq + eq_constr + (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) + (List.map pop binders_to_remove_from_b) + ) + + 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 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 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 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 +(* observe (str "Computing new principe from " ++ 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 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 + 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 pp_dur time time' = + str (string_of_float (System.time_difference time time')) + +(* Things to be removed latter : just here to compare + saving proof with and without normalizing the proof +*) +let new_save id const (locality,kind) hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let l,r = match locality with + | Decl_kinds.Local when Lib.sections_are_opened () -> + let k = Decl_kinds.logical_kind_of_goal_kind kind in + let c = Declare.SectionLocalDef (pft, tpo, opacity) in + let _ = Declare.declare_variable id (Lib.cwd(), c, k) in + (Decl_kinds.Local, Libnames.VarRef id) + | Decl_kinds.Local -> + let k = Decl_kinds.logical_kind_of_goal_kind kind in + let kn = Declare.declare_constant id (DefinitionEntry const, k) in + (Decl_kinds.Global, Libnames.ConstRef kn) + | Decl_kinds.Global -> + let k = Decl_kinds.logical_kind_of_goal_kind kind in + let kn = Declare.declare_constant id (DefinitionEntry const, k) in + (Decl_kinds.Global, Libnames.ConstRef kn) in + let time1 = System.get_time () in + Pfedit.delete_current_proof (); + let time2 = System.get_time () in + hook l r; + time1,time2 +(* definition_message id *) + + + + + +let new_save_named opacity = +(* if do_observe () *) +(* then *) + let time1 = System.get_time () in + let id,(const,persistence,hook) = Pfedit.cook_proof () in + let time2 = System.get_time () in + let const = + { const with + const_entry_body = (* nf_betaoiotazeta *)const.const_entry_body ; + const_entry_opaque = opacity + } + in + let time3 = System.get_time () in + let time4,time5 = new_save id const persistence hook in + let time6 = System.get_time () in + Pp.msgnl + (str "cooking proof time : " ++ pp_dur time1 time2 ++ fnl () ++ + str "reducing proof time : " ++ pp_dur time2 time3 ++ fnl () ++ + str "saving proof time : " ++ pp_dur time3 time4 ++fnl () ++ + str "deleting proof time : " ++ pp_dur time4 time5 ++fnl () ++ + str "hook time :" ++ pp_dur time5 time6 + ) + +;; + +(* End of things to be removed latter : just here to compare + saving proof with and without normalizing the proof +*) + + +let generate_functional_principle + interactive_proof + old_princ_type sorts new_princ_name funs i proof_tac + = + let f = funs.(i) in + let type_sort = Termops.new_sort_in_family InType in + let new_sorts = + match sorts with + | None -> Array.make (Array.length funs) (type_sort) + | Some a -> a + in + (* First we get the type of the old graph principle *) + 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) + new_sorts + old_princ_type + in +(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) + let base_new_princ_name,new_princ_name = + match new_princ_name with + | Some (id) -> id,id + | None -> + let id_of_f = id_of_label (con_label f) in + id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + in + let names = ref [new_princ_name] in + let hook _ _ = + if sorts = None + then +(* 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 base_new_princ_name fam_sort in + let value = + change_property_sort s new_principle_type new_princ_name + in +(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let ce = + { const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() + } + in + ignore( + Declare.declare_constant + name + (Entries.DefinitionEntry ce, + Decl_kinds.IsDefinition (Decl_kinds.Scheme) + ) + ); + names := name :: !names + in + register_with_sort InProp; + register_with_sort InSet + in + begin + Command.start_proof + new_princ_name + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) + new_principle_type + hook + ; + try + let _tim1 = System.get_time () in + Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + let _tim2 = System.get_time () in +(* begin *) +(* let dur1 = System.time_difference tim1 tim2 in *) +(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) +(* end; *) + let do_save = not (do_observe ()) && not interactive_proof in + let _ = + try + Options.silently Command.save_named true; + let _dur2 = System.time_difference _tim2 (System.get_time ()) in +(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *) + Options.if_verbose + (fun () -> + Pp.msgnl ( + prlist_with_sep + (fun () -> str" is defined " ++ fnl ()) + Ppconstr.pr_id + (List.rev !names) ++ str" is defined " + ) + ) + () + with e when do_save -> + msg_warning + ( + Cerrors.explain_exn e + ); + if not (do_observe ()) + then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + in + () + +(* let tim3 = Sys.time () in *) +(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *) + + with + | e -> + msg_warning + ( + Cerrors.explain_exn e + ); + if not ( do_observe ()) + then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + end + + + + + + +let get_funs_constant mp dp = + let rec get_funs_constant const e : (Names.constant*int) array = + match kind_of_term (snd (decompose_lam e)) with + | Fix((_,(na,_,_))) -> + Array.mapi + (fun i na -> + match na with + | Name id -> + let const = make_con mp dp (label_of_id id) in + const,i + | Anonymous -> + anomaly "Anonymous fix" + ) + na + | _ -> [|const,0|] + in + function const -> + let find_constant_body const = + match (Global.lookup_constant const ).const_body with + | Some b -> + let body = force b in + let body = Tacred.cbv_norm_flags + (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + (Global.env ()) + (Evd.empty) + body + in + body + | None -> error ( "Cannot define a principle over an axiom ") + in + let f = find_constant_body const in + let l_const = get_funs_constant const f in + (* + We need to check that all the functions found are in the same block + to prevent Reset stange thing + *) + let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in + let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in + (* all the paremeter must be equal*) + let _check_params = + let first_params = List.hd l_params in + List.iter + (fun params -> + if not ((=) first_params params) + then error "Not a mutal recursive block" + ) + l_params + in + (* The bodies has to be very similar *) + let _check_bodies = + try + let extract_info is_first body = + match kind_of_term body with + | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) + | _ -> + if is_first && (List.length l_bodies = 1) + then raise Not_Rec + else error "Not a mutal recursive block" + in + let first_infos = extract_info true (List.hd l_bodies) in + let check body = (* Hope this is correct *) + if not (first_infos = (extract_info false body)) + then error "Not a mutal recursive block" + in + List.iter check l_bodies + with Not_Rec -> () + in + l_const + +let make_scheme fas = + let env = Global.env () + and sigma = Evd.empty in + let id_to_constr id = + Tacinterp.constr_of_id env id + in + let funs = List.map (fun (_,f,_) -> id_to_constr f) fas in + let first_fun = destConst (List.hd funs) in + let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in + let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let first_fun_kn = + (* Fixme: take into accour funs_mp and funs_dp *) + fst (destInd (id_to_constr first_fun_rel_id)) + in + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in + let this_block_funs = Array.map fst this_block_funs_indexes in + let prop_sort = InProp in + let funs_indexes = + let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + List.map + (function const -> List.assoc (destConst const) this_block_funs_indexes) + funs + in + let ind_list = + List.map + (fun (idx) -> + let ind = first_fun_kn,idx in + let (mib,mip) = Global.lookup_inductive ind in + ind,mib,mip,true,prop_sort + ) + funs_indexes + in + let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in + let i = ref (-1) in + let sorts = + List.rev_map (fun (_,_,x) -> + Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + ) + fas + in + let princ_names = List.map (fun (x,_,_) -> x) fas in + let _ = List.map2 + (fun princ_name scheme_type -> + incr i; +(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) +(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) +(* ); *) + generate_functional_principle + false + scheme_type + (Some (Array.of_list sorts)) + (Some princ_name) + this_block_funs + !i + (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) + ) + princ_names + l_schemes + in + () + +let make_case_scheme fa = + let env = Global.env () + and sigma = Evd.empty in + let id_to_constr id = + Tacinterp.constr_of_id env id + in + let funs = (fun (_,f,_) -> id_to_constr f) fa in + let first_fun = destConst funs in + let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in + let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let first_fun_kn = + (* Fixme: take into accour funs_mp and funs_dp *) + fst (destInd (id_to_constr first_fun_rel_id)) + in + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in + let this_block_funs = Array.map fst this_block_funs_indexes in + let prop_sort = InProp in + let funs_indexes = + let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + List.assoc (destConst funs) this_block_funs_indexes + in + let ind_fun = + let ind = first_fun_kn,funs_indexes in + ind,prop_sort + in + let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in + let sorts = + (fun (_,_,x) -> + Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + ) + fa + in + let princ_name = (fun (x,_,_) -> x) fa in + let _ = +(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) +(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) +(* ); *) + generate_functional_principle + false + scheme_type + (Some ([|sorts|])) + (Some princ_name) + this_block_funs + 0 + (prove_princ_for_struct false 0 [|destConst funs|]) + in + () |