diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 3 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 329 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 17 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 4 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/output/reduction.out | 4 | ||||
| -rw-r--r-- | test-suite/output/reduction.v | 13 |
9 files changed, 213 insertions, 167 deletions
@@ -26,6 +26,8 @@ Tactics - New tactics [apply -> term], [apply <- term], [apply -> term in ident], [apply <- term in ident] for applying equivalences (iff). +- Slight improvement of the hnf and simpl tactics when applied on + expressions with explicit occurrences of match or fix. Changes from V8.1gamma to V8.1 ============================== diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 987d07912..8c792dc80 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -181,7 +181,8 @@ val is_arity : env -> evar_map -> constr -> bool val whd_programs : reduction_function -(* [reduce_fix] contracts a fix redex if it is actually reducible *) +(* [reduce_fix redfun fix stk] contracts [fix stk] if it is actually + reducible; the structural argument is reduced by [redfun] *) type fix_reduction_result = NotReducible | Reduced of state diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index d79295c0b..9c6582bec 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -90,8 +90,8 @@ let reference_value sigma env c = | Some d -> d (************************************************************************) -(* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick *) -(* is to reuse the name of the function after reduction of the fixpoint *) +(* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic). *) +(* One reuses the name of the function after reduction of the fixpoint *) type constant_evaluation = | EliminationFix of int * (int * (int * constr) list * int) @@ -103,7 +103,6 @@ type constant_evaluation = (* We use a cache registered as a global table *) - module CstOrdered = struct type t = constant @@ -325,20 +324,18 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) -> let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in let tij' = substl (List.rev subst) tij in - mkLambda (x,tij',c) - ) 1 body (List.rev lv) + mkLambda (x,tij',c)) 1 body (List.rev lv) in Some g -(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)] make - the reduction using this extra information *) +(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: + do so that the reduction uses this extra information *) let contract_fix_use_function f - ((recindices,bodynum),(types,names,bodies as typedbodies)) = + ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = match f j with | None -> mkFix((recindices,j),typedbodies) | Some c -> c in -(* match List.nth names j with Name id -> f id | _ -> assert false in*) let lbodies = list_tabulate make_Fi nbodies in substl (List.rev lbodies) bodies.(bodynum) @@ -358,12 +355,11 @@ let reduce_fix_use_function f whfun fix stack = Reduced (contract_fix_use_function f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = +let contract_cofix_use_function f (bodynum,(names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in - let make_Fi j = match f j with + let make_Fi j = match f names.(j) with | None -> mkCoFix(j,typedbodies) | Some c -> c in -(* match List.nth names j with Name id -> f id | _ -> assert false in*) let subbodies = list_tabulate make_Fi nbodies in substl subbodies bodies.(bodynum) @@ -372,19 +368,16 @@ let reduce_mind_case_use_function func env mia = | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1), real_cargs) - | CoFix (_,(names,_,_) as cofix) -> - let build_fix_name i = - match names.(i) with - | Name id -> - if isConst func then - let (mp,dp,_) = repr_con (destConst func) in - let kn = make_con mp dp (label_of_id id) in - (match constant_opt_value env kn with - | None -> None - | Some _ -> Some (mkConst kn)) - else None - | Anonymous -> None in - let cofix_def = contract_cofix_use_function build_fix_name cofix in + | CoFix cofix -> + let build_cofix_name = function + | Name id when isConst func -> + let (mp,dp,_) = repr_con (destConst func) in + let kn = make_con mp dp (label_of_id id) in + (match constant_opt_value env kn with + | None -> None + | Some _ -> Some (mkConst kn)) + | _ -> None in + let cofix_def = contract_cofix_use_function build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -412,20 +405,23 @@ let special_red_case sigma env whfun (ci, p, c, lf) = in redrec (c, empty_stack) +(* [red_elim_const] contracts iota/fix/cofix redexes hidden behind + constants by keeping the name of the constants in the recursive calls; + it fails if no redex is around *) let rec red_elim_const env sigma ref largs = match reference_eval sigma env ref with | EliminationCases n when stack_args_size largs >= n -> let c = reference_value sigma env ref in let c', lrest = whd_betadelta_state env sigma (c,largs) in - (special_red_case sigma env (construct_const env sigma) (destCase c'), - lrest) + let whfun = whd_simpl_state env sigma in + (special_red_case sigma env whfun (destCase c'), lrest) | EliminationFix (min,infos) when stack_args_size largs >=min -> let c = reference_value sigma env ref in let d, lrest = whd_betadelta_state env sigma (c,largs) in let f = make_elim_fun ([|Some ref|],infos) largs in - let co = construct_const env sigma in - (match reduce_fix_use_function f co (destFix d) lrest with + let whfun = whd_construct_state env sigma in + (match reduce_fix_use_function f whfun (destFix d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta c, rest)) | EliminationMutualFix (min,refgoal,refinfos) @@ -440,53 +436,65 @@ let rec red_elim_const env sigma ref largs = let (_, midargs as s) = descend ref largs in let d, lrest = whd_betadelta_state env sigma s in let f = make_elim_fun refinfos midargs in - let co = construct_const env sigma in - (match reduce_fix_use_function f co (destFix d) lrest with + let whfun = whd_construct_state env sigma in + (match reduce_fix_use_function f whfun (destFix d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta c, rest)) | _ -> raise Redelimination -and construct_const env sigma = - let rec hnfstack (x, stack as s) = +(* reduce to whd normal form or to an applied constant that does not hide + a reducible iota/fix/cofix redex (the "simpl" tactic) *) + +and whd_simpl_state env sigma s = + let rec redrec (x, stack as s) = match kind_of_term x with - | Cast (c,_,_) -> hnfstack (c, stack) - | App (f,cl) -> hnfstack (f, append_stack cl stack) - | Lambda (id,t,c) -> + | Lambda (na,t,c) -> (match decomp_stack stack with - | None -> assert false - | Some (c',rest) -> - stacklam hnfstack [c'] c rest) - | LetIn (n,b,t,c) -> stacklam hnfstack [b] c stack + | None -> s + | Some (a,rest) -> stacklam redrec [a] c rest) + | LetIn (n,b,t,c) -> stacklam redrec [b] c stack + | App (f,cl) -> redrec (f, append_stack cl stack) + | Cast (c,_,_) -> redrec (c, stack) | Case (ci,p,c,lf) -> - hnfstack - (special_red_case sigma env - (construct_const env sigma) (ci,p,c,lf), stack) - | Construct _ -> s - | CoFix _ -> s - | Fix fix -> - (match reduce_fix hnfstack fix stack with - | Reduced s' -> hnfstack s' - | NotReducible -> raise Redelimination) + (try + redrec (special_red_case sigma env redrec (ci,p,c,lf), stack) + with + Redelimination -> s) + | Fix fix -> + (try match reduce_fix (whd_construct_state env sigma) fix stack with + | Reduced s' -> redrec s' + | NotReducible -> s + with Redelimination -> s) | _ when isEvalRef env x -> let ref = destEvalRef x in (try - hnfstack (red_elim_const env sigma ref stack) + redrec (red_elim_const env sigma ref stack) with Redelimination -> - (match reference_opt_value sigma env ref with - | Some cval -> - (match kind_of_term cval with - | CoFix _ -> s - | _ -> hnfstack (cval, stack)) - | None -> - raise Redelimination)) - | _ -> raise Redelimination + s) + | _ -> s in - hnfstack + redrec s + +(* reduce until finding an applied constructor or fail *) + +and whd_construct_state env sigma s = + let (constr, cargs as s') = whd_simpl_state env sigma s in + if reducible_mind_case constr then s' + else if isEvalRef env constr then + let ref = destEvalRef constr in + match reference_opt_value sigma env ref with + | None -> raise Redelimination + | Some gvalue -> whd_construct_state env sigma (gvalue, cargs) + else + raise Redelimination (************************************************************************) (* Special Purpose Reduction Strategies *) -(* Red reduction tactic: reduction to a product *) +(* Red reduction tactic: one step of delta reduction + full + beta-iota-fix-cofix-zeta-cast at the head of the conclusion of a + sequence of products; fails if no delta redex is around +*) let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in @@ -521,77 +529,89 @@ let red_product env sigma c = try try_red_product env sigma c with Redelimination -> error "Not reducible" -let hnf_constr env sigma c = - let rec redrec (x, largs as s) = +(* +(* This old version of hnf uses betadeltaiota instead of itself (resp + whd_construct_state) to reduce the argument of Case (resp Fix); + The new version uses the "simpl" strategy instead. For instance, + + Variable n:nat. + Eval hnf in match (plus (S n) O) with S n => n | _ => O end. + + returned + + (fix plus (n m : nat) {struct n} : nat := + match n with + | O => m + | S p => S (plus p m) + end) n 0 + + while the new version returns (plus n O) + *) + +let whd_simpl_orelse_delta_but_fix_old env sigma c = + let whd_all = whd_betadeltaiota_state env sigma in + let rec redrec (x, stack as s) = match kind_of_term x with - | Lambda (n,t,c) -> - (match decomp_stack largs with - | None -> app_stack s - | Some (a,rest) -> - stacklam redrec [a] c rest) - | LetIn (n,b,t,c) -> stacklam redrec [b] c largs - | App (f,cl) -> redrec (f, append_stack cl largs) - | Cast (c,_,_) -> redrec (c, largs) - | Case (ci,p,c,lf) -> + | Lambda (na,t,c) -> + (match decomp_stack stack with + | None -> s + | Some (a,rest) -> stacklam redrec [a] c rest) + | LetIn (n,b,t,c) -> stacklam redrec [b] c stack + | App (f,cl) -> redrec (f, append_stack cl stack) + | Cast (c,_,_) -> redrec (c, stack) + | Case (ci,p,d,lf) -> (try - redrec - (special_red_case sigma env (whd_betadeltaiota_state env sigma) - (ci, p, c, lf), largs) + redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack) with Redelimination -> - app_stack s) + s) | Fix fix -> - (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with + (match reduce_fix whd_all fix stack with | Reduced s' -> redrec s' - | NotReducible -> app_stack s) + | NotReducible -> s) | _ when isEvalRef env x -> let ref = destEvalRef x in (try - let (c',lrest) = red_elim_const env sigma ref largs in - redrec (c', lrest) + redrec (red_elim_const env sigma ref stack) with Redelimination -> match reference_opt_value sigma env ref with | Some c -> (match kind_of_term (snd (decompose_lam c)) with - | CoFix _ | Fix _ -> app_stack (x,largs) - | _ -> redrec (c, largs)) - | None -> app_stack s) - | _ -> app_stack s - in - redrec (c, empty_stack) + | CoFix _ | Fix _ -> s + | _ -> redrec (c, stack)) + | None -> s) + | _ -> s + in app_stack (redrec (c, empty_stack)) +*) -(* Simpl reduction tactic: same as simplify, but also reduces - elimination constants *) +(* Same as [whd_simpl] but also reduces constants that do not hide a + reducible fix, but does this reduction of constants only until it + it immediately hides a non reducible fix or a cofix *) -let whd_nf env sigma c = - let rec nf_app (c, stack as s) = - match kind_of_term c with - | Lambda (name,c1,c2) -> - (match decomp_stack stack with - | None -> (c,empty_stack) - | Some (a1,rest) -> - stacklam nf_app [a1] c2 rest) - | LetIn (n,b,t,c) -> stacklam nf_app [b] c stack - | App (f,cl) -> nf_app (f, append_stack cl stack) - | Cast (c,_,_) -> nf_app (c, stack) - | Case (ci,p,d,lf) -> - (try - nf_app (special_red_case sigma env nf_app (ci,p,d,lf), stack) - with Redelimination -> - s) - | Fix fix -> - (match reduce_fix nf_app fix stack with - | Reduced s' -> nf_app s' - | NotReducible -> s) - | _ when isEvalRef env c -> - (try - nf_app (red_elim_const env sigma (destEvalRef c) stack) - with Redelimination -> - s) - | _ -> s - in - app_stack (nf_app (c, empty_stack)) +let whd_simpl_orelse_delta_but_fix env sigma c = + let rec redrec s = + let (constr, stack as s') = whd_simpl_state env sigma s in + if isEvalRef env constr then + match reference_opt_value sigma env (destEvalRef constr) with + | Some c -> + (match kind_of_term (snd (decompose_lam c)) with + | CoFix _ | Fix _ -> s' + | _ -> redrec (c, stack)) + | None -> s' + else s' + in app_stack (redrec (c, empty_stack)) + +let hnf_constr = whd_simpl_orelse_delta_but_fix + +(* The "simpl" reduction tactic *) + +let whd_simpl env sigma c = + app_stack (whd_simpl_state env sigma (c, empty_stack)) + +let simpl env sigma c = strong whd_simpl env sigma c -let nf env sigma c = strong whd_nf env sigma c +let nf = simpl (* Compatibility *) + +(* Reduction at specific subterms *) let is_head c t = match kind_of_term t with @@ -808,69 +828,66 @@ let pattern_occs loccs_trm env sigma c = (* Used in several tactics. *) +(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name + return name, B and t' *) + +let reduce_to_ind_gen allow_product env sigma t = + let rec elimrec env t l = + let t = hnf_constr env sigma t in + match kind_of_term (fst (decompose_app t)) with + | Ind ind-> (ind, it_mkProd_or_LetIn t l) + | Prod (n,ty,t') -> + if allow_product then + elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l) + else + errorlabstrm "tactics__reduce_to_mind" + (str"Not an inductive definition") + | _ -> + errorlabstrm "tactics__reduce_to_mind" + (str"Not an inductive product") + in + elimrec env t [] + +let reduce_to_quantified_ind x = reduce_to_ind_gen true x +let reduce_to_atomic_ind x = reduce_to_ind_gen false x + +(* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta] + or raise [NotStepReducible] if not a weak-head redex *) + exception NotStepReducible let one_step_reduce env sigma c = - let rec redrec (x, largs) = + let rec redrec (x, stack) = match kind_of_term x with | Lambda (n,t,c) -> - (match decomp_stack largs with + (match decomp_stack stack with | None -> raise NotStepReducible | Some (a,rest) -> (subst1 a c, rest)) - | App (f,cl) -> redrec (f, append_stack cl largs) - | LetIn (_,f,_,cl) -> (subst1 f cl,largs) + | App (f,cl) -> redrec (f, append_stack cl stack) + | LetIn (_,f,_,cl) -> (subst1 f cl,stack) + | Cast (c,_,_) -> redrec (c,stack) | Case (ci,p,c,lf) -> (try - (special_red_case sigma env (whd_betadeltaiota_state env sigma) - (ci,p,c,lf), largs) + (special_red_case sigma env (whd_simpl_state env sigma) + (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with + (match reduce_fix (whd_construct_state env sigma) fix stack with | Reduced s' -> s' | NotReducible -> raise NotStepReducible) - | Cast (c,_,_) -> redrec (c,largs) | _ when isEvalRef env x -> - let ref = - try destEvalRef x - with Redelimination -> raise NotStepReducible in + let ref = destEvalRef x in (try - red_elim_const env sigma ref largs + red_elim_const env sigma ref stack with Redelimination -> match reference_opt_value sigma env ref with - | Some d -> d, largs + | Some d -> d, stack | None -> raise NotStepReducible) | _ -> raise NotStepReducible in app_stack (redrec (c, empty_stack)) -(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name - return name, B and t' *) - -let reduce_to_ind_gen allow_product env sigma t = - let rec elimrec env t l = - let c, _ = Reductionops.whd_stack t in - match kind_of_term c with - | Ind (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l) - | Prod (n,ty,t') -> - if allow_product then - elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l) - else - errorlabstrm "tactics__reduce_to_mind" - (str"Not an inductive definition") - | _ -> - (try - let t' = nf_betaiota (one_step_reduce env sigma t) in - elimrec env t' l - with NotStepReducible -> - errorlabstrm "tactics__reduce_to_mind" - (str"Not an inductive product")) - in - elimrec env t [] - -let reduce_to_quantified_ind x = reduce_to_ind_gen true x -let reduce_to_atomic_ind x = reduce_to_ind_gen false x - let reduce_to_ref_gen allow_product env sigma ref t = let rec elimrec env t l = let c, _ = Reductionops.whd_stack t in diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 84cc87e7f..0ff5154f6 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -35,11 +35,15 @@ val red_product : reduction_function (* Red (raise Redelimination if nothing reducible) *) val try_red_product : reduction_function -(* Hnf *) -val hnf_constr : reduction_function - (* Simpl *) -val nf : reduction_function +val simpl : reduction_function + +(* Simpl only at the head *) +val whd_simpl : reduction_function + +(* Hnf: like whd_simpl but force delta-reduction of constants that do + not immediately hide a non reducible fix or cofix *) +val hnf_constr : reduction_function (* Unfold *) val unfoldn : @@ -79,3 +83,8 @@ val reduce_to_atomic_ref : val contextually : bool -> int list * constr -> reduction_function -> reduction_function + +(* Compatibility *) +(* use [simpl] instead of [nf] *) +val nf : reduction_function + diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c69d1be36..2f85b18e5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -106,8 +106,8 @@ let reduction_of_red_expr = function else (red_product,DEFAULTcast) | Hnf -> (hnf_constr,DEFAULTcast) | Simpl (Some (_,c as lp)) -> - (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast) - | Simpl None -> (nf,DEFAULTcast) + (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast) + | Simpl None -> (simpl,DEFAULTcast) | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 500a7f40d..1273c65e4 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -903,7 +903,7 @@ let new_morphism m signature id hook = (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref)) env Evd.empty lem in (* "simpl" *) - let lem = Tacred.nf env Evd.empty lem in + let lem = Tacred.simpl env Evd.empty lem in if Lib.is_modtype () then begin ignore diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9e25055e9..f9e623469 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -208,9 +208,9 @@ let red_option = reduct_option (red_product,DEFAULTcast) let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast) let hnf_in_hyp = reduct_in_hyp hnf_constr let hnf_option = reduct_option (hnf_constr,DEFAULTcast) -let simpl_in_concl = reduct_in_concl (nf,DEFAULTcast) -let simpl_in_hyp = reduct_in_hyp nf -let simpl_option = reduct_option (nf,DEFAULTcast) +let simpl_in_concl = reduct_in_concl (simpl,DEFAULTcast) +let simpl_in_hyp = reduct_in_hyp simpl +let simpl_option = reduct_option (simpl,DEFAULTcast) let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast) let normalise_in_hyp = reduct_in_hyp compute let normalise_option = reduct_option (compute,DEFAULTcast) diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out new file mode 100644 index 000000000..ff327aa5f --- /dev/null +++ b/test-suite/output/reduction.out @@ -0,0 +1,4 @@ + = a + : nat + = n + 0 + : nat diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v new file mode 100644 index 000000000..4a460a83f --- /dev/null +++ b/test-suite/output/reduction.v @@ -0,0 +1,13 @@ +(* Test the behaviour of hnf and simpl introduced in revision *) + +Variable n:nat. +Definition a:=0. + +Eval simpl in (fix plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (p + m) + end) a a. + +Eval hnf in match (plus (S n) O) with S n => n | _ => O end. + |