From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 01:14:28 +0100 Subject: [api] Remove deprecated objects in engine / interp / library --- library/globnames.ml | 2 -- library/globnames.mli | 4 ---- library/libnames.ml | 9 --------- library/libnames.mli | 13 ------------- library/summary.ml | 44 -------------------------------------------- library/summary.mli | 20 -------------------- 6 files changed, 92 deletions(-) (limited to 'library') diff --git a/library/globnames.ml b/library/globnames.ml index 6b78d12ba..6383a1f8f 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -87,8 +87,6 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -let reference_of_constr = global_of_constr - let global_eq_gen eq_cst eq_ind eq_cons x y = x == y || match x, y with diff --git a/library/globnames.mli b/library/globnames.mli index 2fe35ebcc..15fcd5bdd 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -49,10 +49,6 @@ val printable_constr_of_global : GlobRef.t -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t -(** Obsolete synonyms for constr_of_global and global_of_constr *) -val reference_of_constr : constr -> GlobRef.t -[@@ocaml.deprecated "Alias of Globnames.global_of_constr"] - module RefOrdered : sig type t = GlobRef.t val compare : t -> t -> int diff --git a/library/libnames.ml b/library/libnames.ml index 4ceea480d..8d5a02a29 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -15,8 +15,6 @@ open Names (**********************************************) -let pr_dirpath sl = DirPath.print sl - (*s Operations on dirpaths *) let split_dirpath d = match DirPath.repr d with @@ -80,8 +78,6 @@ let dirpath_of_string s = in DirPath.make path -let string_of_dirpath = Names.DirPath.to_string - module Dirset = Set.Make(DirPath) module Dirmap = Map.Make(DirPath) @@ -240,8 +236,3 @@ let default_library = Names.DirPath.initial (* = ["Top"] *) let coq_string = "Coq" let coq_root = Id.of_string coq_string let default_root_prefix = DirPath.empty - -(* Deprecated synonyms *) - -let make_short_qualid = qualid_of_ident -let qualid_of_sp = qualid_of_path diff --git a/library/libnames.mli b/library/libnames.mli index 81e5bc5b1..5f69b1f0f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -14,12 +14,6 @@ open Names (** {6 Dirpaths } *) val dirpath_of_string : string -> DirPath.t -val pr_dirpath : DirPath.t -> Pp.t -[@@ocaml.deprecated "Alias for DirPath.print"] - -val string_of_dirpath : DirPath.t -> string -[@@ocaml.deprecated "Alias for DirPath.to_string"] - (** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *) val pop_dirpath : DirPath.t -> DirPath.t @@ -155,10 +149,3 @@ val coq_string : string (** "Coq" *) (** This is the default root prefix for developments which doesn't mention a root *) val default_root_prefix : DirPath.t - -(** Deprecated synonyms *) -val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *) -[@@ocaml.deprecated "Alias for qualid_of_ident"] - -val qualid_of_sp : full_path -> qualid (** = qualid_of_path *) -[@@ocaml.deprecated "Alias for qualid_of_sp"] diff --git a/library/summary.ml b/library/summary.ml index 7ef19fbfb..9b2294591 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -75,20 +75,6 @@ let freeze_summaries ~marshallable : frozen = ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod; } -let unfreeze_single name state = - let decl = - try String.Map.find name !sum_map - with - | Not_found -> - CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name) - in - try decl.unfreeze_function state - with e when CErrors.noncritical e -> - let e = CErrors.push e in - Feedback.msg_warning - Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); - iraise e - let warn_summary_out_of_scope = let name = "summary-out-of-scope" in let category = "dev" in @@ -142,36 +128,6 @@ let remove_from_summary st tag = let summaries = String.Map.remove id st.summaries in {st with summaries} -(** Selective freeze *) - -type frozen_bits = Dyn.t String.Map.t - -let freeze_summary ~marshallable ?(complement=false) ids = - let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in - String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map - -let unfreeze_summary = String.Map.iter unfreeze_single - -let surgery_summary { summaries; ml_module } bits = - let summaries = - String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in - { summaries; ml_module } - -let project_summary { summaries; ml_module } ?(complement=false) ids = - String.Map.filter (fun name _ -> complement <> List.(mem name 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 - let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in - CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 - (** All-in-one reference declaration + registration *) let ref_tag ?(freeze=fun _ r -> r) ~name x = diff --git a/library/summary.mli b/library/summary.mli index ed6c26b19..7d91a7918 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -91,25 +91,5 @@ val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen val project_from_summary : frozen -> 'a Dyn.tag -> 'a val remove_from_summary : frozen -> 'a Dyn.tag -> frozen -(** The type [frozen_bits] is a snapshot of some of the registered - tables. It is DEPRECATED in favor of the typed projection - version. *) - -type frozen_bits -[@@ocaml.deprecated "Please use the typed version of summary projection"] - -[@@@ocaml.warning "-3"] -val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits -[@@ocaml.deprecated "Please use the typed version of summary projection"] -val unfreeze_summary : frozen_bits -> unit -[@@ocaml.deprecated "Please use the typed version of summary projection"] -val surgery_summary : frozen -> frozen_bits -> frozen -[@@ocaml.deprecated "Please use the typed version of summary projection"] -val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits -[@@ocaml.deprecated "Please use the typed version of summary projection"] -val pointer_equal : frozen_bits -> frozen_bits -> bool -[@@ocaml.deprecated "Please use the typed version of summary projection"] -[@@@ocaml.warning "+3"] - (** {6 Debug} *) val dump : unit -> (int * string) list -- cgit v1.2.3