Utilisation de Let In pour les constantes locales, prise en compte des Let In dans le discharge, l'unification de evarconv et l'unification de clenv

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

3 files changed, 120 insertions, 101 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 075e98a7d..004b59b10 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -90,6 +90,7 @@ let unfold_red sp = {
 type red_kind =
     BETA | DELTA | ZETA | EVAR | IOTA
   | CONST of constant_path list | CONSTBUT of constant_path list
+  | VAR of identifier
 
 let rec red_add red = function
   | BETA -> { red with r_beta = true }
@@ -107,6 +108,7 @@ let rec red_add red = function
   | IOTA -> { red with r_iota = true }
   | EVAR -> { red with r_evar = true }
   | ZETA -> { red with r_zeta = true }
+  | VAR id -> red_add red (CONST [make_path [] id CCI])
 
 let incr_cnt red cnt =
   if red then begin
@@ -124,12 +126,16 @@ let red_set red = function
       let (b,l) = red.r_const in
       let c = List.mem sp l in
       incr_cnt ((b & not c) or (c & not b)) delta
+  | VAR id -> (* En attendant d'avoir des sp pour les Var *)
+      let (b,l) = red.r_const in
+      let c = List.exists (fun sp -> basename sp = id) l in
+      incr_cnt ((b & not c) or (c & not b)) delta
   | ZETA -> incr_cnt red.r_zeta zeta
   | EVAR -> incr_cnt red.r_zeta evar
   | IOTA -> incr_cnt red.r_iota iota
   | DELTA -> fst red.r_const  (* Used for Rel/Var defined in context *)
   (* Not for internal use *)
-  | CONST _ | CONSTBUT _ -> failwith "not implemented"
+  | CONST _ | CONSTBUT _ | VAR _ -> failwith "not implemented"
 
 (* Gives the constant list *)
 let red_get_const red =
@@ -294,24 +300,24 @@ let ref_value_cache info ref =
       -> None
 
 let defined_vars flags env =
-  if red_local_const (snd flags) then
+(*  if red_local_const (snd flags) then*)
     fold_named_context 
       (fun env (id,b,t) e ->
 	 match b with
 	   | None -> e
 	   | Some body -> (id, body)::e)
       env []
-  else []
+(*  else []*)
 
 let defined_rels flags env =
-  if red_local_const (snd flags) then
+(*  if red_local_const (snd flags) then*)
   fold_rel_context 
       (fun env (id,b,t) (i,subs) ->
 	 match b with
 	   | None -> (i+1, subs)
 	   | Some body -> (i+1, (i,body) :: subs))
       env (0,[])
-  else (0,[])
+(*  else (0,[])*)
 
 let infos_under infos = { infos with i_flags = flags_under infos.i_flags }
 
@@ -434,7 +440,8 @@ let red_allowed flags stack rk =
     red_top flags rk
 
 let red_allowed_ref flags stack = function
-  | FarRelBinding _ | VarBinding _ -> red_allowed flags stack DELTA
+  | FarRelBinding _ -> red_allowed flags stack DELTA
+  | VarBinding id -> red_allowed flags stack (VAR id)
   | EvarBinding _ -> red_allowed flags stack EVAR
   | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp])
 
@@ -1098,7 +1105,7 @@ and whnf_frterm info ft =
 	  else 
 	    ft
       | FFlex (FVar id) as t->
-	  if red_under info.i_flags DELTA then
+	  if red_under info.i_flags (VAR id) then
 	    match ref_value_cache info (VarBinding id) with
 	      | Some def ->
 		  let udef = unfreeze info def in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index bf855b262..b546942e1 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -28,6 +28,7 @@ type red_kind =
   | IOTA
   | CONST of section_path list
   | CONSTBUT of section_path list
+  | VAR of identifier
 
 (* Sets of reduction kinds. *)
 type reds
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3316e2381..c90dcddb1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -12,6 +12,26 @@ open Classops
 open Recordops 
 open Evarutil
 
+
+type flexible_term = FConst of constant | FRel of int | FVar of identifier 
+type flex_kind_of_term =
+  | Rigid of constr 
+  | MaybeFlexible of flexible_term
+  | Flexible of existential
+
+let flex_kind_of_term c =
+  match kind_of_term c with
+    | IsConst c -> MaybeFlexible (FConst c)
+    | IsRel n -> MaybeFlexible (FRel n)
+    | IsVar id -> MaybeFlexible (FVar id)
+    | IsEvar ev -> Flexible ev
+    | _ -> Rigid c
+
+let eval_flexible_term env = function
+  | FConst c -> constant_opt_value env c
+  | FRel n -> option_app (lift n) (lookup_rel_value n env)
+  | FVar id -> lookup_named_value id env
+
 let evar_apprec env isevars stack c =
   let rec aux s =
     let (t,stack as s') = Reduction.apprec env !isevars s in
@@ -53,8 +73,8 @@ let rec evar_conv_x env isevars pbty term1 term2 =
 
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
-  match (kind_of_term term1, kind_of_term term2) with
-    | IsEvar (sp1,al1 as ev1), IsEvar (sp2,al2 as ev2) ->
+  match (flex_kind_of_term term1, flex_kind_of_term term2) with
+    | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 () =
 	  if List.length l1 > List.length l2 then 
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
@@ -73,7 +93,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f2]
 
-    | IsEvar ev1, IsConst cst2 ->
+    | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
@@ -81,7 +101,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (pbty,ev1,applist(term2,deb2))
           & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f4 () =
-	  match constant_opt_value env cst2 with
+	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x env isevars pbty
 		  appr1 (evar_apprec env isevars l2 v2)
@@ -89,7 +109,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst cst1, IsEvar ev2 ->
+    | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
@@ -97,7 +117,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (pbty,ev2,applist(term1,deb1))
           & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	and f4 () =
-	  match constant_opt_value env cst1 with
+	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x env isevars pbty
 		  (evar_apprec env isevars l1 v1) appr2
@@ -105,10 +125,9 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst (sp1,al1 as cst1), IsConst (sp2,al2 as cst2) ->
+    | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f2 () =
-          (sp1 = sp2)
-	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
+          (flex1 = flex2)
 	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	and f3 () =
 	  (try conv_record env isevars 
@@ -116,12 +135,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	      with Not_found -> check_conv_record appr2 appr1)
            with _ -> false)
 	and f4 () =
-	  match constant_opt_value env cst2 with
+	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x env isevars pbty
 		  appr1 (evar_apprec env isevars l2 v2)
 	    | None ->
-		match constant_opt_value env cst1 with
+		match eval_flexible_term env flex1 with
 		  | Some v1 ->
 		      evar_eqappr_x env isevars pbty
 			(evar_apprec env isevars l1 v1) appr2
@@ -129,26 +148,26 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f2; f3; f4]
 
-    | IsEvar ev1, _ ->
+    | Flexible ev1, Rigid _ ->
        	(List.length l1 <= List.length l2) &
        	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
 	solve_simple_eqn evar_conv_x env isevars
 	  (pbty,ev1,applist(term2,deb2))
         & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 
-    | _, IsEvar ev2 ->
+    | Rigid _, Flexible ev2 ->
        	(List.length l2 <= List.length l1) &
        	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
 	solve_simple_eqn evar_conv_x env isevars
 	  (pbty,ev2,applist(term1,deb1))
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
-    | IsConst cst1, _ ->
+    | MaybeFlexible flex1, Rigid _ ->
 	let f3 () =
 	  (try conv_record env isevars (check_conv_record appr1 appr2)
            with _ -> false)
 	and f4 () =
-	  match constant_opt_value env cst1 with
+	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
  		evar_eqappr_x env isevars pbty
 		  (evar_apprec env isevars l1 v1) appr2
@@ -156,12 +175,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f3; f4]
 	     
-    | _ , IsConst cst2 -> 
+    | Rigid _ , MaybeFlexible flex2 -> 
 	let f3 () = 
 	  (try (conv_record env isevars (check_conv_record appr2 appr1))
            with _ -> false)
 	and f4 () =
-	  match constant_opt_value env cst2 with
+	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
  		evar_eqappr_x env isevars pbty
 		  appr1 (evar_apprec env isevars l2 v2)
@@ -169,89 +188,81 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f3; f4]
 
