From addaf91cbaa07d9cd10f16d36122c0e9670e878f Mon Sep 17 00:00:00 2001
From: Gustavo Delerue <gxdelerue@proton.me>
Date: Thu, 9 Jan 2025 19:56:19 +0000
Subject: [PATCH] PR: Irreducible solve hints and print hint
This PR introduces two new features:
- Irreducible hints:
This features allows the introduction of the "irreducible" keyword
between "hint" and "exact" or "solve" (e.g. "hint irreducible exact") in
order to disable reduction of the hinted expression when auto-solving
goals.
- Print hint:
This introduces the following commands:
"print hint" - prints all hints in the current scope
"print hint simplify" - same but only for simplify hints
"print hint solve" - same but only for solve hints
"print hint rewrite" - same but only for rewrite hints
---
src/ecCommands.ml | 169 ++++++++++++----------
src/ecCorePrinting.ml | 6 +
src/ecEnv.ml | 75 +++++++---
src/ecEnv.mli | 16 +-
src/ecLexer.mll | 1 +
src/ecLowGoal.ml | 33 +++--
src/ecLowGoal.mli | 7 +-
src/ecMaps.ml | 41 ++++++
src/ecParser.mly | 27 +++-
src/ecParsetree.ml | 16 +-
src/ecPrinting.ml | 86 +++++++++--
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 | 21 +++
tests/hint_rigid_should_fail_timeout.ec | 21 +++
19 files changed, 438 insertions(+), 171 deletions(-)
create mode 100644 tests/hint_rigid_should_fail_immediate.ec
create mode 100644 tests/hint_rigid_should_fail_timeout.ec
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 6b0e8f4fad..264c99c28a 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -255,6 +255,83 @@ module HiPrinting = struct
fmt (goal, `One sz)
end
end
+
+ let pr_axioms (fmt : Format.formatter) (env : EcEnv.env) =
+ let ax = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env in
+ 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, 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 = (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
+
+ let pr_hint_rewrite (fmt : Format.formatter) (env : EcEnv.env) =
+ let hint_rewrite = EcEnv.BaseRw.all env in
+
+ let ppe = EcPrinting.PPEnv.ofenv env in
+
+ let pp_hint_rewrite _ppe fmt = (fun (p, sp) ->
+ let elems = EcPath.Sp.ntr_elements sp in
+ if List.is_empty elems then
+ Format.fprintf fmt "%s (empty)@." (EcPath.tostring p)
+ else
+ Format.fprintf fmt "%s = @.@[<b 2>%a@]@." (EcPath.tostring p)
+ (EcPrinting.pp_list "@." (fun fmt p ->
+ Format.fprintf fmt "%s" (EcPath.tostring p)))
+ (EcPath.Sp.ntr_elements sp)
+ )
+ in
+
+ EcPrinting.pp_by_theory ppe pp_hint_rewrite fmt hint_rewrite
+
+ 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 ppe = EcPrinting.PPEnv.ofenv env in
+
+ let pp_hint_simplify ppe fmt = (fun (p, (rls : rule list)) ->
+ Format.fprintf fmt "%s:@.@[<b 2>%a@]" (EcPath.tostring p)
+ (EcPrinting.pp_list "@." (fun fmt rl ->
+ Format.fprintf fmt "Conditions: %a@.Target: %a@.Pattern: %a@."
+ (EcPrinting.pp_list "," (EcPrinting.pp_form ppe)) rl.rl_cond
+ (EcPrinting.pp_form ppe) rl.rl_tg
+ (EcPrinting.pp_rule_pattern ppe) rl.rl_ptn
+ ))
+ rls
+ )
+ in
+
+ EcPrinting.pp_by_theory ppe pp_hint_simplify fmt hint_simplify
+
+ let pr_hints (fmt : Format.formatter) (env : EcEnv.env) =
+ let ax = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env in
+ let ppe0 = EcPrinting.PPEnv.ofenv env in
+ EcPrinting.pp_by_theory ppe0 (EcPrinting.pp_axiom) fmt ax
end
(* -------------------------------------------------------------------- *)
@@ -280,6 +357,23 @@ let process_pr fmt scope p =
| Pr_glob pm -> HiPrinting.pr_glob fmt env pm
| Pr_goal n -> HiPrinting.pr_goal fmt scope n
+ | Pr_axioms -> HiPrinting.pr_axioms fmt env
+
+ | Pr_hint (Some `Simplify) -> HiPrinting.pr_hint_simplify fmt env
+ | Pr_hint (Some `Solve) -> HiPrinting.pr_hint_solve fmt env
+ | Pr_hint (Some `Rewrite) -> HiPrinting.pr_hint_rewrite fmt env
+
+ | Pr_hint None ->
+ let printers = [
+ ("Solve" , (fun fmt -> HiPrinting.pr_hint_solve fmt env));
+ ("Simplify", (fun fmt -> HiPrinting.pr_hint_simplify fmt env));
+ ("Rewrite" , (fun fmt -> HiPrinting.pr_hint_rewrite fmt env));
+ ] in
+
+ List.iter (fun (header, printer) ->
+ Format.fprintf fmt "%s hints:@.%t@." header printer
+ ) printers
+
(* -------------------------------------------------------------------- *)
let check_opname_validity (scope : EcScope.scope) (x : string) =
if EcIo.is_binop x = `Invalid then
@@ -293,80 +387,6 @@ let check_opname_validity (scope : EcScope.scope) (x : string) =
let process_print scope p =
process_pr Format.std_formatter scope p
-(* -------------------------------------------------------------------- *)
-let process_print_ax (scope : EcScope.scope) =
- let env = EcScope.env scope in
- let ax = EcEnv.Ax.all ~check:(fun _ ax -> EcDecl.is_axiom ax.ax_kind) env in
-
- let module Trie : sig
- type ('a, 'b) t
-
- val empty : ('a, 'b) t
- val add : 'a list -> 'b -> ('a, 'b) t -> ('a, 'b) t
- val iter : ('a list -> 'b list -> unit) -> ('a, 'b) t -> unit
- end = struct
- module Map = BatMap
-
- type ('a, 'b) t =
- { children : ('a, ('a, 'b) t) Map.t
- ; value : 'b list }
-
- let empty : ('a, 'b) t =
- { value = []; children = Map.empty; }
-
- let add (path : 'a list) (value : 'b) (t : ('a, 'b) t) =
- let rec doit (path : 'a list) (t : ('a, 'b) t) =
- match path with
- | [] ->
- { t with value = value :: t.value }
- | v :: path ->
- let children =
- t.children |> Map.update_stdlib v (fun children ->
- let subtrie = Option.value ~default:empty children in
- Some (doit path subtrie)
- )
- in { t with children }
- in doit path t
-
- let iter (f : 'a list -> 'b list -> unit) (t : ('a, 'b) t) =
- let rec doit (prefix : 'a list) (t : ('a, 'b) t) =
- if not (List.is_empty t.value) then
- f prefix t.value;
- Map.iter (fun k v -> doit (k :: prefix) v) t.children
- in
-
- doit [] t
- end in
-
- let ax =
- List.fold_left (fun axs ((p, _) as ax) ->
- Trie.add (EcPath.tolist (oget (EcPath.prefix p))) ax axs
- ) Trie.empty ax in
-
- let ppe0 = EcPrinting.PPEnv.ofenv env in
- let buffer = Buffer.create 0 in
- let fmt = Format.formatter_of_buffer buffer in
-
- Trie.iter (fun prefix axs ->
- let thpath =
- match prefix with
- | [] -> assert false
- | name :: prefix -> (List.rev prefix, name) in
-
- let thpath = EcPath.fromqsymbol thpath in
-
- let ppe = EcPrinting.PPEnv.enter_theory ppe0 thpath in
-
- Format.fprintf fmt
- "@.========== %a ==========@.@." (EcPrinting.pp_thname ppe0) thpath;
-
- List.iter (fun ax ->
- Format.fprintf fmt "%a@." (EcPrinting.pp_axiom ppe) ax
- ) axs
- ) ax;
-
- EcScope.notify scope `Warning "%s" (Buffer.contents buffer)
-
(* -------------------------------------------------------------------- *)
exception Pragma of [`Reset | `Restart]
@@ -734,7 +754,6 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
| GsctOpen name -> `Fct (fun scope -> process_sct_open scope name)
| GsctClose name -> `Fct (fun scope -> process_sct_close scope name)
| Gprint p -> `Fct (fun scope -> process_print scope p; scope)
- | Gpaxiom -> `Fct (fun scope -> process_print_ax scope; scope)
| Gsearch qs -> `Fct (fun scope -> process_search scope qs; scope)
| Glocate x -> `Fct (fun scope -> process_locate scope x; scope)
| Gtactics t -> `Fct (fun scope -> process_tactics scope t)
diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml
index a8187a70e0..23948f1e92 100644
--- a/src/ecCorePrinting.ml
+++ b/src/ecCorePrinting.ml
@@ -98,6 +98,12 @@ module type PrinterAPI = sig
val pp_hyps : PPEnv.t -> EcEnv.LDecl.hyps pp
val pp_goal : PPEnv.t -> prpo_display -> ppgoal pp
+ (* ------------------------------------------------------------------ *)
+ val pp_by_theory : PPEnv.t -> (PPEnv.t -> (EcPath.path * 'a) pp) -> ((EcPath.path * 'a) list) pp
+
+ (* ------------------------------------------------------------------ *)
+ val pp_rule_pattern : PPEnv.t -> EcTheory.rule_pattern pp
+
(* ------------------------------------------------------------------ *)
module ObjectInfo : sig
type db = [`Rewrite of qsymbol | `Solve of symbol]
diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index 34662c4b04..bcb4593cb4 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
@@ -1444,6 +1448,13 @@ module BaseRw = struct
(omap (fun s -> List.fold_left (fun s r -> Sp.add r s) s l))
(IPPath p) env.env_rwbase;
env_item = mkitem import (Th_addrw (p, l, lc)) :: env.env_item; }
+
+ let all env =
+ List.filter_map (fun (ip, sp) ->
+ match ip with
+ | IPPath p -> Some (p, sp)
+ | _ -> None) @@
+ Mip.bindings env.env_rwbase
end
(* -------------------------------------------------------------------- *)
@@ -1496,45 +1507,65 @@ module Reduction = struct
Mrd.find_opt p env.env_redbase
|> omap (fun x -> Lazy.force x.ri_list)
|> odfl []
+
+ (* FIXME: handle other cases, right now only used for print hint *)
+ let all (env : env) =
+ List.map (fun (ts, mr) ->
+ (ts, Lazy.force mr.ri_list))
+ (Mrd.bindings env.env_redbase)
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 =
+ let dbs =
List.fold_left (fun db mi ->
Mint.union (fun _ sp1 sp2 -> Some (sp1 @ sp2)) db mi)
Mint.empty dbs
@@ -1543,6 +1574,9 @@ module Auto = struct
let getx (base : symbol) (env : env) =
let db = Msym.find_def Mint.empty base env.env_atbase in
Mint.bindings db
+
+ let all (env : env) : atbase0 list =
+ Msym.values env.env_atbase |> List.map flatten_db |> List.flatten
end
(* -------------------------------------------------------------------- *)
@@ -2932,8 +2966,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
@@ -3106,9 +3140,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 0e8712174a..c3dad555ab 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -398,6 +398,8 @@ module BaseRw : sig
val add : ?import:import -> symbol -> is_local -> env -> env
val addto : ?import:import -> path -> path list -> is_local -> env -> env
+
+ val all : env -> (path * Sp.t) list
end
(* -------------------------------------------------------------------- *)
@@ -405,6 +407,7 @@ module Reduction : sig
type rule = EcTheory.rule
type topsym = [ `Path of path | `Tuple | `Proj of int]
+ val all : env -> (topsym * rule list) list
val add1 : path * rule_option * rule option -> env -> env
val add : ?import:import -> (path * rule_option * rule option) list -> env -> env
val get : topsym -> env -> rule list
@@ -412,12 +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 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/ecLexer.mll b/src/ecLexer.mll
index c1225b0720..b977371a04 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -183,6 +183,7 @@
"local" , LOCAL ; (* KW: global *)
"declare" , DECLARE ; (* KW: global *)
"hint" , HINT ; (* KW: global *)
+ "rigid" , RIGID ; (* KW: global *)
"module" , MODULE ; (* KW: global *)
"of" , OF ; (* KW: global *)
"const" , CONST ; (* KW: global *)
diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
index 003bf07a9a..3c6cf8cf8d 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
@@ -2506,22 +2506,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 093f144240..b9107b8dca 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/ecMaps.ml b/src/ecMaps.ml
index b06579abcc..61609a19d1 100644
--- a/src/ecMaps.ml
+++ b/src/ecMaps.ml
@@ -148,3 +148,44 @@ module Hdint = EHashtbl.Make(DInt)
(* --------------------------------------------------------------------*)
module Mstr = Map.Make(String)
module Sstr = Set.MakeOfMap(Mstr)
+
+(* --------------------------------------------------------------------*)
+module Trie : sig
+ type ('a, 'b) t
+
+ val empty : ('a, 'b) t
+ val add : 'a list -> 'b -> ('a, 'b) t -> ('a, 'b) t
+ val iter : ('a list -> 'b list -> unit) -> ('a, 'b) t -> unit
+end = struct
+ module Map = BatMap
+
+ type ('a, 'b) t =
+ { children : ('a, ('a, 'b) t) Map.t
+ ; value : 'b list }
+
+ let empty : ('a, 'b) t =
+ { value = []; children = Map.empty; }
+
+ let add (path : 'a list) (value : 'b) (t : ('a, 'b) t) =
+ let rec doit (path : 'a list) (t : ('a, 'b) t) =
+ match path with
+ | [] ->
+ { t with value = value :: t.value }
+ | v :: path ->
+ let children =
+ t.children |> Map.update_stdlib v (fun children ->
+ let subtrie = Option.value ~default:empty children in
+ Some (doit path subtrie)
+ )
+ in { t with children }
+ in doit path t
+
+ let iter (f : 'a list -> 'b list -> unit) (t : ('a, 'b) t) =
+ let rec doit (prefix : 'a list) (t : ('a, 'b) t) =
+ if not (List.is_empty t.value) then
+ f prefix t.value;
+ Map.iter (fun k v -> doit (k :: prefix) v) t.children
+ in
+
+ doit [] t
+end
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 71dfbc9b26..6837b7578c 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -546,6 +546,7 @@
%token RETURN
%token REWRITE
%token RIGHT
+%token RIGID
%token RND
%token RNDSEM
%token RPAREN
@@ -3747,6 +3748,11 @@ realize:
(* -------------------------------------------------------------------- *)
(* Printing *)
+phint:
+| SIMPLIFY { `Simplify }
+| SOLVE { `Solve }
+| REWRITE { `Rewrite }
+
print:
| qs=qoident { Pr_any qs }
| STAR qs=qoident { Pr_any qs }
@@ -3762,10 +3768,12 @@ print:
| GOAL n=sword { Pr_goal n }
| REWRITE qs=qident { Pr_db (`Rewrite qs) }
| SOLVE qs=ident { Pr_db (`Solve qs) }
+| AXIOM { Pr_axioms }
+| HINT p=phint? { Pr_hint p }
coq_info:
| { None }
-| CHECK { Some EcProvers.Check }
+| CHECK { Some EcProvers.Check }
| EDIT { Some EcProvers.Edit }
| FIX { Some EcProvers.Fix }
@@ -3817,14 +3825,22 @@ addrw:
| local=is_local HINT REWRITE p=lqident COLON l=lqident*
{ (local, p, l) }
+hintoption:
+| RIGID { (true, `Rigid) }
+
+%inline hintoptions:
+| xs=bracket(hintoption+) { xs }
+
hint:
-| local=is_local HINT EXACT base=lident? COLON l=qident*
+| local=is_local HINT opts=ioption(hintoptions) EXACT base=lident? COLON l=qident*
{ { ht_local = local; ht_prio = 0;
- ht_base = base ; ht_names = l; } }
+ ht_base = base ; ht_names = l;
+ ht_options = odfl [] opts; } }
-| local=is_local HINT SOLVE i=word base=lident? COLON l=qident*
+| local=is_local HINT opts=ioption(hintoptions) SOLVE i=word base=lident? COLON l=qident*
{ { ht_local = local; ht_prio = i;
- ht_base = base ; ht_names = l; } }
+ ht_base = base ; ht_names = l;
+ ht_options = odfl [] opts; } }
(* -------------------------------------------------------------------- *)
(* User reduction *)
@@ -3887,7 +3903,6 @@ global_action:
| hint { Ghint $1 }
| x=loc(proofend) { Gsave x }
| PRINT p=print { Gprint p }
-| PRINT AXIOM { Gpaxiom }
| SEARCH x=search+ { Gsearch x }
| LOCATE x=qident { Glocate x }
| WHY3 x=STRING { GdumpWhy3 x }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 53eda26b84..43cd31a144 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1122,6 +1122,8 @@ type pprint =
| Pr_glob of pmsymbol located
| Pr_goal of int
| Pr_db of [`Rewrite of pqsymbol | `Solve of psymbol]
+ | Pr_axioms
+ | Pr_hint of [`Simplify | `Rewrite | `Solve] option
(* -------------------------------------------------------------------- *)
type renaming_kind =
@@ -1228,12 +1230,17 @@ type save = [ `Qed | `Admit | `Abort ]
(* -------------------------------------------------------------------- *)
type theory_clear = (pqsymbol option) list
+(* -------------------------------------------------------------------- *)
+type phintoption = [ `Rigid ]
+type phintoptions = (bool * phintoption) list
+
(* -------------------------------------------------------------------- *)
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 : phintoptions;
}
(* -------------------------------------------------------------------- *)
@@ -1263,7 +1270,6 @@ type global_action =
| Greduction of puserred
| Ghint of phint
| Gprint of pprint
- | Gpaxiom
| Gsearch of pformula list
| Glocate of pqsymbol
| GthOpen of (is_local * bool * psymbol)
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index 9b5232c5b7..d4f98ea4a9 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -476,6 +476,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)
@@ -2890,23 +2897,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
@@ -3391,11 +3406,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 =
@@ -3407,6 +3422,57 @@ let pp_stmt_with_nums (ppe : PPEnv.t) fmt stmt =
let pp_stmt ?(lineno = false) =
if lineno then pp_stmt_with_nums else pp_stmt
+(* -------------------------------------------------------------------- *)
+let pp_by_theory
+ (ppe0 : PPEnv.t)
+ (pp : PPEnv.t -> (EcPath.path * 'a) pp)
+ (fmt : Format.formatter)
+ (xs : (EcPath.path * 'a) list)
+=
+ let tr =
+ List.fold_left (fun tr ((p, _) as x) ->
+ Trie.add (EcPath.tolist (oget (EcPath.prefix p))) x tr
+ ) Trie.empty xs
+ in
+
+ Trie.iter (fun prefix xs ->
+ let thpath =
+ match prefix with
+ | [] -> assert false
+ | name :: prefix -> (List.rev prefix, name) in
+
+ let thpath = EcPath.fromqsymbol thpath in
+
+ let ppe = PPEnv.enter_theory ppe0 thpath in
+
+ Format.fprintf fmt
+ "@.========== %a ==========@.@." (pp_thname ppe0) thpath;
+
+ List.iter (fun x ->
+ Format.fprintf fmt "%a@." (pp ppe) x
+ ) xs
+ ) tr
+
+let rec pp_rule_pattern ppe fmt (rl_pt: EcTheory.rule_pattern) =
+ match rl_pt with
+ | Rule (trp, rp_list) -> pp_rule ppe fmt trp rp_list
+ | Int z -> Format.fprintf fmt "%s" (EcBigInt.to_string z)
+ | Var v -> Format.fprintf fmt "%s" (EcIdent.name v)
+
+and pp_rule_patterns ppe fmt (rl_pts: EcTheory.rule_pattern list) =
+ match rl_pts with
+ | [] -> ()
+ | rl_pts -> Format.fprintf fmt "(%a)" (pp_list "," (pp_rule_pattern ppe)) rl_pts
+
+and pp_rule ppe fmt trp rl_pts =
+ match trp with
+ | `Tuple -> Format.fprintf fmt "tuple%a" (pp_rule_patterns ppe) rl_pts
+ | `Op (p, _) -> Format.fprintf fmt "%a%a" (pp_opname ppe) p (pp_rule_patterns ppe) rl_pts
+ | `Proj i -> if List.is_empty rl_pts then () else
+ Format.fprintf fmt "%a`%d" (pp_rule_patterns ppe) rl_pts i
+
+
+
(* -------------------------------------------------------------------- *)
module ObjectInfo = struct
exception NoObject
diff --git a/src/ecScope.ml b/src/ecScope.ml
index b17295a4d5..ac3ce3439d 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 (true, `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..a00d6a3178
--- /dev/null
+++ b/tests/hint_rigid_should_fail_immediate.ec
@@ -0,0 +1,21 @@
+require import AllCore List IntDiv.
+
+lemma iteri_red n (opr: int -> 'a -> 'a) x :
+ 0 < n => iteri n opr x = opr (n-1) (iteri (n-1) opr x).
+ proof.
+ smt (iteriS).
+ qed.
+
+hint simplify iteri_red.
+
+lemma ge0_test: 0 < 2^512.
+ proof. by auto. qed.
+
+hint [rigid] exact : ge0_test.
+
+timeout 1.
+
+lemma foo (l : int list) (x : int) :
+ [x] = x :: l.
+by done.
+
diff --git a/tests/hint_rigid_should_fail_timeout.ec b/tests/hint_rigid_should_fail_timeout.ec
new file mode 100644
index 0000000000..d97cdb9dfa
--- /dev/null
+++ b/tests/hint_rigid_should_fail_timeout.ec
@@ -0,0 +1,21 @@
+require import AllCore List IntDiv.
+
+lemma iteri_red n (opr: int -> 'a -> 'a) x :
+ 0 < n => iteri n opr x = opr (n-1) (iteri (n-1) opr x).
+ proof.
+ smt (iteriS).
+ qed.
+
+hint simplify iteri_red.
+
+lemma ge0_test: 0 < 2^512.
+ proof. by auto. qed.
+
+hint exact : ge0_test.
+
+timeout 1.
+
+lemma foo (l : int list) (x : int) :
+ [x] = x :: l.
+by done.
+