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.

Author: strub

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
 

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

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]

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 ()