From 15d4547b977e96ed2bc26cea683f5f4f3c9ee137 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 3 May 2019 00:34:21 +0200 Subject: Abstract the Tactic.e_change_hyps function over the reduction function. --- tactics/tactics.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 806c955591..869e3039ab 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -614,7 +614,7 @@ let cofix id = mutual_cofix id [] 0 type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = +let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma decl = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> @@ -713,7 +713,7 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id gl in - let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + let (sigma, c) = e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp ~check ~reorder c) end @@ -721,13 +721,13 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> let fold (env, sigma) arg = - let (redfun, id, where) = f arg in + let (id, redfun) = f arg in let hyp = try lookup_named id env with Not_found -> raise (RefinerError (env, sigma, NoSuchHyp id)) in - let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in + let (sigma, d) = redfun env sigma hyp in let sign = Logic.convert_hyp ~check ~reorder env sigma d in let env = reset_with_named_context sign env in (env, sigma) @@ -851,7 +851,8 @@ let change ~check chg c cls = let f (id, occs, where) = let occl = bind_change_occurrences occs chg in let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in (* Don't check, we do it already in [change_on_subterm] *) e_change_in_hyps ~check:false ~reorder:check f hyps @@ -905,7 +906,8 @@ let reduce redexp cl = let redexp = bind_red_expr_occurrences occs nbcl redexp in let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in let redfun _ env sigma c = redfun env sigma c in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in e_change_in_hyps ~check ~reorder f hyps end -- cgit v1.2.3 From 3c6ed7485293c7eb80f9c4d415af0ee0b977f157 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 3 May 2019 00:41:55 +0200 Subject: Generalize map_named_val to handle whole declarations. --- engine/evd.ml | 2 +- engine/proofview.ml | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/engine/evd.ml b/engine/evd.ml index b89222cf8e..96c2719f8f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -222,7 +222,7 @@ let map_evar_body f = function let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; + evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } diff --git a/engine/proofview.ml b/engine/proofview.ml index f278c83912..6992d15fcb 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -46,7 +46,7 @@ let compact el ({ solution } as pv) = let apply_subst_einfo _ ei = Evd.({ ei with evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf0 ei.evar_hyps; + evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps; evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in diff --git a/kernel/environ.ml b/kernel/environ.ml index 97c9f8654a..617519a038 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with let map_named_val f ctxt = let open Context.Named.Declaration in let fold accu d = - let d' = map_constr f d in + let d' = f d in let accu = if d == d' then accu else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu diff --git a/kernel/environ.mli b/kernel/environ.mli index 8c6bc105c7..4e6dbbe206 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) + *** /!\ *** [f t] should be convertible with t, and preserve the name *) val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val + (named_declaration -> named_declaration) -> named_context_val -> named_context_val val push_named : Constr.named_declaration -> env -> env val push_named_context : Constr.named_context -> env -> env -- cgit v1.2.3 From ec6c11c67a01122f52f615691f120bde9da9a61e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 3 May 2019 00:38:25 +0200 Subject: Introducing a local flag to hypothesis conversion function. If the reduction function is known not to depend on the named context, then we can perform it in parallel on the various variables. --- tactics/tactics.ml | 62 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 49 insertions(+), 13 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 869e3039ab..ecb8c9dc1f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -718,23 +718,56 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = (convert_hyp ~check ~reorder c) end +type hyp_conversion = +| AnyHypConv (** Arbitrary conversion *) +| StableHypConv (** Does not introduce new dependencies on variables *) +| LocalHypConv (** Same as above plus no dependence on the named environment *) + let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> - let fold (env, sigma) arg = - let (id, redfun) = f arg in - let hyp = - try lookup_named id env - with Not_found -> - raise (RefinerError (env, sigma, NoSuchHyp id)) + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let (env, sigma) = match reorder with + | LocalHypConv -> + (* If the reduction function is known not to depend on the named + context, then we can perform it in parallel. *) + let fold accu arg = + let (id, redfun) = f arg in + let old = try Id.Map.find id accu with Not_found -> [] in + Id.Map.add id (redfun :: old) accu + in + let reds = List.fold_left fold Id.Map.empty args in + let evdref = ref sigma in + let map d = + let id = NamedDecl.get_id d in + match Id.Map.find id reds with + | reds -> + let d = EConstr.of_named_decl d in + let fold redfun (sigma, d) = redfun env sigma d in + let (sigma, d) = List.fold_right fold reds (sigma, d) in + let () = evdref := sigma in + EConstr.Unsafe.to_named_decl d + | exception Not_found -> d in - let (sigma, d) = redfun env sigma hyp in - let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in - (env, sigma) + (env, !evdref) + | StableHypConv | AnyHypConv -> + let reorder = reorder == AnyHypConv in + let fold (env, sigma) arg = + let (id, redfun) = f arg in + let hyp = + try lookup_named id env + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + in + let (sigma, d) = redfun env sigma hyp in + let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let env = reset_with_named_context sign env in + (env, sigma) + in + List.fold_left fold (env, sigma) args in - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (env, sigma) = List.fold_left fold (env, sigma) args in let ty = Proofview.Goal.concl gl in Proofview.Unsafe.tclEVARS sigma <*> @@ -854,8 +887,9 @@ let change ~check chg c cls = let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) in + let reorder = if check then AnyHypConv else StableHypConv in (* Don't check, we do it already in [change_on_subterm] *) - e_change_in_hyps ~check:false ~reorder:check f hyps + e_change_in_hyps ~check:false ~reorder f hyps end let change_concl t = @@ -909,6 +943,8 @@ let reduce redexp cl = let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) in + (* FIXME: use local flag *) + let reorder = if reorder then AnyHypConv else StableHypConv in e_change_in_hyps ~check ~reorder f hyps end end -- cgit v1.2.3 From 076932d4bf602560b24c14dc3397e51db5114244 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 3 May 2019 01:05:05 +0200 Subject: Actually use the conversion locality flag. Fixes #9919. --- tactics/tactics.ml | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ecb8c9dc1f..03b628dca3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -916,6 +916,22 @@ let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast) (* The main reduction function *) +let is_local_flag env flags = + if flags.rDelta then false + else + let check = function + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags.rConst + +let is_local_unfold env flags = + let check (_, c) = match c with + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags + let reduce redexp cl = let trace env sigma = let open Printer in @@ -924,27 +940,34 @@ let reduce redexp cl = in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in + let reorder = match redexp with + | Fold _ | Pattern _ -> AnyHypConv + | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags -> + if is_local_flag env flags then LocalHypConv else StableHypConv + | Unfold flags -> + if is_local_unfold env flags then LocalHypConv else StableHypConv + | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv + | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) + in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> let redexp = bind_red_expr_occurrences occs nbcl redexp in - let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let redfun = Redexpr.reduction_of_red_expr env redexp in e_change_in_concl ~check (revert_cast redfun) end <*> let f (id, occs, where) = let redexp = bind_red_expr_occurrences occs nbcl redexp in - let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let redfun _ env sigma c = redfun env sigma c in let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) in - (* FIXME: use local flag *) - let reorder = if reorder then AnyHypConv else StableHypConv in e_change_in_hyps ~check ~reorder f hyps end end -- cgit v1.2.3