Skip to content

Commit

Permalink
Better printing of hint DBs
Browse files Browse the repository at this point in the history 
This commit introduces the following printing 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

Co-Authored-By: Gustavo Delerue <[email protected]>
Co-Authored-By: Pierre-Yves Strub <[email protected]>
  • Loading branch information
@Gustavo2622 @strub
Gustavo2622 and strub committed Jan 16, 2025
1 parent 2194cd8 commit d84e76f
Show file tree
Hide file tree
Showing 8 changed files with 222 additions and 80 deletions.
164 changes: 89 additions & 75 deletions src/ecCommands.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,7 @@ let process_locate scope x =

(* -------------------------------------------------------------------- *)
module HiPrinting = struct
(* ------------------------------------------------------------------ *)
let pr_glob fmt env pm =
let ppe = EcPrinting.PPEnv.ofenv env in
let (p, _) = EcTyping.trans_msymbol env pm in
Expand All @@ -226,6 +227,7 @@ module HiPrinting = struct
pv


(* ------------------------------------------------------------------ *)
let pr_goal fmt scope n =
match EcScope.xgoal scope with
| None | Some { EcScope.puc_active = None} ->
Expand Down Expand Up @@ -255,6 +257,76 @@ 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 ->
(p, EcEnv.Ax.by_path p env)
) 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
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: %[email protected]: %[email protected]: %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
end

(* -------------------------------------------------------------------- *)
Expand All @@ -280,6 +352,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
Expand All @@ -293,80 +382,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]

Expand Down Expand Up @@ -734,7 +749,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)
Expand Down
6 changes: 6 additions & 0 deletions src/ecCorePrinting.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
18 changes: 17 additions & 1 deletion src/ecEnv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1447,6 +1447,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
(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1499,6 +1506,12 @@ 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
(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1537,7 +1550,7 @@ module Auto = struct
let getall (bases : symbol list) (env : env) =
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
Expand All @@ -1546,6 +1559,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) : path list =
Msym.values env.env_atbase |> List.map flatten_db |> List.flatten
end
(* -------------------------------------------------------------------- *)
Expand Down
6 changes: 5 additions & 1 deletion src/ecEnv.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -398,13 +398,16 @@ 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

(* -------------------------------------------------------------------- *)
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
Expand All @@ -417,7 +420,8 @@ module Auto : sig
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 getx : symbol -> env -> (int * path list) list
val all : env -> path list
end

(* -------------------------------------------------------------------- *)
Expand Down
41 changes: 41 additions & 0 deletions src/ecMaps.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
10 changes: 8 additions & 2 deletions src/ecParser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3622,6 +3622,11 @@ realize:

(* -------------------------------------------------------------------- *)
(* Printing *)
phint:
| SIMPLIFY { `Simplify }
| SOLVE { `Solve }
| REWRITE { `Rewrite }

print:
| qs=qoident { Pr_any qs }
| STAR qs=qoident { Pr_any qs }
Expand All @@ -3637,10 +3642,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 }

Expand Down Expand Up @@ -3762,7 +3769,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 }
Expand Down
3 changes: 2 additions & 1 deletion src/ecParsetree.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1120,6 +1120,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 =
Expand Down Expand Up @@ -1261,7 +1263,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)
Expand Down
Loading

0 comments on commit d84e76f

Please sign in to comment.