Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules

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

17 files changed, 99 insertions, 70 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9b3aa06940..2574a3b30f 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -212,7 +212,8 @@ let recognize_number t =
  This is the right way to access to Coq constants in tactics ML code *)
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("Zarith"::dir) (id_of_string s) CCI)
 
 (* fast_integer *)
 let coq_xH = lazy (constant ["fast_integer"] "xH")
@@ -337,36 +338,39 @@ let coq_imp_simp = lazy (constant ["auxiliary"] "imp_simp")
 let coq_neq = lazy (constant ["auxiliary"] "neq")
 let coq_Zne = lazy (constant ["auxiliary"] "Zne")
 
-(* Compare_dec *)
-let coq_le_gt_dec = lazy (constant ["Compare_dec"] "le_gt_dec")
+let constant dir s =
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 (* Peano *)
-let coq_le = lazy (constant ["Peano"] "le")
-let coq_gt = lazy (constant ["Peano"] "gt")
+let coq_le = lazy (constant ["Init";"Peano"] "le")
+let coq_gt = lazy (constant ["Init";"Peano"] "gt")
 
 (* Datatypes *)
-let coq_nat = lazy (constant ["Datatypes"] "nat")
-let coq_S = lazy (constant ["Datatypes"] "S")
-let coq_O = lazy (constant ["Datatypes"] "O")
+let coq_nat = lazy (constant ["Init";"Datatypes"] "nat")
+let coq_S = lazy (constant ["Init";"Datatypes"] "S")
+let coq_O = lazy (constant ["Init";"Datatypes"] "O")
 
 (* Minus *)
-let coq_minus = lazy (constant ["Minus"] "minus")
+let coq_minus = lazy (constant ["Arith";"Minus"] "minus")
+
+(* Compare_dec *)
+let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
 
 (* Logic *)
-let coq_eq = lazy (constant ["Logic"] "eq")
-let coq_and = lazy (constant ["Logic"] "and")
-let coq_not = lazy (constant ["Logic"] "not")
-let coq_or = lazy (constant ["Logic"] "or")
-let coq_ex = lazy (constant ["Logic"] "ex")
+let coq_eq = lazy (constant ["Init";"Logic"] "eq")
+let coq_and = lazy (constant ["Init";"Logic"] "and")
+let coq_not = lazy (constant ["Init";"Logic"] "not")
+let coq_or = lazy (constant ["Init";"Logic"] "or")
+let coq_ex = lazy (constant ["Init";"Logic"] "ex")
 
 (* Section paths for unfold *)
-let sp_Zs = path_of_string "#zarith_aux#Zs.cci"
-let sp_Zminus = path_of_string "#zarith_aux#Zminus.cci"
-let sp_Zle = path_of_string "#zarith_aux#Zle.cci"
-let sp_Zgt = path_of_string "#zarith_aux#Zgt.cci"
-let sp_Zge = path_of_string "#zarith_aux#Zge.cci"
-let sp_Zlt = path_of_string "#zarith_aux#Zlt.cci"
-let sp_not = path_of_string "#Logic#not.cci"
+let sp_Zs = path_of_string "Zarith.zarith_aux.Zs"
+let sp_Zminus = path_of_string "Zarith.zarith_aux.Zminus"
+let sp_Zle = path_of_string "Zarith.zarith_aux.Zle"
+let sp_Zgt = path_of_string "Zarith.zarith_aux.Zgt"
+let sp_Zge = path_of_string "Zarith.zarith_aux.Zge"
+let sp_Zlt = path_of_string "Zarith.zarith_aux.Zlt"
+let sp_not = path_of_string "Init.Logic.not"
 
 let mk_var v = mkVar (id_of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index b3462d8f37..a8250f4900 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -113,7 +113,8 @@ open Proof_type
   the constants are loaded in the environment *)
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("ring"::dir) (id_of_string s) CCI)
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 775724e49a..fccdc3e784 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -26,7 +26,8 @@ let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("ring"::dir) (id_of_string s) CCI)
 
 (* Ring_theory *)
 
@@ -84,10 +85,14 @@ let coq_aspolynomial_normalize_ok =
 let coq_apolynomial_normalize_ok = 
   lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")
 
+let logic_constant dir s =
+  Declare.global_absolute_reference
+    (make_path ("Init"::dir) (id_of_string s) CCI)
+
 (* Logic *)
