feat(simplify): delta[f g] forces unfolding of listed operators

doc/tactics/hint-simplify.rst

@@ -70,10 +70,12 @@ user reduction restricted to the selected operators.
 
 The `hint` clause is independent of the reduction arguments that
 `simplify` and `cbv` already accept: a bare `simplify` performs full
-simplification, `simplify delta` additionally unfolds all definitions,
-`simplify f g` unfolds the operators `f` and `g`, and a keyword-less list
-such as `beta zeta` performs only the named reductions. A `hint` clause
-may follow any of these (for example `simplify delta hint +[f]`).
+simplification, `simplify delta` additionally unfolds all transparent
+definitions, `simplify delta[f g]` does the same and also unfolds `f` and
+`g` even when they are declared `[opaque]`, `simplify f g` unfolds only
+the operators `f` and `g`, and a keyword-less list such as `beta zeta`
+performs only the named reductions. A `hint` clause may follow any of
+these (for example `simplify delta hint +[f]`).
 
 ------------------------------------------------------------------------
 Proof-local commands

src/ecHiGoal.ml

@@ -167,10 +167,10 @@ let process_simplify_info ri (tc : tcenv1) =
   in
 
   let delta_p, delta_h =
-    ri.pdelta
-      |> omap (List.fold_left do1 (Sp.empty, Sid.empty))
-      |> omap (fun (x, y) -> (fun p -> if Sp.mem p x then `Force else `IfApplied), (Sid.mem^~ y))
-      |> odfl ((fun _ -> `IfTransparent), predT)
+    let sop, sid = List.fold_left do1 (Sp.empty, Sid.empty) ri.pdelta.pd_ops in
+    let dflt = if ri.pdelta.pd_all then `IfTransparent else `IfApplied in
+    ((fun p -> if Sp.mem p sop then `Force else dflt),
+     (if ri.pdelta.pd_all then predT else Sid.mem^~ sid))
   in
 
   let hint = ri.phint in

src/ecParser.mly

@@ -101,14 +101,14 @@
     if l = [] then
       { pbeta  = true; pzeta  = true;
         piota  = true; peta   = true;
-        plogic = true; pdelta = None;
+        plogic = true; pdelta = { pd_all = true; pd_ops = []; };
         pmodpath = true; puser = true; phint = hint; }
     else
       let doarg acc = function
-        | `Delta l ->
-            if   l = [] || acc.pdelta = None
-            then { acc with pdelta = None }
-            else { acc with pdelta = Some (oget acc.pdelta @ l) }
+        | `Delta pd ->
+            let pd_all = acc.pdelta.pd_all || pd.pd_all in
+            let pd_ops = acc.pdelta.pd_ops @  pd.pd_ops in
+            { acc with pdelta = { pd_all; pd_ops; } }
 
         | `Zeta    -> { acc with pzeta    = true }
         | `Iota    -> { acc with piota    = true }
@@ -121,7 +121,7 @@
         List.fold_left doarg
           { pbeta  = false; pzeta  = false;
             piota  = false; peta   = false;
-            plogic = false; pdelta = Some [];
+            plogic = false; pdelta = { pd_all = false; pd_ops = []; };
             pmodpath = false; puser = false; phint = hint; } l
 
   let simplify_red = [`Zeta; `Iota; `Beta; `Eta; `Logic; `ModPath; `User]
@@ -2525,14 +2525,20 @@ genpattern:
    head filter is NOT allowed here: those tokens are bullet operators and
    only a keyword ([simplify]/[cbv]) lets them be read as a head filter. *)
 simplify_arg:
-| DELTA l=qoident* { `Delta l }
+| DELTA l=qoident* { `Delta { pd_all = (l = []); pd_ops = l; } }
+| d=delta_arg      { `Delta d }
 | ZETA             { `Zeta }
 | IOTA             { `Iota }
 | BETA             { `Beta }
 | ETA              { `Eta }
 | LOGIC            { `Logic }
 | MODPATH          { `ModPath }
 
+(* [delta[f g]]: unfold every transparent definition and force [f] and
+   [g], opaque or not. Plain [delta] is the bracket-less case. *)
+%inline delta_arg:
+| DELTA l=bracket(qoident+) { { pd_all = true; pd_ops = l; } }
+
 %inline pmode:
 | PLUS  { `Plus  }
 | MINUS { `Minus }
@@ -2586,17 +2592,21 @@ simplify:
 | SIMPLIFY hint=simplify_mod
     { mk_simplify ~hint simplify_red }
 | SIMPLIFY l=qoident+ hint=simplify_mod
-    { mk_simplify ~hint (`Delta l  :: simplify_red) }
+    { mk_simplify ~hint (`Delta { pd_all = false; pd_ops = l; } :: simplify_red) }
 | SIMPLIFY DELTA hint=simplify_mod
