Names.substitution (and related functions) and Term.subst_mps moved to

the new module kernel/mod_subst.ml.

MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).


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

14 files changed, 226 insertions, 181 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1b93dc4b6..f1c662207 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -2,6 +2,7 @@ open Names
 open Term
 open Cbytecodes
 open Copcodes
+open Mod_subst
 
 (* Relocation information *)
 type reloc_info =
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 438da15dd..ca6da65e1 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -8,7 +8,7 @@ type reloc_info =
 
 type patch = reloc_info * int 
 (* A virer *)
-val subst_patch : substitution -> patch -> patch
+val subst_patch : Mod_subst.substitution -> patch -> patch
  
 type emitcodes 
 
@@ -18,7 +18,7 @@ val patch_int : emitcodes -> (*pos*)int -> int -> unit
 
 type to_patch = emitcodes * (patch list) * fv
 
-val subst_to_patch : substitution -> to_patch -> to_patch
+val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of bool*to_patch
@@ -34,7 +34,7 @@ val force : to_patch_substituted -> body_code
 
 val is_boxed : to_patch_substituted -> bool
 
-val subst_to_patch_subst : substitution -> to_patch_substituted -> to_patch_substituted
+val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted
 
 val to_memory : bytecodes * bytecodes * fv -> to_patch
                (* init code, fun code, fv *) 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b5505bce3..72f37e226 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -14,6 +14,7 @@ open Names
 open Univ
 open Term
 open Sign
