From f9a2515eeb33674fd906e653cb896f286d6a6a55 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 1 Jul 2026 17:49:06 +0200 Subject: [PATCH] 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. --- src/ecCommands.ml | 1 + src/ecCorePrinting.ml | 1 + src/ecParser.mly | 1 + src/ecParsetree.ml | 1 + src/ecPrinting.ml | 101 +++++++++++++++++++++++++++--------------- tests/print-proc.ec | 59 ++++++++++++++++++++++++ 6 files changed, 128 insertions(+), 36 deletions(-) create mode 100644 tests/print-proc.ec diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 01db9811d..8cdbf561e 100644 --- a/src/ecCommands.ml +++ b/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) diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml index dc8986959..c576efca1 100644 --- a/src/ecCorePrinting.ml +++ b/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 diff --git a/src/ecParser.mly b/src/ecParser.mly index 2707f2e2c..9a24157bd 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3881,6 +3881,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 } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index a4d73b072..18f4acccf 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1261,6 +1261,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 diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index 22a39940d..b423e7d24 100644 --- a/src/ecPrinting.ml +++ b/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 "@[var %a;@]" (pp_pvdecl ppe) pv + | `Instr i -> + Format.fprintf fmt "%a" (pp_instr ppe) i + | `Return e -> + Format.fprintf fmt "@[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 "{@, @[%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 "@[%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 "@[var %a@]" (pp_pvdecl ppe) v | MI_Function f -> - let pp_item ppe fmt = function - | `Var pv -> - Format.fprintf fmt "@[var %a;@]" (pp_pvdecl ppe) pv - | `Instr i -> - Format.fprintf fmt "%a" (pp_instr ppe) i - | `Return e -> - Format.fprintf fmt "@[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 "{@, @[%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 "@[%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 "@[(* 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 diff --git a/tests/print-proc.ec b/tests/print-proc.ec new file mode 100644 index 000000000..8c7115323 --- /dev/null +++ b/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.