From e9ddf697a1451f1928e05dba9722c876b6962e45 Mon Sep 17 00:00:00 2001 From: Theo Zimmermann Date: Tue, 16 Jun 2015 18:50:58 +0200 Subject: Strategy is now a record type with a function field. --- tactics/rewrite.ml | 99 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 57 insertions(+), 42 deletions(-) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b442ca98b..fa9710ea3 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -652,14 +652,14 @@ type rewrite_result = | Identity | Success of rewrite_result_info -type 'a pure_strategy = +type 'a pure_strategy = { strategy : 'a -> (* a parameter: for instance, a state *) Environ.env -> Id.t list -> (* Unfresh names *) constr -> types -> (* first term and its type (convertible to rew_from) *) (bool (* prop *) * constr option) -> evars -> - 'a * rewrite_result (* the updated state for instance and the "result" *) + 'a * rewrite_result (* the updated state for instance and the "result" *) } type strategy = unit pure_strategy @@ -831,7 +831,7 @@ let apply_rule unify loccs : int pure_strategy = then List.mem occ occs else not (List.mem occ occs) in - fun occ env avoid t ty cstr evars -> + { strategy = fun occ env avoid t ty cstr evars -> let unif = if isEvar t then None else unify env evars t in match unif with | None -> (occ, Fail) @@ -844,8 +844,9 @@ let apply_rule unify loccs : int pure_strategy = let rel, prf = get_rew_prf res in let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in (occ, res) + } -let apply_lemma l2r flags oc by loccs : strategy = +let apply_lemma l2r flags oc by loccs : strategy = { strategy = fun () env avoid t ty cstr (sigma, cstrs) -> let sigma, c = oc sigma in let sigma, hypinfo = decompose_applied_relation env sigma c in @@ -858,8 +859,9 @@ let apply_lemma l2r flags oc by loccs : strategy = | None -> None | Some rew -> Some rew in - let _, res = apply_rule unify loccs 0 env avoid t ty cstr evars in + let _, res = (apply_rule unify loccs).strategy 0 env avoid t ty cstr evars in (), res + } let e_app_poly env evars f args = let evars', c = app_poly_nocheck env !evars f args in @@ -951,7 +953,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = state, (None :: acc, evars, progress) else let argty = Retyping.get_type_of env (goalevars evars) arg in - let state, res = s state env avoid arg argty (prop,None) evars in + let state, res = s.strategy state env avoid arg argty (prop,None) evars in let res' = match res with | Identity -> @@ -1003,7 +1005,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = evars, Some cstr', m, mty, args, Array.of_list args | None -> evars, None, m, mty, argsl, args in - let state, m' = s state env avoid m mty (prop, cstr') evars in + let state, m' = s.strategy state env avoid m mty (prop, cstr') evars in match m' with | Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *) | Identity -> rewrite_args state (Some false) @@ -1110,7 +1112,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let env' = Environ.push_rel (n', None, t) env in let bty = Retyping.get_type_of env' (goalevars evars) b in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in - let state, b' = s state env' avoid b bty (prop, unlift env evars cstr) evars in + let state, b' = s.strategy state env' avoid b bty (prop, unlift env evars cstr) evars in let res = match b' with | Success r -> @@ -1135,7 +1137,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = 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 - let state, c' = s state env avoid c cty (prop, cstr') evars' in + let state, c' = s.strategy state env avoid c cty (prop, cstr') evars' in let state, res = match c' with | Success r -> @@ -1151,7 +1153,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = if not (Option.is_empty found) then (state, found, fun x -> lift 1 br :: acc x) else - let state, res = s state env avoid br ty (prop,cstr) evars in + let state, res = s.strategy state env avoid br ty (prop,cstr) evars in match res with | Success r -> (state, Some r, fun x -> mkRel 1 :: acc x) | Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x)) @@ -1184,7 +1186,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> res in state, res | _ -> state, Fail - in aux + in { strategy = aux } let all_subterms = subterm true default_flags let one_subterm = subterm false default_flags @@ -1195,7 +1197,7 @@ let one_subterm = subterm false default_flags let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) : 'a * rewrite_result = let state, nextres = - next state env avoid res.rew_to res.rew_car + next.strategy state env avoid res.rew_to res.rew_car (prop, get_opt_rew_rel res.rew_prf) res.rew_evars in let res = @@ -1232,15 +1234,17 @@ let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pur module Strategies = struct - let fail : 'a pure_strategy = + let fail : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> - state, Fail + state, Fail + } - let id : 'a pure_strategy = + let id : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> - state, Identity + state, Identity + } - let refl : 'a pure_strategy = + let refl : 'a pure_strategy = { strategy = fun state env avoid t ty (prop,cstr) evars -> let evars, rel = match cstr with | None -> @@ -1260,29 +1264,33 @@ module Strategies = let res = Success { rew_car = ty; rew_from = t; rew_to = t; rew_prf = RewPrf (rel, proof); rew_evars = evars } in state, res + } - let progress (s : 'a pure_strategy) : 'a pure_strategy = + let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> - let state, res = s state env avoid t ty cstr evars in + let state, res = s.strategy state env avoid t ty cstr evars in match res with | Fail -> state, Fail | Identity -> state, Fail | Success r -> state, Success r + } - let seq first snd : 'a pure_strategy = + let seq first snd : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> - let state, res = first state env avoid t ty cstr evars in + let state, res = first.strategy state env avoid t ty cstr evars in match res with | Fail -> state, Fail - | Identity -> snd state env avoid t ty cstr evars + | Identity -> snd.strategy state env avoid t ty cstr evars | Success res -> transitivity state env avoid (fst cstr) res snd + } - let choice fst snd : 'a pure_strategy = + let choice fst snd : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> - let state, res = fst state env avoid t ty cstr evars in + let state, res = fst.strategy state env avoid t ty cstr evars in match res with - | Fail -> snd state env avoid t ty cstr evars + | Fail -> snd.strategy state env avoid t ty cstr evars | Identity | Success _ -> state, res + } let try_ str : 'a pure_strategy = choice str id @@ -1291,7 +1299,8 @@ module Strategies = str s e l c t r ev let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy = - let rec aux state = f (fun state -> check_interrupt aux state) state in aux + let rec aux state = (f { strategy = fun state -> check_interrupt aux state }).strategy state in + { strategy = aux } let any (s : 'a pure_strategy) : 'a pure_strategy = fix (fun any -> try_ (seq s any)) @@ -1327,15 +1336,16 @@ module Strategies = (List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules) - let hints (db : string) : 'a pure_strategy = + let hints (db : string) : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> let rules = Autorewrite.find_matches db t in let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac) in let lems = List.map lemma rules in - lemmas lems state env avoid t ty cstr evars + (lemmas lems).strategy state env avoid t ty cstr evars + } - let reduce (r : Redexpr.red_expr) : 'a pure_strategy = + let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in let evars', t' = rfn env (goalevars evars) t in @@ -1345,8 +1355,9 @@ module Strategies = state, Success { rew_car = ty; rew_from = t; rew_to = t'; rew_prf = RewCast ckind; rew_evars = evars', cstrevars evars } + } - let fold_glob c : 'a pure_strategy = + let fold_glob c : 'a pure_strategy = { strategy = fun state env avoid t ty cstr evars -> (* 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 @@ -1362,6 +1373,7 @@ module Strategies = rew_prf = RewCast DEFAULTcast; rew_evars = (sigma, snd evars) } with e when Errors.noncritical e -> state, Fail + } end @@ -1372,7 +1384,7 @@ end even finding a first application of the rewriting lemma, in setoid_rewrite mode *) -let rewrite_with l2r flags c occs : strategy = +let rewrite_with l2r flags c occs : strategy = { strategy = fun () env avoid t ty cstr (sigma, cstrs) -> let unify env evars t = let (sigma, cstrs) = evars in @@ -1393,12 +1405,13 @@ let rewrite_with l2r flags c occs : strategy = Strategies.fix (fun aux -> Strategies.choice app (subterm true default_flags aux)) in - let _, res = strat 0 env avoid t ty cstr (sigma, cstrs) in - ((), res) + let _, res = strat.strategy 0 env avoid t ty cstr (sigma, cstrs) in + ((), res) + } let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars = let ty = Retyping.get_type_of env (goalevars evars) concl in - let _, res = s () env avoid concl ty (prop, Some cstr) evars in + let _, res = s.strategy () env avoid concl ty (prop, Some cstr) evars in res let solve_constraints env (evars,cstrs) = @@ -1583,7 +1596,7 @@ let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars -> (sigma, (c, NoBindings)) in let flags = general_rewrite_unif_flags () in - apply_lemma l2r flags c None occs () env avoid t ty cstr evars + (apply_lemma l2r flags c None occs).strategy () env avoid t ty cstr evars let interp_glob_constr_list env = let make c = (); fun sigma -> @@ -1647,16 +1660,17 @@ let rec strategy_of_ast = function | Compose -> Strategies.seq | Choice -> Strategies.choice in f' s' t' - | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences + | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences } | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id - | StratTerms l -> + | StratTerms l -> { strategy = (fun () env avoid t ty cstr evars -> let l' = interp_glob_constr_list env (List.map fst l) in - Strategies.lemmas l' () env avoid t ty cstr evars) - | StratEval r -> + (Strategies.lemmas l').strategy () env avoid t ty cstr evars) + } + | StratEval r -> { strategy = (fun () env avoid t ty cstr evars -> let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in - Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars)) + (Strategies.reduce r_interp).strategy () env avoid t ty cstr (sigma,cstrevars evars)) } | StratFold c -> Strategies.fold_glob (fst c) @@ -1965,9 +1979,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let app = apply_rule unify occs in let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in let substrat = Strategies.fix recstrat in - let strat () env avoid t ty cstr evars = - let _, res = substrat 0 env avoid t ty cstr evars in + let strat = { strategy = fun () env avoid t ty cstr evars -> + let _, res = substrat.strategy 0 env avoid t ty cstr evars in (), res + } in let origsigma = project gl in init_setoid (); -- cgit v1.2.3