diff options
Diffstat (limited to 'contrib/funind/new_arg_principle.ml')
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 1770 |
1 files changed, 0 insertions, 1770 deletions
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml deleted file mode 100644 index 8ef23c48..00000000 --- a/contrib/funind/new_arg_principle.ml +++ /dev/null @@ -1,1770 +0,0 @@ -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 - () |