diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 92 |
1 files changed, 46 insertions, 46 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 1eb9a317..a3aa71f2 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting @@ -34,33 +36,28 @@ struct let hash = String.hash - let warn_invalid_identifier = - CWarnings.create ~name:"invalid-identifier" ~category:"parsing" - ~default:CWarnings.Disabled - (fun s -> str s) - - let check_soft ?(warn = true) x = - let iter (fatal, x) = - if fatal then CErrors.error x else - if warn then warn_invalid_identifier x - in + let check_valid ?(strict=true) x = + let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in Option.iter iter (Unicode.ident_refutation x) let is_valid s = match Unicode.ident_refutation s with | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_valid s; + String.hcons s + let of_string s = - let () = check_soft s in - let s = String.copy s in + let () = check_valid s in String.hcons s let of_string_soft s = - let () = check_soft ~warn:false s in - let s = String.copy s in + let () = check_valid ~strict:false s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id @@ -88,11 +85,14 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false - let is_name = not % is_anonymous + let is_name = is_anonymous %> not let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -106,13 +106,16 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = Id.t -> Id.t let hashcons hident = function | Name id -> Name (hident id) @@ -156,21 +159,8 @@ module DirPath = struct type t = module_ident list - let rec compare (p1 : t) (p2 : t) = - if p1 == p2 then 0 - else begin match p1, p2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | id1 :: p1, id2 :: p2 -> - let c = Id.compare id1 id2 in - if Int.equal c 0 then compare p1 p2 else c - end - - let rec equal p1 p2 = p1 == p2 || match p1, p2 with - | [], [] -> true - | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2 - | _ -> false + let compare = List.compare Id.compare + let equal = List.equal Id.equal let rec hash accu = function | [] -> accu @@ -185,12 +175,14 @@ struct let empty = [] - let is_empty d = match d with [] -> true | _ -> false + let is_empty = List.is_empty let to_string = function | [] -> "<>" | 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) @@ -247,8 +239,7 @@ struct module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = @@ -549,7 +540,6 @@ module KerPair = struct end module SyntacticOrd = struct - type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -601,7 +591,13 @@ end module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "canonical form" of the constant. *) + module Cmap_env = HMap.Make(Constant.UserOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) + module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Cmap.Set module Cset_env = Cmap_env.Set @@ -705,6 +701,12 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) +type global_reference = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** 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. *) + (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of Id.t @@ -866,7 +868,6 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c module SyntacticOrd = struct - type t = constant * bool let compare (c, b) (c', b') = if b = b' then Constant.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = @@ -876,8 +877,7 @@ struct module Self_Hashcons = struct - type _t = t - type t = _t + type nonrec t = t type u = Constant.t -> Constant.t let hashcons hc (c,b) = (hc c,b) let eq ((c,b) as x) ((c',b') as y) = |