Simplify evarconv thanks to new delta status of projections,

using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.

5 files changed, 70 insertions, 64 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index ab678666fa..734b7853f5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -310,6 +310,12 @@ let destCase c = match kind_of_term c with
 
 let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
 
+let isProj c =  match kind_of_term c with Proj _ -> true | _ -> false
+
+let destProj c = match kind_of_term c with
+  | Proj (p, c) -> (p, c)
+  | _ -> raise DestKO
+
 let destFix c = match kind_of_term c with
   | Fix fix -> fix
   | _ -> raise DestKO
diff --git a/kernel/term.mli b/kernel/term.mli
index 28ebc41e24..50cd433e95 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -112,6 +112,7 @@ val isConstruct : constr -> bool
 val isFix : constr -> bool
 val isCoFix : constr -> bool
 val isCase : constr -> bool
+val isProj : constr -> bool
 
 val is_Prop : constr -> bool
 val is_Set  : constr -> bool
@@ -183,6 +184,9 @@ return P in t1], or [if c then t1 else t2])
 where [info] is pretty-printing information *)
 val destCase : constr -> case_info * constr * constr * constr array
 
+(** Destructs a projection *)
+val destProj : constr -> projection * constr
+
 (** Destructs the {% $ %}i{% $ %}th function of the block
    [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
     with    f{_ 2} ctx{_ 2} = b{_ 2}
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a8ab0666d7..f5f8e8c206 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -33,62 +33,52 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_unification:=a);
 }
 