-let coq_f_equal2 = lazy (constant ["Logic"] "f_equal2")
-let coq_eq = lazy (constant ["Logic"] "eq")
-let coq_eqT = lazy (constant ["Logic_Type"] "eqT")
+let coq_f_equal2 = lazy (logic_constant ["Logic"] "f_equal2")
+let coq_eq = lazy (logic_constant ["Logic"] "eq")
+let coq_eqT = lazy (logic_constant ["Logic_Type"] "eqT")
 
 (*********** Useful types and functions ************)
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index df79fe3f7f..62f7020a1e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -847,7 +847,7 @@ and print_node n id sp bprintleaf dn =
        end ;
       print_if_verbose "/ClosedDir\n"
    | L.Module s ->
-      print_if_verbose ("Module " ^ s ^ "\n")
+      print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
    | L.FrozenState _ ->
       print_if_verbose ("FrozenState\n")
 ;;
diff --git a/kernel/names.ml b/kernel/names.ml
index ae80915b74..657a23ac3c 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -167,11 +167,27 @@ let string_of_path sp =
   String.concat ""
     (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
      @ [ string_of_id id ])
+
+let parse_sp s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      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'
+    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
     
 let path_of_string s =
   try
-    let (sl,s,k) = parse_section_path s in
-    make_path sl (id_of_string s) (kind_of_string k)
+    let sl,s = parse_sp s in
+    make_path sl (id_of_string s) CCI
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 76fc0b12a9..4ea2ded009 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -16,7 +16,7 @@
 open Pp
 open Util
 
-type universe = { u_mod : string; u_num : int }
+type universe = { u_mod : Names.dir_path; u_num : int }
 
 let universe_ord x y =
   let c = x.u_num - y.u_num in
@@ -27,12 +27,13 @@ module UniverseOrdered = struct
   let compare = universe_ord
 end
 
