Add named and local simplify hint databases

Introduce named simplify databases for global `hint simplify`
declarations, and add proof-local control over which simplify DBs are
active and which simplify lemmas are temporarily added or removed.

Thread the local simplify context through proof goals so the active
DB set and local lemma overrides propagate across subgoals and are
consulted by `simplify` and `cbv`. Also update simplify-hint printing
and reduction storage to support named databases.

Add regression tests for named simplify DB selection and for local
proof commands that activate or deactivate simplify DBs and manipulate
local simplify lemmas.

Author: strub

src/ecCommands.ml

@@ -315,18 +315,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
@@ -341,7 +334,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.local_simplify;       (* 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_local_simplify (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.LocalSimplify.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_local_simplify 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.LocalSimplify.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.local_simplify;
 }
 
 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_local_simplify : tcenv1 -> EcEnv.local_simplify
 
   (* Low-level tactic markers *)
   val t_low0 : string -> backward -> backward

src/ecEnv.ml

@@ -187,7 +187,7 @@ type preenv = {
   env_tc       : TC.graph;
   env_rwbase   : Sp.t Mip.t;
   env_atbase   : atbase Msym.t;
-  env_redbase  : mredinfo;
+  env_redbase  : mredinfo Msym.t;
   env_ntbase   : ntbase Mop.t;
   env_albase   : path Mp.t;             (* theory aliases   *)
   env_modlcs   : Sid.t;                 (* declared modules *)
@@ -217,9 +217,11 @@ and tcinstance = [
   | `General of EcPath.path
 ]
 
+and redentry = EcPath.path * EcTheory.rule
+
 and redinfo =
-  { ri_priomap : (EcTheory.rule list) Mint.t;
-    ri_list    : (EcTheory.rule list) Lazy.t; }
+  { ri_priomap : (redentry list) Mint.t;
+    ri_list    : (redentry list) Lazy.t; }
 
 and mredinfo = redinfo Mrd.t
 
@@ -316,7 +318,7 @@ let empty gstate =
     env_tc       = TC.Graph.empty;
     env_rwbase   = Mip.empty;
     env_atbase   = Msym.empty;
-    env_redbase  = Mrd.empty;
+    env_redbase  = Msym.empty;
     env_ntbase   = Mop.empty;
     env_albase   = Mp.empty;
     env_modlcs   = Sid.empty;
@@ -1487,10 +1489,14 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction = struct
+  type entry  = redentry
   type rule   = EcTheory.rule
   type topsym = red_topsym
+  type base = symbol
+
+  let dname : symbol = ""
 
-  let add_rule ((_, rule) : path * rule option) (db : mredinfo) =
+  let add_rule ((src, rule) : path * rule option) (db : mredinfo) =
     match rule with None -> db | Some rule ->
 
     let p : topsym =
@@ -1507,7 +1513,7 @@ module Reduction = struct
         | Some x -> x in
 
       let ri_priomap =
-        let change prules = Some (odfl [] prules @ [rule]) in
+        let change prules = Some (odfl [] prules @ [(src, rule)]) in
         Mint.change change (abs rule.rl_prio) ri_priomap in
 
       let ri_list =
@@ -1518,26 +1524,111 @@ module Reduction = struct
   let add_rules (rules : (path * rule option) list) (db : mredinfo) =
     List.fold_left ((^~) add_rule) db rules
 
-  let add ?(import = true) (rules : (path * rule_option * rule option) list) (env : env) =
-    let rstrip = List.map (fun (x, _, y) -> (x, y)) rules in
+  let updatedb ?(base : symbol option) (rules : (path * rule option) list) (db : mredinfo Msym.t) =
+    let nbase = odfl dname base in
+    let base = Msym.find_def Mrd.empty nbase db in
+    Msym.add nbase (add_rules rules base) db
+
+  let add ?(import = true) ({ red_base; red_rules } : reduction_rule) (env : env) =
+    let rstrip = List.map (fun (x, _, y) -> (x, y)) red_rules in
 
     { env with
-        env_redbase = add_rules rstrip env.env_redbase;
-        env_item = mkitem ~import (Th_reduction rules) :: env.env_item; }
+        env_redbase = updatedb ?base:red_base rstrip env.env_redbase;
+        env_item = mkitem ~import (Th_reduction { red_base; red_rules }) :: env.env_item; }
 
-  let add1 (prule : path * rule_option * rule option) (env : env) =
-    add [prule] env
+  let add1 ?base (prule : path * rule_option * rule option) (env : env) =
+    add { red_base = base; red_rules = [prule] } env
 
-  let get (p : topsym) (env : env) =
-    Mrd.find_opt p env.env_redbase
+  let get_entries ?base (p : topsym) (env : env) =
+    Msym.find_opt (odfl dname base) env.env_redbase
+    |> obind (Mrd.find_opt p)
     |> omap (fun x -> Lazy.force x.ri_list)
     |> odfl []
 
-  (* FIXME: handle other cases, right now only used for print hint *)
+  let get ?base (p : topsym) (env : env) =
+    List.map snd (get_entries ?base p env)
+
+  let getx (base : symbol) (env : env) =
+    Msym.find_def Mrd.empty base env.env_redbase
+    |> Mrd.bindings
+    |> List.map (fun (ts, mr) -> (ts, List.map snd (Lazy.force mr.ri_list)))
+
   let all (env : env) =
-    List.map (fun (ts, mr) ->
-      (ts, Lazy.force mr.ri_list))
-    (Mrd.bindings env.env_redbase)
+    Msym.bindings env.env_redbase
+    |> List.map (fun (base, db) ->
+      (base, List.map (fun (ts, mr) -> (ts, List.map snd (Lazy.force mr.ri_list))) (Mrd.bindings db)))
+end
+
+type local_simplify = {
+  ls_active  : Ssym.t;
+  ls_added   : Reduction.entry list Msym.t;
+  ls_removed : Sp.t Msym.t;
+}
+
+module LocalSimplify = struct
+  let empty = {
+    ls_active  = Ssym.singleton Reduction.dname;
+    ls_added   = Msym.empty;
+    ls_removed = Msym.empty;
+  }
+
+  let active ls = ls.ls_active
+
+  let normbase = function
+    | Some "default" | None -> Reduction.dname
+    | Some base -> base
+
+  let activate bases ls =
+    { ls with ls_active = List.fold_left (fun st b -> Ssym.add (normbase (Some b)) st) ls.ls_active bases }
+
+  let deactivate bases ls =
+    { ls with ls_active = List.fold_left (fun st b -> Ssym.remove (normbase (Some b)) st) ls.ls_active bases }
+
+  let added ?base ls =
+    Msym.find_def [] (normbase base) ls.ls_added
+
+  let removed ?base ls =
+    Msym.find_def Sp.empty (normbase base) ls.ls_removed
+
+  let add_rules ?base rules ls =
+    let base = normbase base in
+    let old = Msym.find_def [] base ls.ls_added in
+    let old =
+      List.filter (fun (p, _) ->
+        not (List.exists (fun (p', _) -> EcPath.p_equal p p') rules))
+        old
+    in
+    let ls_added = Msym.add base (old @ rules) ls.ls_added in
+    let ls_removed =
+      let removed = Msym.find_def Sp.empty base ls.ls_removed in
+      let removed = List.fold_left (fun st (p, _) -> Sp.remove p st) removed rules in
+      Msym.add base removed ls.ls_removed
+    in
+    { ls with ls_added; ls_removed }
+
+  let remove_paths ?base paths ls =
+    let base = normbase base in
+    let ls_added =
+      let added = Msym.find_def [] base ls.ls_added in
+      let added =
+        List.filter (fun (p, _) ->
+          not (List.exists (EcPath.p_equal p) paths))
+          added
+      in
+      Msym.add base added ls.ls_added
+    in
+    let ls_removed =
+      let removed = Msym.find_def Sp.empty base ls.ls_removed in
+      let removed = List.fold_left (fun st p -> Sp.add p st) removed paths in
+      Msym.add base removed ls.ls_removed
+    in
+    { ls with ls_added; ls_removed }
+
+  let clear ?base ls =
+    let base = normbase base in
+    { ls with
+        ls_added = Msym.remove base ls.ls_added;
+        ls_removed = Msym.remove base ls.ls_removed; }
 end
 
 (* -------------------------------------------------------------------- *)
@@ -3003,9 +3094,9 @@ module Theory = struct
   (* ------------------------------------------------------------------ *)
   let bind_rd_th =
     let for1 _path db = function
-      | Th_reduction rules ->
-         let rules = List.map (fun (x, _, y) -> (x, y)) rules in
-         Some (Reduction.add_rules rules db)
+      | Th_reduction { red_base; red_rules } ->
+         let rules = List.map (fun (x, _, y) -> (x, y)) red_rules in
+         Some (Reduction.updatedb ?base:red_base rules db)
       | _ -> None
 
     in bind_base_th for1

src/ecEnv.mli

@@ -420,13 +420,32 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Reduction : sig
+  type entry = path * EcTheory.rule
   type rule   = EcTheory.rule
   type topsym = [ `Path of path | `Tuple | `Proj of int]
+  type base = symbol
+
+  val dname : symbol
+  val all : env -> (base * (topsym * rule list) list) list
+  val add1 : ?base:symbol -> path * rule_option * rule option -> env -> env
+  val add  : ?import:bool -> reduction_rule -> env -> env
+  val get  : ?base:symbol -> topsym -> env -> rule list
+  val get_entries : ?base:symbol -> topsym -> env -> entry list
+  val getx : symbol -> env -> (topsym * rule list) list
+end
 
-  val all : env -> (topsym * rule list) list
-  val add1 : path * rule_option * rule option -> env -> env
-  val add  : ?import:bool -> (path * rule_option * rule option) list -> env -> env
-  val get  : topsym -> env -> rule list
+type local_simplify
+
+module LocalSimplify : sig
+  val empty : local_simplify
+  val active : local_simplify -> Ssym.t
+  val activate : symbol list -> local_simplify -> local_simplify
+  val deactivate : symbol list -> local_simplify -> local_simplify
+  val added : ?base:symbol -> local_simplify -> Reduction.entry list
+  val removed : ?base:symbol -> local_simplify -> Sp.t
+  val add_rules : ?base:symbol -> Reduction.entry list -> local_simplify -> local_simplify
+  val remove_paths : ?base:symbol -> path list -> local_simplify -> local_simplify
+  val clear : ?base:symbol -> local_simplify -> local_simplify
 end
 
 (* -------------------------------------------------------------------- *)