Uniformisation politique de nommage evd/isevars (evd si evar_defs,

evdref si evar_defs ref)


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

1 files changed, 106 insertions, 106 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 66270c2b3..b65ad37b1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -67,30 +67,30 @@ let rec apprec_nobeta env sigma s =
 	     | NotReducible -> s)
     | _ -> s
 
-let evar_apprec_nobeta env isevars stack c =
+let evar_apprec_nobeta env evd stack c =
   let rec aux s =
-    let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in
+    let (t,stack as s') = apprec_nobeta env (evars_of evd) s in
     match kind_of_term t with
-      | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
-	  aux (Evd.existential_value (evars_of isevars) ev, stack)
+      | Evar (evk,_ as ev) when Evd.is_defined (evars_of evd) evk ->
+	  aux (Evd.existential_value (evars_of evd) ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 *)
 
-let evar_apprec env isevars stack c =
-  let sigma = evars_of isevars in
+let evar_apprec env evd stack c =
+  let sigma = evars_of evd in
   let rec aux s =
     let (t,stack) = Reductionops.apprec env sigma s in
     match kind_of_term t with
-      | Evar (n,_ as ev) when Evd.is_defined sigma n ->
+      | Evar (evk,_ as ev) when Evd.is_defined sigma evk ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack_list stack empty_stack)
 
-let apprec_nohdbeta env isevars c =
+let apprec_nohdbeta env evd c =
   let (t,stack as s) = Reductionops.whd_stack c in
   match kind_of_term t with
