From 5f7be80cc247e5ad91606e139b9b20c30be91d3c Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Thu, 9 Jan 2025 19:56:19 +0000 Subject: [PATCH] Rigid unification option for `hint solve/exact` This features introduced a new `rigid` flag for `hint exact/solve`. Lemmas added to a hint with this flag are applied using a rigid unification algorithm. Co-Authored-By: Gustavo Delerue Co-Authored-By: Pierre-Yves Strub --- src/ecCommands.ml | 15 ++++-- src/ecEnv.ml | 59 +++++++++++++++-------- src/ecEnv.mli | 14 +++--- src/ecLowGoal.ml | 33 +++++++------ src/ecLowGoal.mli | 7 ++- src/ecParser.mly | 25 +++++++--- src/ecParsetree.ml | 12 +++-- src/ecPrinting.ml | 35 ++++++++++---- src/ecScope.ml | 10 ++-- src/ecSection.ml | 45 +++++++++-------- src/ecSubst.ml | 5 +- src/ecTheory.ml | 9 +++- src/ecTheory.mli | 9 +++- src/ecTheoryReplay.ml | 12 ++--- tests/hint_rigid_should_fail_immediate.ec | 15 ++++++ 15 files changed, 203 insertions(+), 102 deletions(-) create mode 100644 tests/hint_rigid_should_fail_immediate.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 753c91424c..8114cbac50 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -264,17 +264,22 @@ module HiPrinting = struct let ppe0 = EcPrinting.PPEnv.ofenv env in EcPrinting.pp_by_theory ppe0 (EcPrinting.pp_axiom) fmt ax - (* ------------------------------------------------------------------ *) let pr_hint_solve (fmt : Format.formatter) (env : EcEnv.env) = let hint_solve = EcEnv.Auto.all env in - let hint_solve = List.map (fun p -> - (p, EcEnv.Ax.by_path p env) + let hint_solve = List.map (fun (p, mode) -> + let ax = EcEnv.Ax.by_path p env in + (p, (ax, mode)) ) hint_solve in let ppe = EcPrinting.PPEnv.ofenv env in - let pp_hint_solve ppe fmt pax = - Format.fprintf fmt "%a" (EcPrinting.pp_axiom ppe) pax + let pp_hint_solve ppe fmt = (fun (p, (ax, mode)) -> + let mode = + match mode with + | `Default -> "" + | `Rigid -> "(rigid)" in + Format.fprintf fmt "%a %s" (EcPrinting.pp_axiom ppe) (p, ax) mode + ) in EcPrinting.pp_by_theory ppe pp_hint_solve fmt hint_solve diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a870a017fe..a83045d38d 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -181,7 +181,7 @@ type preenv = { env_tci : ((ty_params * ty) * tcinstance) list; env_tc : TC.graph; env_rwbase : Sp.t Mip.t; - env_atbase : (path list Mint.t) Msym.t; + env_atbase : atbase Msym.t; env_redbase : mredinfo; env_ntbase : ntbase Mop.t; env_modlcs : Sid.t; (* declared modules *) @@ -221,6 +221,10 @@ and env_notation = ty_params * EcDecl.notation and ntbase = (path * env_notation) list +and atbase0 = path * [`Rigid | `Default] + +and atbase = atbase0 list Mint.t + (* -------------------------------------------------------------------- *) type env = preenv @@ -1516,39 +1520,53 @@ end (* -------------------------------------------------------------------- *) module Auto = struct + type base0 = path * [`Rigid | `Default] + let dname : symbol = "" - let updatedb ~level ?base (ps : path list) (db : (path list Mint.t) Msym.t) = + let updatedb + ~(level : int) + ?(base : symbol option) + (ps : atbase0 list) + (db : atbase Msym.t) + = let nbase = (odfl dname base) in - let ps' = Msym.find_def Mint.empty nbase db in - let ps' = + let base = Msym.find_def Mint.empty nbase db in + let levels = let doit x = Some (ofold (fun x ps -> ps @ x) ps x) in - Mint.change doit level ps' in - Msym.add nbase ps' db - - let add ?(import = import0) ~level ?base (ps : path list) lc (env : env) = + Mint.change doit level base in + Msym.add nbase levels db + + let add + ?(import = import0) + ~(level : int) + ?(base : symbol option) + (axioms : atbase0 list) + (locality : is_local) + (env : env) + = let env = if import.im_immediate then { env with - env_atbase = updatedb ?base ~level ps env.env_atbase; } + env_atbase = updatedb ?base ~level axioms env.env_atbase; } else env in { env with env_item = mkitem import - (Th_auto (level, base, ps, lc)) :: env.env_item; } + (Th_auto { level; base; axioms; locality; }) :: env.env_item; } - let add1 ?import ~level ?base (p : path) lc (env : env) = + let add1 ?import ~level ?base (p : atbase0) lc (env : env) = add ?import ?base ~level [p] lc env let get_core ?base (env : env) = Msym.find_def Mint.empty (odfl dname base) env.env_atbase - let flatten_db (db : path list Mint.t) = + let flatten_db (db : atbase) = Mint.fold_left (fun ps _ ps' -> ps @ ps') [] db let get ?base (env : env) = flatten_db (get_core ?base env) - let getall (bases : symbol list) (env : env) = + let getall (bases : symbol list) (env : env) : atbase0 list = let dbs = List.map (fun base -> get_core ~base env) bases in let dbs = List.fold_left (fun db mi -> @@ -1560,7 +1578,7 @@ module Auto = struct let db = Msym.find_def Mint.empty base env.env_atbase in Mint.bindings db - let all (env : env) : path list = + let all (env : env) : atbase0 list = Msym.values env.env_atbase |> List.map flatten_db |> List.flatten end @@ -2951,8 +2969,8 @@ module Theory = struct (* ------------------------------------------------------------------ *) let bind_at_th = let for1 _path db = function - | Th_auto (level, base, ps, _) -> - Some (Auto.updatedb ?base ~level ps db) + | Th_auto {level; base; axioms; _} -> + Some (Auto.updatedb ?base ~level axioms db) | _ -> None in bind_base_th for1 @@ -3125,9 +3143,12 @@ module Theory = struct let ps = List.filter ((not) |- inclear |- oget |- EcPath.prefix) ps in if List.is_empty ps then None else Some (Th_addrw (p, ps,lc)) - | Th_auto (lvl, base, ps, lc) -> - let ps = List.filter ((not) |- inclear |- oget |- EcPath.prefix) ps in - if List.is_empty ps then None else Some (Th_auto (lvl, base, ps, lc)) + | Th_auto ({ axioms } as auto_rl) -> + let axioms = List.filter (fun (p, _) -> + let p = oget (EcPath.prefix p) in + not (inclear p) + ) axioms in + if List.is_empty axioms then None else Some (Th_auto {auto_rl with axioms}) | (Th_export (p, _)) as item -> if Sp.mem p cleared then None else Some item diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 4bee0ef828..0ed659eb22 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -415,13 +415,15 @@ end (* -------------------------------------------------------------------- *) module Auto : sig + type base0 = path * [`Rigid | `Default] + val dname : symbol - val add1 : ?import:import -> level:int -> ?base:symbol -> path -> is_local -> env -> env - val add : ?import:import -> level:int -> ?base:symbol -> path list -> is_local -> env -> env - val get : ?base:symbol -> env -> path list - val getall : symbol list -> env -> path list - val getx : symbol -> env -> (int * path list) list - val all : env -> path list + val add1 : ?import:import -> level:int -> ?base:symbol -> base0 -> is_local -> env -> env + val add : ?import:import -> level:int -> ?base:symbol -> base0 list -> is_local -> env -> env + val get : ?base:symbol -> env -> base0 list + val getall : symbol list -> env -> base0 list + val getx : symbol -> env -> (int * base0 list) list + val all : env -> base0 list end (* -------------------------------------------------------------------- *) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 273d5a4130..88bd20a4f5 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -726,7 +726,7 @@ module Apply = struct exception NoInstance of (bool * reason * PT.pt_env * (form * form)) - let t_apply_bwd_r ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) = + let t_apply_bwd_r ?(ri = EcReduction.full_compat) ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) = let ((hyps, concl), pterr) = (FApi.tc1_flat tc, PT.copy pt.ptev_env) in let noinstance ?(dpe = false) reason = @@ -736,7 +736,7 @@ module Apply = struct match istop && PT.can_concretize pt.PT.ptev_env with | true -> let ax = PT.concretize_form pt.PT.ptev_env pt.PT.ptev_ax in - if EcReduction.is_conv ~ri:EcReduction.full_compat hyps ax concl + if EcReduction.is_conv ~ri hyps ax concl then pt else instantiate canview false pt @@ -747,7 +747,7 @@ module Apply = struct noinstance `IncompleteInference; pt with EcMatching.MatchFailure -> - match TTC.destruct_product hyps pt.PT.ptev_ax with + match TTC.destruct_product ~reduce:(mode.fm_conv) hyps pt.PT.ptev_ax with | Some _ -> (* FIXME: add internal marker *) instantiate canview false (PT.apply_pterm_to_hole pt) @@ -800,15 +800,15 @@ module Apply = struct t_apply pt tc - let t_apply_bwd ?mode ?canview pt (tc : tcenv1) = + let t_apply_bwd ?(ri : EcReduction.reduction_info option) ?mode ?canview pt (tc : tcenv1) = let hyps = FApi.tc1_hyps tc in let pt, ax = LowApply.check `Elim pt (`Hyps (hyps, !!tc)) in let ptenv = ptenv_of_penv hyps !!tc in let pt = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = ax; } in - t_apply_bwd_r ?mode ?canview pt tc + t_apply_bwd_r ?ri ?mode ?canview pt tc - let t_apply_bwd_hi ?(dpe = true) ?mode ?canview pt (tc : tcenv1) = - try t_apply_bwd ?mode ?canview pt tc + let t_apply_bwd_hi ?(ri : EcReduction.reduction_info option) ?(dpe = true) ?mode ?canview pt (tc : tcenv1) = + try t_apply_bwd ?ri ?mode ?canview pt tc with (NoInstance (_, r, pt, f)) -> tc_error_exn !!tc (NoInstance (dpe, r, pt, f)) end @@ -2582,22 +2582,27 @@ let t_coq let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(depth = 1) (tc : tcenv1) = let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in - let t_apply1 p tc = - + let t_apply1 ((p, rigid): Auto.base0) tc = + let ri, mode = + match rigid with + | `Rigid -> EcReduction.no_red, fmsearch + | `Default -> EcReduction.full_compat, mode in let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in try - Apply.t_apply_bwd_r ~mode ~canview:false pt tc - with Apply.NoInstance _ -> t_fail tc in + Apply.t_apply_bwd_r ~ri ~mode ~canview:false pt tc + with Apply.NoInstance _ -> + t_fail tc + in - let rec t_apply ctn p tc = + let rec t_apply ctn ip tc = if ctn > depth then t_fail tc - else (t_apply1 p @! t_trivial @! t_solve (ctn + 1) bases) tc + else (t_apply1 ip @! t_trivial @! t_solve (ctn + 1) bases) tc and t_solve ctn bases tc = match bases with | [] -> t_abort tc - | p::bases -> (FApi.t_or (t_apply ctn p) (t_solve ctn bases)) tc in + | ip::bases -> (FApi.t_or (t_apply ctn ip) (t_solve ctn bases)) tc in let t = t_solve 0 bases in let t = if canfail then FApi.t_try t else t in diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 30148db5c0..d7f4421ab4 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -134,14 +134,13 @@ module Apply : sig exception NoInstance of (bool * reason * pt_env * (form * form)) val t_apply_bwd_r : - ?mode:fmoptions -> ?canview:bool -> pt_ev -> FApi.backward + ?ri:EcReduction.reduction_info -> ?mode:fmoptions -> ?canview:bool -> pt_ev -> FApi.backward val t_apply_bwd : - ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward + ?ri:EcReduction.reduction_info -> ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward val t_apply_bwd_hi: - ?dpe:bool -> ?mode:fmoptions -> ?canview:bool - -> proofterm -> FApi.backward + ?ri:EcReduction.reduction_info -> ?dpe:bool -> ?mode:fmoptions -> ?canview:bool -> proofterm -> FApi.backward end (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 708ee96d61..b612e28d57 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3699,14 +3699,25 @@ addrw: | local=is_local HINT REWRITE p=lqident COLON l=lqident* { (local, p, l) } -hint: -| local=is_local HINT EXACT base=lident? COLON l=qident* - { { ht_local = local; ht_prio = 0; - ht_base = base ; ht_names = l; } } +hintoption: +| x=lident { + match unloc x with + | "rigid" -> `Rigid + | _ -> + parse_error x.pl_loc + (Some ("invalid option: " ^ (unloc x))) + } -| local=is_local HINT SOLVE i=word base=lident? COLON l=qident* - { { ht_local = local; ht_prio = i; - ht_base = base ; ht_names = l; } } +hint: +| local=is_local + HINT opts=ioption(bracket(hintoption)+) + prio=ID(EXACT { 0 } | SOLVE i=word { i }) + base=lident? COLON l=qident* + { { ht_local = local; + ht_prio = prio; + ht_base = base ; + ht_names = l; + ht_options = odfl [] opts; } } (* -------------------------------------------------------------------- *) (* User reduction *) diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 89039ad254..a93ada6c8f 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1228,12 +1228,16 @@ type save = [ `Qed | `Admit | `Abort ] (* -------------------------------------------------------------------- *) type theory_clear = (pqsymbol option) list +(* -------------------------------------------------------------------- *) +type phintoption = [ `Rigid ] + (* -------------------------------------------------------------------- *) type phint = { - ht_local : is_local; - ht_prio : int; - ht_base : psymbol option; - ht_names : pqsymbol list; + ht_local : is_local; + ht_prio : int; + ht_base : psymbol option; + ht_names : pqsymbol list; + ht_options : phintoption list; } (* -------------------------------------------------------------------- *) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 5b800e2b46..593a5abfca 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -499,6 +499,13 @@ let pp_rwname ppe fmt p = let pp_axname ppe fmt p = Format.fprintf fmt "%a" EcSymbols.pp_qsymbol (PPEnv.ax_symb ppe p) +let pp_axhnt ppe fmt (p, b) = + let b = + match b with + | `Default -> "" + | `Rigid -> " (rigid)" in + Format.fprintf fmt "%a%s" (pp_axname ppe) p b + (* -------------------------------------------------------------------- *) let pp_thname ppe fmt p = EcSymbols.pp_qsymbol fmt (PPEnv.th_symb ppe p) @@ -3020,23 +3027,31 @@ let pp_rwbase ppe fmt (p, rws) = (pp_rwname ppe) p (pp_list ", " (pp_axname ppe)) (Sp.elements rws) (* -------------------------------------------------------------------- *) -let pp_solvedb ppe fmt db = +let pp_solvedb ppe fmt (db: (int * (P.path * _) list) list) = List.iter (fun (lvl, ps) -> Format.fprintf fmt "[%3d] %a\n%!" - lvl (pp_list ", " (pp_axname ppe)) ps) + lvl + (pp_list ", " (pp_axhnt ppe)) + ps) db; let lemmas = List.flatten (List.map snd db) in - let lemmas = List.pmap (fun p -> + let lemmas = List.pmap (fun (p, ir) -> let ax = EcEnv.Ax.by_path_opt p ppe.PPEnv.ppe_env in - (omap (fun ax -> (p, ax)) ax)) - lemmas + (omap (fun ax -> (ir, (p, ax))) ax) + ) lemmas in if not (List.is_empty lemmas) then begin Format.fprintf fmt "\n%!"; List.iter - (fun ax -> Format.fprintf fmt "%a\n\n%!" (pp_axiom ppe) ax) + (fun (ir, ax) -> + let ir = + match ir with + | `Default -> "" + | `Rigid -> " (rigid)" in + + Format.fprintf fmt "%a%s\n\n%!" (pp_axiom ppe) ax ir) lemmas end @@ -3526,11 +3541,11 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) = (* FIXME: section we should add the lemma in the reduction *) Format.fprintf fmt "hint simplify." - | EcTheory.Th_auto (lvl, base, p, lc) -> + | EcTheory.Th_auto { level; base; axioms; locality; } -> Format.fprintf fmt "%ahint solve %d %s : %a." - pp_locality lc - lvl (odfl "" base) - (pp_list "@ " (pp_axname ppe)) p + pp_locality locality + level (odfl "" base) + (pp_list "@ " (pp_axhnt ppe)) axioms (* -------------------------------------------------------------------- *) let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt = diff --git a/src/ecScope.ml b/src/ecScope.ml index 364e755252..ac291529da 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -796,8 +796,8 @@ module Auto = struct let item = EcTheory.mkitem EcTheory.import0 (Th_addrw (base, l, local)) in { scope with sc_env = EcSection.add_item item scope.sc_env } - let bind_hint scope ~local ~level ?base names = - let item = EcTheory.mkitem EcTheory.import0 (Th_auto (level, base, names, local)) in + let bind_hint scope ~local ~level ?base axioms = + let item = EcTheory.mkitem EcTheory.import0 (Th_auto { level; base; axioms; locality=local} ) in { scope with sc_env = EcSection.add_item item scope.sc_env } let add_hint scope hint = @@ -806,6 +806,8 @@ module Auto = struct let names = List.map (fun l -> EcEnv.Ax.lookup_path (unloc l) env) hint.ht_names in + let mode = if List.mem `Rigid hint.ht_options then `Rigid else `Default in + let names = List.map (fun p -> (p, mode)) names in bind_hint scope ~local:hint.ht_local ~level:hint.ht_prio ?base names end @@ -1287,7 +1289,9 @@ module Op = struct List.fold_left (fun scope base -> - Auto.bind_hint ~local:(local_of_locality lc) ~level:0 ~base scope [axpath]) + Auto.bind_hint + ~local:(local_of_locality lc) ~level:0 ~base scope + [(axpath, `Default)]) scope bases in diff --git a/src/ecSection.ml b/src/ecSection.ml index 127040f6b1..3c8257547c 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1016,12 +1016,16 @@ let generalize_addrw to_gen (p, ps, lc) = let generalize_reduction to_gen _rl = to_gen, None -let generalize_auto to_gen (n,s,ps,lc) = - if lc = `Local then to_gen, None +let generalize_auto to_gen auto_rl = + if auto_rl.locality = `Local then + to_gen, None else - let ps = List.filter (fun p -> to_keep to_gen (`Ax p)) ps in - if ps = [] then to_gen, None - else to_gen, Some (Th_auto (n,s,ps,lc)) + let axioms = + List.filter (fun (p, _) -> to_keep to_gen (`Ax p)) auto_rl.axioms in + if List.is_empty axioms then + to_gen, None + else + to_gen, Some (Th_auto {auto_rl with axioms}) (* --------------------------------------------------------------- *) let get_locality scenv = scenv.sc_loca @@ -1046,7 +1050,7 @@ let rec set_local_item item = | Th_baserw (s,lc) -> Th_baserw (s, set_local lc) | Th_addrw (p,ps,lc) -> Th_addrw (p, ps, set_local lc) | Th_reduction r -> Th_reduction r - | Th_auto (i,s,p,lc) -> Th_auto (i, s, p, set_local lc) + | Th_auto auto_rl -> Th_auto {auto_rl with locality=set_local auto_rl.locality} in { item with ti_item = lcitem } @@ -1337,19 +1341,20 @@ let add_item_ (item : theory_item) (scenv:scenv) = let env = scenv.sc_env in let env = match item.ti_item with - | Th_type (s,tyd) -> EcEnv.Ty.bind s tyd env - | Th_operator (s,op) -> EcEnv.Op.bind s op env - | Th_axiom (s, ax) -> EcEnv.Ax.bind s ax env - | Th_modtype (s, ms) -> EcEnv.ModTy.bind s ms env - | Th_module me -> EcEnv.Mod.bind me.tme_expr.me_name me env - | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind s tc env - | Th_export (p, lc) -> EcEnv.Theory.export p lc env + | Th_type (s,tyd) -> EcEnv.Ty.bind s tyd env + | Th_operator (s,op) -> EcEnv.Op.bind s op env + | Th_axiom (s, ax) -> EcEnv.Ax.bind s ax env + | Th_modtype (s, ms) -> EcEnv.ModTy.bind s ms env + | Th_module me -> EcEnv.Mod.bind me.tme_expr.me_name me env + | Th_typeclass(s,tc) -> EcEnv.TypeClass.bind s tc env + | Th_export (p, lc) -> EcEnv.Theory.export p lc env | Th_instance (tys,i,lc) -> EcEnv.TypeClass.add_instance tys i lc env - | Th_baserw (s,lc) -> EcEnv.BaseRw.add s lc env - | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env - | Th_auto (level, base, ps, lc) -> EcEnv.Auto.add ~level ?base ps lc env - | Th_reduction r -> EcEnv.Reduction.add r env - | _ -> assert false + | Th_baserw (s,lc) -> EcEnv.BaseRw.add s lc env + | Th_addrw (p,ps,lc) -> EcEnv.BaseRw.addto p ps lc env + | Th_auto auto -> EcEnv.Auto.add ~level:auto.level ?base:auto.base + auto.axioms auto.locality env + | Th_reduction r -> EcEnv.Reduction.add r env + | _ -> assert false in { scenv with sc_env = env; @@ -1493,8 +1498,8 @@ let check_item scenv item = | Th_addrw (_,_,lc) -> if (lc = `Local && not scenv.sc_insec) then hierror "local hint rewrite can only be declared inside section"; - | Th_auto (_, _, _, lc) -> - if (lc = `Local && not scenv.sc_insec) then + | Th_auto { locality } -> + if (locality = `Local && not scenv.sc_insec) then hierror "local hint can only be declared inside section"; | Th_reduction _ -> () | Th_theory _ -> assert false diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 977f7e3657..d1b24f4f6f 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -1075,8 +1075,9 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) = List.map (fun (p, opts, _) -> (subst_path s p, opts, None)) rules in Th_reduction rules - | Th_auto (lvl, base, ps, lc) -> - Th_auto (lvl, base, List.map (subst_path s) ps, lc) + | Th_auto ({ axioms } as auto_rl) -> + Th_auto { auto_rl with axioms = + List.map (fst_map (subst_path s)) axioms } (* -------------------------------------------------------------------- *) and subst_theory (s : subst) (items : theory) = diff --git a/src/ecTheory.ml b/src/ecTheory.ml index 0d39c8d21d..a329d9318d 100644 --- a/src/ecTheory.ml +++ b/src/ecTheory.ml @@ -37,7 +37,7 @@ and theory_item_r = | 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_auto of (int * symbol option * path list * is_local) + | Th_auto of auto_rule and thsource = { ths_base : EcPath.path; @@ -75,6 +75,13 @@ and rule_option = { ur_eqtrue : bool; } +and auto_rule = { + level : int; + base : symbol option; + axioms : (path * [`Rigid | `Default]) list; + locality : is_local; +} + let mkitem (import : import) (item : theory_item_r) = { ti_import = import; ti_item = item; } diff --git a/src/ecTheory.mli b/src/ecTheory.mli index 472928561f..fb63e85447 100644 --- a/src/ecTheory.mli +++ b/src/ecTheory.mli @@ -34,7 +34,7 @@ and theory_item_r = | 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_auto of (int * symbol option * path list * is_local) + | Th_auto of auto_rule and thsource = { ths_base : EcPath.path; @@ -72,6 +72,13 @@ and rule_option = { ur_eqtrue : bool; } +and auto_rule = { + level : int; + base : symbol option; + axioms : (path * [`Rigid | `Default]) list; + locality : is_local; +} + val mkitem : import -> theory_item_r -> theory_item (* -------------------------------------------------------------------- *) diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 227aaee341..0b122511bf 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -825,12 +825,12 @@ and replay_addrw (* -------------------------------------------------------------------- *) and replay_auto - (ove : _ ovrenv) (subst, ops, proofs, scope) (import, lvl, base, ps, lc) + (ove : _ ovrenv) (subst, ops, proofs, scope) (import, at_base) = let env = EcSection.env (ove.ovre_hooks.henv scope) in - let ps = List.map (EcSubst.subst_path subst) ps in - let ps = List.filter (fun p -> Option.is_some (EcEnv.Ax.by_path_opt p env)) ps in - let scope = ove.ovre_hooks.hadd_item scope import (Th_auto (lvl, base, ps, lc)) in + let axioms = List.map (fst_map (EcSubst.subst_path subst)) at_base.axioms in + let axioms = List.filter (fun (p, _) -> Option.is_some (EcEnv.Ax.by_path_opt p env)) axioms in + let scope = ove.ovre_hooks.hadd_item scope import (Th_auto { at_base with axioms }) in (subst, ops, proofs, scope) (* -------------------------------------------------------------------- *) @@ -981,8 +981,8 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item = | Th_reduction rules -> replay_reduction ove (subst, ops, proofs, scope) (item.ti_import, rules) - | Th_auto (lvl, base, ps, lc) -> - replay_auto ove (subst, ops, proofs, scope) (item.ti_import, lvl, base, ps, lc) + | Th_auto at_base -> + replay_auto ove (subst, ops, proofs, scope) (item.ti_import, at_base) | Th_typeclass (x, tc) -> replay_typeclass ove (subst, ops, proofs, scope) (item.ti_import, x, tc) diff --git a/tests/hint_rigid_should_fail_immediate.ec b/tests/hint_rigid_should_fail_immediate.ec new file mode 100644 index 0000000000..d89b977e66 --- /dev/null +++ b/tests/hint_rigid_should_fail_immediate.ec @@ -0,0 +1,15 @@ +(*-------------------------------------------------------------------- *) +require import AllCore List IntDiv. + +axiom iteri_red (n : int) (opr : int -> int -> int) (x : int) : + 0 < n => iteri n opr x = opr (n-1) (iteri (n-1) opr x). + +hint simplify iteri_red. + +(* BIG enough so that unfolding unfolding will be untrackable *) +axiom ge0_test: 0 < 2^100000000000000000000000000. + +hint [rigid] exact : ge0_test. + +lemma foo (l : int list) (x : int) : [x] = x :: l. +proof. fail by done. abort.