-    { mk_simplify ~hint (`Delta [] :: simplify_red) }
+    { mk_simplify ~hint (`Delta { pd_all = true; pd_ops = []; } :: simplify_red) }
+| SIMPLIFY d=delta_arg hint=simplify_mod
+    { mk_simplify ~hint (`Delta d :: simplify_red) }
 
 cbv:
 | CBV hint=simplify_mod
     { mk_simplify ~hint simplify_red }
 | CBV l=qoident+ hint=simplify_mod
-    { mk_simplify ~hint (`Delta l  :: simplify_red) }
+    { mk_simplify ~hint (`Delta { pd_all = false; pd_ops = l; } :: simplify_red) }
 | CBV DELTA hint=simplify_mod
-    { mk_simplify ~hint (`Delta [] :: simplify_red) }
+    { mk_simplify ~hint (`Delta { pd_all = true; pd_ops = []; } :: simplify_red) }
+| CBV d=delta_arg hint=simplify_mod
+    { mk_simplify ~hint (`Delta d :: simplify_red) }
 
 conseq:
 | empty                            { None, None }

src/ecParsetree.ml

@@ -586,9 +586,16 @@ let empty_simplify_hint = {
 }
 
 (* -------------------------------------------------------------------- *)
+(* [pd_all] unfolds every transparent definition; [pd_ops] are unfolded
+   unconditionally, opaque ones included. Both may be set at once. *)
+type pdelta = {
+  pd_all : bool;
+  pd_ops : pqsymbol list;
+}
+
 type preduction = {
   pbeta    : bool;                      (* β-reduction *)
-  pdelta   : pqsymbol list option;      (* definition unfolding *)
+  pdelta   : pdelta;                    (* definition unfolding *)
   pzeta    : bool;                      (* let-reduction *)
   piota    : bool;                      (* case/if-reduction *)
   peta     : bool;                      (* η-reduction *)

tests/simplify-delta-ops.ec

@@ -0,0 +1,78 @@
+require import AllCore.
+
+(* [g]/[h] are opaque for reduction: [delta] alone never unfolds them
+   (and neither does the conversion behind [done]), so a goal that needs
+   their body closes only when they are listed in a [delta[...]]
+   argument. [f] is transparent and is unfolded by [delta] as usual;
+   naming it alone ([delta f], [simplify f]) leaves [g] folded. *)
+op f (x : int) = x + 1.
+op [opaque] g (x : int) = x + 2.
+op [opaque] h (x : int) = x + 3.
+
+(* Opaque, but with an unfold threshold (the [/]): never unfolded by
+   [delta] or by conversion, yet unfolded by the [IfApplied] mode that
+   [delta f] / [simplify f] use for unlisted operators, provided the
+   application reaches the threshold. *)
+op [opaque] k  (x : int)   / = x + 5.
+op [opaque] k2 (x y : int) / = x + y.
+
+lemma t1 (x : int) : f x + g x = x + 1 + (x + 2).
+proof.
+  fail (simplify delta; done).
+  fail (simplify f; done).
+  by simplify delta[g].
+qed.
+
+lemma t2 (x : int) : f x + g x + h x = x + 1 + (x + 2) + (x + 3).
+proof.
+  fail (cbv delta[g]; done).
+  by cbv delta[g h].
+qed.
+
+lemma t3 (x : int) : f x + g x = x + 1 + (x + 2).
+proof.
+  fail (delta; done).
+  fail (delta f; done).
+  by delta[g].
+qed.
+
+lemma t4 (x : int) : f x + g x = x + 1 + (x + 2).
+proof. by simplify delta[g] hint +core. qed.
+
+(* [delta f]: [f] is forced, [k] unfolds because it is applied to its
+   parameter, [g] stays folded. *)
+lemma t5 (x : int) : f x + g x + k x = x + 1 + g x + (x + 5).
+proof.
+  fail (delta; done).
+  fail (delta[f]; done).
+  by delta f.
+qed.
+
+lemma t6 (x : int) : f x + g x + k x = x + 1 + g x + (x + 5).
+proof.
+  fail (simplify delta; done).
+  by simplify f.
+qed.
+
+lemma t7 (x : int) : f x + g x + k x = x + 1 + g x + (x + 5).
+proof. by cbv f. qed.
+
+(* Below the threshold, [IfApplied] does not fire: [k] unapplied and
+   [k2] applied to one of its two parameters stay folded. *)
+lemma t8 : k = fun x => x + 5.
+proof.
+  fail (delta f; done).
+  by delta[k].
+qed.
+
+lemma t9 (x : int) : k2 x = fun y => x + y.
+proof.
+  fail (delta f; done).
+  by delta[k2].
+qed.
+
+lemma t10 (x : int) : k2 x x = x + x.
+proof.
+  fail (delta; done).
+  by delta f.
+qed.