diff options
Diffstat (limited to 'library/nameops.ml')
| -rw-r--r-- | library/nameops.ml | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index e733d19d..02b085a7 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,7 @@ open Names (* Identifiers *) -let pr_id id = str (string_of_id id) +let pr_id id = str (Id.to_string id) let pr_name = function | Anonymous -> str "_" @@ -24,20 +24,20 @@ let code_of_0 = Char.code '0' let code_of_9 = Char.code '9' let cut_ident skip_quote s = - let s = string_of_id s in + let s = Id.to_string s in let slen = String.length s in (* [n'] is the position of the first non nullary digit *) let rec numpart n n' = - if n = 0 then + if Int.equal n 0 then (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) slen else let c = Char.code (String.get s (n-1)) in - if c = code_of_0 && n <> slen then + if Int.equal c code_of_0 && not (Int.equal n slen) then numpart (n-1) n' else if code_of_0 <= c && c <= code_of_9 then numpart (n-1) (n-1) - else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then + else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then numpart (n-1) (n-1) else n' @@ -46,9 +46,9 @@ let cut_ident skip_quote s = let repr_ident s = let numstart = cut_ident false s in - let s = string_of_id s in + let s = Id.to_string s in let slen = String.length s in - if numstart = slen then + if Int.equal numstart slen then (s, None) else (String.sub s 0 numstart, @@ -58,24 +58,24 @@ let make_ident sa = function | Some n -> let c = Char.code (String.get sa (String.length sa -1)) in let s = - if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n) + 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 (String.copy sa) + Id.of_string s + | None -> Id.of_string (String.copy sa) let root_of_id id = let suffixstart = cut_ident true id in - id_of_string (String.sub (string_of_id id) 0 suffixstart) + Id.of_string (String.sub (Id.to_string id) 0 suffixstart) (* Rem: semantics is a bit different, if an ident starts with toto00 then after successive renamings it comes to toto09, then it goes on with toto10 *) let lift_subscript id = - let id = string_of_id id in + 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 c = '9' then begin + if Int.equal (Char.code c) (Char.code '9') then begin assert (carrypos>0); add (carrypos-1) end @@ -93,20 +93,20 @@ let lift_subscript id = end; newid end - in id_of_string (add (len-1)) + in Id.of_string (add (len-1)) let has_subscript id = - let id = string_of_id id in + 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 = String.make (numstart+1) '0' in - String.blit (string_of_id id) 0 newid 0 numstart; - (id_of_string newid) + String.blit (Id.to_string id) 0 newid 0 numstart; + (Id.of_string newid) -let add_suffix id s = id_of_string (string_of_id id ^ s) -let add_prefix s id = id_of_string (s ^ string_of_id id) +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) @@ -114,7 +114,7 @@ let atompart_of_id id = fst (repr_ident id) let out_name = function | Name id -> id - | Anonymous -> failwith "out_name: expects a defined name" + | Anonymous -> failwith "Nameops.out_name" let name_fold f na a = match na with @@ -136,13 +136,14 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous -let pr_lab l = str (string_of_label l) +let pr_lab l = str (Label.to_string l) -let default_library = Names.initial_dir (* = ["Top"] *) +let default_library = Names.DirPath.initial (* = ["Top"] *) (*s Roots of the space of absolute names *) -let coq_root = id_of_string "Coq" -let default_root_prefix = make_dirpath [] +let coq_string = "Coq" +let coq_root = Id.of_string coq_string +let default_root_prefix = DirPath.empty (* Metavariables *) let pr_meta = Pp.int |