diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 14:32:25 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-29 14:57:12 +0200 |
commit | 449123ef56e7d323d89ba2cc331b007f695b29e9 (patch) | |
tree | a63c481a850cb48f1a121e8b2089614aee0cf069 | |
parent | 883611696f3388ac5fb9b08930f0ea4564749446 (diff) |
Rework code for refolding projections in whd_state/whd_simpl to allow Arguments
Specifications indicating that the record object must be a constructor. Fixes bug #3432.
-rw-r--r-- | pretyping/reductionops.ml | 39 | ||||
-rw-r--r-- | pretyping/tacred.ml | 4 |
2 files changed, 31 insertions, 12 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f4b32ee77..e6844673c 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -513,9 +513,10 @@ struct | _ -> def in List.fold_left (aux sk) s l - let constr_of_cst_member = function - | Cst_const (c, u) -> mkConstU (c,u) - | Cst_proj (p, c) -> mkProj (p, c) + let constr_of_cst_member f sk = + match f with + | Cst_const (c, u) -> mkConstU (c,u), sk + | Cst_proj (p, c) -> mkProj (p, c), tail 1 sk let rec zip ?(refold=false) = function | f, [] -> f @@ -532,9 +533,9 @@ struct | f, (Fix (fix,st,_)::s) -> zip ~refold (mkFix fix, st @ (append_app [|f|] s)) | f, (Cst (cst,_,_,params,cst_l)::s) when refold -> - zip ~refold (best_state (constr_of_cst_member cst,params @ (append_app [|f|] s)) cst_l) + zip ~refold (best_state (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> - zip ~refold (constr_of_cst_member cst,params @ (append_app [|f|] s)) + zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s))) | f, (Shift n::s) -> zip ~refold (lift n f, s) | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (p,f),s) | _, (Update _::_) -> assert false @@ -823,17 +824,26 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1)))) then fold () else - match List.map (fun x -> x - (npars + 1)) recargs with + 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 -> match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> + | curr::remains -> + if curr == 0 then (* Try to reduce the record argument *) whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_proj (p, c),curr,remains,bef,cst_l)::s') + (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) | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> apply_subst whrec [b] cst_l c stack @@ -898,7 +908,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj (p, c) -> - whrec Cst_stack.empty (mkProj (p, c), s' @ (Stack.append_app [|x'|] s''))) + let pb = lookup_projection p env in + let npars = pb.Declarations.proj_npars in + let narg = pb.Declarations.proj_arg in + let stack = s' @ (Stack.append_app [|x'|] s'') in + match Stack.strip_n_app 0 stack with + | None -> assert false + | Some (_,arg,s'') -> + whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p) :: s'')) | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with | None -> fold () | Some (bef,arg,s''') -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7b26a73b1..fad8623b0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -738,7 +738,9 @@ and whd_simpl_stack env sigma = (match ReductionBehaviour.get (ConstRef p) with | Some (l, n, f) when List.mem `ReductionNeverUnfold f -> (* simpl never *) s' | Some (l, n, f) when not (List.is_empty l) -> - let l' = List.map (fun i -> i - (pb.Declarations.proj_npars + 1)) l in + let l' = List.map_filter (fun i -> + let idx = (i - (pb.Declarations.proj_npars + 1)) in + if idx < 0 then None else Some idx) l in let stack = reduce_params env sigma stack l' in (match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack |