Proof of concept "noopaques" flag makes reduction fail if it encounters an opaque

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

doc/tools/docgram/fullGrammar

@@ -799,6 +799,7 @@ red_flag: [
 | "zeta"
 | "delta" delta_flag
 | "head"
+| "noopaques"
 ]
 
 delta_flag: [

doc/tools/docgram/orderedGrammar

@@ -530,6 +530,7 @@ reductions: [
 
 reduction: [
 | "head"
+| "noopaques"
 | "beta"
 | "delta" OPT delta_reductions
 | "match"

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 *)

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

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}}

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

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

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 =

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
 

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
 

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 *)

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

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 =

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.

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: