From b359ef0ffad7fd1fc0e4db99fc1e38a1389802bc Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 2 Nov 2011 18:59:57 +0000 Subject: Add type annotations around all calls to Libobject.declare_object These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/implicit_quantifiers.ml | 6 +- interp/notation.ml | 8 +- interp/reserve.ml | 2 +- interp/syntax_def.ml | 2 +- library/declare.ml | 14 +++- library/declaremods.ml | 143 ++++++++++++++++------------------- library/goptions.ml | 2 +- library/heads.ml | 4 +- library/impargs.ml | 6 +- library/lib.ml | 2 +- library/library.ml | 13 ++-- plugins/dp/dp.ml | 12 +-- plugins/extraction/table.ml | 17 ++--- plugins/field/field.ml4 | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/ring/ring.ml | 2 +- plugins/setoid_ring/newring.ml4 | 4 +- plugins/subtac/subtac_obligations.ml | 2 +- pretyping/classops.ml | 5 +- pretyping/recordops.ml | 12 ++- pretyping/recordops.mli | 6 +- pretyping/typeclasses.ml | 4 +- proofs/redexpr.ml | 7 +- tactics/auto.ml | 4 +- tactics/autorewrite.ml | 2 +- tactics/dhyp.ml | 2 +- tactics/extratactics.ml4 | 2 +- tactics/tacinterp.ml | 2 +- tactics/tactic_option.ml | 2 +- toplevel/ind_tables.ml | 2 +- toplevel/libtypes.ml | 2 +- toplevel/metasyntax.ml | 25 ++++-- toplevel/mltop.ml4 | 2 +- 33 files changed, 180 insertions(+), 142 deletions(-) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a104cd5db..f27390435 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -56,14 +56,14 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table - -let in_generalizable = + +let in_generalizable : bool * identifier located list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } - + let declare_generalizable local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) diff --git a/interp/notation.ml b/interp/notation.ml index ae14cd5ca..aa35e4af0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -117,7 +117,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope = +let inScope : bool * bool * scope_elem -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -520,7 +520,11 @@ let rebuild_arguments_scope (req,r,l,_) = let l1,_ = list_chop (List.length l' - List.length l) l' in (req,r,l1@l,cls) -let inArgumentsScope = +type arguments_scope_obj = + arguments_scope_discharge_request * global_reference * + scope_name option list * Classops.cl_typ option list + +let inArgumentsScope : arguments_scope_obj -> obj = declare_object {(default_object "ARGUMENTS-SCOPE") with cache_function = cache_arguments_scope; load_function = load_arguments_scope; diff --git a/interp/reserve.ml b/interp/reserve.ml index 6c96e20c1..a07f5c846 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -37,7 +37,7 @@ let cache_reserved_type (_,(id,t)) = reserve_table := Idmap.add id t !reserve_table; reserve_revtable := Gmapl.add key (t,id) !reserve_revtable -let in_reserved = +let in_reserved : identifier * aconstr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 8056ab426..8863bbbd3 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -62,7 +62,7 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) = let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant = +let in_syntax_constant : bool * interpretation * bool -> obj = declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; diff --git a/library/declare.ml b/library/declare.ml index 10dc35b95..0afd4bd9e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -78,7 +78,10 @@ let discharge_variable (_,o) = match o with | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let inVariable = +type variable_obj = + (Univ.constraints, identifier * variable_declaration) union + +let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -151,7 +154,10 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let classify_constant cst = Substitute (dummy_constant cst) -let inConstant = +type constant_obj = + global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind + +let inConstant : constant_obj -> obj = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -246,7 +252,9 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = true; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) -let inInductive = +type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry + +let inInductive : inductive_obj -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; diff --git a/library/declaremods.ml b/library/declaremods.ml index 95d2310ce..90d4245a4 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -179,14 +179,21 @@ let check_sub mtb sub_mtb_l = environment. *) let check_subtypes mp sub_mtb_l = - let mb = Global.lookup_module mp in + let mb = + try Global.lookup_module mp + with Not_found -> assert false + in let mtb = Modops.module_type_of_module None mb in check_sub mtb sub_mtb_l (* Same for module type [mp] *) let check_subtypes_mt mp sub_mtb_l = - check_sub (Global.lookup_modtype mp) sub_mtb_l + let mtb = + try Global.lookup_modtype mp + with Not_found -> assert false + in + check_sub mtb sub_mtb_l (* Create a functor type entry *) @@ -274,42 +281,26 @@ let conv_names_do_module exists what iter_objects i functions can be called only once (and "end_mod*" set the flag to false then) *) -let cache_module ((sp,kn),(entry,substobjs)) = +let cache_module ((sp,kn),substobjs) = let dir,mp = dir_of_sp sp, mp_of_kn kn in do_module false "cache" load_objects 1 dir mp substobjs [] - -(* TODO: This check is not essential *) -let check_empty s = function - | None -> () - | Some _ -> - anomaly ("We should never have full info in " ^ s^"!") - (* When this function is called the module itself is already in the environment. This function loads its objects only *) -let load_module i (oname,(entry,substobjs)) = - (* TODO: This check is not essential *) - check_empty "load_module" entry; +let load_module i (oname,substobjs) = conv_names_do_module false "load" load_objects i oname substobjs - -let open_module i (oname,(entry,substobjs)) = - (* TODO: This check is not essential *) - check_empty "open_module" entry; +let open_module i (oname,substobjs) = conv_names_do_module true "open" open_objects i oname substobjs +let subst_module (subst,(mbids,mp,objs)) = + (mbids,subst_mp subst mp, subst_objects subst objs) +let classify_module substobjs = Substitute substobjs -let subst_module (subst,(entry,(mbids,mp,objs))) = - check_empty "subst_module" entry; - (None,(mbids,subst_mp subst mp, subst_objects subst objs)) - - -let classify_module (_,substobjs) = - Substitute (None,substobjs) - -let (in_module,out_module) = +let (in_module : substitutive_objects -> obj), + (out_module : obj -> substitutive_objects) = declare_object_full {(default_object "MODULE") with cache_function = cache_module; load_function = load_module; @@ -337,7 +328,7 @@ let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,empty_dirpath)) seg -let in_modkeep = +let in_modkeep : lib_objects -> obj = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; @@ -369,6 +360,7 @@ let _ = Summary.declare_summary "MODTYPE-INFO" let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let mp = mp_of_kn kn in + (* We enrich the global environment *) let _ = match entry with | None -> @@ -392,7 +384,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = - check_empty "load_modtype" entry; + assert (entry = None); if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" @@ -404,7 +396,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = let open_modtype i ((sp,kn),(entry,_,_)) = - check_empty "open_modtype" entry; + assert (entry = None); if try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) @@ -416,15 +408,18 @@ let open_modtype i ((sp,kn),(entry,_,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = - check_empty "subst_modtype" entry; + assert (entry = None); (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) - let classify_modtype (_,substobjs,_) = Substitute (None,substobjs,[]) +type modtype_obj = + (module_struct_entry * Entries.inline) option (* will be None in vo *) + * substitutive_objects + * module_type_body list -let in_modtype = +let in_modtype : modtype_obj -> obj = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; open_function = open_modtype; @@ -432,35 +427,27 @@ let in_modtype = subst_function = subst_modtype; classify_function = classify_modtype } -let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1= - if mbids<>[] then - error "Unexpected functor objects" - else - let rec replace_idl = function - | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj = "MODULE" then - (match idl with - [] -> (id, in_module - (None,(mbids,(MPdot(mp,label_of_id id)),subst_objects - (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail - | _ -> - let (_,substobjs) = out_module obj in - let substobjs' = replace_module_object idl substobjs - (mbids2,mp2,objs) mp in - (id, in_module (None,substobjs'))::tail - ) - else error "MODULE expected!" - | idl,lobj::tail -> lobj::replace_idl (idl,tail) - in - (mbids, mp, replace_idl (idl,lib_stack)) +let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 = + if mbids<>[] then anomaly "Unexpected functor objects"; + let rec replace_idl = function + | _,[] -> [] + | id::idl,(id',obj)::tail when id = id' -> + if object_tag obj <> "MODULE" then anomaly "MODULE expected!"; + let substobjs = + if idl = [] then + let mp' = MPdot(mp, label_of_id id) in + mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs + else + replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp + in + (id, in_module substobjs)::tail + | idl,lobj::tail -> lobj::replace_idl (idl,tail) + in + (mbids, mp, replace_idl (idl,lib_stack)) -let discr_resolver mb = - match mb.mod_type with - SEBstruct _ -> - Some mb.mod_delta - | _ -> (*case mp is a functor *) - None +let discr_resolver mb = match mb.mod_type with + | SEBstruct _ -> Some mb.mod_delta + | _ -> None (* when mp is a functor *) (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_modtype_application env = function @@ -622,7 +609,7 @@ let end_module () = | Some mp_from,(mbids,_,objs) -> (mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) in - let node = in_module (None,substobjs) in + let node = in_module substobjs in let objects = if keep = [] || mbids <> [] then special@[node] (* no keep objects or we are defining a functor *) @@ -859,7 +846,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = reset_scope_subst (); ignore (add_leaf id - (in_module (Some (entry), substobjs))); + (in_module substobjs)); mmp (* Include *) @@ -887,32 +874,33 @@ let lift_oname (sp,kn) = let dir,_ = Libnames.repr_path sp in (dir,mp) -let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) = +let cache_include (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in load_objects 1 prefix objs; - open_objects 1 prefix objs - -let load_include i (oname,((me,is_mod),(mbis,mp1,objs))) = + open_objects 1 prefix objs + +let load_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in load_objects i prefix objs - - -let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) = + +let open_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in let prefix = (dir,(mp1,empty_dirpath)) in open_objects i prefix objs - -let subst_include (subst,((me,is_mod),substobj)) = + +let subst_include (subst,(me,substobj)) = let (mbids,mp,objs) = substobj in let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in - ((subst_inc_expr subst me,is_mod),substobjs) - -let classify_include ((me,is_mod),substobjs) = - Substitute ((me,is_mod),substobjs) + (subst_inc_expr subst me,substobjs) + +let classify_include (me,substobjs) = Substitute (me,substobjs) + +type include_obj = module_struct_entry * substitutive_objects -let (in_include,out_include) = +let (in_include : include_obj -> obj), + (out_include : obj -> include_obj) = declare_object_full {(default_object "INCLUDE") with cache_function = cache_include; load_function = load_include; @@ -987,8 +975,7 @@ let declare_one_include_inner annot (me,is_mod) = let substobjs = (mbids,mp1, subst_objects (map_mp mp mp1 resolver) objs) in reset_scope_subst (); - ignore (add_leaf id - (in_include ((me,is_mod), substobjs))) + ignore (add_leaf id (in_include (me, substobjs))) let declare_one_include interp_struct (me_ast,annot) = declare_one_include_inner annot diff --git a/library/goptions.ml b/library/goptions.ml index fbce68fad..7c522022f 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -94,7 +94,7 @@ module MakeTable = if p' == p then obj else (f,p') in - let inGo = + let inGo : option_mark * A.t -> obj = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; Libobject.open_function = load_options; diff --git a/library/heads.ml b/library/heads.ml index 813031558..9f9f1ca25 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -167,7 +167,9 @@ let discharge_head (_,(ref,k)) = let rebuild_head (ref,k) = (ref, compute_head ref) -let inHead = +type head_obj = evaluable_global_reference * head_approximation + +let inHead : head_obj -> obj = declare_object {(default_object "HEAD") with cache_function = cache_head; load_function = load_head; diff --git a/library/impargs.ml b/library/impargs.ml index 3f60bf96a..2d5ffe9ab 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -548,7 +548,11 @@ let rebuild_implicits (req,l) = let classify_implicits (req,_ as obj) = if req = ImplLocal then Dispose else Substitute obj -let inImplicits = +type implicits_obj = + implicit_discharge_request * + (global_reference * implicits_list list) list + +let inImplicits : implicits_obj -> obj = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; diff --git a/library/lib.ml b/library/lib.ml index 23d334a5d..7554fd0bb 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -539,7 +539,7 @@ let close_section () = (*****************) (* Backtracking. *) -let (inLabel,outLabel) = +let (inLabel : int -> obj), (outLabel : obj -> int) = declare_object_full {(default_object "DOT") with classify_function = (fun _ -> Dispose)} diff --git a/library/library.ml b/library/library.ml index 9c602adbb..071c7a46c 100644 --- a/library/library.ml +++ b/library/library.ml @@ -300,7 +300,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let in_import = +let in_import : dir_path * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -498,7 +498,7 @@ let rec_intern_library_from_file idopt f = type library_reference = dir_path list * bool option -let register_library (dir,m) = +let register_library m = Declaremods.register_library m.library_name m.library_compiled @@ -526,7 +526,9 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -let in_require = +type require_obj = library_t list * dir_path list * bool option + +let in_require : require_obj -> obj = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; @@ -541,7 +543,8 @@ let xml_require = ref (fun d -> ()) let set_xml_require f = xml_require := f let require_library_from_dirpath modrefl export = - let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in + let needed = List.fold_left rec_intern_library [] modrefl in + let needed = List.rev_map snd needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin @@ -561,7 +564,7 @@ let require_library qidl export = let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in - let needed = List.rev needed in + let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index b025cea64..837195e44 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -36,7 +36,7 @@ let set_trace b = trace := b let timeout = ref 10 let set_timeout n = timeout := n -let dp_timeout_obj = +let dp_timeout_obj : int -> obj = declare_object {(default_object "Dp_timeout") with cache_function = (fun (_,x) -> set_timeout x); @@ -44,7 +44,7 @@ let dp_timeout_obj = let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) -let dp_debug_obj = +let dp_debug_obj : bool -> obj = declare_object {(default_object "Dp_debug") with cache_function = (fun (_,x) -> set_debug x); @@ -52,7 +52,7 @@ let dp_debug_obj = let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) -let dp_trace_obj = +let dp_trace_obj : bool -> obj = declare_object {(default_object "Dp_trace") with cache_function = (fun (_,x) -> set_trace x); @@ -825,7 +825,7 @@ let prelude_files = ref ([] : string list) let set_prelude l = prelude_files := l -let dp_prelude_obj = +let dp_prelude_obj : string list -> obj = declare_object {(default_object "Dp_prelude") with cache_function = (fun (_,x) -> set_prelude x); @@ -1087,7 +1087,7 @@ let dp_hint l = in List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l) -let dp_hint_obj = +let dp_hint_obj : reference list -> obj = declare_object {(default_object "Dp_hint") with cache_function = (fun (_,l) -> dp_hint l); @@ -1113,7 +1113,7 @@ let dp_predefined qid s = with NotFO -> msg_warning (str " ignored (not a first order declaration)") -let dp_predefined_obj = +let dp_predefined_obj : reference * string -> obj = declare_object {(default_object "Dp_predefined") with cache_function = (fun (_,(id,s)) -> dp_predefined id s); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 502d06235..75584ead3 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -493,7 +493,7 @@ let lang_ref = ref Ocaml let lang () = !lang_ref -let extr_lang = +let extr_lang : lang -> obj = declare_object {(default_object "Extraction Lang") with cache_function = (fun (_,l) -> lang_ref := l); @@ -525,7 +525,7 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let inline_extraction = +let inline_extraction : bool * global_reference list -> obj = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); @@ -569,7 +569,7 @@ let print_extraction_inline () = (* Reset part *) -let reset_inline = +let reset_inline : unit -> obj = declare_object {(default_object "Reset Extraction Inline") with cache_function = (fun (_,_)-> inline_table := empty_inline_table); @@ -608,7 +608,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let implicit_extraction = +let implicit_extraction : global_reference * int_or_id list -> obj = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -668,12 +668,11 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) -let blacklist_extraction = +let blacklist_extraction : string list -> obj = declare_object {(default_object "Extraction Blacklist") with cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); - classify_function = (fun o -> Libobject.Keep o); subst_function = (fun (_,x) -> x) } @@ -696,7 +695,7 @@ let print_extraction_blacklist () = (* Reset part *) -let reset_blacklist = +let reset_blacklist : unit -> obj = declare_object {(default_object "Reset Extraction Blacklist") with cache_function = (fun (_,_)-> blacklist_table := Idset.empty); @@ -742,7 +741,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let in_customs = +let in_customs : global_reference * string list * string -> obj = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -757,7 +756,7 @@ let _ = declare_summary "ML extractions" unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap'.empty) } -let in_custom_matchs = +let in_custom_matchs : global_reference * string -> obj = declare_object {(default_object "ML extractions custom matchs") with cache_function = (fun (_,(r,s)) -> add_custom_match r s); diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 8b6bb133a..9e4f4d745 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -67,7 +67,7 @@ let subst_addfield (subst,(typ,th as obj)) = (typ',th') (* Declaration of the Add Field library object *) -let in_addfield = +let in_addfield : types * constr -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); Libobject.cache_function = cache_addfield; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 094d2e50f..951b25baf 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -362,7 +362,7 @@ 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 = +let in_Function : function_info -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "FUNCTIONS_DB") with Libobject.cache_function = cache_Function; diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 9a252dfb7..98d6361c0 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) = (c',th') -let theory_to_obj = +let theory_to_obj : constr * theory -> obj = let cache_th (_,(c, th)) = theories_map_add (c,th) in declare_object {(default_object "tactic-ring-theory") with open_function = (fun i o -> if i=1 then cache_th o); diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 6ff673023..af236bc0f 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -438,7 +438,7 @@ let subst_th (subst,th) = ring_post_tac = posttac' } -let theory_to_obj = +let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with @@ -1014,7 +1014,7 @@ let subst_th (subst,th) = field_pre_tac = pretac'; field_post_tac = posttac' } -let ftheory_to_obj = +let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in declare_object {(default_object "tactic-new-field-theory") with diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index b3ff7c9f0..74ee05bbc 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -213,7 +213,7 @@ let close sec = (str (if List.length keys = 1 then " has " else "have ") ++ str "unsolved obligations")) -let input = +let input : program_info ProgMap.t -> obj = declare_object { (default_object "Program state") with cache_function = (fun (na, pi) -> from_prg := pi); diff --git a/pretyping/classops.ml b/pretyping/classops.ml index f6eaaa665..03ae6e763 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -405,7 +405,10 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = if stre = Local then Dispose else Substitute obj -let inCoercion = +type coercion_obj = + coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int + +let inCoercion : coercion_obj -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 0f1b9ac97..994fe33d0 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -43,6 +43,12 @@ type struc_typ = { let structure_table = ref (Indmap.empty : struc_typ Indmap.t) let projection_table = ref Cmap.empty +(* TODO: could be unify struc_typ and struc_tuple ? in particular, + is the inductive always (fst constructor) ? It seems so... *) + +type struc_tuple = + inductive * constructor * (name * bool) list * constant option list + let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let struc = @@ -75,7 +81,7 @@ let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, discharge_constructor id, kl, List.map (Option.map Lib.discharge_con) projs) -let inStruc = +let inStruc : struc_tuple -> obj = declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -134,7 +140,7 @@ open Libobject let load_method (_,(ty,id)) = meth_dnet := MethodsDnet.add ty id !meth_dnet -let in_method = +let in_method : constr * MethodsDnet.ident -> obj = declare_object { (default_object "RECMETHODS") with load_function = (fun _ -> load_method); @@ -289,7 +295,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let inCanonStruc = +let inCanonStruc : constant * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e5b94449c..b4e76756b 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -25,8 +25,10 @@ type struc_typ = { s_PROJKIND : (name * bool) list; s_PROJ : constant option list } -val declare_structure : - inductive * constructor * (name * bool) list * constant option list -> unit +type struc_tuple = + inductive * constructor * (name * bool) list * constant option list + +val declare_structure : struc_tuple -> unit (** [lookup_structure isp] returns the struc_typ associated to the inductive path [isp] if it corresponds to a structure, otherwise diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index caee039e0..89e0fc93d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -210,7 +210,7 @@ let rebuild_class cl = set_typeclass_transparency cst false false; cl with _ -> cl -let class_input = +let class_input : typeclass -> obj = declare_object { (default_object "type classes state") with cache_function = cache_class; @@ -282,7 +282,7 @@ let load_instance (_, (action, inst) as ai) = if action = AddInstance then add_instance_hint inst.is_impl (is_local inst) inst.is_pri -let instance_input = +let instance_input : instance_action * instance -> obj = declare_object { (default_object "type classes instances state") with cache_function = cache_instance; diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c6b3339d7..0430a239e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -86,7 +86,10 @@ let discharge_strategy (_,(local,obj)) = if local then None else map_strategy disch_ref obj -let inStrategy = +type strategy_obj = + bool * (Conv_oracle.level * evaluable_global_reference list) list + +let inStrategy : strategy_obj -> obj = declare_object {(default_object "STRATEGY") with cache_function = (fun (_,obj) -> cache_strategy obj); load_function = (fun _ (_,obj) -> cache_strategy obj); @@ -212,7 +215,7 @@ let subst_red_expr subs e = (Pattern.subst_pattern subs) e -let inReduction = +let inReduction : bool * string * red_expr -> obj = declare_object {(default_object "REDUCTION") with cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); diff --git a/tactics/auto.ml b/tactics/auto.ml index 8fc403b78..72917530b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -487,6 +487,8 @@ type hint_action = | AddHints of hint_entry list | RemoveHints of global_reference list +type hint_obj = bool * string * hint_action (* locality, name, action *) + let cache_autohint (_,(local,name,hints)) = match hints with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) @@ -556,7 +558,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let classify_autohint ((local,name,hintlist) as obj) = if local or hintlist = (AddHints []) then Dispose else Substitute obj -let inAutoHint = +let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 13f8784f5..c9951bea2 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -223,7 +223,7 @@ let classify_hintrewrite x = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) -let inHintRewrite = +let inHintRewrite : string * HintDN.t -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with Libobject.cache_function = cache_hintrewrite; Libobject.load_function = (fun _ -> cache_hintrewrite); diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index f9c316955..fd924707c 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -220,7 +220,7 @@ let subst_dd (subst,(local,na,dd)) = d_pri = dd.d_pri; d_code = !forward_subst_tactic subst dd.d_code }) -let inDD = +let inDD : bool * identifier * destructor_data -> obj = declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 4af1bce7d..bae28c7ce 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -442,7 +442,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity = +let inTransitivity : bool * constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b310dd645..90e4582fa 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2844,7 +2844,7 @@ let subst_md (subst,(local,defs)) = let classify_md (local,defs as o) = if local then Dispose else Substitute o -let inMD = +let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 1310fe7f9..57b8c5406 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -25,7 +25,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = let subst (s, (local, tac)) = (local, Tacinterp.subst_tactic s tac) in - let input = + let input : bool * Tacexpr.glob_tactic_expr -> obj = declare_object { (default_object name) with cache_function = cache; diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index bb5ab795d..30c537f28 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -51,7 +51,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let inScheme = +let inScheme : string * (inductive * constant) array -> obj = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index c182fb385..2f98962cf 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -71,7 +71,7 @@ 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 = +let input : TypeDnet.t -> obj = declare_object { (default_object "LIBTYPES") with load_function = (fun _ -> load); diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 3c7e98722..6a4d72516 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -32,7 +32,7 @@ open Nameops let cache_token (_,s) = add_keyword s -let inToken = +let inToken : string -> obj = declare_object {(default_object "TOKEN") with open_function = (fun i o -> if i=1 then cache_token o); cache_function = cache_token; @@ -70,7 +70,12 @@ let subst_tactic_parule subst (key,n,p,(d,tac)) = let subst_tactic_notation (subst,(pa,pp)) = (subst_tactic_parule subst pa,pp) -let inTacticGrammar = +type tactic_grammar_obj = + (string * int * grammar_prod_item list * + (dir_path * Tacexpr.glob_tactic_expr)) + * (string * Genarg.argument_type list * (int * Pptactic.grammar_terminals)) + +let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with open_function = (fun i o -> if i=1 then cache_tactic_notation o); cache_function = cache_tactic_notation; @@ -710,7 +715,13 @@ let subst_syntax_extension (subst,(local,sy)) = let classify_syntax_definition (local,_ as o) = if local then Dispose else Substitute o -let inSyntaxExtension = +type syntax_extension_obj = + bool * + (notation_var_internalization_type list * Notation.level * + notation * notation_grammar * unparsing list) + list + +let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with open_function = (fun i o -> if i=1 then cache_syntax_extension o); cache_function = cache_syntax_extension; @@ -962,7 +973,11 @@ let subst_notation (subst,(lc,scope,pat,b,ndf)) = let classify_notation (local,_,_,_,_ as o) = if local then Dispose else Substitute o -let inNotation = +type notation_obj = + bool * scope_name option * interpretation * bool * + (notation * notation_location) + +let inNotation : notation_obj -> obj = declare_object {(default_object "NOTATION") with open_function = open_notation; cache_function = cache_notation; @@ -1138,7 +1153,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with scope, ScopeClasses cl' | _ -> x -let inScopeCommand = +let inScopeCommand : scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d9a261ed4..3cda90425 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -296,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) = let classify_ml_module_object ({mlocal=mlocal} as o) = if mlocal then Dispose else Substitute o -let inMLModule = +let inMLModule : ml_module_object -> obj = declare_object {(default_object "ML-MODULE") with load_function = (fun _ -> cache_ml_module_object); cache_function = cache_ml_module_object; -- cgit v1.2.3