diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 2 | ||||
| -rw-r--r-- | library/dischargedhypsmap.ml | 21 | ||||
| -rw-r--r-- | library/dischargedhypsmap.mli | 19 | ||||
| -rw-r--r-- | library/dune | 9 | ||||
| -rw-r--r-- | library/global.ml | 11 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | library/globnames.ml | 69 | ||||
| -rw-r--r-- | library/globnames.mli | 31 | ||||
| -rw-r--r-- | library/goptions.ml | 21 | ||||
| -rw-r--r-- | library/heads.ml | 193 | ||||
| -rw-r--r-- | library/heads.mli | 28 | ||||
| -rw-r--r-- | library/keys.ml | 6 | ||||
| -rw-r--r-- | library/lib.ml | 25 | ||||
| -rw-r--r-- | library/lib.mli | 5 | ||||
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 48 |
16 files changed, 83 insertions, 412 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 408e259196..36a9598f36 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -47,7 +47,7 @@ let gen_reference_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let qualid = qualid_of_string s in let all = Nametab.locate_all qualid in - let all = List.sort_uniquize RefOrdered_env.compare all in + let all = List.sort_uniquize GlobRef.Ordered_env.compare all in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> x diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml deleted file mode 100644 index abcdb93a27..0000000000 --- a/library/dischargedhypsmap.ml +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis" - -let set_discharged_hyps sp hyps = - discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map - -let get_discharged_hyps sp = - try Spmap.find sp !discharged_hyps_map with Not_found -> [] diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli deleted file mode 100644 index c70677225b..0000000000 --- a/library/dischargedhypsmap.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -(** Discharged hypothesis. Here we store the discharged hypothesis of each - constant or inductive type declaration. *) - -val set_discharged_hyps : full_path -> discharged_hyps -> unit -val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/dune b/library/dune new file mode 100644 index 0000000000..344fad5a75 --- /dev/null +++ b/library/dune @@ -0,0 +1,9 @@ +(library + (name library) + (synopsis "Coq's Loadable Libraries (vo) Support") + (public_name coq.library) + (wrapped false) + (libraries kernel)) + +(documentation + (package coq)) diff --git a/library/global.ml b/library/global.ml index dcb20a280e..5872126a12 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -270,11 +271,17 @@ let with_global f = push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) -let register field value by_clause = - globalize0 (Safe_typing.register field value by_clause) +let register field value = + globalize0 (Safe_typing.register field value) let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) +let set_reduction_sharing b = + let env = safe_env () in + let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in + let flags = { flags with Declarations.share_reduction = b } in + let env = Safe_typing.set_typing_flags flags env in + GlobalSafeEnv.set_safe_env env diff --git a/library/global.mli b/library/global.mli index b2a191ceeb..6aeae9fd02 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit val set_typing_flags : Declarations.typing_flags -> unit +val typing_flags : unit -> Declarations.typing_flags (** Variables, Local definitions, constants, inductive types *) @@ -147,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Constr.constr -> Constr.constr -> unit + Retroknowledge.field -> GlobRef.t -> unit val register_inline : Constant.t -> unit @@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit +val set_reduction_sharing : bool -> unit + (* Modifies the global state, registering new universes *) val current_modpath : unit -> ModPath.t diff --git a/library/globnames.ml b/library/globnames.ml index 6383a1f8f6..6bbdd36489 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -87,65 +87,14 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -let global_eq_gen eq_cst eq_ind eq_cons x y = - x == y || - match x, y with - | ConstRef cx, ConstRef cy -> eq_cst cx cy - | IndRef indx, IndRef indy -> eq_ind indx indy - | ConstructRef consx, ConstructRef consy -> eq_cons consx consy - | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false - -let global_ord_gen ord_cst ord_ind ord_cons x y = - if x == y then 0 - else match x, y with - | VarRef v1, VarRef v2 -> Id.compare v1 v2 - | VarRef _, _ -> -1 - | _, VarRef _ -> 1 - | ConstRef cx, ConstRef cy -> ord_cst cx cy - | ConstRef _, _ -> -1 - | _, ConstRef _ -> 1 - | IndRef indx, IndRef indy -> ord_ind indx indy - | IndRef _, _ -> -1 - | _ , IndRef _ -> 1 - | ConstructRef consx, ConstructRef consy -> ord_cons consx consy - -let global_hash_gen hash_cst hash_ind hash_cons gr = - let open Hashset.Combine in - match gr with - | ConstRef c -> combinesmall 1 (hash_cst c) - | IndRef i -> combinesmall 2 (hash_ind i) - | ConstructRef c -> combinesmall 3 (hash_cons c) - | VarRef id -> combinesmall 4 (Id.hash id) - -(* By default, [global_reference] are ordered on their canonical part *) - -module RefOrdered = struct - open Constant.CanOrd - type t = global_reference - let compare gr1 gr2 = - global_ord_gen compare ind_ord constructor_ord gr1 gr2 - let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2 - let hash gr = global_hash_gen hash ind_hash constructor_hash gr -end - -module RefOrdered_env = struct - open Constant.UserOrd - type t = global_reference - let compare gr1 gr2 = - global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2 - let equal gr1 gr2 = - global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2 - let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr -end - -module Refmap = HMap.Make(RefOrdered) -module Refset = Refmap.Set +module RefOrdered = Names.GlobRef.Ordered +module RefOrdered_env = Names.GlobRef.Ordered_env -(* Alternative sets and maps indexed by the user part of the kernel names *) +module Refmap = Names.GlobRef.Map +module Refset = Names.GlobRef.Set -module Refmap_env = HMap.Make(RefOrdered_env) -module Refset_env = Refmap_env.Set +module Refmap_env = Names.GlobRef.Map_env +module Refset_env = Names.GlobRef.Set_env (* Extended global references *) @@ -164,14 +113,14 @@ module ExtRefOrdered = struct let equal x y = x == y || match x, y with - | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry | SynDef knx, SynDef kny -> KerName.equal knx kny | (TrueGlobal _ | SynDef _), _ -> false let compare x y = if x == y then 0 else match x, y with - | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry + | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry | SynDef knx, SynDef kny -> KerName.compare knx kny | TrueGlobal _, SynDef _ -> -1 | SynDef _, TrueGlobal _ -> 1 @@ -179,7 +128,7 @@ module ExtRefOrdered = struct open Hashset.Combine let hash = function - | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr) + | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr) | SynDef kn -> combinesmall 2 (KerName.hash kn) end diff --git a/library/globnames.mli b/library/globnames.mli index 15fcd5bdd9..45ee069b06 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Constr open Mod_subst @@ -49,27 +48,21 @@ val printable_constr_of_global : GlobRef.t -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t -module RefOrdered : sig - type t = GlobRef.t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int -end +module RefOrdered = Names.GlobRef.Ordered +[@@ocaml.deprecated "Use Names.GlobRef.Ordered"] -module RefOrdered_env : sig - type t = GlobRef.t - val compare : t -> t -> int - val equal : t -> t -> bool - val hash : t -> int -end +module RefOrdered_env = Names.GlobRef.Ordered_env +[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"] -module Refset : CSig.SetS with type elt = GlobRef.t -module Refmap : Map.ExtS - with type key = GlobRef.t and module Set := Refset +module Refset = Names.GlobRef.Set +[@@ocaml.deprecated "Use Names.GlobRef.Set"] +module Refmap = Names.GlobRef.Map +[@@ocaml.deprecated "Use Names.GlobRef.Map"] -module Refset_env : CSig.SetS with type elt = GlobRef.t -module Refmap_env : Map.ExtS - with type key = GlobRef.t and module Set := Refset_env +module Refset_env = GlobRef.Set_env +[@@ocaml.deprecated "Use Names.GlobRef.Set_env"] +module Refmap_env = GlobRef.Map_env +[@@ocaml.deprecated "Use Names.GlobRef.Map_env"] (** {6 Extended global references } *) diff --git a/library/goptions.ml b/library/goptions.ml index f14ad333e9..dcbc46ab72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (name, depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") let check_int_value v = function | IntValue _ -> IntValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "bool" let check_string_value v = function | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | _ -> bad_type_error () + | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | _ -> bad_type_error () + | optv -> bad_type_error optv "nothing" (* Nota: For compatibility reasons, some errors are treated as warning. This allows a script to refer to an option that doesn't @@ -403,7 +412,7 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - str "Synchronous options:" ++ fnl () ++ + str "Options:" ++ fnl () ++ OptionMap.fold (fun key (name, depr, (read,_,_)) p -> p ++ print_option key name (read ()) depr) diff --git a/library/heads.ml b/library/heads.ml deleted file mode 100644 index d9d650ac07..0000000000 --- a/library/heads.ml +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Names -open Constr -open Vars -open Mod_subst -open Environ -open Globnames -open Libobject -open Lib -open Context.Named.Declaration - -(** Characterization of the head of a term *) - -(* We only compute an approximation to ensure the computation is not - arbitrary long (e.g. the head constant of [h] defined to be - [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch - the evaluation of [phi(0)] and the head of [h] is declared unknown). *) - -type rigid_head_kind = -| RigidParameter of Constant.t (* a Const without body *) -| RigidVar of variable (* a Var without body *) -| RigidType (* an inductive, a product or a sort *) - -type head_approximation = -| RigidHead of rigid_head_kind -| ConstructorHead -| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) -| NotImmediatelyComputableHead - -(** Registration as global tables and rollback. *) - -module Evalreford = struct - type t = evaluable_global_reference - let compare gr1 gr2 = match gr1, gr2 with - | EvalVarRef id1, EvalVarRef id2 -> Id.compare id1 id2 - | EvalVarRef _, EvalConstRef _ -> -1 - | EvalConstRef c1, EvalConstRef c2 -> - Constant.CanOrd.compare c1 c2 - | EvalConstRef _, EvalVarRef _ -> 1 -end - -module Evalrefmap = - Map.Make (Evalreford) - - -let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl" - -let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map -let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map - -let kind_of_head env t = - let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with - | Rel n when n > k -> NotImmediatelyComputableHead - | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) - | Var id -> - (try on_subterm k l b (variable_head id) - with Not_found -> - (* a goal variable *) - match lookup_named id env with - | LocalDef (_,c,_) -> aux k l c b - | LocalAssum _ -> NotImmediatelyComputableHead) - | Const (cst,_) -> - (try on_subterm k l b (constant_head cst) - with Not_found -> - CErrors.anomaly - Pp.(str "constant not found in kind_of_head: " ++ - Names.Constant.print cst ++ - str ".")) - | Construct _ | CoFix _ -> - if b then NotImmediatelyComputableHead else ConstructorHead - | Sort _ | Ind _ | Prod _ -> RigidHead RigidType - | Cast (c,_,_) -> aux k l c b - | Lambda (_,_,c) -> - begin match l with - | [] -> - let () = assert (not b) in - aux (k + 1) [] c b - | h :: l -> aux k l (subst1 h c) b - end - | LetIn _ -> assert false - | Meta _ | Evar _ -> NotImmediatelyComputableHead - | App (c,al) -> aux k (Array.to_list al @ l) c b - | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) - with Not_found -> assert false) - - | Case (_,_,c,_) -> aux k [] c true - | Fix ((i,j),_) -> - let n = i.(j) in - try aux k [] (List.nth l n) true - with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true) - and on_subterm k l with_case = function - | FlexibleHead (n,i,q,with_subcase) -> - let m = List.length l in - let k',rest,a = - if n > m then - (* eta-expansion *) - let a = - if i <= m then - (* we pick the head in the existing arguments *) - lift (n-m) (List.nth l (i-1)) - else - (* we pick the head in the added arguments *) - mkRel (n-i+1) in - k+n-m,[],a - else - (* enough arguments to [cst] *) - k,List.skipn n l,List.nth l (i-1) in - let l' = List.make q (mkMeta 0) @ rest in - aux k' l' a (with_subcase || with_case) - | ConstructorHead when with_case -> NotImmediatelyComputableHead - | x -> x - in aux 0 [] t false - -(* FIXME: maybe change interface here *) -let compute_head = function -| EvalConstRef cst -> - let env = Global.env() in - let cb = Environ.lookup_constant cst env in - let is_Def = function Declarations.Def _ -> true | _ -> false in - let body = - if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body - then Global.body_of_constant cst else None - in - (match body with - | None -> RigidHead (RigidParameter cst) - | Some (c, _) -> kind_of_head env c) -| EvalVarRef id -> - (match Global.lookup_named id with - | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> - kind_of_head (Global.env()) c - | _ -> - RigidHead (RigidVar id)) - -let is_rigid env t = - match kind_of_head env t with - | RigidHead _ | ConstructorHead -> true - | _ -> false - -(** Registration of heads as an object *) - -let load_head _ (_,(ref,(k:head_approximation))) = - head_map := Evalrefmap.add ref k !head_map - -let cache_head o = - load_head 1 o - -let subst_head_approximation subst = function - | RigidHead (RigidParameter cst) as k -> - let cst,c = subst_con_kn subst cst in - if isConst c && Constant.equal (fst (destConst c)) cst then - (* A change of the prefix of the constant *) - k - else - (* A substitution of the constant by a functor argument *) - kind_of_head (Global.env()) c - | x -> x - -let subst_head (subst,(ref,k)) = - (subst_evaluable_reference subst ref, subst_head_approximation subst k) - -let discharge_head (_,(ref,k)) = - match ref with - | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k) - | EvalVarRef id -> None - -let rebuild_head (ref,k) = - (ref, compute_head ref) - -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; - subst_function = subst_head; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_head; - rebuild_function = rebuild_head } - -let declare_head c = - let hd = compute_head c in - add_anonymous_leaf (inHead (c,hd)) diff --git a/library/heads.mli b/library/heads.mli deleted file mode 100644 index 421242996c..0000000000 --- a/library/heads.mli +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Environ - -(** This module is about the computation of an approximation of the - head symbol of defined constants and local definitions; it - provides the function to compute the head symbols and a table to - store the heads *) - -(** [declared_head] computes and registers the head symbol of a - possibly evaluable constant or variable *) - -val declare_head : evaluable_global_reference -> unit - -(** [is_rigid] tells if some term is known to ultimately reduce to a term - with a rigid head symbol *) - -val is_rigid : env -> constr -> bool diff --git a/library/keys.ml b/library/keys.ml index 3cadcb6472..a74d13c600 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -31,7 +31,7 @@ module KeyOrdered = struct let hash gr = match gr with - | KGlob gr -> 8 + RefOrdered.hash gr + | KGlob gr -> 8 + GlobRef.Ordered.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 @@ -43,14 +43,14 @@ module KeyOrdered = struct let compare gr1 gr2 = match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2 + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 | _, KGlob _ -> -1 | KGlob _, _ -> 1 | k, k' -> Int.compare (hash k) (hash k') let equal k1 k2 = match k1, k2 with - | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2 + | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 | _, KGlob _ -> false | KGlob _, _ -> false | k, k' -> k == k' diff --git a/library/lib.ml b/library/lib.ml index a20de55bf6..8ebe44890c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -26,13 +26,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of is_type * export * object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_entry = object_name * node +type library_entry = object_name * node -and library_segment = library_entry list +type library_segment = library_entry list type lib_objects = (Names.Id.t * obj) list @@ -73,10 +71,6 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (_,ClosedSection _) :: stk -> clean acc stk - (* LEM; TODO: Understand what this does and see if what I do is the - correct thing for ClosedMod(ule|type) *) - | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -307,7 +301,6 @@ let end_mod is_type = in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !lib_state.path_prefix in recalc_path_prefix (); (oname, prefix, fs, after) @@ -555,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -570,7 +562,6 @@ let close_section () = let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); - add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls @@ -589,10 +580,8 @@ let freeze ~marshallable = | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) - | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -656,6 +645,14 @@ let discharge_kn kn = let discharge_con cst = if con_defined_in_sec cst then Globnames.pop_con cst else cst +let discharge_proj_repr = + Projection.Repr.map_npars (fun mind npars -> + if not (defined_in_sec mind) then mind, npars + else + let modlist = replacement_context () in + let _, newpars = Mindmap.find mind (snd modlist) in + Globnames.pop_kn mind, npars + Array.length newpars) + let discharge_inductive (kn,i) = (discharge_kn kn,i) diff --git a/library/lib.mli b/library/lib.mli index 5abfccfc7d..9933b762ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,11 +23,9 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list @@ -189,6 +187,7 @@ val replacement_context : unit -> Opaqueproof.work_list val discharge_kn : MutInd.t -> MutInd.t val discharge_con : Constant.t -> Constant.t +val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_global : GlobRef.t -> GlobRef.t val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : diff --git a/library/library.mllib b/library/library.mllib index 2ac4266fc0..8f694f4a31 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -11,9 +11,7 @@ Loadpath Library States Kindops -Dischargedhypsmap Goptions Decls -Heads Keys Coqlib diff --git a/library/nametab.ml b/library/nametab.ml index a3b3ca6e74..840cf8e380 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -279,10 +279,10 @@ module ExtRefTab = Make(FullPath)(ExtRefEqual) module MPTab = Make(FullPath)(MPEqual) type ccitab = ExtRefTab.t -let the_ccitab = ref (ExtRefTab.empty : ccitab) +let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab) type mptab = MPTab.t -let the_modtypetab = ref (MPTab.empty : mptab) +let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab) module DirPath' = struct @@ -303,7 +303,7 @@ module DirTab = Make(DirPath')(GlobDir) (* If we have a (closed) module M having a submodule N, than N does not have the entry in [the_dirtab]. *) type dirtab = DirTab.t -let the_dirtab = ref (DirTab.empty : dirtab) +let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab) type universe_id = DirPath.t * int @@ -314,7 +314,7 @@ struct end module UnivTab = Make(FullPath)(UnivIdEqual) type univtab = UnivTab.t -let the_univtab = ref (UnivTab.empty : univtab) +let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab) (* Reversed name tables ***************************************************) @@ -322,14 +322,14 @@ let the_univtab = ref (UnivTab.empty : univtab) module Globrevtab = HMap.Make(ExtRefOrdered) type globrevtab = full_path Globrevtab.t -let the_globrevtab = ref (Globrevtab.empty : globrevtab) +let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab) type mprevtab = DirPath.t MPmap.t -let the_modrevtab = ref (MPmap.empty : mprevtab) +let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t -let the_modtyperevtab = ref (MPmap.empty : mptrevtab) +let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab) module UnivIdOrdered = struct @@ -344,7 +344,7 @@ end module UnivIdMap = HMap.Make(UnivIdOrdered) type univrevtab = full_path UnivIdMap.t -let the_univrevtab = ref (UnivIdMap.empty : univrevtab) +let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab) (* Push functions *********************************************************) @@ -546,38 +546,6 @@ let global_inductive qid = (********************************************************************) -(********************************************************************) -(* Registration of tables as a global table and rollback *) - -type frozen = ccitab * dirtab * mptab * univtab - * globrevtab * mprevtab * mptrevtab * univrevtab - -let freeze _ : frozen = - !the_ccitab, - !the_dirtab, - !the_modtypetab, - !the_univtab, - !the_globrevtab, - !the_modrevtab, - !the_modtyperevtab, - !the_univrevtab - -let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) = - the_ccitab := ccit; - the_dirtab := dirt; - the_modtypetab := mtyt; - the_univtab := univt; - the_globrevtab := globr; - the_modrevtab := modr; - the_modtyperevtab := mtyr; - the_univrevtab := univr - -let _ = - Summary.declare_summary "names" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = Summary.nop } - (* Deprecated synonyms *) let extended_locate = locate_extended |