From fab0ba7722e601f5107a9ff09a0e63624d488be2 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 25 Mar 2026 19:38:41 +0100 Subject: [PATCH] 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. --- src/ecCommands.ml | 27 ++++--- src/ecCoreGoal.ml | 18 ++++- src/ecCoreGoal.mli | 3 + src/ecEnv.ml | 133 +++++++++++++++++++++++++++++------ src/ecEnv.mli | 27 +++++-- src/ecHiGoal.ml | 39 ++++++++++ src/ecHiGoal.mli | 1 + src/ecHiTacticals.ml | 1 + src/ecParser.mly | 57 +++++++++++---- src/ecParsetree.ml | 12 +++- src/ecPrinting.ml | 7 +- src/ecReduction.ml | 35 ++++++++- src/ecReduction.mli | 2 + src/ecScope.ml | 7 +- src/ecSubst.ml | 9 ++- src/ecTheory.ml | 7 +- src/ecTheory.mli | 7 +- src/ecTheoryReplay.ml | 6 +- tests/hint_simplify_db.ec | 25 +++++++ tests/local_hint_simplify.ec | 60 ++++++++++++++++ 20 files changed, 416 insertions(+), 67 deletions(-) create mode 100644 tests/hint_simplify_db.ec create mode 100644 tests/local_hint_simplify.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index acca51faeb..1534ee6fff 100644 --- a/src/ecCommands.ml +++ b/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 "@[%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 "@[%s:@\n%a@]" + (if base = EcEnv.Reduction.dname then "" 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 (* -------------------------------------------------------------------- *) diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c1..d2c4c9db8a 100644 --- a/src/ecCoreGoal.ml +++ b/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; diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index f574b49bf3..243e63413e 100644 --- a/src/ecCoreGoal.mli +++ b/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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index edd45ca71f..89aaf579ac 100644 --- a/src/ecEnv.ml +++ b/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 diff --git a/src/ecEnv.mli b/src/ecEnv.mli index d96a9e192a..5322509845 100644 --- a/src/ecEnv.mli +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 1b79f912fc..be9331b378 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -90,9 +90,46 @@ let process_change fp (tc : tcenv1) = let fp = TTC.tc1_process_formula tc fp in t_change fp tc +(* -------------------------------------------------------------------- *) +let process_local_hint (hint : plocalhint) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let simpl = FApi.tc1_local_simplify tc in + + let simpl = + match hint with + | PLHDb (`Add, dbs) -> + EcEnv.LocalSimplify.activate dbs simpl + + | PLHDb (`Remove, dbs) -> + EcEnv.LocalSimplify.deactivate dbs simpl + + | PLHLemmas (mode, base, lemmas) -> + let opts = EcTheory.{ ur_delta = false; ur_eqtrue = false; } in + let entries = + List.map (fun lemma -> + let path = EcEnv.Ax.lookup_path (unloc lemma) env in + let rule = EcReduction.User.compile ~opts ~prio:0 env path in + (path, rule) + ) lemmas + in + begin match mode with + | `Add -> + EcEnv.LocalSimplify.add_rules ?base entries simpl + | `Remove -> + EcEnv.LocalSimplify.remove_paths ?base (List.map fst entries) simpl + end + + | PLHClear base -> + EcEnv.LocalSimplify.clear ?base simpl + in + + FApi.tcenv_of_tcenv1 + (FApi.map_pregoal1 (fun goal -> { goal with g_simpl = simpl }) tc) + (* -------------------------------------------------------------------- *) let process_simplify_info ri (tc : tcenv1) = let env, hyps, _ = FApi.tc1_eflat tc in + let simpl = FApi.tc1_local_simplify tc in let do1 (sop, sid) ps = match ps.pl_desc with @@ -123,6 +160,8 @@ let process_simplify_info ri (tc : tcenv1) = EcReduction.logic = if ri.plogic then Some `Full else None; EcReduction.modpath = ri.pmodpath; EcReduction.user = ri.puser; + EcReduction.user_db = ri.puser_db; + EcReduction.user_local = simpl; } (*-------------------------------------------------------------------- *) diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 317163fd6e..b3a2fdd197 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -90,6 +90,7 @@ val process_congr : backward val process_solve : ?bases:symbol list -> ?depth:int -> backward val process_trivial : backward val process_change : pformula -> backward +val process_local_hint : plocalhint -> backward val process_simplify : preduction -> backward val process_cbv : preduction -> backward val process_pose : psymbol -> ptybindings -> rwocc -> pformula -> backward diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 86338c5af9..ac2210159b 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -154,6 +154,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Pmemory m -> process_memory m | Pwlog (ids, b, f) -> process_wlog ~suff:b ids f | Pgenhave gh -> process_genhave ttenv gh + | PlocalHint h -> process_local_hint h | Prwnormal _ -> assert false | Pcoq (m, n, pi) -> process_coq ~loc:(loc t) ~name:n.pl_desc ttenv m pi in diff --git a/src/ecParser.mly b/src/ecParser.mly index d97f4ccb93..1068768b38 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -88,12 +88,12 @@ pa_kind = k; pa_locality = locality; } - let mk_simplify l = + let mk_simplify ?db l = if l = [] then { pbeta = true; pzeta = true; piota = true; peta = true; plogic = true; pdelta = None; - pmodpath = true; puser = true; } + pmodpath = true; puser = true; puser_db = db; } else let doarg acc = function | `Delta l -> @@ -113,10 +113,14 @@ { pbeta = false; pzeta = false; piota = false; peta = false; plogic = false; pdelta = Some []; - pmodpath = false; puser = false; } l + pmodpath = false; puser = false; puser_db = db; } l let simplify_red = [`Zeta; `Iota; `Beta; `Eta; `Logic; `ModPath; `User] + let as_hintdb_mode = function + | `Plus -> `Add + | `Minus -> `Remove + let mk_pterm explicit head args = { fp_mode = if explicit then `Explicit else `Implicit; fp_head = head; @@ -2491,16 +2495,30 @@ simplify_arg: | LOGIC { `Logic } | MODPATH { `ModPath } +%inline simplify_db: +| HINT x=lident { unloc x } + +%inline pmode: +| PLUS { `Plus } +| MINUS { `Minus } + simplify: -| l=simplify_arg+ { l } -| SIMPLIFY { simplify_red } -| SIMPLIFY l=qoident+ { `Delta l :: simplify_red } -| SIMPLIFY DELTA { `Delta [] :: simplify_red } +| l=simplify_arg+ db=simplify_db? + { mk_simplify ?db l } +| SIMPLIFY db=simplify_db? + { mk_simplify ?db simplify_red } +| SIMPLIFY l=qoident+ db=simplify_db? + { mk_simplify ?db (`Delta l :: simplify_red) } +| SIMPLIFY DELTA db=simplify_db? + { mk_simplify ?db (`Delta [] :: simplify_red) } cbv: -| CBV { simplify_red } -| CBV l=qoident+ { `Delta l :: simplify_red } -| CBV DELTA { `Delta [] :: simplify_red } +| CBV db=simplify_db? + { mk_simplify ?db simplify_red } +| CBV l=qoident+ db=simplify_db? + { mk_simplify ?db (`Delta l :: simplify_red) } +| CBV DELTA db=simplify_db? + { mk_simplify ?db (`Delta [] :: simplify_red) } conseq: | empty { None, None } @@ -2723,6 +2741,17 @@ logtactic: | ASSUMPTION { Passumption } +| HINT m=pmode x=lident SIMPLIFY dbs=lident+ + { if unloc x <> "db" then + parse_error x.pl_loc (Some ("invalid hint command: " ^ (unloc x))); + PlocalHint (PLHDb (as_hintdb_mode m, List.map unloc dbs)) } + +| HINT m=pmode SIMPLIFY db=prefix(IN, lident)? l=qident+ + { PlocalHint (PLHLemmas (as_hintdb_mode m, omap unloc db, l)) } + +| HINT CLEAR SIMPLIFY db=prefix(IN, lident)? + { PlocalHint (PLHClear (omap unloc db)) } + | MOVE vw=prefix(SLASH, pterm)* gp=prefix(COLON, revert)? { Pmove { pr_rev = odfl prevert0 gp; pr_view = vw; } } @@ -2808,10 +2837,10 @@ logtactic: { Papply (`Apply (es, `Exact), None) } | l=simplify - { Psimplify (mk_simplify l) } + { Psimplify l } | l=cbv - { Pcbv (mk_simplify l) } + { Pcbv l } | CHANGE f=sform { Pchange f } @@ -3804,8 +3833,10 @@ hint: (* -------------------------------------------------------------------- *) (* User reduction *) reduction: +| HINT SIMPLIFY IN db=lident COLON opt=bracket(user_red_option*)? xs=plist1(user_red_info, COMMA) + { (Some (unloc db), odfl [] opt, xs) } | HINT SIMPLIFY opt=bracket(user_red_option*)? xs=plist1(user_red_info, COMMA) - { (odfl [] opt, xs) } + { (None, odfl [] opt, xs) } user_red_info: | x=qident i=prefix(AT, word)? diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 877f370741..7ddac527bf 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -534,6 +534,7 @@ type preduction = { plogic : bool; (* logical simplification *) pmodpath : bool; (* modpath normalization *) puser : bool; (* user reduction *) + puser_db : symbol option; (* user reduction database *) } (* -------------------------------------------------------------------- *) @@ -991,6 +992,14 @@ type clear_info = [ (* -------------------------------------------------------------------- *) type pgenhave = psymbol * intropattern option * psymbol list * pformula +(* -------------------------------------------------------------------- *) +type phintdbmode = [ `Add | `Remove ] + +type plocalhint = + | PLHDb of phintdbmode * symbol list + | PLHLemmas of phintdbmode * symbol option * pqsymbol list + | PLHClear of symbol option + (* -------------------------------------------------------------------- *) type logtactic = | Preflexivity @@ -1022,6 +1031,7 @@ type logtactic = | Pgenhave of pgenhave | Pwlog of (psymbol list * bool * pformula) | Pcoq of (EcProvers.coq_mode option * psymbol * pprover_infos) + | PlocalHint of plocalhint (* -------------------------------------------------------------------- *) and ptactic_core_r = @@ -1278,7 +1288,7 @@ type puseroption = [`Delta | `EqTrue] type puserred = - puseroption list * (pqsymbol list * int option) list + symbol option * puseroption list * (pqsymbol list * int option) list type threquire = psymbol option * (psymbol * psymbol option) list * [`Import|`Export] option diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index dff558c4db..2b28d9aa95 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3762,9 +3762,12 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = pp_locality lc (pp_rwname ppe) p (pp_list "@ " (pp_axname ppe)) l - | EcTheory.Th_reduction _ -> + | EcTheory.Th_reduction { red_base; _ } -> (* FIXME: section we should add the lemma in the reduction *) - Format.fprintf fmt "hint simplify." + begin match red_base with + | None -> Format.fprintf fmt "hint simplify." + | Some base -> Format.fprintf fmt "hint simplify in %s : ." base + end | EcTheory.Th_auto { level; base; axioms; locality; } -> Format.fprintf fmt "%ahint solve %d %s : %a." diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 261740e899..ffd8ee9845 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -642,6 +642,8 @@ type reduction_info = { logic : rlogic_info; modpath : bool; user : bool; + user_db : EcSymbols.symbol option; + user_local : EcEnv.local_simplify; } and deltap = [Op.redmode | `No] @@ -658,6 +660,8 @@ let full_red = { logic = Some `Full; modpath = true; user = true; + user_db = None; + user_local = EcEnv.LocalSimplify.empty; } let no_red = { @@ -670,6 +674,8 @@ let no_red = { logic = None; modpath = false; user = false; + user_db = None; + user_local = EcEnv.LocalSimplify.empty; } let beta_red = { no_red with beta = true; } @@ -741,8 +747,35 @@ let reduce_user_gen simplify ri env hyps f = | Fproj (_, i) -> `Proj i | _ -> raise nohead in - let rules = EcEnv.Reduction.get p env in + let get_rules_for_base base = + let removed = EcEnv.LocalSimplify.removed ~base ri.user_local in + let rules = + EcEnv.Reduction.get_entries ~base p env + |> List.filter (fun (src, _) -> not (EcPath.Sp.mem src removed)) + |> List.map snd + in + let added = + EcEnv.LocalSimplify.added ~base ri.user_local + |> List.filter_map (fun ((_, rule) : EcEnv.Reduction.entry) -> + let p' : EcEnv.Reduction.topsym = + match rule.rl_ptn with + | Rule (`Op p, _) -> `Path (fst p) + | Rule (`Tuple, _) -> `Tuple + | Rule (`Proj i, _) -> `Proj i + | Var _ | Int _ -> assert false + in + if p' = p then Some rule else None) + in + rules @ added + in + + let bases = + match ri.user_db with + | Some base -> [if base = "default" then EcEnv.Reduction.dname else base] + | None -> EcSymbols.Ssym.elements (EcEnv.LocalSimplify.active ri.user_local) + in + let rules = List.flatten (List.map get_rules_for_base bases) in if rules = [] then raise nohead; let module R = EcTheory in diff --git a/src/ecReduction.mli b/src/ecReduction.mli index ceb057d245..1b5011419f 100644 --- a/src/ecReduction.mli +++ b/src/ecReduction.mli @@ -70,6 +70,8 @@ type reduction_info = { logic : rlogic_info; (* perform logical simplification *) modpath : bool; (* reduce module path *) user : bool; (* reduce user defined rules *) + user_db : EcSymbols.symbol option; (* user reduction database *) + user_local : EcEnv.local_simplify; (* proof-local simplify overlay *) } and deltap = [EcEnv.Op.redmode | `No] diff --git a/src/ecScope.ml b/src/ecScope.ml index e7a753b0fe..97c17ff632 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2082,7 +2082,7 @@ end (* -------------------------------------------------------------------- *) module Reduction = struct (* FIXME: section -> allow "local" flag *) - let add_reduction scope (opts, reds) = + let add_reduction scope (base, opts, reds) = check_state `InTop "hint simplify" scope; let rules = @@ -2103,7 +2103,10 @@ module Reduction = struct in - let item = EcTheory.mkitem ~import:true (EcTheory.Th_reduction rules) in + let item = + EcTheory.mkitem ~import:true + (EcTheory.Th_reduction { red_base = base; red_rules = rules }) + in { scope with sc_env = EcSection.add_item item scope.sc_env } end diff --git a/src/ecSubst.ml b/src/ecSubst.ml index bc52ff4ba4..868e5e742c 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1061,10 +1061,10 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = | Th_addrw (b, ls, lc) -> Th_addrw (subst_path s b, List.map (subst_path s) ls, lc) - | Th_reduction rules -> - let rules = - List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) rules - in Th_reduction rules + | Th_reduction ({ red_rules } as red) -> + let red_rules = + List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) red_rules + in Th_reduction { red with red_rules } | Th_auto ({ axioms } as auto_rl) -> Th_auto { auto_rl with axioms = @@ -1209,4 +1209,3 @@ let inv_rebind (inv : inv) (ms : memory list) : inv = | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr) | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m) | _, _ -> assert false - diff --git a/src/ecTheory.ml b/src/ecTheory.ml index c4bcbfe19c..5f6e375f15 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -29,7 +29,7 @@ and theory_item_r = | Th_instance of (ty_params * EcTypes.ty) * tcinstance * is_local | Th_baserw of symbol * is_local | Th_addrw of EcPath.path * EcPath.path list * is_local - | Th_reduction of (EcPath.path * rule_option * rule option) list + | Th_reduction of reduction_rule | Th_auto of auto_rule | Th_alias of (symbol * path) (* FIXME: currently, only theories *) @@ -69,6 +69,11 @@ and rule_option = { ur_eqtrue : bool; } +and reduction_rule = { + red_base : symbol option; + red_rules : (path * rule_option * rule option) list; +} + and auto_rule = { level : int; base : symbol option; diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 20c34364b8..2a59ff246c 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -26,7 +26,7 @@ and theory_item_r = | Th_baserw of symbol * is_local | Th_addrw of EcPath.path * EcPath.path list * is_local (* reduction rule does not survive to section so no locality *) - | Th_reduction of (EcPath.path * rule_option * rule option) list + | Th_reduction of reduction_rule | Th_auto of auto_rule | Th_alias of (symbol * path) @@ -66,6 +66,11 @@ and rule_option = { ur_eqtrue : bool; } +and reduction_rule = { + red_base : symbol option; + red_rules : (path * rule_option * rule option) list; +} + and auto_rule = { level : int; base : symbol option; diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index de60a2a630..e65de8c93f 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -926,7 +926,7 @@ and replay_auto (* -------------------------------------------------------------------- *) and replay_reduction (ove : _ ovrenv) (subst, ops, proofs, scope) - (import, rules : _ * (EcPath.path * EcTheory.rule_option * EcTheory.rule option) list) + (import, ({ red_rules } as red) : _ * EcTheory.reduction_rule) = let for1 (p, opts, rule) = let exception Removed in @@ -945,8 +945,8 @@ and replay_reduction in (p, opts, rule) in - let rules = List.map for1 rules in - let scope = ove.ovre_hooks.hadd_item scope ~import (Th_reduction rules) in + let red_rules = List.map for1 red_rules in + let scope = ove.ovre_hooks.hadd_item scope ~import (Th_reduction { red with red_rules }) in (subst, ops, proofs, scope) diff --git a/tests/hint_simplify_db.ec b/tests/hint_simplify_db.ec new file mode 100644 index 0000000000..e9e316eaa4 --- /dev/null +++ b/tests/hint_simplify_db.ec @@ -0,0 +1,25 @@ +require import Int. + +op wrap_default : int -> int. +op wrap_named : int -> int. +op box : int -> int. + +axiom wrap_defaultE (x : int) : wrap_default x = x + 1. +axiom wrap_namedE (x : int) : wrap_named x = x + 2. + +hint simplify wrap_defaultE. +hint simplify in named: wrap_namedE. + +lemma wrap_default_simplifies (x : int) : + box (wrap_default x) = box (x + 1). +proof. + simplify. + trivial. +qed. + +lemma wrap_named_simplifies (x : int) : + box (wrap_named x) = box (x + 2). +proof. + simplify hint named. + trivial. +qed. diff --git a/tests/local_hint_simplify.ec b/tests/local_hint_simplify.ec new file mode 100644 index 0000000000..b84d2796f9 --- /dev/null +++ b/tests/local_hint_simplify.ec @@ -0,0 +1,60 @@ +require import Int. + +op wrap_default : int -> int. +op wrap_named : int -> int. +op wrap_local : int -> int. +op box : int -> int. + +axiom wrap_defaultE (x : int) : wrap_default x = x + 1. +axiom wrap_namedE (x : int) : wrap_named x = x + 2. +axiom wrap_localE (x : int) : wrap_local x = x + 3. + +hint simplify wrap_defaultE. +hint simplify in named: wrap_namedE. + +lemma explicit_named_db (x : int) : + box (wrap_named x) = box (x + 2). +proof. + simplify hint named. + trivial. +qed. + +lemma activate_named_db (x : int) : + box (wrap_named x) = box (x + 2). +proof. + hint +db simplify named. + simplify. + trivial. +qed. + +lemma deactivate_default_db (x : int) : + box (wrap_default x) = box (x + 1). +proof. + hint -db simplify default. + simplify. + hint +db simplify default. + simplify. + trivial. +qed. + +lemma add_remove_clear_local_hints (x : int) : + box (wrap_local x) = box (x + 3). +proof. + hint +simplify wrap_localE. + simplify. + trivial. +qed. + +lemma remove_local_hint (x : int) : + box (wrap_local x) = box (x + 3). +proof. + hint +simplify wrap_localE. + hint -simplify wrap_localE. + simplify. + hint +simplify wrap_localE. + hint clear simplify. + simplify. + hint +simplify wrap_localE. + simplify. + trivial. +qed.