From 5ad8256ed5043f4e79cf0be59a364043749352a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 19 Aug 2026 14:38:15 +0200 Subject: [PATCH] Proof of concept "noopaques" flag makes reduction fail if it encounters an opaque TODO: - don't ignore the flag for non-lazy reductions (ie implement for non-lazy reductions) - improve error printing - decide if evars count as opaques Close #3296 --- doc/sphinx/proofs/writing-proofs/equality.rst | 1 + doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + kernel/cClosure.ml | 26 +++++++- kernel/cClosure.mli | 2 + kernel/redFlags.ml | 15 ++--- kernel/redFlags.mli | 1 + plugins/funind/recdef.ml | 12 ++-- plugins/ltac2/tac2quote.ml | 3 +- plugins/ltac2/tac2stdlib.ml | 1 + plugins/ssr/ssrcommon.ml | 3 +- tactics/genredexpr.mli | 4 +- tactics/redexpr.ml | 1 + tactics/redops.ml | 63 ++++++++++--------- test-suite/success/noopaques.v | 17 +++++ vernac/g_redexpr.mlg | 1 + 16 files changed, 104 insertions(+), 48 deletions(-) create mode 100644 test-suite/success/noopaques.v diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst index 5d9e94b20ff4..b944701a552c 100644 --- a/doc/sphinx/proofs/writing-proofs/equality.rst +++ b/doc/sphinx/proofs/writing-proofs/equality.rst @@ -488,6 +488,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: reductions ::= {+ @reduction } | {? head } @delta_reductions reduction ::= head + | noopaques | beta | delta {? @delta_reductions } | match diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a8310f63de8c..72f82518d6e8 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -799,6 +799,7 @@ red_flag: [ | "zeta" | "delta" delta_flag | "head" +| "noopaques" ] delta_flag: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a88d50b82330..b6616bfea3ee 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -530,6 +530,7 @@ reductions: [ reduction: [ | "head" +| "noopaques" | "beta" | "delta" OPT delta_reductions | "match" diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 80e6500c442a..6a17bbfb625b 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1978,6 +1978,21 @@ end type 'a depth = 'a RedPattern.depth +exception EncounteredOpaque of Environ.env * table_key + +let encountered_opaque_printer = ref (fun _ -> function + | ConstKey (c, _) -> Constant.print c + | VarKey id -> Id.print id + | RelKey n -> Pp.(str "UNBOUND_REL_" ++ int n)) + +let () = CErrors.register_handler @@ function + | EncounteredOpaque (env, k) -> + Some Pp.(str "Encountered opaque " ++ !encountered_opaque_printer env k ++ + str " in lazy with noopaques flag.") + | _ -> None + +let set_encountered_opaque_printer f = encountered_opaque_printer := f + (* Computes a weak head normal form from the result of knh. *) let rec knr info tab ~pat_state m stk = match m.term with @@ -1998,7 +2013,11 @@ let rec knr info tab ~pat_state m stk = knr_ret info tab ~pat_state (m, stk) | Symbol (u, b, r) -> RedPattern.match_symbol knred info tab ~pat_state fl (u, b, r) stk - | Undef _ | OpaqueDef _ -> (set_ntrl m; knr_ret info tab ~pat_state (m,stk))) + | Undef _ | OpaqueDef _ -> + let () = if red_set info.i_flags fNoOpaques then + raise (EncounteredOpaque (info_env info, fl)) + in + (set_ntrl m; knr_ret info tab ~pat_state (m,stk))) | FConstruct (c, args) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in @@ -2066,6 +2085,11 @@ let rec knr info tab ~pat_state m stk = | FIrrelevant -> let stk = skip_irrelevant_stack info stk in knr_ret info tab ~pat_state (m, stk) + | FFlex fl when red_set info.i_flags fNoOpaques -> raise (EncounteredOpaque (info_env info, fl)) + | FRel n when red_set info.i_flags fNoOpaques -> + (* XXX RelKey is incorrect? the env if the outer env? *) + raise (EncounteredOpaque (info_env info, RelKey n)) + (* XXX also reject FEvar when noopaques? *) | FProd _ | FAtom _ | FInd _ (* relevant statically *) | FCaseInvert _ | FProj _ | FFix _ | FEvar _ (* relevant because of knh(t) *) | FLambda _ | FFlex _ | FRel _ (* irrelevance handled by conversion *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index a384d9bcb054..8839d8af4637 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -213,3 +213,5 @@ val get_ref_mask : clos_infos -> clos_tab -> table_key -> bool array (** Hook for Reduction *) val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit + +val set_encountered_opaque_printer : (Environ.env -> table_key -> Pp.t) -> unit diff --git a/kernel/redFlags.ml b/kernel/redFlags.ml index 42d07e8c3dac..72cf022e81ac 100644 --- a/kernel/redFlags.ml +++ b/kernel/redFlags.ml @@ -19,12 +19,13 @@ type red_kind = | PROJ of Projection.Repr.t | VAR of Id.t -let fBETA = FLAG 0b000001 -let fDELTA = FLAG 0b000010 -let fMATCH = FLAG 0b000100 -let fFIX = FLAG 0b001000 -let fCOFIX = FLAG 0b010000 -let fZETA = FLAG 0b100000 +let fBETA = FLAG 0b0000001 +let fDELTA = FLAG 0b0000010 +let fMATCH = FLAG 0b0000100 +let fFIX = FLAG 0b0001000 +let fCOFIX = FLAG 0b0010000 +let fZETA = FLAG 0b0100000 +let fNoOpaques = FLAG 0b1000000 let fCONST kn = CONST kn let fPROJ p = PROJ p let fVAR id = VAR id @@ -38,7 +39,7 @@ let red_add ({flags; ts} as red) = function | VAR id -> {red with ts = {ts with tr_var = Id.Pred.add id ts.tr_var}} let red_sub ({flags; ts} as red) = function - | FLAG f -> {red with flags = flags land (0b111111 lxor f)} + | FLAG f -> {red with flags = flags land (0b1111111 lxor f)} | CONST kn -> {red with ts = {ts with tr_cst = Cpred.remove kn ts.tr_cst}} | PROJ p -> {red with ts = {ts with tr_prj = PRpred.remove p ts.tr_prj}} | VAR id -> { red with ts = {ts with tr_var = Id.Pred.remove id ts.tr_var}} diff --git a/kernel/redFlags.mli b/kernel/redFlags.mli index e226ab5de5fe..a267a2171c80 100644 --- a/kernel/redFlags.mli +++ b/kernel/redFlags.mli @@ -25,6 +25,7 @@ val fMATCH : red_kind val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind +val fNoOpaques : red_kind val fCONST : Names.Constant.t -> red_kind val fPROJ : Names.Projection.Repr.t -> red_kind val fVAR : Names.Id.t -> red_kind diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0d81630d88e6..3297cb8daa58 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -153,14 +153,10 @@ let rec n_x_id ids n = let simpl_iter clause = reduce (Lazy - { rBeta = true - ; rMatch = true - ; rFix = true - ; rCofix = true - ; rZeta = true - ; rDelta = false - ; rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))] - ; rStrength = Norm }) + { Redops.all_flags with + rDelta = false; + rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))]; + }) clause (* [value_f ctx ref] build [fun ctx => proj1_sig (ref ctx)] where diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml index 26b3be162ee5..79bc1725e623 100644 --- a/plugins/ltac2/tac2quote.ml +++ b/plugins/ltac2/tac2quote.ml @@ -444,7 +444,8 @@ let make_red_flag l = in add_flag {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []; rStrength = Norm; } + rZeta = false; rDelta = false; rConst = []; rStrength = Norm; + rNoOpaques = false; } l let of_reference r = diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index 26d557d90bed..26c8cb971fd2 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -76,6 +76,7 @@ let to_red_flag v : Tac2types.red_flag = match Value.to_tuple v with rZeta = Value.to_bool zeta; rDelta = Value.to_bool delta; rConst = Value.to_list Value.to_reference const; + rNoOpaques = false; } | _ -> assert false diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 40258be845cb..9d3e7e73480c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1241,7 +1241,8 @@ let tclFULL_BETAIOTA = Goal.enter begin fun gl -> let r, _ = Redexpr.reduction_of_red_expr (Goal.env gl) Genredexpr.(Lazy { rBeta=true; rMatch=true; rFix=true; rCofix=true; - rZeta=false; rDelta=false; rConst=[]; rStrength=Norm}) in + rZeta=false; rDelta=false; rConst=[]; rStrength=Norm; + rNoOpaques=false; }) in Tactics.e_reduct_in_concl ~cast:false ~check:false (r,Constr.DEFAULTcast) end diff --git a/tactics/genredexpr.mli b/tactics/genredexpr.mli index 3fca916bdd85..36786319aa8b 100644 --- a/tactics/genredexpr.mli +++ b/tactics/genredexpr.mli @@ -21,6 +21,7 @@ type 'a red_atom = | FConst of 'a list | FDeltaBut of 'a list | FHead + | FNoOpaques (** This list of atoms is immediately converted to a [glob_red_flag] *) @@ -35,7 +36,8 @@ type 'a glob_red_flag = { rCofix : bool; rZeta : bool; rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) - rConst : 'a list + rConst : 'a list; + rNoOpaques : bool; } (** Generic kinds of reductions *) diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 7e36eaf48aaf..08b58768c247 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -219,6 +219,7 @@ let make_flag env f = let red = if f.rFix then red_add red fFIX else red in let red = if f.rCofix then red_add red fCOFIX else red in let red = if f.rZeta then red_add red fZETA else red in + let red = if f.rNoOpaques then red_add red fNoOpaques else red in let red = if f.rDelta then (* All but rConst *) let red = red_add red fDELTA in diff --git a/tactics/redops.ml b/tactics/redops.ml index d391f2ea68eb..ac635afa1ad2 100644 --- a/tactics/redops.ml +++ b/tactics/redops.ml @@ -12,42 +12,47 @@ open Genredexpr let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *) - let all_flags = {rBeta = true; rMatch = true; rFix = true; rCofix = true; - rZeta = true; rDelta = true; rConst = []; rStrength = Norm; } + rZeta = true; rDelta = true; rConst = []; rStrength = Norm; + rNoOpaques = false; + } let make_red_flag l = - let rec add_flag red = function - | [] -> red - | FHead :: lf -> add_flag { red with rStrength = Head } lf - | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FMatch :: lf -> add_flag { red with rMatch = true } lf - | FFix :: lf -> add_flag { red with rFix = true } lf - | FCofix :: lf -> add_flag { red with rCofix = true } lf - | FZeta :: lf -> add_flag { red with rZeta = true } lf - | FConst l :: lf -> - if red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag { red with rConst = union_consts red.rConst l } lf - | FDeltaBut l :: lf -> - if red.rConst <> [] && not red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag - { red with rConst = union_consts red.rConst l; rDelta = true } - lf + let add_flag red = function + | FHead -> { red with rStrength = Head } + | FBeta -> { red with rBeta = true } + | FMatch -> { red with rMatch = true } + | FFix -> { red with rFix = true } + | FCofix -> { red with rCofix = true } + | FZeta -> { red with rZeta = true } + | FConst l -> + let () = if red.rDelta then + CErrors.user_err + Pp.(str "Cannot set both constants to unfold and constants not to unfold") + in + { red with rConst = union_consts red.rConst l } + | FDeltaBut l -> + let () = if red.rConst <> [] && not red.rDelta then + CErrors.user_err + Pp.(str "Cannot set both constants to unfold and constants not to unfold") + in + { red with rConst = union_consts red.rConst l; rDelta = true } + | FNoOpaques -> { red with rNoOpaques = true } + in + let base = + (* if the flags are just head and/or noopaques, don't disable reduction *) + if List.exists (function FHead | FNoOpaques -> false | _ -> true) l then + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []; rStrength = Norm; + rNoOpaques = false; + } + else all_flags in - add_flag - {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []; rStrength = Norm; } + List.fold_left add_flag + base l -let make_red_flag = function - | [FHead] -> { all_flags with rStrength = Head } - | l -> make_red_flag l - (** Mapping [red_expr_gen] *) let map_flags f flags = diff --git a/test-suite/success/noopaques.v b/test-suite/success/noopaques.v new file mode 100644 index 000000000000..768cd9c7c770 --- /dev/null +++ b/test-suite/success/noopaques.v @@ -0,0 +1,17 @@ +Lemma foo : nat. Proof. exact 0. Qed. + +Axiom bar : nat. + +Eval lazy noopaques in (fun _ => 1) foo. +Fail Eval lazy noopaques in foo = foo. +Eval lazy head noopaques in foo = foo. + +Fail Eval lazy noopaques in (fun x => x + x). +Eval lazy head noopaques in (fun x => x + x). + +Fail Eval lazy noopaques in bar. + +Require PrimInt63. + +(* unapplied primitives are not considered opaque *) +Eval lazy noopaques in PrimInt63.add. diff --git a/vernac/g_redexpr.mlg b/vernac/g_redexpr.mlg index ad30e803ee21..a7d91b05ecd7 100644 --- a/vernac/g_redexpr.mlg +++ b/vernac/g_redexpr.mlg @@ -77,6 +77,7 @@ GRAMMAR EXTEND Gram | IDENT "zeta" -> { [FZeta] } | IDENT "delta"; d = delta_flag -> { [d] } | IDENT "head" -> { [FHead] } + | IDENT "noopaques" -> { [FNoOpaques] } ] ] ; delta_flag: