feat: print an individual procedure (print [proc] M.p)

Add support for printing a single procedure instead of a whole module.

Procedures of an un-instantiated functor print in suspended mode, with
the functor parameters kept abstract.

Author: strub

src/ecCommands.ml

@@ -390,6 +390,7 @@ let process_pr fmt scope p =
   | Pr_th   qs -> EcPrinting.ObjectInfo.pr_th   fmt env   (unloc qs)
   | Pr_ax   qs -> EcPrinting.ObjectInfo.pr_ax   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)
   | Pr_any  qs -> EcPrinting.ObjectInfo.pr_any  fmt env   (unloc qs)
 

src/ecCorePrinting.ml

@@ -136,6 +136,7 @@ module type PrinterAPI = sig
     val pr_th  : Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_ax  : 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
     val pr_rw  : Format.formatter -> EcEnv.env -> qsymbol -> unit
     val pr_at  : Format.formatter -> EcEnv.env -> symbol -> unit

src/ecParser.mly

@@ -3849,6 +3849,7 @@ print:
 | AXIOM       qs=qident          { Pr_ax   qs            }
 | LEMMA       qs=qident          { Pr_ax   qs            }
 | MODULE      qs=qident          { Pr_mod  qs            }
+| PROC        qs=qident          { Pr_proc qs            }
 | MODULE TYPE qs=qident          { Pr_mty  qs            }
 | GLOB        qs=loc(mod_qident) { Pr_glob qs            }
 | GOAL        n=sword            { Pr_goal n             }

src/ecParsetree.ml

@@ -1254,6 +1254,7 @@ type pprint =
   | Pr_pr   of pqsymbol
   | Pr_ax   of pqsymbol
   | Pr_mod  of pqsymbol
+  | Pr_proc of pqsymbol
   | Pr_mty  of pqsymbol
   | Pr_glob of pmsymbol located
   | Pr_goal of int

src/ecPrinting.ml

@@ -3645,6 +3645,44 @@ and pp_block ppe fmt s =
 and pp_stmt ppe fmt s =
   pp_list "@," (pp_instr ppe) fmt s.s_node
 
+let pp_function ppe fmt (fun_ : function_) =
+  let pp_item ppe fmt = function
+    | `Var pv ->
+        Format.fprintf fmt "@[<hov 2>var %a;@]" (pp_pvdecl ppe) pv
+    | `Instr i ->
+        Format.fprintf fmt "%a" (pp_instr ppe) i
+    | `Return e ->
+        Format.fprintf fmt "@[<hov 2>return@ @[%a@];@]" (pp_expr ppe) e
+  in
+
+  let pp_funhdr ppe fmt fun_ =
+    let with_sig = match fun_.f_def with FBalias _ -> false | _ -> true in
+    Format.fprintf fmt "%a" (pp_funsig ~with_sig ppe) fun_.f_sig in
+
+  let pp_fundef ppe fmt fun_ =
+    match fun_.f_def with
+    | (FBdef def) ->
+      let dummy_mem = EcIdent.create "&hr_dummy" in
+      let _, me = EcEnv.Fun.actmem_body dummy_mem fun_ in
+      let ppe  = PPEnv.push_mem ppe ~active:true me in
+      let vars = List.map (fun x -> `Var    x) def.f_locals in
+      let stmt = List.map (fun x -> `Instr  x) def.f_body.s_node in
+      let ret  = List.map (fun x -> `Return x) (otolist def.f_ret) in
+      let all  = List.filter (fun x -> not (List.is_empty x)) [vars; stmt; ret] in
+
+      if List.is_empty all then Format.fprintf fmt "{}" else
+        Format.fprintf fmt "{@,  @[<v>%a@]@,}"
+          (pp_list "@,@," (pp_list "@," (pp_item ppe))) all;
+
+    | FBalias g ->
+        Format.fprintf fmt "%a" (pp_funname ppe) g
+
+    | FBabs _ ->
+        Format.fprintf fmt "?ABSTRACT?"
+  in
+
+  Format.fprintf fmt "@[<v>%a = %a@]" (pp_funhdr ppe) fun_ (pp_fundef ppe) fun_
+
 let rec pp_modexp ppe fmt (p, me) =
   let params =
     match me.me_body with
@@ -3676,42 +3714,7 @@ and pp_moditem ppe fmt (p, i) =
       Format.fprintf fmt "@[<hov 2>var %a@]" (pp_pvdecl ppe) v
 
   | MI_Function f ->
