This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



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

1 files changed, 91 insertions, 92 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index 359e3fe7f..8076e252c 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,100 +1,99 @@
-(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
 
-(* $Id$ *)
 
-(* This file implements the basic structure of what Chet called
-   ``discrimination nets''. If my understanding is right, it serves
-   to associate actions (for example, tactics) with a priority to term
-   patterns, so that if a hypothesis matches a pattern in the net,
-   then the associated tactic is applied. Discrimination nets are used
-   (only) to implement the tactics Auto, DHyp and Point.
 
-   A discrimination net is a tries structure, that is, a tree structure
-   specially conceived for searching patterns, like for example strings
-   --see the file Tlm.ml in the directory lib/util--. Here the tries
-   structure are used for looking for term patterns.
 
-   This module is then used in :
-     - termdn.ml   (discrimination nets of terms);
-     - btermdn.ml  (discrimination nets of terms with bounded depth,
-                    used in the tactic auto);
-     - nbtermdn.ml (named discrimination nets with bounded depth, used
-                    in the tactics Dhyp and Point).
-  Eduardo (4/8/97) *)
 
-(* Definition of the basic structure *)
-
-type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option
-
-type 'res lookup_res = Label of 'res | Nothing | Everything
-
-type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res
-
-type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t
-
-let create () = Tlm.empty
-
-(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
+module Make = 
+  functor (X : Set.OrderedType) ->
+    functor (Y : Map.OrderedType) ->
+      functor (Z : Map.OrderedType) ->
+struct
+  
+  module Y_tries = struct
+    type t = (Y.t * int) option
+    let compare x y = 
+      match x,y with
+	  None,None -> 0
+	| Some (l,n),Some (l',n') -> 
+	    if (Y.compare l l') = 0 && n = n' then 0 
+	    else Pervasives.compare x y
+	| a,b -> Pervasives.compare a b 
+  end
+  module X_tries = struct
+    type t = X.t * Z.t
+    let compare (x1,x2) (y1,y2) = 
+	    if (X.compare x1 y1) = 0 && (Z.compare x2 y2)=0 then 0 
+	    else Pervasives.compare (x1,x2) (y1,y2)
+  end
+
+  module T = Tries.Make(X_tries)(Y_tries)
+    
+  type  decompose_fun = X.t -> (Y.t * X.t list) option
+    
+  type 'res lookup_res = Label of 'res | Nothing | Everything
+    
+  type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
+
+  type  t = T.t
+
+  let create () = T.empty
+
+(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in 
 prefix ordering, [dna] is the function returning the main node of a pattern *)
 
-let path_of dna =
-  let rec path_of_deferred = function
-    | [] -> []
-    | h::tl -> pathrec tl h
-
-  and pathrec deferred t =
-    match dna t with
-    | None ->
-	None :: (path_of_deferred deferred)
-    | Some (lbl,[]) ->
-	(Some (lbl,0))::(path_of_deferred deferred)
-    | Some (lbl,(h::def_subl as v)) ->
-	(Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
-  in
-  pathrec []
-
-let tm_of tm lbl =
-  try [Tlm.map tm lbl, true] with Not_found -> []
-
-let rec skip_arg n tm =
-  if n = 0 then [tm,true]
-  else
-    List.flatten
-      (List.map
-	  (fun a -> match a with
-	  | None -> skip_arg (pred n) (Tlm.map tm a)
-	  | Some (lbl,m) ->
-	      skip_arg (pred n + m) (Tlm.map tm a))
-	  (Tlm.dom tm))
-
-let lookup tm dna t =
-  let rec lookrec t tm =
-    match dna t with
-    | Nothing -> tm_of tm None
-    | Label(lbl,v) ->
-	tm_of tm None@
-	  (List.fold_left
-	      (fun l c ->
+  let path_of dna =
+    let rec path_of_deferred = function
+      | [] -> []
+      | h::tl -> pathrec tl h
+	  
+    and pathrec deferred t =
+      match dna t with
+	| None -> 
+	    None :: (path_of_deferred deferred)
+	| Some (lbl,[]) ->
+	    (Some (lbl,0))::(path_of_deferred deferred)
+	| Some (lbl,(h::def_subl as v)) ->
+	    (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+    in 
+      pathrec []
+	
+  let tm_of tm lbl =
+    try [T.map tm lbl, true] with Not_found -> []
+      
+  let rec skip_arg n tm =
+    if n = 0 then [tm,true]
+    else
+      List.flatten 
+	(List.map 
+	   (fun a -> match a with
+	      | None -> skip_arg (pred n) (T.map tm a)
+	      | Some (lbl,m) -> 
+		  skip_arg (pred n + m) (T.map tm a)) 
+	   (T.dom tm))
+	
+  let lookup tm dna t =
+    let rec lookrec t tm =
+      match dna t with
+	| Nothing -> tm_of tm None
+	| Label(lbl,v) ->
+	    tm_of tm None@
+	      (List.fold_left 
+		 (fun l c -> 
 		List.flatten(List.map (fun (tm, b) ->
-		  if b then lookrec c tm
-		  else [tm,b]) l))
-              (tm_of tm (Some(lbl,List.length v))) v)
-    | Everything -> skip_arg 1 tm
-  in
-    List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm))
-
-let add tm dna (pat,inf) =
-  let p = path_of dna pat in Tlm.add tm (p,(pat,inf))
-
-let rmv tm dna (pat,inf) =
-  let p = path_of dna pat in Tlm.rmv tm (p,(pat,inf))
-
-let app f tm = Tlm.app (fun (_,p) -> f p) tm
-
+					 if b then lookrec c tm
+					 else [tm,b]) l))
+		 (tm_of tm (Some(lbl,List.length v))) v)
+	| Everything -> skip_arg 1 tm
+    in 
+      List.flatten (List.map (fun (tm,b) -> T.xtract tm) (lookrec t tm))
+	
+  let add tm dna (pat,inf) =
+    let p = path_of dna pat in T.add tm (p,(pat,inf))
+				 
+  let rmv tm dna (pat,inf) =
+  let p = path_of dna pat in T.rmv tm (p,(pat,inf))
+			       
+  let app f tm = T.app (fun (_,p) -> f p) tm
+    
+end
+