diff options
| -rw-r--r-- | pretyping/evarconv.ml | 56 |
1 files changed, 35 insertions, 21 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8e84d799b4..2184d44d34 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -288,6 +288,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) | None -> (i,false) in ise_try evd [f1; f2; f3] in + let eta env evd onleft sk term sk' term' = + assert (match sk with [] -> true | _ -> 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 + in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) @@ -401,16 +411,28 @@ 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 -> - miller_pfenning true + let f1 evd = + miller_pfenning true ((* Postpone the use of an heuristic *) add_conv_pb (pbty,env,zip appr1,zip appr2) evd, true) ev1 appr1 appr2 evd + and f2 evd = + if isLambda term2 then + eta env evd false sk2 term2 sk1 term1 + else (evd,false) + in ise_try evd [f1;f2] | Rigid, Flexible ev2 -> - miller_pfenning false + let f1 evd = + miller_pfenning false ((* Postpone the use of an heuristic *) add_conv_pb (pbty,env,zip appr1,zip appr2) evd, true) ev2 appr2 appr1 evd + and f2 evd = + if isLambda term1 then + eta env evd true sk1 term1 sk2 term2 + else (evd,false) + in ise_try evd [f1;f2] | MaybeFlexible, Rigid -> let f3 i = @@ -421,9 +443,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) | Some v1 -> evar_eqappr_x ts env i pbty (whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2 - | None -> (i,false) - in - ise_try evd [f3; f4] + | None -> + if isLambda term2 then eta env evd false sk2 term2 sk1 term1 + else (i,false) + in + ise_try evd [f3; f4] | Rigid, MaybeFlexible -> let f3 i = @@ -434,28 +458,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) | Some v2 -> evar_eqappr_x ts env i pbty appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2)) - | None -> (i,false) + | None -> + if isLambda term1 then eta env evd true sk1 term1 sk2 term2 + else (i,false) in - ise_try evd [f3; f4] + ise_try evd [f3; f4] (* Eta-expansion *) | Rigid, _ when isLambda term1 -> - assert (match sk1 with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda term1 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 (term2, sk2 @ [Zshift 1]), [Zapp [mkRel 1]]) in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd true sk1 term1 sk2 term2 | _, Rigid when isLambda term2 -> - assert (match sk2 with [] -> true | _ -> false); - let (na,c2,c'2) = destLambda term2 in - let c = nf_evar evd c2 in - let env' = push_rel (na,None,c) env in - let appr1 = whd_nored_state evd (zip (term1, sk1 @ [Zshift 1]), [Zapp [mkRel 1]]) in - let appr2 = whd_betaiota_deltazeta_for_iota_state ts env' evd (c'2, empty_stack) in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin match kind_of_term term1, kind_of_term term2 with |