diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 6b0e8f4fa..9b08572c9 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -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 @@ -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} -> @@ -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 = @.@[%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:@.@[%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 end (* -------------------------------------------------------------------- *) @@ -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 @@ -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] @@ -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) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index a8187a70e..23948f1e9 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 0bf97288d..a870a017f 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -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 (* -------------------------------------------------------------------- *) @@ -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 (* -------------------------------------------------------------------- *) @@ -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 @@ -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 (* -------------------------------------------------------------------- *) diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 95ae7910c..4bee0ef82 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 @@ -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 (* -------------------------------------------------------------------- *) diff --git a/src/ecMaps.ml b/src/ecMaps.ml index b06579abc..61609a19d 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 9f72e6abf..708ee96d6 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -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 } @@ -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 } @@ -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 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 67eba5e11..89039ad25 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -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 = @@ -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) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index afec71e62..e9e5f0651 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -3519,6 +3519,60 @@ 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 : PPEnv.t) + (fmt : Format.formatter) + (rule : EcTheory.rule_pattern) += + match rule with + | Rule (`Tuple, args) -> + Format.fprintf fmt "(%a)" (pp_list ",@ " (pp_rule_pattern ppe)) args + | Rule (`Op (p, _), []) -> + Format.fprintf fmt "%a" (pp_opname ppe) p + | Rule (`Op (p, _), args) -> + Format.fprintf fmt "%a@ %a" (pp_opname ppe) p + (pp_list "@ " (pp_paren (pp_rule_pattern ppe))) args + | Rule (`Proj i, [arg]) -> + Format.fprintf fmt "(%a)`.%d" (pp_rule_pattern ppe) arg i + | Rule (`Proj _, _) -> + assert false + | Int z -> + Format.fprintf fmt "%s" (EcBigInt.to_string z) + | Var v -> + Format.fprintf fmt "%s" (EcIdent.name v) + (* -------------------------------------------------------------------- *) module ObjectInfo = struct exception NoObject