From 3e263a02f6d3f2895893e55a5095e7603ff360e1 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Thu, 23 Apr 2026 16:33:35 +0200
Subject: [PATCH] feat: add `expect "..." by print ...` command

Introduce a top-level command for unit-testing pretty-printer output
from inside `.ec` files:

    expect "op foo : int = 1." by print op foo.

The expected string is compared (after `String.trim` on both sides)
against the captured output of the inner `print` command. On mismatch,
raise an `hierror` with the expected and actual blocks; this fails the
enclosing script in the standard way and is picked up by `scripts/testing/runtest`.

Multi-line expected literals are supported out of the box because the
existing STRING lexer rule already accepts embedded newlines.

Also adds tests/expect.ec covering nullary/parametric ops, record
types, axioms, and leading/trailing whitespace tolerance.
---
 src/ecCommands.ml  | 17 +++++++++++++++++
 src/ecParser.mly   |  2 ++
 src/ecParsetree.ml |  1 +
 tests/expect.ec    | 30 ++++++++++++++++++++++++++++++
 4 files changed, 50 insertions(+)
 create mode 100644 tests/expect.ec

diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 4910def1f..2b08923ea 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -397,6 +397,22 @@ let check_opname_validity (scope : EcScope.scope) (x : string) =
 let process_print scope p =
   process_pr Format.std_formatter scope p
 
+(* -------------------------------------------------------------------- *)
+let process_expect scope (expected, p) =
+  let buf = Buffer.create 256 in
+  let fmt = Format.formatter_of_buffer buf in
+  process_pr fmt scope p;
+  Format.pp_print_flush fmt ();
+  let actual = Buffer.contents buf in
+  if String.trim actual <> String.trim (unloc expected) then
+    EcScope.hierror ~loc:(loc expected)
+      "expect: output mismatch@\n\
+       --- expected ---@\n\
+       %s@\n\
+       --- actual ---@\n\
+       %s"
+      (unloc expected) actual
+
 (* -------------------------------------------------------------------- *)
 exception Pragma of [`Reset | `Restart]
 
@@ -782,6 +798,7 @@ and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope)
       | GsctOpen     name -> `Fct   (fun scope -> process_sct_open   scope  name)
       | GsctClose    name -> `Fct   (fun scope -> process_sct_close  scope  name)
       | Gprint       p    -> `Fct   (fun scope -> process_print      scope  p; scope)
+      | Gexpect      x    -> `Fct   (fun scope -> process_expect     scope  x; scope)
       | Gsearch      qs   -> `Fct   (fun scope -> process_search     scope  qs; scope)
       | Glocate      x    -> `Fct   (fun scope -> process_locate     scope  x; scope)
       | Gtactics     t    -> `Fct   (fun scope -> process_tactics    ?src scope  t)
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 7a044d45a..65cd97b95 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -3950,6 +3950,8 @@ global_action:
 | hint             { Ghint        $1 }
 | x=loc(proofend)  { Gsave        x  }
 | PRINT p=print    { Gprint       p  }
+| EXPECT s=loc(STRING) BY PRINT p=print
+    { Gexpect (s, p) }
 | SEARCH x=search+ { Gsearch      x  }
 | LOCATE x=qident  { Glocate      x  }
 | WHY3 x=STRING    { GdumpWhy3    x  }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 24d42a667..fa83d6e69 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1351,6 +1351,7 @@ type global_action =
   | Greduction   of puserred
   | Ghint        of phint
   | Gprint       of pprint
+  | Gexpect      of (string located * pprint)
   | Gsearch      of pformula list
   | Glocate      of pqsymbol
   | GthOpen      of (is_local * bool * psymbol)
diff --git a/tests/expect.ec b/tests/expect.ec
new file mode 100644
index 000000000..d6c97b692
--- /dev/null
+++ b/tests/expect.ec
@@ -0,0 +1,30 @@
+(* Unit tests for the `expect "..." by print ...` command. *)
+
+require import Int.
+
+type point = { x : int; y : int; }.
+
+op foo : int = 1.
+op bar (n : int) : int = n + 1.
+
+axiom foo_pos : 0 < foo.
+
+(* nullary op *)
+expect "op foo : int = 1." by print op foo.
+
+(* op with arguments *)
+expect "op bar (n : int) : int = n + 1." by print op bar.
+
+(* record type *)
+expect "type point = { x: int; y: int; }." by print type point.
+
+(* axiom *)
+expect "axiom foo_pos: 0 < foo." by print axiom foo_pos.
+
+(* multi-line string literal with leading/trailing whitespace is
+   tolerated (String.trim-based comparison) *)
+expect "
+
+    op foo : int = 1.
+
+  " by print op foo.