diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 49 |
1 files changed, 24 insertions, 25 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 77162ce89a..6d0e0c36b3 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -855,26 +855,20 @@ let coerce env cstr res = let res = { res with rew_evars = evars } in apply_constraint env res.rew_car rel prf cstr res -let apply_rule unify loccs : int pure_strategy = - let (nowhere_except_in,occs) = convert_occs loccs in - let is_occ occ = - if nowhere_except_in - then List.mem occ occs - else not (List.mem occ occs) - in - { strategy = fun { state = occ ; env ; +let apply_rule unify : occurrences_count pure_strategy = + { strategy = fun { state = occs ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with - | None -> (occ, Fail) + | None -> (occs, Fail) | Some rew -> - let occ = succ occ in - if not (is_occ occ) then (occ, Fail) - else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) + let b, occs = update_occurrence_counter occs in + if not b then (occs, Fail) + else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occs, Identity) else let res = { rew with rew_car = ty } in let res = Success (coerce env cstr res) in - (occ, res) + (occs, res) } let apply_lemma l2r flags oc by loccs : strategy = { strategy = @@ -890,9 +884,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy = | None -> None | Some rew -> Some rew in - let _, res = (apply_rule unify loccs).strategy { input with - state = 0 ; + let loccs, res = (apply_rule unify).strategy { input with + state = initialize_occurrence_counter loccs ; evars } in + check_used_occurrences loccs; (), res } @@ -923,7 +918,8 @@ let reset_env env = Environ.push_rel_context (Environ.rel_context env) env' let fold_match ?(force=false) env sigma c = - let (ci, p, iv, c, brs) = destCase sigma c in + let case = destCase sigma c in + let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in let cty = Retyping.get_type_of env sigma c in let dep, pred, exists, sk = let env', ctx, body = @@ -991,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let argty = Retyping.get_type_of env (goalevars evars) arg in let state, res = s.strategy { state ; env ; unfresh ; - term1 = arg ; ty1 = argty ; + term1 = arg ; ty1 = argty ; cstr = (prop,None) ; evars } in let res' = @@ -1158,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> b' in state, res - | Case (ci, p, iv, c, brs) -> + | Case (ci, u, pms, p, iv, c, brs) -> + let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in let cty = Retyping.get_type_of env (goalevars evars) c in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in @@ -1168,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let state, res = match c' with | Success r -> - let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in + let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in let res = make_leibniz_proof env case ty r in state, Success (coerce env (prop,cstr) res) | Fail | Identity -> @@ -1190,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in match found with | Some r -> - let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in + let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in state, Success (make_leibniz_proof env ctxc ty r) | None -> state, c' else @@ -1391,7 +1388,7 @@ module Strategies = let fold_glob c : 'a pure_strategy = { strategy = fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> -(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) +(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in let unfolded = try Tacred.try_red_product env sigma c @@ -1423,12 +1420,13 @@ let rewrite_with l2r flags c occs : strategy = { strategy = let (sigma, rew) = refresh_hypinfo env sigma c in unify_eqn rew l2r flags env (sigma, cstrs) None t in - let app = apply_rule unify occs in + let app = apply_rule unify in let strat = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in - let _, res = strat.strategy { input with state = 0 } in + let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in + check_used_occurrences occs; ((), res) } @@ -2076,11 +2074,12 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = Proofview.Goal.enter begin fun gl -> let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in let unify env evars t = unify_abs res l2r sort env evars t in - let app = apply_rule unify occs in + let app = apply_rule unify in let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in let substrat = Strategies.fix recstrat in let strat = { strategy = fun ({ state = () } as input) -> - let _, res = substrat.strategy { input with state = 0 } in + let occs, res = substrat.strategy { input with state = initialize_occurrence_counter occs } in + check_used_occurrences occs; (), res } in |