diff --git a/src/ecCommands.ml b/src/ecCommands.ml index acca51fae..1534ee6ff 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 4b75e5b0c..d2c4c9db8 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 f574b49bf..243e63413 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 edd45ca71..89aaf579a 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 d96a9e192..532250984 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 1b79f912f..be9331b37 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 317163fd6..b3a2fdd19 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 86338c5af..ac2210159 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 d97f4ccb9..1068768b3 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 877f37074..7ddac527b 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 dff558c4d..2b28d9aa9 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 261740e89..ffd8ee984 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 ceb057d24..1b5011419 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 e7a753b0f..97c17ff63 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 bc52ff4ba..868e5e742 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 c4bcbfe19..5f6e375f1 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 20c34364b..2a59ff246 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 de60a2a63..e65de8c93 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 000000000..e9e316eaa --- /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 000000000..b84d2796f --- /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.