Add named and local simplify hint databases

doc/tactics/hint-simplify.rst

@@ -0,0 +1,188 @@
+========================================================================
+Hints: `hint simplify`
+========================================================================
+
+The `hint simplify` commands manage user reduction rules used by
+`simplify`, `cbv`, and tactics that rely on the same simplification
+machinery.
+
+Hints can be declared globally in a theory, selected through named
+databases, and adjusted locally inside a proof.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Global declarations
+------------------------------------------------------------------------
+
+Global declarations add lemmas to a simplification database.
+
+.. admonition:: Syntax
+
+   `hint simplify {lemma}+ .`
+
+Add the listed lemmas to the default simplification database.
+
+.. admonition:: Syntax
+
+   `hint simplify in {db} : {lemma}+ .`
+
+Add the listed lemmas to the named database `{db}`.
+
+These commands are theory-level declarations: once imported, the
+corresponding rules are available to simplification.
+
+------------------------------------------------------------------------
+The `hint` clause
+------------------------------------------------------------------------
+
+`simplify` and `cbv` accept a single `hint` clause that controls which
+user-reduction rules are used. The clause is introduced by the `hint`
+keyword and is built from an unsigned base database selection followed by
+any number of signed items:
+
+.. admonition:: Syntax
+
+   `simplify hint {db}* {item}*`
+
+where each `{item}` is one of:
+
+- `+ {db}` / `- {db}` — activate / deactivate a database;
+- `+[ {op}+ ]` / `-[ {op}+ ]` — head filter: keep only / drop rules headed
+  by the listed operators (at most one filter per clause);
+- `{ {lemma}+ }` — add lemmas to the default database for this call.
+
+The delimiter disambiguates an item: a bare name is a database, `[…]`
+holds operators, `{…}` holds lemmas. Lemma sets are add-only -- a clause
+never removes lemmas from a database; use the head filter to restrict
+which rules apply. The same clause is accepted by `cbv`.
+
+The database part of a clause is *either* an unsigned selection *or*
+signed deltas, never both (mixing them is redundant and rejected). An
+unsigned list `hint d1 d2` **replaces** the consulted databases with
+exactly `{d1, d2}`. Signed `+ {db}` / `- {db}` instead modify the current
+set (the proof-local default, else the active set): `simplify hint +d2`
+adds `d2` to it, `simplify hint -d3` removes `d3`.
+
+A head filter performs full simplification (like a bare `simplify`) with
+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]`).
+
+------------------------------------------------------------------------
+Proof-local commands
+------------------------------------------------------------------------
+
+Inside a proof, the simplify configuration can be changed without
+modifying the theory-level declarations. The `hint` command takes the
+same clause as the `simplify`/`cbv` tactics, and each kind of item has a
+persistent effect on the proof state:
+
+.. admonition:: Syntax
+
+   `hint {db}* {item}* .`
+
+- `+ {db}` / `- {db}` — activate / deactivate a database (for later bare
+  `simplify`/`cbv`);
+- `{ {lemma}+ }` — add lemmas to the default database;
+- an unsigned database list `{db}+` — set the proof-local default
+  databases used by later `simplify`/`cbv` calls;
+- `+[ {op}+ ]` / `-[ {op}+ ]` — set the proof-local default head filter.
+
+As in the tactic clause, the database part is *either* an unsigned
+selection *or* signed `+`/`-` deltas, never both.
+
+.. admonition:: Syntax
+
+   `hint clear [ {db} ] .`
+
+Clear the local lemma additions (for the default database, or for
+`{db}`).
+
+.. admonition:: Syntax
+
+   `hint clear default .`
+
+Clear the proof-local default database and head filter.
+
+These proof-local changes are part of the proof state and therefore
+follow the usual subgoal branching behavior. Explicit arguments on
+`simplify`/`cbv` take precedence over the proof-local defaults.
+
+------------------------------------------------------------------------
+Scoped application
+------------------------------------------------------------------------
+
+A `hint` command can be used as a scoped wrapper around a tactic, with the
+same clause syntax.
+
+.. admonition:: Syntax
+
+   `with hint {clause} ( {tactic} )`
+
+For example:
+
+.. code-block:: easycrypt
+
+   with hint +ring (simplify).
+   with hint {fooE} (rewrite foo /=).
+   with hint ring (cbv).
+
+The wrapped tactic runs with the modified hint configuration, but the
+subgoals produced afterwards are restored to the original configuration.
+
+------------------------------------------------------------------------
+Example
+------------------------------------------------------------------------
+
+.. ecproof::
+   :title: Simplify hint databases
+
+   require import AllCore Int.
+
+   op wrap1 (x : int) = x + 1.
+   op wrap2 (x : int) = x + 2.
+   op box   (x : int) = x.
+
+   lemma wrap1E x : box (wrap1 x) = box (x + 1).
+   proof. smt(). qed.
+
+   lemma wrap2E x : box (wrap2 x) = box (x + 2).
+   proof. smt(). qed.
+
+   hint simplify wrap1E.
+   hint simplify in named : wrap2E.
+
+   lemma demo_default (x : int) :
+     box (wrap1 x) = box (x + 1).
+   proof.
+     simplify.
+     trivial.
+   qed.
+
+   lemma demo_named (x : int) :
+     box (wrap2 x) = box (x + 2).
+   proof.
+     simplify hint named.
+     trivial.
+   qed.
+
+   lemma demo_local_default (x : int) :
+     box (wrap2 x) = box (x + 2).
+   proof.
+     with hint named (simplify).
+     trivial.
+   qed.
+
+   lemma demo_head_filter (x : int) :
+     box (wrap1 x) = box (x + 1).
+   proof.
+     simplify hint +[wrap1].
+     trivial.
+   qed.

src/ecCommands.ml

@@ -322,18 +322,11 @@ module HiPrinting = struct
   let pr_hint_simplify (fmt : Format.formatter) (env : EcEnv.env) =
     let open EcTheory in
 
-    let (hint_simplify: (EcEnv.Reduction.topsym * rule list) list) = EcEnv.Reduction.all env in
-
-    let hint_simplify = List.filter_map (fun (ts, rl) ->
-      match ts with
-      | `Path p -> Some (p, rl)
-      | _ -> None
-    ) hint_simplify
-    in
+    let hint_simplify = EcEnv.Reduction.all env in
 
     let ppe = EcPrinting.PPEnv.ofenv env in
 
