diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f9938c0356..e34323abf4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -129,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const ?hook (locality,_,kind) = +let save with_clean id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) = (locality, ConstRef kn) in if with_clean then Proof_global.discard_current (); - Lemmas.call_hook ?hook ~fix_exn l r; + Lemmas.call_hook ?hook ~fix_exn uctx [] l r; definition_message id let with_full_print f a = @@ -199,6 +199,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -249,6 +250,7 @@ let subst_Function (subst,finfos) = let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in + let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -256,7 +258,8 @@ let subst_Function (subst,finfos) = completeness_lemma' == finfos.completeness_lemma && rect_lemma' == finfos.rect_lemma && rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma + prop_lemma' == finfos.prop_lemma && + sprop_lemma' == finfos.sprop_lemma then finfos else { function_constant = function_constant'; @@ -267,17 +270,16 @@ let subst_Function (subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + sprop_lemma = sprop_lemma'; is_general = finfos.is_general } let discharge_Function (_,finfos) = Some finfos -let pr_ocst c = - let sigma, env = Pfedit.get_current_context () in +let pr_ocst env sigma c = Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) -let pr_info f_info = - let sigma, env = Pfedit.get_current_context () in +let pr_info env sigma f_info = str "function_constant := " ++ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ @@ -285,17 +287,17 @@ let pr_info f_info = Printer.pr_lconstr_env env sigma (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ - str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ - str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ - str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ - str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ - str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ - str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ + str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++ + str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++ + str "correctness_lemma := " ++ pr_ocst env sigma f_info.correctness_lemma ++ fnl () ++ + str "rect_lemma := " ++ pr_ocst env sigma f_info.rect_lemma ++ fnl () ++ + str "rec_lemma := " ++ pr_ocst env sigma f_info.rec_lemma ++ fnl () ++ + str "prop_lemma := " ++ pr_ocst env sigma f_info.prop_lemma ++ fnl () ++ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () -let pr_table tb = +let pr_table env sigma tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in - Pp.prlist_with_sep fnl pr_info l + Pp.prlist_with_sep fnl (pr_info env sigma) l let in_Function : function_info -> Libobject.obj = let open Libobject in @@ -333,6 +335,7 @@ let add_Function is_general f = 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 sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") @@ -345,6 +348,7 @@ let add_Function is_general f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; + sprop_lemma = sprop_lemma; graph_ind = graph_ind; is_general = is_general @@ -352,7 +356,7 @@ let add_Function is_general f = in update_Function finfos -let pr_table () = pr_table !from_function +let pr_table env sigma = pr_table env sigma !from_function (*********************************) (* Debuging *) let functional_induction_rewrite_dependent_proofs = ref true |