diff options
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 8 | ||||
-rw-r--r-- | library/declaremods.ml | 2 | ||||
-rw-r--r-- | library/decls.ml | 13 | ||||
-rw-r--r-- | library/global.mli | 6 | ||||
-rw-r--r-- | library/globnames.ml | 23 | ||||
-rw-r--r-- | library/globnames.mli | 8 | ||||
-rw-r--r-- | library/heads.ml | 11 | ||||
-rw-r--r-- | library/impargs.ml | 15 | ||||
-rw-r--r-- | library/keys.ml | 28 | ||||
-rw-r--r-- | library/lib.ml | 9 | ||||
-rw-r--r-- | library/lib.mli | 8 | ||||
-rw-r--r-- | library/libnames.ml | 4 | ||||
-rw-r--r-- | library/libobject.ml | 21 | ||||
-rw-r--r-- | library/libobject.mli | 5 | ||||
-rw-r--r-- | library/library.ml | 46 | ||||
-rw-r--r-- | library/library.mli | 3 | ||||
-rw-r--r-- | library/loadpath.ml | 25 | ||||
-rw-r--r-- | library/loadpath.mli | 2 | ||||
-rw-r--r-- | library/nameops.ml | 4 | ||||
-rw-r--r-- | library/nametab.ml | 2 | ||||
-rw-r--r-- | library/summary.ml | 26 | ||||
-rw-r--r-- | library/summary.mli | 4 | ||||
-rw-r--r-- | library/universes.ml | 83 | ||||
-rw-r--r-- | library/universes.mli | 13 |
24 files changed, 195 insertions, 174 deletions
diff --git a/library/declare.ml b/library/declare.ml index c9d5fdbe2..c59d190a0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -426,13 +426,13 @@ let definition_message id = Flags.if_verbose msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) -type universe_names = - (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) - (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list diff --git a/library/declaremods.ml b/library/declaremods.ml index 651c76ae1..701c15e14 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (object_has_tag obj "MODULE"); + assert (String.equal (object_tag obj) "MODULE"); let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 diff --git a/library/decls.ml b/library/decls.ml index 0cd4ccb25..6e21880f1 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -11,7 +11,6 @@ open Util open Names -open Context open Decl_kinds open Libnames @@ -47,16 +46,20 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) +open Context.Named.Declaration + let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in + (fun d signv -> + let id = get_id d in + let d = if variable_opacity id then LocalAssum (id, get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = - fold_named_context - (fun (id,_,_) sec_ids -> + Context.Named.fold_outside + (fun d sec_ids -> + let id = get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/global.mli b/library/global.mli index 9db30c8ff..bf653307c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -19,9 +19,9 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool -val universes : unit -> Univ.universes +val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.named_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) @@ -73,7 +73,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/globnames.ml b/library/globnames.ml index 3ae44b2cc..bec463ecf 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -14,10 +14,10 @@ open Libnames (*s Global reference is a kernel side type for all references together *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) let isVarRef = function VarRef _ -> true | _ -> false let isConstRef = function ConstRef _ -> true | _ -> false @@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y = 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 - | VarRef v1, VarRef v2 -> Id.compare v1 v2 - - | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 - | ConstRef _, VarRef _ -> 1 - | ConstRef _, (IndRef _ | ConstructRef _) -> -1 - | IndRef _, (VarRef _ | ConstRef _) -> 1 - | IndRef _, ConstructRef _ -> -1 - | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in diff --git a/library/globnames.mli b/library/globnames.mli index f94f6216f..f4956e3df 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -13,10 +13,10 @@ open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) val isVarRef : global_reference -> bool val isConstRef : global_reference -> bool diff --git a/library/heads.ml b/library/heads.ml index 8124d3474..4c9b78976 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -15,6 +15,7 @@ open Environ open Globnames open Libobject open Lib +open Context.Named.Declaration (** Characterization of the head of a term *) @@ -63,9 +64,9 @@ let kind_of_head env t = (try on_subterm k l b (variable_head id) with Not_found -> (* a goal variable *) - match pi2 (lookup_named id env) with - | Some c -> aux k l c b - | None -> NotImmediatelyComputableHead) + 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 -> @@ -132,8 +133,8 @@ let compute_head = function | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match pi2 (Global.lookup_named id) with - | Some c when not (Decls.variable_opacity id) -> + (match Global.lookup_named id with + | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c | _ -> RigidHead (RigidVar id)) diff --git a/library/impargs.ml b/library/impargs.ml index f5f6a3eba..4e344a954 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -165,6 +165,7 @@ let update pos rig (na,st) = (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env bound depth f = + let open Context.Named.Declaration in match kind_of_term f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true @@ -173,8 +174,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - let (_, value, _) = Environ.lookup_named id env in - begin match value with None -> false | _ -> true end + Environ.lookup_named id env |> is_local_def | Ind _ | Construct _ -> false | _ -> true @@ -234,13 +234,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) = let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in + let open Context.Rel.Declaration in let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) - (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) + (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) | _ -> rigid := is_rigid_head t; let names = List.rev names in @@ -252,7 +253,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in - let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in + let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] @@ -427,7 +428,7 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = @@ -449,8 +450,8 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let (_,_,ty) = lookup_named id env in - compute_semi_auto_implicits env flags manual ty + let open Context.Named.Declaration in + compute_semi_auto_implicits env flags manual (get_type (lookup_named id env)) (* Implicits of a global reference. *) diff --git a/library/keys.ml b/library/keys.ml index 0c167494e..057dc3b65 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -12,35 +12,31 @@ open Globnames open Term open Libobject -type key = +type key = | KGlob of global_reference - | KLam + | KLam | KLet | KProd | KSort - | KEvar - | KCase - | KFix + | KCase + | KFix | KCoFix - | KRel - | KMeta + | KRel module KeyOrdered = struct type t = key let hash gr = match gr with - | KGlob gr -> 10 + RefOrdered.hash gr + | KGlob gr -> 8 + RefOrdered.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 | KSort -> 3 - | KEvar -> 4 - | KCase -> 5 - | KFix -> 6 - | KCoFix -> 7 - | KRel -> 8 - | KMeta -> 9 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 let compare gr1 gr2 = match gr1, gr2 with @@ -62,8 +58,6 @@ module Keyset = Keymap.Set (* Mapping structure for references to be considered equivalent *) -type keys = Keyset.t Keymap.t - let keys = Summary.ref Keymap.empty ~name:"Keys_decl" let add_kv k v m = @@ -153,12 +147,10 @@ let pr_key pr_global = function | KLet -> str"Let" | KProd -> str"Product" | KSort -> str"Sort" - | KEvar -> str"Evar" | KCase -> str"Case" | KFix -> str"Fix" | KCoFix -> str"CoFix" | KRel -> str"Rel" - | KMeta -> str"Meta" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) diff --git a/library/lib.ml b/library/lib.ml index e4617cafb..f8bb6bac5 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -428,8 +428,10 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = + let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> + let (id',b,t) = to_tuple decl in let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -448,7 +450,10 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx +let named_of_variable_context ctx = let open Context.Named.Declaration in + List.map (function id,_,None,t -> LocalAssum (id,t) + | id,_,Some b,t -> LocalDef (id,b,t)) + ctx let add_section_replacement f g poly hyps = match !sectab with diff --git a/library/lib.mli b/library/lib.mli index 513c48549..e2e71ac90 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -168,7 +168,7 @@ type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Context.named_context +val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info @@ -179,9 +179,9 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : Decl_kinds.polymorphic -> - Names.constant -> Context.named_context -> unit + Names.constant -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.mutual_inductive -> Context.named_context -> unit + Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) @@ -194,6 +194,6 @@ val discharge_inductive : Names.inductive -> Names.inductive (* discharging a constant in one go *) val full_replacement_context : unit -> Opaqueproof.work_list list val full_section_segment_of_constant : - Names.constant -> (Context.named_context -> Context.named_context) list + Names.constant -> (Context.Named.t -> Context.Named.t) list diff --git a/library/libnames.ml b/library/libnames.ml index a2f22b2ef..99ff2f2fb 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,7 +13,7 @@ open Names (**********************************************) -let pr_dirpath sl = (str (DirPath.to_string sl)) +let pr_dirpath sl = str (DirPath.to_string sl) (*s Operations on dirpaths *) @@ -197,7 +197,7 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> str (Id.to_string id) + | Ident (_,id) -> Id.print id let loc_of_reference = function | Qualid (loc,qid) -> loc diff --git a/library/libobject.ml b/library/libobject.ml index 706e39915..bbbb134df 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,6 +8,9 @@ open Libnames open Pp +open Util + +module Dyn = Dyn.Make(struct end) (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -70,15 +73,25 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let tag = Dyn.create na in + let (infun, outfun) = make_dyn tag in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) @@ -158,3 +171,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump diff --git a/library/libobject.mli b/library/libobject.mli index f3880a437..dbe0de8f8 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -99,7 +99,6 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string -val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit @@ -109,3 +108,7 @@ val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/library.ml b/library/library.ml index ccda57c2c..8e2402dda 100644 --- a/library/library.ml +++ b/library/library.ml @@ -132,7 +132,7 @@ let try_find_library dir = try find_library dir with Not_found -> errorlabstrm "Library.find_library" - (str "Unknown library " ++ str (DirPath.to_string dir)) + (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -285,28 +285,18 @@ let locate_absolute_library dir = with Not_found -> [] in match find ".vo" @ find ".vio" with | [] -> raise LibNotFound - | [file] -> dir, file + | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); - dir, vi - | [vo;vi] -> dir, vo + vi + | [vo;vi] -> vo | _ -> assert false let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = match root with - | None -> Loadpath.expand_path dir - | Some root -> - let filter path = - if is_dirpath_prefix_of root path then - let path = drop_dirpath_prefix root path in - is_dirpath_suffix_of dir path - else false - in - Loadpath.filter_path filter - in + let loadpath = Loadpath.expand_path ?root dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -458,7 +448,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, f)); + Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -466,6 +456,7 @@ let rec intern_library (needed, contents) (dir, f) from = try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" @@ -480,13 +471,13 @@ and intern_library_deps libs dir m from = (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (try_locate_absolute_library dir) from in + let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); libs -let rec_intern_library libs mref = - let _, libs = intern_library libs mref None in +let rec_intern_library libs (dir, f) = + let _, libs = intern_library libs (dir, Some f) None in libs let native_name_from_filename f = @@ -578,7 +569,7 @@ let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> user_err_loc - (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module") + (loc,"import_library", pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -603,7 +594,7 @@ let import_module export modl = try Declaremods.import_module export mp; aux [] l with Not_found -> user_err_loc (loc,"import_library", - str (string_of_qualid dir) ++ str " is not a module")) + pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -613,9 +604,9 @@ let import_module export modl = let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then + if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then errorlabstrm "" - (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain @@ -780,13 +771,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f' ch (proofs : seg_proofs); close_out ch -(************************************************************************) -(*s Display the memory use of a library. *) - -open Printf - -let mem s = Pp.mt () - module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) diff --git a/library/library.mli b/library/library.mli index 25c9604ce..8f5b775d8 100644 --- a/library/library.mli +++ b/library/library.mli @@ -85,8 +85,5 @@ val locate_qualified_library : *) -(** {6 Statistics: display the memory use of a library. } *) -val mem : DirPath.t -> Pp.std_ppcmds - (** {6 Native compiler. } *) val native_name_from_filename : string -> string diff --git a/library/loadpath.ml b/library/loadpath.ml index 78f8dd25f..f8169576d 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit = end | _ -> anomaly_too_many_paths phys_path -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.rev_map Id.to_string (DirPath.repr dir)) - let filter_path f = let rec aux = function | [] -> [] @@ -97,18 +93,19 @@ let filter_path f = in aux !load_paths -let expand_path dir = +let expand_path ?root dir = let rec aux = function | [] -> [] - | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> - match implicit with - | true -> - (** The path is implicit, so that we only want match the logical suffix *) - if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l - | false -> - (** Otherwise we must match exactly *) - if DirPath.equal dir lg then (ph, lg) :: aux l else aux l - in + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then is_dirpath_suffix_of dir lg + else DirPath.equal dir lg + | Some root -> + is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + if success then (ph, lg) :: aux l else aux l in aux !load_paths let locate_file fname = diff --git a/library/loadpath.mli b/library/loadpath.mli index 49ffc1148..4e79edbdc 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -42,7 +42,7 @@ val find_load_path : CUnix.physical_path -> t val is_in_load_paths : CUnix.physical_path -> bool (** Whether a physical path is currently bound. *) -val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list (** Given a relative logical path, associate the list of absolute physical and logical paths which are possible matches of it. *) diff --git a/library/nameops.ml b/library/nameops.ml index 98b417c2a..71405d024 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -12,7 +12,7 @@ open Names (* Identifiers *) -let pr_id id = str (Id.to_string id) +let pr_id id = Id.print id let pr_name = function | Anonymous -> str "_" @@ -141,7 +141,7 @@ let name_max na1 na2 = | Name _ -> na1 | Anonymous -> na2 -let pr_lab l = str (Label.to_string l) +let pr_lab l = Label.print l let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nametab.ml b/library/nametab.ml index 40acb3ae2..bbae98fc0 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -523,7 +523,7 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - try str (string_of_qualid (shortest_qualid_of_global env ref)) + try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e diff --git a/library/summary.ml b/library/summary.ml index 46c52acc4..19e7e5fd9 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,6 +10,8 @@ open Pp open Errors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -20,8 +22,19 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.create (mangle sumname) in + let tag = Dyn.create (mangle sumname) in + let (infun, outfun) = make_dyn tag in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -164,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids = List.filter (fun (id, _) -> List.mem id ids) summaries let pointer_equal l1 l2 = + let ptr_equal d1 d2 = + let Dyn.Dyn (t1, x1) = d1 in + let Dyn.Dyn (t2, x2) = d2 in + match Dyn.eq t1 t2 with + | None -> false + | Some Refl -> x1 == x2 + in CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2 + (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) @@ -176,3 +196,5 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index c24a0b4b8..27889cab2 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/universes.ml b/library/universes.ml index 3bebdafc7..c4eb2afcb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -102,6 +102,7 @@ module Constraints = struct end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -135,82 +136,76 @@ let to_constraints g s = | _, ULe, Some l' -> enforce_leq x y acc | _, ULub, _ -> acc | _, d, _ -> - let f = if d == ULe then check_leq else check_eq in + let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in if f g x y then acc else raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") in Constraints.fold tr s Constraint.empty -let eq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let eq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) -let eq_constr_univs_infer_with kind1 kind2 univs m n = +let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = (* spiwack: duplicates the code of [eq_constr_univs_infer] because I haven't find a way to factor the code without destroying pointer-equality optimisations in [eq_constr_univs_infer]. Pointer equality is not sufficient to ensure equality up to [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) - let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None -let leq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let leq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let cstrs = ref accu in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then - ((if Univ.is_type0_univ u1 then - cstrs := Constraints.add (u1, ULe, u2) !cstrs); - true) - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -220,7 +215,7 @@ let leq_constr_univs_infer univs m n = eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + if res then Some !cstrs else None let eq_constr_universes m n = if m == n then true, Constraints.empty @@ -650,14 +645,14 @@ let normalize_univ_variable_opt_subst ectx = in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - ectx := Univ.LMap.add l (Some b) !ectx; b + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - subst := Univ.LMap.add l b !subst; b in + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = @@ -869,27 +864,27 @@ let normalize_context_set ctx us algs = let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g) - ctx Univ.empty_universes + let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.empty_universes in let g = Univ.Constraint.fold (fun (l, d, r) g -> let g = if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe l false g + with UGraph.AlreadyDeclared -> g else g in let g = if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe r false g + with UGraph.AlreadyDeclared -> g else g in g) csts g in - let g = Univ.Constraint.fold Univ.enforce_constraint csts g in - Univ.constraints_of_universes g + let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + UGraph.constraints_of_universes g in let noneqs = Constraint.fold (fun (l,d,r as cstr) noneqs -> @@ -1027,7 +1022,7 @@ let refresh_constraints univs (ctx, cstrs) = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in if is_trivial_leq c then acc - else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') diff --git a/library/universes.mli b/library/universes.mli index edb06dfc5..53cf5f384 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -63,6 +63,7 @@ module Constraints : sig end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -71,11 +72,12 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function -val to_constraints : universes -> universe_constraints -> constraints +val to_constraints : UGraph.t -> universe_constraints -> constraints (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -83,12 +85,13 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_ val eq_constr_univs_infer_with : (constr -> (constr,types) kind_of_term) -> (constr -> (constr,types) kind_of_term) -> - Univ.universes -> constr -> constr -> bool universe_constrained + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) @@ -223,7 +226,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst -val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes +val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t (** Pretty-printing *) |