diff options
Diffstat (limited to 'toplevel/libtypes.ml')
-rw-r--r-- | toplevel/libtypes.ml | 111 |
1 files changed, 0 insertions, 111 deletions
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml deleted file mode 100644 index b392f82c..00000000 --- a/toplevel/libtypes.ml +++ /dev/null @@ -1,111 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Summary -open Libobject -open Libnames -open Names -(* - * Module construction - *) - -(* let reduce c = Reductionops.head_unfold_under_prod *) -(* (Auto.Hint_db.transparent_state (Auto.searchtable_map "typeclass_instances")) *) -(* (Global.env()) Evd.empty c *) - -let reduce c = c - -module TypeDnet = Term_dnet.Make - (struct - type t = Libnames.global_reference - let compare = RefOrdered.compare - let subst s gr = fst (Libnames.subst_global s gr) - let constr_of = Global.type_of_global - end) - (struct let reduce = reduce - let direction = false - end) - -type result = Libnames.global_reference * (constr*existential_key) * Termops.subst - -let all_types = ref TypeDnet.empty -let defined_types = ref TypeDnet.empty - -(* - * Bookeeping & States - *) - -let freeze () = - (!all_types,!defined_types) - -let unfreeze (lt,dt) = - all_types := lt; - defined_types := dt - -let init () = - all_types := TypeDnet.empty; - defined_types := TypeDnet.empty - -let _ = - declare_summary "type-library-state" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = init } - -let load (_,d) = -(* Profile.print_logical_stats !all_types; - Profile.print_logical_stats d;*) - all_types := TypeDnet.union d !all_types - -let subst s t = TypeDnet.subst s t -(* -let subst_key = Profile.declare_profile "subst" -let subst a b = Profile.profile2 subst_key TypeDnet.subst a b - -let load_key = Profile.declare_profile "load" -let load a = Profile.profile1 load_key load a -*) -let input : TypeDnet.t -> obj = - declare_object - { (default_object "LIBTYPES") with - load_function = (fun _ -> load); - subst_function = (fun (s,t) -> subst s t); - classify_function = (fun x -> Substitute x) - } - -let update () = Lib.add_anonymous_leaf (input !defined_types) - -(* - * Search interface - *) - -let search_pattern pat = TypeDnet.search_pattern !all_types pat -let search_concl pat = TypeDnet.search_concl !all_types pat -let search_head_concl pat = TypeDnet.search_head_concl !all_types pat -let search_eq_concl eq pat = TypeDnet.search_eq_concl !all_types eq pat - -let add typ gr = - defined_types := TypeDnet.add typ gr !defined_types; - all_types := TypeDnet.add typ gr !all_types -(* -let add_key = Profile.declare_profile "add" -let add a b = Profile.profile1 add_key add a b -*) - -(* - * Hooks declaration - *) - -let _ = Declare.add_cache_hook - ( fun sp -> - let gr = Nametab.global_of_path sp in - let ty = Global.type_of_global gr in - add ty gr ) - -let _ = Declaremods.set_end_library_hook update |