-let pr_uni u = [< 'sTR u.u_mod ; 'sTR"." ; 'iNT u.u_num >]
+let pr_uni u =
+  [< 'sTR (Names.string_of_dirpath u.u_mod) ; 'sTR"." ; 'iNT u.u_num >]
 
-let dummy_univ = { u_mod = "dummy univ"; u_num = 0 } (* for prover terms *)
-let implicit_univ = { u_mod = "implicit univ"; u_num = 0 }
+let dummy_univ = { u_mod = ["dummy univ"]; u_num = 0 } (* for prover terms *)
+let implicit_univ = { u_mod = ["implicit univ"]; u_num = 0 }
 
-let current_module = ref ""
+let current_module = ref []
 
 let set_module m = current_module := m
 
@@ -68,7 +69,7 @@ let declare_univ u g =
 (* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the
    resulting graph. *)
 let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) =
-  let prop_sp = "prop_univ" in
+  let prop_sp = ["prop_univ"] in
   let u = { u_mod = prop_sp; u_num = 0 } in
   let su = { u_mod = prop_sp; u_num = 1 } in
   let ssu = { u_mod = prop_sp; u_num = 2 } in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c37ddba88b..ba0b6aea19 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,7 +16,7 @@ val prop_univ : universe
 val prop_univ_univ : universe
 val prop_univ_univ_univ : universe
 
-val set_module : string -> unit
+val set_module : dir_path -> unit
 
 val new_univ : unit -> universe
 
diff --git a/lib/system.ml b/lib/system.ml
index 55c77b0769..5da2d9f357 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -41,9 +41,8 @@ let all_subdirs root =
   in
   if exists_dir root then
    begin
-    let root_base_name = Filename.basename root in
-     add root root_base_name ;
-     traverse root root_base_name
+     add root "";
+     traverse root ""
    end ;
   List.rev !l
 
diff --git a/lib/util.ml b/lib/util.ml
index dd5be58714..05b147cee3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -32,28 +32,26 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
-let parse_section_path s =
+let check_is_ident s =
+  let len = String.length s in
+  if len = 0 then invalid_arg "parse_loadpath: is not a valid name";
+  (* TODO... *)
+  ()
+
+let parse_loadpath s =
   let len = String.length s in
   let rec decoupe_dirs n =
-    try
-      let pos = String.index_from s n '#' in
+    try  
+      let pos = String.index_from s n '/' in
+      if pos = n then
+	invalid_arg "parse_loadpath: find an empty dir in loadpath";
       let dir = String.sub s n (pos-n) in
-      let dirs,n' = decoupe_dirs (succ pos) in
-      dir::dirs,n'
-    with
-      | Not_found -> [],n
-  in
-  let decoupe_kind n =
-    try
-      let pos = String.index_from s n '.' in
-      String.sub s n (pos-n), String.sub s (succ pos) (pred (len-pos))
+      check_is_ident dir;
+      dir :: (decoupe_dirs (succ pos))
     with
-      | Not_found -> invalid_arg "parse_section_path"
+      | Not_found -> [String.sub s n (len-n)]
   in
-  if len = 0 || String.get s 0 <> '#' then invalid_arg "parse_section_path";
-  let dirs,n = decoupe_dirs 1 in
-  let id,k = decoupe_kind n in
-  dirs,id,k
+  if len = 0 then [] else decoupe_dirs 0
 
 module Stringset = Set.Make(struct type t = string let compare = compare end)
 
diff --git a/lib/util.mli b/lib/util.mli
index ed1ac8ee35..58e356c0d2 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -30,7 +30,7 @@ val invalid_arg_loc : loc * string -> 'a
 val explode : string -> string list
 val implode : string list -> string
 
-val parse_section_path : string -> string list * string * string
+val parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
 
diff --git a/library/lib.ml b/library/lib.ml
index 4dd0a36f20..a7028e1201 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,7 +8,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | Module of string
+  | Module of dir_path
   | OpenedSection of string * Summary.frozen
   (* bool is to tell if the section must be opened automatically *)
   | ClosedSection of bool * string * library_segment
@@ -36,7 +36,7 @@ let recalc_path_prefix () =
     | (sp, OpenedSection _) :: _ ->
 	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
     | _::l -> recalc l
-    | [] -> (match !module_name with Some m -> [m] | None -> [])
+    | [] -> (match !module_name with Some m -> m | None -> [])
   in
   path_prefix := recalc !lib_stk
 
@@ -120,7 +120,7 @@ let start_module s =
   module_name := Some s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
-  path_prefix := [s]
+  path_prefix := s
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
@@ -198,7 +198,7 @@ let is_section_p sp = dirpath_prefix_of sp !path_prefix
 
 (* State and initialization. *)
 
-type frozen = string option * library_segment
+type frozen = dir_path option * library_segment
 
 let freeze () = (!module_name, !lib_stk)
 
diff --git a/library/lib.mli b/library/lib.mli
index 35d8cf2acf..ed08bcc1d5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,7 +13,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | Module of string
+  | Module of dir_path
   | OpenedSection of string * Summary.frozen
   | ClosedSection of bool * string * library_segment
   | FrozenState of Summary.frozen
@@ -47,7 +47,7 @@ val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> dir_path
 val is_section_p : dir_path -> bool
 
-val start_module : string -> unit
+val start_module : dir_path -> unit
 val export_module : unit -> library_segment
 
 
diff --git a/library/library.ml b/library/library.ml
index b9f1b109a3..cd99b603e2 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -159,7 +159,8 @@ let rec load_module_from s f =
     List.iter (load_mandatory_module s) m.module_deps;
     Global.import m.module_compiled_env;
     load_objects m.module_declarations;
-    let sp = Names.make_path [] (id_of_string s) CCI in
+    let dir = parse_loadpath lpe.relative_subdir in
+    let sp = Names.make_path dir (id_of_string s) CCI in
     Nametab.push_module sp m.module_nametab;
     modules_table := Stringmap.add s m !modules_table;
     m
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 22c735e474..1fa038777a 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -253,8 +253,8 @@ let rec print_library_entry with_values ent =
     | (sp,Lib.ClosedSection _) -> 
         [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
 	   'fNL >]
-    | (_,Lib.Module str) ->
-	[< 'sTR(" >>>>>>> Module " ^ str); 'fNL >]
+    | (_,Lib.Module dir) ->
+	[< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >]
     | (_,Lib.FrozenState _) ->
 	[< >]
 	
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 83af309491..2e8ce398ee 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -670,7 +670,8 @@ let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)"
 let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)"
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("Init"::dir) (id_of_string s) CCI)
 
 let build_sigma_set () =
   { proj1 = constant ["Specif"] "projS1";
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cf9946b8e9..b1eb7b6efd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1527,8 +1527,8 @@ let contradiction_on_hyp id gl =
 let constant dir s = 
   Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
-let coq_False = lazy (constant ["Logic"] "False")
-let coq_not = lazy (constant ["Logic"] "not")
+let coq_False = lazy (constant ["Init";"Logic"] "False")
+let coq_not = lazy (constant ["Init";"Logic"] "not")
 
 (* Absurd *)
 let absurd c gls =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e94b73f180..3e34733f50 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -283,7 +283,10 @@ let _ =
   add "BeginModule"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   fun () -> Lib.start_module (string_of_id id)
+	   let s = string_of_id id in
+	   let {relative_subdir = dir},_ = 
+	     System.find_file_in_path (Library.get_load_path ()) (s^".v") in
+	   fun () -> Lib.start_module ((parse_loadpath dir)@[s])
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =