Add #trace debugging hook

k-distribution/include/kframework/builtin/domains.md

@@ -2419,6 +2419,18 @@ finishes.
   syntax K ::= #logToFile(name: String, value: String) [function, functional, hook(IO.log), impure, returnsUnit, symbol]
 ```
 
+Terms can also be logged to standard error in _surface syntax_, rather than as
+KORE using `#trace`. This operator has similar semantics to `#logToFile` (i.e.
+it returns `.K`, but prints as an impure side effect). Note that calling
+`#trace` is equivalent to invoking the `kprint` tool for the first term that is
+logged, which requires re-parsing the underlying K definition. Subsequent calls
+do not incur this overhead again; the definition is cached.
+
+```k
+  syntax K ::= #trace(value: KItem) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol]
+             | #traceK(value: K)    [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol]
+```
+
 ### Implementation of high-level I/O streams in K
 
 Below is an implementation of the `stream="stdin"` and `stream="stdout"`

k-distribution/tests/regression-new/trace/1.test

@@ -0,0 +1 @@
+bar foo(34) * frob("Hello", false)

k-distribution/tests/regression-new/trace/1.test.out

@@ -0,0 +1,8 @@
+foo ( 34 )
+frob ( "Hello" , false )
+"builtin"
+bar
+  foo ( 2 ) * foo ( 0 )
+<k>
+  .
+</k>

k-distribution/tests/regression-new/trace/Makefile

@@ -0,0 +1,8 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=--syntax-module TEST
+
+CHECK=2>&1 | diff -
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/trace/test.k

@@ -0,0 +1,14 @@
+module TEST
+  imports DOMAINS
+  imports K-IO
+
+  syntax Foo ::= foo(Int)
+               | frob(String, Bool)
+
+  syntax Bar ::= "bar" Foo "*" Foo [format(%1%i%n%2 %3 %4)]
+               | "(" Bar ")" [bracket]
+
+  rule bar F1 * F2 =>
+    #let _ = #trace(F1) #in
+    (#trace(F2) ~> #trace("builtin") ~> #trace(bar foo(2) * foo(0)) ~> .K)
+endmodule