From 6ff8dbc29581bf709991b6e4264d0b91d6d0ba3d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 8 Mar 2026 05:56:02 +0100 Subject: [PATCH] [refold]: allow rigid unification Syntax: `rewrite -/~(pattern)` --- src/ecHiGoal.ml | 42 +++++++++++++++++++++++------------------- src/ecHiGoal.mli | 2 +- src/ecParser.mly | 4 ++-- src/ecParsetree.ml | 2 +- 4 files changed, 27 insertions(+), 23 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index d34ba4aa76..f2b67436a9 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -598,9 +598,10 @@ let process_rewrite1_core ?mode ?(close = true) ?target (s, p, o) pt tc = tc_error !!tc "r-pattern does not match the rewriting rule" (* -------------------------------------------------------------------- *) -let process_delta ~und_delta ?target (s, o, p) tc = +let process_delta ~und_delta ?(rigid = false) ?target (s, o, p) tc = let env, hyps, concl = FApi.tc1_eflat tc in let o = norm_rwocc o in + let occmode = if rigid then Some om_rigid else None in let idtg, target = match target with @@ -668,7 +669,7 @@ let process_delta ~und_delta ?target (s, o, p) tc = match s with | `LtoR -> begin let matches = - try ignore (PT.pf_find_occurence ptenv ~ptn:p target); true + try ignore (PT.pf_find_occurence ptenv ?occmode ~ptn:p target); true with PT.FindOccFailure _ -> false in @@ -729,23 +730,26 @@ let process_delta ~und_delta ?target (s, o, p) tc = with EcEnv.NotReducible -> fp in - let matches = - try ignore (PT.pf_find_occurence ptenv ~ptn:fp target); true - with PT.FindOccFailure _ -> false - in + begin + match PT.pf_find_occurence ?occmode ptenv ~ptn:fp target with + | (_, occmode) -> + let p = concretize_form ptenv p in + let fp = concretize_form ptenv fp in + let cpos = + try + FPosition.select_form + ?xconv:(if rigid then Some `AlphaEq else None) + ?keyed:(if rigid then Some occmode.k_keyed else None) + hyps o fp target + with InvalidOccurence -> + tc_error !!tc "invalid occurences selector" in - if matches then begin - let p = concretize_form ptenv p in - let fp = concretize_form ptenv fp in - let cpos = - try FPosition.select_form hyps o fp target - with InvalidOccurence -> - tc_error !!tc "invalid occurences selector" - in + let target = FPosition.map cpos (fun _ -> p) target in + t_change ~ri ?target:idtg target tc - let target = FPosition.map cpos (fun _ -> p) target in - t_change ~ri ?target:idtg target tc - end else t_id tc + | exception (PT.FindOccFailure _) -> + t_id tc + end (* -------------------------------------------------------------------- *) let process_rewrite1_r ttenv ?target ri tc = @@ -768,11 +772,11 @@ let process_rewrite1_r ttenv ?target ri tc = let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc - | RWDelta ((s, r, o, px), p) -> begin + | RWDelta (rigid, (s, r, o, px), p) -> begin if Option.is_some px then tc_error !!tc "cannot use pattern selection in delta-rewrite rules"; - let do1 tc = process_delta ~und_delta ?target (s, o, p) tc in + let do1 tc = process_delta ~und_delta ~rigid ?target (s, o, p) tc in match r with | None -> do1 tc diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 317163fd6e..ff18b1f8c9 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -75,7 +75,7 @@ val process_clear : clear_info -> backward val process_smt : ?loc:EcLocation.t -> ttenv -> pprover_infos option -> backward val process_coq : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward val process_apply : implicits:bool -> apply_t * prevert option -> backward -val process_delta : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward +val process_delta : und_delta:bool -> ?rigid:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward val process_rewrite : ttenv -> ?target:psymbol -> rwarg list -> backward val process_subst : pformula list -> backward val process_cut : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward diff --git a/src/ecParser.mly b/src/ecParser.mly index 7147db3321..4e52c56f82 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2389,8 +2389,8 @@ rwarg1: | s=rwside r=rwrepeat? o=rwocc? p=bracket(form_h)? fp=rwpterms { RWRw ((s, r, o, p), fp) } -| s=rwside r=rwrepeat? o=rwocc? SLASH x=sform_h %prec prec_tactic - { RWDelta ((s, r, o, None), x); } +| s=rwside r=rwrepeat? o=rwocc? SLASH rigid=iboption(TILD) x=sform_h %prec prec_tactic + { RWDelta (rigid, (s, r, o, None), x); } | PR s=bracket(rwpr_arg) { RWPr s } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index bcb6342d56..54eaecf696 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -860,7 +860,7 @@ type rwarg = (tfocus located) option * rwarg1 located and rwarg1 = | RWSimpl of [`Default | `Variant] - | RWDelta of (rwoptions * pformula) + | RWDelta of (bool * rwoptions * pformula) | RWRw of (rwoptions * (rwside * ppterm) list) | RWPr of (psymbol * pformula option) | RWDone of [`Default | `Variant] option