portage Correctness (substitutivité pour les modules)

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

3 files changed, 32 insertions, 5 deletions

diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 568253864d..6d96df032a 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -110,13 +110,17 @@ let add_pgm id p = pgm_table := Idmap.add id p !pgm_table
 let cache_global (_,(id,v,p)) =
   env := Env.add id v !env; add_pgm id p
 
+let type_info_app f = function Set -> Set | TypeV v -> TypeV (f v)
+
+let subst_global (_,s,(id,v,p)) = (id, type_info_app (type_v_knsubst s) v, p)
+
 let (inProg,outProg) =
   declare_object { object_name = "programs-objects";
                    cache_function = cache_global;
                    load_function = (fun _ -> cache_global);
                    open_function = (fun _ _ -> ());
-		   classify_function = (fun _ -> Dispose);
-		   subst_function = (fun (_,_,x) -> x);
+		   classify_function = (fun (_,x) -> Substitute x);
+		   subst_function = subst_global;
 		   export_function = (fun x -> Some x) }
 
 let is_mutable = function Ref _ | Array _ -> true | _ -> false
@@ -174,14 +178,16 @@ let all_refs () =
 let cache_init (_,(id,c)) =
   init_table := Idmap.add id c !init_table
 
+let subst_init (_,s,(id,c)) = (id, subst_mps s c)
+
 let (inInit,outInit) =
   declare_object { object_name = "programs-objects-init";
                    cache_function = cache_init;
                    load_function = (fun _ -> cache_init);
 		   open_function = (fun _ _-> ());
-		   classify_function = (fun _ -> Dispose);
-		   subst_function = (fun (_,_,x) -> x);
-                   export_function = fun x -> Some x }
+		   classify_function = (fun (_,x) -> Substitute x);
+		   subst_function = subst_init;
+                   export_function = (fun x -> Some x) }
 
 let initialize id c = Lib.add_anonymous_leaf (inInit (id,c))
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 2772b9f7a8..bb660ddb4c 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Pp
+open Util
 open Coqast
 open Names
 open Nameops
@@ -185,4 +186,20 @@ let rec n_lambda v = function
 
 let abstract ids c = n_lambda c (List.rev ids)
 
+(* substitutivity (of kernel names, for modules management) *)
 
+open Ptype
+
+let rec type_v_knsubst s = function
+  | Ref v -> Ref (type_v_knsubst s v)
+  | Array (c, v) -> Array (subst_mps s c, type_v_knsubst s v)
+  | Arrow (bl, c) -> Arrow (List.map (binder_knsubst s) bl, type_c_knsubst s c)
+  | TypePure c -> TypePure (subst_mps s c)
+
+and type_c_knsubst s ((id,v),e,pl,q) =
+  ((id, type_v_knsubst s v), e, 
+   List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
+   option_app (fun q -> { q with a_value = subst_mps s q.a_value }) q)
+
+and binder_knsubst s (id,b) = 
+  (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index 393141233a..207e74b2be 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -12,6 +12,7 @@
 
 open Names
 open Term
+open Ptype
 
 (* Some misc. functions *)
 
@@ -68,6 +69,9 @@ val n_mkNamedProd : constr -> (identifier * constr) list -> constr
 val n_lambda  : constr -> (identifier * constr) list -> constr
 val abstract : (identifier * constr) list -> constr -> constr
 
+val type_v_knsubst : substitution -> type_v -> type_v
+val type_c_knsubst : substitution -> type_c -> type_c
+
 (* for debugging purposes *)
 
 val deb_mess : Pp.std_ppcmds -> unit