Changed the semantics of AddRecPath.

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

2 files changed, 75 insertions, 28 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index ec9c3b5d2e..926d350579 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -15,7 +15,7 @@
 (* CONFIGURATION PARAMETERS *)
 
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
-let verbose = ref false;; (* always set to true during a "Print XML All" *)
+let verbose = ref true;; (* always set to true during a "Print XML All" *)
 
 (* UTILITY FUNCTIONS *)
 
@@ -66,7 +66,8 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 
 (*V7*)
 exception Not_match
-let trim_wrong_uri_prefix pref =
+let trim_wrong_uri_prefix pref {System.relative_subdir=rs ; System.directory=d} =
+(*
  let map =
   [(".","/prove");
    ("/home/pauillac/coq3/sacerdot/V7/theories/Arith","/coq/Arith");
@@ -97,6 +98,8 @@ let trim_wrong_uri_prefix pref =
        _ -> trim tl
  in
   trim map
+*)
+  "/" ^ rs
 ;;
 
 
@@ -110,8 +113,8 @@ let uri_of_path sp =
      match sl with
         []             -> assert false (*V7 WHAT NOW? *)
       | module_name::_ ->
-	  let _,file = Library.module_filename module_name in
-          trim_wrong_uri_prefix file
+	  let (prefix,file) = Library.module_filename module_name in
+          trim_wrong_uri_prefix file prefix
    in
     "cic:" ^ module_path ^ "/" ^ (String.concat "/" sl) ^ "/" ^
      (N.string_of_id id) ^ "." ^ (ext_of_sp sp)
@@ -176,6 +179,14 @@ let string_of_pvars pvars hyps =
   let rec aux n =
    function
       [] -> assert false
+(*print_string "\nPVARS:" ;
+List.iter (List.iter print_string) pvars ;
+print_string "\nHYPS:" ;
+List.iter print_string hyps ;
+print_string "\n" ;
+flush stdout ;
+(-1,"?")
+*)
     | l::_ when List.mem v l -> (n,v)
     | _::tl -> aux (n+1) tl
   in
@@ -590,6 +601,17 @@ let toprint = ref [];;
 
 (* makes a filename from a directory name, a section path and an extension *)
 let mkfilename dn sp ext =
+ let dir_list_of_dirpath s =
+  let rec aux n =
+   try
+    let pos = String.index_from s n '/' in
+    let head = String.sub s n (pos - n) in
+     head::(aux (pos + 1))
+   with
+    Not_found -> [String.sub s n (String.length s - n)]
+  in
+   aux 0
+ in
  let rec join_dirs cwd =
    function
       [] -> ""
@@ -601,13 +623,22 @@ let mkfilename dn sp ext =
         ) ;
         he ^ "/" ^ join_dirs newcwd tail
  in
+  let module L = Library in
+  let module S = System in
   let module N = Names in
    match dn with
       None         -> None
     | Some basedir ->
-       let (dirs, filename, _) = N.repr_path sp in
-        Some (basedir ^ "/" ^ join_dirs basedir dirs ^
-              N.string_of_id filename ^ "." ^ ext ^ ".xml")
+       match N.repr_path sp with
+          (module_name::_ as dirs, filename, _) ->
+           let dirs = 
+             (dir_list_of_dirpath
+              (fst (L.module_filename module_name)).S.relative_subdir
+             ) @ dirs
+           in
+            Some (basedir ^ "/" ^ join_dirs basedir dirs ^
+                  N.string_of_id filename ^ "." ^ ext ^ ".xml")
+        | _ -> assert false
 ;;
 
 (* Next exception is used only inside print_object *)
@@ -657,13 +688,16 @@ let print_object lobj id sp dn fv =
            print_mutual_inductive packs fv hyps nparams
     | "VARIABLE" ->
         let (_,(varentry,_,_)) = Declare.out_variable lobj in
-         let typ =
+         add_to_pvars (N.string_of_id id) ;
+         begin
           match varentry with
-             Declare.SectionLocalDef _ -> assert false
-           | Declare.SectionLocalAssum typ -> typ
-         in
-          add_to_pvars (N.string_of_id id) ;
-          print_variable id (T.body_of_type typ)
+             Declare.SectionLocalDef body ->
+              print_string "************** UNIMPLEMENTED ***********\n" ;
+              flush stdout ;
+              [<>]
+           | Declare.SectionLocalAssum typ ->
+              print_variable id (T.body_of_type typ)
+         end
     | "CLASS"
     | "COERCION"
     | _ -> raise Uninteresting
@@ -687,7 +721,7 @@ let rec print_library_segment state bprintleaf dn =
      print_if_verbose (Names.string_of_path sp ^ "\n") ;
      print_node node (Names.basename sp) sp bprintleaf dn ;
      print_if_verbose "\n"
-   ) state
+   ) (List.rev state)
 (* print_node node id section_path bprintleaf directory_name             *)
 (* prints a single node (and all it's subnodes via print_library_segment *)
 and print_node n id sp bprintleaf dn =
@@ -709,21 +743,29 @@ and print_node n id sp bprintleaf dn =
           (* this is an uncooked term or a local (with no namesakes) term *)
           begin
            if could_have_namesakes o sp then
-            (* this is an uncooked term *)
-            toprint := (id,sp,sp,o,!pvars,dn)::!toprint
+            begin
+             (* this is an uncooked term *)
+             print_if_verbose ("Rimando " ^ Names.string_of_id id ^ "\n") ;
+             toprint := (id,sp,sp,o,!pvars,dn)::!toprint
+            end
            else
-            (* this is a local term *)
-            print_object o id sp dn !pvars ;
-            print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n")
+            begin
+             (* this is a local term *)
+             print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
+             print_object o id sp dn !pvars
+            end
           end
          else
-          (* update the least cooked sp *)
-          toprint :=
-           List.map
-            (function
-               (id',usp,_,uo,pv,dn) when id' = id -> (id,usp,sp,uo,pv,dn)
-             | t -> t
-            ) !toprint
+          begin
+           (* update the least cooked sp *)
+           print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n") ;
+           toprint :=
+            List.map
+             (function
+                (id',usp,_,uo,pv,dn) when id' = id -> (id,usp,sp,uo,pv,dn)
+              | t -> t
+             ) !toprint
+          end
        end
    | L.OpenedSection s -> print_if_verbose ("OpenDir " ^ s ^ "\n")
    | L.ClosedSection (s,state) ->
@@ -788,7 +830,7 @@ let printModule id dn =
   let ls = L.module_segment (Some str) in
    print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
     (snd (L.module_filename str)) ^ "\n") ;
-   print_closed_section str ls dn ;
+   print_closed_section str (List.rev ls) dn ;
    print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
     (snd (L.module_filename str)) ^ "\n")
 ;;
diff --git a/lib/system.ml b/lib/system.ml
index a967ed191c..55c77b0769 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -39,7 +39,12 @@ let all_subdirs root =
     with End_of_file ->
       closedir dirh
   in
-  if exists_dir root then traverse root ""; 
+  if exists_dir root then
+   begin
+    let root_base_name = Filename.basename root in
+     add root root_base_name ;
+     traverse root root_base_name
+   end ;
   List.rev !l
 
 let safe_getenv_def var def =