-    let pp_item ppe fmt = function
-      | `Var pv ->
-          Format.fprintf fmt "@[<hov 2>var %a;@]" (pp_pvdecl ppe) pv
-      | `Instr i ->
-          Format.fprintf fmt "%a" (pp_instr ppe) i
-      | `Return e ->
-          Format.fprintf fmt "@[<hov 2>return@ @[%a@];@]" (pp_expr ppe) e
-    in
-
-    let pp_funsig ppe fmt fun_ =
-      let with_sig = match fun_.f_def with FBalias _ -> false | _ -> true in
-      Format.fprintf fmt "%a" (pp_funsig ~with_sig ppe) fun_.f_sig in
-
-    let pp_fundef ppe fmt fun_ =
-      match fun_.f_def with
-      | (FBdef def) ->
-        let dummy_mem = EcIdent.create "&hr_dummy" in
-        let _, me = EcEnv.Fun.actmem_body dummy_mem fun_ in
-        let ppe  = PPEnv.push_mem ppe ~active:true me in
-        let vars = List.map (fun x -> `Var    x) def.f_locals in
-        let stmt = List.map (fun x -> `Instr  x) def.f_body.s_node in
-        let ret  = List.map (fun x -> `Return x) (otolist def.f_ret) in
-        let all  = List.filter (fun x -> not (List.is_empty x)) [vars; stmt; ret] in
-
-        if List.is_empty all then Format.fprintf fmt "{}" else
-          Format.fprintf fmt "{@,  @[<v>%a@]@,}"
-            (pp_list "@,@," (pp_list "@," (pp_item ppe))) all;
-
-      | FBalias g ->
-          Format.fprintf fmt "%a" (pp_funname ppe) g
-
-      | FBabs _ ->
-          Format.fprintf fmt "?ABSTRACT?"
-    in
-
-    Format.fprintf fmt "@[<v>%a = %a@]" (pp_funsig ppe) f (pp_fundef ppe) f
+    pp_function ppe fmt f
 
 let pp_modexp ppe fmt (mp, me) =
   Format.fprintf fmt "%a." (pp_modexp ppe) (mp, me)
@@ -4103,6 +4106,31 @@ module ObjectInfo = struct
 
   let pr_mod = pr_gen pr_mod_r
 
+  (* ------------------------------------------------------------------ *)
+  let pr_fun_r =
+    (* Prefer the substituting lookup so that a concrete or fully-applied
+       procedure prints with its instantiated names.  When the enclosing
+       module still has functor parameters, that lookup fails; we then fall
+       back to the suspended view, which keeps the parameters abstract. *)
+    let lookup qs env =
+      try
+        let (xp, f) = EcEnv.Fun.lookup qs env in
+        (xp, { EcEnv.sp_target = f; sp_params = (0, []); })
+      with EcEnv.LookupFailure _ -> EcEnv.Fun.sp_lookup qs env in
+    { od_name    = "procedures";
+      od_lookup  = lookup;
+      od_printer =
+        (fun ppe fmt (_, susp) ->
+          let (_, params) = susp.EcEnv.sp_params in
+          let (ppe, pp_params) = pp_mod_params ppe params in
+          if List.is_empty params then
+            pp_function ppe fmt susp.EcEnv.sp_target
+          else
+            Format.fprintf fmt "@[<v>(* in functor %t *)@ %a@]"
+              pp_params (pp_function ppe) susp.EcEnv.sp_target); }
+
+  let pr_fun = pr_gen pr_fun_r
+
   (* ------------------------------------------------------------------ *)
   let pr_mty_r =
     { od_name    = "module types";
@@ -4148,6 +4176,7 @@ module ObjectInfo = struct
                     pr_gen_r ~prcat:true pr_th_r ;
                     pr_gen_r ~prcat:true pr_ax_r ;
                     pr_gen_r ~prcat:true pr_mod_r;
+                    pr_gen_r ~prcat:true pr_fun_r;
                     pr_gen_r ~prcat:true pr_mty_r;
                     pr_gen_r ~prcat:true pr_rw_r ;
                     pr_gen_r ~prcat:true pr_at_r ; ] in

tests/print-proc.ec

@@ -0,0 +1,59 @@
+(* Unit tests for `print proc M.p` and printing a procedure via the
+   untyped `print M.p` lookup. Uses the `expect "..." by print ...`
+   command (String.trim-based comparison). *)
+
+require import Int.
+
+module type T = { proc o (x : int) : int }.
+
+module M = {
+  var g : int
+
+  proc k () : int = {
+    return 3;
+  }
+
+  proc w () : unit = {
+    g <- g + 1;
+  }
+}.
+
+module F (A : T) = {
+  var g : int
+
+  proc run (x : int) : unit = {
+    g <@ A.o(x);
+  }
+}.
+
+module Impl = { proc o (x : int) : int = { return x; } }.
+module G = F(Impl).
+
+(* explicit `print proc`, simple body *)
+expect "proc k() : int = {
+  return 3;
+}" by print proc M.k.
+
+(* explicit `print proc`, statement body referencing a module variable *)
+expect "proc w() : unit = {
+  M.g <- M.g + 1;
+}" by print proc M.w.
+
+(* bare `print M.k` finds the procedure via the untyped lookup *)
+expect "* In [procedures]:
+
+proc k() : int = {
+  return 3;
+}" by print M.k.
+
+(* a procedure of an un-instantiated functor prints in suspended mode,
+   with the call to the abstract parameter [A] kept abstract *)
+expect "(* in functor (A : T) *)
+proc run(x : int) : unit = {
+  F.g <@ A.o(x);
+}" by print proc F.run.
+
+(* once the functor is applied, the call to [A] is resolved concretely *)
+expect "proc run(x : int) : unit = {
+  F.g <@ Impl.o(x);
+}" by print proc G.run.