feat: add expect "..." by print ... command

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)

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  }

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)

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.