From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- contrib/funind/Recdef.v | 48 + contrib/funind/functional_principles_proofs.ml | 88 +- contrib/funind/functional_principles_types.ml | 25 +- contrib/funind/g_indfun.ml4 | 485 ++++++++ contrib/funind/indfun.ml | 114 +- contrib/funind/indfun_common.ml | 57 +- contrib/funind/indfun_main.ml4 | 470 -------- contrib/funind/invfun.ml | 76 +- contrib/funind/merge.ml | 514 ++++++--- contrib/funind/rawterm_to_relation.ml | 41 +- contrib/funind/rawtermops.ml | 142 ++- contrib/funind/rawtermops.mli | 8 +- contrib/funind/recdef.ml | 1430 ++++++++++++++++++++++++ contrib/funind/tacinv.ml4 | 872 --------------- contrib/funind/tacinvutils.ml | 284 ----- contrib/funind/tacinvutils.mli | 80 -- 16 files changed, 2632 insertions(+), 2102 deletions(-) create mode 100644 contrib/funind/Recdef.v create mode 100644 contrib/funind/g_indfun.ml4 delete mode 100644 contrib/funind/indfun_main.ml4 create mode 100644 contrib/funind/recdef.ml delete mode 100644 contrib/funind/tacinv.ml4 delete mode 100644 contrib/funind/tacinvutils.ml delete mode 100644 contrib/funind/tacinvutils.mli (limited to 'contrib/funind') diff --git a/contrib/funind/Recdef.v b/contrib/funind/Recdef.v new file mode 100644 index 00000000..2d206220 --- /dev/null +++ b/contrib/funind/Recdef.v @@ -0,0 +1,48 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A) -> A -> A := + fun (fl : A -> A) (def : A) => + match n with + | O => def + | S m => fl (iter m fl def) + end. +End Iter. + +Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')). + intro p; intro p'; change (S p <= S (S (p + p'))); + apply le_S; apply Gt.gt_le_S; change (p < S (p + p')); + apply Lt.le_lt_n_Sm; apply Plus.le_plus_l. +Qed. + + +Theorem Splus_lt : forall p p' : nat, p' < S (p + p'). + intro p; intro p'; change (S p' <= S (p + p')); + apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm; + apply Plus.le_plus_r. +Qed. + +Theorem le_lt_SS : forall x y, x <= y -> x < S (S y). +intro x; intro y; intro H; change (S x <= S (S y)); + apply le_S; apply Gt.gt_le_S; change (x < S y); + apply Lt.le_lt_n_Sm; exact H. +Qed. + +Inductive max_type (m n:nat) : Set := + cmt : forall v, m <= v -> n <= v -> max_type m n. + +Definition max : forall m n:nat, max_type m n. +intros m n; case (Compare_dec.le_gt_dec m n). +intros h; exists n; [exact h | apply le_n]. +intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h]. +Defined. diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 975cf60b..3d80bd00 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -47,7 +47,7 @@ let observe_tac_stream s tac g = let observe_tac s tac g = observe_tac_stream (str s) tac g (* let tclTRYD tac = *) -(* if !Options.debug || do_observe () *) +(* if !Flags.debug || do_observe () *) (* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *) (* else tac *) @@ -140,7 +140,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); - (* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id) + (* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id]) ]] g exception TOREMOVE @@ -573,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id tclTHENLIST[ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); thin [hid]; - (h_rename prov_hid hid) + h_rename [prov_hid,hid] ] g ) ( (* @@ -637,7 +637,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; + pattern_option [(false,[1]),t] None; h_simplest_case t; (fun g' -> let g'_nb_prod = nb_prod (pf_concl g') in @@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (out_some f_def.const_body) + force (Option.get f_def.const_body) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -910,7 +910,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case (mkVar rec_id,Rawterm.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings)); intros_reflexivity] g ) ] @@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try let finfos = find_Function_infos (destConst f) in - mkConst (out_some finfos.equation_lemma) - with (Not_found | Failure "out_some" as e) -> + mkConst (Option.get finfos.equation_lemma) + with (Not_found | Option.IsNone as e) -> let f_id = id_of_label (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious @@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with - | Failure "out_some" -> + | Option.IsNone -> let finfos = find_Function_infos (destConst f) in update_Function {finfos with @@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : then (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) else - h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) + h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1) other_fix_infos | _ -> anomaly "Not a valid information" in @@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [([],Names.EvalConstRef fname)]; + [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1347,19 +1347,27 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> ([],id),Tacexpr.InHyp) + (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp) eqs ); - Tacexpr.onconcl = false; - Tacexpr.concl_occs = [] + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = match eqs with | [] -> tclIDTAC | eq::eqs -> + tclTHEN - (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs) + (tclMAP + (fun id gl -> + observe_tac + (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) + (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false)) + gl + ) + eqs + ) (rewrite_eqs_in_eqs eqs) let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = @@ -1373,21 +1381,26 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = [ tclTHENSEQ [ keep (tcc_hyps@eqs); - apply (Lazy.force acc_inv); (fun g -> if is_mes then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" (tclTHENLIST [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); - rewrite_eqs_in_eqs eqs; - (observe_tac "finishing" - (tclCOMPLETE ( - Eauto.gen_eauto false (false,5) [] (Some [])) + observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); + (observe_tac "finishing using" + ( + tclCOMPLETE( + Eauto.eauto_with_bases + false + (true,5) + [Lazy.force refl_equal] + [empty_transparent_state, Auto.Hint_db.empty] + ) ) ) ] @@ -1445,7 +1458,7 @@ let prove_principle_for_gen let wf_tac = if is_mes then - (fun b -> Recdef.tclUSER_if_not_mes b None) + (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None) else fun _ -> prove_with_tcc tcc_lemma_ref [] in let real_rec_arg_num = rec_arg_num - princ_info.nparams in @@ -1502,16 +1515,16 @@ let prove_principle_for_gen | None -> anomaly ( "No tcc proof !!") | Some lemma -> lemma in - let rec list_diff del_list check_list = - match del_list with - [] -> - [] - | f::r -> - if List.mem f check_list then - list_diff r check_list - else - f::(list_diff r check_list) - in +(* let rec list_diff del_list check_list = *) +(* match del_list with *) +(* [] -> *) +(* [] *) +(* | f::r -> *) +(* if List.mem f check_list then *) +(* list_diff r check_list *) +(* else *) +(* f::(list_diff r check_list) *) +(* in *) let tcc_list = ref [] in let start_tac gls = let hyps = pf_ids_of_hyps gls in @@ -1527,7 +1540,7 @@ let prove_principle_for_gen Elim.h_decompose_and (mkVar hid); (fun g -> let new_hyps = pf_ids_of_hyps g in - tcc_list := list_diff new_hyps (hid::hyps); + tcc_list := List.rev (list_subtract new_hyps (hid::hyps)); if !tcc_list = [] then begin @@ -1593,14 +1606,15 @@ let prove_principle_for_gen (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) (* observe_tac "new_prove_with_tcc" *) - (new_prove_with_tcc + (new_prove_with_tcc is_mes acc_inv fix_id - !tcc_list - ((List.map + + (!tcc_list@(List.map (fun (na,_,_) -> (Nameops.out_name na)) (princ_info.args@princ_info.params) - )@ (acc_rec_arg_id::eqs)) + )@ ([acc_rec_arg_id])) eqs ) + ); is_valid = is_valid_hypothesis predicates_names } diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 8ad2e72b..16076479 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = it_mkProd_or_LetIn ~init: (it_mkProd_or_LetIn - ~init:(option_fold_right + ~init:(Option.fold_right mkProd_or_LetIn princ_type_info.indarg princ_type_info.concl @@ -384,7 +384,7 @@ let generate_functional_principle { const_entry_body = value; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() + const_entry_boxed = Flags.boxed_definitions() } in ignore( @@ -394,7 +394,7 @@ let generate_functional_principle Decl_kinds.IsDefinition (Decl_kinds.Scheme) ) ); - Options.if_verbose + Flags.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) name; names := name :: !names @@ -561,6 +561,15 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent (fun _ _ _ -> ()) in incr i; + let opacity = + let finfos = find_Function_infos this_block_funs.(0) in + try + let equation = Option.get finfos.equation_lemma in + (Global.lookup_constant equation).Declarations.const_opaque + with Option.IsNone -> (* non recursive definition *) + false + in + let const = {const with const_entry_opaque = opacity } in (* The others are just deduced *) if other_princ_types = [] then @@ -642,10 +651,12 @@ let build_scheme fas = in List.iter2 (fun (princ_id,_,_) def_entry -> - ignore (Declare.declare_constant - princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); - Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id + ignore + (Declare.declare_constant + princ_id + (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + Flags.if_verbose + (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id ) fas bodies_types diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 new file mode 100644 index 00000000..dae76f2d --- /dev/null +++ b/contrib/funind/g_indfun.ml4 @@ -0,0 +1,485 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + +let pr_bindings prc prlc = function + | Rawterm.ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + Util.prlist_with_sep spc prc l + | Rawterm.ExplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | Rawterm.NoBindings -> mt () + +let pr_with_bindings prc prlc (c,bl) = + prc c ++ hv 0 (pr_bindings prc prlc bl) + +let pr_fun_ind_using prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) + +(* Duplication of printing functions because "'a with_bindings" is + (internally) not uniform in 'a: indeed constr_with_bindings at the + "typed" level has type "open_constr with_bindings" instead of + "constr with_bindings"; hence, its printer cannot be polymorphic in + (prc,prlc)... *) + +let pr_with_bindings_typed prc prlc (c,bl) = + prc c ++ + hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + +let pr_fun_ind_using_typed prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + + +ARGUMENT EXTEND fun_ind_using + TYPED AS constr_with_bindings_opt + PRINTED BY pr_fun_ind_using_typed + RAW_TYPED AS constr_with_bindings_opt + RAW_PRINTED BY pr_fun_ind_using + GLOB_TYPED AS constr_with_bindings_opt + GLOB_PRINTED BY pr_fun_ind_using +| [ "using" constr_with_bindings(c) ] -> [ Some c ] +| [ ] -> [ None ] +END + + +TACTIC EXTEND newfuninv + [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> + [ + Invfun.invfun hyp fname + ] +END + + +let pr_intro_as_pat prc _ _ pat = + match pat with + | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat + | None -> mt () + + +ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat +| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] +| [] ->[ None ] +END + + + + +TACTIC EXTEND newfunind + ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + [ + let pat = + match pat with + | None -> IntroAnonymous + | Some pat -> pat + in + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in + functional_induction true c princl pat ] +END +(***** debug only ***) +TACTIC EXTEND snewfunind + ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + [ + let pat = + match pat with + | None -> IntroAnonymous + | Some pat -> pat + in + let c = match cl with + | [] -> assert false + | [c] -> c + | c::cl -> applist(c,cl) + in + functional_induction false c princl pat ] +END + + +let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc + +ARGUMENT EXTEND constr_coma_sequence' + TYPED AS constr_list + PRINTED BY pr_constr_coma_sequence +| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] +| [ constr(c) ] -> [ [c] ] +END + +let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc + +ARGUMENT EXTEND auto_using' + TYPED AS constr_list + PRINTED BY pr_auto_using +| [ "using" constr_coma_sequence'(l) ] -> [ l ] +| [ ] -> [ [] ] +END + +VERNAC ARGUMENT EXTEND rec_annotation2 + [ "{" "struct" ident(id) "}"] -> [ Struct id ] +| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] +| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] +END + + +VERNAC ARGUMENT EXTEND binder2 + [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> + [ + LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ] +END + + +VERNAC ARGUMENT EXTEND rec_definition2 + [ ident(id) binder2_list( bl) + rec_annotation2_opt(annot) ":" lconstr( type_) + ":=" lconstr(def)] -> + [let names = List.map snd (Topconstr.names_of_local_assums bl) in + let check_one_name () = + if List.length names > 1 then + Util.user_err_loc + (Util.dummy_loc,"Function", + Pp.str "the recursive argument needs to be specified"); + in + let check_exists_args an = + try + let id = match an with + | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id + | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" + in + (try ignore(Util.list_index0 (Name id) names); annot + with Not_found -> Util.user_err_loc + (Util.dummy_loc,"Function", + Pp.str "No argument named " ++ Nameops.pr_id id) + ) + with Failure "check_exists_args" -> check_one_name ();annot + in + let ni = + match annot with + | None -> + annot + | Some an -> + check_exists_args an + in + ((Util.dummy_loc,id), ni, bl, type_, def) ] + END + + +VERNAC ARGUMENT EXTEND rec_definitions2 +| [ rec_definition2(rd) ] -> [ [rd] ] +| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ] +END + + +VERNAC COMMAND EXTEND Function + ["Function" rec_definitions2(recsl)] -> + [ + do_generate_principle false recsl; + + ] +END + + +VERNAC ARGUMENT EXTEND fun_scheme_arg +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +END + +VERNAC ARGUMENT EXTEND fun_scheme_args +| [ fun_scheme_arg(fa) ] -> [ [fa] ] +| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas] +END + +VERNAC COMMAND EXTEND NewFunctionalScheme + ["Functional" "Scheme" fun_scheme_args(fas) ] -> + [ + try + Functional_principles_types.build_scheme fas + with Functional_principles_types.No_graph_found -> + match fas with + | (_,fun_name,_)::_ -> + begin + begin + make_graph (Nametab.global fun_name) + end + ; + try Functional_principles_types.build_scheme fas + with Functional_principles_types.No_graph_found -> + Util.error ("Cannot generate induction principle(s)") + end + | _ -> assert false (* we can only have non empty list *) + ] +END +(***** debug only ***) + +VERNAC COMMAND EXTEND NewFunctionalCase + ["Functional" "Case" fun_scheme_arg(fas) ] -> + [ + Functional_principles_types.build_case_scheme fas + ] +END + +(***** debug only ***) +VERNAC COMMAND EXTEND GenerateGraph +["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] +END + + + + + +(* FINDUCTION *) + +(* comment this line to see debug msgs *) +let msg x = () ;; let pr_lconstr c = str "" + (* uncomment this to see debugging *) +let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prlistconstr lc = List.iter prconstr lc +let prstr s = msg(str s) +let prNamedConstr s c = + begin + msg(str ""); + msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); + msg(str ""); + end + + + +(** Information about an occurrence of a function call (application) + inside a term. *) +type fapp_info = { + fname: constr; (** The function applied *) + largs: constr list; (** List of arguments *) + free: bool; (** [true] if all arguments are debruijn free *) + max_rel: int; (** max debruijn index in the funcall *) + onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) +} + + +(** [constr_head_match(a b c) a] returns true, false otherwise. *) +let constr_head_match u t= + if isApp u + then + let uhd,args= destApp u in + uhd=t + else false + +(** [hdMatchSub inu t] returns the list of occurrences of [t] in + [inu]. DeBruijn are not pushed, so some of them may be unbound in + the result. *) +let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = + let subres = + match kind_of_term inu with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> + hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test + | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) + [] bl + | _ -> (* Cofix will be wrong *) + fold_constr + (fun l cstr -> + l @ hdMatchSub cstr test) [] inu in + if not (test inu) then subres + else + let f,args = decompose_app inu in + let freeset = Termops.free_rels inu in + let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in + {fname = f; largs = args; free = Util.Intset.is_empty freeset; + max_rel = max_rel; onlyvars = List.for_all isVar args } + ::subres + +let mkEq typ c1 c2 = + mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) + + +let poseq_unsafe idunsafe cstr gl = + let typ = Tacmach.pf_type_of gl cstr in + tclTHEN + (Tactics.letin_tac None (Name idunsafe) cstr allClauses) + (tclTHENFIRST + (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) + Tactics.reflexivity) + gl + + +let poseq id cstr gl = + let x = Tactics.fresh_id [] id gl in + poseq_unsafe x cstr gl + +(* dirty? *) + +let list_constr_largs = ref [] + +let rec poseq_list_ids_rec lcstr gl = + match lcstr with + | [] -> tclIDTAC gl + | c::lcstr' -> + match kind_of_term c with + | Var _ -> + (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) + | _ -> + let _ = prstr "c = " in + let _ = prconstr c in + let _ = prstr "\n" in + let typ = Tacmach.pf_type_of gl c in + let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in + let x = Tactics.fresh_id [] cname gl in + let _ = list_constr_largs:=mkVar x :: !list_constr_largs in + let _ = prstr " list_constr_largs = " in + let _ = prlistconstr !list_constr_largs in + let _ = prstr "\n" in + + tclTHEN + (poseq_unsafe x c) + (poseq_list_ids_rec lcstr') + gl + +let poseq_list_ids lcstr gl = + let _ = list_constr_largs := [] in + poseq_list_ids_rec lcstr gl + +(** [find_fapp test g] returns the list of [app_info] of all calls to + functions that satisfy [test] in the conclusion of goal g. Trivial + repetition (not modulo conversion) are deleted. *) +let find_fapp (test:constr -> bool) g : fapp_info list = + let pre_res = hdMatchSub (Tacmach.pf_concl g) test in + let res = + List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in + (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); + res) + + + +(** [finduction id filter g] tries to apply functional induction on + an occurence of function [id] in the conclusion of goal [g]. If + [id]=[None] then calls to any function are selected. In any case + [heuristic] is used to select the most pertinent occurrence. *) +let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) + (nexttac:Proof_type.tactic) g = + let test = match oid with + | Some id -> + let idconstr = mkConst (const_of_id id) in + (fun u -> constr_head_match u idconstr) (* select only id *) + | None -> (fun u -> isApp u) in (* select calls to any function *) + let info_list = find_fapp test g in + let ordered_info_list = heuristic info_list in + prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); + if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; + let taclist: Proof_type.tactic list = + List.map + (fun info -> + (tclTHEN + (tclTHEN (poseq_list_ids info.largs) + ( + fun gl -> + (functional_induction + true (applist (info.fname, List.rev !list_constr_largs)) + None IntroAnonymous) gl)) + nexttac)) ordered_info_list in + (* we try each (f t u v) until one does not fail *) + (* TODO: try also to mix functional schemes *) + tclFIRST taclist g + + + + +(** [chose_heuristic oi x] returns the heuristic for reordering + (and/or forgetting some elts of) a list of occurrences of + function calls infos to chose first with functional induction. *) +let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = + match oi with + | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) + | None -> + (* Default heuristic: put first occurrences where all arguments + are *bound* (meaning already introduced) variables *) + let ordering x y = + if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) + else if x.free && x.onlyvars then -1 + else if y.free && y.onlyvars then 1 + else 0 (* both not pertinent *) + in + List.sort ordering + + + +TACTIC EXTEND finduction + ["finduction" ident(id) natural_opt(oi)] -> + [ + match oi with + | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" + | _ -> + let heuristic = chose_heuristic oi in + finduction (Some id) heuristic tclIDTAC + ] +END + + + +TACTIC EXTEND fauto + [ "fauto" tactic(tac)] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic (snd tac) + ] + | + [ "fauto" ] -> + [ + let heuristic = chose_heuristic None in + finduction None heuristic tclIDTAC + ] + +END + + +TACTIC EXTEND poseq + [ "poseq" ident(x) constr(c) ] -> + [ poseq x c ] +END + +VERNAC COMMAND EXTEND Showindinfo + [ "showindinfo" ident(x) ] -> [ Merge.showind x ] +END + +VERNAC COMMAND EXTEND MergeFunind + [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" + "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> + [ + let f1 = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id1))) in + let f2 = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Util.dummy_loc,id2))) in + let f1type = Typing.type_of (Global.env()) Evd.empty f1 in + let f2type = Typing.type_of (Global.env()) Evd.empty f2 in + let ar1 = List.length (fst (decompose_prod f1type)) in + let ar2 = List.length (fst (decompose_prod f2type)) in + let _ = + if ar1 <> List.length cl1 then + Util.error ("not the right number of arguments for " ^ string_of_id id1) in + let _ = + if ar2 <> List.length cl2 then + Util.error ("not the right number of arguments for " ^ string_of_id id2) in + Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id + ] +END diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 82bee01f..a6cbb321 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -22,8 +22,8 @@ let is_rec_info scheme_info = let choose_dest_or_ind scheme_info = if is_rec_info scheme_info - then Tactics.new_induct - else Tactics.new_destruct + then Tactics.new_induct false + else Tactics.new_destruct false let functional_induction with_clean c princl pat = @@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat = | InType -> finfo.rect_lemma in let princ = (* then we get the principle *) - try mkConst (out_some princ_option ) - with Failure "out_some" -> + try mkConst (Option.get princ_option ) + with Option.IsNone -> (*i If there is not default lemma defined then, we cross our finger and try to find a lemma named f_ind (or f_rec, f_rect) i*) @@ -77,7 +77,7 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) + List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) in let princ' = Some (princ,bindings) in let princ_vars = @@ -120,7 +120,8 @@ let functional_induction with_clean c princl pat = princ_infos args_as_induction_constr princ' - pat) + pat + None) subst_and_reduce g @@ -139,14 +140,14 @@ type newfixpoint_expr = let rec abstract_rawconstr c = function | [] -> c | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl) - | Topconstr.LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl + | Topconstr.LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl (abstract_rawconstr c bl) let interp_casted_constr_with_implicits sigma env impls c = (* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) Constrintern.intern_gen false sigma env ~impls:([],impls) - ~allow_soapp:false ~ltacvars:([],[]) c + ~allow_patvar:false ~ltacvars:([],[]) c (* @@ -160,7 +161,7 @@ let build_newrecursive in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (recname,_,bl,arityc,_) -> + (fun (env,impls) ((_,recname),_,bl,arityc,_) -> let arityc = Command.generalize_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = @@ -213,7 +214,7 @@ let rec is_rec names = | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) -> + | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b | RLetTuple(_,nal,_,t,b) -> lookup names t || lookup @@ -224,7 +225,7 @@ let rec is_rec names = ) b | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl and lookup_br names (_,idl,_,rt) = @@ -266,7 +267,7 @@ let derive_inversion fix_names = ) with e -> msg_warning - (str "Cannot build functional inversion principle" ++ + (str "Cannot built inversion information" ++ if do_observe () then Cerrors.explain_exn e else mt ()) with _ -> () @@ -297,7 +298,7 @@ let generate_principle on_error is_general do_built fix_rec_l recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in + let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in @@ -318,7 +319,7 @@ let generate_principle on_error f_R_mut) in let fname_kn (fname,_,_,_,_) = - let f_ref = Ident (dummy_loc,fname) in + let f_ref = Ident fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -351,17 +352,17 @@ let generate_principle on_error let register_struct is_rec fixpoint_exprl = match fixpoint_exprl with - | [(fname,_,bl,ret_type,body),_] when not is_rec -> + | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> Command.declare_definition fname - (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition) + (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> - Command.build_recursive fixpoint_exprl (Options.boxed_definitions()) + Command.build_recursive fixpoint_exprl (Flags.boxed_definitions()) let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -402,7 +403,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - Topconstr.CApp (dummy_loc,(None,Topconstr.mkIdentC (id_of_string "eq")), + Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in let eq = Command.generalize_constr_expr unbounded_eq args in @@ -434,7 +435,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b | None -> begin match args with - | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x + | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -442,7 +443,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b match List.find (function - | Topconstr.LocalRawAssum(l,t) -> + | Topconstr.LocalRawAssum(l,k,t) -> List.exists (function (_,Name id) -> id = wf_args | _ -> false) l @@ -450,7 +451,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b ) args with - | Topconstr.LocalRawAssum(_,t) -> t,wf_args + | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -462,7 +463,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b let fun_from_mes = let applied_mes = Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in - Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) + Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -475,7 +476,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with - | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> + | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle on_error @@ -488,7 +489,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp if register_built then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook; false - | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> + | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle on_error @@ -503,20 +504,15 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp true | _ -> let fix_names = - List.map (function (name,_,_,_,_) -> name) fixpoint_exprl + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_one_rec = is_rec fix_names in let old_fixpoint_exprl = List.map (function | (name,Some (Struct id),args,types,body),_ -> - let names = - List.map - snd - (Topconstr.names_of_local_assums args) - in let annot = - try Some (list_index (Name id) names - 1), Topconstr.CStructRec + try Some (dummy_loc, id), Topconstr.CStructRec with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) @@ -529,7 +525,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp (dummy_loc,"Function", Pp.str "the recursive argument needs to be specified in Function") else - (name,(Some 0, Topconstr.CStructRec),args,types,body), + let loc, na = List.hd names in + (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), (None:Vernacexpr.decl_notation) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> error @@ -539,7 +536,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp in (* ok all the expressions are structural *) let fix_names = - List.map (function (name,_,_,_,_) -> name) fixpoint_exprl + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in if register_built then register_struct is_rec old_fixpoint_exprl; @@ -570,11 +567,11 @@ let rec add_args id new_args b = CArrow(loc,add_args id new_args b1, add_args id new_args b2) | CProdN(loc,nal,b1) -> CProdN(loc, - List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) | CLambdaN(loc,nal,b1) -> CLambdaN(loc, - List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) | CLetIn(loc,na,b1,b2) -> CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) @@ -588,22 +585,22 @@ let rec add_args id new_args b = | CApp(loc,(pf,b),bl) -> CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) - | CCases(loc,b_option,cel,cal) -> - CCases(loc,option_map (add_args id new_args) b_option, + | CCases(loc,sty,b_option,cel,cal) -> + CCases(loc,sty,Option.map (add_args id new_args) b_option, List.map (fun (b,(na,b_option)) -> add_args id new_args b, - (na,option_map (add_args id new_args) b_option)) cel, + (na,Option.map (add_args id new_args) b_option)) cel, List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal ) | CLetTuple(loc,nal,(na,b_option),b1,b2) -> - CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option), + CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), add_args id new_args b1, add_args id new_args b2 ) | CIf(loc,b1,(na,b_option),b2,b3) -> CIf(loc,add_args id new_args b1, - (na,option_map (add_args id new_args) b_option), + (na,Option.map (add_args id new_args) b_option), add_args id new_args b2, add_args id new_args b3 ) @@ -644,13 +641,15 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,t'')::nal_ta' -> + | (nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then aux (n - nal_l) nal_ta' else - let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t') + let new_t' = + Topconstr.CProdN(dummy_loc, + ((snd (list_chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') in @@ -668,12 +667,12 @@ let rec get_args b t : Topconstr.local_binder list * | Topconstr.CLambdaN (loc, (nal_ta), b') -> begin let n = - (List.fold_left (fun n (nal,_) -> + (List.fold_left (fun n (nal,_,_) -> n+List.length nal) 0 nal_ta ) 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'' + (List.map (fun (nal,k,ta) -> + (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -711,26 +710,13 @@ let make_graph (f_ref:global_reference) = let l = List.map (fun (id,(n,recexp),bl,t,b) -> - let bl' = - List.flatten - (List.map - (function - | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_) -> nal - ) - bl - ) - in - let rec_id = - match List.nth bl' (out_some n) with - |(_,Name id) -> id | _ -> anomaly "" - in + let loc, rec_id = Option.get n in let new_args = List.flatten (List.map (function | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_) -> + | Topconstr.LocalRawAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) @@ -739,7 +725,7 @@ let make_graph (f_ref:global_reference) = nal_tas ) in - let b' = add_args id new_args b in + let b' = add_args (snd id) new_args b in (id, Some (Struct rec_id),nal_tas@bl,t,b') ) fixexprl @@ -747,13 +733,13 @@ let make_graph (f_ref:global_reference) = l | _ -> let id = id_of_label (con_label c) in - [(id,None,nal_tas,t,b)] + [((dummy_loc,id),None,nal_tas,t,b)] in do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter - (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) + (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) expr_list diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 13b242d5..4010b49d 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -76,7 +76,7 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Rawterm.RLambda(_,name,k,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", @@ -90,7 +90,7 @@ let chop_rprod_n = then List.rev acc,rt else match rt with - | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -131,7 +131,7 @@ let coq_constant s = (Coqlib.init_modules @ Coqlib.arith_modules) s;; let constant sl s = - constr_of_reference + constr_of_global (Nametab.locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) (id_of_string s)));; @@ -153,7 +153,7 @@ open Entries open Decl_kinds open Declare let definition_message id = - Options.if_verbose message ((string_of_id id) ^ " is defined") + Flags.if_verbose message ((string_of_id id) ^ " is defined") let save with_clean id const (locality,kind) hook = @@ -237,24 +237,29 @@ let with_full_print f a = 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; + let old_rawprint = !Flags.raw_print in + let old_dump = !Flags.dump in + Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; + Impargs.make_contextual_implicit_args false; + Flags.dump := false; try let res = f a 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; + Flags.raw_print := old_rawprint; + Flags.dump := old_dump; res with | 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; + Flags.raw_print := old_rawprint; + Flags.dump := old_dump; raise e @@ -319,12 +324,12 @@ let subst_Function (_,subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Util.option_smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -354,12 +359,12 @@ let export_Function infos = Some infos let discharge_Function (_,finfos) = let function_constant' = Lib.discharge_con finfos.function_constant and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma + and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma + and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma + and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma + and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma + and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma + and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && @@ -387,12 +392,12 @@ let pr_info f_info = str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++ - str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ - str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ - str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ - str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++ - str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++ - str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++ + str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ + str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ + str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ + str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++ + str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++ + str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++ str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 deleted file mode 100644 index 9cee9edc..00000000 --- a/contrib/funind/indfun_main.ml4 +++ /dev/null @@ -1,470 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Rawterm.NoBindings -> mt () - - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - - -let pr_fun_ind_using prc prlc _ opt_c = - match opt_c with - | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) - - -ARGUMENT EXTEND fun_ind_using - TYPED AS constr_with_bindings_opt - PRINTED BY pr_fun_ind_using -| [ "using" constr_with_bindings(c) ] -> [ Some c ] -| [ ] -> [ None ] -END - - -TACTIC EXTEND newfuninv - [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> - [ - Invfun.invfun hyp fname - ] -END - - -let pr_intro_as_pat prc _ _ pat = - match pat with - | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat - | None -> mt () - - -ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat -| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] -| [] ->[ None ] -END - - - - -TACTIC EXTEND newfunind - ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> applist(c,cl) - in - functional_induction true c princl pat ] -END -(***** debug only ***) -TACTIC EXTEND snewfunind - ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> applist(c,cl) - in - functional_induction false c princl pat ] -END - - -let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc - -ARGUMENT EXTEND constr_coma_sequence' - TYPED AS constr_list - PRINTED BY pr_constr_coma_sequence -| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] -| [ constr(c) ] -> [ [c] ] -END - -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc - -ARGUMENT EXTEND auto_using' - TYPED AS constr_list - PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence'(l) ] -> [ l ] -| [ ] -> [ [] ] -END - -VERNAC ARGUMENT EXTEND rec_annotation2 - [ "{" "struct" ident(id) "}"] -> [ Struct id ] -| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] -| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] -END - - -VERNAC ARGUMENT EXTEND binder2 - [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> - [ - LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ] -END - - -VERNAC ARGUMENT EXTEND rec_definition2 - [ ident(id) binder2_list( bl) - rec_annotation2_opt(annot) ":" lconstr( type_) - ":=" lconstr(def)] -> - [let names = List.map snd (Topconstr.names_of_local_assums bl) in - let check_one_name () = - if List.length names > 1 then - Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - in - let check_exists_args an = - try - let id = match an with - | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id - | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" - in - (try ignore(Util.list_index (Name id) names - 1); annot - with Not_found -> Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "No argument named " ++ Nameops.pr_id id) - ) - with Failure "check_exists_args" -> check_one_name ();annot - in - let ni = - match annot with - | None -> - annot - | Some an -> - check_exists_args an - in - (id, ni, bl, type_, def) ] - END - - -VERNAC ARGUMENT EXTEND rec_definitions2 -| [ rec_definition2(rd) ] -> [ [rd] ] -| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ] -END - - -VERNAC COMMAND EXTEND Function - ["Function" rec_definitions2(recsl)] -> - [ - do_generate_principle false recsl; - - ] -END - - -VERNAC ARGUMENT EXTEND fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] -END - -VERNAC ARGUMENT EXTEND fun_scheme_args -| [ fun_scheme_arg(fa) ] -> [ [fa] ] -| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas] -END - -VERNAC COMMAND EXTEND NewFunctionalScheme - ["Functional" "Scheme" fun_scheme_args(fas) ] -> - [ - try - Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - match fas with - | (_,fun_name,_)::_ -> - begin - begin - make_graph (Nametab.global fun_name) - end - ; - try Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - Util.error ("Cannot generate induction principle(s)") - end - | _ -> assert false (* we can only have non empty list *) - ] -END -(***** debug only ***) - -VERNAC COMMAND EXTEND NewFunctionalCase - ["Functional" "Case" fun_scheme_arg(fas) ] -> - [ - Functional_principles_types.build_case_scheme fas - ] -END - -(***** debug only ***) -VERNAC COMMAND EXTEND GenerateGraph -["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] -END - - - - - -(* FINDUCTION *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - - - -(** Information about an occurrence of a function call (application) - inside a term. *) -type fapp_info = { - fname: constr; (** The function applied *) - largs: constr list; (** List of arguments *) - free: bool; (** [true] if all arguments are debruijn free *) - max_rel: int; (** max debruijn index in the funcall *) - onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) -} - - -(** [constr_head_match(a b c) a] returns true, false otherwise. *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - uhd=t - else false - -(** [hdMatchSub inu t] returns the list of occurrences of [t] in - [inu]. DeBruijn are not pushed, so some of them may be unbound in - the result. *) -let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = - let subres = - match kind_of_term inu with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> - hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test - | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) - [] bl - | _ -> (* Cofix will be wrong *) - fold_constr - (fun l cstr -> - l @ hdMatchSub cstr test) [] inu in - if not (test inu) then subres - else - let f,args = decompose_app inu in - let freeset = Termops.free_rels inu in - let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in - {fname = f; largs = args; free = Util.Intset.is_empty freeset; - max_rel = max_rel; onlyvars = List.for_all isVar args } - ::subres - -let mkEq typ c1 c2 = - mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) - - -let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_type_of gl cstr in - tclTHEN - (Tactics.letin_tac true (Name idunsafe) cstr allClauses) - (tclTHENFIRST - (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) - Tactics.reflexivity) - gl - - -let poseq id cstr gl = - let x = Tactics.fresh_id [] id gl in - poseq_unsafe x cstr gl - -(* dirty? *) - -let list_constr_largs = ref [] - -let rec poseq_list_ids_rec lcstr gl = - match lcstr with - | [] -> tclIDTAC gl - | c::lcstr' -> - match kind_of_term c with - | Var _ -> - (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) - | _ -> - let _ = prstr "c = " in - let _ = prconstr c in - let _ = prstr "\n" in - let typ = Tacmach.pf_type_of gl c in - let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in - let x = Tactics.fresh_id [] cname gl in - let _ = list_constr_largs:=mkVar x :: !list_constr_largs in - let _ = prstr " list_constr_largs = " in - let _ = prlistconstr !list_constr_largs in - let _ = prstr "\n" in - - tclTHEN - (poseq_unsafe x c) - (poseq_list_ids_rec lcstr') - gl - -let poseq_list_ids lcstr gl = - let _ = list_constr_largs := [] in - poseq_list_ids_rec lcstr gl - -(** [find_fapp test g] returns the list of [app_info] of all calls to - functions that satisfy [test] in the conclusion of goal g. Trivial - repetition (not modulo conversion) are deleted. *) -let find_fapp (test:constr -> bool) g : fapp_info list = - let pre_res = hdMatchSub (Tacmach.pf_concl g) test in - let res = - List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in - (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); - res) - - - -(** [finduction id filter g] tries to apply functional induction on - an occurence of function [id] in the conclusion of goal [g]. If - [id]=[None] then calls to any function are selected. In any case - [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list) - (nexttac:Proof_type.tactic) g = - let test = match oid with - | Some id -> - let idconstr = mkConst (const_of_id id) in - (fun u -> constr_head_match u idconstr) (* select only id *) - | None -> (fun u -> isApp u) in (* select calls to any function *) - let info_list = find_fapp test g in - let ordered_info_list = heuristic info_list in - prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; - let taclist: Proof_type.tactic list = - List.map - (fun info -> - (tclTHEN - (tclTHEN (poseq_list_ids info.largs) - ( - fun gl -> - (functional_induction - true (applist (info.fname, List.rev !list_constr_largs)) - None IntroAnonymous) gl)) - nexttac)) ordered_info_list in - (* we try each (f t u v) until one does not fail *) - (* TODO: try also to mix functional schemes *) - tclFIRST taclist g - - - - -(** [chose_heuristic oi x] returns the heuristic for reordering - (and/or forgetting some elts of) a list of occurrences of - function calls infos to chose first with functional induction. *) -let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = - match oi with - | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) - | None -> - (* Default heuristic: put first occurrences where all arguments - are *bound* (meaning already introduced) variables *) - let ordering x y = - if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) - else if x.free && x.onlyvars then -1 - else if y.free && y.onlyvars then 1 - else 0 (* both not pertinent *) - in - List.sort ordering - - - -TACTIC EXTEND finduction - ["finduction" ident(id) natural_opt(oi)] -> - [ - match oi with - | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" - | _ -> - let heuristic = chose_heuristic oi in - finduction (Some id) heuristic tclIDTAC - ] -END - - - -TACTIC EXTEND fauto - [ "fauto" tactic(tac)] -> - [ - let heuristic = chose_heuristic None in - finduction None heuristic (snd tac) - ] - | - [ "fauto" ] -> - [ - let heuristic = chose_heuristic None in - finduction None heuristic tclIDTAC - ] - -END - - -TACTIC EXTEND poseq - [ "poseq" ident(x) constr(c) ] -> - [ poseq x c ] -END - -VERNAC COMMAND EXTEND Showindinfo - [ "showindinfo" ident(x) ] -> [ Merge.showind x ] -END - -VERNAC COMMAND EXTEND MergeFunind - [ "Mergeschemes" lconstr(c) "with" lconstr(c') "using" ident(id) ] -> - [ - let c1 = Constrintern.interp_constr Evd.empty (Global.env()) c in - let c2 = Constrintern.interp_constr Evd.empty (Global.env()) c' in - let id1,args1 = - try - let hd,args = destApp c1 in - if Term.isInd hd then hd , args - else raise (Util.error "Ill-formed (fst) argument") - with Invalid_argument _ - -> Util.error ("Bad argument form for merging schemes") in - let id2,args2 = - try - let hd,args = destApp c2 in - if isInd hd then hd , args - else raise (Util.error "Ill-formed (snd) argument") - with Invalid_argument _ - -> Util.error ("Bad argument form for merging schemes") in - (* TOFO: enlever le ignore et declarer l'inductif *) - ignore(Merge.merge c1 c2 args1 args2 id) - ] -END diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index c7a3d164..63d44916 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -16,6 +16,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach +open Termops open Sign open Hiddentac @@ -23,13 +24,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + Util.prlist_with_sep spc (fun (_,c) -> prc c) l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -59,13 +60,13 @@ let observennl strm = let do_observe_tac s tac g = - try let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in - let v = tac g in msgnl (goal ++ fnl () ++ 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 "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); - raise e;; + let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in + try + let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v + with e -> + msgnl (str "observation "++ s++str " raised exception " ++ + Cerrors.explain_exn e ++ str " on goal " ++ goal ); + raise e;; let observe_tac s tac g = @@ -314,7 +315,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | None -> (id::pre_args,pre_tac) | Some b -> (pre_args, - tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac + tclTHEN (h_reduce (Rawterm.Unfold([Rawterm.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac ) else (pre_args,pre_tac) @@ -425,7 +426,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -435,7 +436,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) @@ -461,14 +462,14 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem ] g -(* [generalize_depedent_of x hyp g] +(* [generalize_dependent_of x hyp g] generalize every hypothesis which depends of [x] but [hyp] *) -let generalize_depedent_of x hyp g = +let generalize_dependent_of x hyp g = tclMAP (function | (id,None,t) when not (id = hyp) && - (Termops.occur_var (pf_env g) x t) -> h_generalize [mkVar id] + (Termops.occur_var (pf_env g) x t) -> tclTHEN (h_generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -490,12 +491,17 @@ and intros_with_rewrite_aux : tactic = | Prod(_,t,t') -> begin match kind_of_term t with - | App(eq,args) when (eq_constr eq eq_ind) -> - if isVar args.(1) + | App(eq,args) when (eq_constr eq eq_ind) -> + if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) + then + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g + + else if isVar args.(1) then let id = pf_get_new_id (id_of_string "y") g in tclTHENSEQ [ h_intro id; - generalize_depedent_of (destVar args.(1)) id; + generalize_dependent_of (destVar args.(1)) id; tclTRY (Equality.rewriteLR (mkVar id)); intros_with_rewrite ] @@ -513,7 +519,7 @@ and intros_with_rewrite_aux : tactic = Tauto.tauto g | Case(_,_,v,_) -> tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); + h_case false (v,Rawterm.NoBindings); intros_with_rewrite ] g | LetIn _ -> @@ -550,7 +556,7 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (snd (destApp (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); + h_case false (v,Rawterm.NoBindings); intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] @@ -567,9 +573,9 @@ let rec reflexivity_with_destruct_cases g = match kind_of_term (pf_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 - then Equality.discr id g + then Equality.discrHyp id g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENSEQ [Equality.inj [] id;thin [id];intros_with_rewrite] g + then tclTHENSEQ [Equality.injHyp id;thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) @@ -665,8 +671,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = if infos.is_general || Rtree.is_infinite graph_def.mind_recargs then let eq_lemma = - try out_some (infos).equation_lemma - with Failure "out_some" -> anomaly "Cannot find equation lemma" + try Option.get (infos).equation_lemma + with Option.IsNone -> anomaly "Cannot find equation lemma" in tclTHENSEQ[ tclMAP h_intro ids; @@ -682,7 +688,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = h_generalize (List.map mkVar ids); thin ids ] - else unfold_in_concl [([],Names.EvalConstRef (destConst f))] + else unfold_in_concl [(all_occurrences,Names.EvalConstRef (destConst f))] in (* The proof of each branche itself *) let ind_number = ref 0 in @@ -706,7 +712,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (* we expand the definition of the function *) observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids); (* introduce hypothesis with some rewrite *) - (intros_with_rewrite); + observe_tac "intros_with_rewrite" intros_with_rewrite; (* The proof is (almost) complete *) observe_tac "reflexivity" (reflexivity_with_destruct_cases) ] @@ -720,7 +726,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); h_intro graph_principle_id; observe_tac "" (tclTHEN_i - (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) + (observe_tac "elim" ((elim false (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g @@ -769,7 +775,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.of_list (List.map (fun entry -> - (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type ) + (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) ) @@ -960,13 +966,13 @@ let invfun qhyp f = in try let finfos = find_Function_infos f in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp with | Not_found -> error "No graph found" - | Failure "out_some" -> error "Cannot use equivalence with graph!" + | Option.IsNone -> error "Cannot use equivalence with graph!" let invfun qhyp f g = @@ -983,23 +989,23 @@ let invfun qhyp f g = try if not (isConst f1) then failwith ""; let finfos = find_Function_infos (destConst f1) in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct g - with | Failure "" | Failure "out_some" | Not_found -> + with | Failure "" | Option.IsNone | Not_found -> try let f2,_ = decompose_app args.(2) in if not (isConst f2) then failwith ""; let finfos = find_Function_infos (destConst f2) in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f2 f_correct g with | Failure "" -> errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function") - | Failure "out_some" -> + | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index 1b796a81..ec456aae 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -9,13 +9,16 @@ (* Merging of induction principles. *) (*i $Id: i*) - +open Libnames +open Tactics +open Indfun_common open Util open Topconstr open Vernacexpr open Pp open Names open Term +open Termops open Declarations open Environ open Rawterm @@ -25,6 +28,8 @@ open Rawtermops (** {2 Useful operations on constr and rawconstr} *) +let rec popn i c = if i<=0 then c else pop (popn (i-1) c) + (** Substitutions in constr *) let compare_constr_nosub t1 t2 = if compare_constr (fun _ _ -> false) t1 t2 @@ -110,6 +115,19 @@ let prNamedLDecl s lc = List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc; prstr "\n"; end +let prNamedRLDecl s lc = + begin + prstr s; prstr "\n"; prstr "{§§ "; + List.iter + (fun x -> + match x with + | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp + | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy + | _ -> assert false + ) lc; + prstr " §§}\n"; + prstr "\n"; + end let showind (id:identifier) = let cstrid = Tacinterp.constr_of_id (Global.env()) id in @@ -193,7 +211,7 @@ type linked_var = | Funres (** When merging two graphs, parameters may become regular arguments, - and thus be shifted. This type describe the result of computing + and thus be shifted. This type describes the result of computing the changes. *) type 'a shifted_params = { @@ -237,39 +255,47 @@ type 'a merged_arg = | Arg_linked of 'a | Arg_funres +(** Information about graph merging of two inductives. + All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *) + type merge_infos = { - ident:identifier; (* new inductive name *) + ident:identifier; (** new inductive name *) mib1: mutual_inductive_body; oib1: one_inductive_body; mib2: mutual_inductive_body; oib2: one_inductive_body; - (* Array of links of the first inductive (should be all stable) *) + + (** Array of links of the first inductive (should be all stable) *) lnk1: int merged_arg array; - (* Array of links of the second inductive (point to the first ind param/args) *) + + (** Array of links of the second inductive (point to the first ind param/args) *) lnk2: int merged_arg array; - (* number of rec params of ind1 which remai rec param in merge *) - nrecprms1: int; - (* number of other rec params of ind1 (which become non parm) *) - notherprms1:int; - (* number of functional result params of ind2 (which become non parm) *) - nfunresprms1:int; - (* list of decl of rec parms from ind1 which remain parms *) + + (** rec params which remain rec param (ie not linked) *) recprms1: rel_declaration list; - (* List of other rec parms from ind1 *) - otherprms1: rel_declaration list; (* parms that became args *) - funresprms1: rel_declaration list; (* parms that are functional result args *) - (* number of rec params of ind2 which remain rec param in merge (and not linked) *) + recprms2: rel_declaration list; + nrecprms1: int; nrecprms2: int; - (* number of other params of ind2 (which become non rec parm) *) + + (** rec parms which became non parm (either linked to something + or because after a rec parm that became non parm) *) + otherprms1: rel_declaration list; + otherprms2: rel_declaration list; + notherprms1:int; notherprms2:int; - (* number of functional result params of ind2 (which become non parm) *) + + (** args which remain args in merge *) + args1:rel_declaration list; + args2:rel_declaration list; + nargs1:int; + nargs2:int; + + (** functional result args *) + funresprms1: rel_declaration list; + funresprms2: rel_declaration list; + nfunresprms1:int; nfunresprms2:int; - (* list of decl of rec parms from ind2 which remain parms (and not linked) *) - recprms2: rel_declaration list; - (* List of other rec parms from ind2 (which are linked or become non parm) *) - otherprms2: rel_declaration list; - funresprms2: rel_declaration list; (* parms that are functional result args *) } @@ -288,7 +314,11 @@ let pr_merginfo x = let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false -let isArg_stable x = match x with Arg_stable _ -> true | _ -> false +(* ?? prm_linked?? *) +let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false + +let is_stable x = + match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false let isArg_funres x = match x with Arg_funres -> true | _ -> false @@ -346,6 +376,24 @@ let verify_inds mib1 mib2 = if mib2.mind_ntypes <> 1 then error "Second argument is mutual"; () +(* +(** [build_raw_params prms_decl avoid] returns a list of variables + attributed to the list of decl [prms_decl], avoiding names in + [avoid]. *) +let build_raw_params prms_decl avoid = + let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in + let _ = prNamedConstr "DUMMY" dummy_constr in + let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in + let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in + let res,_ = raw_decompose_prod dummy_rawconstr in + let comblist = List.combine prms_decl res in + comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr))) +*) + +let ids_of_rawlist avoid rawl = + List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl) + + (** {1 Merging function graphs} *) @@ -366,6 +414,7 @@ let verify_inds mib1 mib2 = ones, they become non rec (and the following too). And functinal argument have to be shifted at the end *) let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id = + let _ = prstr "\nYOUHOU shift\n" in let linked_targets = revlinked lnk2 in let is_param_of_mib1 x = x < mib1.mind_nparams_rec in let is_param_of_mib2 x = x < mib2.mind_nparams_rec in @@ -409,15 +458,29 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in let bldprms arity_ctxt mlnk = list_fold_lefti - (fun i (acc1,acc2,acc3) x -> + (fun i (acc1,acc2,acc3,acc4) x -> + prstr (pr_merginfo mlnk.(i));prstr "\n"; match mlnk.(i) with - | Prm_stable _ -> x::acc1 , acc2 , acc3 - | Prm_arg _ | Arg_stable _ -> acc1 , x::acc2 , acc3 - | Arg_funres -> acc1 , acc2 , x::acc3 - | _ -> acc1 , acc2 , acc3) (* Prm_linked and Arg_xxx = forget it *) - ([],[],[]) arity_ctxt in - let recprms1,otherprms1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in - let recprms2,otherprms2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in + | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4 + | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4 + | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4 + | Arg_funres -> acc1 , acc2 , acc3, x::acc4 + | _ -> acc1 , acc2 , acc3, acc4) + ([],[],[],[]) arity_ctxt in +(* let arity_ctxt2 = + build_raw_params oib2.mind_arity_ctxt + (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*) + let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in + let _ = prstr "\n\n\n" in + let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in + let _ = prstr "\notherprms1:\n" in + let _ = + List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + otherprms1 in + let _ = prstr "\notherprms2:\n" in + let _ = + List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + otherprms2 in { ident=id; mib1=mib1; @@ -429,14 +492,18 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array nrecprms1 = n_params1; recprms1 = recprms1; otherprms1 = otherprms1; + args1 = args1; funresprms1 = funresprms1; notherprms1 = Array.length mlnk1 - n_params1; nfunresprms1 = List.length funresprms1; + nargs1 = List.length args1; nrecprms2 = n_params2; recprms2 = recprms2; otherprms2 = otherprms2; + args2 = args2; funresprms2 = funresprms2; notherprms2 = Array.length mlnk2 - n_params2; + nargs2 = List.length args2; nfunresprms2 = List.length funresprms2; } @@ -447,45 +514,61 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array exception NoMerge -(* lnk is an link array of *all* args (from 1 and 2) *) -let merge_app c1 c2 id1 id2 shift filter_shift_stable = +let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> + let _ = prstr "\nICI1!\n";Pp.flush_all() in let args = filter_shift_stable lnk (arr1 @ arr2) in RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args) | RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge - | _ -> raise NoMerge - -let merge_app_unsafe c1 c2 shift filter_shift_stable = + | RLetIn(_,nme,bdy,trm) , _ -> + let _ = prstr "\nICI2!\n";Pp.flush_all() in + let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in + RLetIn(dummy_loc,nme,bdy,newtrm) + | _, RLetIn(_,nme,bdy,trm) -> + let _ = prstr "\nICI3!\n";Pp.flush_all() in + let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in + RLetIn(dummy_loc,nme,bdy,newtrm) + | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in + raise NoMerge + +let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with | RApp(_,f1, arr1), RApp(_,f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args) - | _ -> raise NoMerge + (* FIXME: what if the function appears in the body of the let? *) + | RLetIn(_,nme,bdy,trm) , _ -> + let _ = prstr "\nICI2 '!\n";Pp.flush_all() in + let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in + RLetIn(dummy_loc,nme,bdy,newtrm) + | _, RLetIn(_,nme,bdy,trm) -> + let _ = prstr "\nICI3 '!\n";Pp.flush_all() in + let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in + RLetIn(dummy_loc,nme,bdy,newtrm) + | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge (* Heuristic when merging two lists of hypothesis: merge every rec - calls of nrach 1 with all rec calls of branch 2. *) + calls of branch 1 with all rec calls of branch 2. *) (* TODO: reecrire cette heuristique (jusqu'a merge_types) *) -let onefoud = ref false (* Ugly *) - -let rec merge_rec_hyps shift accrec (ltyp:(Names.name * Rawterm.rawconstr) list) - filter_shift_stable = +let rec merge_rec_hyps shift accrec + (ltyp:(Names.name * rawconstr option * rawconstr option) list) + filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list = + let mergeonehyp t reldecl = + match reldecl with + | (nme,x,Some (RApp(_,i,args) as ind)) + -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) + | (nme,Some _,None) -> error "letins with recursive calls not treated yet" + | (nme,None,Some _) -> assert false + | (nme,None,None) | (nme,Some _,Some _) -> assert false in match ltyp with | [] -> [] - | (nme,(RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> - let _ = onefoud := true in - let rechyps = - List.map - (fun (nme,ind) -> - match ind with - | RApp(_,i,args) -> - nme, merge_app_unsafe ind t shift filter_shift_stable - | _ -> assert false) - accrec in + | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f -> + let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -494,50 +577,58 @@ let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec -let find_app (nme:identifier) (ltyp: (name * rawconstr) list) = +let find_app (nme:identifier) ltyp = try ignore (List.map (fun x -> match x with - | _,(RApp(_,f,_)) when isVarf nme f -> raise (Found 0) + | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0) | _ -> ()) ltyp); false with Found _ -> true + +let prnt_prod_or_letin nm letbdy typ = + match letbdy , typ with + | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy + | None , Some tp -> prNamedRConstr (string_of_name nm) tp + | _ , _ -> assert false + -let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list) - concl1 (ltyp2:(name * rawconstr) list) concl2 - : (name * rawconstr) list * rawconstr = +let rec merge_types shift accrec1 + (ltyp1:(name * rawconstr option * rawconstr option) list) + (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2 + : (name * rawconstr option * rawconstr option) list * rawconstr = let _ = prstr "MERGE_TYPES\n" in let _ = prstr "ltyp 1 : " in - let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp1 in + let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in let _ = prstr "\nltyp 2 : " in - let _ = List.iter (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) ltyp2 in + let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in let _ = prstr "\n" in - - let res = match ltyp1 with | [] -> let isrec1 = (accrec1<>[]) in let isrec2 = find_app ind2name ltyp2 in - let _ = if isrec2 then prstr " ISREC2 TRUE" else prstr " ISREC2 FALSE" in - let _ = if isrec1 then prstr " ISREC1 TRUE\n" else prstr " ISREC1 FALSE\n" in let rechyps = if isrec1 && isrec2 - then merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable + then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *) + merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 + filter_shift_stable_right + @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2] + filter_shift_stable else if isrec1 (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *) - then merge_rec_hyps shift accrec1 (ltyp2@[name_of_string "concl2",concl2]) - filter_shift_stable + then + merge_rec_hyps shift accrec1 + (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable else if isrec2 - then merge_rec_hyps shift [name_of_string "concl1",concl1] ltyp2 + then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2 filter_shift_stable_right - else [] in + else ltyp2 in let _ = prstr"\nrechyps : " in - let _ = List.iter - (fun (nm,tp) -> prNamedRConstr (string_of_name nm) tp) rechyps in + let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in let _ = prstr "MERGE CONCL : " in let _ = prNamedRConstr "concl1" concl1 in let _ = prstr " with " in @@ -548,15 +639,22 @@ let rec merge_types shift accrec1 (ltyp1:(name * rawconstr) list) let _ = prstr "FIN " in let _ = prNamedRConstr "concl" concl in let _ = prstr "\n" in + rechyps , concl - | (nme,t1)as e ::lt1 -> - match t1 with + | (nme,None, Some t1)as e ::lt1 -> + (match t1 with | RApp(_,f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> let recres, recconcl2 = merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in - ((nme,t1) :: recres) , recconcl2 + ((nme,None,Some t1) :: recres) , recconcl2) + | (nme,Some bd, None) ::lt1 -> + (* FIXME: what if ind1name appears in bd? *) + let recres, recconcl2 = + merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in + ((nme,Some bd,None) :: recres) , recconcl2 + | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false in res @@ -578,9 +676,9 @@ let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array) let build_link_map allargs1 allargs2 lnk = let allargs1 = - Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs1)) in + Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs1)) in let allargs2 = - Array.of_list (List.rev (List.map (fun (x,y) -> id_of_name x) allargs2)) in + Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in build_link_map_aux allargs1 allargs2 lnk @@ -598,7 +696,7 @@ let build_link_map allargs1 allargs2 lnk = forall recparams1 (recparams2 without linked params), forall ordparams1 (ordparams2 without linked params), - H1a' -> H2a' -> ... -> H2a' -> H2b' -> ... + H1a' -> H2a' -> ... -> H2a' -> H2b'(shifted) -> ... -> (newI x1 ... z1 x2 y2 ...z2 without linked params) where Hix' have been adapted, ie: @@ -621,21 +719,27 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr) shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in let nargs2 = shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in - let allargs1,rest1 = raw_decompose_prod_n nargs1 typcstr1 in - let allargs2,rest2 = raw_decompose_prod_n nargs2 typcstr2 in + let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in + let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *) let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in let rest2 = change_vars linked_map rest2 in - let hyps1,concl1 = raw_decompose_prod rest1 in - let hyps2,concl2' = raw_decompose_prod rest2 in + let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in + let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in let ltyp,concl2 = merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in - let typ = raw_compose_prod concl2 (List.rev ltyp) in + let _ = prNamedRLDecl "ltyp result:" ltyp in + let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in let revargs1 = list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in + let _ = prNamedRLDecl "ltyp allargs1" allargs1 in + let _ = prNamedRLDecl "ltyp revargs1" revargs1 in let revargs2 = list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in - let typwithprms = raw_compose_prod typ (List.rev revargs2 @ List.rev revargs1) in + let _ = prNamedRLDecl "ltyp allargs2" allargs2 in + let _ = prNamedRLDecl "ltyp revargs2" revargs2 in + let typwithprms = + raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in typwithprms @@ -661,22 +765,16 @@ let merge_constructor_id id1 id2 shift:identifier = constructor [(name*type)]. These are translated to rawterms first, each of them having distinct var names. *) let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) - (typcstr1:(identifier * types) list) - (typcstr2:(identifier * types) list) : (identifier * rawconstr) list = + (typcstr1:(identifier * rawconstr) list) + (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list = List.flatten (List.map - (fun (id1,typ1) -> - let typ1 = substitterm 0 (mkRel 1) (mkVar ind1name) typ1 in - let rawtyp1 = Detyping.detype false (Idset.elements avoid) [] typ1 in - let idsoftyp1:Idset.t = ids_of_rawterm rawtyp1 in + (fun (id1,rawtyp1) -> List.map - (fun (id2,typ2) -> - let typ2 = substitterm 0 (mkRel 1) (mkVar ind2name) typ2 in - (* Avoid also rawtyp1 names *) - let avoid2 = Idset.union avoid idsoftyp1 in - let rawtyp2 = Detyping.detype false (Idset.elements avoid2) [] typ2 in + (fun (id2,rawtyp2) -> let typ = merge_one_constructor shift rawtyp1 rawtyp2 in let newcstror_id = merge_constructor_id id1 id2 shift in + let _ = prstr "\n**************\n" in newcstror_id , typ) typcstr2) typcstr1) @@ -685,22 +783,33 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) inductive bodies [oib1] and [oib2], linking with [lnk], params info in [shift], avoiding identifiers in [avoid]. *) let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) - (oib2:one_inductive_body) : (identifier * rawconstr) list = - let lcstr1 = Array.to_list oib1.mind_user_lc in - let lcstr2 = Array.to_list oib2.mind_user_lc in + (oib2:one_inductive_body) = + (* building rawconstr type of constructors *) + let mkrawcor nme avoid typ = + (* first replace rel 1 by a varname *) + let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in + Detyping.detype false (Idset.elements avoid) [] substindtyp in + let lcstr1: rawconstr list = + Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in + (* add to avoid all indentifiers of lcstr1 *) + let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in + let lcstr2 = + Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in + let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in + + let params1 = + try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1)) + with _ -> [] in + let params2 = + try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2)) + with _ -> [] in + let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in + cstror_suffix_init(); - merge_constructors shift avoid lcstr1 lcstr2 + params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2 -(** [build_raw_params prms_decl avoid] returns a list of variables - attributed to the list of decl [prms_decl], avoiding names in - [avoid]. *) -let build_raw_params prms_decl avoid = - let dummy_constr = compose_prod prms_decl mkProp in - let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in - let res,_ = raw_decompose_prod dummy_rawconstr in - res , (avoid @ (Idset.elements (ids_of_rawterm dummy_rawconstr))) (** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual inductive bodies [mib1] and [mib2] linking vars with @@ -708,42 +817,35 @@ let build_raw_params prms_decl avoid = For the moment, inductives are supposed to be non mutual. *) let rec merge_mutual_inductive_body - (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) - (shift:merge_infos) = + (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = (* Mutual not treated, we take first ind body of each. *) - let nprms1 = mib1.mind_nparams_rec in (* n# of rec uniform parms of mib1 *) - let prms1 = (* rec uniform parms of mib1 *) - List.map (fun (x,_,y) -> x,y) (fst (list_chop nprms1 mib1.mind_params_ctxt)) in - - (* useless: *) - let prms1_named,avoid' = build_raw_params prms1 [] in - let prms2_named,avoid = build_raw_params prms1 avoid' in - let avoid:Idset.t = List.fold_right Idset.add avoid Idset.empty in - (* *** *) - - merge_inductive_body shift avoid mib1.mind_packets.(0) mib2.mind_packets.(0) + merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) +let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) + Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x -let merge_rec_params_and_arity params1 params2 shift (concl:constr) = - let params = shift.recprms1 @ shift.recprms2 in - let resparams, _ = +let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = + let params = prms2 @ prms1 in + let resparams = List.fold_left - (fun (acc,env) (nme,_,tp) -> - let typ = Constrextern.extern_constr false env tp in - let newenv = Environ.push_rel (nme,None,tp) env in - LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc , newenv) - ([],Global.env()) - params in + (fun acc (nme,tp) -> + let _ = prstr "param :" in + let _ = prNamedRConstr (string_of_name nme) tp in + let _ = prstr " ; " in + let typ = rawterm_to_constr_expr tp in + LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) + [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in let arity,_ = List.fold_left (fun (acc,env) (nm,_,c) -> let typ = Constrextern.extern_constr false env c in let newenv = Environ.push_rel (nm,None,c) env in - CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv) + CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) - (shift.otherprms1@shift.otherprms2@shift.funresprms1@shift.funresprms2) in + (shift.funresprms2 @ shift.funresprms1 + @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in resparams,arity @@ -752,20 +854,37 @@ let merge_rec_params_and_arity params1 params2 shift (concl:constr) = induct_expr corresponding to the the list of constructor types [rawlist], named ident. FIXME: params et cstr_expr (arity) *) -let rawterm_list_to_inductive_expr mib1 mib2 shift +let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(identifier * rawconstr) list):inductive_expr = - let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) - Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x in let lident = dummy_loc, shift.ident in let bindlist , cstr_expr = (* params , arities *) - merge_rec_params_and_arity - mib1.mind_params_ctxt mib2.mind_params_ctxt shift mkSet in + merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = List.map (* zeta_normalize t ? *) (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t)) rawlist in lident , bindlist , cstr_expr , lcstor_expr + + +let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = + match rdecl with + | (nme,None,t) -> + let traw = Detyping.detype false [] [] t in + RProd (dummy_loc,nme,Explicit,traw,t2) + | (_,Some _,_) -> assert false + + + + +let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = + match rdecl with + | (nme,None,t) -> + let traw = Detyping.detype false [] [] t in + RProd (dummy_loc,nme,Explicit,traw,t2) + | (_,Some _,_) -> assert false + + (** [merge_inductive ind1 ind2 lnk] merges two graphs, linking variables specified in [lnk]. Graphs are not supposed to be mutual inductives for the moment. *) @@ -777,35 +896,124 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *) (* compute params that become ordinary args (because linked to ord. args) *) let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in - let rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in - let indexpr = rawterm_list_to_inductive_expr mib1 mib2 shift_prm rawlist in + let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in + let _ = prstr "\nrawlist : " in + let _ = + List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in + let _ = prstr "\nend rawlist\n" in +(* FIX: retransformer en constr ici + let shift_prm = + { shift_prm with + recprms1=prms1; + recprms1=prms1; + } in *) + let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) Command.build_mutual [(indexpr,None)] true (* means: not coinductive *) - -let merge (cstr1:constr) (cstr2:constr) (args1:constr array) (args2:constr array) id = - let env = Global.env() in - let ind1,_cstrlist1 = Inductiveops.find_inductive env Evd.empty cstr1 in - let ind2,_cstrlist2 = Inductiveops.find_inductive env Evd.empty cstr2 in - let lnk1 = (* args1 are unlinked. FIXME? mergescheme (G x x) ?? *) - Array.mapi (fun i c -> Unlinked) args1 in - let _ = lnk1.(Array.length lnk1 - 1) <- Funres in (* last arg is functional result *) - let lnk2 = (* args2 may be linked to args1 members. FIXME: same - as above: vars may be linked inside args2?? *) +(* Find infos on identifier id. *) +let find_Function_infos_safe (id:identifier): Indfun_common.function_info = + let kn_of_id x = + let f_ref = Libnames.Ident (dummy_loc,x) in + locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref) + locate_constant f_ref in + try find_Function_infos (kn_of_id id) + with Not_found -> + errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme") + +(** [merge id1 id2 args1 args2 id] builds and declares a new inductive + type called [id], representing the merged graphs of both graphs + [ind1] and [ind2]. identifiers occuring in both arrays [args1] and + [args2] are considered linked (i.e. are the same variable) in the + new graph. + + Warning: For the moment, repetitions of an id in [args1] or + [args2] are not supported. *) +let merge (id1:identifier) (id2:identifier) (args1:identifier array) + (args2:identifier array) id : unit = + let finfo1 = find_Function_infos_safe id1 in + let finfo2 = find_Function_infos_safe id2 in + (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *) + (* We add one arg (functional arg of the graph) *) + let lnk1 = Array.make (Array.length args1 + 1) Unlinked in + let lnk2' = (* args2 may be linked to args1 members. FIXME: same + as above: vars may be linked inside args2?? *) Array.mapi (fun i c -> match array_find args1 (fun i x -> x=c) with | Some j -> Linked j | None -> Unlinked) args2 in - let _ = lnk2.(Array.length lnk2 - 1) <- Funres in (* last arg is functional result *) - let resa = merge_inductive ind1 ind2 lnk1 lnk2 id in - resa - - - + (* We add one arg (functional arg of the graph) *) + let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in + (* setting functional results *) + let _ = lnk1.(Array.length lnk1 - 1) <- Funres in + let _ = lnk2.(Array.length lnk2 - 1) <- Funres in + merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id + + +let remove_last_arg c = + let (x,y) = decompose_prod c in + let xnolast = List.rev (List.tl (List.rev x)) in + compose_prod xnolast y + +let rec remove_n_fst_list n l = if n=0 then l else remove_n_fst_list (n-1) (List.tl l) +let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l)) + +let remove_last_n_arg n c = + let (x,y) = decompose_prod c in + let xnolast = remove_n_last_list n x in + compose_prod xnolast y + +(* [funify_branches relinfo nfuns branch] returns the branch [branch] + of the relinfo [relinfo] modified to fit in a functional principle. + Things to do: + - remove indargs from rel applications + - replace *variables only* corresponding to function (recursive) + results by the actual function application. *) +let funify_branches relinfo nfuns branch = + let mut_induct, induct = + match relinfo.indref with + | None -> assert false + | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind + | _ -> assert false in + let is_dom c = + match kind_of_term c with + | Ind((u,_)) | Construct((u,_),_) -> u = mut_induct + | _ -> false in + let _dom_i c = + assert (is_dom c); + match kind_of_term c with + | Ind((u,i)) | Construct((u,_),i) -> i + | _ -> assert false in + let _is_pred c shift = + match kind_of_term c with + | Rel i -> let reali = i-shift in (reali>=0 && reali false in + (* FIXME: *) + (Anonymous,Some mkProp,mkProp) + +let relprinctype_to_funprinctype relprinctype nfuns = + let relinfo = compute_elim_sig relprinctype in + assert (not relinfo.farg_in_concl); + assert (relinfo.indarg_in_concl); + (* first remove indarg and indarg_in_concl *) + let relinfo_noindarg = { relinfo with + indarg_in_concl = false; indarg = None; + concl = remove_last_arg (pop relinfo.concl); } in + (* the nfuns last induction arguments are functional ones: remove them *) + let relinfo_argsok = { relinfo_noindarg with + nargs = relinfo_noindarg.nargs - nfuns; + (* args is in reverse order, so remove fst *) + args = remove_n_fst_list nfuns relinfo_noindarg.args; + concl = popn nfuns relinfo_noindarg.concl + } in + let new_branches = + List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in + let relinfo_branches = { relinfo_argsok with branches = new_branches } in + relinfo_branches (* @article{ bundy93rippling, author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill", diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index b34a1097..08a97fd2 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in + let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in Environ.push_named (id,value,typ) env @@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env = | Anonymous -> assert false | Name id -> let new_t = substl ctxt t in - let new_v = option_map (substl ctxt) v in + let new_v = Option.map (substl ctxt) v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ + Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) ); (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) ) @@ -446,7 +446,7 @@ let rec pattern_to_term_and_type env typ = function let patl_as_term = List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl in - mkRApp(mkRRef(Libnames.ConstructRef constr), + mkRApp(mkRRef(ConstructRef constr), implicit_args@patl_as_term ) @@ -586,7 +586,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = | RProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | RLambda(_,n,t,b) -> + | RLambda(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -601,7 +601,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | RProd(_,n,t,b) -> + | RProd(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) @@ -689,7 +689,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case env funname make_discr - (el:tomatch_tuple) + (el:tomatch_tuples) (brl:Rawterm.cases_clauses) avoid : rawconstr build_entry_return = match el with @@ -865,7 +865,7 @@ let is_res id = *) let rec rebuild_cons nb_args relname args crossed_types depth rt = match rt with - | RProd(_,n,t,b) -> + | RProd(_,n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin @@ -928,7 +928,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = (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) -> + | RLambda(_,n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -944,7 +944,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = 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 + RProd(dummy_loc,n,k,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 *) @@ -1016,11 +1016,12 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | RApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> + | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b - | RCases _ -> params (* If there is still cases at this point they can only be - discriminitation ones *) + | RCases _ -> + params (* If there is still cases at this point they can only be + discriminitation ones *) | RSort _ -> params | RHole _ -> params | RIf _ | RRec _ | RCast _ | RDynamic _ -> @@ -1153,7 +1154,7 @@ let do_build_inductive else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], acc ) ) @@ -1173,7 +1174,7 @@ let do_build_inductive Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t) else Topconstr.LocalRawAssum - ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t) + ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t) ) rels_params in @@ -1181,8 +1182,8 @@ let do_build_inductive Array.map (List.map (fun (id,t) -> false,((dummy_loc,id), - Options.with_option - Options.raw_print + Flags.with_option + Flags.raw_print (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t) ) )) @@ -1218,7 +1219,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Options.silently (Command.build_mutual rel_inds)) true + with_full_print (Flags.silently (Command.build_mutual rel_inds)) true with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 113ddd8b..92396af5 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -12,10 +12,10 @@ let idmap_is_empty m = m = Idmap.empty let mkRRef ref = RRef(dummy_loc,ref) let mkRVar id = RVar(dummy_loc,id) let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b) -let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b) +let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) +let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) -let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) +let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl) let mkRSort s = RSort(dummy_loc,s) let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) @@ -26,27 +26,59 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) *) let raw_decompose_prod = let rec raw_decompose_prod args = function - | RProd(_,n,t,b) -> + | RProd(_,n,k,t,b) -> raw_decompose_prod ((n,t)::args) b | rt -> args,rt in raw_decompose_prod [] +let raw_decompose_prod_or_letin = + let rec raw_decompose_prod args = function + | RProd(_,n,k,t,b) -> + raw_decompose_prod ((n,None,Some t)::args) b + | RLetIn(_,n,t,b) -> + raw_decompose_prod ((n,Some t,None)::args) b + | rt -> args,rt + in + raw_decompose_prod [] + let raw_compose_prod = List.fold_left (fun b (n,t) -> mkRProd(n,t,b)) +let raw_compose_prod_or_letin = + List.fold_left ( + fun concl decl -> + match decl with + | (n,None,Some t) -> mkRProd(n,t,concl) + | (n,Some bdy,None) -> mkRLetIn(n,bdy,concl) + | _ -> assert false) + let raw_decompose_prod_n n = let rec raw_decompose_prod i args c = if i<=0 then args,c else match c with - | RProd(_,n,t,b) -> + | RProd(_,n,_,t,b) -> raw_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in raw_decompose_prod n [] +let raw_decompose_prod_or_letin_n n = + let rec raw_decompose_prod i args c = + if i<=0 then args,c + else + match c with + | RProd(_,n,_,t,b) -> + raw_decompose_prod (i-1) ((n,None,Some t)::args) b + | RLetIn(_,n,t,b) -> + raw_decompose_prod (i-1) ((n,Some t,None)::args) b + | rt -> args,rt + in + raw_decompose_prod n [] + + let raw_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *) @@ -103,15 +135,17 @@ let change_vars = change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, name, + k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) @@ -125,12 +159,12 @@ let change_vars = let new_mapping = List.fold_left remove_name_from_mapping mapping nal in RLetTuple(loc, nal, - (na, option_map (change_vars mapping) rto), + (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl @@ -138,7 +172,7 @@ let change_vars = | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, change_vars mapping b, - (na,option_map (change_vars mapping) e_option), + (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) @@ -229,21 +263,21 @@ let rec alpha_rt excluded rt = let new_rt = match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,t,b) -> + | RLambda(loc,Anonymous,k,t,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) -> + RLambda(loc,Name new_id,k,new_t,new_b) + | RProd(loc,Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RProd(loc,Anonymous,new_t,new_b) + RProd(loc,Anonymous,k,new_t,new_b) | RLetIn(loc,Anonymous,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in RLetIn(loc,Anonymous,new_t,new_b) - | RLambda(loc,Name id,t,b) -> + | RLambda(loc,Name id,k,t,b) -> let new_id = Nameops.next_ident_away id excluded in let t,b = if new_id = id @@ -255,8 +289,8 @@ let rec alpha_rt excluded rt = 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,Name id,t,b) -> + RLambda(loc,Name new_id,k,new_t,new_b) + | RProd(loc,Name id,k,t,b) -> let new_id = Nameops.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -268,7 +302,7 @@ let rec alpha_rt excluded rt = in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RProd(loc,Name new_id,new_t,new_b) + RProd(loc,Name new_id,k,new_t,new_b) | RLetIn(loc,Name id,t,b) -> let new_id = Nameops.next_ident_away id excluded in let t,b = @@ -306,20 +340,20 @@ let rec alpha_rt excluded rt = if idmap_is_empty mapping then rto,t,b else let replace = change_vars mapping in - (option_map replace rto, t,replace b) + (Option.map replace rto, t,replace b) in let new_t = alpha_rt new_excluded new_t in let new_b = alpha_rt new_excluded new_b in - let new_rto = option_map (alpha_rt new_excluded) new_rto in + let new_rto = Option.map (alpha_rt new_excluded) new_rto in RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) - | RCases(loc,infos,el,brl) -> + | RCases(loc,sty,infos,el,brl) -> let new_el = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in - RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) + RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) | RIf(loc,b,(na,e_o),lhs,rhs) -> RIf(loc,alpha_rt excluded b, - (na,option_map (alpha_rt excluded) e_o), + (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) @@ -357,17 +391,16 @@ let is_free_in id = | REvar _ -> false | RPatVar _ -> false | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) -> + | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) -> let check_in_b = match n with | Name id' -> id_ord id' id <> 0 | _ -> true in is_free_in t || (check_in_b && is_free_in b) - | RCases(_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl - | RLetTuple(_,nal,_,b,t) -> let check_in_nal = not (List.exists (function Name id' -> id'= id | _ -> false) nal) @@ -428,17 +461,19 @@ let replace_var_by_term x_id term = replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLambda(loc,name,t,b) -> + | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,t,b) -> + | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | RProd(loc,name,k,t,b) -> RProd(loc, name, + k, replace_var_by_pattern t, replace_var_by_pattern b ) @@ -455,19 +490,19 @@ let replace_var_by_term x_id term = | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, - (na,option_map replace_var_by_pattern rto), + (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, replace_var_by_pattern b, - (na,option_map replace_var_by_pattern e_option), + (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) @@ -558,15 +593,15 @@ let ids_of_rawterm c = | RVar (_,id) -> id::acc | RApp (loc,g,args) -> ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc | RLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCases (loc,rtntypopt,tml,brchl) -> + | RCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl) | RRec _ -> failwith "Fix inside a constructor branch" | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> [] @@ -590,15 +625,17 @@ let zeta_normalize = zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, - name, + name, + k, zeta_normalize_term t, zeta_normalize_term b ) @@ -608,19 +645,19 @@ let zeta_normalize = | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, - (na,option_map zeta_normalize_term rto), + (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) - | RCases(loc,infos,el,brl) -> - RCases(loc, + | RCases(loc,sty,infos,el,brl) -> + RCases(loc,sty, infos, List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, List.map zeta_normalize_br brl ) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, zeta_normalize_term b, - (na,option_map zeta_normalize_term e_option), + (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs ) @@ -659,24 +696,23 @@ let expand_as = with Not_found -> rt end | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args) - | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b) - | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b) + | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b) + | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b) | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) | RLetTuple(loc,nal,(na,po),v,b) -> - RLetTuple(loc,nal,(na,option_map (expand_as map) po), + RLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) | RIf(loc,e,(na,po),br1,br2) -> - RIf(loc,expand_as map e,(na,option_map (expand_as map) po), + RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) - | RCases(loc,po,el,brl) -> - RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + | RCases(loc,sty,po,el,brl) -> + RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - and expand_as_br map (loc,idl,cpl,rt) = - (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) + (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt) in expand_as Idmap.empty diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index 9647640c..358c6ba6 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -22,7 +22,7 @@ val mkRApp : rawconstr*(rawconstr list) -> rawconstr val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr -val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr +val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr val mkRSort : rawsort -> rawconstr val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *) val mkRCast : rawconstr* rawconstr -> rawconstr @@ -31,8 +31,14 @@ val mkRCast : rawconstr* rawconstr -> rawconstr These are analogous to the ones constrs *) val raw_decompose_prod : rawconstr -> (Names.name*rawconstr) list * rawconstr +val raw_decompose_prod_or_letin : + rawconstr -> (Names.name*rawconstr option*rawconstr option) list * rawconstr val raw_decompose_prod_n : int -> rawconstr -> (Names.name*rawconstr) list * rawconstr +val raw_decompose_prod_or_letin_n : int -> rawconstr -> + (Names.name*rawconstr option*rawconstr option) list * rawconstr val raw_compose_prod : rawconstr -> (Names.name*rawconstr) list -> rawconstr +val raw_compose_prod_or_letin: rawconstr -> + (Names.name*rawconstr option*rawconstr option) list -> rawconstr val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list) diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml new file mode 100644 index 00000000..c9bf2f1f --- /dev/null +++ b/contrib/funind/recdef.ml @@ -0,0 +1,1430 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* next_global_ident_away false id (acc@ids)::acc) + idl + [] + +let pf_get_new_id id g = + List.hd (pf_get_new_ids [id] g) + +let h_intros l = + tclMAP h_intro l + +let do_observe_tac s tac g = + let goal = begin (Printer.pr_goal (sig_it g)) end in + try let v = tac g in msgnl (goal ++ fnl () ++ (str "recdef ") ++ + (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;; + + +let observe_tac s tac g = + if Tacinterp.get_debug () <> Tactic_debug.DebugOff + then do_observe_tac s tac g + else tac g + +let hyp_ids = List.map id_of_string + ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res"; + "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];; + +let rec nthtl = function + l, 0 -> l | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];; + +let hyp_id n l = List.nth l n;; + +let (x_id:identifier) = hyp_id 0 hyp_ids;; +let (v_id:identifier) = hyp_id 1 hyp_ids;; +let (k_id:identifier) = hyp_id 2 hyp_ids;; +let (def_id:identifier) = hyp_id 3 hyp_ids;; +let (p_id:identifier) = hyp_id 4 hyp_ids;; +let (h_id:identifier) = hyp_id 5 hyp_ids;; +let (n_id:identifier) = hyp_id 6 hyp_ids;; +let (h'_id:identifier) = hyp_id 7 hyp_ids;; +let (ano_id:identifier) = hyp_id 8 hyp_ids;; +let (rec_res_id:identifier) = hyp_id 10 hyp_ids;; +let (hspec_id:identifier) = hyp_id 11 hyp_ids;; +let (heq_id:identifier) = hyp_id 12 hyp_ids;; +let (hrec_id:identifier) = hyp_id 13 hyp_ids;; +let (hex_id:identifier) = hyp_id 14 hyp_ids;; +let (teq_id:identifier) = hyp_id 15 hyp_ids;; +let (pmax_id:identifier) = hyp_id 16 hyp_ids;; +let (hle_id:identifier) = hyp_id 17 hyp_ids;; + +let message s = if Flags.is_verbose () then msgnl(str s);; + +let def_of_const t = + match (kind_of_term t) with + Const sp -> + (try (match (Global.lookup_constant sp) with + {const_body=Some c} -> Declarations.force c + |_ -> assert false) + with _ -> + anomaly ("Cannot find definition of constant "^ + (string_of_id (id_of_label (con_label sp)))) + ) + |_ -> assert false + +let type_of_const t = + match (kind_of_term t) with + Const sp -> Typeops.type_of_constant (Global.env()) sp + |_ -> assert false + +let arg_type t = + match kind_of_term (def_of_const t) with + Lambda(a,b,c) -> b + | _ -> assert false;; + +let evaluable_of_global_reference r = + match r with + ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> assert false;; + + +let rank_for_arg_list h = + let predicate a b = + try List.for_all2 eq_constr a b with + Invalid_argument _ -> false in + let rec rank_aux i = function + | [] -> None + | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in + rank_aux 0;; + +let rec (find_call_occs : int -> constr -> constr -> + (constr list -> constr) * constr list list) = + fun nb_lam f expr -> + match (kind_of_term expr) with + App (g, args) when g = f -> + (fun l -> List.hd l), [Array.to_list args] + | App (g, args) -> + let (largs: constr list) = Array.to_list args in + let rec find_aux = function + [] -> (fun x -> []), [] + | a::upper_tl -> + (match find_aux upper_tl with + (cf, ((arg1::args) as args_for_upper_tl)) -> + (match find_call_occs nb_lam f a with + cf2, (_ :: _ as other_args) -> + let rec avoid_duplicates args = + match args with + | [] -> (fun _ -> []), [] + | h::tl -> + let recomb_tl, args_for_tl = + avoid_duplicates tl in + match rank_for_arg_list h args_for_upper_tl with + | None -> + (fun l -> List.hd l::recomb_tl(List.tl l)), + h::args_for_tl + | Some i -> + (fun l -> List.nth l (i+List.length args_for_tl):: + recomb_tl l), + args_for_tl + in + let recombine, other_args' = + avoid_duplicates other_args in + let len1 = List.length other_args' in + (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))), + other_args'@args_for_upper_tl + | _, [] -> (fun x -> a::cf x), args_for_upper_tl) + | _, [] -> + (match find_call_occs nb_lam f a with + cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args) + | _, [] -> (fun x -> a::upper_tl), [])) in + begin + match (find_aux largs) with + cf, [] -> (fun l -> mkApp(g, args)), [] + | cf, args -> + (fun l -> mkApp (g, Array.of_list (cf l))), args + end + | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[]) + | Var(id) -> (fun l -> expr), [] + | Meta(_) -> error "find_call_occs : Meta" + | Evar(_) -> error "find_call_occs : Evar" + | Sort(_) -> (fun l -> expr), [] + | Cast(b,_,_) -> find_call_occs nb_lam f b + | Prod(_,_,_) -> error "find_call_occs : Prod" + | Lambda(na,t,b) -> + begin + match find_call_occs (succ nb_lam) f b with + | _, [] -> (* Lambda are authorized as long as they do not contain + recursives calls *) + (fun l -> expr),[] + | _ -> error "find_call_occs : Lambda" + end + | LetIn(na,v,t,b) -> + begin + match find_call_occs nb_lam f v, find_call_occs (succ nb_lam) f b with + | (_,[]),(_,[]) -> + ((fun l -> expr), []) + | (_,[]),(cf,(_::_ as l)) -> + ((fun l -> mkLetIn(na,v,t,cf l)),l) + | (cf,(_::_ as l)),(_,[]) -> + ((fun l -> mkLetIn(na,cf l,t,b)), l) + | _ -> error "find_call_occs : LetIn" + end + | Const(_) -> (fun l -> expr), [] + | Ind(_) -> (fun l -> expr), [] + | Construct (_, _) -> (fun l -> expr), [] + | Case(i,t,a,r) -> + (match find_call_occs nb_lam f a with + cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args) + | _ -> (fun l -> expr),[]) + | Fix(_) -> error "find_call_occs : Fix" + | CoFix(_) -> error "find_call_occs : CoFix";; + +let coq_constant s = + Coqlib.gen_constant_in_modules "RecursiveDefinition" + (Coqlib.init_modules @ Coqlib.arith_modules) s;; + +let constant sl s = + constr_of_global + (locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let find_reference sl s = + (locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let delayed_force f = f () + +let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") +let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm") + +let le_trans = function () -> (coq_constant "le_trans") +let le_lt_trans = function () -> (coq_constant "le_lt_trans") +let lt_S_n = function () -> (coq_constant "lt_S_n") +let le_n = function () -> (coq_constant "le_n") +let refl_equal = function () -> (coq_constant "refl_equal") +let eq = function () -> (coq_constant "eq") +let ex = function () -> (coq_constant "ex") +let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") +let coq_sig = function () -> (coq_constant "sig") +let coq_O = function () -> (coq_constant "O") +let coq_S = function () -> (coq_constant "S") + +let gt_antirefl = function () -> (coq_constant "gt_irrefl") +let lt_n_O = function () -> (coq_constant "lt_n_O") +let lt_n_Sn = function () -> (coq_constant "lt_n_Sn") + +let f_equal = function () -> (coq_constant "f_equal") +let well_founded_induction = function () -> (coq_constant "well_founded_induction") +let well_founded = function () -> (coq_constant "well_founded") +let acc_rel = function () -> (coq_constant "Acc") +let acc_inv_id = function () -> (coq_constant "Acc_inv") +let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") +let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded") +let max_ref = function () -> (find_reference ["Recdef"] "max") +let iter = function () -> (constr_of_global (delayed_force iter_ref)) +let max_constr = function () -> (constr_of_global (delayed_force max_ref)) + +let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") +let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" + +(* These are specific to experiments in nat with lt as well_founded_relation, *) +(* but this should be made more general. *) +let nat = function () -> (coq_constant "nat") +let lt = function () -> (coq_constant "lt") + +(* This is simply an implementation of the case_eq tactic. this code + should be replaced with the tactic defined in Ltac in Init/Tactics.v *) +let mkCaseEq a : tactic = + (fun g -> + let type_of_a = pf_type_of g a in + tclTHENLIST + [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; + (fun g2 -> + change_in_concl None + (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2)) + g2); + simplest_case a] g);; + +(* This is like the previous one except that it also rewrite on all + hypotheses except the ones given in the first argument. All the + modified hypotheses are generalized in the process and should be + introduced back later; the result is the pair of the tactic and the + list of hypotheses that have been generalized and cleared. *) +let mkDestructEq : + identifier list -> constr -> goal sigma -> tactic * identifier list = + fun not_on_hyp expr g -> + let hyps = pf_hyps g in + let to_revert = + Util.map_succeed + (fun (id,_,t) -> + if List.mem id not_on_hyp || not (Termops.occur_term expr t) + then failwith "is_expr_context"; + id) hyps in + let to_revert_constr = List.rev_map mkVar to_revert in + let type_of_expr = pf_type_of g expr in + let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|]):: + to_revert_constr in + tclTHENLIST + [h_generalize new_hyps; + (fun g2 -> + change_in_concl None + (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2); + simplest_case expr], to_revert + +let rec mk_intros_and_continue thin_intros (extra_eqn:bool) + cont_function (eqs:constr list) nb_lam (expr:constr) g = + let finalize () = if extra_eqn then + let teq = pf_get_new_id teq_id g in + tclTHENLIST + [ h_intro teq; + thin thin_intros; + h_intros thin_intros; + + tclMAP + (fun eq -> tclTRY (Equality.general_rewrite_in true all_occurrences teq eq false)) + (List.rev eqs); + (fun g1 -> + let ty_teq = pf_type_of g1 (mkVar teq) in + let teq_lhs,teq_rhs = + let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in + args.(1),args.(2) + in + cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1 + ) + ] + g + else + tclTHENSEQ[ + thin thin_intros; + h_intros thin_intros; + cont_function eqs expr + ] g + in + if nb_lam = 0 + then finalize () + else + match kind_of_term expr with + | Lambda (n, _, b) -> + let n1 = + match n with + Name x -> x + | Anonymous -> ano_id + in + let new_n = pf_get_new_id n1 g in + tclTHEN (h_intro new_n) + (mk_intros_and_continue thin_intros extra_eqn cont_function eqs + (pred nb_lam) (subst1 (mkVar new_n) b)) g + | _ -> + assert false +(* finalize () *) +let const_of_ref = function + ConstRef kn -> kn + | _ -> anomaly "ConstRef expected" + +let simpl_iter clause = + reduce + (Lazy + {rBeta=true;rIota=true;rZeta= true; rDelta=false; + rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) +(* (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *) + clause + +(* The boolean value is_mes expresses that the termination is expressed + using a measure function instead of a well-founded relation. *) +let tclUSER tac is_mes l g = + let clear_tac = + match l with + | None -> h_clear true [] + | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l) + in + tclTHENSEQ + [ + clear_tac; + if is_mes + then tclTHEN + (unfold_in_concl [(all_occurrences, evaluable_of_global_reference + (delayed_force ltof_ref))]) + tac + else tac + ] + g + + +let list_rewrite (rev:bool) (eqs: constr list) = + tclREPEAT + (List.fold_right + (fun eq i -> tclORELSE (rewriteLR eq) i) + (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; + +let base_leaf_terminate (func:global_reference) eqs expr = +(* let _ = msgnl (str "entering base_leaf") in *) + (fun g -> + let k',h = + match pf_get_new_ids [k_id;h_id] g with + [k';h] -> k',h + | _ -> assert false + in + tclTHENLIST + [observe_tac "first split" (split (ImplicitBindings [expr])); + observe_tac "second split" + (split (ImplicitBindings [delayed_force coq_O])); + observe_tac "intro k" (h_intro k'); + observe_tac "case on k" + (tclTHENS (simplest_case (mkVar k')) + [(tclTHEN (h_intro h) + (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl, + [| delayed_force coq_O |]))) + default_auto)); tclIDTAC ]); + intros; + simpl_iter onConcl; + unfold_constr func; + list_rewrite true eqs; + default_auto] g);; + +(* La fonction est donnee en premier argument a la + fonctionnelle suivie d'autres Lambdas et de Case ... + Pour recuperer la fonction f a partir de la + fonctionnelle *) + +let get_f foncl = + match (kind_of_term (def_of_const foncl)) with + Lambda (Name f, _, _) -> f + |_ -> error "la fonctionnelle est mal definie";; + + +let rec compute_le_proofs = function + [] -> assumption + | a::tl -> + tclORELSE assumption + (tclTHENS + (fun g -> + let le_trans = delayed_force le_trans in + let t_le_trans = compute_renamed_type g le_trans in + let m_id = + let _,_,t = destProd t_le_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id,a]) + g) + [compute_le_proofs tl; + tclORELSE (apply (delayed_force le_n)) assumption]) + +let make_lt_proof pmax le_proof = + tclTHENS + (fun g -> + let le_lt_trans = delayed_force le_lt_trans in + let t_le_lt_trans = compute_renamed_type g le_lt_trans in + let m_id = + let _,_,t = destProd t_le_lt_trans in + let na,_,_ = destProd t in + Nameops.out_name na + in + apply_with_bindings + (le_lt_trans, + ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) + [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); + tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; + +let rec list_cond_rewrite k def pmax cond_eqs le_proofs = + match cond_eqs with + [] -> tclIDTAC + | eq::eqs -> + (fun g -> + let t_eq = compute_renamed_type g (mkVar eq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + tclTHENS + (general_rewrite_bindings false all_occurrences + (mkVar eq, + ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; + dummy_loc, NamedHyp def_id, mkVar def]) false) + [list_cond_rewrite k def pmax eqs le_proofs; + observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g + ) + +let rec introduce_all_equalities func eqs values specs bound le_proofs + cond_eqs = + match specs with + [] -> + fun g -> + let ids = pf_ids_of_hyps g in + let s_max = mkApp(delayed_force coq_S, [|bound|]) in + let k = next_global_ident_away true k_id ids in + let ids = k::ids in + let h' = next_global_ident_away true (h'_id) ids in + let ids = h'::ids in + let def = next_global_ident_away true def_id ids in + tclTHENLIST + [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max])); + observe_tac "introduce_all_equalities_final intro k" (h_intro k); + tclTHENS + (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k))) + [ + tclTHENLIST[h_intro h'; + simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])); + default_full_auto]; + tclIDTAC + ]; + observe_tac "clearing k " (clear [k]); + observe_tac "intros k h' def" (h_intros [k;h';def]); + observe_tac "simple_iter" (simpl_iter onConcl); + observe_tac "unfold functional" + (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]); + observe_tac "rewriting equations" + (list_rewrite true eqs); + observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs); + observe_tac "refl equal" (apply (delayed_force refl_equal))] g + | spec1::specs -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let p = next_global_ident_away true p_id ids in + let ids = p::ids in + let pmax = next_global_ident_away true pmax_id ids in + let ids = pmax::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + let hle2 = next_global_ident_away true hle_id ids in + let ids = hle2::ids in + let heq = next_global_ident_away true heq_id ids in + tclTHENLIST + [simplest_elim (mkVar spec1); + list_rewrite true eqs; + h_intros [p; heq]; + simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|])); + h_intros [pmax; hle1; hle2]; + introduce_all_equalities func eqs values specs + (mkVar pmax) ((mkVar pmax)::le_proofs) + (heq::cond_eqs)] g;; + +let string_match s = + if String.length s < 3 then failwith "string_match"; + try + for i = 0 to 3 do + if String.get s i <> String.get "Acc_" i then failwith "string_match" + done; + with Invalid_argument _ -> failwith "string_match" + +let retrieve_acc_var g = + (* Julien: I don't like this version .... *) + let hyps = pf_ids_of_hyps g in + map_succeed + (fun id -> string_match (string_of_id id);id) + hyps + +let rec introduce_all_values concl_tac is_mes acc_inv func context_fn + eqs hrec args values specs = + (match args with + [] -> + tclTHENLIST + [observe_tac "split" (split(ImplicitBindings + [context_fn (List.map mkVar (List.rev values))])); + observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs + (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] + | arg::args -> + (fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let rec_res = next_global_ident_away true rec_res_id ids in + let ids = rec_res::ids in + let hspec = next_global_ident_away true hspec_id ids in + let tac = + observe_tac "introduce_all_values" ( + introduce_all_values concl_tac is_mes acc_inv func context_fn eqs + hrec args + (rec_res::values)(hspec::specs)) in + (tclTHENS + (observe_tac "elim h_rec" + (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))) + ) + [tclTHENLIST [h_intros [rec_res; hspec]; + tac]; + (tclTHENS + (observe_tac "acc_inv" (apply (Lazy.force acc_inv))) + [(* tclTHEN (tclTRY(list_rewrite true eqs)) *) + (observe_tac "h_assumption" h_assumption) + ; + tclTHENLIST + [ + tclTRY(list_rewrite true eqs); + observe_tac "user proof" + (fun g -> + tclUSER + concl_tac + is_mes + (Some (hrec::hspec::(retrieve_acc_var g)@specs)) + g + ) + ] + ] + ) + ]) g) + + ) + + +let rec_leaf_terminate f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = + match find_call_occs 0 f_constr expr with + | context_fn, args -> + observe_tac "introduce_all_values" + (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) + +let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) + (f_constr:constr) (func:global_reference) base_leaf rec_leaf = + let rec proveterminate (eqs:constr list) (expr:constr) = + try + (* let _ = msgnl (str "entering proveterminate") in *) + let v = + match (kind_of_term expr) with + Case (ci, t, a, l) -> + (match find_call_occs 0 f_constr a with + _,[] -> + (fun g -> + let destruct_tac, rev_to_thin_intro = + mkDestructEq rec_arg_id a g in + tclTHENS destruct_tac + (list_map_i + (fun i -> mk_intros_and_continue + (List.rev rev_to_thin_intro) + true + proveterminate + eqs + ci.ci_cstr_nargs.(i)) + 0 (Array.to_list l)) g) + | _, _::_ -> + (match find_call_occs 0 f_constr expr with + _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr) + | _, _:: _ -> + observe_tac "rec_leaf" + (rec_leaf is_mes acc_inv hrec func eqs expr))) + | _ -> + (match find_call_occs 0 f_constr expr with + _,[] -> + (try observe_tac "base_leaf" (base_leaf func eqs expr) + with e -> (msgerrnl (str "failure in base case");raise e )) + | _, _::_ -> + observe_tac "rec_leaf" + (rec_leaf is_mes acc_inv hrec func eqs expr)) in + v + with e -> begin msgerrnl(str "failure in proveterminate"); raise e end + in + proveterminate + +let hyp_terminates nb_args func = + let a_arrow_b = arg_type (constr_of_global func) in + let rev_args,b = decompose_prod_n nb_args a_arrow_b in + let left = + mkApp(delayed_force iter, + Array.of_list + (lift 5 a_arrow_b:: mkRel 3:: + constr_of_global func::mkRel 1:: + List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args) + ) + ) + in + let right = mkRel 5 in + let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in + let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in + let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in + let nb_iter = + mkApp(delayed_force ex, + [|delayed_force nat; + (mkLambda + (Name + p_id, + delayed_force nat, + (mkProd (Name k_id, delayed_force nat, + mkArrow cond result))))|])in + let value = mkApp(delayed_force coq_sig, + [|b; + (mkLambda (Name v_id, b, nb_iter))|]) in + compose_prod rev_args value + + + +let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = + if is_mes + then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof)) + else tclUSER concl_tac is_mes names_to_suppress + +let termination_proof_header is_mes input_type ids args_id relation + rec_arg_num rec_arg_id tac wf_tac : tactic = + begin + fun g -> + let nargs = List.length args_id in + let pre_rec_args = + List.rev_map + mkVar (fst (list_chop (rec_arg_num - 1) args_id)) + in + let relation = substl pre_rec_args relation in + let input_type = substl pre_rec_args input_type in + let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in + let wf_rec_arg = + next_global_ident_away true + (id_of_string ("Acc_"^(string_of_id rec_arg_id))) + (wf_thm::ids) + in + let hrec = next_global_ident_away true hrec_id + (wf_rec_arg::wf_thm::ids) in + let acc_inv = + lazy ( + mkApp ( + delayed_force acc_inv_id, + [|input_type;relation;mkVar rec_arg_id|] + ) + ) + in + tclTHEN + (h_intros args_id) + (tclTHENS + (observe_tac + "first assert" + (assert_tac + true (* the assert thm is in first subgoal *) + (Name wf_rec_arg) + (mkApp (delayed_force acc_rel, + [|input_type;relation;mkVar rec_arg_id|]) + ) + ) + ) + [ + (* accesibility proof *) + tclTHENS + (observe_tac + "second assert" + (assert_tac + true + (Name wf_thm) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + ) + ) + [ + (* interactive proof that the relation is well_founded *) + observe_tac "wf_tac" (wf_tac is_mes (Some args_id)); + (* this gives the accessibility argument *) + observe_tac + "apply wf_thm" + (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])) + ) + ] + ; + (* rest of the proof *) + tclTHENSEQ + [observe_tac "generalize" + (onNLastHyps (nargs+1) + (fun (id,_,_) -> + tclTHEN (h_generalize [mkVar id]) (h_clear false [id]) + )) + ; + observe_tac "h_fix" (h_fix (Some hrec) (nargs+1)); + h_intros args_id; + h_intro wf_rec_arg; + observe_tac "tac" (tac wf_rec_arg hrec acc_inv) + ] + ] + ) g + end + + + +let rec instantiate_lambda t l = + match l with + | [] -> t + | a::l -> + let (bound_name, _, body) = destLambda t in + instantiate_lambda (subst1 a body) l +;; + + +let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic = + begin + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + let func_body = (def_of_const (constr_of_global func)) in + let (f_name, _, body1) = destLambda func_body in + let f_id = + match f_name with + | Name f_id -> next_global_ident_away true f_id ids + | Anonymous -> anomaly "Anonymous function" + in + let n_names_types,_ = decompose_lam_n nb_args body1 in + let n_ids,ids = + List.fold_left + (fun (n_ids,ids) (n_name,_) -> + match n_name with + | Name id -> + let n_id = next_global_ident_away true id ids in + n_id::n_ids,n_id::ids + | _ -> anomaly "anonymous argument" + ) + ([],(f_id::ids)) + n_names_types + in + let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in + let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in + termination_proof_header + is_mes + input_type + ids + n_ids + relation + rec_arg_num + rec_arg_id + (fun rec_arg_id hrec acc_inv g -> + (proveterminate + [rec_arg_id] + is_mes + acc_inv + hrec + (mkVar f_id) + func + base_leaf_terminate + (rec_leaf_terminate (mkVar f_id) concl_tac) + [] + expr + ) + g + ) + (tclUSER_if_not_mes concl_tac) + g + end + +let get_current_subgoals_types () = + let pts = get_pftreestate () in + let _,subs = extract_open_pftreestate pts in + List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs ) + +let build_and_l l = + let and_constr = Coqlib.build_coq_and () in + let conj_constr = coq_conj () in + let mk_and p1 p2 = + Term.mkApp(and_constr,[|p1;p2|]) in + let rec f = function + | [] -> failwith "empty list of subgoals!" + | [p] -> p,tclIDTAC,1 + | p1::pl -> + let c,tac,nb = f pl in + mk_and p1 c, + tclTHENS + (apply (constr_of_global conj_constr)) + [tclIDTAC; + tac + ],nb+1 + in f l + + +let is_rec_res id = + let rec_res_name = string_of_id rec_res_id in + let id_name = string_of_id id in + try + String.sub id_name 0 (String.length rec_res_name) = rec_res_name + with _ -> false + +let clear_goals = + let rec clear_goal t = + match kind_of_term t with + | Prod(Name id as na,t,b) -> + let b' = clear_goal b in + if noccurn 1 b' && (is_rec_res id) + then pop b' + else if b' == b then t + else mkProd(na,t,b') + | _ -> map_constr clear_goal t + in + List.map clear_goal + + +let build_new_goal_type () = + let sub_gls_types = get_current_subgoals_types () in + let sub_gls_types = clear_goals sub_gls_types in + let res = build_and_l sub_gls_types in + res + + + (* +let prove_with_tcc lemma _ : tactic = + fun gls -> + let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in + tclTHENSEQ + [ + h_generalize [lemma]; + h_intro hid; + Elim.h_decompose_and (mkVar hid); + gen_eauto(* default_eauto *) false (false,5) [] (Some []) + (* default_auto *) + ] + gls + *) + + + +let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = + let current_proof_name = get_current_proof_name () in + let name = match goal_name with + | Some s -> s + | None -> + try (add_suffix current_proof_name "_subproof") + with _ -> anomaly "open_new_goal with an unamed theorem" + in + let sign = Global.named_context () in + let sign = clear_proofs sign in + let na = next_global_ident_away false name [] in + if occur_existential gls_type then + Util.error "\"abstract\" cannot handle existentials"; + let hook _ _ = + let opacity = + let na_ref = Libnames.Ident (dummy_loc,na) in + let na_global = Nametab.global na_ref in + match na_global with + ConstRef c -> + let cb = Global.lookup_constant c in + if cb.Declarations.const_opaque then true + else begin match cb.const_body with None -> true | _ -> false end + | _ -> anomaly "equation_lemma: not a constant" + in + let lemma = mkConst (Lib.make_con na) in + ref_ := Some lemma ; + let lid = ref [] in + let h_num = ref (-1) in + Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None); + build_proof + ( fun gls -> + let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in + tclTHENSEQ + [ + h_generalize [lemma]; + h_intro hid; + (fun g -> + let ids = pf_ids_of_hyps g in + tclTHEN + (Elim.h_decompose_and (mkVar hid)) + (fun g -> + let ids' = pf_ids_of_hyps g in + lid := List.rev (list_subtract ids' ids); + if !lid = [] then lid := [hid]; +(* list_iter_i *) +(* (fun i v -> *) +(* msgnl (str "hyp" ++ int i ++ str " " ++ *) +(* Nameops.pr_id v ++ fnl () ++ fnl())) *) +(* !lid; *) + tclIDTAC g + ) + g + ); + ] gls) + (fun g -> + match kind_of_term (pf_concl g) with + | App(f,_) when eq_constr f (well_founded ()) -> + Auto.h_auto None [] (Some []) g + | _ -> + incr h_num; + tclTHEN + (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + e_assumption + g) +; + Command.save_named opacity; + in + start_proof + na + (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) + sign + gls_type + hook ; + by ( + fun g -> + tclTHEN + (decompose_and_tac) + (tclORELSE + (tclFIRST + (List.map + (fun c -> + tclTHENSEQ + [intros; + h_simplest_apply (interp_constr Evd.empty (Global.env()) c); + tclCOMPLETE Auto.default_auto + ] + ) + using_lemmas) + ) tclIDTAC) + g); + try + by tclIDTAC; (* raises UserError _ if the proof is complete *) + if Flags.is_verbose () then (pp (Printer.pr_open_subgoals())) + with UserError _ -> + defined () + +;; + + +let com_terminate + tcc_lemma_name + tcc_lemma_ref + is_mes + fonctional_ref + input_type + relation + rec_arg_num + thm_name using_lemmas + nb_args + hook = + let start_proof (tac_start:tactic) (tac_end:tactic) = + let (evmap, env) = Command.get_current_context() in + start_proof thm_name + (Global, Proof Lemma) (Environ.named_context_val env) + (hyp_terminates nb_args fonctional_ref) hook; + by (observe_tac "starting_tac" tac_start); + by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num )) + + in + start_proof tclIDTAC tclIDTAC; + try + let new_goal_type = build_new_goal_type () in + open_new_goal start_proof using_lemmas tcc_lemma_ref + (Some tcc_lemma_name) + (new_goal_type) + with Failure "empty list of subgoals!" -> + (* a non recursive function declared with measure ! *) + defined () + + + + +let ind_of_ref = function + | IndRef (ind,i) -> (ind,i) + | _ -> anomaly "IndRef expected" + +let (value_f:constr list -> global_reference -> constr) = + fun al fterm -> + let d0 = dummy_loc in + let rev_x_id_l = + ( + List.fold_left + (fun x_id_l _ -> + let x_id = next_global_ident_away true x_id x_id_l in + x_id::x_id_l + ) + [] + al + ) + in + let fun_body = + RCases + (d0,RegularStyle,None, + [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l), + (Anonymous,None)], + [d0, [v_id], [PatCstr(d0,(ind_of_ref + (delayed_force coq_sig_ref),1), + [PatVar(d0, Name v_id); + PatVar(d0, Anonymous)], + Anonymous)], + RVar(d0,v_id)]) + in + let value = + List.fold_left2 + (fun acc x_id a -> + RLambda + (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), + acc + ) + ) + fun_body + rev_x_id_l + (List.rev al) + in + understand Evd.empty (Global.env()) value;; + +let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = + fun f_id kind value -> + let ce = {const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = true} in + ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; + +let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = + fun f_id kind input_type fterm_ref -> + declare_fun f_id kind (value_f input_type fterm_ref);; + +let rec n_x_id ids n = + if n = 0 then [] + else let x = next_global_ident_away true x_id ids in + x::n_x_id (x::ids) (n-1);; + +let start_equation (f:global_reference) (term_f:global_reference) + (cont_tactic:identifier list -> tactic) g = + let ids = pf_ids_of_hyps g in + let terminate_constr = constr_of_global term_f in + let nargs = nb_prod (type_of_const terminate_constr) in + let x = n_x_id ids nargs in + tclTHENLIST [ + h_intros x; + unfold_in_concl [(all_occurrences, evaluable_of_global_reference f)]; + observe_tac "simplest_case" + (simplest_case (mkApp (terminate_constr, + Array.of_list (List.map mkVar x)))); + observe_tac "prove_eq" (cont_tactic x)] g;; + +let base_leaf_eq func eqs f_id g = + let ids = pf_ids_of_hyps g in + let k = next_global_ident_away true k_id ids in + let p = next_global_ident_away true p_id (k::ids) in + let v = next_global_ident_away true v_id (p::k::ids) in + let heq = next_global_ident_away true heq_id (v::p::k::ids) in + let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in + let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in + tclTHENLIST [ + h_intros [v; hex]; + simplest_elim (mkVar hex); + h_intros [p;heq1]; + tclTRY + (rewriteRL + (mkApp(mkVar heq1, + [|mkApp (delayed_force coq_S, [|mkVar p|]); + mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|]))); + simpl_iter onConcl; + tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]); + list_rewrite true eqs; + apply (delayed_force refl_equal)] g;; + +let f_S t = mkApp(delayed_force coq_S, [|t|]);; + + +let rec introduce_all_values_eq cont_tac functional termine + f p heq1 pmax bounds le_proofs eqs ids = + function + [] -> + let heq2 = next_global_ident_away true heq_id ids in + tclTHENLIST + [forward None (IntroIdentifier heq2) + (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); + simpl_iter (onHyp heq2); + unfold_in_hyp [((true,[1]), evaluable_of_global_reference + (global_of_constr functional))] + ((all_occurrences_expr, heq2), Tacexpr.InHyp); + tclTHENS + (fun gls -> + let t_eq = compute_renamed_type gls (mkVar heq2) in + let def_id = + let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in + Nameops.out_name def_na + in + observe_tac "rewrite heq" (general_rewrite_bindings false all_occurrences + (mkVar heq2, + ExplicitBindings[dummy_loc,NamedHyp def_id, + f]) false) gls) + [tclTHENLIST + [observe_tac "list_rewrite" (list_rewrite true eqs); + cont_tac pmax le_proofs]; + tclTHENLIST[apply (delayed_force le_lt_SS); + compute_le_proofs le_proofs]]] + | arg::args -> + let v' = next_global_ident_away true v_id ids in + let ids = v'::ids in + let hex' = next_global_ident_away true hex_id ids in + let ids = hex'::ids in + let p' = next_global_ident_away true p_id ids in + let ids = p'::ids in + let new_pmax = next_global_ident_away true pmax_id ids in + let ids = pmax::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + let hle2 = next_global_ident_away true hle_id ids in + let ids = hle2::ids in + let heq = next_global_ident_away true heq_id ids in + let ids = heq::ids in + let heq2 = next_global_ident_away true heq_id ids in + let ids = heq2::ids in + tclTHENLIST + [mkCaseEq(mkApp(termine, Array.of_list arg)); + h_intros [v'; hex']; + simplest_elim(mkVar hex'); + h_intros [p']; + simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax; + mkVar p'|])); + h_intros [new_pmax;hle1;hle2]; + introduce_all_values_eq + (fun pmax' le_proofs'-> + tclTHENLIST + [cont_tac pmax' le_proofs'; + h_intros [heq;heq2]; + observe_tac ("rewriteRL " ^ (string_of_id heq2)) + (tclTRY (rewriteLR (mkVar heq2))); + tclTRY (tclTHENS + ( fun g -> + let t_eq = compute_renamed_type g (mkVar heq) in + let k_id,def_id = + let k_na,_,t = destProd t_eq in + let _,_,t = destProd t in + let def_na,_,_ = destProd t in + Nameops.out_name k_na,Nameops.out_name def_na + in + let c_b = (mkVar heq, + ExplicitBindings + [dummy_loc, NamedHyp k_id, + f_S(mkVar pmax'); + dummy_loc, NamedHyp def_id, f]) + in + observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false all_occurrences + c_b false)) + g + ) + [tclIDTAC; + tclTHENLIST + [apply (delayed_force le_lt_n_Sm); + compute_le_proofs le_proofs']])]) + functional termine f p heq1 new_pmax + (p'::bounds)((mkVar pmax)::le_proofs) eqs + (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args] + + +let rec_leaf_eq termine f ids functional eqs expr fn args = + let p = next_global_ident_away true p_id ids in + let ids = p::ids in + let v = next_global_ident_away true v_id ids in + let ids = v::ids in + let hex = next_global_ident_away true hex_id ids in + let ids = hex::ids in + let heq1 = next_global_ident_away true heq_id ids in + let ids = heq1::ids in + let hle1 = next_global_ident_away true hle_id ids in + let ids = hle1::ids in + tclTHENLIST + [observe_tac "intros v hex" (h_intros [v;hex]); + simplest_elim (mkVar hex); + h_intros [p;heq1]; + h_generalize [mkApp(delayed_force le_n,[|mkVar p|])]; + h_intros [hle1]; + observe_tac "introduce_all_values_eq" (introduce_all_values_eq + (fun _ _ -> tclIDTAC) + functional termine f p heq1 p [] [] eqs ids args); + observe_tac "failing here" (apply (delayed_force refl_equal))] + +let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) + (eqs:constr list) (expr:constr) = +(* tclTRY *) + (match kind_of_term expr with + Case(ci,t,a,l) -> + (match find_call_occs 0 f a with + _,[] -> + (fun g -> + let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in + tclTHENS + destruct_tac + (list_map_i + (fun i -> mk_intros_and_continue + (List.rev rev_to_thin_intro) true + (prove_eq termine f functional) + eqs ci.ci_cstr_nargs.(i)) + 0 (Array.to_list l)) g) + | _,_::_ -> + (match find_call_occs 0 f expr with + _,[] -> base_leaf_eq functional eqs f + | fn,args -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + rec_leaf_eq termine f ids + (constr_of_global functional) + eqs expr fn args g)) + | _ -> + (match find_call_occs 0 f expr with + _,[] -> base_leaf_eq functional eqs f + | fn,args -> + fun g -> + let ids = ids_of_named_context (pf_hyps g) in + observe_tac "rec_leaf_eq" (rec_leaf_eq + termine f ids (constr_of_global functional) + eqs expr fn args) g));; + +let (com_eqn : identifier -> + global_reference -> global_reference -> global_reference + -> constr -> unit) = + fun eq_name functional_ref f_ref terminate_ref equation_lemma_type -> + let opacity = + match terminate_ref with + | ConstRef c -> + let cb = Global.lookup_constant c in + if cb.Declarations.const_opaque then true + else begin match cb.const_body with None -> true | _ -> false end + | _ -> anomaly "terminate_lemma: not a constant" + in + let (evmap, env) = Command.get_current_context() in + let f_constr = (constr_of_global f_ref) in + let equation_lemma_type = subst1 f_constr equation_lemma_type in + (start_proof eq_name (Global, Proof Lemma) + (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); + by + (start_equation f_ref terminate_ref + (fun x -> + prove_eq + (constr_of_global terminate_ref) + f_constr + functional_ref + [] + (instantiate_lambda + (def_of_const (constr_of_global functional_ref)) + (f_constr::List.map mkVar x) + ) + ) + ); +(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) +(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) + Flags.silently (fun () ->Command.save_named opacity) () ; +(* Pp.msgnl (str "eqn finished"); *) + + );; + +let nf_zeta env = + Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + env + Evd.empty + +let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq + generate_induction_principle using_lemmas : unit = + let function_type = interp_constr Evd.empty (Global.env()) type_of_f in + let env = push_named (function_name,None,function_type) (Global.env()) in +(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) + let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in +(* Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *) + let res_vars,eq' = decompose_prod equation_lemma_type in + let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in + let eq' = nf_zeta env_eq' eq' in + let res = +(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) +(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) +(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) + match kind_of_term eq' with + | App(e,[|_;_;eq_fix|]) -> + mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) + | _ -> failwith "Recursive Definition (res not eq)" + in + let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in + let (_, rec_arg_type, _) = destProd function_type_before_rec_arg in + let arg_types = List.rev_map snd (fst (decompose_prod_n (List.length res_vars) function_type)) in + let equation_id = add_suffix function_name "_equation" in + let functional_id = add_suffix function_name "_F" in + let term_id = add_suffix function_name "_terminate" in + let functional_ref = declare_fun functional_id (IsDefinition Definition) res in + let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in + let relation = + interp_constr + Evd.empty + env_with_pre_rec_args + r + in + let tcc_lemma_name = add_suffix function_name "_tcc" in + let tcc_lemma_constr = ref None in +(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) + let hook _ _ = + let term_ref = Nametab.locate (make_short_qualid term_id) in + let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in +(* message "start second proof"; *) + let stop = ref false in + begin + try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type) + with e -> + begin + if Tacinterp.get_debug () <> Tactic_debug.DebugOff + then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) + else anomaly "Cannot create equation Lemma" + ; +(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) + stop := true; + end + end; + if not !stop + then + let eq_ref = Nametab.locate (make_short_qualid equation_id ) in + let f_ref = destConst (constr_of_global f_ref) + and functional_ref = destConst (constr_of_global functional_ref) + and eq_ref = destConst (constr_of_global eq_ref) in + generate_induction_principle f_ref tcc_lemma_constr + functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; + if Flags.is_verbose () + then msgnl (h 1 (Ppconstr.pr_id function_name ++ + spc () ++ str"is defined" )++ fnl () ++ + h 1 (Ppconstr.pr_id equation_id ++ + spc () ++ str"is defined" ) + ) + in + try + com_terminate + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + rec_arg_type + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + hook + with e -> + begin + ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); +(* anomaly "Cannot create termination Lemma" *) + raise e + end + + + diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 deleted file mode 100644 index 5d19079b..00000000 --- a/contrib/funind/tacinv.ml4 +++ /dev/null @@ -1,872 +0,0 @@ -(*i camlp4deps: "parsing/grammar.cma" i*) - -(*s FunInv Tactic: inversion following the shape of a function. *) - -(* Deprecated: see indfun_main.ml4 instead *) - -(* Don't delete this file yet, it may be used for other purposes *) - -(*i*) -open Termops -open Equality -open Names -open Pp -open Tacmach -open Proof_type -open Tacinterp -open Tactics -open Tacticals -open Term -open Util -open Printer -open Reductionops -open Inductiveops -open Coqlib -open Refine -open Typing -open Declare -open Decl_kinds -open Safe_typing -open Vernacinterp -open Evd -open Environ -open Entries -open Setoid_replace -open Tacinvutils -(*i*) - -module Smap = Map.Make(struct type t = constr let compare = compare end) -let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m [] -let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2 -let rec listsuf i l = if i<=0 then l else listsuf (i-1) (List.tl l) -let rec listpref i l = if i<=0 then [] else List.hd l :: listpref (i-1) (List.tl l) -let rec split3 l = - List.fold_right (fun (e1,e2,e3) (a,b,c) -> (e1::a),(e2::b),(e3::c)) l ([],[],[]) - -let mkthesort = mkProp (* would like to put Type here, but with which index? *) - -(* this is the prefix used to name equality hypothesis generated by - case analysis*) -let equality_hyp_string = "_eg_" - -(* bug de refine: on doit ssavoir sur quelle hypothese on se trouve. valeur - initiale au debut de l'appel a la fonction proofPrinc: 1. *) -let nthhyp = ref 1 - -let debug i = prstr ("DEBUG "^ string_of_int i ^"\n") -let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2) -(* Operations on names *) -let id_of_name = function - Anonymous -> id_of_string "H" - | Name id -> id;; -let string_of_name nme = string_of_id (id_of_name nme) - (*end debugging *) - -(* Interpretation of constr's *) -let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c - -(*s specific manipulations on constr *) -let lift1_leqs leq= - List.map - (function (r,(typofg,g,d)) - -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq - -let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq - -(* WARNING: In the types, we don't lift the rels in the type. This is - intentional. Use with care. *) -let lift1_lvars lvars= List.map - (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars - -let pop1_levar levars = List.map (function ev,tev -> ev, popn 1 tev) levars - - -let rec add_n_dummy_prod t n = - if n<=0 then t - else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort t) (n-1) - -(* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1] - [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables - are not specified *) -let rec add_lambdas t gl lcsr = - match lcsr with - | [] -> t - | csr::lcsr' -> - let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in - lambda_id hyp_csr hyptyp (add_lambdas t gl lcsr') - -(* [add_pis t gl [csr1;csr2...]] returns ([x1] :type of [csr1] - [x2]:type of csr2) [t]*) -let rec add_pis t gl lcsr = - match lcsr with - | [] -> t - | csr::lcsr' -> - let hyp_csr,hyptyp = csr,(pf_type_of gl csr) in - prod_id hyp_csr hyptyp (add_pis t gl lcsr') - -let mkProdEg teq eql eqr concl = - mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl) - -let eqs_of_beqs x = - List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x - - -let rec eqs_of_beqs_named_aux s i l = - match l with - | [] -> [] - | (r,(a,b,c))::l' -> - (Name(id_of_string (s^ string_of_int i)), mkEq a b c) - ::eqs_of_beqs_named_aux s (i-1) l' - - -let eqs_of_beqs_named s l = eqs_of_beqs_named_aux s (List.length l) l - -let rec patternify ltypes c nme = - match ltypes with - | [] -> c - | (mv,t)::ltypes' -> - let c'= substitterm 0 mv (mkRel 1) c in - let tlift = lift (List.length ltypes') t in - let res = - patternify ltypes' (mkLambda (newname_append nme "rec", tlift, c')) nme in - res - -let rec npatternify ltypes c = - match ltypes with - | [] -> c - | (mv,nme,t)::ltypes' -> - let c'= substitterm 0 mv (mkRel 1) c in - let tlift = lift (List.length ltypes') t in - let res = - npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in - res - -(* fait une application (c m1 m2...mn, où mi est une evar, on rend également - la liste des evar munies de leur type) *) -let rec apply_levars c lmetav = - match lmetav with - | [] -> [],c - | (i,typ) :: lmetav' -> - let levars,trm = apply_levars c lmetav' in - let exkey = mknewexist() in - ((exkey,typ)::levars), applistc trm [mkEvar exkey] - (* EXPERIMENT le refine est plus long si on met un cast: - ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *) - - -let prod_change_concl c newconcl = - let lv,_ = decompose_prod c in prod_it newconcl lv - -let lam_change_concl c newconcl = - let lv,_ = decompose_prod c in lam_it newconcl lv - - -let rec mkAppRel c largs n = - match largs with - | [] -> c - | arg::largs' -> - let newc = mkApp (c,[|(mkRel n)|]) in mkAppRel newc largs' (n-1) - -let applFull c typofc = - let lv,t = decompose_prod typofc in - let ltyp = List.map fst lv in - let res = mkAppRel c ltyp (List.length ltyp) in - res - -(* Take two terms with same structure and return a map of deBruijn from the - first to the second. Only DeBruijn should be different between the two - terms. *) -let rec build_rel_map typ type_of_b = - match (kind_of_term typ), (kind_of_term type_of_b) with - Evar _ , Evar _ -> Smap.empty - | Const c1, Const c2 when c1=c2 -> Smap.empty - | Ind c1, Ind c2 when c1=c2 -> Smap.empty - | Rel i, Rel j when i=j -> Smap.empty - | Rel i, Rel j -> Smap.add typ type_of_b Smap.empty - | Prod (name,c1,c2), Prod (nameb,c1b,c2b) -> - let map1 = build_rel_map c1 c1b in - let map2 = build_rel_map (pop c2) (pop c2b) in - merge_smap map1 map2 - | App (f,args), App (fb,argsb) when Array.length args = Array.length argsb -> - build_rel_map_list (Array.to_list args) (Array.to_list argsb) - | _,_ -> failwith ("Could not generate case annotation. "^ - "Incompatibility between annotation and actual type") - -and build_rel_map_list ltyp ltype_of_b = - List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c)) - Smap.empty ltyp ltype_of_b - - -(*s Use (and proof) of the principle *) - -(* This is the type of the argument of [proofPrinc] *) - -type mimickinfo = - { - concl: constr; (* conclusion voulue, cad (xi:ti)gl, ou gl est le but a - prouver, et xi:ti correspondent aux arguments donnés à - la tactique. On enlèvera un produit à chaque fois - qu'on rencontrera un binder, sans lift ou pop. - Initialement: une seule conclusion, puis specifique à - chaque branche. *) - absconcl: constr array; (* conclusions patternisées pour pouvoir être - appliquées = un predicat pour chaque fixpt - mutuel. *) - mimick: constr; (* le terme qu'on imite. On plongera dedans au fur et - à mesure, sans lift ni pop. *) - env: env; (* The global typing environment, we will add thing in it when - going inside the term (push_rel, push_rec_types) *) - sigma: Evd.evar_map; - nmefonc: constr array; (* la constante correspondant à la fonction - appelée, permet de remplacer les appels - recursifs par des appels à la constante - correspondante (non pertinent (et inutile) si - on permet l'appel de la tactique sur une terme - donné directement (au lieu d'une constante - comme pour l'instant)). *) - fonc: int * int; (* bornes des indices des variable correspondant aux - appels récursifs (plusieurs car fixp. mutuels), - utile pour reconnaître les appels récursifs - (ATTENTION: initialement vide, reste vide tant qu'on - n'est pas dans un fix). *) - doeqs: bool; (* this reference is to toggle building of equalities during - the building of the principle (default is true) *) - fix: bool; (* did I already went through a fix or case constr? lambdas - found before a case or a fix are treated as parameters of - the induction principle *) - lst_vars: (constr*(name*constr)) list ; (* Variables rencontrées jusque là *) - lst_eqs: (Term.constr * (Term.constr * Term.constr * Term.constr)) list ; - (* liste d'équations engendrées au cours du - parcours, cette liste grandit à chaque - case, et il faut lifter le tout à chaque - binder *) - lst_recs: constr list ; (* appels récursifs rencontrés jusque là *) - } - -(* This is the return type of [proofPrinc] *) -type 'a funind = (* 'A = CONTR OU CONSTR ARRAY *) - { - - princ:'a; (* le (ou les) principe(s) demandé(s), il contient des meta - variables représentant soit des trous à prouver plus tard, - soit les conclusions à compléter avant de rendre le terme - (suivant qu'on utilise le principe pour faire refine ou - functional scheme). Il y plusieurs conclusions si plusieurs - fonction mutuellement récursives) voir la suite. *) - evarlist: (constr*Term.types) list; (* [(ev1,tev1);(ev2,tev2)...]] - l'ensemble des meta variables - correspondant à des trous. [evi] - est la meta variable, [tevi] est - son type. *) - hypnum: (int*int*int) list; (* [[(in,jn,kn)...]] sont les nombres - respectivement de variables, d'équations, - et d'hypothèses de récurrence pour le but - n. Permet de faire le bon nombre d'intros - et des rewrite au bons endroits dans la - suite. *) - mutfixmetas: constr array ; (* un tableau de meta variables correspondant - à chacun des prédicats mutuellement - récursifs construits. *) - conclarray: types array; (* un tableau contenant les conclusions - respectives de chacun des prédicats - mutuellement récursifs. Permet de finir la - construction du principe. *) - params:(constr*name*constr) list; (* [[(metavar,param,tparam)..]] la - liste des paramètres (les lambdas - au-dessus du fix) du fixpoint si - fixpoint il y a, le paramètre est - une meta var, dont on stocke le nom - et le type. TODO: utiliser la - structure adequat? *) - } - - - -let empty_funind_constr = - { - princ = mkProp; - evarlist = []; - hypnum = []; - mutfixmetas = [||]; - conclarray = [||]; - params = [] - } - -let empty_funind_array = - { empty_funind_constr with - princ = [||]; - } - -(* Replace the calls to the function (recursive calls) by calls to the - corresponding constant *) -let replace_reccalls mi b = - let d,f = mi.fonc in - let res = ref b in - let _ = for i = d to f do - res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in - !res - - - -(* collects all information of match branches stored in [l] *) -let rec collect_cases l = - match l with - | [||] -> empty_funind_array - | arr -> - let x = arr.(0) in - let resrec = collect_cases (Array.sub arr 1 (Array.length arr - 1)) in - { x with - princ= Array.append [|x.princ|] resrec.princ; - evarlist = x.evarlist@resrec.evarlist; - hypnum = x.hypnum@resrec.hypnum; - } - -let collect_pred l = - let l1,l2,l3 = split3 l in - Array.of_list l1 , Array.of_list l2 , Array.of_list l3 - - -(* [build_pred n tarr] builds the right predicates for each element of [tarr] - (of type: [type array] of size [n]). Return the list of triples: - (?i , - fun (x1:t1) ... (xn:tn) => (?i x1...xn) , - forall (x1:t1) ... (xn:tn), (?i x1...xn)), - where ti's are deduced from elements of tarr, which are of the form: - t1 -> t2 -> ... -> tn -> . *) -let rec build_pred n tarr = - if n >= Array.length tarr (* iarr *) then [] - else - let ftyp = Array.get tarr n in - let gl = mknewmeta() in - let gl_app = applFull gl ftyp in - let pis = prod_change_concl ftyp gl_app in - let gl_abstr = lam_change_concl ftyp gl_app in - (gl,gl_abstr,pis):: build_pred (n+1) tarr - - -let heq_prefix = "H_eq_" - -type kind_of_hyp = Var | Eq (*| Rec*) - -(* the main function, build the principle by exploring the term and reproduce - the same structure. *) -let rec proofPrinc mi: constr funind = - match kind_of_term mi.mimick with - (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on - the name of recursive calls *) - | Fix((iarr,i),(narr,tarr,carr)) -> - (* We construct the right predicates for each mutual fixpt *) - let evararr,newabsconcl,pisarr = collect_pred (build_pred 0 tarr) in - let newenv = push_rec_types (narr,tarr,carr) mi.env in - let anme',aappel_rec,llevar,llposeq = - collect_fix mi 0 iarr narr carr pisarr newabsconcl newenv in - let anme = Array.map (fun nme -> newname_append nme "_ind") anme' in - { - princ = mkFix((iarr,i),(anme, pisarr,aappel_rec)); - evarlist= pop1_levar llevar; (* llevar are put outside the fix, so we pop 1 *) - hypnum = llposeq; - mutfixmetas = evararr; - conclarray = pisarr; - params = [] - } - (* Cases b of arrPt end.*) - | Case (cinfo, pcase, b, arrPt) -> - let prod_pcase,_ = decompose_lam pcase in - let _nmeb,_ = List.hd prod_pcase in - let newb'= apply_leqtrpl_t b mi.lst_eqs in - let type_of_b = Typing.type_of mi.env mi.sigma b in - (* Replace the recursive calls to the function by calls to the constant *) - let newb = replace_reccalls mi newb' in - let cases = collect_cases (Array.mapi (fold_proof mi b type_of_b newb) arrPt) in - (* the match (case) annotation must be transformed, see [build_pcase] below *) - let newpcase = build_pcase mi pcase b type_of_b newb in - let trm' = mkCase (cinfo,newpcase,newb, cases.princ) in - { cases with - princ = if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) else trm'; - params = [] (* FIX: fix parms here (fixpt inside a match)*) - } - - - | Lambda(nme, typ, cstr) -> - let _, _, cconcl = destProd mi.concl in - let d,f=mi.fonc in - let newenv = push_rel (nme,None,typ) mi.env in - let newlst_var = (* if this lambda is a param, then don't add it here *) - if mi.fix then (mkRel 1,(nme,typ)) :: lift1_lvars mi.lst_vars - else (*(mkRel 1,(nme,typ)) :: *) lift1_lvars mi.lst_vars in - let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv; - fonc = (if d > 0 then d+1 else 0) , (if f > 0 then f+1 else 0); - lst_vars = newlst_var ; lst_eqs = lift1_leqs mi.lst_eqs; - lst_recs = lift1L mi.lst_recs} in - let resrec = proofPrinc newmi in - (* are we inside a fixpoint or a case? then this is a normal lambda *) - if mi.fix - then { resrec with princ = mkLambda (nme,typ,resrec.princ) ; params = [] } - else (* otherwise this is a parameter *) - let metav = mknewmeta() in - let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in - { resrec with - princ = substmeta resrec.princ; - evarlist = List.map (fun (ev,tev) -> ev, substmeta tev) resrec.evarlist; - conclarray = Array.map substmeta resrec.conclarray; - params = (metav,nme,typ) :: resrec.params - } - - - | LetIn(nme,cstr1, typ, cstr) -> - failwith ("I don't deal with let ins yet. "^ - "Please expand them before applying this function.") - - | u -> - let varrels = List.rev (List.map fst mi.lst_vars) in - let varnames = List.map snd mi.lst_vars in - let nb_vars = List.length varnames in - let nb_eqs = List.length mi.lst_eqs in - let _eqrels = List.map fst mi.lst_eqs in - (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs - trouvés dans les let in et les Cases avec ceux trouves dans u (ie - mi.mimick). *) - (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *) - let terms_recs = mi.lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in - (*c construction du terme: application successive des variables, des - egalites et des appels rec, a la variable existentielle correspondant a - l'hypothese de recurrence en cours. *) - (* d'abord, on fabrique les types des appels recursifs en replacant le nom - de des fonctions par les predicats dans [terms_recs]: [(f_i t u v)] - devient [(P_i t u v)] *) - (* TODO optimiser ici: *) - let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in - let typeofhole'' = prod_it_anonym_lift mi.concl appsrecpred in - let typeofhole = prodn nb_vars varnames typeofhole'' in - (* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point, - mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les - '?' à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *) - let newmeta = mknewmeta() in - let concl_with_var = applistc newmeta varrels in - let conclrecs = applistc concl_with_var terms_recs in - { empty_funind_constr with - princ = conclrecs; - evarlist = [ newmeta , typeofhole ]; - hypnum = [ nb_vars , List.length terms_recs , nb_eqs ]; - conclarray = mi.absconcl; - } - - -(* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant - l'annotation de type du case [pcase] contient des lambdas supplémentaires - en tête. Je les récupère dans la variable [suppllam_pcase]. Le problème est - que la conclusion de l'annotation du nouveauacse doit faire référence à ces - variables plutôt qu'à celle de l'exterieur. Ce qui suit permet de changer - les reference de newpcase' pour pointer vers les lambda du piquant. On - procède comme suit: on repère les rels qui pointent à l'interieur de - l'annotation dans la fonction initiale et on les relie à celle du type - voulu pour le case, pour ça ([build_rel_map]) on parcourt en même temps le - dernier lambda du piquant ([typ]) (qui contient le type de l'argument du - case) et le type attendu pour le case ([type_of_b]) et on construit un - map. Ensuite on remplace les rels correspondant dans la preuve construite - en suivant le map. *) - -and build_pcase mi pcase b type_of_b newb = - let prod_pcase,_ = decompose_lam pcase in - let nme,typ = List.hd prod_pcase in - (* je remplace b par rel1 (apres avoir lifte un coup) dans la future - annotation du futur case: ensuite je mettrai un lambda devant *) - let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 mi.concl) in - let suppllam_pcase = List.tl prod_pcase in - let suppllam_pcasel = List.length suppllam_pcase in - let rel_smap = - if suppllam_pcasel=0 then Smap.empty else (* FIX: is this test necessary ? *) - build_rel_map (lift suppllam_pcasel type_of_b) typ in - let newpcase''' = - Smap.fold (fun e e' acc -> substitterm 0 e (lift 1 e') acc) - rel_smap typeof_case'' in - let neweq = mkEq (lift (suppllam_pcasel + 1) type_of_b) - (lift (suppllam_pcasel + 1) newb) (mkRel 1) in - let newpcase'' = - if mi.doeqs - then mkProd (name_of_string "eg", neweq, lift 1 newpcase''') - else newpcase''' in - (* construction du dernier lambda du piquant. *) - let newpcase' = mkLambda (newname_append nme "_ind" ,typ, newpcase'') in - (* ajout des lambdas supplémentaires (type dépendant) du piquant. *) - lamn suppllam_pcasel suppllam_pcase newpcase' - - -(* [fold_proof mi b typeofb newb l n] rend le resultat de l'appel recursif sur - cstr (correpsondant au ième elt de [arrPt] ci-dessus et donc au ième - constructeur de [typeofb]), appele avec les bons arguments: [mi.concl] - devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments - du constructeur considéré, et [concl'] est [mi.concl] ou l'on a réécrit [b] - en ($c_n$ [rel1]...). *) -and fold_proof mi b type_of_b newb i cstr = - let new_lst_recs = mi.lst_recs @ hdMatchSub_cpl b mi.fonc in - (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3 - x2 x1... ], sans quoi les annotations ne sont plus coherentes *) - let cstr_appl,nargs = nth_dep_constructor type_of_b i in - let concl'' = - substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in - let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in - let concl_dummy = add_n_dummy_prod concl'' nargs in - let lsteqs_rew = apply_eq_leqtrpl mi.lst_eqs neweq in - let new_lsteqs = (mkRel (-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in - let a',a'' = decompose_lam_n nargs cstr in - let newa'' = - if mi.doeqs - then mkLambda (name_of_string heq_prefix,lift nargs neweq,lift 1 a'') - else a'' in - let newmimick = lamn nargs a' newa'' in - let b',b'' = decompose_prod_n nargs concl_dummy in - let newb'' = - if mi.doeqs - then mkProd (name_of_string heq_prefix,lift nargs neweq,lift 1 b'') - else b'' in - let newconcl = prodn nargs b' newb'' in - let newmi = {mi with mimick=newmimick; concl=newconcl; fix=true; - lst_eqs= new_lsteqs; lst_recs = new_lst_recs} in - proofPrinc newmi - - -and collect_fix mi n iarr narr carr pisarr newabsconcl newenv = - if n >= Array.length iarr then [||],[||],[],[] - else - let nme = Array.get narr n in - let c = Array.get carr n in - (* rappelle sur le sous-terme, on ajoute un niveau de - profondeur (lift) parce que Fix est un binder. *) - let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl; - mimick=c; fonc=(1,((Array.length iarr)));env=newenv;fix=true; - lst_vars=lift1_lvars mi.lst_vars; lst_eqs=lift1_leqs mi.lst_eqs; - lst_recs= lift1L mi.lst_recs;} in - let resrec = proofPrinc newmi in - let lnme,lappel_rec,llevar,llposeq = - collect_fix mi (n+1) iarr narr carr pisarr newabsconcl newenv in - Array.append [|nme|] lnme , Array.append [|resrec.princ|] lappel_rec - , (resrec.evarlist@llevar) , (resrec.hypnum@llposeq) - -let mkevarmap_aux ex = let x,y = ex in (mkevarmap_from_listex x),y - - -(* TODO: deal with any term, not only a constant. *) -let interp_fonc_tacarg fonctac gl = - (* [fonc] is the constr corresponding to fontact not unfolded, - if [fonctac] is a (qualified) name then this is a [const] ?. *) -(* let fonc = constr_of_Constr fonctac in *) - (* TODO: replace the [with _ -> ] by something more precise in - the following. *) - (* [def_fonc] is the definition of fonc. TODO: We should do this only - if [fonc] is a const, and take [fonc] otherwise.*) - try fonctac, pf_const_value gl (destConst fonctac) - with _ -> failwith ("don't know how to deal with this function " - ^"(DEBUG:is it a constante?)") - - - - -(* [invfun_proof fonc def_fonc gl_abstr pis] builds the principle, - following the shape of [def_fonc], [fonc] is the constant - corresponding to [def_func] (or a reduced form of it ?), gl_abstr and - pis are the goal to be proved, of the form [x,y...]g and (x.y...)g. - - This function calls the big function proofPrinc. *) - -let invfun_proof fonc def_fonc gl_abstr pis env sigma = - let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env; - sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false ; - lst_vars = []; lst_eqs = []; lst_recs = []} in - proofPrinc mi - -(* Do intros [i] times, then do rewrite on all introduced hyps which are called - like [heq_prefix], FIX: have another filter than the name. *) -let rec iterintro i = - if i<=0 then tclIDTAC else - tclTHEN - (tclTHEN - intro - (iterintro (i-1))) - (fun gl -> - (tclREPEAT - (tclNTH_HYP i - (fun hyp -> - let hypname = (string_of_id (destVar hyp)) in - let sub = - try String.sub hypname 0 (String.length heq_prefix) - with _ -> "" (* different than [heq_prefix] *) in - if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite")) - )) gl) - - -(* - (fun hyp gl -> - let _ = prstr ("nthhyp= "^ string_of_int i) in - if isConst hyp && ((name_of_const hyp)==heq_prefix) then - let _ = prstr "YES\n" in - rewriteLR hyp gl - else - let _ = prstr "NO\n" in - tclIDTAC gl) - *) - -(* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic - which: - \begin{itemize} - \item Do refine on C (the induction principle), - \item try to Clear listargs_ids - \item if boolean dorew is true, then intro all new hypothesis, and - try rewrite on those hypothesis that are equalities. - \end{itemize} -*) - -let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq = - (tclTHEN_i - (tclTHEN - (tclTHEN - (* Refine on the right term (following the sheme of the - given function) *) - (fun gl -> refine open_princ_proof_applied gl) - (* Clear the hypothesis given as arguments of the tactic - (because they are generalized) *) - (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids)))) - (* Now we introduce the created hypothesis, and try rewrite on - equalities due to case analysis *) - (fun gl -> (tclIDTAC gl))) - (fun i gl -> - if not dorew then tclIDTAC gl - else - (* d,m,f correspond respectively to vars, induction hyps and - equalities*) - let d,m,f = List.nth lposeq (i-1) in - tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) gl) - ) - gl - - - - -(* This function trys to reduce instanciated arguments, provided they - are of the form [(C t u v...)] where [C] is a constructor, and - provided that the argument is not the argument of a fixpoint (i.e. the - argument corresponds to a simple lambda) . *) -let rec applistc_iota cstr lcstr env sigma = - match lcstr with - | [] -> cstr,[] - | arg::lcstr' -> - let arghd = - if isApp arg then let x,_ = destApp arg in x else arg in - if isConstruct arghd (* of the form [(C ...)]*) - then - applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg]))) - lcstr' env sigma - else - try - let nme,typ,suite = destLambda cstr in - let c, l = applistc_iota suite lcstr' env sigma in - mkLambda (nme,typ,c), arg::l - with _ -> cstr,arg::lcstr' (* the arg does not correspond to a lambda*) - - - -(* TODO: ne plus mettre les sous-but à l'exterieur, mais à l'intérieur (le bug - de refine est normalement resolu). Ca permettra 2 choses: d'une part que - les preuves soient plus simple, et d'autre part de fabriquer un terme de - refine qui pourra s'aapliquer SANS FAIRE LES INTROS AVANT, ce qui est bcp - mieux car fonctionne comme induction et plus comme inversion (pas de perte - de connexion entre les hypothèse et les variables). *) - -(*s Tactic that makes induction and case analysis following the shape - of a function (idf) given with arguments (listargs) *) -let invfun c l dorew gl = -(* \begin{itemize} - \item [fonc] = the constant corresponding to the function - (necessary for equalities of the form [(f x1 x2 ...)=...] where - [f] is the recursive function). - \item [def_fonc] = body of the function, where let ins have - been expanded. *) - let fonc, def_fonc' = interp_fonc_tacarg c gl in - let def_fonc'',listargs' = - applistc_iota def_fonc' l (pf_env gl) (project gl) in - let def_fonc = expand_letins def_fonc'' in - (* quantifies on previously generalized arguments. - [(x1:T1)...g[arg1 <- x1 ...]] *) - let pis = add_pis (pf_concl gl) gl listargs' in - (* princ_proof builds the principle *) - let _ = resetmeta() in - let pr = invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in - (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *) - let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in - (* apply parameters immediately *) - let gl_abstr = - applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev pr.params)) in - (* we apply args of the fix now, the parameters will be applied later *) - let princ_proof_applied_args = - applistc pr.princ (listsuf (List.length pr.params) listargs') in - (* parameters are still there so patternify must not take them -> lift *) - let princ_proof_applied_lift = - lift (List.length pr.evarlist) princ_proof_applied_args in - let princ_applied_hyps'' = patternify (List.rev pr.evarlist) - princ_proof_applied_lift (Name (id_of_string "Hyp")) in - (* if there was a fix, we will not add "Q" as in funscheme, so we make a pop, - TODO: find were we made the lift in proofPrinc instead and supress it here, - and add lift in funscheme. *) - let princ_applied_hyps' = - if Array.length pr.mutfixmetas > 0 then popn 1 princ_applied_hyps'' - else princ_applied_hyps'' in - (* if there is was fix, we have to replace the meta representing the - predicate of the goal by the abstracted goal itself. *) - let princ_applied_hyps = - if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) - (substit_red 0 (pr.mutfixmetas.(0)) gl_abstr princ_applied_hyps') - else princ_applied_hyps' (* No Fixpoint *) in - let _ = prNamedConstr "princ_applied_hyps" princ_applied_hyps in - (* Same thing inside levar *) - let newlevar' = - if Array.length pr.mutfixmetas > 0 then(* mutual Fixpoint not treated in the tactic*) - List.map (fun (x,y) -> x,substit_red 0 (pr.mutfixmetas.(0)) gl_abstr y) pr.evarlist - else pr.evarlist - in - (* replace params metavar by real args *) - let rec replace_parms lparms largs t = - match lparms, largs with - [], _ -> t - | ((p,_,_)::lp), (a::la) -> let t'= substitterm 0 p a t in replace_parms lp la t' - | _, _ -> error "problem with number of args." in - let princ_proof_applied = replace_parms pr.params listargs' princ_applied_hyps in - let _ = prNamedLConstr "levar:" (List.map fst newlevar') in - let _ = prNamedLConstr "levar types:" (List.map snd newlevar') in - let _ = prNamedConstr "princ_proof_applied" princ_proof_applied in - (* replace also in levar *) - let newlevar = - List.rev (List.map (fun (x,y) -> x, replace_parms pr.params listargs' y) newlevar') in -(* - (* replace params metavar by abstracted variables *) - let princ_proof_params = npatternify (List.rev pr.params) princ_applied_hyps in - (* we apply now the real parameters *) - let princ_proof_applied = - applistc princ_proof_params (listpref (List.length pr.params) listargs') in -*) - let princ_applied_evars = apply_levars princ_proof_applied newlevar in - let open_princ_proof_applied = princ_applied_evars in - let _ = prNamedConstr "princ_applied_evars" (snd princ_applied_evars) in - let _ = prNamedLConstr "evars" (List.map snd (fst princ_applied_evars)) in - let listargs_ids = List.map destVar (List.filter isVar listargs') in - (* debug: impression du but*) - let lgl = Evd.to_list (sig_sig gl) in - let _ = prNamedLConstr "\ngl= " (List.map (fun x -> (snd x).evar_concl) lgl) in - let _ = prstr "fin gl \n\n" in - invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids - gl dorew pr.hypnum - -(* function must be a constant, all arguments must be given. *) -let invfun_verif c l dorew gl = - if not (isConst c) then error "given function is not a constant" - else - let x,_ = decompose_prod (pf_type_of gl c) in - if List.length x = List.length l then - try invfun c l dorew gl - with UserError (x,y) -> raise (UserError (x,y)) - else error "wrong number of arguments for the function" - - - - -(* Construction of the functional scheme. *) -let buildFunscheme fonc mutflist = - let def_fonc = expand_letins (def_of_const fonc) in - let ftyp = type_of (Global.env ()) Evd.empty fonc in - let _ = resetmeta() in - let gl = mknewmeta() in - let gl_app = applFull gl ftyp in - let pis = prod_change_concl ftyp gl_app in - (* Here we call the function invfun_proof, that effectively - builds the scheme *) -(* let princ_proof,levar,_,evararr,absc,parms = *) - let _ = prstr "Recherche du principe... lancement de invfun_proof\n" in - let pr = invfun_proof mutflist def_fonc [||] pis (Global.env()) Evd.empty in - (* parameters are still there (unboud rel), and patternify must not take them - -> lift*) - let princ_proof_lift = lift (List.length pr.evarlist) pr.princ in - let princ_proof_hyps = - patternify (List.rev pr.evarlist) princ_proof_lift (Name (id_of_string "Hyp")) in - let rec princ_replace_metas ev abs i t = - if i>= Array.length ev then t - else (* fix? *) - princ_replace_metas ev abs (i+1) - (mkLambda ( - (Name (id_of_string ("Q"^(string_of_int i)))), - prod_change_concl (lift 0 abs.(i)) mkthesort, - (substitterm 0 ev.(i) (mkRel 1) (lift 0 t)))) - in - let rec princ_replace_params params t = - List.fold_left ( - fun acc (ev,nam,typ) -> - mkLambda (Name (id_of_name nam) , typ, - substitterm 0 ev (mkRel 1) (lift 0 acc))) - t (List.rev params) in - if Array.length pr.mutfixmetas = 0 (* Is there a Fixpoint? *) - then (* No Fixpoint *) - princ_replace_params pr.params (mkLambda ((Name (id_of_string "Q")), - prod_change_concl ftyp mkthesort, - (substitterm 0 gl (mkRel 1) princ_proof_hyps))) - else (* there is a fix -> add parameters + replace metas *) - let princ_rpl = - princ_replace_metas pr.mutfixmetas pr.conclarray 0 princ_proof_hyps in - princ_replace_params pr.params princ_rpl - - - -(* Declaration of the functional scheme. *) -let declareFunScheme f fname mutflist = - let _ = prstr "Recherche du perincipe...\n" in - let id_to_cstr id = - try constr_of_id (Global.env()) id - with - Not_found -> error (string_of_id id ^ " not found in the environment") in - let flist = if mutflist=[] then [f] else mutflist in - let fcstrlist = Array.of_list (List.map id_to_cstr flist) in - let idf = id_to_cstr f in - let scheme = buildFunscheme idf fcstrlist in - let _ = prstr "Principe:" in - let _ = prconstr scheme in - let ce = { - const_entry_body = scheme; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true } in - let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in - () - - - -TACTIC EXTEND functional_induction - [ "old" "functional" "induction" constr(c) ne_constr_list(l) ] - -> [ invfun_verif c l true ] -END - -VERNAC COMMAND EXTEND FunctionalScheme - [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" - ident(c) "with" ne_ident_list(l) ] - -> [ declareFunScheme c na l ] -| [ "Old" "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ] - -> [ declareFunScheme c na [] ] -END - - - - - -(* -*** Local Variables: *** -*** compile-command: "make -C ../.. contrib/funind/tacinv.cmo" *** -*** tuareg-default-indent:1 *** -*** tuareg-begin-indent:1 *** -*** tuareg-let-indent:1 *** -*** tuareg-match-indent:-1 *** -*** tuareg-try-indent:1 *** -*** tuareg-with-indent:1 *** -*** tuareg-if-then-else-inden:1 *** -*** fill-column: 78 *** -*** indent-tabs-mode: nil *** -*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" *** -*** End: *** -*) - - diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml deleted file mode 100644 index ce775e0b..00000000 --- a/contrib/funind/tacinvutils.ml +++ /dev/null @@ -1,284 +0,0 @@ -(* tacinvutils.ml *) -(*s utilities *) - -(*i*) -open Names -open Util -open Term -open Termops -open Coqlib -open Pp -open Printer -open Inductiveops -open Environ -open Declarations -open Nameops -open Evd -open Sign -open Reductionops -(*i*) - -(*s printing of constr -- debugging *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) - -let prchr () = msg (str" (ret) \n") -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - -let prNamedLConstr_aux lc = - List.iter (prNamedConstr "#>") lc - -let prNamedLConstr s lc = - begin - prstr s; - prNamedLConstr_aux lc - end - - -(* FIXME: ref 1, pas bon, si? *) -let evarcpt = ref 0 -let metacpt = ref 0 -let mknewexist ()= - begin - evarcpt := !evarcpt+1; - !evarcpt,[||] - end - -let resetexist ()= evarcpt := 0 - -let mknewmeta ()= - begin - metacpt := !metacpt+1; - mkMeta (!metacpt) - end - -let resetmeta () = metacpt := 0 - -let rec mkevarmap_from_listex lex = - match lex with - | [] -> Evd.empty - | ((ex,_),typ)::lex' -> -(* let _ = prstr "mkevarmap" in - let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in - let _ = prstr "OF TYPE: " in - let _ = prconstr typ in*) - let info = { - evar_concl = typ; - evar_hyps = empty_named_context_val; - evar_body = Evar_empty; - evar_extra = None} in - Evd.add (mkevarmap_from_listex lex') ex info - -let mkEq typ c1 c2 = - mkApp (build_coq_eq(),[| typ; c1; c2|]) - -let mkRefl typ c1 = - mkApp ((build_coq_eq_data()).refl, [| typ; c1|]) - -let rec popn i c = if i<=0 then c else pop (popn (i-1) c) - - -(* Operations on names *) -let id_of_name = function - Anonymous -> id_of_string "H" - | Name id -> id;; -let string_of_name nme = string_of_id (id_of_name nme) -let name_of_string str = Name (id_of_string str) -let newname_append nme str = - Name(id_of_string ((string_of_id (id_of_name nme))^str)) - -(* Substitutions in constr *) - -let compare_constr_nosub t1 t2 = - if compare_constr (fun _ _ -> false) t1 t2 - then true - else false - -let rec compare_constr' t1 t2 = - if compare_constr_nosub t1 t2 - then true - else (compare_constr (compare_constr') t1 t2) - -let rec substitterm prof t by_t in_u = - if (compare_constr' (lift prof t) in_u) - then (lift prof by_t) - else map_constr_with_binders succ - (fun i -> substitterm i t by_t) prof in_u - - -let apply_eqtrpl eq t = - let r,(tb,b,by_t) = eq in - substitterm 0 b by_t t - -let apply_eqtrpl_lt lt eq = List.map (apply_eqtrpl eq) lt - -let apply_leqtrpl_t t leq = - List.fold_left (fun x y -> apply_eqtrpl y x) t leq - - -let apply_refl_term eq t = - let _,arr = destApp eq in - let reli= (Array.get arr 1) in - let by_t= (Array.get arr 2) in - substitterm 0 reli by_t t - -let apply_eq_leqtrpl leq eq = - List.map - (function (r,(tb,b,t)) -> - r,(tb, - (if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t)) - leq - - - -(* [(a b c) a] -> true *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - uhd=t - else false - -(* My operations on constr *) -let lift1L l = (List.map (lift 1) l) -let mkArrow_lift t1 t2 = mkArrow t1 (lift 1 t2) -let mkProd_liftc nme c1 c2 = mkProd (nme,c1,(lift 1 c2)) -(* prod_it_lift x [a1 a2 ...] *) -let prod_it_lift ini lcpl = - List.fold_right (function a,b -> (fun c -> mkProd_liftc a b c)) ini lcpl;; - -let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm - -let lam_it_anonymous trm lst = - List.fold_right - (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm - -let lambda_id id typeofid cstr = - let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in - substitterm 0 id (mkRel 0) cstr' - -let prod_id id typeofid cstr = - let cstr' = mkNamedProd (id_of_string "FUNX") typeofid cstr in - substitterm 0 id (mkRel 0) cstr' - - - - - -let nth_dep_constructor indtype n = - let sigma = Evd.empty and env = Global.env() in - let indtypedef = find_rectype env sigma indtype in - let indfam,_ = dest_ind_type indtypedef in - let arr_cstr_summary = get_constructors env indfam in - let cstr_sum = Array.get arr_cstr_summary n in - build_dependent_constructor cstr_sum, cstr_sum.cs_nargs - - -let rec buildrefl_from_eqs eqs = - match eqs with - | [] -> [] - | cstr::eqs' -> - let eq,args = destApp cstr in - (mkRefl (Array.get args 0) (Array.get args 2)) - :: (buildrefl_from_eqs eqs') - - - - -(* list of occurrences of a term inside another *) -(* Cofix will be wrong, not sure Fix is correct too *) -let rec hdMatchSub u t= - let subres = - match kind_of_term u with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t - | Fix (_,(lna,tl,bl)) -> - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) - [] bl - | LetIn _ -> assert false - (* Correct? *) - | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u - in - if constr_head_match u t then u :: subres else subres - - -(* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *) -let hdMatchSub_cpl u (d,f) = - let res = ref [] in - begin - for i = d to f do res := hdMatchSub u (mkRel i) @ !res done; - !res - end - - -(* destApplication raises an exception if [t] is not an application *) -let exchange_hd_prod subst_hd t = - let hd,args= destApplication t in mkApp (subst_hd,args) - -(* substitute t by by_t in head of products inside in_u, reduces each - product found *) -let rec substit_red prof t by_t in_u = - if constr_head_match in_u (lift prof t) - then - let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in - x - else - map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u - -(* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each - reli by tarr.(f-i). *) -let exchange_reli_arrayi tarr (d,f) t = - let hd,args= destApp t in - let i = destRel hd in - let res = whd_beta (mkApp (tarr.(f-i) ,args)) in - res - -let exchange_reli_arrayi_L tarr (d,f) = - List.map (exchange_reli_arrayi tarr (d,f)) - - -(* expand all letins in a term, before building the principle. *) -let rec expand_letins mimick = - match kind_of_term mimick with - | LetIn(nme,cstr1, typ, cstr) -> - let cstr' = substitterm 0 (mkRel 1) (lift 1 cstr1) cstr in - expand_letins (pop cstr') - | x -> map_constr expand_letins mimick - - -(* Valeur d'une constante, or identity *) -let def_of_const t = - match kind_of_term t with - | Const sp -> - (try - match Global.lookup_constant sp with - {const_body=Some c} -> force c - |_ -> assert false - with _ -> assert false) - | _ -> t - -(* nom d'une constante. Must be a constante. x*) -let name_of_const t = - match (kind_of_term t) with - Const cst -> Names.string_of_label (Names.con_label cst) - |_ -> assert false - ;; - - -(*i -*** Local Variables: -*** compile-command: "make -k tacinvutils.cmo" -*** test-tactic: "../../bin/coqtop -translate -q -batch -load-vernac-source ../../test-suite/success/Funind.v" -*** End: -i*) - diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli deleted file mode 100644 index 64b21213..00000000 --- a/contrib/funind/tacinvutils.mli +++ /dev/null @@ -1,80 +0,0 @@ -(* tacinvutils.ml *) -(*s utilities *) - -(*i*) -open Termops -open Equality -open Names -open Pp -open Tacmach -open Proof_type -open Tacinterp -open Tactics -open Tacticals -open Term -open Util -open Printer -open Reductionops -open Inductiveops -open Coqlib -open Refine -open Evd -(*i*) - -(* printing debugging *) -val prconstr: constr -> unit -val prlistconstr: constr list -> unit -val prNamedConstr:string -> constr -> unit -val prNamedLConstr:string -> constr list -> unit -val prstr: string -> unit - - -val mknewmeta: unit -> constr -val mknewexist: unit -> existential -val resetmeta: unit -> unit (* safe *) -val resetexist: unit -> unit (* be careful with this one *) -val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map -val mkEq: types -> constr -> constr -> constr -(* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *) -val mkRefl: types -> constr -> constr -val buildrefl_from_eqs: constr list -> constr list -(* typ c1 = mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *) - -val nth_dep_constructor: constr -> int -> (constr*int) - -val prod_it_lift: (name*constr) list -> constr -> constr -val prod_it_anonym_lift: constr -> constr list -> constr -val lam_it_anonymous: constr -> constr list -> constr -val lift1L: (constr list) -> constr list -val popn: int -> constr -> constr -val lambda_id: constr -> constr -> constr -> constr -val prod_id: constr -> constr -> constr -> constr - - -val name_of_string : string -> name -val newname_append: name -> string -> name - -val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr -val substitterm: int -> constr -> constr -> constr -> constr -val apply_leqtrpl_t: - constr -> (constr*(constr*constr*constr)) list -> constr -val apply_eq_leqtrpl: - (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list -(* val apply_leq_lt: constr list -> constr list -> constr list *) - -val hdMatchSub: constr -> constr -> constr list -val hdMatchSub_cpl: constr -> int*int -> constr list -val exchange_hd_prod: constr -> constr -> constr -val exchange_reli_arrayi_L: constr array -> int*int -> constr list -> constr list -val substit_red: int -> constr -> constr -> constr -> constr -val expand_letins: constr -> constr - -val def_of_const: constr -> constr -val name_of_const: constr -> string - -(*i - *** Local Variables: *** - *** compile-command: "make -C ../.. contrib/funind/tacinvutils.cmi" *** - *** End: *** -i*) - -- cgit v1.2.3