-let unfold_projection env evd ts p c stk =
-  (match try Some (lookup_projection p env) with Not_found -> None with
-  | Some pb -> 
+let unfold_projection env evd ts p c =
+  if Projection.unfolded p then Some c
+  else     
     let cst = Projection.constant p in
-    let unfold () = 
-      let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
-			  p, Cst_stack.empty) in
-	Some (c, s :: stk)
-    in
-    let unfold_app () =
-      let t' = Retyping.expand_projection env evd p c [] in
-      let f, args = destApp t' in
-      let stk = Stack.append_app args stk in
-	Some (f, stk)
-    in
-      if Projection.unfolded p then unfold ()
-      else 
-	if is_transparent_constant ts cst then
+      if is_transparent_constant ts cst then
+	let unfold_app () =
+	  let t' = Retyping.expand_projection env evd p c [] in
+	    Some t'
+	in
 	  (match ReductionBehaviour.get (Globnames.ConstRef cst) with
 	  | None -> unfold_app ()
 	  | Some (recargs, nargs, flags) ->
 	    if (List.mem `ReductionNeverUnfold flags) then None
 	    else unfold_app ())
-	else None
-  | None -> None)
+      else None
 
-let eval_flexible_term ts env evd c stk =
+let eval_flexible_term ts env evd c =
   match kind_of_term c with
   | Const (c,u as cu) ->
       if is_transparent_constant ts c
-      then Option.map (fun x -> x, stk) (constant_opt_value_in env cu)
+      then constant_opt_value_in env cu
       else None
   | Rel n ->
-      (try let (_,v,_) = lookup_rel n env in Option.map (fun t -> lift n t, stk) v
+      (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
       with Not_found -> None)
   | Var id ->
       (try
 	 if is_transparent_variable ts id then
-	   let (_,v,_) = lookup_named id env in Option.map (fun t -> t, stk) v
+	   let (_,v,_) = lookup_named id env in v
 	 else None
        with Not_found -> None)
-  | LetIn (_,b,_,c) -> Some (subst1 b c, stk)
-  | Lambda _ -> Some (c, stk)
-  | Proj (p, c) -> unfold_projection env evd ts p c stk
+  | LetIn (_,b,_,c) -> Some (subst1 b c)
+  | Lambda _ -> Some c
+  | Proj (p, c) -> unfold_projection env evd ts p c
   | _ -> assert false
 
 type flex_kind_of_term =
   | Rigid
-  | MaybeFlexible of Constr.t * Constr.t Stack.t (* reducible but not necessarily reduced *)
+  | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *)
   | Flexible of existential
 
 let flex_kind_of_term ts env evd c sk =
   match kind_of_term c with
     | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
-      Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env evd c sk)
-    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible (c, sk)
+      Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
+    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
     | Evar ev -> Flexible ev
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
     | Meta _ -> Rigid
@@ -437,7 +427,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       else quick_fail i
     and f3 i =
       switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
-	(whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM vM)
+	(whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM))
     in
     ise_try evd [f1; f2; f3] in
   let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
@@ -471,7 +461,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     let open Pp in
 	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
 		 ++ fnl ()) in
-  match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with
+  match (flex_kind_of_term (fst ts) env evd term1 sk1, 
+	 flex_kind_of_term (fst ts) env evd term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
 	  match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
@@ -515,13 +506,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	in
 	ise_try evd [f1; f2]
 
-    | Flexible ev1, MaybeFlexible (v2,sk2) -> 
-      flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) (v2,sk2)
+    | Flexible ev1, MaybeFlexible v2 ->
+      flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
 
-    | MaybeFlexible (v1,sk1), Flexible ev2 -> 
-      flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (v1,sk1)
+    | MaybeFlexible v1, Flexible ev2 -> 
+      flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
 
-    | MaybeFlexible (v1,sk1'), MaybeFlexible (v2,sk2') -> begin
+    | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
         | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
         let f1 i =
@@ -532,22 +523,23 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
 	       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')]
+	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
-          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
-          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
+          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
+          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
 	  in evar_eqappr_x ts env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
 
-	| Proj (p, c), Proj (p', c') when Projection.equal p p' ->
+	| Proj (p, c), Proj (p', c') 
+	  when Constant.equal (Projection.constant p) (Projection.constant p') ->
 	  let f1 i = 
 	    ise_and i 
 	    [(fun i -> evar_conv_x ts env i CONV c c');
-	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
+	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1')
-            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2')
+            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
+            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
@@ -565,7 +557,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		try Success (Evd.add_universe_constraints i univs)
 		with UniversesDiffer -> UnifFailure (i,NotSameHead)
 		| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1' sk2')]
+			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	    else UnifFailure (i,NotSameHead)
 	and f2 i =
 	  (try 
@@ -593,7 +585,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    | Proj (p, c) -> true
             | Case _ | App _| Cast _ -> assert false in
           let rhs_is_stuck_and_unnamed () =
-	    let applicative_stack = fst (Stack.strip_app sk2') in
+	    let applicative_stack = fst (Stack.strip_app sk2) in
 	    is_unnamed
 	      (fst (whd_betaiota_deltazeta_for_iota_state
 		      (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
@@ -601,15 +593,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 
 	  if (isLambda term1 || rhs_is_already_stuck)
-	    && (not (Stack.not_purely_applicative sk1')) then
+	    && (not (Stack.not_purely_applicative sk1)) then
 	    evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1'))
+		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	      (appr2,csts2)
 	  else
 	    evar_eqappr_x ts env i pbty (appr1,csts1)
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2'))
+		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	ise_try evd [f1; f2; f3]
     end
@@ -627,7 +619,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
     | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
 
-    | MaybeFlexible (v1,sk1), Rigid ->
+    | MaybeFlexible v1, Rigid ->
 	let f3 i =
 	  (try 
 	     if not (snd ts) then raise Not_found
@@ -641,7 +633,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	in
 	  ise_try evd [f3; f4]
 
-    | Rigid, MaybeFlexible (v2,sk2) ->
+    | Rigid, MaybeFlexible v2 ->
 	let f3 i =
 	  (try
 	     if not (snd ts) then raise Not_found
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 58d309997e..1131e81fef 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -189,7 +189,7 @@ module Cst_stack = struct
     let p_c = Termops.print_constr in
     prlist_with_sep pr_semicolon
       (fun (c,params,args) ->
-	hov 1 (p_c c ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
+	hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
 		 pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++
 		 str ")")) l
 end
@@ -329,7 +329,8 @@ struct
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
 	Constant.equal c1 c2 && Univ.Instance.equal u1 u2
       | Cst_proj (p1,c1), Cst_proj (p2,c2) ->
-	Projection.equal p1 p2 && f (c1,lft1) (c2,lft2)
+	Constant.equal (Projection.constant p1) (Projection.constant p2)
+	&& f (c1,lft1) (c2,lft2)
       | _, _ -> false
     in
     let rec equal_rec sk1 lft1 sk2 lft2  =
@@ -838,7 +839,10 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
        let kn = Projection.constant p in
        let npars = pb.Declarations.proj_npars 
        and arg = pb.Declarations.proj_arg in
-	 match ReductionBehaviour.get (Globnames.ConstRef kn) with
+	 if not tactic_mode then 
+	   let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
+	     whrec Cst_stack.empty stack'
+	 else match ReductionBehaviour.get (Globnames.ConstRef kn) with
 	 | None ->
 	   let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
 	   let stack'', csts = whrec Cst_stack.empty stack' in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a347149e37..8d0d5394a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -603,7 +603,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	    (try 
 	       let sigma' = 
 		 if pb == CUMUL
-		 then Evd.set_leq_sort env sigma s1 s2 
+		 then Evd.set_leq_sort curenv sigma s1 s2 
 		 else Evd.set_eq_sort sigma s1 s2 
 	       in (sigma', metasubst, evarsubst)
 	     with e when Errors.noncritical e ->
@@ -627,8 +627,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
 
 	(* For records *)
-	| App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app env f1 l1 ->
-	  (try let l1', l2' = eta_constructor_app env f1 l1 cN in
+	| App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app curenv f1 l1 ->
+	  (try let l1', l2' = eta_constructor_app curenv f1 l1 cN in
 		 Array.fold_left2 
 		   (unirec_rec curenvnb CONV true wt) substn l1' l2'
 	   with ex when precatchable_exception ex -> 
@@ -636,8 +636,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
              | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
              | _ -> unify_not_same_head curenvnb pb b wt substn cM cN))
 
-	| _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app env f2 l2 ->
-	  (try let l2', l1' = eta_constructor_app env f2 l2 cM in
+	| _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app curenv f2 l2 ->
+	  (try let l2', l1' = eta_constructor_app curenv f2 l2 cM in
 		 Array.fold_left2 
 		   (unirec_rec curenvnb CONV true wt) substn l1' l2'
 	   with ex when precatchable_exception ex -> 
@@ -661,7 +661,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		  try (* Force unification of the types to fill in parameters *)
 		    let ty1 = get_type_of curenv ~lax:true sigma c1 in
 		    let ty2 = get_type_of curenv ~lax:true sigma c2 in
-		      unify_0_with_initial_metas substn true env cv_pb 
+		      unify_0_with_initial_metas substn true curenv cv_pb 
 			{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
 			  modulo_delta = full_transparent_state;
 			  modulo_eta = true;
@@ -777,7 +777,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       | None -> (* some undefined Metas in cN *) None
       | Some n1 ->
           (* No subterm restriction there, too much incompatibilities *)
-	  let sigma, b = infer_conv ~pb ~ts:convflags env sigma m1 n1 in
+	  let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
 	    if b then Some (sigma, metasubst, evarsubst)
 	    else 
 	      if is_ground_term sigma m1 && is_ground_term sigma n1 then
@@ -787,7 +787,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       match res with
       | Some substn -> substn
       | None ->
-      let cf1 = key_of env b flags f1 and cf2 = key_of env b flags f2 in
+      let cf1 = key_of curenv b flags f1 and cf2 = key_of curenv b flags f2 in
 	match oracle_order curenv cf1 cf2 with
 	| None -> error_cannot_unify curenv sigma (cM,cN)
 	| Some true ->
@@ -815,11 +815,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 
-  and canonical_projections curenvnb pb b cM cN (sigma,_,_ as substn) =
+  and canonical_projections (curenv, _ as curenvnb) pb b cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp cM then
 	let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
-	  if is_open_canonical_projection env sigma f1l1 then
+	  if is_open_canonical_projection curenv sigma f1l1 then
 	    let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
 	      solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -835,7 +835,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	try f1 () with e when precatchable_exception e ->
 	  if isApp cN then
 	    let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
-	      if is_open_canonical_projection env sigma f2l2 then
+	      if is_open_canonical_projection curenv sigma f2l2 then
 		let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
 		  solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
 	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)