diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 12:55:09 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-04 12:55:09 +0000 |
| commit | d2cb529b790723c2315b980197e2846c14af1eeb (patch) | |
| tree | 48b6c44c63d863519783a93acee96af633195540 /contrib | |
| parent | 5c785f63a08464164df9e3182e019cf36ac8d2ff (diff) | |
- completely new version of "functional inversion" using inversion on
inductive
- bug correction in "Functional scheme" and "functional inversion": the
function are now parsed as references and not indent
- adding a zeta normalization function in rawtermops to zeta normalize
graph constructions (not used for now)
- Bug correction in generation of functional principle types (if an
arguments of the function has a type which is a sort)
- adding a new persistent table for functional induction informations
(graph,...)
- new save mechanism for functional induction principles (reuse of
proofs when possible)
- Minor bug correction in proof of principle.
- Distinguishing building_principles (that is save them) and making then
(just construct their proof term)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 30 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 386 | ||||
| -rw-r--r-- | contrib/funind/functional_principles_types.mli | 11 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 312 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.ml | 470 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.mli | 58 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 67 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 1024 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 14 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 60 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.mli | 6 |
11 files changed, 1813 insertions, 625 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 1173e1a41..14dfbdffc 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -909,6 +909,9 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = ] in Command.start_proof + (*i The next call to mk_equation_id is valid since we are constructing the lemma + Ensures by: obvious + i*) (mk_equation_id f_id) (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type @@ -920,16 +923,33 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = - let f_id = id_of_label (con_label (destConst f)) in - let equation_lemma_id = (mk_equation_id f_id) in let equation_lemma = try - Tacinterp.constr_of_id (pf_env g) equation_lemma_id - with Not_found -> + let finfos = find_Function_infos (destConst f) in + mkConst (out_some finfos.equation_lemma) + with (Not_found | Failure "out_some" 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 + i*) + let equation_lemma_id = (mk_equation_id f_id) in 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" -> + let finfos = find_Function_infos (destConst f) in + update_Function + {finfos with + equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with + ConstRef c -> c + | _ -> Util.anomaly "Not a constant" + ) + } + | _ -> () + + in Tacinterp.constr_of_id (pf_env g) equation_lemma_id in -(* observe (Ppconstr.pr_id equation_lemma_id ++ str " has type " ++ pr_lconstr_env (pf_env g) (pf_type_of g equation_lemma)); *) let nb_intro_to_do = nb_prod (pf_concl g) in tclTHEN (tclDO nb_intro_to_do intro) diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 9d337fec8..8e6ff7c2f 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -19,8 +19,21 @@ exception Toberemoved_with_rel of int*constr exception Toberemoved +let pr_elim_scheme el = + let env = Global.env () in + let msg = str "params := " ++ Printer.pr_rel_context env el.params in + let env = Environ.push_rel_context el.params env in + let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in + let env = Environ.push_rel_context el.predicates env in + let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in + let env = Environ.push_rel_context el.branches env in + let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in + let env = Environ.push_rel_context el.args env in + msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl +let observe s = if Functional_principles_proofs.do_observe () +then Pp.msgnl s let pr_elim_scheme el = @@ -285,124 +298,101 @@ let change_property_sort toSort princ princName = let pp_dur time time' = str (string_of_float (System.time_difference time time')) -let qed () = Command.save_named true +(* let qed () = save_named true *) let defined () = Command.save_named false -let generate_functional_principle - interactive_proof - old_princ_type sorts new_princ_name funs i proof_tac - = - let f = funs.(i) in - let type_sort = Termops.new_sort_in_family InType in - let new_sorts = - match sorts with - | None -> Array.make (Array.length funs) (type_sort) - | Some a -> a - in + + + + + +let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in - (* First we get the type of the old graph principle *) - let new_principle_type = + (* let time1 = System.get_time () in *) + let new_principle_type = compute_new_princ_type_from_rel (Array.map mkConst funs) - new_sorts + sorts old_princ_type - in -(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) - let base_new_princ_name,new_princ_name = - match new_princ_name with - | Some (id) -> id,id - | None -> - let id_of_f = id_of_label (con_label f) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in - let names = ref [new_princ_name] in - let hook _ _ = - if sorts = None - then -(* let id_of_f = id_of_label (con_label f) in *) - let register_with_sort fam_sort = - let s = Termops.new_sort_in_family fam_sort in - let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - let value = - change_property_sort s new_principle_type new_princ_name - in -(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = - { const_entry_body = value; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() - } - in - ignore( - Declare.declare_constant - name - (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) - ); - names := name :: !names - in - register_with_sort InProp; - register_with_sort InSet + (* let time2 = System.get_time () in *) + (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) + (* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) + let new_princ_name = + next_global_ident_away true (id_of_string "___________princ_________") [] in begin Command.start_proof new_princ_name (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type - hook + (hook new_principle_type) ; - try - let _tim1 = System.get_time () in - Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); - let _tim2 = System.get_time () in -(* begin *) -(* let dur1 = System.time_difference tim1 tim2 in *) -(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) -(* end; *) - let do_save = not (do_observe ()) && not interactive_proof in - let _ = - try -(* Vernacentries.show_script (); *) - Options.silently defined (); - let _dur2 = System.time_difference _tim2 (System.get_time ()) in -(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *) - Options.if_verbose - (fun () -> - Pp.msgnl ( - prlist_with_sep - (fun () -> str" is defined " ++ fnl ()) - Ppconstr.pr_id - (List.rev !names) ++ str" is defined " - ) - ) - () - with e when do_save -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not (do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end - in - () - -(* let tim3 = Sys.time () in *) -(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *) - - with - | e -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not ( do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + (* let _tim1 = System.get_time () in *) + Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + (* let _tim2 = System.get_time () in *) + (* begin *) + (* let dur1 = System.time_difference tim1 tim2 in *) + (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) + (* end; *) + get_proof_clean true end +let generate_functional_principle + interactive_proof + old_princ_type sorts new_princ_name funs i proof_tac + = + let f = funs.(i) in + let type_sort = Termops.new_sort_in_family InType in + let new_sorts = + match sorts with + | None -> Array.make (Array.length funs) (type_sort) + | Some a -> a + in + let base_new_princ_name,new_princ_name = + match new_princ_name with + | Some (id) -> id,id + | None -> + let id_of_f = id_of_label (con_label f) in + id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + in + let names = ref [new_princ_name] in + let hook new_principle_type _ _ = + if sorts = None + then + (* let id_of_f = id_of_label (con_label f) in *) + let register_with_sort fam_sort = + let s = Termops.new_sort_in_family fam_sort in + let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in + let value = change_property_sort s new_principle_type new_princ_name in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let ce = + { const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() + } + in + ignore( + Declare.declare_constant + name + (Entries.DefinitionEntry ce, + Decl_kinds.IsDefinition (Decl_kinds.Scheme) + ) + ); + names := name :: !names + in + register_with_sort InProp; + register_with_sort InSet + in + let (id,(entry,g_kind,hook)) = + build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook + in + save false new_princ_name entry g_kind hook +(* defined () *) + exception Not_Rec @@ -476,30 +466,20 @@ let get_funs_constant mp dp = l_const exception No_graph_found - -let make_scheme fas = +exception Found_type of int + +let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = - List.map - (fun (_,f,_) -> - try id_to_constr f - with Not_found -> - Util.error ("Cannot find "^ string_of_id f) - ) - fas - in - let first_fun = destConst (List.hd funs) in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let funs = List.map fst fas in + let first_fun = List.hd funs in + + + let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try - (* Fixme: take into account funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - with Not_found -> raise No_graph_found + fst (find_Function_infos first_fun).graph_ind + with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map fst this_block_funs_indexes in @@ -507,7 +487,7 @@ let make_scheme fas = let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.map - (function const -> List.assoc (destConst const) this_block_funs_indexes) + (function const -> List.assoc const this_block_funs_indexes) funs in let ind_list = @@ -519,49 +499,149 @@ let make_scheme fas = ) funs_indexes in - let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in + let l_schemes = + List.map + (Typing.type_of env sigma) + (Indrec.build_mutual_indrec env sigma ind_list) + in let i = ref (-1) in let sorts = - List.rev_map (fun (_,_,x) -> + List.rev_map (fun (_,x) -> Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) ) fas in - let princ_names = List.map (fun (x,_,_) -> x) fas in - let _ = List.map2 - (fun princ_name scheme_type -> - incr i; -(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) -(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) -(* ); *) - generate_functional_principle - false - scheme_type - (Some (Array.of_list sorts)) - (Some princ_name) - this_block_funs - !i - (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) - ) - princ_names - l_schemes + (* We create the first priciple by tactic *) + let first_type,other_princ_types = + match l_schemes with + s::l_schemes -> s,l_schemes + | _ -> anomaly "" in - () + let (_,(const,_,_)) = + build_functional_principle false + first_type + (Array.of_list sorts) + this_block_funs + 0 + (prove_princ_for_struct false 0 (Array.of_list funs)) + (fun _ _ _ -> ()) + in + incr i; + (* The others are just deduced *) + if other_princ_types = [] + then + [const] + else + let other_fun_princ_types = + let funs = Array.map mkConst this_block_funs in + let sorts = Array.of_list sorts in + List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types + in + let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) + let (idxs,_),(_,ta,_ as decl) = destFix fix in + let other_result = + List.map (* we can now compute the other principles *) + (fun scheme_type -> + incr i; + observe (Printer.pr_lconstr scheme_type); + let type_concl = snd (Sign.decompose_prod_assum scheme_type) in + let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in + let f = fst (decompose_app applied_f) in + try (* we search the number of the function in the fix block (name of the function) *) + Array.iteri + (fun j t -> + let t = snd (Sign.decompose_prod_assum t) in + let applied_g = List.hd (List.rev (snd (decompose_app t))) in + let g = fst (decompose_app applied_g) in + if eq_constr f g + then raise (Found_type j); + observe (Printer.pr_lconstr f ++ str " <> " ++ + Printer.pr_lconstr g) + + ) + ta; + (* If we reach this point, the two principle are not mutually recursive + We fall back to the previous method + *) + let (_,(const,_,_)) = + build_functional_principle + false + (List.nth other_princ_types (!i - 1)) + (Array.of_list sorts) + this_block_funs + !i + (prove_princ_for_struct false !i (Array.of_list funs)) + (fun _ _ _ -> ()) + in + const + with Found_type i -> + let princ_body = + Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt + in + {const with + Entries.const_entry_body = princ_body; + Entries.const_entry_type = Some scheme_type + } + ) + other_fun_princ_types + in + const::other_result + +let build_scheme fas = +(* (fun (f,_) -> *) +(* try Libnames.constr_of_global (Nametab.global f) *) +(* with Not_found -> *) +(* Util.error ("Cannot find "^ Libnames.string_of_reference f) *) +(* ) *) +(* fas *) -let make_case_scheme fa = + let bodies_types = + make_scheme + (List.map + (fun (_,f,sort) -> + let f_as_constant = + try + match Nametab.global f with + | Libnames.ConstRef c -> c + | _ -> Util.error "Functional Scheme can only be used with functions" + with Not_found -> + Util.error ("Cannot find "^ Libnames.string_of_reference f) + in + (f_as_constant,sort) + ) + 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 + ) + fas + bodies_types + + + +let build_case_scheme fa = let env = Global.env () and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = (fun (_,f,_) -> id_to_constr f) fa in +(* let id_to_constr id = *) +(* Tacinterp.constr_of_id env id *) +(* in *) + let funs = (fun (_,f,_) -> + try Libnames.constr_of_global (Nametab.global f) + with Not_found -> + Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun = destConst funs in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in - let first_fun_kn = - (* Fixme: take into accour funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - in + + let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in + + + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map fst this_block_funs_indexes in let prop_sort = InProp in diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli index 8b4faaf44..cf28c6e6c 100644 --- a/contrib/funind/functional_principles_types.mli +++ b/contrib/funind/functional_principles_types.mli @@ -1,5 +1,7 @@ open Names open Term + + val generate_functional_principle : (* do we accept interactive proving *) bool -> @@ -19,13 +21,14 @@ val generate_functional_principle : (constr array -> int -> Tacmach.tactic) -> unit - - val compute_new_princ_type_from_rel : constr array -> sorts array -> types -> types exception No_graph_found -val make_scheme : (identifier*identifier*Rawterm.rawsort) list -> unit -val make_case_scheme : (identifier*identifier*Rawterm.rawsort) -> unit +val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list + +val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list -> unit +val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort) -> unit + diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index d109b3746..3830cdb21 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -7,6 +7,124 @@ open Libnames open Rawterm open Declarations +let is_rec_info scheme_info = + let test_branche min acc (_,_,br) = + acc || ( + let new_branche = + Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in + let free_rels_in_br = Termops.free_rels new_branche in + let max = min + scheme_info.Tactics.npredicates in + Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br + ) + in + Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) + + +let choose_dest_or_ind scheme_info = + if is_rec_info scheme_info + then Tactics.new_induct + else Tactics.new_destruct + + +let functional_induction with_clean c princl pat = + let f,args = decompose_app c in + fun g -> + let princ,bindings, princ_type = + match princl with + | None -> (* No principle is given let's find the good one *) + begin + match kind_of_term f with + | Const c' -> + let princ_option = + let finfo = (* we first try to find out a graph on f *) + try find_Function_infos c' + with Not_found -> + errorlabstrm "" (str "Cannot find induction information on "++Printer.pr_lconstr (mkConst c') ) + in + match Tacticals.elimination_sort_of_goal g with + | InProp -> finfo.prop_lemma + | InSet -> finfo.rec_lemma + | InType -> finfo.rect_lemma + in + let princ = (* then we get the principle *) + try mkConst (out_some princ_option ) + with Failure "out_some" -> + (*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*) + let princ_name = + Indrec.make_elimination_ident + (id_of_label (con_label c')) + (Tacticals.elimination_sort_of_goal g) + in + try + mkConst(const_of_id princ_name ) + with Not_found -> (* This one is neither defined ! *) + errorlabstrm "" (str "Cannot find induction principle for " + ++Printer.pr_lconstr (mkConst c') ) + in + (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ) + | _ -> raise (UserError("",str "functional induction must be used with a function" )) + + end + | Some ((princ,binding)) -> + princ,binding,Tacmach.pf_type_of g princ + in + let princ_infos = Tactics.compute_elim_sig princ_type in + let args_as_induction_constr = + let c_list = + if princ_infos.Tactics.farg_in_concl + then [c] else [] + in + List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) + in + let princ' = Some (princ,bindings) in + let princ_vars = + List.fold_right + (fun a acc -> + try Idset.add (destVar a) acc + with _ -> acc + ) + args + Idset.empty + in + let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in + let old_idl = Idset.diff old_idl princ_vars in + let subst_and_reduce g = + let idl = + map_succeed + (fun id -> + if Idset.mem id old_idl then failwith "subst_and_reduce"; + id + ) + (Tacmach.pf_ids_of_hyps g) + in + let flag = + Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + } + in + if with_clean + then + Tacticals.tclTHEN + (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl ) + (Hiddentac.h_reduce flag Tacticals.allClauses) + g + else Tacticals.tclIDTAC g + + in + Tacticals.tclTHEN + (choose_dest_or_ind + princ_infos + args_as_induction_constr + princ' + pat) + subst_and_reduce + g + + + + type annot = Struct of identifier | Wf of Topconstr.constr_expr * identifier option @@ -122,7 +240,7 @@ let prepare_body (name,annot,args,types,body) rt = let generate_principle do_built fix_rec_l recdefs interactive_proof parametrize - (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) = + (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 fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -133,6 +251,9 @@ let generate_principle if do_built then begin + (*i The next call to mk_rel_id is valid since we have just construct the graph + Ensures by : do_built + i*) let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg @@ -149,7 +270,7 @@ let generate_principle in let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in let _ = - Util.list_map_i + list_map_i (fun i x -> let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in let princ_type = @@ -167,6 +288,7 @@ let generate_principle 0 fix_rec_l in + Array.iter add_Function funs_kn; () end with e -> @@ -210,7 +332,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body if List.length names = 1 then 1 else error "Recursive argument must be specified" | Some wf_arg -> - Util.list_index (Name wf_arg) names + list_index (Name wf_arg) names in let unbounded_eq = let f_app_args = @@ -333,15 +455,15 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = (Topconstr.names_of_local_assums args) in let annot = - try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec + try Some (list_index (Name id) names - 1), Topconstr.CStructRec with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) in (name,annot,args,types,body),(None:Vernacexpr.decl_notation) | (name,None,args,types,body),recdef -> let names = (Topconstr.names_of_local_assums args) in if is_one_rec recdef && List.length names > 1 then - Util.user_err_loc - (Util.dummy_loc,"Function", + user_err_loc + (dummy_loc,"Function", Pp.str "the recursive argument needs to be specified in Function") else (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation) @@ -364,8 +486,23 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = interactive_proof true (Functional_principles_proofs.prove_princ_for_struct interactive_proof); - true - + if register_built + then + begin + try + Invfun.derive_correctness + Functional_principles_types.make_scheme + functional_induction + (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names) + (*i The next call to mk_rel_id is valid since we have just construct the graph + Ensures by : register_built + i*) + (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names) + with e -> + msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e) + end; + true; + in () @@ -397,19 +534,19 @@ 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,Util.option_map (add_args id new_args) b_option, - List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,Util.option_map (add_args id new_args) b_option)) cel, + CCases(loc,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, 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,Util.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,Util.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 ) @@ -426,15 +563,17 @@ let rec add_args id new_args b = -let make_graph (id:identifier) = - let c_body = - try - let c = const_of_id id in - Global.lookup_constant c - with Not_found -> - raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) ) - in +let make_graph (f_ref:global_reference) = + let c,c_body = + match f_ref with + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) + end + | _ -> raise (UserError ("", str "Not a function reference") ) + in match c_body.const_body with | None -> error "Cannot build a graph over an axiom !" | Some b -> @@ -494,7 +633,7 @@ let make_graph (id:identifier) = (fun n (nal,t'') -> n+List.length nal) n nal_ta' in - assert (n'<= n); +(* assert (n'<= n); *) chop_n_arrow (n - n') t' | _ -> anomaly "Not enough products" else t @@ -511,16 +650,6 @@ let make_graph (id:identifier) = let l = List.map (fun (id,(n,recexp),bl,t,b) -> -(* let nal = *) -(* List.flatten *) -(* (List.map *) -(* (function *) -(* | Topconstr.LocalRawDef (na,_)-> [] *) -(* | Topconstr.LocalRawAssum (nal,_) -> nal *) -(* ) *) -(* (nal_tas@bl) *) -(* ) *) -(* in *) let bl' = List.flatten (List.map @@ -539,7 +668,8 @@ let make_graph (id:identifier) = (List.map (function | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal + | Topconstr.LocalRawAssum (nal,_) -> + List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal ) nal_tas ) @@ -551,121 +681,17 @@ let make_graph (id:identifier) = in l | _ -> + let id = id_of_label (con_label c) in [(id,None,nal_tas,t,b)] in -(* List.iter (fun (id,rec_arg,bl,t,b) -> *) -(* Pp.msgnl *) -(* (Ppconstr.pr_id id ++ *) -(* Ppconstr.pr_binders bl ++ *) -(* begin match rec_arg with *) -(* | Some (Struct id) -> str " { struct " ++ Ppconstr.pr_id id ++ str " }" *) -(* | _ -> (mt ()) *) -(* end ++ *) -(* str " : " ++ Ppconstr.pr_lconstr_expr t ++ *) -(* str " := " ++ *) -(* Ppconstr.pr_lconstr_expr b *) -(* ) *) -(* ) *) -(* expr_list; *) - do_generate_principle false false expr_list + do_generate_principle false false expr_list; + (* We register the infos *) + let mp,dp,_ = repr_con c in + List.iter (fun (id,_,_,_,_) -> add_Function (make_con mp dp (label_of_id id))) expr_list + + (* let make_graph _ = assert false *) let do_generate_principle = do_generate_principle true - - -let is_rec_info scheme_info = - let test_branche min acc (_,_,br) = - acc || ( - let new_branche = - Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in - let free_rels_in_br = Termops.free_rels new_branche in - let max = min + scheme_info.Tactics.npredicates in - Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br - ) - in - Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) - - -let choose_dest_or_ind scheme_info = - if is_rec_info scheme_info - then Tactics.new_induct - else Tactics.new_destruct - - -let functional_induction with_clean c princl pat = - let f,args = decompose_app c in - fun g -> - let princ,bindings = - match princl with - | None -> (* No principle is given let's find the good one *) - let fname = - match kind_of_term f with - | Const c' -> - id_of_label (con_label c') - | _ -> Util.error "Must be used with a function" - in - let princ_name = - ( - Indrec.make_elimination_ident - fname - (Tacticals.elimination_sort_of_goal g) - ) - in - mkConst(const_of_id princ_name ),Rawterm.NoBindings - | Some princ -> princ - in - let princ_type = Tacmach.pf_type_of g princ in - let princ_infos = Tactics.compute_elim_sig princ_type in - let args_as_induction_constr = - let c_list = - if princ_infos.Tactics.farg_in_concl - then [c] else [] - in - List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list) - in - let princ' = Some (princ,bindings) in - let princ_vars = - List.fold_right - (fun a acc -> - try Idset.add (destVar a) acc - with _ -> acc - ) - args - Idset.empty - in - let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in - let old_idl = Idset.diff old_idl princ_vars in - let subst_and_reduce g = - let idl = - Util.map_succeed - (fun id -> - if Idset.mem id old_idl then failwith ""; - id - ) - (Tacmach.pf_ids_of_hyps g) - in - let flag = - Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - } - in - if with_clean - then - Tacticals.tclTHEN - (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl ) - (Hiddentac.h_reduce flag Tacticals.allClauses) - g - else Tacticals.tclIDTAC g - - in - Tacticals.tclTHEN - (choose_dest_or_ind - princ_infos - args_as_induction_constr - princ' - pat) - subst_and_reduce - g diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 4eefb3013..71840de9e 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -14,24 +14,6 @@ let msgnl m = let invalid_argument s = raise (Invalid_argument s) -(* let idtbl = Hashtbl.create 29 *) -(* let reset_name () = Hashtbl.clear idtbl *) - -(* let fresh_id s = *) -(* try *) -(* let id = Hashtbl.find idtbl s in *) -(* incr id; *) -(* id_of_string (s^(string_of_int !id)) *) -(* with Not_found -> *) -(* Hashtbl.add idtbl s (ref (-1)); *) -(* id_of_string s *) - -(* let fresh_name s = Name (fresh_id s) *) -(* let get_name ?(default="H") = function *) -(* | Anonymous -> fresh_name default *) -(* | Name n -> Name n *) - - let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid @@ -162,161 +144,301 @@ let find_reference sl s = let eq = lazy(coq_constant "eq") let refl_equal = lazy(coq_constant "refl_equal") +(*****************************************************************) +(* Copy of the standart save mechanism but without the much too *) +(* slow reduction function *) +(*****************************************************************) +open Declarations +open Entries +open Decl_kinds +open Declare +let definition_message id = + Options.if_verbose message ((string_of_id id) ^ " is defined") + + +let save with_clean id const (locality,kind) hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let l,r = match locality with + | Local when Lib.sections_are_opened () -> + let k = logical_kind_of_goal_kind kind in + let c = SectionLocalDef (pft, tpo, opacity) in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local, VarRef id) + | Local -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) + | Global -> + let k = logical_kind_of_goal_kind kind in + let kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) in + if with_clean then Pfedit.delete_current_proof (); + hook l r; + definition_message id + + + + +let extract_pftreestate pts = + let pfterm,subgoals = Refiner.extract_open_pftreestate pts in + let tpfsigma = Refiner.evc_of_pftreestate pts in + let exl = Evarutil.non_instantiated tpfsigma in + if subgoals <> [] or exl <> [] then + Util.errorlabstrm "extract_proof" + (if subgoals <> [] then + str "Attempt to save an incomplete proof" + else + str "Attempt to save a proof with existential variables still non-instantiated"); + let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in + env,tpfsigma,pfterm + + +let nf_betaiotazeta = + let clos_norm_flags flgs env sigma t = + Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags Closure.betaiotazeta + +let nf_betaiota = + let clos_norm_flags flgs env sigma t = + Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in + clos_norm_flags Closure.betaiota + +let cook_proof do_reduce = + let pfs = Pfedit.get_pftreestate () +(* and ident = Pfedit.get_current_proof_name () *) + and (ident,strength,concl,hook) = Pfedit.current_proof_statement () in + let env,sigma,pfterm = extract_pftreestate pfs in + let pfterm = + if do_reduce + then nf_betaiota env sigma pfterm + else pfterm + in + (ident, + ({ const_entry_body = pfterm; + const_entry_type = Some concl; + const_entry_opaque = false; + const_entry_boxed = false}, + strength, hook)) + + +let new_save_named opacity = + let id,(const,persistence,hook) = cook_proof true in + let const = { const with const_entry_opaque = opacity } in + save true id const persistence hook + +let get_proof_clean do_reduce = + let result = cook_proof do_reduce in + Pfedit.delete_current_proof (); + result + + + + +(**********************) + +type function_info = + { + function_constant : constant; + graph_ind : inductive; + equation_lemma : constant option; + correctness_lemma : constant option; + completeness_lemma : constant option; + rect_lemma : constant option; + rec_lemma : constant option; + prop_lemma : constant option; + } + + +type function_db = function_info list + +let function_table = ref ([] : function_db) + + +let rec do_cache_info finfo = function + | [] -> raise Not_found + | (finfo'::finfos as l) -> + if finfo' == finfo then l + else if finfo'.function_constant = finfo.function_constant + then finfo::finfos + else + let res = do_cache_info finfo finfos in + if res == finfos then l else finfo'::l + -(* (\************************************************\) *) -(* (\* Should be removed latter *\) *) -(* (\* Comes from new induction (cf Pierre) *\) *) -(* (\************************************************\) *) - -(* open Sign *) -(* open Term *) - -(* type elim_scheme = *) - -(* (\* { (\\* lists are in reverse order! *\\) *\) *) -(* (\* params: rel_context; (\\* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *\\) *\) *) -(* (\* predicates: rel_context; (\\* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *\\) *\) *) -(* (\* branches: rel_context; (\\* branchr,...,branch1 *\\) *\) *) -(* (\* args: rel_context; (\\* (xni, Ti_ni) ... (x1, Ti_1) *\\) *\) *) -(* (\* indarg: rel_declaration option; (\\* Some (H,I prm1..prmp x1...xni) if present, None otherwise *\\) *\) *) -(* (\* concl: types; (\\* Qi x1...xni HI, some prmis may not be present *\\) *\) *) -(* (\* indarg_in_concl:bool; (\\* true if HI appears at the end of conclusion (dependent scheme) *\\) *\) *) -(* (\* } *\) *) - - - -(* let occur_rel n c = *) -(* let res = not (noccurn n c) in *) -(* res *) - -(* let list_filter_firsts f l = *) -(* let rec list_filter_firsts_aux f acc l = *) -(* match l with *) -(* | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' *) -(* | _ -> acc,l *) -(* in *) -(* list_filter_firsts_aux f [] l *) - -(* let count_rels_from n c = *) -(* let rels = Termops.free_rels c in *) -(* let cpt,rg = ref 0, ref n in *) -(* while Util.Intset.mem !rg rels do *) -(* cpt:= !cpt+1; rg:= !rg+1; *) -(* done; *) -(* !cpt *) - -(* let count_nonfree_rels_from n c = *) -(* let rels = Termops.free_rels c in *) -(* if Util.Intset.exists (fun x -> x >= n) rels then *) -(* let cpt,rg = ref 0, ref n in *) -(* while not (Util.Intset.mem !rg rels) do *) -(* cpt:= !cpt+1; rg:= !rg+1; *) -(* done; *) -(* !cpt *) -(* else raise Not_found *) - -(* (\* cuts a list in two parts, first of size n. Size must be greater than n *\) *) -(* let cut_list n l = *) -(* let rec cut_list_aux acc n l = *) -(* if n<=0 then acc,l *) -(* else match l with *) -(* | [] -> assert false *) -(* | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in *) -(* let res = cut_list_aux [] n l in *) -(* res *) - -(* let exchange_hd_prod subst_hd t = *) -(* let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) *) - -(* let compute_elim_sig elimt = *) -(* (\* conclusion is the final (Qi ...) *\) *) -(* let hyps,conclusion = decompose_prod_assum elimt in *) -(* (\* ccl is conclusion where Qi (that is rel <something>) is replaced *) -(* by a constant (Prop) to avoid it being counted as an arg or *) -(* parameter in the following. *\) *) -(* let ccl = exchange_hd_prod mkProp conclusion in *) -(* (\* indarg is the inductive argument if it exists. If it exists it is *) -(* the last hyp before the conclusion, so it is the first element of *) -(* hyps. To know the first elmt is an inductive arg, we check if the *) -(* it appears in the conclusion (as rel 1). If yes, then it is not *) -(* an inductive arg, otherwise it is. There is a pathological case *) -(* with False_inf where Qi is rel 1, so we first get rid of Qi in *) -(* ccl. *\) *) -(* (\* if last arg of ccl is an application then this a functional ind *) -(* principle *\) let last_arg_ccl = *) -(* try List.hd (List.rev (snd (decompose_app ccl))) *) -(* with Failure "hd" -> mkProp in (\* dummy constr that is not an app *) -(* *\) let hyps',indarg,dep = *) -(* if isApp last_arg_ccl *) -(* then *) -(* hyps,None , false (\* no HI at all *\) *) -(* else *) -(* try *) -(* if noccurn 1 ccl (\* rel 1 does not occur in ccl *\) *) -(* then *) -(* List.tl hyps , Some (List.hd hyps), false (\* it does not *) -(* occur in concl *\) else *) -(* List.tl hyps , Some (List.hd hyps) , true (\* it does occur in concl *\) *) -(* with Failure s -> Util.error "cannot recognise an induction schema" *) -(* in *) - -(* (\* Arguments [xni...x1] must appear in the conclusion, so we count *) -(* successive rels appearing in conclusion **Qi is not considered a *) -(* rel** *\) let nargs = count_rels_from *) -(* (match indarg with *) -(* | None -> 1 *) -(* | Some _ -> 2) ccl in *) -(* let args,hyps'' = cut_list nargs hyps' in *) -(* let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in *) -(* let branches,hyps''' = *) -(* list_filter_firsts (function x -> not (rel_is_pred x)) hyps'' *) -(* in *) -(* (\* Now we want to know which hyps remaining are predicates and which *) -(* are parameters *\) *) -(* (\* We rebuild *) - -(* forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY *) -(* x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^ ^^ *) -(* optional *) -(* opt *) - -(* Free rels appearing in this term are parameters. We catch all of *) -(* them if HI is present. In this case the number of parameters is *) -(* the number of free rels. Otherwise (principle generated by *) -(* functional induction or by hand) WE GUESS that all parameters *) -(* appear in Ti_js, IS THAT TRUE??. *) - -(* TODO: if we want to generalize to the case where arges are merged *) -(* with branches (?) and/or where several predicates are cited in *) -(* the conclusion, we should do something more precise than just *) -(* counting free rels. *) -(* *\) *) -(* let concl_with_indarg = *) -(* match indarg with *) -(* | None -> ccl *) -(* | Some c -> it_mkProd_or_LetIn ccl [c] in *) -(* let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in *) -(* (\* let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *\) *) -(* let nparams = *) -(* try List.length (hyps'''@branches) - count_nonfree_rels_from 1 *) -(* concl_with_args with Not_found -> 0 in *) -(* let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in *) -(* let elimscheme = { *) -(* params = params; *) -(* predicates = preds; *) -(* branches = branches; *) -(* args = args; *) -(* indarg = indarg; *) -(* concl = conclusion; *) -(* indarg_in_concl = dep; *) -(* } *) -(* in *) -(* elimscheme *) - -(* let get_params elimt = *) -(* (compute_elim_sig elimt).params *) -(* (\************************************************\) *) -(* (\* end of Should be removed latter *\) *) -(* (\* Comes from new induction (cf Pierre) *\) *) -(* (\************************************************\) *) +let cache_Function (_,(finfos)) = + let new_tbl = + try do_cache_info finfos !function_table + with Not_found -> finfos::!function_table + in + if new_tbl != !function_table + then function_table := new_tbl + +let load_Function _ = cache_Function +let open_Function _ = cache_Function +let subst_Function (_,subst,finfos) = + let do_subst_con c = fst (Mod_subst.subst_con subst c) + and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i) + 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 + if function_constant' == finfos.function_constant && + graph_ind' == finfos.graph_ind && + equation_lemma' == finfos.equation_lemma && + correctness_lemma' == finfos.correctness_lemma && + completeness_lemma' == finfos.completeness_lemma && + rect_lemma' == finfos.rect_lemma && + rec_lemma' == finfos.rec_lemma && + prop_lemma' == finfos.prop_lemma + then finfos + else + { function_constant = function_constant'; + graph_ind = graph_ind'; + equation_lemma = equation_lemma' ; + correctness_lemma = correctness_lemma' ; + completeness_lemma = completeness_lemma' ; + rect_lemma = rect_lemma' ; + rec_lemma = rec_lemma'; + prop_lemma = prop_lemma'; + } + +let classify_Function (_,infos) = Libobject.Substitute infos + +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 + in + if function_constant' == finfos.function_constant && + graph_ind' == finfos.graph_ind && + equation_lemma' == finfos.equation_lemma && + correctness_lemma' == finfos.correctness_lemma && + completeness_lemma' == finfos.completeness_lemma && + rect_lemma' == finfos.rect_lemma && + rec_lemma' == finfos.rec_lemma && + prop_lemma' == finfos.prop_lemma + then Some finfos + else + Some { function_constant = function_constant' ; + graph_ind = graph_ind' ; + equation_lemma = equation_lemma' ; + correctness_lemma = correctness_lemma' ; + completeness_lemma = completeness_lemma'; + rect_lemma = rect_lemma'; + rec_lemma = rec_lemma'; + prop_lemma = prop_lemma' ; + } + +open Term +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 "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + +let pr_table l = + Util.prlist_with_sep fnl pr_info l + +let in_Function,out_Function = + Libobject.declare_object + {(Libobject.default_object "FUNCTIONS_DB") with + Libobject.cache_function = cache_Function; + Libobject.load_function = load_Function; + Libobject.classify_function = classify_Function; + Libobject.subst_function = subst_Function; + Libobject.export_function = export_Function; + Libobject.discharge_function = discharge_Function +(* Libobject.open_function = open_Function; *) + } + + + +(* Synchronisation with reset *) +let freeze () = + let tbl = !function_table in +(* Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *) + tbl + +let unfreeze l = +(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *) + function_table := + l +let init () = +(* Pp.msgnl (str "reseting function_table"); *) + function_table := [] + +let _ = + Summary.declare_summary "functions_db_sum" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } + +let find_or_none id = + try Some + (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" + ) + with Not_found -> None + + + +let find_Function_infos f = + List.find (fun finfo -> finfo.function_constant = f) !function_table + + +let find_Function_of_graph ind = + List.find (fun finfo -> finfo.graph_ind = ind) !function_table + +let update_Function finfo = +(* Pp.msgnl (pr_info finfo); *) + Lib.add_anonymous_leaf (in_Function finfo) + + +let add_Function f = + let f_id = id_of_label (con_label f) in + let equation_lemma = find_or_none (mk_equation_id f_id) + and correctness_lemma = find_or_none (mk_correct_id f_id) + and completeness_lemma = find_or_none (mk_complete_id f_id) + and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect") + and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec") + and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") + and graph_ind = + match Nametab.locate (make_short_qualid (mk_rel_id f_id)) + with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive" + in + let finfos = + { function_constant = f; + equation_lemma = equation_lemma; + completeness_lemma = completeness_lemma; + correctness_lemma = correctness_lemma; + rect_lemma = rect_lemma; + rec_lemma = rec_lemma; + prop_lemma = prop_lemma; + graph_ind = graph_ind + } + in + update_Function finfos +let pr_table () = pr_table !function_table diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli index 8385eef20..e3e49603f 100644 --- a/contrib/funind/indfun_common.mli +++ b/contrib/funind/indfun_common.mli @@ -1,11 +1,16 @@ open Names open Pp +(* + The mk_?_id function build different name w.r.t. a function + Each of their use is justified in the code +*) val mk_rel_id : identifier -> identifier val mk_correct_id : identifier -> identifier val mk_complete_id : identifier -> identifier val mk_equation_id : identifier -> identifier + val msgnl : std_ppcmds -> unit val invalid_argument : string -> 'a @@ -42,3 +47,56 @@ val refl_equal : Term.constr Lazy.t val const_of_id: identifier -> constant +(* [save_named] is a copy of [Command.save_named] but uses + [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] + + + + DON'T USE IT if you cannot ensure that there is no VMcast in the proof + +*) + +(* val nf_betaiotazeta : Reductionops.reduction_function *) + +val new_save_named : bool -> unit + +val save : bool -> identifier -> Entries.definition_entry -> Decl_kinds.goal_kind -> + Tacexpr.declaration_hook -> unit + +(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and + abort the proof +*) +val get_proof_clean : bool -> + Names.identifier * + (Entries.definition_entry * Decl_kinds.goal_kind * + Tacexpr.declaration_hook) + + + + +(*****************) + +type function_info = + { + function_constant : constant; + graph_ind : inductive; + equation_lemma : constant option; + correctness_lemma : constant option; + completeness_lemma : constant option; + rect_lemma : constant option; + rec_lemma : constant option; + prop_lemma : constant option; + } + +val find_Function_infos : constant -> function_info +val find_Function_of_graph : inductive -> function_info +(* WARNING: To be used just after the graph definition !!! *) +val add_Function : constant -> unit + +val update_Function : function_info -> unit + + +(** debugging *) +val pr_info : function_info -> Pp.std_ppcmds +val pr_table : unit -> Pp.std_ppcmds + diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index cb51069df..f19b4de90 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -37,7 +37,8 @@ let pr_with_bindings prc prlc (c,bl) = let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc c) + | 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 @@ -48,25 +49,9 @@ END TACTIC EXTEND newfuninv - [ "functional" "inversion" ident(hyp) ident(fname) fun_ind_using(princl)] -> + [ "functional" "inversion" ident(hyp) reference(fname) ] -> [ - fun g -> - let fconst = const_of_id fname in - let princ = - match princl with - | None -> - let f_ind_id = - ( - Indrec.make_elimination_ident - fname - (Tacticals.elimination_sort_of_goal g) - ) - in - let princ = const_of_id f_ind_id in - princ - | Some princ -> destConst (fst princ) - in - Invfun.invfun hyp fconst princ g + Invfun.invfun hyp fname ] END @@ -98,7 +83,23 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction true c princl pat ] + 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 @@ -129,7 +130,10 @@ VERNAC ARGUMENT EXTEND rec_definition2 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 + 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", @@ -156,12 +160,15 @@ END VERNAC COMMAND EXTEND Function ["Function" rec_definitions2(recsl)] -> - [ do_generate_principle false recsl] + [ + do_generate_principle false recsl; + + ] END VERNAC ARGUMENT EXTEND fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] END VERNAC ARGUMENT EXTEND fun_scheme_args @@ -173,31 +180,31 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ["Functional" "Scheme" fun_scheme_args(fas) ] -> [ try - Functional_principles_types.make_scheme fas + Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> match fas with | (_,fun_name,_)::_ -> begin - make_graph fun_name; - try Functional_principles_types.make_scheme fas + make_graph (Nametab.global fun_name); + 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.make_case_scheme fas + Functional_principles_types.build_case_scheme fas ] END - +(***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph -["Generate" "graph" "for" ident(c)] -> [ make_graph c ] +["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] END diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 2e5616f0e..a6a4e0d73 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -1,7 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Tacexpr +open Declarations open Util open Names open Term -open Tacinvutils open Pp open Libnames open Tacticals @@ -9,131 +17,919 @@ open Tactics open Indfun_common open Tacmach open Sign +open Hiddentac +(* Some pretty printing function for debugging purpose *) -let tac_pattern l = - (Hiddentac.h_reduce - (Rawterm.Pattern l) - Tacticals.onConcl - ) +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) +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 rec nb_prod x = - let rec count n c = - match kind_of_term c with - Prod(_,_,t) -> count (n+1) t - | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_,_) -> count n c - | _ -> n - in count 0 x -let intro_discr_until n tac : tactic = - let rec intro_discr_until acc : tactic = - fun g -> - if nb_prod (pf_concl g) <= n then tac (List.rev acc) g - else - tclTHEN - intro - (fun g' -> - let id,_,t = pf_last_hyp g' in - tclORELSE - (tclABSTRACT None (Extratactics.h_discrHyp (Rawterm.NamedHyp id))) - (intro_discr_until ((id,t)::acc)) - g' - ) - g +let pr_with_bindings prc prlc (c,bl) = + prc c ++ hv 0 (pr_bindings prc prlc bl) + + + +let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = + pr_with_bindings prc prc (c,bl) + +let pr_elim_scheme el = + let env = Global.env () in + let msg = str "params := " ++ Printer.pr_rel_context env el.params in + let env = Environ.push_rel_context el.params env in + let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in + let env = Environ.push_rel_context el.predicates env in + let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in + let env = Environ.push_rel_context el.branches env in + let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in + let env = Environ.push_rel_context el.args env in + let msg = + Util.option_fold_right + (fun o msg -> msg ++ fnl () ++ str "indarg := " ++ Printer.pr_rel_context env [o]) + el.indarg + msg + in + let env = Util.option_fold_right (fun o env -> Environ.push_rel_context [o] env) el.indarg env in + msg ++ fnl () ++ str "concl := " ++ Printer.pr_lconstr_env env el.concl + +(* The local debuging mechanism *) +let msgnl = Pp.msgnl + +let do_observe () = + Tacinterp.get_debug () <> Tactic_debug.DebugOff + + +let observe strm = + if do_observe () + then Pp.msgnl strm + else () + +let observennl strm = + if do_observe () + then begin Pp.msg strm;Pp.pp_flush () end + else () + + +let do_observe_tac s tac g = + try let 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 observe_tac s tac g = + if do_observe () + then do_observe_tac (str s) tac g + else tac g + +(* [nf_zeta] $\zeta$-normalization of a term *) +let nf_zeta = + Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Environ.empty_env + Evd.empty + + +(* [id_to_constr id] finds the term associated to [id] in the global environment *) +let id_to_constr id = + try + Tacinterp.constr_of_id (Global.env ()) id + with Not_found -> + raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id)) + +(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] + (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. + + [generate_type true f i] returns + \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, + graph\ x_1\ldots x_n\ res \rightarrow res = fv \] decomposed as the context and the conclusion + + [generate_type false f i] returns + \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, + res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion + *) + +let generate_type g_to_f f graph i = + (*i we deduce the number of arguments of the function and its returned type from the graph i*) + let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph)) in + let ctxt,_ = decompose_prod_assum graph_arity in + let fun_ctxt,res_type = + match ctxt with + | [] | [_] -> anomaly "Not a valid context" + | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type in - intro_discr_until [] - - -let rec discr_rew_in_H hypname idl : tactic = - match idl with - | [] -> (Extratactics.h_discrHyp (Rawterm.NamedHyp hypname)) - | ((id,t)::idl') -> - match kind_of_term t with - | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) -> - begin - let constr,_ = decompose_app arg1 in - if isConstruct constr - then - (discr_rew_in_H hypname idl') - else - tclTHEN - (tclTRY (Equality.general_rewrite_in true hypname (mkVar id))) - (discr_rew_in_H hypname idl') - end - | _ -> discr_rew_in_H hypname idl' - -let finalize fname hypname idl : tactic = - tclTRY ( - (tclTHEN - (Hiddentac.h_reduce - (Rawterm.Unfold [[],EvalConstRef fname]) - (Tacticals.onHyp hypname) - ) - (discr_rew_in_H hypname idl) - )) + let nb_args = List.length fun_ctxt in + let args_from_decl i decl = + match decl with + | (_,Some _,_) -> incr i; failwith "args_from_decl" + | _ -> let j = !i in incr i;mkRel (nb_args - j + 1) + in + (*i We need to name the vars [res] and [fv] i*) + let res_id = + Termops.next_global_ident_away + true + (id_of_string "res") + (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt) + in + let fv_id = + Termops.next_global_ident_away + true + (id_of_string "fv") + (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt)) + in + (*i we can then type the argument to be applied to the function [f] i*) + let args_as_rels = + let i = ref 0 in + Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt))) + in + let args_as_rels = Array.map Termops.pop args_as_rels in + (*i + the hypothesis [res = fv] can then be computed + We will need to lift it by one in order to use it as a conclusion + i*) + let res_eq_f_of_args = + mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|]) + in + (*i + The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed + We will need to lift it by one in order to use it as a conclusion + i*) + let graph_applied = + let args_and_res_as_rels = + let i = ref 0 in + Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) ) + in + let args_and_res_as_rels = + Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels + in + mkApp(graph,args_and_res_as_rels) + in + (*i The [pre_context] is the defined to be the context corresponding to + \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] + i*) + let pre_ctxt = + (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(mkConst f,args_as_rels)),res_type)::fun_ctxt + in + (*i and we can return the solution depending on which lemma type we are defining i*) + if g_to_f + then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args) + else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied) -let gen_fargs fargs : tactic = - fun g -> - generalize - (List.map - (fun arg -> - let targ = pf_type_of g arg in - let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in - refl_arg - ) - (Array.to_list fargs) - ) - g - -let invfun (hypname:identifier) fname princ : tactic= - fun g -> - let nprod_goal = nb_prod (pf_concl g) in - let princ_info = - let princ_type = - (try (match (Global.lookup_constant princ) with - {Declarations.const_type=t} -> t - ) - with _ -> assert false) +(* + [find_induction_principle f] searches and returns the [body] and the [type] of [f_rect] + + WARNING: while convertible, [type_of body] and [type] can be non equal +*) +let find_induction_principle f = + let f_as_constant = match kind_of_term f with + | Const c' -> c' + | _ -> error "Must be used with a function" + in + let infos = find_Function_infos f_as_constant in + match infos.rect_lemma with + | None -> raise Not_found + | Some rect_lemma -> + let rect_lemma = mkConst rect_lemma in + let typ = Typing.type_of (Global.env ()) Evd.empty rect_lemma in + rect_lemma,typ + + + +(* let fname = *) +(* match kind_of_term f with *) +(* | Const c' -> *) +(* id_of_label (con_label c') *) +(* | _ -> error "Must be used with a function" *) +(* in *) + +(* let princ_name = *) +(* ( *) +(* Indrec.make_elimination_ident *) +(* fname *) +(* InType *) +(* ) *) +(* in *) +(* let c = (\* mkConst(mk_from_const (destConst f) princ_name ) in *\) failwith "" in *) +(* c,Typing.type_of (Global.env ()) Evd.empty c *) + + +let rec generate_fresh_id x avoid i = + if i == 0 + then [] + else + let id = Termops.next_global_ident_away true x avoid in + id::(generate_fresh_id x (id::avoid) (pred i)) + + +(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] + is the tactic used to prove correctness lemma. + + [functional_induction] is the tactic defined in [indfun] (dependency problem) + [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions + (resp. graphs of the functions and principles and correctness lemma types) to prove correct. + + [i] is the indice of the function to prove correct + + The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is + it looks like~: + [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, + res = f x_1\ldots x_n in, \rightarrow graph\ x_1\ldots x_n\ res] + + + The sketch of the proof is the following one~: + \begin{enumerate} + \item intros until $x_n$ + \item $functional\ induction\ (f.(i)\ x_1\ldots x_n)$ using schemes.(i) + \item for each generated branch intro [res] and [hres :res = f x_1\ldots x_n], rewrite [hres] and the + apply the corresponding constructor of the corresponding graph inductive. + \end{enumerate} + +*) +let prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = + fun g -> + (* first of all we recreate the lemmas types to be used as predicates of the induction principle + that is~: + \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\] + *) + let lemmas = + Array.map + (fun (_,(ctxt,concl)) -> + match ctxt with + | [] | [_] | [_;_] -> anomaly "bad context" + | hres::res::(x,_,t)::ctxt -> + Termops.it_mkLambda_or_LetIn + ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res]) + ((x,None,t)::ctxt) + ) + lemmas_types_infos + in + (* we the get the definition of the graphs block *) + let graph_ind = destInd graphs_constr.(i) in + let kn = fst graph_ind in + let mib,_ = Global.lookup_inductive graph_ind in + (* and the principle to use in this lemma in $\zeta$ normal form *) + let f_principle,princ_type = schemes.(i) in + let princ_type = nf_zeta princ_type in + let princ_infos = Tactics.compute_elim_sig princ_type in + (* The number of args of the function is then easilly computable *) + let nb_fun_args = nb_prod (pf_concl g) - 2 in + let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in + let ids = args_names@(pf_ids_of_hyps g) in + (* Since we cannot ensure that the funcitonnal principle is defined in the + environement and due to the bug #1174, we will need to pose the principle + using a name + *) + let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in + let ids = principle_id :: ids in + (* We get the branches of the principle *) + let branches = List.rev princ_infos.branches in + (* and built the intro pattern for each of them *) + let intro_pats = + List.map + (fun (_,_,br_type) -> + List.map + (fun id -> Genarg.IntroIdentifier id) + (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + ) + branches + in + (* before building the full intro pattern for the principle *) + let pat = Genarg.IntroOrAndPattern intro_pats in + let eq_ind = Coqlib.build_coq_eq () in + let eq_construct = mkConstruct((destInd eq_ind),1) in + (* The next to referencies will be used to find out which constructor to apply in each branch *) + let ind_number = ref 0 + and min_constr_number = ref 0 in + (* The tactic to prove the ith branch of the principle *) + let prove_branche i g = + (* We get the identifiers of this branch *) + let this_branche_ids = + List.fold_right + (fun pat acc -> + match pat with + | Genarg.IntroIdentifier id -> Idset.add id acc + | _ -> anomaly "Not an identifier" + ) + (List.nth intro_pats (pred i)) + Idset.empty + in + (* and get the real args of the branch by unfolding the defined constant *) + let pre_args,pre_tac = + List.fold_right + (fun (id,b,t) (pre_args,pre_tac) -> + if Idset.mem id this_branche_ids + then + match b with + | None -> (id::pre_args,pre_tac) + | Some b -> + (pre_args, + tclTHEN (h_reduce (Rawterm.Unfold([[],EvalVarRef id])) allHyps) pre_tac + ) + + else (pre_args,pre_tac) + ) + (pf_hyps g) + ([],tclIDTAC) + in + (* + We can then recompute the arguments of the constructor. + For each [hid] introduced by this branch, if [hid] has type + $forall res, res=fv -> graph.(j)\ x_1\ x_n res$ the corresponding arguments of the constructor are + [ fv (hid fv (refl_equal fv)) ]. + + If [hid] has another type the corresponding argument of the constructor is [hid] + *) + let constructor_args = + List.fold_right + (fun hid acc -> + let type_of_hid = pf_type_of g (mkVar hid) in + match kind_of_term type_of_hid with + | Prod(_,_,t') -> + begin + match kind_of_term t' with + | Prod(_,t'',t''') -> + begin + match kind_of_term t'',kind_of_term t''' with + | App(eq,args), App(graph',_) + when + (eq_constr eq eq_ind) && + array_exists (eq_constr graph') graphs_constr -> + ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) + ::args.(2)::acc) + | _ -> mkVar hid :: acc + end + | _ -> mkVar hid :: acc + end + | _ -> mkVar hid :: acc + ) pre_args [] + in + (* in fact we must also add the parameters to the constructor args *) + let constructor_args = + let params_id = fst (list_chop princ_infos.nparams args_names) in + (List.map mkVar params_id)@(List.rev constructor_args) + in + (* We then get the constructor corresponding to this branch and + modifies the references has needed i.e. + if the constructor is the last one of the current inductive then + add one the number of the inductive to take and add the number of constructor of the previous + graph to the minimal constructor number + *) + let constructor = + let constructor_num = i - !min_constr_number in + let length = Array.length (mib.Declarations.mind_packets.(!ind_number).Declarations.mind_consnames) in + if constructor_num <= length + then + begin + (kn,!ind_number),constructor_num + end + else + begin + incr ind_number; + min_constr_number := !min_constr_number + length ; + (kn,!ind_number),1 + end in - Tactics.compute_elim_sig princ_type + (* we can then build the final proof term *) + let app_constructor = applist((mkConstruct(constructor)),constructor_args) in + (* an apply the tactic *) + let res,hres = + match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with + | [res;hres] -> res,hres + | _ -> assert false + in + observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); + ( + tclTHENSEQ + [ + (* unfolding of all the defined variables introduced by this branch *) + observe_tac "unfolding" pre_tac; + (* $zeta$ normalizing of the conclusion *) + h_reduce + (Rawterm.Cbv + { Rawterm.all_flags with + Rawterm.rDelta = false ; + Rawterm.rConst = [] + } + ) + onConcl; + (* introducing the the result of the graph and the equality hypothesis *) + observe_tac "introducing" (tclMAP h_intro [res;hres]); + (* replacing [res] with its value *) + observe_tac "rewriting res value" (Equality.rewriteLR (mkVar hres)); + (* Conclusion *) + observe_tac "exact" (h_exact app_constructor) + ] + ) + g in - let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in - let do_invert fargs appf : tactic = - let frealargs = (snd (array_chop (List.length princ_info.params) fargs)) + (* end of branche proof *) + let param_names = fst (list_chop princ_infos.nparams args_names) in + let params = List.map mkVar param_names in + let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in + (* The bindings of the principle + that is the params of the principle and the different lemma types + *) + let bindings = + let params_bindings,avoid = + List.fold_left2 + (fun (bindings,avoid) (x,_,_) p -> + let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in + (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + ) + ([],[]) + princ_infos.params + (List.rev params) in - let pat_args = - (List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf] + let lemmas_bindings = + List.rev (fst (List.fold_left2 + (fun (bindings,avoid) (x,_,_) p -> + let id = Termops.next_global_ident_away false (Nameops.out_name x) avoid in + (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid) + ([],avoid) + princ_infos.predicates + (lemmas))) in - tclTHENSEQ - [ - gen_fargs frealargs; - tac_pattern pat_args; - Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings); - intro_discr_until nprod_goal (finalize fname hypname) - + Rawterm.ExplicitBindings (params_bindings@lemmas_bindings) + in + tclTHENSEQ + [ observe_tac "intro args_names" (tclMAP h_intro args_names); + observe_tac "principle" (forward + (Some (h_exact f_principle)) + (Genarg.IntroIdentifier principle_id) + princ_type); + tclTHEN_i + (observe_tac "functional_induction" ( + fun g -> + observe + (str "princ" ++ pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); + functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) + (Some (mkVar principle_id,bindings)) + pat g + )) + (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) + ] + g + +(* [generalize_depedent_of x hyp g] + generalize every hypothesis which depends of [x] but [hyp] +*) +let generalize_depedent_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] + | _ -> tclIDTAC + ) + (pf_hyps g) + g + +(* [prove_fun_complete funs graphs schemes lemmas_types_infos i] + is the tactic used to prove completness lemma. + + [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions + (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. + + [i] is the indice of the function to prove complete + + The lemma to prove if suppose to have been generated by [generate_type] (in $\zeta$ normal form that is + it looks like~: + [\forall (x_1:t_1)\ldots(x_n:t_n), forall res, + graph\ x_1\ldots x_n\ res, \rightarrow res = f x_1\ldots x_n in] + + + The sketch of the proof is the following one~: + \begin{enumerate} + \item intros until $H:graph\ x_1\ldots x_n\ res$ + \item $elim\ H$ using schemes.(i) + \item for each generated branch, intro the news hyptohesis, for each such hyptohesis [h], if [h] has + type [x=?] with [x] a variable, then subst [x], + if [h] has type [t=?] with [t] not a variable then rewrite [t] in the subterms, else + if [h] is a match then destruct it, else do just introduce it, + after all intros, the conclusion should be a reflexive equality. + \end{enumerate} + +*) + + +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = + fun g -> + (* We compute the types of the different mutually recursive lemmas + in $\zeta$ normal form + *) + let lemmas = + Array.map + (fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt)) + lemmas_types_infos + in + (* We get the constant and the principle corresponding to this lemma *) + let f = funcs.(i) in + let graph_principle = nf_zeta schemes.(i) in + let princ_type = pf_type_of g graph_principle in + let princ_infos = Tactics.compute_elim_sig princ_type in + (* Then we get the number of argument of the function + and compute a fresh name for each of them + *) + let nb_fun_args = nb_prod (pf_concl g) - 2 in + let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in + let ids = args_names@(pf_ids_of_hyps g) in + (* and fresh names for res H and the principle (cf bug bug #1174) *) + let res,hres,graph_principle_id = + match generate_fresh_id (id_of_string "z") ids 3 with + | [res;hres;graph_principle_id] -> res,hres,graph_principle_id + | _ -> assert false + in + let ids = res::hres::graph_principle_id::ids in + (* we also compute fresh names for each hyptohesis of each branche of the principle *) + let branches = List.rev princ_infos.branches in + let intro_pats = + List.map + (fun (_,_,br_type) -> + List.map + (fun id -> id) + (generate_fresh_id (id_of_string "y") ids (nb_prod br_type)) + ) + branches + in + let eq_ind = Coqlib.build_coq_eq () in + (* We will need to change the function by its body + using [f_equation] if it is recursive (that is the graph is infinite + or unfold if the graph is finite + *) + let rewrite_tac j ids : tactic = + let graph_def = graphs.(j) in + if Rtree.is_infinite graph_def.mind_recargs + then + let eq_lemma = + try out_some (find_Function_infos (destConst funcs.(j))).equation_lemma + with Failure "out_some" | Not_found -> anomaly "Cannot find equation lemma" + in + tclTHENSEQ[ + tclMAP h_intro ids; + Equality.rewriteLR (mkConst eq_lemma); + h_generalize (List.map mkVar ids); + thin ids ] + else unfold_in_concl [([],Names.EvalConstRef (destConst f))] + in + (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis + (unfolding, substituting, destructing cases \ldots) + *) + let rec intros_with_rewrite_aux : tactic = + fun g -> + match kind_of_term (pf_concl g) with + | Prod(_,t,t') -> + begin + match kind_of_term t with + | App(eq,args) when (eq_constr eq eq_ind) -> + 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; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] + g + else + begin + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ[ + h_intro id; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] g + end + | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> + Tauto.tauto g + | Case(_,_,v,_) -> + tclTHENSEQ[ + h_case (v,Rawterm.NoBindings); + intros_with_rewrite + ] g + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id;intros_with_rewrite] g + end + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> tclIDTAC g + and intros_with_rewrite g = + observe_tac "intros_with_rewrite" intros_with_rewrite_aux g + in + (* The proof of each branche itself *) + let ind_number = ref 0 in + let min_constr_number = ref 0 in + let prove_branche i g = + (* we fist compute the inductive corresponding to the branch *) + let this_ind_number = + let constructor_num = i - !min_constr_number in + let length = Array.length (graphs.(!ind_number).Declarations.mind_consnames) in + if constructor_num <= length + then !ind_number + else + begin + incr ind_number; + min_constr_number := !min_constr_number + length; + !ind_number + end + in + let this_branche_ids = List.nth intro_pats (pred i) in + tclTHENSEQ[ + (* 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); + (* The proof is complete *) + observe_tac "reflexivity" (reflexivity) + ] + g in - match kind_of_term typhyp with - | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) -> -(* let valf = def_of_const (mkConst fname) in *) - let eq_arg1 , eq_arg2 , good_eq_form , fargs = - match kind_of_term arg1 , kind_of_term arg2 with - | App(f, args),_ when eq_constr f (mkConst fname) -> - arg1 , arg2 , tclIDTAC , args - | _,App(f, args) when eq_constr f (mkConst fname) -> - arg2 , arg1 , symmetry_in hypname , args - | _ , _ -> error "inversion impossible" - in - tclTHEN - good_eq_form - (do_invert fargs eq_arg1) - g - | App(f',fargs) when eq_constr f' (mkConst fname) -> - do_invert fargs typhyp g - - - | _ -> error "inversion impossible" + let params_names = fst (list_chop princ_infos.nparams args_names) in + let params = List.map mkVar params_names in + tclTHENSEQ + [ tclMAP h_intro (args_names@[res;hres]); + observe_tac "h_generalize" + (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))))) + (fun i g -> prove_branche i g )) + ] + g + + + +let do_save () = Command.save_named false + + +(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness + lemmas for each function in [funs] w.r.t. [graphs] + + [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and + [functional_induction] is Indfun.functional_induction (same pb) +*) + +let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = + let funs = Array.of_list funs and graphs = Array.of_list graphs in + let funs_constr = Array.map mkConst funs in + try + let graphs_constr = Array.map mkInd graphs in + let lemmas_types_infos = + Util.array_map2_i + (fun i f_constr graph -> + let const_of_f = destConst f_constr in + let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = + generate_type false const_of_f graph i + in + let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in + let type_of_lemma = nf_zeta type_of_lemma in + observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); + type_of_lemma,type_info + ) + funs_constr + graphs_constr + in + let schemes = + (* The functional induction schemes are computed and not saved if there is more that one function + if the block contains only one function we can safely reuse [f_rect] + *) + try + if Array.length funs_constr <> 1 then raise Not_found; + [| find_induction_principle funs_constr.(0) |] + with Not_found -> + Array.of_list + (List.map + (fun entry -> + (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type ) + ) + (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) + ) + in + let proving_tac = + prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos + in + Array.iteri + (fun i f_as_constant -> + let f_id = id_of_label (con_label f_as_constant) in + Command.start_proof + (*i The next call to mk_correct_id is valid since we are constructing the lemma + Ensures by: obvious + i*) + (mk_correct_id f_id) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) + (fst lemmas_types_infos.(i)) + (fun _ _ -> ()); + Pfedit.by (observe_tac ("procve correctness ("^(string_of_id f_id)^")") (proving_tac i)); + do_save (); + let finfo = find_Function_infos f_as_constant in + update_Function + {finfo with + correctness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_correct_id f_id))) + } + + ) + funs; + let lemmas_types_infos = + Util.array_map2_i + (fun i f_constr graph -> + let const_of_f = destConst f_constr in + let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = + generate_type true const_of_f graph i + in + let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in + let type_of_lemma = nf_zeta type_of_lemma in + observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma); + type_of_lemma,type_info + ) + funs_constr + graphs_constr + in + let kn,_ as graph_ind = destInd graphs_constr.(0) in + let mib,mip = Global.lookup_inductive graph_ind in + let schemes = + Array.of_list + (Indrec.build_mutual_indrec (Global.env ()) Evd.empty + (Array.to_list + (Array.mapi + (fun i mip -> (kn,i),mib,mip,true,InType) + mib.Declarations.mind_packets + ) + ) + ) + in + let proving_tac = + prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos + in + Array.iteri + (fun i f_as_constant -> + let f_id = id_of_label (con_label f_as_constant) in + Command.start_proof + (*i The next call to mk_complete_id is valid since we are constructing the lemma + Ensures by: obvious + i*) + (mk_complete_id f_id) + (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) + (fst lemmas_types_infos.(i)) + (fun _ _ -> ()); + Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); + do_save (); + let finfo = find_Function_infos f_as_constant in + update_Function + {finfo with + completeness_lemma = Some (destConst (Tacinterp.constr_of_id (Global.env ())(mk_complete_id f_id))) + } + ) + funs; + with e -> + (* In case of problem, we reset all the lemmas *) + (*i The next call to mk_correct_id is valid since we are erasing the lemmas + Ensures by: obvious + i*) + let first_lemma_id = + let f_id = id_of_label (con_label funs.(0)) in + + mk_correct_id f_id + in + ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); + raise e + + + + + +(***********************************************) + +(* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res + when [kn] denotes a graph block into + f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result + + if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing +*) +let revert_graph kn post_tac hid g = + let typ = pf_type_of g (mkVar hid) in + match kind_of_term typ with + | App(i,args) when isInd i -> + let ((kn',num) as ind') = destInd i in + if kn = kn' + then (* We have generated a graph hypothesis so that we must change it if we can *) + let info = + try find_Function_of_graph ind' + with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) + anomaly "Cannot retrieve infos about a mutual block" + in + (* if we can find a completeness lemma for this function + then we can come back to the functional form. If not, we do nothing + *) + match info.completeness_lemma with + | None -> tclIDTAC g + | Some f_complete -> + let f_args,res = array_chop (Array.length args - 1) args in + tclTHENSEQ + [ + h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + thin [hid]; + h_intro hid; + post_tac hid + ] + g + + else tclIDTAC g + | _ -> tclIDTAC g + + +(* + [functional_inversion hid fconst f_correct ] is the functional version of [inversion] + + [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] + is the correctness lemma for [fconst]. + + The sketch is the follwing~: + \begin{enumerate} + \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ + (fails if it is not possible) + \item replace [hid] with $R\_f t_1 \ldots t_n res$ using [f_correct] + \item apply [inversion] on [hid] + \item finally in each branch, replace each hypothesis [R\_f ..] by [f ...] using [f_complete] (whenever + such a lemma exists) + \end{enumerate} +*) + +let functional_inversion kn hid fconst f_correct : tactic = + fun g -> + let old_ids = List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty in + let type_of_h = pf_type_of g (mkVar hid) in + match kind_of_term type_of_h with + | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> + let pre_tac,f_args,res = + match kind_of_term args.(1),kind_of_term args.(2) with + | App(f,f_args),_ when eq_constr f fconst -> + ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2)) + |_,App(f,f_args) when eq_constr f fconst -> + ((fun hid -> tclIDTAC),f_args,args.(1)) + | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) + in + tclTHENSEQ[ + pre_tac hid; + h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + thin [hid]; + h_intro hid; + Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid); + (fun g -> + let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in + tclMAP (revert_graph kn pre_tac) (hid::new_ids) g + ); + ] g + | _ -> tclFAIL 1 (mt ()) g + + + +let invfun hid f gl = + let f = + match f with + | ConstRef f -> f + | _ -> raise (Util.UserError("",str "Not a function")) + in + try + let finfos = find_Function_infos f in + let f_correct = mkConst(out_some finfos.correctness_lemma) + and kn = fst finfos.graph_ind + in + functional_inversion kn hid (mkConst f) f_correct gl + with + | Not_found -> error "No graph found" + | Failure "out_some" -> error "Cannot use equivalence with graph!" diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 66ee42bb4..1efd14d4a 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -722,6 +722,10 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = args new_crossed_types (depth + 1) b in + (*i The next call to mk_rel_id is valid since we are constructing the graph + Ensures by: obvious + i*) + let new_t = mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt]) in mkRProd(n,new_t,new_b), @@ -920,6 +924,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo let returned_types = Array.of_list returned_types in let rtl_alpha = List.map (function rt -> (alpha_rt [] rt) ) rtl in let rta = Array.of_list rtl_alpha in + (*i The next call to mk_rel_id is valid since we are constructing the graph + Ensures by: obvious + i*) let relnames = Array.map mk_rel_id funnames in let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in let resa = Array.map (build_entry_lc funnames_as_set []) rta in @@ -941,6 +948,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo let next_constructor_id = ref (-1) in let mk_constructor_id i = incr next_constructor_id; + (*i The next call to mk_rel_id is valid since we are constructing the graph + Ensures by: obvious + i*) id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) in let rel_constructors i rt : (identifier*rawconstr) list = @@ -1003,9 +1013,9 @@ let build_inductive parametrize funnames (funsargs: (Names.name * rawconstr * bo let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t) + false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty ((* zeta_normalize *) t)) )) - rel_constructors + (rel_constructors) in let rel_ind i ext_rel_constructors = (dummy_loc,relnames.(i)), diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index c6406468a..96b0e1eb7 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -539,3 +539,63 @@ let ids_of_pat = in ids_of_pat Idset.empty + + + + +let zeta_normalize = + let rec zeta_normalize_term rt = + match rt with + | RRef _ -> rt + | RVar _ -> rt + | REvar _ -> rt + | RPatVar _ -> rt + | RApp(loc,rt',rtl) -> + RApp(loc, + zeta_normalize_term rt', + List.map zeta_normalize_term rtl + ) + | RLambda(loc,name,t,b) -> + RLambda(loc, + name, + zeta_normalize_term t, + zeta_normalize_term b + ) + | RProd(loc,name,t,b) -> + RProd(loc, + name, + zeta_normalize_term t, + zeta_normalize_term b + ) + | RLetIn(_,Name id,def,b) -> + zeta_normalize_term (replace_var_by_term id def b) + | RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | RLetTuple(loc,nal,(na,rto),def,b) -> + RLetTuple(loc, + nal, + (na,option_map zeta_normalize_term rto), + zeta_normalize_term def, + zeta_normalize_term b + ) + | RCases(loc,infos,el,brl) -> + RCases(loc, + 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), + zeta_normalize_term lhs, + zeta_normalize_term rhs + ) + | RRec _ -> raise (UserError("",str "Not handled RRec")) + | RSort _ -> rt + | RHole _ -> rt + | RCast(loc,b,k,t) -> + RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t) + | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) + and zeta_normalize_br (loc,idl,patl,res) = + (loc,idl,patl,zeta_normalize_term res) + in + zeta_normalize_term diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index 5dcdb15c5..4df239e32 100644 --- a/contrib/funind/rawtermops.mli +++ b/contrib/funind/rawtermops.mli @@ -106,3 +106,9 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool returns the set of variables appearing in a pattern *) val ids_of_pat : cases_pattern -> Names.Idset.t + + +(* + removing let_in construction in a rawterm +*) +val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr |