diff options
Diffstat (limited to 'library/nameops.ml')
| -rw-r--r-- | library/nameops.ml | 45 |
1 files changed, 11 insertions, 34 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index df9aa95d..28b799f5 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 9433 2006-12-12 09:38:53Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -30,14 +30,14 @@ let cut_ident skip_quote s = 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 n = 0 then (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) slen - else + else let c = Char.code (String.get s (n-1)) in - if c = code_of_0 && n <> slen then - numpart (n-1) n' - else if code_of_0 <= c && c <= code_of_9 then + if c = code_of_0 && 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 numpart (n-1) (n-1) @@ -50,14 +50,14 @@ let repr_ident s = let numstart = cut_ident false s in let s = string_of_id s in let slen = String.length s in - if numstart = slen then + if numstart = slen then (s, None) else (String.sub s 0 numstart, Some (int_of_string (String.sub s numstart (slen - numstart)))) let make_ident sa = function - | Some n -> + | 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) @@ -112,26 +112,8 @@ let add_prefix s id = id_of_string (s ^ string_of_id id) let atompart_of_id id = fst (repr_ident id) -(* Fresh names *) - let lift_ident = lift_subscript -let next_ident_away id avoid = - if List.mem id avoid then - let id0 = if not (has_subscript id) then id else - (* Ce serait sans doute mieux avec quelque chose inspiré de - *** make_ident id (Some 0) *** mais ça brise la compatibilité... *) - forget_subscript id in - let rec name_rec id = - if List.mem id avoid then name_rec (lift_ident id) else id in - name_rec id0 - else id - -let next_ident_away_from id avoid = - let rec name_rec id = - if List.mem id avoid then name_rec (lift_ident id) else id in - name_rec id - (* Names *) let out_name = function @@ -143,9 +125,11 @@ let name_fold f na a = | Name id -> f id a | Anonymous -> a +let name_iter f na = name_fold (fun x () -> f x) na () + let name_cons na l = match na with - | Anonymous -> l + | Anonymous -> l | Name id -> id::l let name_app f = function @@ -156,13 +140,6 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous -let next_name_away_with_default default name l = - match name with - | Name str -> next_ident_away str l - | Anonymous -> next_ident_away (id_of_string default) l - -let next_name_away = next_name_away_with_default "H" - let pr_lab l = str (string_of_label l) let default_library = Names.initial_dir (* = ["Top"] *) |