Add named and local simplify hint databases

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