summaryrefslogtreecommitdiff
path: root/library/nameops.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /library/nameops.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'library/nameops.ml')
-rw-r--r--library/nameops.ml45
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"] *)