Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

1 files changed, 97 insertions, 156 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 4965a733c9..c4ced8e999 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -11,101 +11,16 @@
 open Pp
 open Util
 
+(*s Identifiers *)
+
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
-(* This checks that a string is acceptable as an ident, i.e. starts
-   with a letter and contains only letters, digits or "'" *)
-
-let check_ident_suffix i l s =
-  for i=1 to l-1 do
-    let c = String.get s i in
-    if not (is_letter c or is_digit c or c = '\'') then
-      error
-	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
-  done
-
-let check_ident s =
-  let l = String.length s in
-  if l = 0 then error "The empty string is not an identifier"; 
-  let c = String.get s 0 in
-  if not (is_letter c) then error "An identifier starts with a letter";
-  check_ident_suffix 1 l s
-
-let check_suffix s = check_ident_suffix 0 (String.length s) s
-
-let is_ident s = try check_ident s; true with _ -> false
-
 (* Identifiers *)
-(*
-module Ident = struct
-
-type t = {
-  atom : string ; 
-  index : int }
-
-let repr_ident { atom = sa; index = n } =
-  if n = -1 then (sa,None) else (sa,Some n)
-
-let make_ident sa = function
-  | Some 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 }
-  | None -> { atom = sa; index = -1 }
-
-let string_of_id id = match repr_ident id with
-  | (s,None) -> s
-  | (s,Some n) -> s ^ (string_of_int n)
-
-let id_of_string 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 
-      failwith
-	("The string " ^ s ^ " is not an identifier: it contains only digits")
-    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 
-	numpart (n-1) (n-1)
-      else 
-	n'
-  in
-  let numstart = numpart slen slen in
-  if numstart = slen then 
-    { atom = s; index = -1 } 
-  else
-    { atom = String.sub s 0 numstart;
-      index = int_of_string (String.sub s numstart (slen - numstart)) }
-
-let first_char id =
-  assert (id.atom <> "");
-  String.make 1 id.atom.[0]
-
-let id_ord { atom = s1; index = n1 } { atom = s2; index = n2 } = 
-  let s_bit = Pervasives.compare s1 s2 in
-  if s_bit = 0 then n1 - n2 else s_bit
 
-(* Rem : if an ident starts with toto00 then after successive
-   renamings it comes to toto09, then it goes on with toto010 *)
-let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
-let restart_ident id = { id with index = 0 }
-let has_index id = (id.index <> -1)
-
-let hash_sub hstr id = { atom = hstr id.atom; index = id.index }
-let equal id1 id2 = id1.atom == id2.atom && id1.index = id2.index
-
-end (* End of module Ident *)
-*)
-(* Second implementation *)
-module Ident = struct
-
-type t = string
+type identifier = string
 
 let cut_ident s =
   let slen = String.length s in
@@ -139,13 +54,7 @@ let make_ident sa = function
       let c = Char.code (String.get sa (String.length sa -1)) in
       if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
       else sa ^ "_" ^ (string_of_int n)
-  | None -> sa
-
-let add_suffix id s = check_suffix s; id^s
-let add_prefix s id = check_ident s; s^id
-
-let string_of_id id = id
-let id_of_string s = s
+  | None -> String.copy sa
 
 let first_char id =
   assert (id <> "");
@@ -155,7 +64,7 @@ let id_ord = Pervasives.compare
 
 (* 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_ident id =
+let lift_subscript id =
   let len = String.length id in
   let rec add carrypos =
     let c = id.[carrypos] in
@@ -180,28 +89,52 @@ let lift_ident id =
     end
   in add (len-1)
 
-let has_index id = is_digit (id.[String.length id - 1])
+let has_subscript id = is_digit (id.[String.length id - 1])
 
-let restart_ident id =
+let forget_subscript id =
   let len = String.length id in
   let numstart = cut_ident id in
   let newid = String.make (numstart+1) '0' in
   String.blit id 0 newid 0 numstart;
   newid
 
-let hash_sub hstr id = hstr id
-let equal id1 id2 = id1 == id2
+(* This checks that a string is acceptable as an ident, i.e. starts
+   with a letter and contains only letters, digits or "'" *)
+
+let check_ident_suffix i l s =
+  for i=1 to l-1 do
+    let c = String.get s i in
+    if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then
+      error
+	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
+  done
+
+let check_ident s =
+  let l = String.length s in
+  if l = 0 then error "The empty string is not an identifier";
+  let c = String.get s 0 in
+  if (is_letter c) or c = '_' or c = '$' then check_ident_suffix 1 l s
+  else error (s^": an identifier starts with a letter")
+
+let is_ident s = try check_ident s; true with _ -> false
 
-end (* End of module Ident *)
+let check_suffix s = check_ident_suffix 0 (String.length s) s
 
-type identifier = Ident.t
-let repr_ident = Ident.repr_ident
-let make_ident = Ident.make_ident
 let add_suffix id s = check_suffix s; id^s
 let add_prefix s id = check_ident s; s^id
-let string_of_id = Ident.string_of_id
-let id_of_string = Ident.id_of_string
-let id_ord = Ident.id_ord
+
+let string_of_id id = String.copy id
+let id_of_string s = check_ident s; String.copy s
+
+(* Hash-consing of identifier *)
+module Hident = Hashcons.Make(
+  struct 
+    type t = string
+    type u = string -> string
+    let hash_sub hstr id = hstr id
+    let equal id1 id2 = id1 == id2
+    let hash = Hashtbl.hash
+  end)
 
 module IdOrdered = 
   struct
@@ -216,18 +149,18 @@ let atompart_of_id id = fst (repr_ident id)
 let index_of_id id = snd (repr_ident id)
 let pr_id id = [< 'sTR (string_of_id id) >]
 
-let first_char = Ident.first_char
+let wildcard = id_of_string "_"
 
 (* Fresh names *)
 
-let lift_ident = Ident.lift_ident
+let lift_ident = lift_subscript
 
 let next_ident_away id avoid = 
   if List.mem id avoid then
-    let id0 = if not (Ident.has_index id) then id else 
+    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é... *)
-    Ident.restart_ident id in
+    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
@@ -272,30 +205,25 @@ let kind_of_string = function
   | _ -> invalid_arg "kind_of_string"
 
 (*s Directory paths = section names paths *)
-type dir_path = string list
-
-(*s Section paths are absolute names *)
+type module_ident = identifier
+type dir_path = module_ident list
 
-type section_path = {
-  dirpath : dir_path ;
-  basename : identifier ;
-  kind : path_kind }
+module ModIdOrdered = 
+  struct
+    type t = identifier
+    let compare = Pervasives.compare
+  end
 
-let make_path pa id k = { dirpath = pa; basename = id; kind = k }
-let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+module ModIdmap = Map.Make(ModIdOrdered)
 
-let kind_of_path sp = sp.kind
-let basename sp = sp.basename
-let dirpath sp = sp.dirpath
+let make_dirpath x = x
+let repr_dirpath x = x
 
-(* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "." sl
+let dirpath_prefix = function 
+  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | l -> snd (list_sep_last l)
 
-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 ])
+let split_dirpath d = let (b,d) = list_sep_last d in (d,b)
 
 let parse_sp s =
   let len = String.length s in
@@ -304,37 +232,60 @@ let parse_sp s =
       let pos = String.index_from s n '.' in
       let dir = String.sub s n (pos-n) in
       let dirs,n' = decoupe_dirs (succ pos) in
-      dir::dirs,n'
+      (id_of_string dir)::dirs,n'
     with
       | Not_found -> [],n
   in
   if len = 0 then invalid_arg "parse_section_path";
   let dirs,n = decoupe_dirs 0 in
   let id = String.sub s n (len-n) in
-  dirs,id
+  dirs, (id_of_string id)
 
-let path_of_string s =
+let dirpath_of_string s =
   try
     let sl,s = parse_sp s in
-    make_path sl (id_of_string s) CCI
+    sl @ [s]
   with
-    | Invalid_argument _ -> invalid_arg "path_of_string"
+    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
 
-let dirpath_of_string s =
+let string_of_dirpath sl = String.concat "." (List.map string_of_id sl)
+
+let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
+
+(*s Section paths are absolute names *)
+
+type section_path = {
+  dirpath : dir_path ;
+  basename : identifier ;
+  kind : path_kind }
+
+let make_path pa id k = { dirpath = pa; basename = id; kind = k }
+let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+
+let kind_of_path sp = sp.kind
+let basename sp = sp.basename
+let dirpath sp = sp.dirpath
+
+(* parsing and printing of section paths *)
+let string_of_path sp =
+  let (sl,id,k) = repr_path sp in
+  (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+
+let path_of_string s =
   try
     let sl,s = parse_sp s in
-    sl @ [s]
+    make_path sl s CCI
   with
-    | Invalid_argument _ -> invalid_arg "dirpath_of_string"
+    | Invalid_argument _ -> invalid_arg "path_of_string"
 
 let pr_sp sp = [< 'sTR (string_of_path sp) >]
 
 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
+  | l -> let (bn,dp) = list_sep_last l in make_path dp bn OBJ
 
 let wd_of_sp sp = 
-  let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
+  let (sp,id,_) = repr_path sp in sp @ [id]
 
 let sp_ord sp1 sp2 =
   let (p1,id1,k) = repr_path sp1
@@ -346,7 +297,7 @@ let sp_ord sp1 sp2 =
   else
     ck
 
-let dirpath_prefix_of = list_prefix_of
+let is_dirpath_prefix_of = list_prefix_of
 
 module SpOrdered =
   struct
@@ -366,16 +317,6 @@ type inductive_path = section_path * int
 type constructor_path = inductive_path * int
 type mutual_inductive_path = section_path
 
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
-  struct 
-    type t = Ident.t
-    type u = string -> string
-    let hash_sub = Ident.hash_sub
-    let equal = Ident.equal
-    let hash = Hashtbl.hash
-  end)
-
 (* Hash-consing of name objects *)
 module Hname = Hashcons.Make(
   struct 
@@ -395,9 +336,9 @@ module Hname = Hashcons.Make(
 module Hsp = Hashcons.Make(
   struct 
     type t = section_path
-    type u = (identifier -> identifier) * (string -> string)
-    let hash_sub (hident,hstr) sp =
-      { dirpath = List.map hstr sp.dirpath;
+    type u = identifier -> identifier
+    let hash_sub hident sp =
+      { dirpath = List.map hident sp.dirpath;
         basename = hident sp.basename;
         kind = sp.kind }
     let equal sp1 sp2 =
@@ -411,6 +352,6 @@ let hcons_names () =
   let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
   let hident = Hashcons.simple_hcons Hident.f hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
-  let hspcci = Hashcons.simple_hcons Hsp.f (hident,hstring) in
-  let hspfw = Hashcons.simple_hcons Hsp.f (hident,hstring) in
+  let hspcci = Hashcons.simple_hcons Hsp.f hident in
+  let hspfw = Hashcons.simple_hcons Hsp.f hident in
   (hspcci,hspfw,hname,hident,hstring)