From d01e8ecd82ea18cf7b78b8be6a1ac5dedf78c892 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jun 2025 23:38:08 +0200 Subject: [PATCH 1/3] ssr: skip impargs in pattern FO unif --- plugins/ssrmatching/ssrmatching.ml | 144 +++++++++++++++++++++++++++-- test-suite/ssr/rew_FO.v | 46 +++++++++ 2 files changed, 180 insertions(+), 10 deletions(-) create mode 100644 test-suite/ssr/rew_FO.v diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index d69115ea48fb..b540282e91ee 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -55,6 +55,11 @@ let _ = optread = (fun _ -> !pp_ref == ssr_pp); optwrite = debug } let pp s = !pp_ref s +let { Goptions.get = option_LegacyFoUnif } = + Goptions.declare_bool_option_and_ref ~key:["SsrMatching";"LegacyFoUnif"] + ~depr:{Deprecation.since=Some "9.2"; + note=Some "Use this flag only to port scripts from 9.1 to 9.2, do not leave it in final scripts." } + ~value:false () (** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) @@ -214,11 +219,117 @@ let flags_FO env = Unification.resolve_evars = (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars } +let legacy_unif_FO env ise metas p c = + let _ : _ * Evd.evar_map = Unification.w_unify ~metas env ise Conversion.CONV ~flags:(flags_FO env) p c in + () + +type hd_comparison = + | CompareArgs of evar_map * Unification.Meta.t * Impargs.implicit_status list + | CanonicalInfRequired + | CanonicalRedRequired of Evd.evar_map * EConstr.t * int + | Different + +let implicits_for_rewrite_of gr = + Impargs.implicits_of_global gr |> List.last |> snd + + let failure_FO () = raise (CErrors.user_err Pp.(mt ())) + +let rec same_hd env ise metas p c = + match EConstr.kind ise p, EConstr.kind ise c with + | Const(c1,_), Const(c2,_) when Constant.CanOrd.equal c1 c2 -> + CompareArgs (ise,metas,implicits_for_rewrite_of (GlobRef.ConstRef c1)) + | Ind(c1,_), Ind(c2,_) when Ind.CanOrd.equal c1 c2 -> + CompareArgs (ise,metas,implicits_for_rewrite_of (GlobRef.IndRef c1)) + | Construct(c1,_), Construct(c2,_) when Construct.CanOrd.equal c1 c2 -> + CompareArgs (ise,metas,implicits_for_rewrite_of (GlobRef.ConstructRef c1)) + | Const(c1,_), _ when Structures.Structure.is_projection c1 -> CanonicalInfRequired + | _, Const(c2,i) when Structures.Structure.is_projection c2 -> + let b = Environ.constant_value_in env (c2,EConstr.EInstance.kind ise i) in + CanonicalRedRequired (ise, EConstr.of_constr b, Structures.Structure.projection_nparams c2) + | Rel c1,Rel c2 when c1 == c2 -> CompareArgs (ise,metas,[]) + | Var c1,Var c2 when Id.equal c1 c2 -> + CompareArgs (ise,metas,implicits_for_rewrite_of (GlobRef.VarRef c1)) + | Proj(p1,_,x), Proj(p2,_,y) when Environ.QProjection.equal env p1 p2 -> + let metas, ise = unif_FO_skip_impl env ise metas x y in + CompareArgs (ise,metas,[]) + | _ -> Different +and unif_FO_skip_impl env ise metas p c = + match EConstr.kind ise p, EConstr.kind ise c with + | Meta i, _ when Unification.Meta.meta_opt_fvalue metas i = None -> + let ise,metas = Unification.Meta.meta_assign i (c,TypeNotProcessed) metas ise in metas, ise + | Meta i, _ -> + begin match Unification.Meta.meta_opt_fvalue metas i with + | None -> assert false + | Some { Unification.rebus = p } -> unif_FO_skip_impl env ise metas p c + end + (* | App(hd,args1), _ when EConstr.isMeta ise hd -> metas, ise *) + (* | App(hd,args1), App(f,args2) when EConstr.isMeta ise hd -> + if Array.length args1 > Array.length args2 then failure_FO (); + let args2, rest = CArray.chop (Array.length args2 - Array.length args1) args2 in + let rhs = EConstr.mkApp (f,args2) in + pp(lazy(str "HO-FO" ++ pr_econstr_env env ise hd ++ str " = " ++ pr_econstr_env env ise rhs)); + let metas, ise = unif_FO_skip_impl env ise metas hd rhs in + unif_FO_skip_impl3 env ise metas (Array.to_list args1) (Array.to_list rest) [] *) + | Proj(p1,_,x), Proj(p2,_,y) when Environ.QProjection.equal env p1 p2 -> + unif_FO_skip_impl3 env ise metas [x] [y] [] + | App(hd1,args1), App(hd2,args2) when not @@ EConstr.isMeta ise hd1 -> + begin match same_hd env ise metas hd1 hd2 with + | CanonicalRedRequired(ise,proj,narg) when Array.length args2 > narg -> + pp(lazy(str "Red in " ++ pr_econstr_env env ise c)); + let c' = + let open Reductionops in + let metas = { meta_value = (fun i -> + Option.map (fun x -> x.Unification.rebus) + (Unification.Meta.meta_opt_fvalue metas i)) } in + Stack.zip ise @@ + whd_betaiota_deltazeta_for_iota_state + TransparentState.full env ise ~metas + (EConstr.mkApp (proj,args2),Stack.empty) in + pp(lazy(str "Red out " ++ pr_econstr_env env ise c')); + if EConstr.eq_constr ise c c' then failure_FO () + else unif_FO_skip_impl env ise metas p c' + | CanonicalInfRequired -> + pp(lazy(str "Skip")); + metas, ise + | CompareArgs(ise,metas,imp) -> + pp(lazy(str "Rec")); + unif_FO_skip_impl3 env ise metas (Array.to_list args1) (Array.to_list args2) imp + | _ -> + pp(lazy(str "Fail")); + failure_FO () + end + | _ -> + let kludge v = EConstr.mkLambda (make_annot Anonymous EConstr.ERelevance.relevant, EConstr.mkProp, v) in + Unification.w_unify ~metas env ise Conversion.CONV ~flags:(flags_FO env) (kludge p) (kludge c) +and unif_FO_skip_impl3 env ise metas args1 args2 imp = + match args1, args2, imp with + | a1::args1, a2::args2, Some _ :: imp -> + pp(lazy(str"skip impl " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2)); + unif_FO_skip_impl3 env ise metas args1 args2 imp + | a1::args1, a2::args2, None :: imp -> + pp(lazy(str"do " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2)); + let metas, ise = unif_FO_skip_impl env ise metas a1 a2 in + unif_FO_skip_impl3 env ise metas args1 args2 imp + | a1::args1, a2::args2, [] -> + pp(lazy(str"do " ++ pr_econstr_env env ise a1 ++ str " = " ++ pr_econstr_env env ise a2)); + let metas, ise = unif_FO_skip_impl env ise metas a1 a2 in + unif_FO_skip_impl3 env ise metas args1 args2 [] + | [], [], _ -> + pp(lazy(str"good")); + metas, ise + | _ -> + pp(lazy(str"bad")); + failure_FO () + +let new_unif_FO env ise metas p c = + pp(lazy(str"NEW FO " ++ pr_econstr_env env ise p ++ str " = " ++ pr_econstr_env env ise c)); + let _ : _ * Evd.evar_map = unif_FO_skip_impl env ise metas p c in + () let unif_FO env ise metas p c = let metas = Unification.Metamap.fold (fun mv t accu -> Unification.Meta.meta_declare mv t accu) metas Unification.Meta.empty in - let _ : _ * Evd.evar_map = Unification.w_unify ~metas env ise Conversion.CONV ~flags:(flags_FO env) p c in - () + if option_LegacyFoUnif () then legacy_unif_FO env ise metas p c + else new_unif_FO env ise metas p c (* Perform evar substitution in main term and prune substitution. *) let nf_open_term sigma0 ise c = @@ -559,14 +670,25 @@ let match_upats_FO upats env sigma0 ise orig_c = unif_FO env ise metas p_FO c' in let ise' = (* Unify again using HO to assign evars *) - let p = mkApp (u.up_f, u.up_a) in - try unif_HO env ise p c' with e when CErrors.noncritical e -> raise NoMatch in + if u.up_k = KpatConst then + try + let ise = unif_HO env ise u.up_f f in + unif_HO_args env ise u.up_a (i - Array.length u.up_a) a + with e when CErrors.noncritical e -> raise NoMatch + else + let p = mkApp (u.up_f, u.up_a) in + try unif_HO env ise p c' + with e when CErrors.noncritical e -> raise NoMatch in let lhs = mkSubApp f i a in let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in - raise (FoundUnif (ungen_upat lhs pt' u)) + if option_LegacyFoUnif () || Evar.Set.equal + (Evd.evars_of_term ise' (mkApp (u.up_f, u.up_a))) + (Evd.evars_of_term ise' lhs) + then raise (FoundUnif (ungen_upat lhs pt' u)) + else (pp(lazy(str "not ground" ++ pr_econstr_pat env ise' (mkApp (u.up_f, u.up_a))));raise NoMatch) with FoundUnif (_, s,_,_) as sig_u when dont_impact_evars s -> raise sig_u | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO.") - | e when CErrors.noncritical e -> () in + | e when CErrors.noncritical e -> pp(lazy(str"FO fail: " ++ CErrors.print_no_report e)); () in List.iter one_match fpats done; iter_constr_LR ise loop f; Array.iter loop a in @@ -617,6 +739,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let tfa = Retyping.get_type_of ~lax:true env ise fa in unif_HO env ise tuf tfa | _ -> ise in + pp(lazy(str"FLEX " ++ pr_econstr_env env ise u.up_f ++ str" = " ++ pr_econstr_env env ise fa)); unif_HO env ise u.up_f fa | _ -> unif_HO env ise u.up_f f in let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in @@ -769,14 +892,14 @@ let has_instances = function | None -> false | Some instances -> not (List.is_empty !instances) -let find_tpattern ~raise_NoMatch ~instances ~upat_that_matched ~upats_origin ~upats sigma0 ise occ_state : find_P = +let find_tpattern ~disable_FO ~raise_NoMatch ~instances ~upat_that_matched ~upats_origin ~upats sigma0 ise occ_state : find_P = fun env c h ~k -> do_once upat_that_matched (fun () -> let failed_because_of_TC = ref false in try let () = match instances with - | None -> match_upats_FO upats env sigma0 ise c - | Some _ -> () + | None when not disable_FO -> match_upats_FO upats env sigma0 ise c + | _ -> () in let on_instance = match instances with | None -> fun x -> raise (FoundUnif x) @@ -841,7 +964,8 @@ let mk_tpattern_matcher ?(all_instances=false) let occ_state = create_occ_state occ in let upat_that_matched = ref None in let instances = if all_instances then Some (ref []) else None in - find_tpattern ~raise_NoMatch ~instances ~upat_that_matched ~upats_origin ~upats sigma0 ise occ_state, + let disable_FO = occ = Some(true,[1]) in + find_tpattern ~disable_FO ~raise_NoMatch ~instances ~upat_that_matched ~upats_origin ~upats sigma0 ise occ_state, conclude_tpattern ~raise_NoMatch ~upat_that_matched ~upats_origin ~upats occ_state type ('ident, 'term) ssrpattern = diff --git a/test-suite/ssr/rew_FO.v b/test-suite/ssr/rew_FO.v new file mode 100644 index 000000000000..7dc543bb9521 --- /dev/null +++ b/test-suite/ssr/rew_FO.v @@ -0,0 +1,46 @@ +From Corelib Require Import ssreflect. + +Axiom R : Type. +Axiom op : nat -> R -> R -> R. + +Axiom lemma : forall n x y z, op n (op n x y) z = z. + +Arguments op {_} _ _. + +Goal forall a b c : R, @op (0+1) (@op 1 a b) c = + @op 2 (@op 2 a b) c. +intros a b c. +Show. +rewrite lemma. +Show. +match goal with +| |- c = _ => idtac "ok" +end. +Abort. + +Record foo := F { f : nat }. + +Definition c := F (1 + 2). + +Goal (forall x, 1 + (1 + x) = 5) -> 1 + f c = 1 + (1 + 7) . +Show. +move->. +Show. +match goal with |- 5 = 1 + (1 + 7) => idtac "ok" end. +Abort. + +Goal (forall x, 1 + (1 + x) = 5) -> 1 + f c = 1 + (1 + 7) . +Show. +Set SsrMatching LegacyFoUnif. +move->. +Unset SsrMatching LegacyFoUnif. +Show. +match goal with |- 1 + f c = 5 => idtac "ok" end. +Abort. + +Goal (forall x, 1 + (S x) = 5) -> 1 + f c = 1 + (1 + 7) . +Show. +move->. +Show. +match goal with |- 1 + f c = 1 + 5 => idtac "ok" end. +Abort. From 4f322d53ad1349898e049f10ca72c541c5b2ef81 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Jun 2025 21:10:13 +0200 Subject: [PATCH 2/3] changelog --- .../20707-ssrpat-FO-ignore-imparg-Changed.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 doc/changelog/07-ssreflect/20707-ssrpat-FO-ignore-imparg-Changed.rst diff --git a/doc/changelog/07-ssreflect/20707-ssrpat-FO-ignore-imparg-Changed.rst b/doc/changelog/07-ssreflect/20707-ssrpat-FO-ignore-imparg-Changed.rst new file mode 100644 index 000000000000..904b62f02288 --- /dev/null +++ b/doc/changelog/07-ssreflect/20707-ssrpat-FO-ignore-imparg-Changed.rst @@ -0,0 +1,10 @@ +- **Changed:** + rewrite pattern selection algorithm made more robust in face of changes + to implicit arguments shape. This changes can result in a different + pattern selection in some corner cases. + The option `Set SsrMatching LegacyFoUnif` can be used to obtain the + previous behavior when repairing scripts + (`#20707 `_, + fixes `#16763 `_, + by Enrico Tassi with help from Georges Gonthier, Pierre Roux and + Quentin Vermande). From 73716635d72917a4ded68e4415519c08ee6a2df4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 28 Jun 2025 12:18:18 +0200 Subject: [PATCH 3/3] [CI] Overlays --- dev/ci/user-overlays/20707-gares-sspart-FO-ignore-imparg.sh | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 dev/ci/user-overlays/20707-gares-sspart-FO-ignore-imparg.sh diff --git a/dev/ci/user-overlays/20707-gares-sspart-FO-ignore-imparg.sh b/dev/ci/user-overlays/20707-gares-sspart-FO-ignore-imparg.sh new file mode 100644 index 000000000000..0cd0e42d7674 --- /dev/null +++ b/dev/ci/user-overlays/20707-gares-sspart-FO-ignore-imparg.sh @@ -0,0 +1,2 @@ +overlay coquelicot https://gitlab.inria.fr/qvermand/coquelicot ssrpat-FO-ignore-imparg 20707 +overlay perennial https://github.com/proux01/perennial ssrpat-FO-ignore-imparg 20707