diff options
| -rw-r--r-- | pretyping/evarconv.ml | 40 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 68 |
2 files changed, 59 insertions, 49 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 53c560f86..ed04c7150 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -497,22 +497,34 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] | Proj (p, t), Const (p',_) when eq_constant p p' -> - let pb = Environ.lookup_projection p env in - (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with - | Some (pars, t', rest) -> - ise_and evd - [(fun i -> evar_conv_x ts env i CONV t t'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)] - | None -> UnifFailure (evd, NotSameHead)) + let f1 i = + let pb = Environ.lookup_projection p env in + (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with + | Some (pars, t', rest) -> + ise_and i + [(fun i -> evar_conv_x ts env i CONV t t'); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)] + | None -> UnifFailure (evd, NotSameHead)) + and f2 i = + let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1') + and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2') + in evar_eqappr_x ts env i pbty out1 out2 + in ise_try evd [f1;f2] | Const (p',_), Proj (p, t) when eq_constant p p' -> - let pb = Environ.lookup_projection p env in - (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with - | Some (pars, t', rest) -> - ise_and evd - [(fun i -> evar_conv_x ts env i CONV t t'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)] - | None -> UnifFailure (evd, NotSameHead)) + let f1 i = + let pb = Environ.lookup_projection p env in + (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with + | Some (pars, t', rest) -> + ise_and i + [(fun i -> evar_conv_x ts env i CONV t t'); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)] + | None -> UnifFailure (evd, NotSameHead)) + and f2 i = + let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1') + and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2') + in evar_eqappr_x ts env i pbty out1 out2 + in ise_try evd [f1;f2] | _, _ -> let f1 i = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5ca61e365..260a012aa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -810,41 +810,39 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s') ) | Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) -> - (match (lookup_constant p env).Declarations.const_proj with - | None -> assert false - | Some pb -> begin - let npars = pb.Declarations.proj_npars - and arg = pb.Declarations.proj_arg in - match ReductionBehaviour.get (Globnames.ConstRef p) with - | None -> - let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in - whrec Cst_stack.empty(* cst_l *) stack' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags - || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1)))) - then fold () - else - let recargs = List.map_filter (fun x -> - let idx = x - npars in - if idx < 0 then None else Some idx) recargs - in - match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) - let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in - whrec Cst_stack.empty(* cst_l *) stack' - | curr::remains -> - if curr == 0 then (* Try to reduce the record argument *) - whrec Cst_stack.empty - (c, Stack.Cst(Stack.Cst_proj (p, c),curr,remains,Stack.empty,cst_l)::stack) - else - match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_proj (p, c),curr,remains,bef,cst_l)::s') - end) + (let pb = lookup_projection p env in + let npars = pb.Declarations.proj_npars + and arg = pb.Declarations.proj_arg in + match ReductionBehaviour.get (Globnames.ConstRef p) with + | None -> + let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in + whrec Cst_stack.empty(* cst_l *) stack' + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags + || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1)))) + then fold () + else + let recargs = List.map_filter (fun x -> + let idx = x - npars in + if idx < 0 then None else Some idx) recargs + in + match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) + let stack' = (c, Stack.Proj (npars, arg, p) :: stack) in + whrec Cst_stack.empty(* cst_l *) stack' + | curr::remains -> + if curr == 0 then (* Try to reduce the record argument *) + whrec Cst_stack.empty + (c, Stack.Cst(Stack.Cst_proj (p, c),curr,remains,Stack.empty,cst_l)::stack) + else + match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_proj (p, c),curr,remains,bef,cst_l)::s')) + | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> apply_subst whrec [b] cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) |