Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de DischargeAt)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 70 insertions, 80 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2613199ffd..7501471e54 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,10 +232,9 @@ let hdchar env c =
 	if i=0 then 
 	  lowercase_first_char (basename sp)
 	else 
-	  let na = id_of_global env (IndRef x) in lowercase_first_char na
+	  lowercase_first_char (id_of_global env (IndRef x))
     | IsMutConstruct ((sp,i) as x,_) ->
-	let na = id_of_global env (ConstructRef x) in
-	String.lowercase(List.hd(explode_id na))
+	lowercase_first_char (id_of_global env (ConstructRef x))
     | IsVar id  -> lowercase_first_char id
     | IsSort s -> sort_hdchar s
     | IsRel n ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 2686763aa6..11a4ce28e3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -12,15 +12,18 @@ type identifier = {
 
 type name = Name of identifier | Anonymous
 
-let make_ident sa n = { atom = sa; index = n }
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
 let repr_ident { atom = sa; index = n } = (sa,n)
+let make_ident sa n = 
+  let c = Char.code (String.get sa (String.length sa -1)) in
+  if c < code_of_0 or c > code_of_9 then { atom = sa; index = n }
+  else { atom = sa^"_"; index = n }
 
 let string_of_id { atom = s; index = n } =
   s ^ (if n = -1 then "" else string_of_int n)
 
-let code_of_0 = Char.code '0'
-let code_of_9 = Char.code '9'
-
 let id_of_string s =
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
@@ -46,17 +49,12 @@ let id_of_string s =
 let atompart_of_id id = id.atom
 let index_of_id id = id.index
 
-let explode_id { atom = s; index = n } =
-  (explode s) @ (if n = -1 then [] else explode (string_of_int n))
-
 let print_id { atom = a; index = n } = 
   match (a,n) with
     | ("",-1) -> [< 'sTR"[]" >]
     | ("",n)  -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
     | (s,n)   -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >]
 
-let print_idl idl = prlist_with_sep pr_spc print_id idl
-
 let id_ord id1 id2 =
   let (s1,n1) = repr_ident id1
   and (s2,n2) = repr_ident id2 in
@@ -82,17 +80,26 @@ module Idmap = Map.Make(IdOrdered)
 
 
 (* Fresh names *)
+let add_subscript_to_ident id n =
+  if n < 0 then error "Only natural numbers are allowed as subscripts";
+  if id.index = -1 then { atom = id.atom; index = n }
+  else  { atom = (string_of_id id)^"_"; index = n }
 
 let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
 
-let next_ident_away ({atom=str} as id) avoid = 
-  let rec name_rec i =
-    let create = if i = (-1) then id else {atom=str;index=i} in
-    if List.mem create avoid then name_rec (i+1) else create
-  in 
-  name_rec (-1)
-
-let rec next_ident_away_from {atom=str;index=i} avoid = 
+let next_ident_away id avoid = 
+  if List.mem id avoid then
+    let str = if id.index = -1 then id.atom else 
+    (* Ce serait sans doute mieux avec quelque chose inspiré de 
+       *** string_of_id id ^ "_" *** mais ça brise la compatibilité... *)
+      id.atom in
+    let rec name_rec i =
+      let create = {atom=str;index=i} in
+      if List.mem create avoid then name_rec (i+1) else create in 
+    name_rec 0
+  else id
+
+let next_ident_away_from {atom=str;index=i} avoid = 
   let rec name_rec i =
     let create = {atom=str;index=i} in
     if List.mem create avoid then name_rec (i+1) else create
@@ -109,17 +116,6 @@ let next_name_away name l =
     | Name(str) -> next_ident_away str l
     | Anonymous -> id_of_string "_"
 
-(* returns lids@[i1..in] where i1..in are new identifiers prefixed id *)
-let get_new_ids n id lids  =
-  let rec get_rec n acc =
-    if n = 0 then 
-      acc 
-    else 
-      let nid = next_ident_away id (acc@lids) in
-      get_rec (n-1) (nid::acc) 
-  in 
-  get_rec n []
-
 let id_of_name default = function
   | Name s -> s
   | Anonymous -> default
@@ -140,10 +136,12 @@ let kind_of_string = function
   | _ -> invalid_arg "kind_of_string"
 
 
-(* Section paths *)
+(*s Section paths *)
+
+type dir_path = string list
 
 type section_path = {
-  dirpath : string list ;
+  dirpath : dir_path ;
   basename : identifier ;
   kind : path_kind }
 
@@ -154,14 +152,15 @@ let kind_of_path sp = sp.kind
 let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
-let string_of_path_mind sp id =
-  let (sl,_,k) = repr_path sp in
+(* parsing and printing of section paths *)
+let string_of_dirpath sl = String.concat "#" (""::sl)
+
+let string_of_path sp =
+  let (sl,id,k) = repr_path sp in
   String.concat ""
     ((List.flatten (List.map (fun s -> ["#";s]) sl))
      @ [ "#"; string_of_id id; "."; string_of_kind k ])
     
-let string_of_path sp = string_of_path_mind sp sp.basename
-
 let path_of_string s =
   try
     let (sl,s,k) = parse_section_path s in
@@ -171,33 +170,6 @@ let path_of_string s =
 
 let print_sp sp = [< 'sTR (string_of_path sp) >]
 
-
-let coerce_path k { dirpath = p; basename = id } =
-  { dirpath = p; basename = id; kind = k }
-
-let ccisp_of_fwsp = function
-  | { dirpath = p; basename = id; kind = FW } -> 
-      { dirpath = p; basename = id; kind = CCI }
-  | _ -> invalid_arg "ccisp_of_fwsp"
-
-let ccisp_of { dirpath = p; basename = id } =
-  { dirpath = p; basename = id; kind = CCI }
-
-let objsp_of { dirpath = p; basename = id } =
-  { dirpath = p; basename = id; kind = OBJ }
-
-let fwsp_of_ccisp = function
-  | { dirpath = p; basename = id; kind = CCI } -> 
-      { dirpath = p; basename = id; kind = FW }
-  | _ -> invalid_arg "fwsp_of_ccisp"
-
-let fwsp_of { dirpath = p; basename = id } =
-  { dirpath = p; basename = id; kind = FW }
-
-let append_to_path sp str =
-  let (sp,id,k) = repr_path sp in
-  make_path sp (id_of_string ((string_of_id id)^str)) k
-
 let sp_of_wd = function
   | [] -> invalid_arg "Names.sp_of_wd"
   | l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
@@ -215,7 +187,7 @@ let sp_ord sp1 sp2 =
   else
     ck
 
-let sp_gt (sp1,sp2) = sp_ord sp1 sp2 > 0
+let dirpath_prefix_of = list_prefix_of
 
 module SpOrdered =
   struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 84b25d9cd6..1e1b4cb3f3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -10,19 +10,22 @@ open Pp
 type identifier
 type name = Name of identifier | Anonymous
 
+(* Constructor of an identifier;
+   [make_ident] builds an identifier from a string and an index; if
+   the string ends by a digit, a "_" is inserted *)
 val make_ident : string -> int -> identifier
-val string_of_id : identifier -> string
-val id_of_string : string -> identifier
 
-val explode_id : identifier -> string list
-val print_id : identifier -> std_ppcmds
-val print_idl : identifier list -> std_ppcmds
+(* Some destructors of an identifier *)
 val atompart_of_id : identifier -> string
-val index_of_id : identifier -> int
-val id_ord : identifier -> identifier -> int
-val id_without_number : identifier -> bool
 val first_char : identifier -> string
+val index_of_id : identifier -> int
+
+(* Parsing and printing of identifiers *)
+val string_of_id : identifier -> string
+val id_of_string : string -> identifier
+val print_id : identifier -> std_ppcmds
 
+(* Identifiers sets and maps *)
 module Idset : Set.S with type elt = identifier
 module Idmap : Map.S with type key = identifier
 
@@ -32,32 +35,42 @@ val next_ident_away : identifier -> identifier list -> identifier
 val next_name_away : name -> identifier list -> identifier
 val next_name_away_with_default : 
   string -> name -> identifier list -> identifier
-val get_new_ids : int -> identifier -> identifier list -> identifier list
-
-val id_of_name : identifier -> name -> identifier
 
+(*s path_kind is currently degenerated, only [CCI] is used *)
 type path_kind = CCI | FW | OBJ
 
+(* parsing and printing of path kinds *)
 val string_of_kind : path_kind -> string
 val kind_of_string : string -> path_kind
 
+(*s Directory paths = section names paths *)
+type dir_path = string list
+
+(* Printing of directory paths as "#module#submodule" *)
+val string_of_dirpath : dir_path -> string
+
 (*s Section paths *)
 type section_path
 
-val make_path : string list -> identifier -> path_kind -> section_path
-val repr_path : section_path -> string list * identifier * path_kind
-val dirpath : section_path -> string list
+(* Constructors of [section_path] *)
+val make_path : dir_path -> identifier -> path_kind -> section_path
+
+(* Destructors of [section_path] *)
+val repr_path : section_path -> dir_path * identifier * path_kind
+val dirpath : section_path -> dir_path
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
+(* Parsing and printing of section path as "#module#id#kind" *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
-val string_of_path_mind : section_path -> identifier -> string
 val print_sp : section_path -> std_ppcmds
 
+(*
+val string_of_path_mind : section_path -> identifier -> string
 val coerce_path : path_kind -> section_path -> section_path
 val fwsp_of : section_path -> section_path
 val ccisp_of : section_path -> section_path
@@ -68,8 +81,13 @@ val append_to_path : section_path -> string -> section_path
 
 val sp_ord : section_path -> section_path -> int
 val sp_gt : section_path * section_path -> bool
+*)
 
+(* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
+val dirpath_prefix_of : dir_path -> dir_path -> bool
+(*
 module Spset : Set.S with type elt = section_path
+*)
 module Spmap : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
@@ -80,3 +98,4 @@ type constructor_path = inductive_path * int
 val hcons_names : unit ->
   (section_path -> section_path) * (section_path -> section_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
+