-    | (Case _ | Fix _) -> evar_apprec env isevars [] c
+    | (Case _ | Fix _) -> evar_apprec env evd [] c
     | _ -> s
 
 (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
@@ -131,46 +131,46 @@ let check_conv_record (t1,l1) (t2,l2) =
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
-let rec ise_try isevars = function
+let rec ise_try evd = function
     [] -> assert false
-  | [f] -> f isevars
+  | [f] -> f evd
   | f1::l ->
-      let (isevars',b) = f1 isevars in
-      if b then (isevars',b) else ise_try isevars l
+      let (evd',b) = f1 evd in
+      if b then (evd',b) else ise_try evd l
 
-let ise_and isevars l =
+let ise_and evd l =
   let rec ise_and i = function
       [] -> assert false
     | [f] -> f i
     | f1::l ->
         let (i',b) = f1 i in
-        if b then  ise_and i' l else (isevars,false) in
-  ise_and isevars l
+        if b then  ise_and i' l else (evd,false) in
+  ise_and evd l
 
-let ise_list2 isevars f l1 l2 =
+let ise_list2 evd f l1 l2 =
   let rec ise_list2 i l1 l2 =
     match l1,l2 with
         [], [] -> (i, true)
       | [x], [y] -> f i x y
       | x::l1, y::l2 ->
           let (i',b) = f i x y in
-          if b then ise_list2 i' l1 l2 else (isevars,false)
-      | _ -> (isevars, false) in
-  ise_list2 isevars l1 l2
+          if b then ise_list2 i' l1 l2 else (evd,false)
+      | _ -> (evd, false) in
+  ise_list2 evd l1 l2
 
-let ise_array2 isevars f v1 v2 =
+let ise_array2 evd f v1 v2 =
   let rec allrec i = function
     | -1 -> (i,true)
     | n ->
         let (i',b) = f i v1.(n) v2.(n) in
-        if b then allrec i' (n-1) else (isevars,false)
+        if b then allrec i' (n-1) else (evd,false)
   in 
   let lv1 = Array.length v1 in
-  if lv1 = Array.length v2 then allrec isevars (pred lv1) 
-  else (isevars,false)
+  if lv1 = Array.length v2 then allrec evd (pred lv1) 
+  else (evd,false)
 
-let rec evar_conv_x env isevars pbty term1 term2 = 
-  let sigma = evars_of isevars in
+let rec evar_conv_x env evd pbty term1 term2 = 
+  let sigma = evars_of evd in
   let term1 = whd_castappevar sigma term1 in
   let term2 = whd_castappevar sigma term2 in
 (*
@@ -181,19 +181,19 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
-  if is_ground_term isevars term1 && is_ground_term isevars term2 &
-     is_fconv pbty env (evars_of isevars) term1 term2 then
-      (isevars,true)
-  else if is_undefined_evar isevars term1 then
-    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
-  else if is_undefined_evar isevars term2 then
-    solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
+  if is_ground_term evd term1 && is_ground_term evd term2 &
+     is_fconv pbty env (evars_of evd) term1 term2 then
+      (evd,true)
+  else if is_undefined_evar evd term1 then
+    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+  else if is_undefined_evar evd term2 then
+    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
   else 
-    let (t1,l1) = apprec_nohdbeta env isevars term1 in
-    let (t2,l2) = apprec_nohdbeta env isevars term2 in
-    evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+    let (t1,l1) = apprec_nohdbeta env evd term1 in
+    let (t2,l2) = apprec_nohdbeta env evd term2 in
+    evar_eqappr_x env evd pbty (t1,l1) (t2,l2)
 
-and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -221,19 +221,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                  (fun i -> evar_conv_x env i CONV) l1 l2)]
           else (i,false)
 	in 
-	ise_try isevars [f1; f2]
+	ise_try evd [f1; f2]
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
 	  if 
 	    is_unification_pattern_evar ev1 l1 & 
-	    not (occur_evar (fst ev1) (applist (term2,l2)))
+	    not (occur_evar (fst ev1) (applist appr2))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	    let t2 = nf_evar (evars_of evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
 	  then
@@ -253,19 +253,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f1; f4]
+	ise_try evd [f1; f4]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
 	  if 
 	    is_unification_pattern_evar ev2 l2 & 
-	    not (occur_evar (fst ev2) (applist (term1,l1)))
+	    not (occur_evar (fst ev2) (applist appr1))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
-	    let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	    let t1 = nf_evar (evars_of evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	  else if
        	    List.length l2 <= List.length l1
 	  then
@@ -284,7 +284,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f1; f4]
+	ise_try evd [f1; f4]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f2 i =
@@ -313,36 +313,36 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		      evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 		  | None -> (i,false)
 	in 
-	ise_try isevars [f2; f3; f4]
+	ise_try evd [f2; f3; f4]
 
     | Flexible ev1, Rigid _ ->
 	if 
 	  is_unification_pattern_evar ev1 l1 & 
-	  not (occur_evar (fst ev1) (applist (term2,l2)))
+	  not (occur_evar (fst ev1) (applist appr2))
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	  let t2 = nf_evar (evars_of evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true
 
     | Rigid _, Flexible ev2 ->
 	if 
 	  is_unification_pattern_evar ev2 l2 & 
-	  not (occur_evar (fst ev2) (applist (term1,l1)))
+	  not (occur_evar (fst ev2) (applist appr1))
 	then
 	  (* Miller-Pfenning's patterns unification *)
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
-	  let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	  let t1 = nf_evar (evars_of evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true
 
     | MaybeFlexible flex1, Rigid _ ->
@@ -355,7 +355,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
  		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f3; f4]
+	ise_try evd [f3; f4]
 	     
     | Rigid _ , MaybeFlexible flex2 -> 
 	let f3 i = 
@@ -367,19 +367,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
  		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in 
-	ise_try isevars [f3; f4]
+	ise_try evd [f3; f4]
 
     | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
 	  
-	| Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
+	| Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2
 
-	| _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
+	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            (isevars,base_sort_cmp pbty s1 s2)
+            (evd,base_sort_cmp pbty s1 s2)
 
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
                  let c = nf_evar (evars_of i) c1 in
@@ -400,18 +400,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
               and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
 	      in evar_eqappr_x env i pbty appr1 appr2
 	    in 
-	    ise_try isevars [f1; f2]
+	    ise_try evd [f1; f2]
 
 	| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
-	     let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
-             in evar_eqappr_x env isevars pbty appr1 appr2
+	     let appr1 = evar_apprec env evd l1 (subst1 b1 c'1)
+             in evar_eqappr_x env evd pbty appr1 appr2
 
 	| _, LetIn (_,b2,_,c'2) ->
-	    let appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
-            in evar_eqappr_x env isevars pbty appr1 appr2
+	    let appr2 = evar_apprec env evd l2 (subst1 b2 c'2)
+            in evar_eqappr_x env evd pbty appr1 appr2
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> 
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar (evars_of i) c1 in
@@ -419,16 +419,16 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| Ind sp1, Ind sp2 ->
 	    if sp1=sp2 then
-              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
-            else (isevars, false)
+              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+            else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
 	    if sp1=sp2 then
-              ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
-            else (isevars, false)
+              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+            else (evd, false)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            ise_and isevars
+            ise_and evd
               [(fun i -> evar_conv_x env i CONV p1 p2);
                (fun i -> evar_conv_x env i CONV c1 c2);
 	       (fun i -> ise_array2 i
@@ -437,7 +437,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
             if li1=li2 then
-              ise_and isevars
+              ise_and evd
                 [(fun i -> ise_array2 i
                     (fun i -> evar_conv_x env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
@@ -445,10 +445,10 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
 	         (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
-	    else (isevars,false)
+	    else (evd,false)
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
             if i1=i2  then
-              ise_and isevars
+              ise_and evd
                 [(fun i -> ise_array2 i
                     (fun i -> evar_conv_x env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
@@ -456,30 +456,30 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		     bds1 bds2);
                  (fun i -> ise_list2 i
                      (fun i -> evar_conv_x env i CONV) l1 l2)]
-            else (isevars,false)
+            else (evd,false)
 
-	| (Meta _ | Lambda _), _ -> (isevars,false)
-	| _, (Meta _ | Lambda _) -> (isevars,false)
+	| (Meta _ | Lambda _), _ -> (evd,false)
+	| _, (Meta _ | Lambda _) -> (evd,false)
 
-	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false)
-	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false)
+	| (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
+	| _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
 
 	| (App _ | Case _ | Fix _ | CoFix _), 
-	  (App _ | Case _ | Fix _ | CoFix _) -> (isevars,false)
+	  (App _ | Case _ | Fix _ | CoFix _) -> (evd,false)
 
 	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
 	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
 
-and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
-  let (isevars',ks) =
+and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
+  let (evd',ks) =
     List.fold_left
       (fun (i,ks) b ->
 	 let dloc = (dummy_loc,InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
 	 (i', ev :: ks))
-      (isevars,[]) bs
+      (evd,[]) bs
   in
-  ise_and isevars'
+  ise_and evd'
     [(fun i ->
       ise_list2 i
         (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
@@ -491,11 +491,11 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
      (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
      (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
 
-let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+let first_order_unification env evd pbty (term1,l1) (term2,l2) =
   match kind_of_term term1, kind_of_term term2 with
     | Evar ev1,_ when List.length l1 <= List.length l2 ->
 	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-	ise_and isevars
+	ise_and evd
           (* First compare extra args for better failure message *)
         [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
 	(fun i ->
@@ -507,7 +507,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 	    solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
     | _,Evar ev2 when List.length l2 <= List.length l1 ->
 	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-	ise_and isevars
+	ise_and evd
           (* First compare extra args for better failure message *)
         [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
 	(fun i ->
@@ -519,37 +519,37 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 	    solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
     | _ -> 
 	(* Some head evar have been instantiated *)
-	evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+	evar_conv_x env evd pbty (applist(term1,l1)) (applist(term2,l2))
 
-let consider_remaining_unif_problems env isevars =
-  let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+let consider_remaining_unif_problems env evd =
+  let (evd,pbs) = get_conv_pbs evd (fun _ -> true) in
   List.fold_left
-    (fun (isevars,b as p) (pbty,env,t1,t2) ->
-      if b then first_order_unification env isevars pbty 
-	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
-	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+    (fun (evd,b as p) (pbty,env,t1,t2) ->
+      if b then first_order_unification env evd pbty 
+	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1))
+	(apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2))
       else p)
-    (isevars,true)
+    (evd,true)
     pbs
 
 (* Main entry points *)
 
-let the_conv_x     env t1 t2 isevars =
-  match evar_conv_x env isevars CONV  t1 t2 with
+let the_conv_x     env t1 t2 evd =
+  match evar_conv_x env evd CONV  t1 t2 with
       (evd',true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let the_conv_x_leq env t1 t2 isevars =
-  match evar_conv_x env isevars CUMUL t1 t2 with
+let the_conv_x_leq env t1 t2 evd =
+  match evar_conv_x env evd CUMUL t1 t2 with
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
  
-let e_conv env isevars t1 t2 =
-  match evar_conv_x env !isevars CONV t1 t2 with
-      (evd',true) -> isevars := evd'; true
+let e_conv env evd t1 t2 =
+  match evar_conv_x env !evd CONV t1 t2 with
+      (evd',true) -> evd := evd'; true
     | _ -> false
 
-let e_cumul env isevars t1 t2 =
-  match evar_conv_x env !isevars CUMUL t1 t2 with
-      (evd',true) -> isevars := evd'; true
+let e_cumul env evd t1 t2 =
+  match evar_conv_x env !evd CUMUL t1 t2 with
+      (evd',true) -> evd := evd'; true
     | _ -> false