-    | IsRel n, IsRel m ->
-	n=m
-	  & (List.length(l1) = List.length(l2))
-	  & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
-
-    | IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
-
-    | _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
-
-    | IsVar id1, IsVar id2 ->
-	(id1=id2 & (List.length l1 = List.length l2)
-	     & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
-
-    | IsMeta n, IsMeta m ->
-	(n=m & (List.length(l1) = List.length(l2))
-	   & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
-
-    | IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
-
-    | IsLambda (_,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> 
-	evar_conv_x env isevars CONV c1 c2
-	& evar_conv_x env isevars CONV c'1 c'2
-
-    | IsLetIn (_,b1,_,c'1), IsLetIn (_,b2,_,c'2) ->
-	let f1 () =
-	  evar_conv_x env isevars CONV b1 b2
-	  & evar_conv_x env isevars pbty c'1 c'2
-	  & (List.length l1 = List.length l2)
-	  & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
-	and f2 () =
-	  evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) (subst1 b2 c'2,l2)
-	in 
-	ise_try isevars [f1; f2]
-
-    | IsLetIn (_,b1,_,c'1), _ ->  (* On fait commuter les args avec le Let *)
-	evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2
-
-    | _, IsLetIn (_,b2,_,c'2) ->
-	evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2)
-
-    | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
-        evar_conv_x env isevars CONV c1 c2
-        & 
-	(let d = nf_ise1 !isevars c1 in
-	 evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
-
-    | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
-	sp1=sp2
-	& array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
-        & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+    | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
+	  
+	| IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2
+
+	| _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
+
+	| IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
+
+	| IsLambda (_,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> 
+	    evar_conv_x env isevars CONV c1 c2
+	    & evar_conv_x env isevars CONV c'1 c'2
+
+	| IsLetIn (_,b1,_,c'1), IsLetIn (_,b2,_,c'2) ->
+	    let f1 () =
+	      evar_conv_x env isevars CONV b1 b2
+	      & evar_conv_x env isevars pbty c'1 c'2
+	      & (List.length l1 = List.length l2)
+	      & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
+	    and f2 () =
+	      evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1)
+		(subst1 b2 c'2,l2)
+	    in 
+	    ise_try isevars [f1; f2]
+
+	| IsLetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
+	    evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2
+
+	| _, IsLetIn (_,b2,_,c'2) ->
+	    evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2)
+
+	| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
+            evar_conv_x env isevars CONV c1 c2
+            & 
+	    (let d = nf_ise1 !isevars c1 in
+	     evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
+
+	| IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
+	    sp1=sp2
+	    & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+            & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
              
-    | IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) ->
-	sp1=sp2
-        & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
-        & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
-
-    | IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
-	evar_conv_x env isevars CONV p1 p2
-	& evar_conv_x env isevars CONV c1 c2
-	& (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
-	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-
-    | IsFix (li1,(tys1,_,bds1)), IsFix (li2,(tys2,_,bds2)) ->
-	li1=li2
-	& (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
-	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
-	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+	| IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) ->
+	    sp1=sp2
+            & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+            & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+
+	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
+	    evar_conv_x env isevars CONV p1 p2
+	    & evar_conv_x env isevars CONV c1 c2
+	    & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
+	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+
+	| IsFix (li1,(tys1,_,bds1)), IsFix (li2,(tys2,_,bds2)) ->
+	    li1=li2
+	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
+	    & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
+	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	     
-    | IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) ->
-	i1=i2 
-	& (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
-	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
-	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+	| IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) ->
+	    i1=i2 
+	    & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
+	    & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
+	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-    | (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _), _ -> false
-    | _, (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _) -> false
+	| (IsMeta _ | IsXtra _ | IsLambda _), _ -> false
+	| _, (IsMeta _ | IsXtra _ | IsLambda _) -> false
 
-    | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
-    | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
+	| (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
+	| _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
 
-    | (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), 
-      (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
+	| (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), 
+	  (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
 
+	| (IsRel _ | IsVar _ | IsConst _ | IsEvar _), _ -> assert false
+	| _, (IsRel _ | IsVar _ | IsConst _ | IsEvar _) -> assert false
 
 
 and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =