Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpoint definition

+ Help the use of #trace on evar_conv_appr_x

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

5 files changed, 72 insertions, 52 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index be5eb5dbd..1258e4a09 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -61,9 +61,11 @@ let eval_flexible_term ts env c =
   | _ -> assert false
 
 let apprec_nohdbeta ts env evd c =
-  match kind_of_term (fst (Reductionops.whd_nored_stack evd c)) with
-    | (Case _ | Fix _) -> zip (whd_betaiota_deltazeta_for_iota_state ts env evd (c, []))
-    | _ -> c
+  let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
+  if not_purely_applicative_stack (snd (Reductionops.strip_app sk))
+  then zip (fst (whd_betaiota_deltazeta_for_iota_state
+		   ts env evd Cst_stack.empty appr))
+  else c
 
 let position_problem l2r = function
   | CONV -> None
@@ -257,10 +259,11 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 	    (position_problem false pbty,destEvar term2,term1)
         else
           evar_eqappr_x ts env evd pbty
-            (whd_nored_state evd (term1,empty_stack)) (whd_nored_state evd (term2,empty_stack))
+            (whd_nored_state evd (term1,empty_stack), Cst_stack.empty)
+	    (whd_nored_state evd (term2,empty_stack), Cst_stack.empty)
 
-and evar_eqappr_x ?(rhs_is_already_stuck = false)
-    ts env evd pbty (term1,sk1 as appr1) (term2,sk2 as appr2) =
+and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
+    ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
   let default_fail i = (* costly *)
     UnifFailure (i,ConversionFailed (env, zip appr1, zip appr2)) in
   let miller_pfenning on_left fallback ev (_,skF) apprM evd =
@@ -276,7 +279,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	) fallback
 	(is_unification_pattern_evar env evd ev lF tM)
       ) (default_fail evd) (list_of_app_stack skF) in
-  let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) =
+  let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) =
     let switch f a b = if on_left then f a b else f b a in
     let not_only_app = not_purely_applicative_stack skM in
     let f1 i = miller_pfenning on_left
@@ -296,8 +299,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
     and f3 i =
       match eval_flexible_term ts env termM with
       | Some vM ->
-	switch (evar_eqappr_x ts env i pbty) apprF
-	  (whd_betaiota_deltazeta_for_iota_state ts env i (vM, skM))
+	switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
+	  (whd_betaiota_deltazeta_for_iota_state ts env i cstsM (vM, skM))
       | None -> UnifFailure (i,NotSameHead)
     in
     ise_try evd [f1; f2; f3] in
@@ -306,10 +309,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
     let (na,c1,c'1) = destLambda term in
     let c = nf_evar evd c1 in
     let env' = push_rel (na,None,c) env in
-    let appr1 = whd_betaiota_deltazeta_for_iota_state ts env' evd (c'1, empty_stack) in
-    let appr2 = whd_nored_state evd (zip (term', sk' @ [Zshift 1]), [Zapp [mkRel 1]]) in
-      if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2
-      else evar_eqappr_x ts env' evd CONV appr2 appr1
+    let out1 = whd_betaiota_deltazeta_for_iota_state
+      ts env' evd Cst_stack.empty (c'1, empty_stack) in
+    let out2 = whd_nored_state evd
+      (zip (term', sk' @ [Zshift 1]), [Zapp [mkRel 1]]), Cst_stack.empty in
+    if onleft then evar_eqappr_x ts env' evd CONV out1 out2
+    else evar_eqappr_x ts env' evd CONV out2 out1
   in
 
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
@@ -339,9 +344,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	in
 	ise_try evd [f1; f2]
 
-    | Flexible ev1, MaybeFlexible -> flex_maybeflex true ev1 appr1 appr2
+    | Flexible ev1, MaybeFlexible -> flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2)
 
-    | MaybeFlexible, Flexible ev2 -> flex_maybeflex false ev2 appr2 appr1
+    | MaybeFlexible, Flexible ev2 -> flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1)
 
     | MaybeFlexible, MaybeFlexible -> begin
         match kind_of_term term1, kind_of_term term2 with
