Mod_subst: misc reformulations

 * Remove the mind_of_delta and constant_of_delta functions,
   prefer instead the {mind,constant}_of_delta_kn functions.

 * Attempt to make subst_ind and subst_con0 more self-contained

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

1 files changed, 46 insertions, 56 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 303c65c38..65052d0ed 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -161,6 +161,8 @@ let find_prefix resolve mp =
   in
   try sub_mp mp with Not_found -> mp
 
+(** Applying a resolver to a kernel name *)
+
 exception Change_equiv_to_inline of (int * constr)
 
 let solve_delta_kn resolve kn =
@@ -181,33 +183,23 @@ let kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
   with _ -> kn
 
-let constant_of_delta_kn resolve kn =
-  constant_of_kn_equiv kn (kn_of_delta resolve kn)
+(** Try a 1st resolver, and then a 2nd in case it had no effect *)
 
-let gen_of_delta resolve x kn fix_can =
-  try
-    let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then x else fix_can new_kn
-  with _ -> x
+let kn_of_deltas resolve1 resolve2 kn =
+  let kn' = kn_of_delta resolve1 kn in
+  if kn' == kn then kn_of_delta resolve2 kn else kn'
 
-let constant_of_delta resolve con =
-  let kn = user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+let constant_of_delta_kn resolve kn =
+  constant_of_kn_equiv kn (kn_of_delta resolve kn)
 
-let constant_of_delta2 resolve con =
-  let kn, kn' = canonical_con con, user_con con in
-  gen_of_delta resolve con kn (constant_of_kn_equiv kn')
+let constant_of_deltas_kn resolve1 resolve2 kn =
+  constant_of_kn_equiv kn (kn_of_deltas resolve1 resolve2 kn)
 
 let mind_of_delta_kn resolve kn =
   mind_of_kn_equiv kn (kn_of_delta resolve kn)
 
-let mind_of_delta resolve mind =
-  let kn = user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
-
-let mind_of_delta2 resolve mind =
-  let kn, kn' = canonical_mind mind, user_mind mind in
-  gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
+let mind_of_deltas_kn resolve1 resolve2 kn =
+  mind_of_kn_equiv kn (kn_of_deltas resolve1 resolve2 kn)
 
 let inline_of_delta inline resolver =
   match inline with
@@ -220,18 +212,16 @@ let inline_of_delta inline resolver =
       in
       Deltamap.fold_kn extract resolver []
 
-let find_inline_of_delta kn resolve =
-  match Deltamap.find_kn kn resolve with
+let search_delta_inline resolve kn1 kn2 =
+  let find kn = match Deltamap.find_kn kn resolve with
     | Inline (_,o) -> o
-    | _ -> raise Not_found
-
-let constant_of_delta_with_inline resolve con =
-  let kn1,kn2 = canonical_con con,user_con con in
-  try find_inline_of_delta kn2 resolve
+    | Equiv _ -> raise Not_found
+  in
+  try find kn1
   with Not_found ->
     if kn1 == kn2 then None
     else
-      try find_inline_of_delta kn1 resolve
+      try find kn2
       with Not_found -> None
 
 let subst_mp0 sub mp = (* 's like subst *)
@@ -275,48 +265,48 @@ let subst_kn sub kn =
 
 exception No_subst
 
-type sideconstantsubst =
-  | User
-  | Canonical
-
-let gen_subst_mp f sub mp1 mp2 =
+let subst_dual_mp sub mp1 mp2 =
   let o1 = subst_mp0 sub mp1 in
   let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in
   match o1, o2 with
     | None, None -> raise No_subst
-    | Some (mp',resolve), None -> User, (f mp' mp2), resolve
-    | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
-    | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
+    | Some (mp1',resolve), None -> mp1', mp2, resolve, true
+    | None, Some (mp2',resolve) -> mp1, mp2', resolve, false
+    | Some (mp1',_), Some (mp2',resolve) -> mp1', mp2', resolve, false
+
+let progress f x ~orelse =
+  let y = f x in
+  if y != x then y else orelse
 
 let subst_ind sub mind =
-  let kn1,kn2 = user_mind mind, canonical_mind mind in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
-  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+  let mpu,dir,l = repr_kn (user_mind mind) in
+  let mpc,_,_ = repr_kn (canonical_mind mind) in
   try
-    let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
-    match side with
-      | User -> mind_of_delta resolve mind'
-      | Canonical -> mind_of_delta2 resolve mind'
+    let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
+    let knu = KerName.make mpu dir l in
+    let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+    let knc' =
+      progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
+    in
+    mind_of_kn_equiv knu knc'
   with No_subst -> mind
 
 let subst_con0 sub con =
-  let kn1,kn2 = user_con con,canonical_con con in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
-  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
-  let dup con = con, mkConst con in
-  let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
-  match constant_of_delta_with_inline resolve con' with
+  let mpu,dir,l = repr_kn (user_con con) in
+  let mpc,_,_ = repr_kn (canonical_con con) in
+  let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
+  let knu = make_kn mpu dir l in
+  let knc = if mpu == mpc then knu else make_kn mpc dir l in
+  match search_delta_inline resolve knu knc with
     | Some t ->
       (* In case of inlining, discard the canonical part (cf #2608) *)
-      constant_of_kn (user_con con'), t
+      constant_of_kn knu, t
     | None ->
-      let con'' = match side with
-	| User -> constant_of_delta resolve con'
-	| Canonical -> constant_of_delta2 resolve con'
+      let knc' =
+        progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
       in
-      if con'' == con then raise No_subst else dup con''
+      let con' = constant_of_kn_equiv knu knc' in
+      con', mkConst con'
 
 let subst_con sub con =
   try subst_con0 sub con