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, 121 insertions, 59 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index e28a9e3c3..198ee7859 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -20,71 +20,133 @@ open Libnames
 
 let dnet_depth = ref 8
 
-let bounded_constr_pat_discr_st st (t,depth) =
-  if depth = 0 then
-    None
-  else
-    match constr_pat_discr_st st t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
 
-let bounded_constr_val_discr_st st (t,depth) =
-  if depth = 0 then
-    Dn.Nothing
-  else
-    match constr_val_discr_st st t with
-      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
-      | Dn.Nothing -> Dn.Nothing
-      | Dn.Everything -> Dn.Everything
+module Make =
+  functor (Z : Map.OrderedType) ->
+struct
+  module Term_dn = Termdn.Make(Z)
 
-let bounded_constr_pat_discr (t,depth) =
-  if depth = 0 then
-    None
-  else
-    match constr_pat_discr t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+  module X = struct
+    type t = constr_pattern*int
+    let compare = Pervasives.compare 
+  end
 
-let bounded_constr_val_discr (t,depth) =
-  if depth = 0 then
-    Dn.Nothing
-  else
-    match constr_val_discr t with
-      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
-      | Dn.Nothing -> Dn.Nothing
-      | Dn.Everything -> Dn.Everything
+ module Y = struct 
+     type t = Term_dn.term_label
+     let compare x y = 
+       let make_name n =
+	 match n with
+	 | Term_dn.GRLabel(ConstRef con) -> 
+	     Term_dn.GRLabel(ConstRef(constant_of_kn(canonical_con con)))
+	 | Term_dn.GRLabel(IndRef (kn,i)) ->
+	     Term_dn.GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
+	 | Term_dn.GRLabel(ConstructRef ((kn,i),j ))->
+	     Term_dn.GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
+	 | k -> k
+       in
+	 Pervasives.compare (make_name x) (make_name y)
+ end
+ 
+ module Dn = Dn.Make(X)(Y)(Z)
+  
+ type t = Dn.t
 
-type 'a t = (term_label,constr_pattern * int,'a) Dn.t
+  let create = Dn.create
 
-let create = Dn.create
+  let decomp = 
+    let rec decrec acc c = match kind_of_term c with
+      | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+      | Cast (c1,_,_) -> decrec acc c1
+      | _ -> (c,acc)
+    in 
+      decrec []
 
-let add = function
-  | None ->
-      (fun dn (c,v) ->
-	Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-  | Some st ->
-      (fun dn (c,v) ->
-	Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+  let constr_val_discr t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Const _ -> Dn.Everything
+    | _ -> Dn.Nothing
 
-let rmv = function
-  | None ->
-      (fun dn (c,v) ->
-	Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-  | Some st ->
-      (fun dn (c,v) ->
-	Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+let constr_val_discr_st (idpred,cpred) t =
+  let c, l = decomp t in
+    match kind_of_term c with
+    | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
+    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+    | Evar _ -> Dn.Everything
+    | _ -> Dn.Nothing
 
-let lookup = function
-  | None ->
-      (fun dn t ->
-	List.map
-	  (fun ((c,_),v) -> (c,v))
-	  (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)))
-  | Some st ->
-      (fun dn t ->
-	List.map
-	  (fun ((c,_),v) -> (c,v))
-	  (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)))
-
-let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
+  let bounded_constr_pat_discr_st st (t,depth) =
+    if depth = 0 then 
+      None 
+    else
+      match Term_dn.constr_pat_discr_st st t with
+	| None -> None
+	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+  let bounded_constr_val_discr_st st (t,depth) =
+    if depth = 0 then 
+      Dn.Nothing 
+    else
+      match constr_val_discr_st st t with
+	| Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+	| Dn.Nothing -> Dn.Nothing
+	| Dn.Everything -> Dn.Everything
 
+  let bounded_constr_pat_discr (t,depth) =
+    if depth = 0 then 
+      None 
+    else
+      match Term_dn.constr_pat_discr t with
+	| None -> None
+	| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+  let bounded_constr_val_discr (t,depth) =
+    if depth = 0 then 
+      Dn.Nothing 
+    else
+      match constr_val_discr t with
+	| Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+	| Dn.Nothing -> Dn.Nothing
+	| Dn.Everything -> Dn.Everything
+	    
+	    
+  let add = function
+    | None -> 
+	(fun dn (c,v) -> 
+	   Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+    | Some st -> 
+	(fun dn (c,v) -> 
+	   Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+	  
+  let rmv = function
+    | None -> 
+	(fun dn (c,v) -> 
+	   Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+    | Some st -> 
+	(fun dn (c,v) -> 
+	 Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+	  
+  let lookup = function
+    | None -> 
+	(fun dn t ->
+	   List.map 
+	     (fun ((c,_),v) -> (c,v)) 
+	     (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)))
+    | Some st -> 
+	(fun dn t ->
+	   List.map 
+	     (fun ((c,_),v) -> (c,v)) 
+	     (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)))
+	  
+  let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
+    
+end
+