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

4 files changed, 27 insertions, 30 deletions

diff --git a/lib/system.ml b/lib/system.ml
index cf48f0e4b4..bb3c711307 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -13,22 +13,18 @@ open Util
 open Unix
 
 (* Files and load path. *)
-(* All subdirectories, recursively *)
 
-type load_path_entry = {
-  directory : string;
-  coq_dirpath : string list }
+type physical_path = string
+type load_path = physical_path list
 
-type load_path = load_path_entry list
+(* All subdirectories, recursively *)
 
 let exists_dir dir =
   try let _ = opendir dir in true with Unix_error _ -> false
 
-let all_subdirs root alias =
+let all_subdirs root =
   let l = ref [] in
-  let add f rel = 
-    l := { directory = f; coq_dirpath = rel } :: !l 
-  in
+  let add f rel = l := (f, rel) :: !l in
   let rec traverse dir rel =
     let dirh = opendir dir in
     try
@@ -49,12 +45,8 @@ let all_subdirs root alias =
   in
   if exists_dir root then
    begin
-     let alias = match alias with 
-       | Some a -> a
-       | None -> [Filename.basename root]
-     in
-     add root alias;
-     traverse root alias
+     add root [];
+     traverse root []
    end ;
   List.rev !l
 
@@ -73,7 +65,7 @@ let glob s = s
 let search_in_path path filename =
   let rec search = function
     | lpe :: rem ->
-	let f = glob (Filename.concat lpe.directory filename) in
+	let f = glob (Filename.concat lpe filename) in
 	if Sys.file_exists f then (lpe,f) else search rem
     | [] ->
 	raise Not_found
@@ -86,7 +78,7 @@ let find_file_in_path paths name =
   let globname = glob name in
   if not (Filename.is_relative globname) then
     let root = Filename.dirname globname in
-    { directory = root; coq_dirpath = [] }, globname
+    root, globname
   else 
     try 
       search_in_path paths name
@@ -129,12 +121,11 @@ let raw_extern_intern magic suffix =
       open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
     output_binary_int channel magic;
     filec
-  and intern_state paths name = 
-    let lpe,fname = find_file_in_path paths (make_suffix name suffix) in
+  and intern_state fname = 
     let channel = open_in_bin fname in
     if input_binary_int channel <> magic then
       raise (Bad_magic_number fname);
-    (lpe,fname,channel)
+    channel
   in 
   (extern_state,intern_state)
 
@@ -151,7 +142,8 @@ let extern_intern magic suffix =
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name = 
     try
-      let (_,fname,channel) = raw_intern paths name in
+      let _,fname = find_file_in_path paths (make_suffix name suffix) in
+      let channel = raw_intern fname in
       let v = marshal_in channel in
       close_in channel; 
       v
diff --git a/lib/system.mli b/lib/system.mli
index ee2dca4905..e6eb921883 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -12,15 +12,13 @@
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-type load_path_entry = {
-  directory : string;
-  coq_dirpath : string list }
 
-type load_path = load_path_entry list
+type physical_path = string
+type load_path = physical_path list
 
-val all_subdirs : unix_path:string -> string list option -> load_path
+val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
-val where_in_path : load_path -> string -> load_path_entry * string
+val where_in_path : load_path -> string -> physical_path * string
 
 val make_suffix : string -> string -> string
 val file_readable_p : string -> bool
@@ -31,7 +29,7 @@ val home : string
 
 val exists_dir : string -> bool
 
-val find_file_in_path : load_path -> string -> load_path_entry * string
+val find_file_in_path : load_path -> string -> physical_path * string
 
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
@@ -43,8 +41,7 @@ val marshal_in : in_channel -> 'a
 exception Bad_magic_number of string
 
 val raw_extern_intern : int -> string -> 
-  (string -> string * out_channel) *
-  (load_path -> string -> load_path_entry * string * in_channel)
+  (string -> string * out_channel) * (string -> in_channel)
 
 val extern_intern : 
   int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
diff --git a/lib/util.ml b/lib/util.ml
index 0c3c038dd2..cf5b58b49e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -223,6 +223,13 @@ let rec list_distinct = function
   | h::t -> (not (List.mem h t)) && list_distinct t
   | _ -> true
 
+let rec list_filter2 f = function
+  | [], [] as p -> p
+  | d::dp, l::lp ->
+     let (dp',lp' as p) = list_filter2 f (dp,lp) in
+      if f d l then d::dp', l::lp' else p
+  | _ -> invalid_arg "list_filter2"
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
diff --git a/lib/util.mli b/lib/util.mli
index d5976baf1d..a57803c5e2 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -64,6 +64,7 @@ val list_chop : int -> 'a list -> 'a list * 'a list
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
+val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_map2_i : 
   (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list