@@ -355,9 +360,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
-          let appr1 = whd_betaiota_deltazeta_for_iota_state ts env i ((subst1 b1 c'1),sk1)
-          and appr2 = whd_betaiota_deltazeta_for_iota_state ts env i ((subst1 b2 c'2),sk2)
-	  in evar_eqappr_x ts env i pbty appr1 appr2
+          let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 ((subst1 b1 c'1),sk1)
+          and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 ((subst1 b2 c'2),sk2)
+	  in evar_eqappr_x ts env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
 
@@ -384,35 +389,48 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
             | Evar _ -> not_purely_applicative_stack args
 	    (* false (* immediate solution without Canon Struct *)*)
             | Lambda _ -> assert (match args with [] -> true | _ -> false); true
-            | LetIn (_,b,_,c) ->
-                is_unnamed (whd_betaiota_deltazeta_for_iota_state ts env i (subst1 b c, args))
+            | LetIn (_,b,_,c) -> is_unnamed
+	      (fst (whd_betaiota_deltazeta_for_iota_state
+		      ts env i Cst_stack.empty (subst1 b c, args)))
             | Case _| Fix _| App _| Cast _ -> assert false in
           let rhs_is_stuck_and_unnamed () =
             match eval_flexible_term ts env term2 with
             | None -> false
             | Some v2 ->
 	      let applicative_stack = append_stack_app_list (fst (strip_app sk2)) empty_stack in
-	      is_unnamed (whd_betaiota_deltazeta_for_iota_state ts env i (v2, applicative_stack)) in
+	      is_unnamed
+		(fst (whd_betaiota_deltazeta_for_iota_state
+			ts env i Cst_stack.empty (v2, applicative_stack))) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
-	  if (isLambda term1 || rhs_is_already_stuck) && (not (not_purely_applicative_stack sk1)) then
+	  if (isLambda term1 || rhs_is_already_stuck)
+	    && (not (not_purely_applicative_stack sk1)) then
 	    match eval_flexible_term ts env term1 with
 	    | Some v1 ->
-		evar_eqappr_x ~rhs_is_already_stuck
-                  ts env i pbty (whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2
+	      evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
+		(whd_betaiota_deltazeta_for_iota_state
+		   ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+		(appr2,csts2)
 	    | None ->
 		match eval_flexible_term ts env term2 with
 		| Some v2 ->
-		    evar_eqappr_x ts env i pbty appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2))
+		    evar_eqappr_x ts env i pbty (appr1,csts1)
+		      (whd_betaiota_deltazeta_for_iota_state
+			 ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 		| None -> UnifFailure (i,NotSameHead)
 	  else
 	    match eval_flexible_term ts env term2 with
 	    | Some v2 ->
-		evar_eqappr_x ts env i pbty appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2))
+	      evar_eqappr_x ts env i pbty (appr1,csts1)
+		(whd_betaiota_deltazeta_for_iota_state
+		   ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	    | None ->
 		match eval_flexible_term ts env term1 with
 		| Some v1 ->
-		    evar_eqappr_x ts env i pbty (whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2
+		  evar_eqappr_x ts env i pbty
+		    (whd_betaiota_deltazeta_for_iota_state
+		       ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+		    (appr2,csts2)
 		| None -> UnifFailure (i,NotSameHead)
 	in
 	ise_try evd [f1; f2; f3]
@@ -429,7 +447,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid ->
-      let f1 evd = 
+      let f1 evd =
 	miller_pfenning true
 	(Success ((* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,zip appr1,zip appr2) evd))
@@ -460,11 +478,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	  match eval_flexible_term ts env term1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty
-		  (whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2
-	    | None -> 
+		  (whd_betaiota_deltazeta_for_iota_state
+		     ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+		  (appr2,csts2)
+	    | None ->
 	      if isLambda term2 then eta env evd false sk2 term2 sk1 term1
 	      else UnifFailure (i,NotSameHead)
-	in	 
+	in
 	  ise_try evd [f3; f4]
 
     | Rigid, MaybeFlexible ->
@@ -474,9 +494,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	and f4 i =
 	  match eval_flexible_term ts env term2 with
 	    | Some v2 ->
-		evar_eqappr_x ts env i pbty
-		  appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2))
-	    | None -> 
+		evar_eqappr_x ts env i pbty (appr1,csts1)
+		  (whd_betaiota_deltazeta_for_iota_state
+		     ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+	    | None ->
 	      if isLambda term1 then eta env evd true sk1 term1 sk2 term2
 	      else UnifFailure (i,NotSameHead)
 	in
@@ -578,10 +599,6 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
      (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
      (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))))]
 
-(* getting rid of the optional argument rhs_is_already_stuck *)
-let evar_eqappr_x ts env evd pbty appr1 appr2 =
-  evar_eqappr_x ts env evd pbty appr1 appr2
-
 (* We assume here |l1| <= |l2| *)
 
 let first_order_unification ts env evd (ev1,l1) (term2,l2) =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 5a329f5f4..30495857a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -30,9 +30,9 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -
 (* For debugging *)
 val evar_conv_x : transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
-val evar_eqappr_x : transparent_state ->
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
   env -> evar_map ->
-    conv_pb -> constr * constr stack -> constr * constr stack ->
+    conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
       Evarsolve.unification_result
 (**/**)
 
@@ -46,5 +46,5 @@ val check_conv_record : constr * types stack -> constr * types stack ->
 
 val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
 
-val second_order_matching : transparent_state -> env -> evar_map -> 
+val second_order_matching : transparent_state -> env -> evar_map ->
   existential -> occurrences option list -> constr -> evar_map * bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 624645a8f..0f8f6434f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -911,20 +911,22 @@ let is_sort env sigma arity =
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
 
-let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
-  let rec whrec s =
-    let (t, stack as s) = whd_betaiota_state sigma s in
+let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+  let rec whrec csts s =
+    let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in
     match strip_app stack with
       |args, (Zcase _ :: _ as stack') ->
 	let seq = (t,append_stack_app_list args empty_stack) in
-	let t_o,stack_o = whd_betadeltaiota_state_using ts env sigma seq in
-	if reducible_mind_case t_o then whrec (t_o, stack_o@stack') else s
+	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
+	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Zfix _ :: _ as stack') ->
 	let seq = (t,append_stack_app_list args empty_stack) in
-	let t_o,stack_o = whd_betadeltaiota_state_using ts env sigma seq in
-	if isConstruct t_o then whrec (t_o, stack_o@stack') else s
-      |_ -> s
-  in whrec s
+	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
+	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+      |_ -> s,csts'
+  in whrec csts s
 
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing existential variables.
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 916e001c1..d4bb9aabf 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -230,7 +230,8 @@ val head_unfold_under_prod : transparent_state -> reduction_function
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
-  transparent_state -> state_reduction_function
+  transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
+  state * Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
 val meta_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8b89bd438..e287ca52a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -343,7 +343,7 @@ let oracle_order env cf1 cf2 =
       | Some k2 -> Some (Conv_oracle.oracle_order false k1 k2)
 
 let do_reduce ts (env, nb) sigma c =
-  zip (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack))
+  zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, empty_stack)))
 
 let use_full_betaiota flags =
   flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3