From 7febc65f4c0a6aa3d3de6cb63b8ef347f61f27a4 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 25 Apr 2022 14:47:36 +0100 Subject: [PATCH 1/4] Add hook to K-IO --- k-distribution/include/kframework/builtin/domains.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 59979f37467..4a0b36f8fd2 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2419,6 +2419,17 @@ 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 **each** term that is +logged, which requires that the underlying K definition is re-parsed. Doing so +is expensive, and so `#trace` should only be used as a debugging aid. + +```k + syntax {Sort} K ::= #trace(value: Sort) [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"` From 77880698f7530e0bf7181e79c3c5d02ecae238e3 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 25 Apr 2022 15:20:25 +0100 Subject: [PATCH 2/4] Add test for new #trace hook --- k-distribution/tests/regression-new/trace/1.test | 1 + .../tests/regression-new/trace/1.test.out | 7 +++++++ k-distribution/tests/regression-new/trace/Makefile | 8 ++++++++ k-distribution/tests/regression-new/trace/test.k | 14 ++++++++++++++ 4 files changed, 30 insertions(+) create mode 100644 k-distribution/tests/regression-new/trace/1.test create mode 100644 k-distribution/tests/regression-new/trace/1.test.out create mode 100644 k-distribution/tests/regression-new/trace/Makefile create mode 100644 k-distribution/tests/regression-new/trace/test.k diff --git a/k-distribution/tests/regression-new/trace/1.test b/k-distribution/tests/regression-new/trace/1.test new file mode 100644 index 00000000000..e5c1dcdf879 --- /dev/null +++ b/k-distribution/tests/regression-new/trace/1.test @@ -0,0 +1 @@ +bar foo(34) * frob("Hello", false) diff --git a/k-distribution/tests/regression-new/trace/1.test.out b/k-distribution/tests/regression-new/trace/1.test.out new file mode 100644 index 00000000000..9c62a03b669 --- /dev/null +++ b/k-distribution/tests/regression-new/trace/1.test.out @@ -0,0 +1,7 @@ +foo ( 34 ) +frob ( "Hello" , false ) +bar + foo ( 2 ) * foo ( 0 ) + + . + diff --git a/k-distribution/tests/regression-new/trace/Makefile b/k-distribution/tests/regression-new/trace/Makefile new file mode 100644 index 00000000000..e83e8608d46 --- /dev/null +++ b/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 diff --git a/k-distribution/tests/regression-new/trace/test.k b/k-distribution/tests/regression-new/trace/test.k new file mode 100644 index 00000000000..1956ba2ac9a --- /dev/null +++ b/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(bar foo(2) * foo(0)) ~> .K) +endmodule From 00de9d6b2783359cc63e6d4e406e7afc1505889d Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 16 May 2022 16:32:18 +0100 Subject: [PATCH 3/4] Comment explaining cache --- k-distribution/include/kframework/builtin/domains.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 4a0b36f8fd2..4aa1b3d9c6e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2422,9 +2422,9 @@ finishes. 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 **each** term that is -logged, which requires that the underlying K definition is re-parsed. Doing so -is expensive, and so `#trace` should only be used as a debugging aid. +`#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 {Sort} K ::= #trace(value: Sort) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol] From 3b25304e0e723af0bbe7d427617c8bcac2473324 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Wed, 8 Jun 2022 09:44:28 +0100 Subject: [PATCH 4/4] Ensure that builtin sorts work --- k-distribution/include/kframework/builtin/domains.md | 3 ++- k-distribution/tests/regression-new/trace/1.test.out | 1 + k-distribution/tests/regression-new/trace/test.k | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 4aa1b3d9c6e..de51db23c6f 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2427,7 +2427,8 @@ logged, which requires re-parsing the underlying K definition. Subsequent calls do not incur this overhead again; the definition is cached. ```k - syntax {Sort} K ::= #trace(value: Sort) [function, functional, hook(IO.traceTerm), impure, returnsUnit, symbol] + 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 diff --git a/k-distribution/tests/regression-new/trace/1.test.out b/k-distribution/tests/regression-new/trace/1.test.out index 9c62a03b669..175c9e6f342 100644 --- a/k-distribution/tests/regression-new/trace/1.test.out +++ b/k-distribution/tests/regression-new/trace/1.test.out @@ -1,5 +1,6 @@ foo ( 34 ) frob ( "Hello" , false ) +"builtin" bar foo ( 2 ) * foo ( 0 ) diff --git a/k-distribution/tests/regression-new/trace/test.k b/k-distribution/tests/regression-new/trace/test.k index 1956ba2ac9a..79750afdcd2 100644 --- a/k-distribution/tests/regression-new/trace/test.k +++ b/k-distribution/tests/regression-new/trace/test.k @@ -10,5 +10,5 @@ module TEST rule bar F1 * F2 => #let _ = #trace(F1) #in - (#trace(F2) ~> #trace(bar foo(2) * foo(0)) ~> .K) + (#trace(F2) ~> #trace("builtin") ~> #trace(bar foo(2) * foo(0)) ~> .K) endmodule