+open Mod_subst
 (*i*)
 
 (* This module defines the types of global declarations. This includes
@@ -109,7 +110,7 @@ type mutual_inductive_body = {
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_body = option_app (subst_constr_subst sub) cb.const_body;
-    const_type = type_app (Term.subst_mps sub) cb.const_type;
+    const_type = type_app (subst_mps sub) cb.const_type;
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
@@ -119,17 +120,17 @@ let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
     mind_typename = mbp.mind_typename;
     mind_nf_lc = 
-      array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_nf_lc;
-    mind_nf_arity = type_app (Term.subst_mps sub) mbp.mind_nf_arity;
+      array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc;
+    mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity;
     mind_user_lc = 
-      array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_user_lc;
-    mind_user_arity = type_app (Term.subst_mps sub) mbp.mind_user_arity;
+      array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc;
+    mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity;
     mind_sort = mbp.mind_sort;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_kelim = mbp.mind_kelim;
     mind_nparams = mbp.mind_nparams;
     mind_params_ctxt = 
-      map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt;
+      map_rel_context (subst_mps sub) mbp.mind_params_ctxt;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
     mind_nb_constant = mbp.mind_nb_constant;
     mind_nb_args = mbp.mind_nb_args;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 50c866014..30c0ffde0 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,6 +14,7 @@ open Univ
 open Term
 open Cemitcodes
 open Sign
+open Mod_subst
 (*i*)
 
 (* This module defines the internal representation of global
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
new file mode 100644
index 000000000..ba186d06e
--- /dev/null
+++ b/kernel/mod_subst.ml
@@ -0,0 +1,149 @@
+(************************************************************************)
+(*  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$ *)
+
+open Pp
+open Util
+open Names
+open Term
+
+type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id
+
+let string_of_subst_domain = function
+   MSI msid -> debug_string_of_msid msid
+ | MBI mbid -> debug_string_of_mbid mbid
+
+module Umap = Map.Make(struct 
+			 type t = substitution_domain
+			 let compare = Pervasives.compare
+		       end)
+
+(* this is correct under the condition that bound and struct
+   identifiers can never be identical (i.e. get the same stamp)! *) 
+
+type substitution = module_path Umap.t
+
+let empty_subst = Umap.empty
+
+let add_msid sid = Umap.add (MSI sid)
+let add_mbid bid = Umap.add (MBI bid)
+
+let map_msid msid mp = add_msid msid mp empty_subst
+let map_mbid mbid mp = add_mbid mbid mp empty_subst
+
+let list_contents sub = 
+  let one_pair uid mp l =
+    (string_of_subst_domain uid, string_of_mp mp)::l
+  in
+    Umap.fold one_pair sub []
+
+let debug_string_of_subst sub = 
+  let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
+    "{" ^ String.concat "; " l ^ "}"
+
+let debug_pr_subst sub = 
+  let l = list_contents sub in
+  let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) 
+  in
+    str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
+
+let rec subst_mp sub mp = (* 's like subst *)
+  match mp with
+    | MPself sid -> 
+	(try Umap.find (MSI sid) sub with Not_found -> mp)
+    | MPbound bid ->
+	(try Umap.find (MBI bid) sub with Not_found -> mp)
+    | MPdot (mp1,l) -> 
+	let mp1' = subst_mp sub mp1 in
+	  if mp1==mp1' then 
+	    mp
+	  else
+	    MPdot (mp1',l)
+    | _ -> mp
+
+let join subst1 subst2 = 
+  let subst = Umap.map (subst_mp subst2) subst1 in
+  Umap.fold Umap.add subst2 subst
+
+let rec occur_in_path uid path =
+ match uid,path with
+  | MSI sid,MPself sid' -> sid = sid'
+  | MBI bid,MPbound bid' -> bid = bid'
+  | _,MPdot (mp1,_) -> occur_in_path uid mp1
+  | _ -> false
+    
+let occur_uid uid sub = 
+  let check_one uid' mp =
+    if uid = uid' || occur_in_path uid mp then raise Exit
+  in
+    try 
+      Umap.iter check_one sub;
+      false
+    with Exit -> true
+
+let occur_msid uid = occur_uid (MSI uid)
+let occur_mbid uid = occur_uid (MBI uid)
+    
+type 'a lazy_subst =
+  | LSval of 'a
+  | LSlazy of substitution * 'a
+	
+type 'a substituted = 'a lazy_subst ref
+      
+let from_val a = ref (LSval a)
+    
+let force fsubst r = 
+  match !r with
+  | LSval a -> a
+  | LSlazy(s,a) -> 
+      let a' = fsubst s a in
+      r := LSval a';
+      a' 
+
+let subst_substituted s r =
+  match !r with
+  | LSval a -> ref (LSlazy(s,a))
+  | LSlazy(s',a) ->
+      let s'' = join s' s in
+      ref (LSlazy(s'',a))
+
+let subst_kn sub kn =
+ let mp,dir,l = repr_kn kn in
+  let mp' = subst_mp sub mp in
+    if mp==mp' then kn else make_kn mp' dir l
+
+let subst_con sub con =
+ let mp,dir,l = repr_con con in
+  let mp' = subst_mp sub mp in
+    if mp==mp' then con else make_con mp' dir l
+
+(* 
+map_kn : (kernel_name -> kernel_name) -> constr -> constr
+
+This should be rewritten to prevent duplication of constr's when not
+necessary.
+For now, it uses map_constr and is rather ineffective
+*)
+
+let rec map_kn f f_con c = 
+  let func = map_kn f f_con in
+    match kind_of_term c with
+      | Const kn -> 
+	  mkConst (f_con kn)
+      | Ind (kn,i) -> 
+	  mkInd (f kn,i)
+      | Construct ((kn,i),j) -> 
+	  mkConstruct ((f kn,i),j)
+      | Case (ci,p,c,l) ->
+	  let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
+	  mkCase (ci', func p, func c, array_smartmap func l) 
+      | _ -> map_constr func c
+
+let subst_mps sub = 
+  map_kn (subst_kn sub) (subst_con sub)
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
new file mode 100644
index 000000000..fa37c2509
--- /dev/null
+++ b/kernel/mod_subst.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Names
+open Term
+
+(*s Substitutions *)
+
+type substitution
+
+val empty_subst : substitution
+
+val add_msid : 
+  mod_self_id -> module_path -> substitution -> substitution
+val add_mbid : 
+  mod_bound_id -> module_path -> substitution -> substitution
+
+val map_msid : mod_self_id -> module_path -> substitution
+val map_mbid : mod_bound_id -> module_path -> substitution
+
+(* sequential composition: 
+   [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
+*)
+val join : substitution -> substitution -> substitution
+
+type 'a substituted
+val from_val : 'a -> 'a substituted
+val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
+val subst_substituted : substitution -> 'a substituted -> 'a substituted
+
+(*i debugging *)
+val debug_string_of_subst : substitution -> string
+val debug_pr_subst : substitution -> Pp.std_ppcmds
+(*i*)
+
+(* [subst_mp sub mp] guarantees that whenever the result of the
+   substitution is structutally equal [mp], it is equal by pointers 
+   as well [==] *) 
+
+val subst_mp : 
+  substitution -> module_path -> module_path
+
+(* [occur_*id id sub] returns true iff [id] occurs in [sub] 
+   on either side *)
+
+val occur_msid : mod_self_id -> substitution -> bool
+val occur_mbid : mod_bound_id -> substitution -> bool
+
+val subst_kn : substitution -> kernel_name -> kernel_name
+val subst_con : substitution -> constant -> constant
+
+(* [subst_mps sub c] performs the substitution [sub] on all kernel
+   names appearing in [c] *)
+val subst_mps : substitution -> constr -> constr
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 9f5a5e9a8..9ab200ad1 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -17,6 +17,7 @@ open Environ
 open Term_typing
 open Modops
 open Subtyping
+open Mod_subst
 
 exception Not_path
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index aca663e7c..9aba4d560 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -17,6 +17,7 @@ open Term
 open Declarations
 open Environ
 open Entries
+open Mod_subst
 (*i*)
 
 let error_existing_label l = 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f92c6bf04..0e1d9cd34 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -15,6 +15,7 @@ open Univ
 open Environ
 open Declarations
 open Entries
+open Mod_subst
 (*i*)
 
 (* Various operations on modules and module types *)
diff --git a/kernel/names.ml b/kernel/names.ml
index db1b1b6df..e15d4ab2f 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -138,95 +138,6 @@ end
 module MPset = Set.Make(MPord)
 module MPmap = Map.Make(MPord)
 
-
-(* this is correct under the condition that bound and struct
-   identifiers can never be identical (i.e. get the same stamp)! *) 
-
-type substitution = module_path Umap.t
-
-let empty_subst = Umap.empty
-
-let add_msid = Umap.add 
-let add_mbid = Umap.add
-
-let map_msid msid mp = add_msid msid mp empty_subst
-let map_mbid mbid mp = add_msid mbid mp empty_subst
-
-let list_contents sub = 
-  let one_pair uid mp l =
-    (string_of_uid uid, string_of_mp mp)::l
-  in
-    Umap.fold one_pair sub []
-
-let debug_string_of_subst sub = 
-  let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
-    "{" ^ String.concat "; " l ^ "}"
-
-let debug_pr_subst sub = 
-  let l = list_contents sub in
-  let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) 
-  in
-    str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
-
-let rec subst_mp sub mp = (* 's like subst *)
-  match mp with
-    | MPself sid -> 
-	(try Umap.find sid sub with Not_found -> mp)
-    | MPbound bid ->
-	(try Umap.find bid sub with Not_found -> mp)
-    | MPdot (mp1,l) -> 
-	let mp1' = subst_mp sub mp1 in
-	  if mp1==mp1' then 
-	    mp
-	  else
-	    MPdot (mp1',l)
-    | _ -> mp
-
-let join subst1 subst2 = 
-  let subst = Umap.map (subst_mp subst2) subst1 in
-  Umap.fold Umap.add subst2 subst
-
-let rec occur_in_path uid = function
-  | MPself sid -> sid = uid
-  | MPbound bid -> bid = uid
-  | MPdot (mp1,_) -> occur_in_path uid mp1
-  | _ -> false
-    
-let occur_uid uid sub = 
-  let check_one uid' mp =
-    if uid = uid' || occur_in_path uid mp then raise Exit
-  in
-    try 
-      Umap.iter check_one sub;
-      false
-    with Exit -> true
-
-let occur_msid = occur_uid
-let occur_mbid = occur_uid
-    
-type 'a lazy_subst =
-  | LSval of 'a
-  | LSlazy of substitution * 'a
-	
-type 'a substituted = 'a lazy_subst ref
-      
-let from_val a = ref (LSval a)
-    
-let force fsubst r = 
-  match !r with
-  | LSval a -> a
-  | LSlazy(s,a) -> 
-      let a' = fsubst s a in
-      r := LSval a';
-      a' 
-
-let subst_substituted s r =
-  match !r with
-  | LSval a -> ref (LSlazy(s,a))
-  | LSlazy(s',a) ->
-      let s'' = join s' s in
-      ref (LSlazy(s'',a))
-
 (* Kernel names *)
 
 type kernel_name = module_path * dir_path * label
@@ -246,11 +157,6 @@ let string_of_kn (mp,dir,l) =
 let pr_kn kn = str (string_of_kn kn)
 
 
-let subst_kn sub (mp,dir,l as kn) = 
-  let mp' = subst_mp sub mp in
-    if mp==mp' then kn else (mp',dir,l)
-
-
 let kn_ord kn1 kn2 = 
     let mp1,dir1,l1 = kn1 in
     let mp2,dir2,l2 = kn2 in
@@ -298,7 +204,6 @@ let string_of_con = string_of_kn
 let con_label = label
 let pr_con = pr_kn
 let con_modpath = modpath
-let subst_con = subst_kn
 
 let ith_mutual_inductive (kn,_) i = (kn,i)
 let ith_constructor_of_inductive ind i = (ind,i)
diff --git a/kernel/names.mli b/kernel/names.mli
index 8cda7d958..4350b231a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -83,50 +83,6 @@ val string_of_mp : module_path -> string
 module MPset : Set.S with type elt = module_path
 module MPmap : Map.S with type key = module_path
 
-
-(*s Substitutions *)
-
-type substitution
-
-val empty_subst : substitution
-
-val add_msid : 
-  mod_self_id -> module_path -> substitution -> substitution
-val add_mbid : 
-  mod_bound_id -> module_path -> substitution -> substitution
-
-val map_msid : mod_self_id -> module_path -> substitution
-val map_mbid : mod_bound_id -> module_path -> substitution
-
-(* sequential composition: 
-   [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
-*)
-val join : substitution -> substitution -> substitution
-
-type 'a substituted
-val from_val : 'a -> 'a substituted
-val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
-val subst_substituted : substitution -> 'a substituted -> 'a substituted
-
-(*i debugging *)
-val debug_string_of_subst : substitution -> string
-val debug_pr_subst : substitution -> Pp.std_ppcmds
-(*i*)
-
-(* [subst_mp sub mp] guarantees that whenever the result of the
-   substitution is structutally equal [mp], it is equal by pointers 
-   as well [==] *) 
-
-val subst_mp : 
-  substitution -> module_path -> module_path
-
-(* [occur_*id id sub] returns true iff [id] occurs in [sub] 
-   on either side *)
-
-val occur_msid : mod_self_id -> substitution -> bool
-val occur_mbid : mod_bound_id -> substitution -> bool
-     
-
 (* Name of the toplevel structure *)
 val initial_msid : mod_self_id
 val initial_path : module_path (* [= MPself initial_msid] *)
@@ -147,7 +103,6 @@ val label : kernel_name -> label
 
 val string_of_kn : kernel_name -> string
 val pr_kn : kernel_name -> Pp.std_ppcmds
-val subst_kn : substitution -> kernel_name -> kernel_name
 
 
 module KNset  : Set.S with type elt = kernel_name
@@ -176,7 +131,6 @@ val string_of_con : constant -> string
 val con_label : constant -> label
 val con_modpath : constant -> module_path
 val pr_con : constant -> Pp.std_ppcmds
-val subst_con : substitution -> constant -> constant
 
 val ith_mutual_inductive : inductive -> int -> inductive
 val ith_constructor_of_inductive : inductive -> int -> constructor
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2f39dc61a..383f7c2c9 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -18,6 +18,7 @@ open Environ
 open Reduction
 open Inductive
 open Modops
+open Mod_subst
 (*i*)
 
 (* This local type is used to subtype a constant with a constructor or
diff --git a/kernel/term.ml b/kernel/term.ml
index 21ab2ea5d..65bf7a565 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -790,32 +790,6 @@ let substn_vars p vars =
 
 let subst_vars = substn_vars 1
 
-(* 
-map_kn : (kernel_name -> kernel_name) -> constr -> constr
-
-This should be rewritten to prevent duplication of constr's when not
-necessary.
-For now, it uses map_constr and is rather ineffective
-*)
-
-let rec map_kn f f_con c = 
-  let func = map_kn f f_con in
-    match kind_of_term c with
-      | Const kn -> 
-	  mkConst (f_con kn)
-      | Ind (kn,i) -> 
-	  mkInd (f kn,i)
-      | Construct ((kn,i),j) -> 
-	  mkConstruct ((f kn,i),j)
-      | Case (ci,p,c,l) ->
-	  let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
-	  mkCase (ci', func p, func c, array_smartmap func l) 
-      | _ -> map_constr func c
-
-let subst_mps sub = 
-  map_kn (subst_kn sub) (subst_con sub)
-
-
 (*********************)
 (* Term constructors *)
 (*********************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 2b84f79ba..c9ac9419c 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -460,11 +460,6 @@ val subst_vars : identifier list -> constr -> constr
 val substn_vars : int -> identifier list -> constr -> constr
 
 
-(* [subst_mps sub c] performs the substitution [sub] on all kernel
-   names appearing in [c] *)
-val subst_mps : substitution -> constr -> constr
-
-
 (*s Functionals working on the immediate subterm of a construction *)
 
 (* [fold_constr f acc c] folds [f] on the immediate subterms of [c]