diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun.ml | 227 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.ml | 7 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 111 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 1449 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.mli | 1 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 388 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.mli | 2 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 23 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.mli | 10 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 4 |
11 files changed, 1810 insertions, 414 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index c8ff98289..2fcdd3a75 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -6,6 +6,7 @@ open Pp open Indfun_common open Libnames open Rawterm +open Declarations type annot = Struct of identifier @@ -97,11 +98,14 @@ let rec is_rec names = lookup let prepare_body (name,annot,args,types,body) rt = - let fun_args,rt' = chop_rlambda_n (Topconstr.local_binders_length args) rt in + let n = (Topconstr.local_binders_length args) in +(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) + let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let generate_principle fix_rec_l recdefs interactive_proof parametrize +let generate_principle + do_built fix_rec_l recdefs interactive_proof parametrize (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) = let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in @@ -110,44 +114,47 @@ let generate_principle fix_rec_l recdefs interactive_proof parametrize try (* We then register the Inductive graphs of the functions *) Rawterm_to_relation.build_inductive parametrize names funs_args funs_types recdefs; - let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in - let ind_kn = - fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") - locate_ind - f_R_mut) - in - let fname_kn (fname,_,_,_,_) = - let f_ref = Ident (dummy_loc,fname) in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") - locate_constant - f_ref - in - let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in - let _ = - Util.list_map_i - (fun i x -> - let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in - let princ_type = - (Global.lookup_constant princ).Declarations.const_type - in - New_arg_principle.generate_functional_principle - interactive_proof - princ_type - None - None - funs_kn - i - (continue_proof 0 [|funs_kn.(i)|]) - ) - 0 - fix_rec_l - in - () + if do_built + then + begin + let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in + let ind_kn = + fst (locate_with_msg + (pr_reference f_R_mut++str ": Not an inductive type!") + locate_ind + f_R_mut) + in + let fname_kn (fname,_,_,_,_) = + let f_ref = Ident (dummy_loc,fname) in + locate_with_msg + (pr_reference f_ref++str ": Not an inductive type!") + locate_constant + f_ref + in + let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in + let _ = + Util.list_map_i + (fun i x -> + let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in + let princ_type = + (Global.lookup_constant princ).Declarations.const_type + in + New_arg_principle.generate_functional_principle + interactive_proof + princ_type + None + None + funs_kn + i + (continue_proof 0 [|funs_kn.(i)|]) + ) + 0 + fix_rec_l + in + () + end with e -> -(* Pp.msg_warning (Cerrors.explain_exn e) *) - () + Pp.msg_warning (Cerrors.explain_exn e) let register_struct is_rec fixpoint_exprl = @@ -260,8 +267,7 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body = in let fun_from_mes = let applied_mes = - Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) - in + Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) in let wf_rel_from_mes = @@ -270,31 +276,31 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body = register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body - - -let do_generate_principle interactive_proof fixpoint_exprl = +let do_generate_principle register_built interactive_proof fixpoint_exprl = let recdefs = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> let pre_hook = generate_principle + register_built fixpoint_exprl recdefs true false in - register_wf name wf_rel wf_x args types body pre_hook; + if register_built then register_wf name wf_rel wf_x args types body pre_hook; false | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> let pre_hook = generate_principle + register_built fixpoint_exprl recdefs true false in - register_mes name wf_mes wf_x args types body pre_hook; + if register_built then register_mes name wf_mes wf_x args types body pre_hook; false | _ -> let fix_names = @@ -310,7 +316,10 @@ let do_generate_principle interactive_proof fixpoint_exprl = snd (Topconstr.names_of_local_assums args) in - let annot = Util.list_index (Name id) names - 1, Topconstr.CStructRec in + let annot = + try Util.list_index (Name id) names - 1, Topconstr.CStructRec + with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) + in (name,annot,args,types,body),(None:Vernacexpr.decl_notation) | (name,None,args,types,body),recdef -> let names = (Topconstr.names_of_local_assums args) in @@ -331,8 +340,9 @@ let do_generate_principle interactive_proof fixpoint_exprl = List.map (function (name,_,_,_,_) -> name) fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - register_struct is_rec old_fixpoint_exprl; - generate_principle + if register_built then register_struct is_rec old_fixpoint_exprl; + generate_principle + register_built fixpoint_exprl recdefs interactive_proof @@ -343,11 +353,116 @@ let do_generate_principle interactive_proof fixpoint_exprl = in () +let make_graph (id:identifier) = + let c_body = + try + let c = const_of_id id in + Global.lookup_constant c + with Not_found -> + raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) ) + in + + match c_body.const_body with + | None -> error "Cannot build a graph over an axiom !" + | Some b -> + let env = Global.env () in + let body = (force b) in + -(* let do_generate_principle fix_rec_l = *) -(* (\* we first of all checks whether on not all the correct *) -(* assumption are here *) -(* *\) *) -(* let newfixpoint_exprl = List.map compute_annot fix_rec_l in *) -(* (\* we can then register the functions *\) *) -(* register(\* newfixpoint_exprl *\) fix_rec_l *) + let extern_body,extern_type = + let old_implicit_args = Impargs.is_implicit_args () + and old_strict_implicit_args = Impargs.is_strict_implicit_args () + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in + let old_rawprint = !Options.raw_print in + Options.raw_print := true; + Impargs.make_implicit_args false; + Impargs.make_strict_implicit_args false; + Impargs.make_contextual_implicit_args false; + try + let res = Constrextern.extern_constr false env body in + let res' = Constrextern.extern_type false env c_body.const_type in + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Options.raw_print := old_rawprint; + res,res' + with + | UserError(s,msg) as e -> + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Options.raw_print := old_rawprint; + raise e + | e -> + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Options.raw_print := old_rawprint; + raise e + in + let expr_list = + match extern_body with + | Topconstr.CFix(loc,l_id,fixexprl) -> + let l = + List.map + (fun (id,(n,recexp),bl,t,b) -> + let nal = + List.flatten + (List.map + (function + | Topconstr.LocalRawDef (na,_)-> [] + | Topconstr.LocalRawAssum (nal,_) -> nal + ) + bl + ) + in + let rec_id = + match List.nth nal n with |(_,Name id) -> id | _ -> anomaly "" + in + (id, Some (Struct rec_id),bl,t,b) + ) + fixexprl + in + l + | _ -> + let rec get_args b t : Topconstr.local_binder list * + Topconstr.constr_expr * Topconstr.constr_expr = +(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *) +(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *) +(* Pp.msgnl (fnl ()); *) + match b with + | Topconstr.CLambdaN (loc, (nal_ta), b') -> + begin + let n = + (List.fold_left (fun n (nal,_) -> + n+List.length nal) 0 nal_ta ) + in + let rec chop_n_arrow n t = + if n > 0 + then + match t with + | Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t + | Topconstr.CProdN(_,nal_ta',t') -> + let n' = + List.fold_left + (fun n (nal,t'') -> + n+List.length nal) n nal_ta' + in + assert (n'<= n); + chop_n_arrow (n - n') t' + | _ -> anomaly "Not enough products" + else t + in + let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in + (List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' + end + | _ -> [],b,t + in + let nal_tas,b,t = get_args extern_body extern_type in + [(id,None,nal_tas,t,b)] + + in + do_generate_principle false false expr_list +(* let make_graph _ = assert false *) + +let do_generate_principle = do_generate_principle true diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 96d0df5cc..b32dfacb5 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -91,8 +91,11 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t)::acc) (n-1) b - | _ -> raise (Util.UserError("chop_rlambda_n",str "chop_rlambda_n: Not enough Lambdas")) + | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | _ -> + raise (Util.UserError("chop_rlambda_n", + str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli index 03805ddef..ab5195b07 100644 --- a/contrib/funind/indfun_common.mli +++ b/contrib/funind/indfun_common.mli @@ -28,7 +28,7 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Rawterm.rawconstr -> - (name*Rawterm.rawconstr) list * Rawterm.rawconstr + (name*Rawterm.rawconstr*bool) list * Rawterm.rawconstr val chop_rprod_n : int -> Rawterm.rawconstr -> (name*Rawterm.rawconstr) list * Rawterm.rawconstr diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 3caf94b8e..7b3d8cbda 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -12,6 +12,7 @@ open Pp open Topconstr open Indfun_common open Indfun +open Genarg TACTIC EXTEND newfuninv [ "functional" "inversion" ident(hyp) ident(fname) ] -> @@ -21,34 +22,92 @@ TACTIC EXTEND newfuninv END +let pr_fun_ind_using prc _ _ opt_c = + match opt_c with + | None -> mt () + | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ prc c) + +ARGUMENT EXTEND fun_ind_using + TYPED AS constr_opt + PRINTED BY pr_fun_ind_using +| [ "using" constr(c) ] -> [ Some c ] +| [ ] -> [ None ] +END + +let pr_intro_as_pat prc _ _ pat = + str "as" ++ spc () ++ pr_intro_pattern pat + + + + + +ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat +| [ "as" simple_intropattern(ipat) ] -> [ ipat ] +| [] ->[ IntroAnonymous ] +END + + +let is_rec scheme_info = + let test_branche min acc (_,_,br) = + acc || + (let new_branche = Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in + let free_rels_in_br = Termops.free_rels new_branche in + let max = min + scheme_info.Tactics.npredicates in + Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br) + in + Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) + + +let choose_dest_or_ind scheme_info = + if is_rec scheme_info + then Tactics.new_induct + else + Tactics.new_destruct + TACTIC EXTEND newfunind - ["new" "functional" "induction" constr(c) ] -> + ["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] -> [ let f,args = decompose_app c in - let fname = - match kind_of_term f with - | Const c' -> - id_of_label (con_label c') - | _ -> Util.error "Must be used with a function" - in fun g -> - let princ_name = - ( - Indrec.make_elimination_ident - fname - (Tacticals.elimination_sort_of_goal g) - ) - in - let princ = const_of_id princ_name in - let args_as_induction_constr = - List.map (fun c -> Tacexpr.ElimOnConstr c) (args@[c]) - in - let princ' = Some (mkConst princ,Rawterm.NoBindings) in - Tactics.new_induct args_as_induction_constr princ' Genarg.IntroAnonymous g + let princ = + match princl with + | None -> (* No principle is given let's find the good one *) + let fname = + match kind_of_term f with + | Const c' -> + id_of_label (con_label c') + | _ -> Util.error "Must be used with a function" + in + let princ_name = + ( + Indrec.make_elimination_ident + fname + (Tacticals.elimination_sort_of_goal g) + ) + in + mkConst(const_of_id princ_name ) + | Some princ -> princ + in + let princ_type = Tacmach.pf_type_of g princ in + let princ_infos = Tactics.compute_elim_sig princ_type in + let args_as_induction_constr = + let c_list = + if princ_infos.Tactics.farg_in_concl + then [c] else [] + in + List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) + in + let princ' = Some (princ,Rawterm.NoBindings) in + choose_dest_or_ind + princ_infos + args_as_induction_constr + princ' + pat g ] END + VERNAC ARGUMENT EXTEND rec_annotation2 [ "{" "struct" ident(id) "}"] -> [ Struct id ] | [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ] @@ -128,3 +187,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ] END + +VERNAC COMMAND EXTEND NewFunctionalCase + ["New" "Functional" "Case" fun_scheme_arg(fas) ] -> + [ + New_arg_principle.make_case_scheme fas + ] +END + + +VERNAC COMMAND EXTEND GenerateGraph +["Generate" "graph" "for" ident(c)] -> [ make_graph c ] +END diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml index 94af0b957..0c20d4e73 100644 --- a/contrib/funind/new_arg_principle.ml +++ b/contrib/funind/new_arg_principle.ml @@ -15,26 +15,717 @@ open Tactics open Indfun_common -(* let msgnl = Pp.msgnl *) +let msgnl = Pp.msgnl -let observe strm = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then Pp.msgnl strm +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 observe_tac s tac g = - if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then Recdef.do_observe_tac s tac g - else tac g -let tclTRYD tac = - if !Options.debug || Tacinterp.get_debug () <> Tactic_debug.DebugOff - then tclTRY tac +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|]) + + +let congruence g = + observe_tac "finish" +(* (Auto.default_auto) *) +(* (Eauto.gen_eauto false (false,5) [] (Some [])) *) + h_assumption + g + + +let refine c = + if do_observe () + then Tacmach.refine c + else Tacmach.refine_no_check c + +let thin l = + if do_observe () + then Tacmach.thin l + else Tacmach.thin_no_check l + + +let cut_replacing id t tac :tactic= + if do_observe () + then + Tactics.cut_replacing id t (fun _ -> tac ) + else + 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 = cut_replacing hyp_id t tac +(* let prov_id = id_of_string "_____" in *) +(* tclTHENLIST *) +(* [ *) +(* (forward *) +(* (Some (tclCOMPLETE prove_equiv)) *) +(* (Genarg.IntroIdentifier prov_id) *) +(* new_hyp_typ) ; *) +(* clear [hyp_id]; *) +(* rename_hyp prov_id hyp_id *) +(* ] *) + +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 ptes_to_fix 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) ptes_to_fix + else false + else false + +let isLetIn t = + match kind_of_term t with + | LetIn _ -> true + | _ -> false + + +let rec clean_hyp_with_heq fixes_ids ptes_to_fix 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 + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + (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 ptes_to_fix t_x then + begin + let pte,pte_args = (destApp t_x) in + let (_,_,fix_id,_) = Idmap.find (destVar pte) ptes_to_fix 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_hyp_proof = mkApp(mkVar fix_id,array_get_start pte_args) in + let to_refine = + applist(mkVar hyp_id, + List.rev_map mkVar (context_hyps_ids)@[rec_hyp_proof] + ) + in + 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 + fixes_ids ptes_to_fix continue_tac hyps body heq_id + = + 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 fixes_ids ptes_to_fix hyp_id env sigma + in + (tclTHEN hyp_tac hyps_tac),new_hyp@new_hyps + ) + (tclIDTAC,[]) + hyps + in + tclTHENLIST + [ + tac ; + (continue_tac new_hyps body) + ] + g + +let treat_new_case fixes_ids ptes_to_fix nb_prod continue_tac hyps term body = + tclTHENLIST + [ + (* We first introduce the variables *) + tclDO (nb_prod - 1) intro; + (* Then the equation itself *) + intro; + (fun g' -> + (* We get infos on the equations introduced*) + let (heq_id,_,new_term_value_eq) = pf_last_hyp g' 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) body) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + (* and + 1- rewrite heq in all hyps + 2- call the cleanning tactic + *) + let tac_rew hyp_id = + tclTHENLIST + [ h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + (Tacticals.onHyp hyp_id) + ; + tclTRY (Equality.general_rewrite_in true hyp_id (mkVar heq_id)) + ] + in + tclTHENLIST + [ + tclMAP tac_rew hyps; + ( clean_goal_with_heq fixes_ids ptes_to_fix continue_tac hyps new_body heq_id) + ] + g' + ) + ] + +let rec new_do_prove_princ_for_struct + (interactive_proof:bool) + (fnames:constant list) + (ptes:identifier list) + (fixes:(int*constr*identifier*constr) Idmap.t) + (hyps: identifier list) + (term:constr) : tactic = + let fixes_ids = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in + let rec do_prove_princ_for_struct_aux do_finalize hyps term = + fun g -> +(* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) + match kind_of_term term 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]; + pattern_option [[-1],t] None; + 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 + treat_new_case + fixes_ids fixes + nb_instanciate_partial + (do_prove_princ_for_struct do_finalize) + hyps + t + term + 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(term,[|mkVar id|])) in + do_prove_princ_for_struct do_finalize hyps new_term g' + ) g + | _ -> + do_finalize hyps term g + end + | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize hyps t g + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + do_finalize hyps term g + | App(_,_) -> + let f,args = decompose_app term in + begin + match kind_of_term f with + | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ -> + do_prove_princ_for_struct_args do_finalize hyps f args g + | Const c when not (List.mem c fnames) -> + do_prove_princ_for_struct_args do_finalize hyps f args g + | Const _ -> + do_finalize hyps term 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 (Name id,v,t,b) -> + do_prove_princ_for_struct do_finalize hyps (subst1 v b) g + | LetIn(Anonymous,_,_,b) -> + do_prove_princ_for_struct do_finalize hyps (pop b) 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 hyps term g = +(* observe (str "proving with "++Printer.pr_lconstr term++ str " on goal " ++ pr_gls g); *) + do_prove_princ_for_struct_aux do_finalize hyps term g + and do_prove_princ_for_struct_args do_finalize hyps 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 tac = + match args with + | [] -> + do_finalize hyps f_args' + | arg::args -> + let do_finalize hyps new_arg = + tclTRYD + (do_prove_princ_for_struct_args + do_finalize + hyps + (mkApp(f_args',[|new_arg|])) + args + ) + in + do_prove_princ_for_struct do_finalize hyps arg + in + tclTRYD(tac ) g + in + do_prove_princ_for_struct (fun hyps term -> congruence) hyps term + + + + + + + + + + + + + + + + + + + + + + + + + type rewrite_dir = | LR | RL @@ -53,6 +744,49 @@ let rew_all ?(rev_order=false) lr : tactic = pf_hyps (fun l -> tclMAP (fun (id,_,_) -> tclTRY (rew (mkVar id))) (order l)) g +let rew_all_in_list ?(rev_order=false) idl lr : tactic = + let rew = + match lr with + | LR -> Equality.rewriteLR + | RL -> Equality.rewriteRL + in + let order = + if rev_order then List.rev else fun x -> x + in + fun g -> + tclMAP (fun id -> tclTRY (rew (mkVar id))) (order idl) g + + +let rewrite_and_try_tac ?(rev_order=false) lr tac eqs : tactic = + let rew = + match lr with + | LR -> Equality.rewriteLR + | RL -> Equality.rewriteRL + in + let order = + if rev_order then List.rev else fun x -> x + in + let rec rewrite_and_try_tac = function + | [] -> tclCOMPLETE tac + | id::idl -> + let other_tac = rewrite_and_try_tac idl in + tclFIRST + [ + other_tac; + + + tclTHEN + (rew (mkVar id)) + (tclFIRST + [ + other_tac; + tclCOMPLETE tac + ] + ) + ] + in + rewrite_and_try_tac (order eqs) + let test_var args arg_num = @@ -115,11 +849,7 @@ let rewrite_until_var arg_num : tactic = -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|]) - -let case_eq tac body term g = +let case_eq tac eqs body term g = (* msgnl (str "case_eq on " ++ pr_lconstr_env (pf_env g) term); *) let type_of_term = pf_type_of g term in let term_eq = @@ -130,7 +860,7 @@ let case_eq tac body term g = tclTHENSEQ [intro_patterns [](* ba.branchnames *); fun g -> - let (_,_,new_term_value_eq) = pf_last_hyp g in + let (id,_,new_term_value_eq) = pf_last_hyp g in let new_term_value = match kind_of_term new_term_value_eq with | App(f,[| _;_;args2 |]) -> args2 @@ -144,7 +874,7 @@ let case_eq tac body term g = mkLambda(Anonymous,type_of_term,replace_term term (mkRel 1) body) in let new_body = mkApp(fun_body,[| new_term_value |]) in - tac (pf_nf_betaiota g new_body) g + tac (pf_nf_betaiota g new_body) (id::eqs) g ] g in @@ -160,75 +890,98 @@ let case_eq tac body term g = -let my_reflexivity : tactic = - let test_eq = - lazy (eq_constr (Coqlib.build_coq_eq ())) - in - let build_reflexivity = - lazy (fun ty t -> mkApp((Coqlib.build_coq_eq_data ()).Coqlib.refl,[|ty;t|])) - in - fun g -> - begin - match kind_of_term (pf_concl g) with - | App(eq,[|ty;t1;t2|]) when (Lazy.force test_eq) eq -> - if not (Termops.occur_existential t1) - then tclTHEN (h_change None (mkApp(eq,[|ty;t1;t1|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t1)) - else if not (Termops.occur_existential t2) - then tclTHEN (h_change None (mkApp(eq,[|ty;t2;t2|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t2)) - else tclFAIL 0 (str "") +(* let my_reflexivity : tactic = *) +(* let test_eq = *) +(* lazy (eq_constr (Coqlib.build_coq_eq ())) *) +(* in *) +(* let build_reflexivity = *) +(* lazy (fun ty t -> mkApp((Coqlib.build_coq_eq_data ()).Coqlib.refl,[|ty;t|])) *) +(* in *) +(* fun g -> *) +(* begin *) +(* match kind_of_term (pf_concl g) with *) +(* | App(eq,[|ty;t1;t2|]) when (Lazy.force test_eq) eq -> *) +(* if not (Termops.occur_existential t1) *) +(* then tclTHEN (h_change None (mkApp(eq,[|ty;t1;t1|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t1)) *) +(* else if not (Termops.occur_existential t2) *) +(* then tclTHEN (h_change None (mkApp(eq,[|ty;t2;t2|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t2)) *) +(* else tclFAIL 0 (str "") *) - | _ -> tclFAIL 0 (str "") - end g +(* | _ -> tclFAIL 0 (str "") *) +(* end g *) -let eauto g = - tclFIRST +let eauto : tactic = + fun g -> + tclFIRST [ Eauto.e_assumption ; h_exact (Coqlib.build_coq_I ()); - tclTHEN - (rew_all LR) - (Eauto. gen_eauto false (false,5) [] (Some [])) + tclCOMPLETE + (Eauto.gen_eauto false (false,1) [] (Some [])) ] g - +let do_eauto eqs :tactic = + tclFIRST + [ +(* rewrite_and_try_tac LR eauto eqs; *) +(* rewrite_and_try_tac RL eauto eqs; *) + rewrite_and_try_tac ~rev_order:true LR eauto eqs; +(* rewrite_and_try_tac ~rev_order:true RL eauto eqs *) + ] -let conclude fixes g = +let conclude fixes eqs g = (* let clear_fixes = *) (* let l = Idmap.fold (fun _ (_,_,id,_) acc -> id::acc) fixes [] in *) (* h_clear false l *) (* in *) - match kind_of_term (pf_concl g) with - | App(pte,args) -> - let tac = - if isVar pte - then - try + match kind_of_term (pf_concl g) with + | App(pte,args) -> + let tac = + if isVar pte + then + try let idxs,body,this_fix_id,new_type = Idmap.find (destVar pte) fixes - in - let idx = idxs - 1 in - tclTHEN + in + let idx = idxs - 1 in + tclTHEN (rewrite_until_var idx) - (* If we have an IH then with use the fixpoint *) - (Eauto.e_resolve_constr (mkVar this_fix_id)) - (* And left the generated subgoals to eauto *) - with Not_found -> (* this is not a pte *) + (* If we have an IH then with use the fixpoint *) + (Eauto.e_resolve_constr (mkVar this_fix_id)) + (* And left the generated subgoals to eauto *) + with Not_found -> (* this is not a pte *) tclIDTAC - else tclIDTAC - in - tclTHENSEQ [tac; (* clear_fixes; *) eauto] g - | _ -> eauto g + else tclIDTAC + in + tclTHENSEQ [tac; do_eauto eqs ] + g + | _ -> do_eauto eqs g - -let finalize_proof interactive_proof fixes hyps fnames term = - tclORELSE + +let finalize_proof interactive_proof fixes hyps fnames term eqs = + tclORELSE ( - tclFIRST - (List.map - (fun id -> tclTHEN (Eauto.e_resolve_constr (mkVar id)) - (tclCOMPLETE (conclude fixes))) hyps - ) + tclFIRST +(* ( *) +(* (List.map *) +(* (fun id -> tclTHEN (Eauto.e_resolve_constr (mkVar id)) *) +(* (tclCOMPLETE (conclude fixes eqs))) hyps *) +(* )@ *) + (List.map + (fun id -> + let tac = + tclTHENLIST + [ + (Eauto.e_resolve_constr (mkVar id)); + (tclCOMPLETE (conclude fixes eqs)) + ] + in + rewrite_and_try_tac RL tac eqs + ) + hyps + ) + ) (if interactive_proof then tclIDTAC else tclFAIL 0 (str "")) @@ -239,18 +992,18 @@ let do_prove_princ_for_struct interactive_proof (* (rec_pos:int option) *) (fnames:constant list) (ptes:identifier list) (fixes:(int*constr*identifier*constr) Idmap.t) (hyps: identifier list) (term:constr) : tactic = - let finalize_proof term = - finalize_proof (* rec_pos *) interactive_proof fixes hyps fnames term + let finalize_proof term eqs = + finalize_proof (* rec_pos *) interactive_proof fixes hyps fnames term eqs in - let rec do_prove_princ_for_struct do_finalize term g = + let rec do_prove_princ_for_struct do_finalize term eqs g = (* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) (* then msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *) let tac = fun g -> match kind_of_term term with | Case(_,_,t,_) -> - observe_tac "case_eq" - (case_eq (do_prove_princ_for_struct do_finalize) term t) g + observe_tac "case_eq" + (case_eq (do_prove_princ_for_struct do_finalize) eqs term t) g | Lambda(n,t,b) -> begin match kind_of_term( pf_concl g) with @@ -260,35 +1013,38 @@ let do_prove_princ_for_struct interactive_proof (fun g' -> let (id,_,_) = pf_last_hyp g' in let new_term = pf_nf_betaiota g' (mkApp(term,[|mkVar id|])) in - do_prove_princ_for_struct do_finalize new_term g' + do_prove_princ_for_struct do_finalize new_term eqs g' ) g | _ -> - do_finalize term g + do_finalize term eqs g end - | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize t g + | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize t eqs g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> - do_finalize term g + do_finalize term eqs g | App(_,_) -> let f,args = decompose_app term in begin match kind_of_term f with | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ -> - do_prove_princ_for_struct_args do_finalize f args g + do_prove_princ_for_struct_args do_finalize f args eqs g | Const c when not (List.mem c fnames) -> - do_prove_princ_for_struct_args do_finalize f args g + do_prove_princ_for_struct_args do_finalize f args eqs g | Const _ -> - do_finalize term g + do_finalize term eqs g | _ -> - msg_warning (str "Applied binders not yet implemented: "++ Printer.pr_lconstr_env (pf_env g) term) ; - tclFAIL 0 (str "TODO") 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 (Name id,v,t,b) -> - do_prove_princ_for_struct do_finalize (subst1 v b) g + do_prove_princ_for_struct do_finalize (subst1 v b) eqs g | LetIn(Anonymous,_,_,b) -> - do_prove_princ_for_struct do_finalize (pop b) g + do_prove_princ_for_struct do_finalize (pop b) eqs g | _ -> errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *) (* pr_lconstr_env (pf_env g) term *) @@ -296,7 +1052,7 @@ let do_prove_princ_for_struct interactive_proof in tac g - and do_prove_princ_for_struct_args do_finalize f_args' args :tactic = + and do_prove_princ_for_struct_args do_finalize f_args' args eqs :tactic = fun g -> (* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) (* then msgnl (str "do_prove_princ_for_struct_args with " ++ *) @@ -307,22 +1063,42 @@ let do_prove_princ_for_struct interactive_proof | [] -> do_finalize f_args' | arg::args -> - let do_finalize new_arg = + let do_finalize new_arg eqs = tclTRYD (do_prove_princ_for_struct_args do_finalize (mkApp(f_args',[|new_arg|])) args + eqs ) in do_prove_princ_for_struct do_finalize arg in - tclTRYD(tac) g + tclTRYD(tac eqs) g in do_prove_princ_for_struct (finalize_proof) term + [] + + +let do_prove_princ_for_struct + (interactive_proof:bool) + (fnames:constant list) + (ptes:identifier list) + (fixes:(int*constr*identifier*constr) Idmap.t) + (hyps: identifier list) + (term:constr) + = + observe (str "start_proof"); + new_do_prove_princ_for_struct + (interactive_proof:bool) + (fnames:constant list) + (ptes:identifier list) + (fixes:(int*constr*identifier*constr) Idmap.t) + (hyps: identifier list) + (term:constr) let is_pte_type t = isSort (snd (decompose_prod t)) @@ -331,13 +1107,55 @@ 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] + ) + ( (* + 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 do_prove hyps + else + tclTHEN + (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 : " ++ - Printer.pr_lconstr (mkConst fnames.(fun_num))); - let princ_type = pf_concl goal in + 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 = + let get_body const = match (Global.lookup_constant const ).const_body with | Some b -> let body = force b in @@ -349,83 +1167,83 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : | 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 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 + 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 -> + 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 + 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 avoid = ref avoid in let res = list_fold_left_i - (fun i acc pte_id -> - let this_fix_id = fresh_id !avoid "fix___" in + (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 this_body = substl (List.rev (Array.to_list all_funs)) ca.(i) in - let new_type = prod_applist typearray.(i) true_params + let this_body = substl (List.rev (Array.to_list all_funs)) ca.(i) in + let new_type = prod_applist typearray.(i) true_params and new_body = Reductionops.nf_beta (applist(this_body,true_params)) in - let new_type_args,_ = decompose_prod new_type in + let new_type_args,_ = decompose_prod new_type in let nargs = List.length new_type_args in - let pte_args = + let pte_args = (* let rev_args = List.rev_map (fun (id,_,_) -> mkVar id) new_type_args in *) - let f = applist(all_funs.(i),true_params) in - let app_f = mkApp(f,Array.init nargs (fun i -> mkRel(nargs - i))) 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 = idxs.(i) - offset + 1,new_body,this_fix_id ,new_type 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 = idxs.(i) - offset + 1,new_body,this_fix_id ,new_type in pte_to_fix := Idmap.add pte_id fix_info !pte_to_fix; fix_info::acc ) - 0 + 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 + 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 + let offset = List.length params' in + let not_real_param,true_params = + list_chop ((List.length !params ) - offset) !params in params := true_params; args := not_real_param; - observe (str "mk_fixes : params are "++ - prlist_with_sep spc - (fun id -> Printer.pr_lconstr (mkVar id)) - !params - ); - let new_avoid,infos = +(* 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 + (build_pte_to_fix offset (List.map mkVar !params) (List.rev !predicates) @@ -434,24 +1252,24 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : ((pf_ids_of_hyps g),[]) in let pre_info,infos = list_chop fun_num infos in - match pre_info,infos with - | [],[] -> tclIDTAC g - | _,(idx,_,fix_id,_)::infos' -> - let other_fix_info = + match pre_info,infos with + | [],[] -> tclIDTAC g + | _,(idx,_,fix_id,_)::infos' -> + let other_fix_info = List.map (fun (idx,_,fix_id,fix_typ) -> fix_id,idx,fix_typ) (pre_info@infos') in - tclORELSE - (h_mutual_fix fix_id idx other_fix_info) + tclORELSE + (h_mutual_fix fix_id idx other_fix_info) (tclFAIL 1000 (str "bad index" ++ str (string_of_int idx) ++ str "offset := " ++ (str (string_of_int offset)))) g | _,[] -> anomaly "Not a valid information" in - let do_prove pte_to_fix args : tactic = - fun g -> - match kind_of_term (pf_concl g) with - | App(pte,pte_args) when isVar pte -> + let do_prove pte_to_fix args branches : tactic = + fun g -> + match kind_of_term (pf_concl g) with + | App(pte,pte_args) when isVar pte -> begin let pte = destVar pte in try @@ -461,46 +1279,46 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : 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 "" + 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 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 + Reductionops.nf_beta (applist(new_body,List.rev args_as_constr)) in - let do_prove = + let do_prove = do_prove_princ_for_struct interactive_proof (Array.to_list fnames) !predicates pte_to_fix - !branches - applied_body + branches + applied_body in - let replace_and_prove = + let replace_and_prove = tclTHENS - (fun g -> - observe (str "replacing " ++ - Printer.pr_lconstr_env (pf_env g) (array_last pte_args) ++ - str " with " ++ - Printer.pr_lconstr_env (pf_env g) applied_body ++ - str " rec_arg_num is " ++ str (string_of_int rec_num) - ); + (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 ) [ do_prove; - try + try let id = List.nth (List.rev args_as_constr) (rec_num) in - observe (str "choosen var := "++ Printer.pr_lconstr id); +(* observe (str "choosen var := "++ pr_lconstr id); *) (tclTHENSEQ [(h_simplest_case id); Tactics.intros_reflexivity @@ -509,18 +1327,18 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : ] 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 "doing replacement" ( replace_and_prove)) g + with Not_Rec -> + let fname = destConst (fst (decompose_app (array_last pte_args))) in + tclTHEN + (unfold_in_concl [([],Names.EvalConstRef fname)]) (observe_tac "" (fun g' -> do_prove_princ_for_struct interactive_proof (Array.to_list fnames) !predicates pte_to_fix - !branches + branches (array_last (snd (destApp (pf_concl g')))) g' )) @@ -528,17 +1346,38 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : end | _ -> assert false in - tclTHENSEQ + 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 args = ref [] in *) +(* tclTHENLIST *) +(* [ *) +(* (fun g -> observe_tac "introducing args" (intro_with_remembrance args princ_info.nargs) g); *) +(* (fun g -> observe_tac "instanciating rec hyps" (instanciate_hyps_with_args !branches (List.rev !args)) g); *) +(* (fun g -> observe_tac "proving" (fun g -> do_prove !pte_to_fix !args g) g) *) +(* ] *) +(* g *) +(* ) *) (fun g -> - let args = ref [] in - tclTHEN - (fun g -> observe_tac "introducing args" (intro_with_remembrance args princ_info.nargs) g) - (fun g -> observe_tac "proving" (fun g -> do_prove !pte_to_fix !args g) g) + 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 ) ] @@ -551,8 +1390,17 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _naprams : - - + + + + + + + + + + + @@ -620,8 +1468,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | _ -> assert false in let dummy_var = mkVar (id_of_string "________") in - let mk_replacement i args = - mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) + 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 @@ -646,7 +1496,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | App(f,args) when is_dom f -> let var_to_be_removed = destRel (array_last args) in let num = get_fun_num f in - raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement num args)) + 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 @@ -665,19 +1515,22 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ([],[]) in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - mkApp(new_f,Array.of_list new_args), + 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 -(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *) -(* then *) -(* Pp.msgnl (str "compute_new_princ_type for "++ *) -(* pr_lconstr_env env pre_princ ++ *) -(* str" is "++ *) -(* pr_lconstr_env env new_princ_type); *) - res +(* 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 @@ -741,7 +1594,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc in -(* Pp.msgnl (Printer.pr_lconstr_env env_with_params_and_predicates pre_princ); *) +(* 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 @@ -773,6 +1626,71 @@ let change_property_sort toSort princ princName = 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 @@ -792,10 +1710,8 @@ let generate_functional_principle (Array.map mkConst funs) new_sorts old_princ_type - in -(* let tim2 = Sys.time () in *) -(* Pp.msgnl (str ("Time to compute type: ") ++ str (string_of_float (tim2 -. tim1))) ; *) -(* msgnl (str "new principle type :"++ pr_lconstr new_principle_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 @@ -803,6 +1719,7 @@ let generate_functional_principle 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 @@ -813,7 +1730,7 @@ let generate_functional_principle let value = change_property_sort s new_principle_type new_princ_name in -(* Pp.msgnl (str "new principle := " ++ Printer.pr_lconstr value); *) +(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = { const_entry_body = value; const_entry_type = None; @@ -827,10 +1744,11 @@ let generate_functional_principle (Entries.DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme) ) - ) + ); + names := name :: !names in - register_with_sort InSet; - register_with_sort InProp + register_with_sort InProp; + register_with_sort InSet in begin Command.start_proof @@ -840,13 +1758,43 @@ let generate_functional_principle hook ; try -(* let tim1 = Sys.time () in *) + let tim1 = System.get_time () in Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); -(* let tim2 = Sys.time () in *) -(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float (tim2 -. tim1))); *) - let do_save = Tacinterp.get_debug () = Tactic_debug.DebugOff && not interactive_proof in - if do_save then Options.silently Command.save_named false - + let tim2 = System.get_time () in + let _ = if do_observe () + then + begin + let dur1 = System.time_difference tim1 tim2 in + Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); + end + in + 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 + if do_observe () + then + 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))); *) @@ -857,7 +1805,7 @@ let generate_functional_principle ( Cerrors.explain_exn e ); - if Tacinterp.get_debug () = Tactic_debug.DebugOff + if not ( do_observe ()) then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end end @@ -916,17 +1864,22 @@ let get_funs_constant mp dp = in (* The bodies has to be very similar *) let _check_bodies = - let extract_info body = - match kind_of_term body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) - | _ -> error "Not a mutal recursive block" - in - let first_infos = extract_info (List.hd l_bodies) in - let check body = (* Hope this is correct *) - if not (first_infos = (extract_info body)) - then error "Not a mutal recursive block" - in - List.iter check l_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 @@ -962,7 +1915,7 @@ let make_scheme fas = ) funs_indexes in - let l_schemes = Indrec.build_mutual_indrec env sigma ind_list 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) -> @@ -970,21 +1923,71 @@ let make_scheme fas = ) 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 " ++ - Printer.pr_lconstr scheme_type); - generate_functional_principle +(* 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 - (Typing.type_of env sigma scheme_type) + scheme_type (Some (Array.of_list sorts)) (Some princ_name) this_block_funs - !i + !i (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) ) - (List.map (fun (x,_,_) -> x) fas) + 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 + () diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli index ad71ebd05..cad68da67 100644 --- a/contrib/funind/new_arg_principle.mli +++ b/contrib/funind/new_arg_principle.mli @@ -31,3 +31,4 @@ val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array -> Term.types -> Term.types val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list -> unit +val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) -> unit diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 48bbce6c7..327198b91 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -8,6 +8,14 @@ open Indfun_common open Util open Rawtermops +let observe strm = + if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false + then Pp.msgnl strm + else () +let observennl strm = + if Tacinterp.get_debug () <> Tactic_debug.DebugOff &&false + then Pp.msg strm + else () (* type binder_type = *) (* | Lambda *) @@ -44,7 +52,7 @@ let compose_raw_context = (* The main part deals with building a list of raw constructor expressions - from a rhs of a fixpoint equation. + from the rhs of a fixpoint equation. *) @@ -325,6 +333,75 @@ let make_discr_match brl = make_discr_match_brl i brl) + +let rec make_pattern_eq_precond id e pat : identifier * (binder_type * Rawterm.rawconstr) list = + match pat with + | PatVar(_,Anonymous) -> assert false + | PatVar(_,Name x) -> + id,[Prod (Name x),mkRHole ();Prod Anonymous,raw_make_eq (mkRVar x) e] + | PatCstr(_,constr,patternl,_) -> + let new_id,new_patternl,patternl_eq_precond = + List.fold_right + (fun pat' (id,new_patternl,preconds) -> + match pat' with + | PatVar (_,Name id) -> (id,id::new_patternl,preconds) + | _ -> + let new_id = Nameops.lift_ident id in + let new_id',pat'_precond = + make_pattern_eq_precond new_id (mkRVar id) pat' + in + (new_id',id::new_patternl,preconds@pat'_precond) + ) + patternl + (id,[],[]) + in + let cst_narg = + Inductiveops.mis_constructor_nargs_env + (Global.env ()) + constr + in + let implicit_args = + Array.to_list + (Array.init + (cst_narg - List.length patternl) + (fun _ -> mkRHole ()) + ) + in + let cst_as_term = + mkRApp(mkRRef(Libnames.ConstructRef constr), + implicit_args@(List.map mkRVar new_patternl) + ) + in + let precond' = + (Prod Anonymous, raw_make_eq cst_as_term e)::patternl_eq_precond + in + let precond'' = + List.fold_right + (fun id acc -> + (Prod (Name id),(mkRHole ()))::acc + ) + new_patternl + precond' + in + new_id,precond'' + +let pr_name = function + | Name id -> Ppconstr.pr_id id + | Anonymous -> str "_" + +let make_pattern_eq_precond id e pat = + let res = make_pattern_eq_precond id e pat in + observe + (prlist_with_sep spc + (function (Prod na,t) -> + str "forall " ++ pr_name na ++ str ":" ++ pr_rawconstr t + | _ -> assert false + ) + (snd res) + ); + res + + let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = (* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *) match rt with @@ -400,9 +477,14 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return = | RProd _ -> error "Cannot apply a type" end | RLambda(_,n,t,b) -> - let b_res = build_entry_lc funnames avoid b in + let b_res = build_entry_lc funnames avoid b in let t_res = build_entry_lc funnames avoid t in - combine_results (combine_lam n) t_res b_res + let new_n = + match n with + | Name _ -> n + | Anonymous -> Name (Indfun_common.fresh_id [] "_x") + in + combine_results (combine_lam new_n) t_res b_res | RProd(_,n,t,b) -> let b_res = build_entry_lc funnames avoid b in let t_res = build_entry_lc funnames avoid t in @@ -485,42 +567,55 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo avoid matched_expr in - let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in +(* let ids = List.map (fun id -> Prod (Name id),mkRHole ()) idl in *) let those_pattern_preconds = - ( +( List.flatten + ( List.map2 - (fun pat e -> - let pat_as_term = pattern_to_term pat in - (Prod Anonymous,raw_make_eq pat_as_term e) + (fun pat e -> + let this_pat_ids = ids_of_pat pat in + let pat_as_term = pattern_to_term pat in + List.fold_right + (fun id acc -> + if Idset.mem id this_pat_ids + then (Prod (Name id),mkRHole ())::acc + else acc + + ) + idl + [(Prod Anonymous,raw_make_eq pat_as_term e)] ) patl matched_expr.value ) +) @ - ( if List.exists (function (unifl,neql) -> - let (unif,eqs) = - List.split (List.map2 (fun x y -> x y) unifl patl) - in - List.for_all (fun x -> x) unif) patterns_to_prevent - then - let i = List.length patterns_to_prevent in - [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i )] - else - [] - ) + (if List.exists (function (unifl,neql) -> + let (unif,eqs) = + List.split (List.map2 (fun x y -> x y) unifl patl) + in + List.for_all (fun x -> x) unif) patterns_to_prevent + then + let i = List.length patterns_to_prevent in + [(Prod Anonymous,make_discr (List.map pattern_to_term patl) i )] + else + [] + ) in let return_res = build_entry_lc funname new_avoid return in let this_branch_res = List.map (fun res -> { context = - matched_expr.context@ids@those_pattern_preconds@res.context ; + matched_expr.context@ +(* ids@ *) + those_pattern_preconds@res.context ; value = res.value} ) return_res.result in { brl'_res with result = this_branch_res@brl'_res.result } - + let is_res id = try @@ -528,9 +623,9 @@ let is_res id = with Invalid_argument _ -> false (* rebuild the raw constructors expression. - eliminates some meaningless equality, applies some rewrites...... + eliminates some meaningless equalities, applies some rewrites...... *) -let rec rebuild_cons relname args crossed_types rt = +let rec rebuild_cons nb_args relname args crossed_types depth rt = match rt with | RProd(_,n,t,b) -> let not_free_in_t id = not (is_free_in id t) in @@ -541,7 +636,12 @@ let rec rebuild_cons relname args crossed_types rt = begin match args' with | (RVar(_,this_relname))::args' -> - let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in + let new_b,id_to_exclude = + rebuild_cons + nb_args relname + args new_crossed_types + (depth + 1) b + in let new_t = mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) in mkRProd(n,new_t,new_b), @@ -553,7 +653,7 @@ let rec rebuild_cons relname args crossed_types rt = when eq_as_ref = Lazy.force Coqlib.coq_eq_ref -> let is_in_b = is_free_in id b in - let keep_eq = + let _keep_eq = not (List.exists (is_free_in id) args) || is_in_b || List.exists (is_free_in id) crossed_types in @@ -561,36 +661,70 @@ let rec rebuild_cons relname args crossed_types rt = let subst_b = if is_in_b then b else replace_var_by_term id rt b in - let new_b,id_to_exclude = rebuild_cons relname new_args new_crossed_types subst_b in - if keep_eq then mkRProd(n,t,new_b),id_to_exclude - else new_b, Idset.add id id_to_exclude + let new_b,id_to_exclude = + rebuild_cons + nb_args relname + new_args new_crossed_types + (depth + 1) subst_b + in + mkRProd(n,t,new_b),id_to_exclude +(* if keep_eq then *) +(* mkRProd(n,t,new_b),id_to_exclude *) +(* else new_b, Idset.add id id_to_exclude *) | _ -> - let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in + let new_b,id_to_exclude = + rebuild_cons + nb_args relname + args new_crossed_types + (depth + 1) b + in match n with - | Name id when Idset.mem id id_to_exclude -> + | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude end | RLambda(_,n,t,b) -> begin - let not_free_in_t id = not (is_free_in id t) in - let new_crossed_types = t :: crossed_types in - let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in +(* let not_free_in_t id = not (is_free_in id t) in *) +(* let new_crossed_types = t :: crossed_types in *) +(* let new_b,id_to_exclude = rebuild_cons relname args new_crossed_types b in *) +(* match n with *) +(* | Name id when Idset.mem id id_to_exclude -> *) +(* new_b, *) +(* Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) +(* | _ -> *) +(* RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude *) + let not_free_in_t id = not (is_free_in id t) in + let new_crossed_types = t :: crossed_types in +(* let new_b,id_to_exclude = rebuild_cons relname (args new_crossed_types b in *) match n with - | Name id when Idset.mem id id_to_exclude -> - new_b, - Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> - RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | Name id -> + let new_b,id_to_exclude = + rebuild_cons + nb_args relname + (args@[mkRVar id])new_crossed_types + (depth + 1 ) b + in + if Idset.mem id id_to_exclude && depth >= nb_args + then + new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + else + RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | _ -> anomaly "Should not have an anonymous function here" + (* We have renamed all the anonymous functions during alpha_renaming phase *) + end | RLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_b,id_to_exclude = - rebuild_cons relname args (t::crossed_types) b in + rebuild_cons + nb_args relname + args (t::crossed_types) + (depth + 1 ) b in match n with - | Name id when Idset.mem id id_to_exclude -> + | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) | _ -> RLetIn(dummy_loc,n,t,new_b), Idset.filter not_free_in_t id_to_exclude @@ -600,10 +734,17 @@ let rec rebuild_cons relname args crossed_types rt = begin let not_free_in_t id = not (is_free_in id t) in let new_t,id_to_exclude' = - rebuild_cons relname args (crossed_types) t + rebuild_cons + nb_args + relname + args (crossed_types) + depth t in let new_b,id_to_exclude = - rebuild_cons relname args (t::crossed_types) b + rebuild_cons + nb_args relname + args (t::crossed_types) + (depth + 1) b in (* match n with *) (* | Name id when Idset.mem id id_to_exclude -> *) @@ -617,6 +758,14 @@ let rec rebuild_cons relname args crossed_types rt = | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty +let rebuild_cons nb_args relname args crossed_types rt = + observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ + str "nb_args := " ++ str (string_of_int nb_args)); + let res = + rebuild_cons nb_args relname args crossed_types 0 rt + in + observe (str " leads to "++ pr_rawconstr (fst res)); + res let rec compute_cst_params relnames params = function | RRef _ | RVar _ | REvar _ | RPatVar _ -> params @@ -636,12 +785,12 @@ let rec compute_cst_params relnames params = function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_) as param)::params',(RVar(_,id'))::rtl' - when id_ord id id' == 0 -> + | ((Name id,_,is_defined) as param)::params',(RVar(_,id'))::rtl' + when id_ord id id' == 0 && not is_defined -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames args csts = +let compute_params_name relnames (args : (Names.name * Rawterm.rawconstr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -656,11 +805,11 @@ let compute_params_name relnames args csts = let _ = try list_iter_i - (fun i ((n,nt) as param) -> + (fun i ((n,nt,is_defined) as param) -> if array_for_all (fun l -> - let (n',nt') = List.nth l i in - n = n' && Topconstr.eq_rawconstr nt nt') + let (n',nt',is_defined') = List.nth l i in + n = n' && Topconstr.eq_rawconstr nt nt' && is_defined = is_defined') rels_params then l := param::!l @@ -671,9 +820,26 @@ let compute_params_name relnames args csts = in List.rev !l +(* (Topconstr.CProdN + (dummy_loc, + [[(dummy_loc,Anonymous)],returned_types.(i)], + Topconstr.CSort(dummy_loc, RProp Null ) + ) + ) +*) +let rec rebuild_return_type rt = + match rt with + | Topconstr.CProdN(loc,n,t') -> + Topconstr.CProdN(loc,n,rebuild_return_type t') + | Topconstr.CArrow(loc,t,t') -> + Topconstr.CArrow(loc,t,rebuild_return_type t') + | Topconstr.CLetIn(loc,na,t,t') -> + Topconstr.CLetIn(loc,na,t,rebuild_return_type t') + | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc, RProp Null)) -let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr list) = +let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list) returned_types (rtl:rawconstr list) = +(* Pp.msgnl (prlist_with_sep fnl Printer.pr_rawconstr rtl); *) let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in let funnames = Array.of_list funnames in let funsargs = Array.of_list funsargs in @@ -687,14 +853,18 @@ let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr List.map (function result (* (args',concl') *) -> let rt = compose_raw_context result.context result.value in + let nb_args = List.length funsargs.(i) in (* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *) fst ( - rebuild_cons relnames.(i) - (List.map (function - (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__") - | Name id, _ -> mkRVar id - ) - funsargs.(i)) + rebuild_cons nb_args relnames.(i) +(* (List.map *) +(* (function *) +(* (Anonymous,_,_) -> mkRVar(fresh_id res.to_avoid "x__") *) +(* | Name id, _,_ -> mkRVar id *) +(* ) *) +(* funsargs.(i) *) +(* ) *) + [] [] rt ) @@ -723,29 +893,41 @@ let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr rel_constructors in let rel_arity i funargs = - let rel_first_args :(Names.name * Rawterm.rawconstr) list = (snd (list_chop nrel_params funargs)) in + let rel_first_args :(Names.name * Rawterm.rawconstr * bool ) list = + (snd (list_chop nrel_params funargs)) + in List.fold_right - (fun (n,t) acc -> - Topconstr.CProdN + (fun (n,t,is_defined) acc -> + if is_defined + then + Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_rawconstr Idset.empty t, + acc) + else + Topconstr.CProdN (dummy_loc, [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t], acc ) ) rel_first_args - (Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,Anonymous)],returned_types.(i)], - Topconstr.CSort(dummy_loc, RProp Null ) - ) - ) + (rebuild_return_type returned_types.(i)) +(* (Topconstr.CProdN *) +(* (dummy_loc, *) +(* [[(dummy_loc,Anonymous)],returned_types.(i)], *) +(* Topconstr.CSort(dummy_loc, RProp Null ) *) +(* ) *) +(* ) *) in let rel_arities = Array.mapi rel_arity funsargs in let old_rawprint = !Options.raw_print in Options.raw_print := true; let rel_params = List.map - (fun (n,t) -> + (fun (n,t,is_defined) -> + if is_defined + then + Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t) + else Topconstr.LocalRawAssum ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t) ) @@ -764,33 +946,29 @@ let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr rel_params, rel_arities.(i), ext_rel_constructors - in - let rel_inds = Array.to_list (Array.mapi rel_ind ext_rels_constructors) in -(* msgnl ( *) -(* match rel_ind with *) -(* (_,id),_,params,ar,constr -> *) -(* str "Inductive" ++ spc () ++ Ppconstr.pr_id id ++ *) -(* spc () ++ *) -(* prlist_with_sep *) -(* spc *) -(* (function *) -(* | (Topconstr.LocalRawAssum([_,n],t)) -> *) -(* str "(" ++ Ppconstr.pr_name n ++ str":" ++ *) -(* Ppconstr.pr_type t ++ str ")" *) -(* | _ -> assert false *) -(* ) *) -(* params ++ *) -(* spc () ++ str ":" ++ spc () ++ *) -(* Ppconstr.pr_type rel_arity ++ *) -(* spc () ++ str ":=" ++ spc () ++ *) -(* prlist_with_sep *) -(* (fun () -> fnl () ++ spc () ++ str "|" ++ spc ()) *) -(* (function (_,((_,id),t)) -> *) -(* Ppconstr.pr_id id ++ spc () ++ str ":"++spc () ++ *) -(* Ppconstr.pr_type t *) -(* ) *) -(* ext_rel_constructors *) -(* ); *) + in + let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in + let rel_inds = Array.to_list ext_rel_constructors in + let _ = + observe ( + str "Inductive" ++ spc () ++ + prlist_with_sep + (fun () -> fnl ()++spc () ++ str "with" ++ spc ()) + (function ((_,id),_,params,ar,constr) -> + Ppconstr.pr_id id ++ spc () ++ + Ppconstr.pr_binders params ++ spc () ++ + str ":" ++ spc () ++ + Ppconstr.pr_lconstr_expr ar ++ spc () ++ + prlist_with_sep + (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) + (function (_,((_,id),t)) -> + Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ + Ppconstr.pr_lconstr_expr t) + constr + ) + rel_inds + ) + in let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in @@ -809,24 +987,26 @@ let build_inductive parametrize funnames funsargs returned_types (rtl:rawconstr Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Options.raw_print := old_rawprint; + let msg = + str "while trying to define"++ spc () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + msg + in + observe (msg); raise - (UserError(s, - str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ - msg - ) - ) + (UserError(s, msg)) | e -> Impargs.make_implicit_args old_implicit_args; Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Options.raw_print := old_rawprint; + let msg = + str "while trying to define"++ spc () ++ + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ + Cerrors.explain_exn e + in + observe msg; raise - (UserError("", - str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++ - Cerrors.explain_exn e - ) - ) + (UserError("",msg)) diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli index 8119cd674..0cda56dff 100644 --- a/contrib/funind/rawterm_to_relation.mli +++ b/contrib/funind/rawterm_to_relation.mli @@ -9,7 +9,7 @@ val build_inductive : bool -> Names.identifier list -> - (Names.name*Rawterm.rawconstr) list list -> + (Names.name*Rawterm.rawconstr*bool) list list -> Topconstr.constr_expr list -> Rawterm.rawconstr list -> unit diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 2684a8f11..99bf2bf1d 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -48,7 +48,7 @@ let raw_decompose_app = -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t1 = t2] *) +(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) let raw_make_eq t1 t2 = mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1]) @@ -210,9 +210,11 @@ let rec alpha_rt excluded rt = match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt | RLambda(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in - let new_b = alpha_rt excluded b in - RLambda(loc,Anonymous,new_t,new_b) + let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in + let new_excluded = new_id :: excluded in + let new_t = alpha_rt new_excluded t in + let new_b = alpha_rt new_excluded b in + RLambda(loc,Name new_id,new_t,new_b) | RProd(loc,Anonymous,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in @@ -308,7 +310,7 @@ let rec alpha_rt excluded rt = List.map (alpha_rt excluded) args ) in - if Tacinterp.get_debug () <> Tactic_debug.DebugOff + if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false then Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++ prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++ @@ -510,3 +512,14 @@ let eq_cases_pattern pat1 pat2 = eq_cases_pattern_aux [pat1,pat2]; true with NotUnifiable -> false + + + +let ids_of_pat = + let rec ids_of_pat ids = function + | PatVar(_,Anonymous) -> ids + | PatVar(_,Name id) -> Idset.add id ids + | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl + in + ids_of_pat Idset.empty + diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index ecb59a87f..92df0ec6c 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -38,7 +38,7 @@ val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) -(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t1 = t2] *) +(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *) val raw_make_eq : rawconstr -> rawconstr -> rawconstr (* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *) val raw_make_neq : rawconstr -> rawconstr -> rawconstr @@ -101,3 +101,11 @@ val is_free_in : Names.identifier -> rawconstr -> bool val are_unifiable : cases_pattern -> cases_pattern -> bool val eq_cases_pattern : cases_pattern -> cases_pattern -> bool + + + +(* + ids_of_pat : cases_pattern -> Idset.t + returns the set of variables appearing in a pattern +*) +val ids_of_pat : cases_pattern -> Names.Idset.t diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 36ebaff11..cf09e63a7 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -53,7 +53,9 @@ let do_observe_tac s tac g = let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v with e -> - msgnl (str "observation "++str s++str " raised exception " ++ Cerrors.explain_exn e ++ str "on goal " ++ goal ); raise e;; + msgnl (str "observation "++str s++str " raised exception " ++ + Cerrors.explain_exn e ++ str "on goal " ++ goal ); + raise e;; let observe_tac s tac g = tac g |