From f6f02c26e6907bc2dca8da62abbb4f5c3e783fd8 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 15 Jul 2026 16:50:57 +0200 Subject: [PATCH] Make proof-local simplify hint databases visible to conversion The named/local hint-database mechanism records the set of active databases per goal (g_simpl), but several tactics consulted user reduction rules through static reduction_info values (full_compat / full_red with an empty user_local), so rules activated with `hint +db.` were invisible to them. With this, `hint simplify in db : ...` + a proof-local `hint +db.` behaves exactly like the former global default-database hints. --- src/ecCoreGoal.ml | 2 ++ src/ecCoreGoal.mli | 1 + src/ecHiGoal.ml | 8 +++++--- src/ecLowGoal.ml | 27 +++++++++++++++++++++++---- src/ecMatching.ml | 8 ++++---- src/ecMatching.mli | 6 ++++-- src/ecProofTerm.ml | 33 ++++++++++++++++++++------------- src/ecProofTerm.mli | 5 +++-- 8 files changed, 62 insertions(+), 28 deletions(-) diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index d1cdd85c3..728824b4d 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -420,6 +420,8 @@ module FApi = struct let tc_goal (tc : tcenv) = tc1_goal tc.tce_tcenv let tc_env (tc : tcenv) = tc1_env tc.tce_tcenv + let tc_simplify_context (tc : tcenv) = tc1_simplify_context tc.tce_tcenv + let tc_flat ?target (tc : tcenv) = tc1_flat ?target tc.tce_tcenv let tc_eflat ?target (tc : tcenv) = tc1_eflat ?target tc.tce_tcenv let tc_hyps ?target (tc : tcenv) = tc1_hyps ?target tc.tce_tcenv diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index fdaf7d277..2f1b51740 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -315,6 +315,7 @@ module FApi : sig val tc_flat : ?target:ident -> tcenv -> LDecl.hyps * form val tc_eflat : ?target:ident -> tcenv -> env * LDecl.hyps * form val tc_hyps : ?target:ident -> tcenv -> LDecl.hyps + val tc_simplify_context : tcenv -> EcEnv.simplify_context (* Accessors for focused goal parts (tcenv1) *) val tc1_handle : tcenv1 -> handle diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index b55e9bf2c..e9e011c66 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -986,15 +986,17 @@ let process_rewrite1_r ttenv ?target ri tc = let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in let hyps = FApi.tc1_hyps ?target tc in + let simpl = FApi.tc1_simplify_context tc in + let ptenv, prw = match rwopt.match_ with | None -> - PT.ptenv_of_penv hyps !!tc, None + PT.ptenv_of_penv ~simpl hyps !!tc, None | Some (RWM_Plain p) -> let (ps, ue), p = TTC.tc1_process_pattern tc p in let ev = MEV.of_idents (Mid.keys ps) `Form in - (PT.ptenv !!tc hyps (ue, ev), Some (p, None)) + (PT.ptenv ~simpl !!tc hyps (ue, ev), Some (p, None)) | Some (RWM_Context (x, p)) -> let ps = ref Mid.empty in @@ -1005,7 +1007,7 @@ let process_rewrite1_r ttenv ?target ri tc = let hyps = LDecl.add_local x (LD_var (xty, None)) hyps in let p = EcTyping.trans_pattern (LDecl.toenv hyps) ps ue p in let ev = MEV.of_idents (x :: Mid.keys !ps) `Form in - (PT.ptenv !!tc hyps (ue, ev), Some (p, Some (x, xty))) in + (PT.ptenv ~simpl !!tc hyps (ue, ev), Some (p, Some (x, xty))) in let theside = match rwopt.side, subs with diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 6117f7bcb..e649bc45a 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -387,6 +387,9 @@ let t_cbv_with_info ?target (ri : reduction_info) (tc : tcenv1) = let t_cbv ?target ?(delta = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) = let ri = { nodelta with delta_p = fun _ -> delta } in let ri = { ri with logic } in + (* thread the proof-local simplify overlay (hint +db, local rules) so + that tactics built on [t_cbv] (done, progress, ...) see it *) + let ri = { ri with user_local = FApi.tc1_simplify_context tc } in t_cbv_with_info ?target ri tc (* -------------------------------------------------------------------- *) @@ -398,6 +401,9 @@ let t_cbn_with_info ?target (ri : reduction_info) (tc : tcenv1) = let t_cbn ?target ?(delta = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) = let ri = { nodelta with delta_p = fun _ -> delta } in let ri = { ri with logic } in + (* thread the proof-local simplify overlay (hint +db, local rules) so + that tactics built on [t_cbn] (done, progress, ...) see it *) + let ri = { ri with user_local = FApi.tc1_simplify_context tc } in t_cbn_with_info ?target ri tc (* -------------------------------------------------------------------- *) @@ -676,7 +682,12 @@ let tt_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv) = let tc, (pt, ax, subgoals) = RApi.to_pure (fun tc -> LowApply.check_with_cutsolve `Elim pt (`Tc (tc, None))) tc in - if not (EcReduction.is_conv hyps ax concl) then begin + (* conversion sees the proof-local simplify context (hint +db) *) + let conv_ri = + { EcReduction.full_red with + EcReduction.user_local = FApi.tc_simplify_context tc } in + + if not (EcReduction.is_conv ~ri:conv_ri hyps ax concl) then begin (* let env = FApi.tc_env tc in let ppe = EcPrinting.PPEnv.ofenv env in @@ -757,7 +768,11 @@ module Apply = struct exception NoInstance of (bool * reason * PT.pt_env * (form * form)) - let t_apply_bwd_r ?(ri = EcReduction.full_compat) ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) = + let t_apply_bwd_r ?ri ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) = + (* by default, conversion sees the proof-local simplify context *) + let ri = ri |> odfl + { EcReduction.full_compat with + EcReduction.user_local = pt.PT.ptev_env.PT.pte_lc } in let ((hyps, concl), pterr) = (FApi.tc1_flat tc, PT.copy pt.ptev_env) in let noinstance ?(dpe = false) reason = @@ -834,7 +849,7 @@ module Apply = struct let t_apply_bwd ?(ri : EcReduction.reduction_info option) ?mode ?canview pt (tc : tcenv1) = let hyps = FApi.tc1_hyps tc in let pt, ax = LowApply.check `Elim pt (`Hyps (hyps, !!tc)) in - let ptenv = ptenv_of_penv hyps !!tc in + let ptenv = ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps !!tc in let pt = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = ax; } in t_apply_bwd_r ?ri ?mode ?canview pt tc @@ -1728,6 +1743,10 @@ let t_rewrite ?xconv ?keyed ?target ?(mode : rwmode option) ?(donot=false) (pt : proofterm) (s, pos) (tc : tcenv1) = + (* conversion checks below see the proof-local simplify context *) + let conv_ri = + { EcReduction.full_compat with + EcReduction.user_local = FApi.tc1_simplify_context tc } in let tc = RApi.rtcenv_of_tcenv1 tc in let (hyps, tgfp) = RApi.tc_flat ?target tc in let env = LDecl.toenv hyps in @@ -1763,7 +1782,7 @@ let t_rewrite in let change f = - if not (EcReduction.is_conv hyps f left) then + if not (EcReduction.is_conv ~ri:conv_ri hyps f left) then raise InvalidGoalShape; right in diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 29a4617cb..db71dbf4d 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -880,7 +880,7 @@ let fmnotation = { (* -------------------------------------------------------------------- *) (* Rigid unification *) -let f_match_core opts hyps (ue, ev) f1 f2 = +let f_match_core ?(conv_ri = EcReduction.full_compat) opts hyps (ue, ev) f1 f2 = let ue = EcUnify.UniEnv.copy ue in let ev = ref ev in @@ -891,7 +891,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 = let conv = match opts.fm_conv with - | true -> EcReduction.is_conv ~ri:EcReduction.full_compat hyps + | true -> EcReduction.is_conv ~ri:conv_ri hyps | false -> EcReduction.is_alpha_eq hyps in @@ -1286,8 +1286,8 @@ let f_match_core opts hyps (ue, ev) f1 f2 = doit (EcEnv.LDecl.toenv hyps) (Fsubst.f_subst_id, Mid.empty) f1 f2; (ue, !ev) -let f_match opts hyps (ue, ev) f1 f2 = - let (ue, ev) = f_match_core opts hyps (ue, ev) f1 f2 in +let f_match ?conv_ri opts hyps (ue, ev) f1 f2 = + let (ue, ev) = f_match_core ?conv_ri opts hyps (ue, ev) f1 f2 in if not (MEV.filled ev) then raise MatchFailure; let clue = diff --git a/src/ecMatching.mli b/src/ecMatching.mli index d13622e4d..e4ee9d882 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -371,7 +371,8 @@ val fmdelta : fmoptions val fmnotation : fmoptions val f_match_core : - fmoptions + ?conv_ri:EcReduction.reduction_info + -> fmoptions -> EcEnv.LDecl.hyps -> unienv * mevmap -> form @@ -379,7 +380,8 @@ val f_match_core : -> unienv * mevmap val f_match : - fmoptions + ?conv_ri:EcReduction.reduction_info + -> fmoptions -> EcEnv.LDecl.hyps -> unienv * mevmap -> form diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index 4235c079a..5a5dce7a4 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -19,6 +19,7 @@ type pt_env = { pte_hy : LDecl.hyps; pte_ue : EcUnify.unienv; pte_ev : EcMatching.mevmap ref; + pte_lc : EcEnv.simplify_context; (* proof-local simplify context *) } type pt_ev = { @@ -78,22 +79,24 @@ let argkind_of_ptarg arg : argkind = | PVASub _ -> `PTerm (* -------------------------------------------------------------------- *) -let ptenv pe hyps (ue, ev) = +let ptenv ?(simpl = EcEnv.SimplifyContext.empty) pe hyps (ue, ev) = { pte_pe = pe; pte_hy = hyps; pte_ue = EcUnify.UniEnv.copy ue; - pte_ev = ref ev; } + pte_ev = ref ev; + pte_lc = simpl; } (* -------------------------------------------------------------------- *) let copy pe = - ptenv pe.pte_pe pe.pte_hy (pe.pte_ue, !(pe.pte_ev)) + ptenv ~simpl:pe.pte_lc pe.pte_pe pe.pte_hy (pe.pte_ue, !(pe.pte_ev)) (* -------------------------------------------------------------------- *) -let ptenv_of_penv (hyps : LDecl.hyps) (pe : proofenv) = +let ptenv_of_penv ?(simpl = EcEnv.SimplifyContext.empty) (hyps : LDecl.hyps) (pe : proofenv) = { pte_pe = pe; pte_hy = hyps; pte_ue = PT.unienv_of_hyps hyps; - pte_ev = ref EcMatching.MEV.empty; } + pte_ev = ref EcMatching.MEV.empty; + pte_lc = simpl; } (* -------------------------------------------------------------------- *) let rec get_head_symbol (pt : pt_env) (f : form) = @@ -272,9 +275,13 @@ let pattern_form ?name hyps ~ptn subject = let pf_form_match (pt : pt_env) ?mode ~ptn subject = let mode = mode |> odfl EcMatching.fmrigid in + (* conversion during matching sees the proof-local simplify context *) + let conv_ri = + { EcReduction.full_compat with EcReduction.user_local = pt.pte_lc } in + try let (ue, ev) = - EcMatching.f_match_core mode pt.pte_hy + EcMatching.f_match_core ~conv_ri mode pt.pte_hy (pt.pte_ue, !(pt.pte_ev)) ptn subject in EcUnify.UniEnv.restore ~dst:pt.pte_ue ~src:ue; @@ -282,7 +289,7 @@ let pf_form_match (pt : pt_env) ?mode ~ptn subject = with EcMatching.MatchFailure as exn -> (* FIXME: should we check for empty inters. with ecmap? *) if not mode.fm_conv || - not (EcReduction.is_conv ~ri:EcReduction.full_compat pt.pte_hy ptn subject) then + not (EcReduction.is_conv ~ri:conv_ri pt.pte_hy ptn subject) then raise exn (* -------------------------------------------------------------------- *) @@ -883,37 +890,37 @@ let process_full_closed_pterm pe pf = let tc1_process_pterm_cut ~prcut tc ff = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff + process_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) let tc1_process_pterm tc ff = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_pterm (ptenv_of_penv hyps pe) ff + process_pterm (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) let tc1_process_full_pterm_cut ~prcut (tc : tcenv1) (ff : 'a gppterm) = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_full_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff + process_full_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) let tc1_process_full_pterm ?implicits (tc : tcenv1) (ff : ppterm) = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_full_pterm ?implicits (ptenv_of_penv hyps pe) ff + process_full_pterm ?implicits (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) let tc1_process_full_closed_pterm_cut ~prcut (tc : tcenv1) (ff : 'a gppterm) = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_full_closed_pterm_cut ~prcut (ptenv_of_penv hyps pe) ff + process_full_closed_pterm_cut ~prcut (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) let tc1_process_full_closed_pterm (tc : tcenv1) (ff : ppterm) = let pe = FApi.tc1_penv tc in let hyps = FApi.tc1_hyps tc in - process_full_closed_pterm (ptenv_of_penv hyps pe) ff + process_full_closed_pterm (ptenv_of_penv ~simpl:(FApi.tc1_simplify_context tc) hyps pe) ff (* -------------------------------------------------------------------- *) type prept = [ diff --git a/src/ecProofTerm.mli b/src/ecProofTerm.mli index af3d0509f..bb4aaf6a4 100644 --- a/src/ecProofTerm.mli +++ b/src/ecProofTerm.mli @@ -35,6 +35,7 @@ type pt_env = { pte_hy : LDecl.hyps; (* local context *) pte_ue : EcUnify.unienv; (* unification env. *) pte_ev : mevmap ref; (* metavar env. *) + pte_lc : EcEnv.simplify_context; (* proof-local simplify context *) } type pt_ev = { @@ -148,9 +149,9 @@ val concretize_e_form_gen : cptenv -> bindings -> form -> form val concretize_e_arg : cptenv -> pt_arg -> pt_arg (* PTEnv constructor *) -val ptenv_of_penv : LDecl.hyps -> proofenv -> pt_env +val ptenv_of_penv : ?simpl:EcEnv.simplify_context -> LDecl.hyps -> proofenv -> pt_env -val ptenv : proofenv -> LDecl.hyps -> (EcUnify.unienv * mevmap) -> pt_env +val ptenv : ?simpl:EcEnv.simplify_context -> proofenv -> LDecl.hyps -> (EcUnify.unienv * mevmap) -> pt_env val copy : pt_env -> pt_env (* Proof-terms construction from components *)