Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 260 insertions, 0 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
new file mode 100644
index 00000000..6d2064bf
--- /dev/null
+++ b/kernel/mod_subst.ml
@@ -0,0 +1,260 @@
+(************************************************************************)
+(*  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: mod_subst.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
+
+open Pp
+open Util
+open Names
+open Term
+
+(* WARNING: not every constant in the associative list domain used to exist
+   in the environment. This allows a simple implementation of the join
+   operation. However, iterating over the associative list becomes a non-sense
+*)
+type resolver = (constant * constr option) list
+
+let make_resolver resolve = resolve
+
+let apply_opt_resolver resolve kn =
+ match resolve with
+    None -> None
+  | Some resolve ->
+     try List.assoc kn resolve with Not_found -> assert false
+
+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)
+
+type substitution = (module_path * resolver option) Umap.t
+
+let empty_subst = Umap.empty
+
+let add_msid msid mp =
+  Umap.add (MSI msid) (mp,None)
+let add_mbid mbid mp resolve =
+  Umap.add (MBI mbid) (mp,resolve)
+
+let map_msid msid mp = add_msid msid mp empty_subst
+let map_mbid mbid mp resolve = add_mbid mbid mp resolve 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 subst_mp0 sub mp = (* 's like subst *)
+ let rec aux mp =
+  match mp with
+    | MPself sid -> 
+        let mp',resolve = Umap.find (MSI sid) sub in
+         mp',resolve
+    | MPbound bid ->
+        let mp',resolve = Umap.find (MBI bid) sub in
+         mp',resolve
+    | MPdot (mp1,l) -> 
+	let mp1',resolve = aux mp1 in
+	 MPdot (mp1',l),resolve
+    | _ -> raise Not_found
+ in
+  try Some (aux mp) with Not_found -> None
+
+let subst_mp sub mp =
+ match subst_mp0 sub mp with
+    None -> mp
+  | Some (mp',_) -> mp'
+
+
+let subst_kn0 sub kn =
+ let mp,dir,l = repr_kn kn in
+  match subst_mp0 sub mp with
+     Some (mp',_) ->
+      Some (make_kn mp' dir l)
+   | None -> None
+
+let subst_kn sub kn =
+ match subst_kn0 sub kn with
+    None -> kn
+  | Some kn' -> kn'
+
+let subst_con sub con =
+ let mp,dir,l = repr_con con in
+  match subst_mp0 sub mp with
+     None -> con,mkConst con
+   | Some (mp',resolve) ->
+      let con' = make_con mp' dir l in
+       match apply_opt_resolver resolve con with
+          None -> con',mkConst con'
+        | Some t -> con',t
+
+(* Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
+let subst_evaluable_reference subst = function
+  | EvalVarRef id -> EvalVarRef id
+  | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
+
+(* 
+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' c = 
+  let func = map_kn f f' in
+    match kind_of_term c with
+      | Const kn -> f' kn
+      | Ind (kn,i) -> 
+         (match f kn with
+             None -> c
+           | Some kn' ->
+	      mkInd (kn',i))
+      | Construct ((kn,i),j) -> 
+         (match f kn with
+             None -> c
+           | Some kn' ->
+	      mkConstruct ((kn',i),j))
+      | Case (ci,p,c,l) ->
+	  let ci' =
+           { ci with
+              ci_ind =
+               let (kn,i) = ci.ci_ind in
+                match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in
+	  mkCase (ci', func p, func c, array_smartmap func l) 
+      | _ -> map_constr func c
+
+let subst_mps sub = 
+  map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con))
+
+let rec replace_mp_in_mp mpfrom mpto mp =
+  match mp with
+    | _ when mp = mpfrom -> mpto
+    | MPdot (mp1,l) -> 
+	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+	  if mp1==mp1' then mp
+	  else MPdot (mp1',l)
+    | _ -> mp
+
+let replace_mp_in_con mpfrom mpto kn =
+ let mp,dir,l = repr_con kn in
+  let mp'' = replace_mp_in_mp mpfrom mpto mp in
+    if mp==mp'' then kn
+    else make_con mp'' dir l
+
+exception BothSubstitutionsAreIdentitySubstitutions
+exception ChangeDomain of resolver
+
+let join (subst1 : substitution) (subst2 : substitution) = 
+  let apply_subst (sub : substitution) key (mp,resolve) =
+   let mp',resolve' =
+    match subst_mp0 sub mp with
+       None -> mp, None
+     | Some (mp',resolve') -> mp',resolve' in
+   let resolve'' : resolver option =
+    try
+     let res =
+      match resolve with
+         Some res -> res
+       | None ->
+          match resolve' with
+             None -> raise BothSubstitutionsAreIdentitySubstitutions
+           | Some res -> raise (ChangeDomain res)
+     in
+      Some
+       (List.map
+         (fun (kn,topt) ->
+           kn,
+           match topt with
+              None ->
+               (match key with
+                   MSI msid ->
+                    let kn' = replace_mp_in_con (MPself msid) mp kn in
+                     apply_opt_resolver resolve' kn'
+                 | MBI mbid ->
+                    let kn' = replace_mp_in_con (MPbound mbid) mp kn in
+                     apply_opt_resolver resolve' kn')
+            | Some t -> Some (subst_mps sub t)) res)
+    with
+       BothSubstitutionsAreIdentitySubstitutions -> None
+     | ChangeDomain res ->
+        Some
+         ((List.map
+            (fun (kn,topt) ->
+              let key' =
+               match key with
+                  MSI msid -> MPself msid
+                | MBI mbid -> MPbound mbid in
+              (* let's replace mp with key in kn *)
+              let kn' = replace_mp_in_con mp key' kn in
+               kn',topt)) res)
+   in
+    mp',resolve'' in
+  let subst = Umap.mapi (apply_subst 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))