diff options
Diffstat (limited to 'contrib/funind/indfun_common.ml')
| -rw-r--r-- | contrib/funind/indfun_common.ml | 80 |
1 files changed, 61 insertions, 19 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index f41aac20..13b242d5 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -5,8 +5,8 @@ open Libnames let mk_prefix pre id = id_of_string (pre^(string_of_id id)) let mk_rel_id = mk_prefix "R_" -let mk_correct_id id = Nameops.add_suffix id "_correct" -let mk_complete_id id = Nameops.add_suffix id "_complete" +let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct" +let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete" let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = @@ -233,6 +233,32 @@ let get_proof_clean do_reduce = Pfedit.delete_current_proof (); result +let with_full_print f a = + let old_implicit_args = Impargs.is_implicit_args () + and old_strict_implicit_args = Impargs.is_strict_implicit_args () + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in + let old_rawprint = !Options.raw_print in + Options.raw_print := true; + Impargs.make_implicit_args false; + Impargs.make_strict_implicit_args false; + Impargs.make_contextual_implicit_args false; + try + let res = f a in + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Options.raw_print := old_rawprint; + res + with + | e -> + Impargs.make_implicit_args old_implicit_args; + Impargs.make_strict_implicit_args old_strict_implicit_args; + Impargs.make_contextual_implicit_args old_contextual_implicit_args; + Options.raw_print := old_rawprint; + raise e + + + @@ -248,14 +274,18 @@ type function_info = rect_lemma : constant option; rec_lemma : constant option; prop_lemma : constant option; + is_general : bool; (* Has this function been defined using general recursive definition *) } -type function_db = function_info list +(* type function_db = function_info list *) + +(* let function_table = ref ([] : function_db) *) -let function_table = ref ([] : function_db) - +let from_function = ref Cmap.empty +let from_graph = ref Indmap.empty +(* let rec do_cache_info finfo = function | [] -> raise Not_found | (finfo'::finfos as l) -> @@ -274,6 +304,12 @@ let cache_Function (_,(finfos)) = in if new_tbl != !function_table then function_table := new_tbl +*) + +let cache_Function (_,finfos) = + from_function := Cmap.add finfos.function_constant finfos !from_function; + from_graph := Indmap.add finfos.graph_ind finfos !from_graph + let load_Function _ = cache_Function let open_Function _ = cache_Function @@ -307,6 +343,7 @@ let subst_Function (_,subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + is_general = finfos.is_general } let classify_Function (_,infos) = Libobject.Substitute infos @@ -342,6 +379,7 @@ let discharge_Function (_,finfos) = rect_lemma = rect_lemma'; rec_lemma = rec_lemma'; prop_lemma = prop_lemma' ; + is_general = finfos.is_general } open Term @@ -357,7 +395,8 @@ let pr_info f_info = 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 = +let pr_table tb = + let l = Cmap.fold (fun k v acc -> v::acc) tb [] in Util.prlist_with_sep fnl pr_info l let in_Function,out_Function = @@ -376,17 +415,16 @@ let in_Function,out_Function = (* Synchronisation with reset *) let freeze () = - let tbl = !function_table in -(* Pp.msgnl (str "freezing function_table : " ++ pr_table tbl); *) - tbl - -let unfreeze l = + !from_function,!from_graph +let unfreeze (functions,graphs) = (* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *) - function_table := - l + from_function := functions; + from_graph := graphs + let init () = (* Pp.msgnl (str "reseting function_table"); *) - function_table := [] + from_function := Cmap.empty; + from_graph := Indmap.empty let _ = Summary.declare_summary "functions_db_sum" @@ -405,18 +443,18 @@ let find_or_none id = let find_Function_infos f = - List.find (fun finfo -> finfo.function_constant = f) !function_table + Cmap.find f !from_function let find_Function_of_graph ind = - List.find (fun finfo -> finfo.graph_ind = ind) !function_table + Indmap.find ind !from_graph let update_Function finfo = (* Pp.msgnl (pr_info finfo); *) Lib.add_anonymous_leaf (in_Function finfo) -let add_Function f = +let add_Function is_general 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) @@ -436,12 +474,14 @@ let add_Function f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; - graph_ind = graph_ind + graph_ind = graph_ind; + is_general = is_general + } in update_Function finfos -let pr_table () = pr_table !function_table +let pr_table () = pr_table !from_function (*********************************) (* Debuging *) let function_debug = ref false @@ -464,3 +504,5 @@ let do_observe () = +exception Building_graph of exn +exception Defining_principle of exn |