diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 3e08fb640..1260919e2 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -393,11 +393,14 @@ let process_pr fmt scope p = let env = EcScope.env scope in match p with - | Pr_ty qs -> EcPrinting.ObjectInfo.pr_ty fmt env (unloc qs) - | Pr_op qs -> EcPrinting.ObjectInfo.pr_op fmt env (unloc qs) - | Pr_pr qs -> EcPrinting.ObjectInfo.pr_op fmt env (unloc qs) + (* [~locate] prefixes each printed object with the name `locate' reports + for it, so that a lookup that had homonyms to choose from says which + one each declaration is. *) + | Pr_ty qs -> EcPrinting.ObjectInfo.pr_ty ~locate:true fmt env (unloc qs) + | Pr_op qs -> EcPrinting.ObjectInfo.pr_op ~locate:true fmt env (unloc qs) + | Pr_pr qs -> EcPrinting.ObjectInfo.pr_op ~locate:true fmt env (unloc qs) | Pr_th qs -> EcPrinting.ObjectInfo.pr_th fmt env (unloc qs) - | Pr_ax qs -> EcPrinting.ObjectInfo.pr_ax fmt env (unloc qs) + | Pr_ax qs -> EcPrinting.ObjectInfo.pr_ax ~locate:true fmt env (unloc qs) | Pr_mod qs -> EcPrinting.ObjectInfo.pr_mod fmt env (unloc qs) | Pr_proc qs -> EcPrinting.ObjectInfo.pr_fun fmt env (unloc qs) | Pr_mty qs -> EcPrinting.ObjectInfo.pr_mty fmt env (unloc qs) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index c576efca1..530734805 100644 --- a/src/ecCorePrinting.ml +++ b/src/ecCorePrinting.ml @@ -43,6 +43,9 @@ module type PrinterAPI = sig val pp_list : ?on_empty:unit pp -> ('a, 'b, 'c, 'd, 'd, 'a) format6 -> 'a pp -> 'a list pp (* ------------------------------------------------------------------ *) + (* an operator name, with the parentheses that make it valid syntax *) + val pp_opqsymbol : qsymbol pp + val pp_pv : PPEnv.t -> prog_var pp val pp_local : ?fv:Sid.t -> PPEnv.t -> ident pp val pp_opname : PPEnv.t -> path pp @@ -67,6 +70,16 @@ module type PrinterAPI = sig val pp_shorten_path : PPEnv.t -> (path -> qsymbol -> bool) -> path pp + (* [pp_locate_path ?pp_name ppe lookup] says where an object lives: the + name it is known under, plus the shortest form that [lookup] still + resolves to it. [pp_name] is how the category at hand spells a name -- + [pp_opqsymbol] for an operator, the default for a type or a lemma. *) + val pp_locate_path : + ?pp_name:qsymbol pp + -> PPEnv.t + -> (qsymbol -> EcEnv.env -> (path * 'a) option) + -> path pp + (* ------------------------------------------------------------------ *) val pp_codepos1 : PPEnv.t -> EcMatching.Position.codepos1 pp val pp_codepos_brsel : EcMatching.Position.codepos_brsel pp @@ -131,10 +144,12 @@ module type PrinterAPI = sig module ObjectInfo : sig type db = [`Rewrite of qsymbol | `Solve of symbol] - val pr_ty : Format.formatter -> EcEnv.env -> qsymbol -> unit - val pr_op : Format.formatter -> EcEnv.env -> qsymbol -> unit + (* [locate:true] prefixes each printed object with the name + [pp_locate_path] reports for it. *) + val pr_ty : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit + val pr_op : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit val pr_th : Format.formatter -> EcEnv.env -> qsymbol -> unit - val pr_ax : Format.formatter -> EcEnv.env -> qsymbol -> unit + val pr_ax : ?locate:bool -> Format.formatter -> EcEnv.env -> qsymbol -> unit val pr_mod : Format.formatter -> EcEnv.env -> qsymbol -> unit val pr_fun : Format.formatter -> EcEnv.env -> qsymbol -> unit val pr_mty : Format.formatter -> EcEnv.env -> qsymbol -> unit diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 3fd831673..00c937d34 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -506,6 +506,23 @@ let pp_path fmt p = let pp_xpath fmt (xp: P.xpath) = Format.fprintf fmt "%s" (P.x_tostring xp) +(* -------------------------------------------------------------------- *) +(* [pp_name] is how the category at hand spells a name: an operator needs + its parentheses back ([pp_opqsymbol]) to be valid syntax again, whereas + a type or a lemma is spelled as it stands. *) +let pp_shortened + ?(pp_name : qsymbol pp = EcSymbols.pp_qsymbol) + (fmt : Format.formatter) + ((plong, pshort) : qsymbol * qsymbol option) += + match pshort with + | None -> + Format.fprintf fmt "%a" pp_name plong + | Some pshort -> + Format.fprintf fmt "%a (shorten name: %a)" + pp_name plong + pp_name pshort + (* -------------------------------------------------------------------- *) let pp_shorten_path (ppe : PPEnv.t) @@ -513,15 +530,35 @@ let pp_shorten_path (fmt : Format.formatter) (p : P.path) = - let plong, pshort = shorten_path ppe cond p in + pp_shortened fmt (shorten_path ppe cond p) - match pshort with - | None -> - Format.fprintf fmt "%a" EcSymbols.pp_qsymbol plong - | Some pshort -> - Format.fprintf fmt "%a (shorten name: %a)" - EcSymbols.pp_qsymbol plong - EcSymbols.pp_qsymbol pshort +(* -------------------------------------------------------------------- *) +(* An object is reachable under a name exactly when looking that name up + resolves back to it -- which is the condition [shorten_path] wants. *) +let locate_path + (ppe : PPEnv.t) + (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option) + (p : P.path) + : qsymbol * qsymbol option += + let cond (p : P.path) (qs : qsymbol) = + match lookup qs ppe.PPEnv.ppe_env with + | Some (p', _) -> P.p_equal p p' + | None -> false + in shorten_path ppe cond p + +(* [pp_locate_path] says where an object lives: the name it is known under, + plus the shortest form that still resolves to it. This is the report the + `locate' command lists, and the one `print' prefixes each of the objects + it displays with. *) +let pp_locate_path + ?(pp_name : qsymbol pp = EcSymbols.pp_qsymbol) + (ppe : PPEnv.t) + (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option) + (fmt : Format.formatter) + (p : P.path) += + pp_shortened ~pp_name fmt (locate_path ppe lookup p) (* -------------------------------------------------------------------- *) let rec pp_msymbol (fmt : Format.formatter) (mx : msymbol) = @@ -929,6 +966,10 @@ let pp_opname (fmt : Format.formatter) ((nm, op) : symbol list * symbol) = in EcSymbols.pp_qsymbol fmt (nm, op) +(* [pp_opname] under a name the path-level [pp_opname] defined below does + not shadow. *) +let pp_opqsymbol : qsymbol pp = pp_opname + (* -------------------------------------------------------------------- *) let pp_opname_with_tvi (ppe : PPEnv.t) @@ -4039,6 +4080,30 @@ module ObjectInfo = struct od_printer : PPEnv.t -> Format.formatter -> 'a -> unit; } + (* ------------------------------------------------------------------ *) + (* With [locate], an object is prefixed by the name [locate] reports for + it: the one it is known under, and the shortest form that still + resolves to it. A name with no namespace prefix says nothing the + declaration does not, and is left out -- the same convention as the + [~long] flag of the declaration printers, which the report + supersedes. *) + let pp_located + ?(locate = false) + ?pp_name + (lookup : qsymbol -> EcEnv.env -> (P.path * 'a) option) + (pp : PPEnv.t -> (P.path * 'a) pp) + (ppe : PPEnv.t) + (fmt : Format.formatter) + ((p, _) as obj : P.path * 'a) + = + if locate then begin + match locate_path ppe lookup p with + | (([], _), None) -> () + | located -> + Format.fprintf fmt "(* %a *)@ " (pp_shortened ?pp_name) located + end; + pp ppe fmt obj + (* -------------------------------------------------------------------- *) let pr_gen_r ?(prcat = false) dumper = fun fmt env qs -> let ppe = PPEnv.ofenv env in @@ -4058,30 +4123,35 @@ module ObjectInfo = struct theprinter fmt env qs with NoObject -> Format.fprintf fmt - "no such object in the category [%s]@." dumper.od_name + "no object `%a' in the category [%s]@\n@." + EcSymbols.pp_qsymbol qs dumper.od_name (* ------------------------------------------------------------------ *) - let pr_ty_r = + let pr_ty_r ?locate () = { od_name = "type declarations"; od_lookup = EcEnv.Ty.lookup; - od_printer = pp_typedecl; } + od_printer = pp_located ?locate EcEnv.Ty.lookup_opt pp_typedecl; } - let pr_ty = pr_gen pr_ty_r + let pr_ty ?locate fmt env qs = pr_gen (pr_ty_r ?locate ()) fmt env qs (* ------------------------------------------------------------------ *) - let pr_op_r = + let pr_op_r ?(locate = false) () = let get_ops qs env = let l = EcEnv.Op.all ~name:qs env in if l = [] then raise NoObject; l in + let pp_one = + pp_located ~locate ~pp_name:pp_opqsymbol EcEnv.Op.lookup_opt + (pp_opdecl ~long:(not locate)) in { od_name = "operators, predicates or exceptions"; od_lookup = get_ops; od_printer = fun ppe fmt l -> + (* an annotated object spans two lines: keep the entries apart *) Format.fprintf fmt "@[%a@]" - (pp_list "@ " (pp_opdecl ~long:true ppe)) l; } + (pp_list (if locate then "@ @ " else "@ ") (pp_one ppe)) l; } - let pr_op = pr_gen pr_op_r + let pr_op ?locate fmt env qs = pr_gen (pr_op_r ?locate ()) fmt env qs (* ------------------------------------------------------------------ *) let pr_th_r = @@ -4092,19 +4162,23 @@ module ObjectInfo = struct let pr_th = pr_gen pr_th_r (* ------------------------------------------------------------------ *) - let pr_ax_r = + let pr_ax_r ?(locate = false) () = let get_ops qs env = let l = EcEnv.Ax.all ~name:qs env in if l = [] then raise NoObject; l in + let pp_one = + pp_located ~locate EcEnv.Ax.lookup_opt + (pp_axiom ~long:(not locate)) in { od_name = "lemmas or axioms"; od_lookup = get_ops; od_printer = fun ppe fmt l -> + (* an annotated object spans two lines: keep the entries apart *) Format.fprintf fmt "@[%a@]" - (pp_list "@ " (pp_axiom ~long:true ppe)) l; } + (pp_list (if locate then "@ @ " else "@ ") (pp_one ppe)) l; } - let pr_ax = pr_gen pr_ax_r + let pr_ax ?locate fmt env qs = pr_gen (pr_ax_r ?locate ()) fmt env qs (* ------------------------------------------------------------------ *) let pr_mod_r = @@ -4179,10 +4253,10 @@ module ObjectInfo = struct (* ------------------------------------------------------------------ *) let pr_any fmt env qs = - let printers = [pr_gen_r ~prcat:true pr_ty_r ; - pr_gen_r ~prcat:true pr_op_r ; + let printers = [pr_gen_r ~prcat:true (pr_ty_r ~locate:true ()); + pr_gen_r ~prcat:true (pr_op_r ~locate:true ()); pr_gen_r ~prcat:true pr_th_r ; - pr_gen_r ~prcat:true pr_ax_r ; + pr_gen_r ~prcat:true (pr_ax_r ~locate:true ()); pr_gen_r ~prcat:true pr_mod_r; pr_gen_r ~prcat:true pr_fun_r; pr_gen_r ~prcat:true pr_mty_r; @@ -4195,7 +4269,8 @@ module ObjectInfo = struct (fun f -> try f fmt env qs with NoObject -> decr ok) printers; if !ok = 0 then - Format.fprintf fmt "%s@." "no such object in any category" + Format.fprintf fmt "no object `%a' in any category@\n@." + EcSymbols.pp_qsymbol qs end (* ------------------------------------------------------------------ *) diff --git a/src/ecScope.ml b/src/ecScope.ml index 8f0e27f87..316d0a827 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -3327,46 +3327,33 @@ module Search = struct let locate (scope : scope) ({ pl_desc = name } : pqsymbol) = let ppe = EcPrinting.PPEnv.ofenv (env scope) in - let shorten lk p = - let lk (p : path) (qs : qsymbol) = - match lk qs (env scope) with - | Some (p', _) -> p_equal p p' - | _ -> false in - EcPrinting.shorten_path ppe lk p - in - let buffer = Buffer.create 0 in let fmt = Format.formatter_of_buffer buffer in - let for_kind section getall shorten = + let for_kind ?pp_name section getall lookup = let objs = getall ?check:None ?name:(Some name) (env scope) in - let objs = List.map shorten (List.fst objs) in if not (List.is_empty objs) then begin Format.fprintf fmt "In section [%s]@\n@\n" section; - List.iter (fun (long, short) -> - match short with - | None -> - Format.fprintf fmt " - %a@\n" - EcSymbols.pp_qsymbol long - | Some short -> - Format.fprintf fmt " - %a (shorten name: %a)@\n" - EcSymbols.pp_qsymbol long - EcSymbols.pp_qsymbol short - ) objs + List.iter (fun p -> + Format.fprintf fmt " - %a@\n" + (EcPrinting.pp_locate_path ?pp_name ppe lookup) p + ) (List.fst objs) end in - for_kind "operators" EcEnv.Op.all (shorten EcEnv.Op.lookup_opt); - for_kind "types" EcEnv.Ty.all (shorten EcEnv.Ty.lookup_opt); - for_kind "lemmas" EcEnv.Ax.all (shorten EcEnv.Ax.lookup_opt); + for_kind "operators" EcEnv.Op.all EcEnv.Op.lookup_opt + ~pp_name:EcPrinting.pp_opqsymbol; + for_kind "types" EcEnv.Ty.all EcEnv.Ty.lookup_opt; + for_kind "lemmas" EcEnv.Ax.all EcEnv.Ax.lookup_opt; Format.pp_print_flush fmt (); if Buffer.length buffer = 0 then begin Format.fprintf fmt "no objects found for `%a'" - EcSymbols.pp_qsymbol name + EcSymbols.pp_qsymbol name; + Format.pp_print_flush fmt () end; notify scope `Info "%s" (Buffer.contents buffer) diff --git a/tests/clone-type-inline.ec b/tests/clone-type-inline.ec index a814e36d4..a524e46e5 100644 --- a/tests/clone-type-inline.ec +++ b/tests/clone-type-inline.ec @@ -31,8 +31,11 @@ clone BV as L with type t = int. (* L.t is a plain alias *) clone import Use as UK with theory P <= K. clone import Use as UL with theory P <= L. -(* UK.P.t receives K.t's *body* (K.t is clinline): prints `int`. *) -expect "type t = int." by print type UK.P.t. +(* UK.P.t receives K.t's *body* (K.t is clinline): prints `int`. The + leading comment is the `locate' report `print' prefixes objects with. *) +expect "(* UK.P.t *) +type t = int." by print type UK.P.t. (* UL.P.t keeps the reference to L.t (L.t is a plain alias): prints `L.t`. *) -expect "type t = L.t." by print type UL.P.t. +expect "(* UL.P.t *) +type t = L.t." by print type UL.P.t. diff --git a/tests/print-locate.ec b/tests/print-locate.ec new file mode 100644 index 000000000..9fc6849ae --- /dev/null +++ b/tests/print-locate.ec @@ -0,0 +1,86 @@ +(* Unit tests for the `locate' report that `print' prefixes each object it + displays with. Uses the `expect "..." by print ...' command + (String.trim-based comparison). *) + +require import Int. + +theory A. + op c : int = 1. + + lemma cP : c = 1 by done. +end A. + +theory B. + op c : int = 2. + + lemma cP : c = 2 by done. +end B. + +import A B. + +(* the name the object is known under, plus the shortest form that still + resolves to it *) +expect "(* Int.max (shorten name: max) *) +op max (a b : int) : int = if a < b then b else a." by print op Int.max. + +(* a symbolic operator gets its parentheses back, so that the reported name + is valid syntax again -- `Int.+' does not parse, `Int.(+)' does *) +expect "(* Int.(+) (shorten name: (+)) *) +abbrev (+) : int -> int -> int = CoreInt.add." by print op (+). + +(* a prefix operator keeps its brackets, and takes the parentheses only + under a namespace -- both forms parse *) +expect "(* Int.([-]) (shorten name: [-]) *) +abbrev [-] : int -> int = CoreInt.opp." by print op Int.([-]). + +(* every homonym gets its own report, right before its declaration -- only + the one `c' resolves to has a shortest form *) +expect "(* B.c (shorten name: c) *) +op c : int = 2. + +(* A.c *) +op c : int = 1." by print op c. + +(* same for lemmas *) +expect "(* B.cP (shorten name: cP) *) +lemma cP: B.c = 2. + +(* A.cP *) +lemma cP: A.c = 1." by print lemma cP. + +(* a name with no namespace prefix says nothing the declaration does not, + so it gets no report *) +op standalone : int = 0. + +expect "op standalone : int = 0." by print op standalone. + +(* the untyped `print x' searches every category, and reports in each one + that answered *) +theory Q. + type v = int. + op v : int = 0. +end Q. + +expect "* In [type declarations]: + +(* Q.v *) +type v = int. + +* In [operators, predicates or exceptions]: + +(* Q.v *) +op v : int = 0." by print Q.v. + +(* [locate] knows nothing about modules or procedures: printing one of + those gets no report *) +module M = { proc f () : unit = { } }. + +expect "module M = { + proc f() : unit = {} +}." by print module M. + +expect "proc f() : unit = {}" by print proc M.f. + +(* a name that resolves to nothing keeps the plain `print' diagnostic *) +expect "no object `nosuchop' in the category [operators, predicates or exceptions]" + by print op nosuchop.