From 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 07:42:16 +0100 Subject: [api] Miscellaneous consolidation + moves to engine. We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. --- API/API.mli | 3 + dev/top_printers.ml | 2 +- engine/engine.mllib | 7 +- engine/evarutil.ml | 4 +- engine/geninterp.ml | 100 -------------------- engine/geninterp.mli | 72 --------------- engine/nameops.ml | 216 ++++++++++++++++++++++++++++++++++++++++++++ engine/nameops.mli | 138 ++++++++++++++++++++++++++++ engine/univops.ml | 40 ++++++++ engine/univops.mli | 15 +++ kernel/names.ml | 2 + kernel/names.mli | 1 + library/coqlib.ml | 10 +- library/declaremods.ml | 4 +- library/lib.ml | 6 +- library/libnames.ml | 10 +- library/libnames.mli | 20 +++- library/library.ml | 21 ++--- library/library.mllib | 2 - library/loadpath.ml | 6 +- library/nameops.ml | 215 ------------------------------------------- library/nameops.mli | 136 ---------------------------- library/univops.ml | 40 -------- library/univops.mli | 15 --- plugins/extraction/table.ml | 2 +- pretyping/geninterp.ml | 100 ++++++++++++++++++++ pretyping/geninterp.mli | 72 +++++++++++++++ pretyping/pretyping.mllib | 1 + printing/ppvernac.ml | 6 +- printing/prettyp.ml | 4 +- toplevel/coqinit.ml | 6 +- vernac/vernacentries.ml | 18 ++-- 32 files changed, 662 insertions(+), 632 deletions(-) delete mode 100644 engine/geninterp.ml delete mode 100644 engine/geninterp.mli create mode 100644 engine/nameops.ml create mode 100644 engine/nameops.mli create mode 100644 engine/univops.ml create mode 100644 engine/univops.mli delete mode 100644 library/nameops.ml delete mode 100644 library/nameops.mli delete mode 100644 library/univops.ml delete mode 100644 library/univops.mli create mode 100644 pretyping/geninterp.ml create mode 100644 pretyping/geninterp.mli diff --git a/API/API.mli b/API/API.mli index 86c6f14158..991dca7482 100644 --- a/API/API.mli +++ b/API/API.mli @@ -87,6 +87,7 @@ sig val repr : t -> Id.t list val equal : t -> t -> bool val to_string : t -> string + val print : t -> Pp.t end module MBId : sig @@ -1934,8 +1935,10 @@ sig val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t val dirpath_of_string : string -> Names.DirPath.t val pr_dirpath : Names.DirPath.t -> Pp.t + [@@ocaml.deprecated "Alias for DirPath.print"] val string_of_path : full_path -> string + val basename : full_path -> Names.Id.t type object_name = full_path * Names.KerName.t diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0f496d3b9f..df5f054692 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -39,7 +39,7 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) let ppid id = pp (Id.print id) let pplab l = pp (Label.print l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) -let ppdir dir = pp (pr_dirpath dir) +let ppdir dir = pp (DirPath.print dir) let ppmp mp = pp(str (ModPath.debug_to_string mp)) let ppcon con = pp(Constant.debug_print con) let ppproj con = pp(Constant.debug_print (Projection.constant con)) diff --git a/engine/engine.mllib b/engine/engine.mllib index afc02d7f6d..a3614f6c4a 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,12 +1,13 @@ -Logic_monad Universes +Univops UState +Nameops Evd EConstr Namegen Termops -Proofview_monad Evarutil +Logic_monad +Proofview_monad Proofview Ftactic -Geninterp diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df4ef2ce71..14d07ccaeb 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -11,11 +11,11 @@ open Util open Names open Term open Constr -open Termops -open Namegen open Pre_env open Environ open Evd +open Termops +open Namegen module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/engine/geninterp.ml b/engine/geninterp.ml deleted file mode 100644 index 768ef3cfd9..0000000000 --- a/engine/geninterp.ml +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a typ * 'a -> t - - let eq = ValT.eq - let repr = ValT.repr - let create = ValT.create - - let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) - - let typ_list = ValT.create "list" - let typ_opt = ValT.create "option" - let typ_pair = ValT.create "pair" - - let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with - | Base t -> Dyn (t, x) - | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x) - | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x) - | Pair (tag1, tag2) -> - Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) - -end - -module ValTMap = ValT.Map - -module ValReprObj = -struct - type ('raw, 'glb, 'top) obj = 'top Val.tag - let name = "valrepr" - let default _ = None -end - -module ValRepr = Register(ValReprObj) - -let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function -| ListArg t -> Val.List (val_tag t) -| OptArg t -> Val.Opt (val_tag t) -| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) -| ExtraArg s -> ValRepr.obj (ExtraArg s) - -let val_tag = function Topwit t -> val_tag t - -let register_val0 wit tag = - let tag = match tag with - | None -> - let name = match wit with - | ExtraArg s -> ArgT.repr s - | _ -> assert false - in - Val.Base (Val.create name) - | Some tag -> tag - in - ValRepr.register0 wit tag - -(** Interpretation functions *) - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -module InterpObj = -struct - type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun - let name = "interp" - let default _ = None -end - -module Interp = Register(InterpObj) - -let interp = Interp.obj - -let register_interp0 = Interp.register0 diff --git a/engine/geninterp.mli b/engine/geninterp.mli deleted file mode 100644 index ae0b26e594..0000000000 --- a/engine/geninterp.mli +++ /dev/null @@ -1,72 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a typ - - type _ tag = - | Base : 'a typ -> 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a typ * 'a -> t - - val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option - val repr : 'a typ -> string - val pr : 'a typ -> Pp.t - - val typ_list : t list typ - val typ_opt : t option typ - val typ_pair : (t * t) typ - - val inject : 'a tag -> 'a -> t - -end - -module ValTMap (M : Dyn.TParam) : - Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ - -(** Dynamic types for toplevel values. While the generic types permit to relate - objects at various levels of interpretation, toplevel values are wearing - their own type regardless of where they came from. This allows to use the - same runtime representation for several generic types. *) - -val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag -(** Retrieve the dynamic type associated to a toplevel genarg. *) - -val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit -(** Register the representation of a generic argument. If no tag is given as - argument, a new fresh tag with the same name as the argument is associated - to the generic type. *) - -(** {6 Interpretation functions} *) - -module TacStore : Store.S - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun - -val register_interp0 : - ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/engine/nameops.ml b/engine/nameops.ml new file mode 100644 index 0000000000..5105d7becc --- /dev/null +++ b/engine/nameops.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let c = Char.code (String.get sa (String.length sa -1)) in + let s = + if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) + else sa ^ "_" ^ (string_of_int n) in + Id.of_string s + | None -> Id.of_string sa + +let root_of_id id = + let suffixstart = cut_ident true id in + Id.of_string (String.sub (Id.to_string id) 0 suffixstart) + +(* Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + [bar0] ↦ [bar1] + [bar00] ↦ [bar01] + [bar1] ↦ [bar2] + [bar01] ↦ [bar01] + [bar9] ↦ [bar10] + [bar09] ↦ [bar10] + [bar99] ↦ [bar100] +*) +let increment_subscript id = + let id = Id.to_string id in + let len = String.length id in + let rec add carrypos = + let c = id.[carrypos] in + if is_digit c then + if Int.equal (Char.code c) (Char.code '9') then begin + assert (carrypos>0); + add (carrypos-1) + end + else begin + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); + newid + end + else begin + let newid = Bytes.of_string (id^"0") in + if carrypos < len-1 then begin + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' + end; + newid + end + in Id.of_bytes (add (len-1)) + +let has_subscript id = + let id = Id.to_string id in + is_digit (id.[String.length id - 1]) + +let forget_subscript id = + let numstart = cut_ident false id in + let newid = Bytes.make (numstart+1) '0' in + String.blit (Id.to_string id) 0 newid 0 numstart; + (Id.of_bytes newid) + +let add_suffix id s = Id.of_string (Id.to_string id ^ s) +let add_prefix s id = Id.of_string (s ^ Id.to_string id) + +let atompart_of_id id = fst (repr_ident id) + +(* Names *) + +module type ExtName = +sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a + val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a + val iter : (Id.t -> unit) -> t -> unit + val map : (Id.t -> Id.t) -> t -> t + val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t + val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a + val get_id : t -> Id.t + val pick : t -> t -> t + val cons : t -> Id.t list -> Id.t list + val to_option : Name.t -> Id.t option + +end + +module Name : ExtName = +struct + + include Names.Name + + exception IsAnonymous + + let fold_left f a = function + | Name id -> f a id + | Anonymous -> a + + let fold_right f na a = + match na with + | Name id -> f id a + | Anonymous -> a + + let iter f na = fold_right (fun x () -> f x) na () + + let map f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + + let fold_left_map f a = function + | Name id -> let (a, id) = f a id in (a, Name id) + | Anonymous -> a, Anonymous + + let fold_right_map f na a = match na with + | Name id -> let (id, a) = f id a in (Name id, a) + | Anonymous -> Anonymous, a + + let get_id = function + | Name id -> id + | Anonymous -> raise IsAnonymous + + let pick na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + + let cons na l = + match na with + | Anonymous -> l + | Name id -> id::l + + let to_option = function + | Anonymous -> None + | Name id -> Some id + +end + +open Name + +(* Compatibility *) +let out_name = get_id +let name_fold = fold_right +let name_iter = iter +let name_app = map +let name_fold_map = fold_left_map +let name_cons = cons +let name_max = pick +let pr_name = print + +let pr_lab l = Label.print l + +(* Metavariables *) +let pr_meta = Pp.int +let string_of_meta = string_of_int + +(* Deprecated *) +open Libnames +let default_library = default_library +let coq_string = coq_string +let coq_root = coq_root +let default_root_prefix = default_root_prefix + diff --git a/engine/nameops.mli b/engine/nameops.mli new file mode 100644 index 0000000000..0fec8a925d --- /dev/null +++ b/engine/nameops.mli @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* int option -> Id.t +val repr_ident : Id.t -> string * int option + +val atompart_of_id : Id.t -> string (** remove trailing digits *) +val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) + +val add_suffix : Id.t -> string -> Id.t +val add_prefix : string -> Id.t -> Id.t + +(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) + +val has_subscript : Id.t -> bool + +val increment_subscript : Id.t -> Id.t +(** Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + + [bar0] ↦ [bar1] + + [bar00] ↦ [bar01] + + [bar1] ↦ [bar2] + + [bar01] ↦ [bar01] + + [bar9] ↦ [bar10] + + [bar09] ↦ [bar10] + + [bar99] ↦ [bar100] +*) + +val forget_subscript : Id.t -> Id.t + +module Name : sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a + (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) + + val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) + + val iter : (Id.t -> unit) -> Name.t -> unit + (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) + + val map : (Id.t -> Id.t) -> Name.t -> t + (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) + + val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t + (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. + It is [a,Anonymous] otherwise. *) + + val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a + (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')]. + It is [Anonymous,a] otherwise. *) + + val get_id : Name.t -> Id.t + (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) + + val pick : Name.t -> Name.t -> Name.t + (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. + Pick one of [na] or [na'] otherwise. *) + + val cons : Name.t -> Id.t list -> Id.t list + (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) + + val to_option : Name.t -> Id.t option + (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) + +end + +(** Metavariables *) +val pr_meta : Constr.metavariable -> Pp.t +val string_of_meta : Constr.metavariable -> string + +val out_name : Name.t -> Id.t +[@@ocaml.deprecated "Same as [Name.get_id]"] + +val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +[@@ocaml.deprecated "Same as [Name.fold_right]"] + +val name_iter : (Id.t -> unit) -> Name.t -> unit +[@@ocaml.deprecated "Same as [Name.iter]"] + +val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +[@@ocaml.deprecated "Same as [Name.map]"] + +val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t +[@@ocaml.deprecated "Same as [Name.fold_left_map]"] + +val name_max : Name.t -> Name.t -> Name.t +[@@ocaml.deprecated "Same as [Name.pick]"] + +val name_cons : Name.t -> Id.t list -> Id.t list +[@@ocaml.deprecated "Same as [Name.cons]"] + +val pr_name : Name.t -> Pp.t +[@@ocaml.deprecated "Same as [Name.print]"] + +val pr_id : Id.t -> Pp.t +[@@ocaml.deprecated "Same as [Names.Id.print]"] + +val pr_lab : Label.t -> Pp.t +[@@ocaml.deprecated "Same as [Names.Label.print]"] + +(** Deprecated stuff to libnames *) +val default_library : DirPath.t +[@@ocaml.deprecated "Same as [Libnames.default_library]"] + +val coq_root : module_ident (** "Coq" *) +[@@ocaml.deprecated "Same as [Libnames.coq_root]"] + +val coq_string : string (** "Coq" *) +[@@ocaml.deprecated "Same as [Libnames.coq_string]"] + +val default_root_prefix : DirPath.t +[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"] + diff --git a/engine/univops.ml b/engine/univops.ml new file mode 100644 index 0000000000..9dc138eb8d --- /dev/null +++ b/engine/univops.ml @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Term.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/engine/univops.mli b/engine/univops.mli new file mode 100644 index 0000000000..9af568bcb3 --- /dev/null +++ b/engine/univops.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* LSet.t +val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/kernel/names.ml b/kernel/names.ml index cb27104d15..b02c0b8409 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -179,6 +179,8 @@ struct | [] -> "<>" | sl -> String.concat "." (List.rev_map Id.to_string sl) + let print dp = str (to_string dp) + let initial = [default_module_name] module Hdir = Hashcons.Hlist(Id) diff --git a/kernel/names.mli b/kernel/names.mli index ba0637c8a0..709ebeb7fd 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -159,6 +159,7 @@ sig val hcons : t -> t (** Hashconsing of directory paths. *) + val print : t -> Pp.t end (** {6 Names of structure elements } *) diff --git a/library/coqlib.ml b/library/coqlib.ml index 141fff0335..4a23909858 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,7 @@ open Libnames open Globnames open Nametab -let coq = Nameops.coq_string (* "Coq" *) +let coq = Libnames.coq_string (* "Coq" *) (************************************************************************) (* Generic functions to find Coq objects *) @@ -32,7 +32,7 @@ let find_reference locstr dir s = of not found errors here *) user_err ~hdr:locstr Pp.(str "cannot find " ++ Libnames.pr_path sp ++ - str "; maybe library " ++ Libnames.pr_dirpath dp ++ + str "; maybe library " ++ DirPath.print dp ++ str " has to be required first.") let coq_reference locstr dir s = find_reference locstr (coq::dir) s @@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s = | [] -> anomaly ~label:locstr (str "cannot find " ++ str s ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") + prlist_with_sep pr_comma DirPath.print dirs ++ str ".") | l -> anomaly ~label:locstr (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") + prlist_with_sep pr_comma DirPath.print dirs ++ str ".") (* For tactics/commands requiring vernacular libraries *) @@ -79,7 +79,7 @@ let check_required_library d = *) (* or failing ...*) user_err ~hdr:"Coqlib.check_required_library" - (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") + (str "Library " ++ DirPath.print dir ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/library/declaremods.ml b/library/declaremods.ml index cda40f49f1..db83dafef8 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -167,13 +167,13 @@ let consistency_checks exists dir dirinfo = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> user_err ~hdr:"consistency_checks" - (pr_dirpath dir ++ str " should already exist!") + (DirPath.print dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then user_err ~hdr:"consistency_checks" - (pr_dirpath dir ++ str " already exists") + (DirPath.print dir ++ str " already exists") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i diff --git a/library/lib.ml b/library/lib.ml index 36292d367e..6abbf7ef9b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -12,7 +12,7 @@ open Util open Names open Libnames open Globnames -open Nameops +(* open Nameops *) open Libobject open Context.Named.Declaration @@ -361,8 +361,8 @@ let end_compilation_checks dir = | None -> anomaly (Pp.str "There should be a module name...") | Some m -> if not (Names.DirPath.equal m dir) then anomaly - (str "The current open module has name" ++ spc () ++ pr_dirpath m ++ - spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str "."); + (str "The current open module has name" ++ spc () ++ DirPath.print m ++ + spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); in oname diff --git a/library/libnames.ml b/library/libnames.ml index efb1348ab2..81878e72f9 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 = DirPath.print sl (*s Operations on dirpaths *) @@ -232,6 +232,14 @@ let join_reference ns r = Qualid (loc, make_qualid (dirpath_of_string (Names.Id.to_string id1)) id2) +(* Default paths *) +let default_library = Names.DirPath.initial (* = ["Top"] *) + +(*s Roots of the space of absolute names *) +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 diff --git a/library/libnames.mli b/library/libnames.mli index ab25853346..ed01163ee7 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -11,12 +11,13 @@ open Loc open Names (** {6 Dirpaths } *) -(** FIXME: ought to be in Names.dir_path *) +val dirpath_of_string : string -> DirPath.t val pr_dirpath : DirPath.t -> Pp.t +[@@ocaml.deprecated "Alias for DirPath.print"] -val dirpath_of_string : string -> DirPath.t 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 @@ -127,7 +128,20 @@ val pr_reference : reference -> Pp.t val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference -(** Deprecated synonyms *) +(** some preset paths *) +val default_library : DirPath.t + +(** This is the root of the standard library of Coq *) +val coq_root : module_ident (** "Coq" *) +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/library.ml b/library/library.ml index 99ef66699f..88470d121b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -12,9 +12,8 @@ open Util open Names open Libnames -open Nameops -open Libobject open Lib +open Libobject (************************************************************************) (*s Low-level interning/externing of libraries to files *) @@ -132,7 +131,7 @@ let try_find_library dir = try find_library dir with Not_found -> user_err ~hdr:"Library.find_library" - (str "Unknown library " ++ pr_dirpath dir) + (str "Unknown library " ++ DirPath.print dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -331,7 +330,7 @@ let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) + str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) let error_lib_not_found qid = user_err ~hdr:"load_absolute_library_from" @@ -465,8 +464,8 @@ let rec intern_library (needed, contents) (dir, f) from = if not (DirPath.equal dir m.library_name) then user_err ~hdr:"load_physical_library" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ - spc() ++ pr_dirpath dir); + DirPath.print m.library_name ++ spc () ++ str "and not library" ++ + spc() ++ DirPath.print dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); m.library_digests, intern_library_deps (needed, contents) dir m f @@ -477,9 +476,9 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err (str "Compiled library " ++ pr_dirpath caller ++ + user_err (str "Compiled library " ++ DirPath.print caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ - over library " ++ pr_dirpath dir); + over library " ++ DirPath.print dir); libs let rec_intern_library libs (dir, f) = @@ -617,7 +616,7 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then user_err - (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ Id.print id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") let start_library fo = @@ -625,7 +624,7 @@ let start_library fo = try let lp = Loadpath.find_load_path (Filename.dirname fo) in Loadpath.logical lp - with Not_found -> Nameops.default_root_prefix + with Not_found -> Libnames.default_root_prefix in let file = Filename.chop_extension (Filename.basename fo) in let id = Id.of_string file in @@ -665,7 +664,7 @@ let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = user_err - (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ + (strbrk "Unable to use logical name " ++ DirPath.print dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") diff --git a/library/library.mllib b/library/library.mllib index d94fc22919..e43bfb5a1f 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,5 +1,3 @@ -Univops -Nameops Libnames Globnames Libobject diff --git a/library/loadpath.ml b/library/loadpath.ml index 757e972b1a..eb6dae84aa 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -54,8 +54,8 @@ let warn_overriding_logical_loadpath = CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" (fun (phys_path, old_path, coq_path) -> str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath old_path ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path) + DirPath.print old_path ++ strbrk "; it is remapped to " ++ + DirPath.print coq_path) let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in @@ -75,7 +75,7 @@ let add_load_path phys_path coq_path ~implicit = else let () = (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Nameops.default_root_prefix) then + if not (DirPath.equal old_path Libnames.default_root_prefix) then warn_overriding_logical_loadpath (phys_path, old_path, coq_path) in true in diff --git a/library/nameops.ml b/library/nameops.ml deleted file mode 100644 index d598a63b8d..0000000000 --- a/library/nameops.ml +++ /dev/null @@ -1,215 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let c = Char.code (String.get sa (String.length sa -1)) in - let s = - if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) - else sa ^ "_" ^ (string_of_int n) in - Id.of_string s - | None -> Id.of_string sa - -let root_of_id id = - let suffixstart = cut_ident true id in - Id.of_string (String.sub (Id.to_string id) 0 suffixstart) - -(* Return the same identifier as the original one but whose {i subscript} is incremented. - If the original identifier does not have a suffix, [0] is appended to it. - - Example mappings: - - [bar] ↦ [bar0] - [bar0] ↦ [bar1] - [bar00] ↦ [bar01] - [bar1] ↦ [bar2] - [bar01] ↦ [bar01] - [bar9] ↦ [bar10] - [bar09] ↦ [bar10] - [bar99] ↦ [bar100] -*) -let increment_subscript id = - let id = Id.to_string id in - let len = String.length id in - let rec add carrypos = - let c = id.[carrypos] in - if is_digit c then - if Int.equal (Char.code c) (Char.code '9') then begin - assert (carrypos>0); - add (carrypos-1) - end - else begin - let newid = Bytes.of_string id in - Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; - Bytes.set newid carrypos (Char.chr (Char.code c + 1)); - newid - end - else begin - let newid = Bytes.of_string (id^"0") in - if carrypos < len-1 then begin - Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; - Bytes.set newid (carrypos+1) '1' - end; - newid - end - in Id.of_bytes (add (len-1)) - -let has_subscript id = - let id = Id.to_string id in - is_digit (id.[String.length id - 1]) - -let forget_subscript id = - let numstart = cut_ident false id in - let newid = Bytes.make (numstart+1) '0' in - String.blit (Id.to_string id) 0 newid 0 numstart; - (Id.of_bytes newid) - -let add_suffix id s = Id.of_string (Id.to_string id ^ s) -let add_prefix s id = Id.of_string (s ^ Id.to_string id) - -let atompart_of_id id = fst (repr_ident id) - -(* Names *) - -module type ExtName = -sig - - include module type of struct include Names.Name end - - exception IsAnonymous - - val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a - val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a - val iter : (Id.t -> unit) -> t -> unit - val map : (Id.t -> Id.t) -> t -> t - val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t - val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a - val get_id : t -> Id.t - val pick : t -> t -> t - val cons : t -> Id.t list -> Id.t list - val to_option : Name.t -> Id.t option - -end - -module Name : ExtName = -struct - - include Names.Name - - exception IsAnonymous - - let fold_left f a = function - | Name id -> f a id - | Anonymous -> a - - let fold_right f na a = - match na with - | Name id -> f id a - | Anonymous -> a - - let iter f na = fold_right (fun x () -> f x) na () - - let map f = function - | Name id -> Name (f id) - | Anonymous -> Anonymous - - let fold_left_map f a = function - | Name id -> let (a, id) = f a id in (a, Name id) - | Anonymous -> a, Anonymous - - let fold_right_map f na a = match na with - | Name id -> let (id, a) = f id a in (Name id, a) - | Anonymous -> Anonymous, a - - let get_id = function - | Name id -> id - | Anonymous -> raise IsAnonymous - - let pick na1 na2 = - match na1 with - | Name _ -> na1 - | Anonymous -> na2 - - let cons na l = - match na with - | Anonymous -> l - | Name id -> id::l - - let to_option = function - | Anonymous -> None - | Name id -> Some id - -end - -open Name - -(* Compatibility *) -let out_name = get_id -let name_fold = fold_right -let name_iter = iter -let name_app = map -let name_fold_map = fold_left_map -let name_cons = cons -let name_max = pick -let pr_name = print - -let pr_lab l = Label.print l - -let default_library = Names.DirPath.initial (* = ["Top"] *) - -(*s Roots of the space of absolute names *) -let coq_string = "Coq" -let coq_root = Id.of_string coq_string -let default_root_prefix = DirPath.empty - -(* Metavariables *) -let pr_meta = Pp.int -let string_of_meta = string_of_int diff --git a/library/nameops.mli b/library/nameops.mli deleted file mode 100644 index 60e5a90bb5..0000000000 --- a/library/nameops.mli +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int option -> Id.t -val repr_ident : Id.t -> string * int option - -val atompart_of_id : Id.t -> string (** remove trailing digits *) -val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) - -val add_suffix : Id.t -> string -> Id.t -val add_prefix : string -> Id.t -> Id.t - -(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) - -val has_subscript : Id.t -> bool - -val increment_subscript : Id.t -> Id.t -(** Return the same identifier as the original one but whose {i subscript} is incremented. - If the original identifier does not have a suffix, [0] is appended to it. - - Example mappings: - - [bar] ↦ [bar0] - - [bar0] ↦ [bar1] - - [bar00] ↦ [bar01] - - [bar1] ↦ [bar2] - - [bar01] ↦ [bar01] - - [bar9] ↦ [bar10] - - [bar09] ↦ [bar10] - - [bar99] ↦ [bar100] -*) - -val forget_subscript : Id.t -> Id.t - -module Name : sig - - include module type of struct include Names.Name end - - exception IsAnonymous - - val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a - (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) - - val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a - (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) - - val iter : (Id.t -> unit) -> Name.t -> unit - (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) - - val map : (Id.t -> Id.t) -> Name.t -> t - (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) - - val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. - It is [a,Anonymous] otherwise. *) - - val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a - (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')]. - It is [Anonymous,a] otherwise. *) - - val get_id : Name.t -> Id.t - (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) - - val pick : Name.t -> Name.t -> Name.t - (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. - Pick one of [na] or [na'] otherwise. *) - - val cons : Name.t -> Id.t list -> Id.t list - (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) - - val to_option : Name.t -> Id.t option - (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) - -end - -val out_name : Name.t -> Id.t -[@@ocaml.deprecated "Same as [Name.get_id]"] - -val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a -[@@ocaml.deprecated "Same as [Name.fold_right]"] - -val name_iter : (Id.t -> unit) -> Name.t -> unit -[@@ocaml.deprecated "Same as [Name.iter]"] - -val name_app : (Id.t -> Id.t) -> Name.t -> Name.t -[@@ocaml.deprecated "Same as [Name.map]"] - -val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t -[@@ocaml.deprecated "Same as [Name.fold_left_map]"] - -val name_max : Name.t -> Name.t -> Name.t -[@@ocaml.deprecated "Same as [Name.pick]"] - -val name_cons : Name.t -> Id.t list -> Id.t list -[@@ocaml.deprecated "Same as [Name.cons]"] - -val pr_name : Name.t -> Pp.t -[@@ocaml.deprecated "Same as [Name.print]"] - -val pr_id : Id.t -> Pp.t -[@@ocaml.deprecated "Same as [Names.Id.print]"] - -val pr_lab : Label.t -> Pp.t -[@@ocaml.deprecated "Same as [Names.Label.print]"] - -(** some preset paths *) - -val default_library : DirPath.t - -(** This is the root of the standard library of Coq *) -val coq_root : module_ident (** "Coq" *) -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 - -(** Metavariables *) -val pr_meta : Constr.metavariable -> Pp.t -val string_of_meta : Constr.metavariable -> string diff --git a/library/univops.ml b/library/univops.ml deleted file mode 100644 index 9dc138eb8d..0000000000 --- a/library/univops.ml +++ /dev/null @@ -1,40 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = Term.univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> Constr.fold aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty diff --git a/library/univops.mli b/library/univops.mli deleted file mode 100644 index 9af568bcb3..0000000000 --- a/library/univops.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* LSet.t -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 995d5fd19d..5903733a66 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str "Please load library " ++ pr_dirpath dp ++ str " first.") + err (str "Please load library " ++ DirPath.print dp ++ str " first.") | _ -> () end | _ -> () diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml new file mode 100644 index 0000000000..768ef3cfd9 --- /dev/null +++ b/pretyping/geninterp.ml @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + let eq = ValT.eq + let repr = ValT.repr + let create = ValT.create + + let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) + + let typ_list = ValT.create "list" + let typ_opt = ValT.create "option" + let typ_pair = ValT.create "pair" + + let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with + | Base t -> Dyn (t, x) + | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) + +end + +module ValTMap = ValT.Map + +module ValReprObj = +struct + type ('raw, 'glb, 'top) obj = 'top Val.tag + let name = "valrepr" + let default _ = None +end + +module ValRepr = Register(ValReprObj) + +let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function +| ListArg t -> Val.List (val_tag t) +| OptArg t -> Val.Opt (val_tag t) +| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) +| ExtraArg s -> ValRepr.obj (ExtraArg s) + +let val_tag = function Topwit t -> val_tag t + +let register_val0 wit tag = + let tag = match tag with + | None -> + let name = match wit with + | ExtraArg s -> ArgT.repr s + | _ -> assert false + in + Val.Base (Val.create name) + | Some tag -> tag + in + ValRepr.register0 wit tag + +(** Interpretation functions *) + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +module InterpObj = +struct + type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun + let name = "interp" + let default _ = None +end + +module Interp = Register(InterpObj) + +let interp = Interp.obj + +let register_interp0 = Interp.register0 diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli new file mode 100644 index 0000000000..ae0b26e594 --- /dev/null +++ b/pretyping/geninterp.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option + val repr : 'a typ -> string + val pr : 'a typ -> Pp.t + + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ + + val inject : 'a tag -> 'a -> t + +end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + +(** Dynamic types for toplevel values. While the generic types permit to relate + objects at various levels of interpretation, toplevel values are wearing + their own type regardless of where they came from. This allows to use the + same runtime representation for several generic types. *) + +val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag +(** Retrieve the dynamic type associated to a toplevel genarg. *) + +val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit +(** Register the representation of a generic argument. If no tag is given as + argument, a new fresh tag with the same name as the argument is associated + to the generic type. *) + +(** {6 Interpretation functions} *) + +module TacStore : Store.S + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 9904b73540..1da5b4567f 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Geninterp Ltac_pretype Locusops Pretype_errors diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 143f9ddcc5..e897b19387 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -447,7 +447,7 @@ open Decl_kinds | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> - keyword "Print LoadPath" ++ pr_opt pr_dirpath dir + keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> keyword "Print Modules" | PrintMLLoadPath -> @@ -518,7 +518,7 @@ open Decl_kinds in keyword cmd ++ spc() ++ pr_smart_global qid | PrintNamespace dp -> - keyword "Print Namespace" ++ pr_dirpath dp + keyword "Print Namespace" ++ DirPath.print dp | PrintStrategy None -> keyword "Print Strategies" | PrintStrategy (Some qid) -> @@ -964,7 +964,7 @@ open Decl_kinds keyword "LoadPath" ++ spc() ++ qs s ++ (match d with | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ pr_dirpath dir)) + | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) ) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e2d23ce7b0..060cf6fc76 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -366,7 +366,7 @@ let pr_located_qualid = function | DirModule (dir,_) -> "Module", dir | DirClosedSection dir -> "Closed Section", dir in - str s ++ spc () ++ pr_dirpath dir + str s ++ spc () ++ DirPath.print dir | ModuleType mp -> str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) | Other (obj, info) -> info.name obj @@ -647,7 +647,7 @@ let gallina_print_library_entry env sigma with_values ent = | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> - Some (str " >>>>>>> Library " ++ pr_dirpath dir) + Some (str " >>>>>>> Library " ++ DirPath.print dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index c808992887..3a195c1df0 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -65,7 +65,7 @@ let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml = let add_userlib_path ~unix_path = Mltop.add_rec_path Mltop.AddRecML ~unix_path - ~coq_root:Nameops.default_root_prefix ~implicit:false + ~coq_root:Libnames.default_root_prefix ~implicit:false (* Options -I, -I-as, and -R of the command line *) let includes = ref [] @@ -80,7 +80,7 @@ let init_load_path ~load_init = let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in let coqpath = Envars.coqpath in - let coq_root = Names.DirPath.make [Nameops.coq_root] in + let coq_root = Names.DirPath.make [Libnames.coq_root] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) if Coq_config.local then @@ -105,7 +105,7 @@ let init_load_path ~load_init = List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath; (* then current directory (not recursively!) *) Mltop.add_ml_dir "."; - Loadpath.add_load_path "." Nameops.default_root_prefix ~implicit:false; + Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false; (* additional loadpath, given with options -Q and -R *) List.iter (fun (unix_path, coq_root, implicit) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 10c139e5ab..6191f37080 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -152,7 +152,7 @@ let show_match id = (* "Print" commands *) let print_path_entry p = - let dir = pr_dirpath (Loadpath.logical p) in + let dir = DirPath.print (Loadpath.logical p) in let path = str (Loadpath.physical p) in Pp.hov 2 (dir ++ spc () ++ path) @@ -175,9 +175,9 @@ let print_modules () = let loaded_opened = List.intersect DirPath.equal opened loaded and only_loaded = List.subtract DirPath.equal loaded opened in str"Loaded and imported library files: " ++ - pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ + pr_vertical_list DirPath.print loaded_opened ++ fnl () ++ str"Loaded and not imported library files: " ++ - pr_vertical_list pr_dirpath only_loaded + pr_vertical_list DirPath.print only_loaded let print_module r = @@ -361,29 +361,29 @@ let locate_file f = let msg_found_library = function | Library.LibLoaded, fulldir, file -> Feedback.msg_info (hov 0 - (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++ + (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file)) | Library.LibInPath, fulldir, file -> Feedback.msg_info (hov 0 - (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) + (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)) let err_unmapped_library ?loc ?from qid = let dir = fst (repr_qualid qid) in let prefix = match from with | None -> str "." | Some from -> - str " and prefix " ++ pr_dirpath from ++ str "." + str " and prefix " ++ DirPath.print from ++ str "." in user_err ?loc ~hdr:"locate_library" (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ - pr_dirpath dir ++ prefix) + DirPath.print dir ++ prefix) let err_notfound_library ?loc ?from qid = let prefix = match from with | None -> str "." | Some from -> - str " with prefix " ++ pr_dirpath from ++ str "." + str " with prefix " ++ DirPath.print from ++ str "." in user_err ?loc ~hdr:"locate_library" (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) @@ -893,7 +893,7 @@ let expand filename = let vernac_add_loadpath implicit pdir ldiropt = let pdir = expand pdir in - let alias = Option.default Nameops.default_root_prefix ldiropt in + let alias = Option.default Libnames.default_root_prefix ldiropt in Mltop.add_rec_path Mltop.AddTopML ~unix_path:pdir ~coq_root:alias ~implicit let vernac_remove_loadpath path = -- cgit v1.2.3