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

5 files changed, 87 insertions, 57 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 3aa20400a..f2fe3be86 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -207,6 +207,22 @@ let kind_of_string = function
   | _ -> invalid_arg "kind_of_string"
 
 (*s Directory paths = section names paths *)
+let parse_fields 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
+      (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_of_string id)
+
 type module_ident = identifier
 type dir_path = module_ident list
 
@@ -218,44 +234,43 @@ module ModIdOrdered =
 
 module ModIdmap = Map.Make(ModIdOrdered)
 
-let make_dirpath x = x
-let repr_dirpath x = x
+(* These are the only functions which depend on how a dirpath is encoded *)
+let make_dirpath x = List.rev x
+let repr_dirpath x = List.rev x
+let rev_repr_dirpath x = x
 
 let dirpath_prefix = function 
   | [] -> anomaly "dirpath_prefix: empty dirpath"
-  | l -> snd (list_sep_last l)
+  | _::l -> l
 
-let split_dirpath d = let (b,d) = list_sep_last d in (d,b)
+let split_dirpath = function
+  | [] -> failwith "Empty"
+  | d::b -> (b,d)
 
-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
-      (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_of_string id)
+let extend_dirpath d id = id::d
+let add_dirpath_prefix id d = d@[id]
+
+let is_dirpath_prefix_of d1 d2 = list_prefix_of (List.rev d1) (List.rev d2)
+(**)
+
+let is_empty_dirpath d = (d = [])
 
 let dirpath_of_string s =
   try
-    let sl,s = parse_sp s in
-    sl @ [s]
+    let sl,s = parse_fields s in
+    make_dirpath (sl @ [s])
   with
     | Invalid_argument _ -> invalid_arg "dirpath_of_string"
 
 let string_of_dirpath = function
   | [] -> "<empty>"
-  | sl -> String.concat "." (List.map string_of_id sl)
+  | sl -> String.concat "." (List.map string_of_id (repr_dirpath sl))
 
 let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
 
+let default_module_name = id_of_string "Top"
+let default_module = make_dirpath [default_module_name]
+
 (*s Section paths are absolute names *)
 
 type section_path = {
@@ -278,20 +293,13 @@ let string_of_path sp =
 
 let path_of_string s =
   try
-    let sl,s = parse_sp s in
-    make_path sl s CCI
+    let sl,s = parse_fields s in
+    make_path (make_dirpath sl) s CCI
   with
     | 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 bn OBJ
-
-let wd_of_sp sp = 
-  let (sp,id,_) = repr_path sp in sp @ [id]
-
 let sp_ord sp1 sp2 =
   let (p1,id1,k) = repr_path sp1
   and (p2,id2,k') = repr_path sp2 in
@@ -302,8 +310,6 @@ let sp_ord sp1 sp2 =
   else
     ck
 
-let is_dirpath_prefix_of = list_prefix_of
-
 module SpOrdered =
   struct
     type t = section_path
@@ -345,6 +351,15 @@ module Hname = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
+module Hdir = Hashcons.Make(
+  struct 
+    type t = dir_path
+    type u = identifier -> identifier
+    let hash_sub hident d = List.map hident d
+    let equal d1 d2 = List.for_all2 (==) d1 d2
+    let hash = Hashtbl.hash
+  end)
+
 module Hsp = Hashcons.Make(
   struct 
     type t = section_path
@@ -364,6 +379,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 hdir = Hashcons.simple_hcons Hdir.f hident in
   let hspcci = Hashcons.simple_hcons Hsp.f hident in
-  let hspfw = Hashcons.simple_hcons Hsp.f hident in
-  (hspcci,hspfw,hname,hident,hstring)
+  (hspcci,hdir,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
index a50dc28c4..478b1c8e4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -63,12 +63,14 @@ val kind_of_string : string -> path_kind
 
 (*s Directory paths = section names paths *)
 type module_ident = identifier
-type dir_path = module_ident list
+type dir_path (*= module_ident list*)
 
 module ModIdmap : Map.S with type key = module_ident
 
 val make_dirpath : module_ident list -> dir_path
 val repr_dirpath : dir_path -> module_ident list
+val rev_repr_dirpath : dir_path -> module_ident list
+val is_empty_dirpath : dir_path -> bool
 
 (* Give the immediate prefix of a [dir_path] *)
 val dirpath_prefix : dir_path -> dir_path 
@@ -76,10 +78,14 @@ val dirpath_prefix : dir_path -> dir_path
 (* Give the immediate prefix and basename of a [dir_path] *)
 val split_dirpath : dir_path -> dir_path * identifier
 
+val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 val pr_dirpath : dir_path -> std_ppcmds
 
+val default_module : dir_path
 
 (*s Section paths are {\em absolute} names *)
 type section_path
@@ -93,9 +99,6 @@ val dirpath : section_path -> dir_path
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
-val sp_of_wd : module_ident list -> section_path
-val wd_of_sp : section_path -> module_ident list
-
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
@@ -128,5 +131,5 @@ type global_reference =
 
 (* Hash-consing *)
 val hcons_names : unit ->
-  (section_path -> section_path) * (section_path -> section_path) *
+  (section_path -> section_path) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
diff --git a/kernel/term.ml b/kernel/term.ml
index ea720dbd3..96a4d0d38 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -246,6 +246,17 @@ let hcons_term (hsorts,hsp,hname,hident) =
 (* Constructs a DeBrujin index with number n *)
 let mkRel   n = IsRel n
 
+let r = ref None
+
+let mkRel n =
+  let rels = match !r with
+    | None -> let a = 
+  [|mkRel  1;mkRel  2;mkRel  3;mkRel  4;mkRel  5;mkRel  6;mkRel  7; mkRel  8;
+    mkRel  9;mkRel 10;mkRel 11;mkRel 12;mkRel 13;mkRel 14;mkRel 15; mkRel 16|]
+      in r := Some a; a
+    | Some a -> a in
+  if 0<n & n<=16 then rels.(n-1) else mkRel n
+
 (* Constructs an existential variable named "?n" *)
 let mkMeta  n =  IsMeta n
 
@@ -254,6 +265,7 @@ let mkVar id = IsVar id
 
 (* Construct a type *)
 let mkSort s = IsSort s
+
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
 (* (that means t2 is declared as the type of t1) *)
 let mkCast (t1,t2) =
@@ -1001,10 +1013,13 @@ let mkMeta = mkMeta
 let mkVar = mkVar
 
 (* Construct a type *)
-let mkSort   = mkSort
 let mkProp   = mkSort mk_Prop
 let mkSet    = mkSort mk_Set
 let mkType u = mkSort (Type u)
+let mkSort   = function
+  | Prop Null -> mkProp (* Easy sharing *)
+  | Prop Pos -> mkSet
+  | s -> mkSort s
 
 let prop = mk_Prop
 and spec = mk_Set
@@ -1651,22 +1666,20 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
+let hcons_constr (hspcci,hdir,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  let hsortsfw = Hashcons.simple_hcons hsort hcons1_univ in
   let hcci = hcons_term (hsortscci,hspcci,hname,hident) in
-  let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
-  (hcci,hfw,htcci)
+  (hcci,htcci)
 
 let hcons1_constr =
   let hnames = hcons_names () in
-  let (hc,_,_) = hcons_constr hnames in
+  let (hc,_) = hcons_constr hnames in
   hc
 
 let hcons1_types =
   let hnames = hcons_names () in
-  let (_,_,ht) = hcons_constr hnames in
+  let (_,ht) = hcons_constr hnames in
   ht
 
 (* Abstract decomposition of constr to deal with generic functions *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 418ce2236..90b1dd807 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -641,13 +641,12 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 
 val hcons_constr:
   (section_path -> section_path) *
-  (section_path -> section_path) *
+  (dir_path -> dir_path) *
   (name -> name) *
   (identifier -> identifier) *
   (string -> string) 
   ->
     (constr -> constr) *
-    (constr -> constr) *
     (types -> types)
 
 val hcons1_constr : constr -> constr
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 915092b2e..a74ea74fb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -67,7 +67,7 @@ let implicit_univ =
     { u_mod = Names.make_dirpath [Names.id_of_string "implicit_univ"];
       u_num = 0 }
 
-let current_module = ref []
+let current_module = ref Names.default_module
 
 let set_module m = current_module := m
 
@@ -461,12 +461,12 @@ module Huniv =
   Hashcons.Make(
     struct
       type t = universe
-      type u = Names.identifier -> Names.identifier
-      let hash_aux hstr {u_mod=sp; u_num=n} = {u_mod=List.map hstr sp; u_num=n}
-      let hash_sub hstr = function
-	| Variable u -> Variable (hash_aux hstr u)
+      type u = Names.dir_path -> Names.dir_path
+      let hash_aux hdir {u_mod=sp; u_num=n} = {u_mod = hdir sp; u_num = n}
+      let hash_sub hdir = function
+	| Variable u -> Variable (hash_aux hdir u)
 	| Max (gel,gtl) ->
-	    Max (List.map (hash_aux hstr) gel, List.map (hash_aux hstr) gtl)
+	    Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl)
       let equal u v =
 	match u, v with
 	  | Variable u, Variable v -> u == v
@@ -477,6 +477,6 @@ module Huniv =
     end)
 
 let hcons1_univ u =
-  let _,_,_,hid,_ = Names.hcons_names () in
-  Hashcons.simple_hcons Huniv.f hid u
+  let _,hdir,_,_,_ = Names.hcons_names () in
+  Hashcons.simple_hcons Huniv.f hdir u