From b9887bba357960c4d1ea36877e9ef07404b915fc Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 5 Apr 2026 18:15:51 +0200 Subject: [PATCH] Print type parameters of operators when not inferrable from arguments When an operator has type parameters that cannot be inferred from the types of its provided arguments, the pretty-printer now automatically displays the type instantiation (e.g., `card<:bool>` instead of `card`). A `PP:showtvi` flag (toggled via `pragma +PP:showtvi`) forces display of type parameters even when they are inferrable. --- src/ecCommands.ml | 3 ++- src/ecGState.ml | 6 ++++++ src/ecGState.mli | 4 ++++ src/ecPrinting.ml | 42 +++++++++++++++++++++++++++++++++++++----- 4 files changed, 49 insertions(+), 6 deletions(-) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index acca51faeb..438295196e 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -668,7 +668,8 @@ and process_pragma (scope : EcScope.scope) opt = (* -------------------------------------------------------------------- *) and process_option (scope : EcScope.scope) (name, value) = match value with - | `Bool value when EcLocation.unloc name = EcGState.old_mem_restr -> + | `Bool value when EcLocation.unloc name = EcGState.old_mem_restr + || EcLocation.unloc name = EcGState.pp_showtvi -> let gs = EcEnv.gstate (EcScope.env scope) in EcGState.setflag (unloc name) value gs; scope diff --git a/src/ecGState.ml b/src/ecGState.ml index f7bdb53d9e..cac459c496 100644 --- a/src/ecGState.ml +++ b/src/ecGState.ml @@ -64,6 +64,12 @@ let old_mem_restr = "old_mem_restr" let get_old_mem_restr (g : gstate) : bool = getflag ~default:false old_mem_restr g +(* -------------------------------------------------------------------- *) +let pp_showtvi = "PP:showtvi" + +let get_pp_showtvi (g : gstate) : bool = + getflag ~default:false pp_showtvi g + (* -------------------------------------------------------------------- *) let add_notifier (notifier : loglevel -> string Lazy.t -> unit) (gs : gstate) = let notifier = { nt_id = EcUid.unique (); nt_cb = notifier; } in diff --git a/src/ecGState.mli b/src/ecGState.mli index 2124981bba..3b516421cd 100644 --- a/src/ecGState.mli +++ b/src/ecGState.mli @@ -28,6 +28,10 @@ val setflag : string -> bool -> gstate -> unit val old_mem_restr : string val get_old_mem_restr : gstate -> bool +(* --------------------------------------------------------------------- *) +val pp_showtvi : string +val get_pp_showtvi : gstate -> bool + (* --------------------------------------------------------------------- *) type nid_t type loglevel = [`Debug | `Info | `Warning | `Critical] diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 995bfe01b7..cbe75ad3f2 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -36,19 +36,25 @@ module PPEnv = struct ppe_univar : (symbol Mint.t * Ssym.t) ref; ppe_fb : Sp.t; ppe_width : int; + ppe_showtvi : bool; } let ofenv (env : EcEnv.env) = + let gs = EcEnv.gstate env in + let width = EcGState.asint ~default:80 - (EcGState.getvalue "PP:width" (EcEnv.gstate env)) in + (EcGState.getvalue "PP:width" gs) in + + let showtvi = EcGState.get_pp_showtvi gs in { ppe_env = env; ppe_locals = Mid.empty; ppe_inuse = Ssym.empty; ppe_univar = ref (Mint.empty, Ssym.empty); ppe_fb = Sp.empty; - ppe_width = max 20 width; } + ppe_width = max 20 width; + ppe_showtvi = showtvi; } let enter_theory (ppe : t) (p : EcPath.path) = let ppe_env = EcEnv.Theory.env_of_theory p ppe.ppe_env in @@ -936,7 +942,7 @@ let pp_opname_with_tvi | Some tvi -> Format.fprintf fmt "%a<:%a>" pp_opname (nm, op) - (pp_list "@, " (pp_type ppe)) tvi + (pp_list ",@ " (pp_type ppe)) tvi (* -------------------------------------------------------------------- *) let pp_if_form (type v) @@ -1084,6 +1090,22 @@ let pp_app (type v1 v2) in maybe_paren outer e_app_prio pp fmt () +(* -------------------------------------------------------------------- *) +(* [tvi_dominated env op nargs] checks whether all type parameters of [op] + can be inferred from the types of the first [nargs] arguments. *) +let tvi_dominated (env : EcEnv.env) (op : EcPath.path) (nargs : int) : bool = + match EcEnv.Op.by_path_opt op env with + | None -> false + | Some opdecl -> + let tparams = opdecl.op_tparams in + let dom, _ = tyfun_flat opdecl.op_ty in + let arg_tys = List.take nargs dom in + let covered = + List.fold_left + (fun acc ty -> Sid.union acc (EcTypes.Tvar.fv ty)) + Sid.empty arg_tys in + List.for_all (fun id -> Sid.mem id covered) tparams + (* -------------------------------------------------------------------- *) let pp_opapp (ppe : PPEnv.t) @@ -1158,13 +1180,23 @@ let pp_opapp in fun () -> doit fmt es with E.PrintAsPlain -> + let tvi_opt = + if List.is_empty tvi then None + else + let dominated = + tvi_dominated ppe.PPEnv.ppe_env op (List.length es) in + if dominated && not ppe.PPEnv.ppe_showtvi + then None else Some tvi + in + fun () -> match es with | [] -> - pp_opname fmt (nm, opname) + pp_opname_with_tvi ppe fmt (nm, opname, tvi_opt) | _ -> - let pp_first = (fun _ _ -> pp_opname) in + let pp_first = fun _ _ fmt op -> + pp_opname_with_tvi ppe fmt (fst op, snd op, tvi_opt) in let pp fmt () = pp_app ppe ~pp_first ~pp_sub outer fmt ((nm, opname), es) in maybe_paren outer max_op_prec pp fmt ()