-    let pp_hint_simplify ppe fmt = (fun (p,  (rls : rule list)) ->
+    let pp_rules ppe fmt = (fun (p,  (rls : rule list)) ->
       Format.fprintf fmt "@[<b 2>%s:@\n%a@]" (EcPath.basename p)
         (EcPrinting.pp_list "@\n" (fun fmt rl ->
           begin match rl.rl_cond with
@@ -348,7 +341,21 @@ module HiPrinting = struct
       )
     in
 
-    EcPrinting.pp_by_theory ppe pp_hint_simplify fmt hint_simplify
+    let pp_db fmt (base, entries) =
+      let entries = List.filter_map (fun (ts, rl) ->
+        match ts with
+        | `Path p -> Some (p, rl)
+        | _ -> None
+      ) entries in
+
+      if not (List.is_empty entries) then
+        Format.fprintf fmt "@[<v 2>%s:@\n%a@]"
+          (if base = EcEnv.Reduction.dname then "<default>" else base)
+          (EcPrinting.pp_by_theory ppe pp_rules) entries
+    in
+
+    EcPrinting.pp_list "@.@." pp_db fmt
+      (List.filter (fun (_, entries) -> not (List.is_empty entries)) hint_simplify)
 end
 
 (* -------------------------------------------------------------------- *)

src/ecCoreGoal.ml

@@ -141,6 +141,7 @@ and pregoal = {
   g_uid   : handle;                     (* this goal ID *)
   g_hyps  : LDecl.hyps;                 (* goal local environment *)
   g_concl : form;                       (* goal conclusion *)
+  g_simpl : EcEnv.simplify_context;       (* proof-local simplify context *)
 }
 
 and goal = {
@@ -393,7 +394,7 @@ module FApi = struct
 
   (* ------------------------------------------------------------------ *)
   let tc1_flat ?target (tc : tcenv1) =
-    let { g_hyps; g_concl } = tc1_current tc in
+    let { g_hyps; g_concl; _ } = tc1_current tc in
     match target with
     | None   -> (g_hyps, g_concl)
     | Some h -> (LDecl.local_hyps h g_hyps, LDecl.hyp_by_id h g_hyps)
@@ -410,6 +411,7 @@ module FApi = struct
   let tc1_penv (tc : tcenv1) = tc.tce_penv
   let tc1_goal (tc : tcenv1) = snd (tc1_flat tc)
   let tc1_env  (tc : tcenv1) = LDecl.toenv (tc1_hyps tc)
+  let tc1_simplify_context (tc : tcenv1) = (tc1_current tc).g_simpl
 
   (* ------------------------------------------------------------------ *)
   let tc_handle (tc : tcenv) = tc1_handle tc.tce_tcenv
@@ -460,7 +462,7 @@ module FApi = struct
   (* ------------------------------------------------------------------ *)
   let pf_newgoal (pe : proofenv) ?vx hyps concl =
     let hid     = ID.gen () in
-    let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; } in
+    let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; g_simpl = EcEnv.SimplifyContext.empty; } in
     let goal    = { g_goal = pregoal; g_validation = vx; } in
     let pe      = { pe with pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals; } in
       (pe, pregoal)
@@ -469,6 +471,8 @@ module FApi = struct
   let newgoal (tc : tcenv) ?(hyps : LDecl.hyps option) (concl : form) =
     let hyps     = ofdfl (fun () -> tc_hyps tc) hyps in
     let (pe, pg) = pf_newgoal (tc_penv tc) hyps concl in
+    let pg = { pg with g_simpl = tc1_simplify_context tc.tce_tcenv } in
+    let pe = update_goal_map (fun g -> { g with g_goal = pg }) pg.g_uid pe in
 
     let tc = tc_update_tcenv (fun te -> { te with tce_penv = pe }) tc in
     let tc = { tc with tce_goals = tc.tce_goals @ [pg.g_uid] } in
@@ -506,6 +510,14 @@ module FApi = struct
     let tc = mutate (tcenv_of_tcenv1 tc) vx ?hyps fp in
     assert (tc.tce_goals = []); tc.tce_tcenv
 
+  let map_pregoal1 (tx : pregoal -> pregoal) (tc : tcenv1) =
+    let current = tc1_current tc in
+    let current = tx current in
+    let tc =
+      tc1_update_goal_map (fun g -> { g with g_goal = current }) current.g_uid tc
+    in
+    { tc with tce_goal = Some current }
+
   (* ------------------------------------------------------------------ *)
   let xmutate (tc : tcenv) (vx : 'a) (fp : form list) =
     let (tc, hds) = List.map_fold (fun tc fp -> newgoal tc fp) tc fp in
@@ -989,7 +1001,7 @@ let start (hyps : LDecl.hyps) (goal : form) =
   let uid = ID.gen () in
   let hid = ID.gen () in
 
-  let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; } in
+  let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; g_simpl = EcEnv.SimplifyContext.empty; } in
   let goal = { g_goal = goal; g_validation = None; } in
   let env  = { pr_uid   = uid;
                pr_main  = hid;

src/ecCoreGoal.mli

@@ -144,6 +144,7 @@ type pregoal = {
   g_uid   : handle;
   g_hyps  : LDecl.hyps;
   g_concl : form;
+  g_simpl : EcEnv.simplify_context;
 }
 
 type validation =
@@ -279,6 +280,7 @@ module FApi : sig
    * focused goal local context. *)
   val mutate  : tcenv  -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv
   val mutate1 : tcenv1 -> (handle -> validation) -> ?hyps:LDecl.hyps -> form -> tcenv1
+  val map_pregoal1 : (pregoal -> pregoal) -> tcenv1 -> tcenv1
 
   (* Same as xmutate, but for an external node resolution depending on
    * a unbounded numbers of premises. The ['a] argument is the external
@@ -321,6 +323,7 @@ module FApi : sig
   val tc1_hyps   : ?target:ident -> tcenv1 -> LDecl.hyps
   val tc1_goal   : tcenv1 -> form
   val tc1_env    : tcenv1 -> EcEnv.env
+  val tc1_simplify_context : tcenv1 -> EcEnv.simplify_context
 
   (* Low-level tactic markers *)
   val t_low0 : string -> backward -> backward