Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins

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

4 files changed, 32 insertions, 18 deletions

diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 4ed6dbcd9e..5b97716fcf 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -16,7 +16,10 @@ type t =
 
 let section_path sl k =
   match List.rev sl with
-    | s::pa -> make_path (List.rev (List.map id_of_string pa)) (id_of_string s) (kind_of_string k)
+    | s::pa ->
+	make_path
+	  (make_dirpath (List.rev (List.map id_of_string pa)))
+	  (id_of_string s) (kind_of_string k)
     | [] -> invalid_arg "section_path"
 
 let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -53,7 +56,7 @@ let rec ast_to_ct = function
   | Coqast.Str (loc,a) -> Str (loc,a)
   | Coqast.Path (loc,a) ->
     let (sl,bn,pk) = repr_path a in
-    Path(loc, (List.map string_of_id sl) @ [string_of_id bn],(* Bidon *) "CCI")
+    Path(loc, (List.map string_of_id (repr_dirpath sl)) @ [string_of_id bn],(* Bidon *) "CCI")
   | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
 
 let loc = function
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 00259ef99f..e4523121c9 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -84,9 +84,9 @@ let implicit_args_to_ast_list sp mipv =
 	      
 let convert_qualid qid =
   let d, id = Nametab.repr_qualid qid in
-    match d with
+    match repr_dirpath d with
 	[] -> nvar id
-      | _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
+      | d -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
 		   [nvar id]);;
 
 (* This function converts constructors for an inductive definition to a
@@ -228,7 +228,7 @@ let name_to_ast (qid:Nametab.qualid) =
   	with Not_found -> 
 	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
 	    let dir,name = Nametab.repr_qualid qid in 
-	      if dir <> [] then raise Not_found;
+	      if dir <> make_dirpath [] then raise Not_found;
 	      let (c,typ) = Global.lookup_named name in 
 		(match c with
 		     None -> make_variable_ast name typ []
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index ff76f2c753..42daf3c191 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -58,7 +58,7 @@ let ctf_FileErrorMessage reqid pps =
   function has no effect on parsing *)
 let try_require_module import specif name fname =
  try Library.require_module (if specif = "UNSPECIFIED" then None
-  else Some (specif = "SPECIFICATION")) (Nametab.make_qualid [] (Names.id_of_string name)) fname (import = "IMPORT")
+  else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
  with
  | e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
 
@@ -292,24 +292,35 @@ let parse_file_action reqid file_name =
 (* This function is taken from Mltop.add_path *)
 
 let add_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+  if coq_dirpath = Names.make_dirpath [] then
+    anomaly "add_path: empty path in library";
+*)
   if exists_dir dir then
     begin
       Library.add_load_path_entry (dir,coq_dirpath);
-      Nametab.push_library_root (List.hd coq_dirpath)
+      Nametab.push_library_root coq_dirpath
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
+let convert_string d =
+  try Names.id_of_string d
+  with _ -> failwith "caught"
+
 let add_rec_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+  if coq_dirpath = Names.make_dirpath [] then anomaly "add_path: empty path in library";
+*)
   let dirs = all_subdirs dir in
+  let prefix = Names.repr_dirpath coq_dirpath in
   if dirs <> [] then
-    let convert = List.map Names.id_of_string in
-    let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
+    let convert_dirs (lp,cp) =
+      (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
+    let dirs = map_succeed convert_dirs dirs in
     begin
       List.iter Library.add_load_path_entry dirs;
-      Nametab.push_library_root (List.hd coq_dirpath)
+      Nametab.push_library_root coq_dirpath
     end
     else
       wARNING [< 'sTR ("Cannot open " ^ dir) >];;
@@ -318,7 +329,7 @@ let add_path_action reqid string_arg =
   let directory_name = glob string_arg in
   let alias = Filename.basename directory_name in
     begin
-      add_path directory_name [Names.id_of_string alias]
+      add_path directory_name (Names.make_dirpath [Names.id_of_string alias])
     end;;
 
 let print_version_action () =
@@ -328,7 +339,7 @@ let print_version_action () =
 let load_syntax_action reqid module_name =
  mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
  try
-      (let qid = Nametab.make_qualid [] (Names.id_of_string module_name) in
+      (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
       read_module qid;
       mSG [< 'sTR "opening... ">];
       let fullname = Nametab.locate_loaded_library qid in 
@@ -369,9 +380,9 @@ Libobject.relax true;
        else
 	 (mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
      begin
-       add_rec_path (Filename.concat coqdir "theories") [Nametab.coq_root];
-       add_path (Filename.concat coqdir "tactics") [Nametab.coq_root];
-       add_rec_path (Filename.concat coqdir "contrib") [Nametab.coq_root];
+       add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nametab.coq_root]);
+       add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nametab.coq_root]);
+       add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nametab.coq_root]);
        List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
      end;
 (try 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index cefc9f7e07..4ece713f51 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -176,7 +176,7 @@ let (imply_elim2: pbp_rule) = function
   | _ -> None;;
 
 let reference dir s =
-  let dir = List.map id_of_string ("Coq"::"Init"::[dir]) in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::[dir])) in
   let id = id_of_string s in
   try 
     Nametab.locate_in_absolute_module dir id