Reformat dotk{} to print as .K rather than . (#990)

See runtimeverification/k#4017 for full context. Blocked on downstream semantics updates.
runtimeverification · Feb 21, 2024 · d3c1ee7 · d3c1ee7
1 parent 0861085
commit d3c1ee7
Show file tree

Hide file tree

Showing 8 changed files with 12 additions and 12 deletions.
diff --git a/lib/printer/printer.cpp b/lib/printer/printer.cpp
@@ -43,7 +43,7 @@ std::map<std::string, std::string> getFormats() {
   if (once) {
     formats["kseq"] = "%1 ~> %2";
     formats["append"] = "%1 ~> %2";
-    formats["dotk"] = ".";
+    formats["dotk"] = ".K";
     formats["inj"] = "%1";
     formats["\\bottom"] = "#Bottom";
     formats["\\top"] = "#Top";

diff --git a/test/output/amb.out.diff b/test/output/amb.out.diff
@@ -1,3 +1,3 @@
 <k>
-  amb ( ( 1 * 2 ) * 3 , 1 * ( 2 * 3 ) ) ~> .
+  amb ( ( 1 * 2 ) * 3 , 1 * ( 2 * 3 ) ) ~> .K
 </k>
diff --git a/test/output/locations.out.diff b/test/output/locations.out.diff
@@ -1,3 +1,3 @@
 <k>
-  stop ( ) ~> bar ( foo ( ) , bar ( bar ( baz ( ) , foo ( ) ) , bar ( foo ( ) , baz ( ) ) ) ) ~> .
+  stop ( ) ~> bar ( foo ( ) , bar ( bar ( baz ( ) , foo ( ) ) , bar ( foo ( ) , baz ( ) ) ) ) ~> .K
 </k>
diff --git a/test/unparse/filter/result.kore.out b/test/unparse/filter/result.kore.out
@@ -1,5 +1,5 @@
 {
   V:K
 #Equals
-  3 ~> .
+  3 ~> .K
 }
diff --git a/test/unparse/imp++/search.cfg.kore.out b/test/unparse/imp++/search.cfg.kore.out
@@ -3,7 +3,7 @@
   #Equals
     [38;5;226m<T>[0m
       [38;5;46m<k>[0m
-        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m 1 ~> . )[0m ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp1_[0m ([0m ++[0m x ~> . )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> . )[0m ~> .
+        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m 1 ~> .K )[0m ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp1_[0m ([0m ++[0m x ~> .K )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> .K )[0m ~> .K
       [38;5;46m</k>[0m
       [38;5;196m<state>[0m
         x |->[0m 1
@@ -17,7 +17,7 @@
   #Equals
     [38;5;226m<T>[0m
       [38;5;46m<k>[0m
-        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m ++[0m x /[0m x ~> . )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> . )[0m ~> .
+        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m ++[0m x /[0m x ~> .K )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> .K )[0m ~> .K
       [38;5;46m</k>[0m
       [38;5;196m<state>[0m
         x |->[0m 1
@@ -31,7 +31,7 @@
   #Equals
     [38;5;226m<T>[0m
       [38;5;46m<k>[0m
-        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m x ~> . )[0m ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp1_[0m ([0m ++[0m x ~> . )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> . )[0m ~> .
+        ++[0m x ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp0_[0m ([0m x ~> .K )[0m ~> #freezer_/__IMP-SYNTAX_AExp_AExp_AExp1_[0m ([0m ++[0m x ~> .K )[0m ~> #freezer_=_;_IMP-SYNTAX_Stmt_Id_AExp1_[0m ([0m y ~> .K )[0m ~> .K
       [38;5;46m</k>[0m
       [38;5;196m<state>[0m
         x |->[0m 1

diff --git a/test/unparse/string/string.cfg.kore.out b/test/unparse/string/string.cfg.kore.out
@@ -1,3 +1,3 @@
 <k>[0m
-  "hello world!" ~> .
+  "hello world!" ~> .K
 </k>[0m
diff --git a/test/unparse/subst/subst.cfg.kore.out b/test/unparse/subst/subst.cfg.kore.out
@@ -5,9 +5,9 @@
     } )
   #And
     <k>[0m
-      ?_0:Int ~> .
+      ?_0:Int ~> .K
     </k>[0m
 #Or
   <k>[0m
-    one[0m ~> .
+    one[0m ~> .K
   </k>[0m
diff --git a/test/unparse/subst/subst2.cfg.kore.out b/test/unparse/subst/subst2.cfg.kore.out
@@ -1,5 +1,5 @@
     <k>[0m
-      ?_0:Int ~> .
+      ?_0:Int ~> .K
     </k>[0m
   #And
     {
@@ -9,5 +9,5 @@
     }
 #Or
   <k>[0m
-    one[0m ~> .
+    one[0m ~> .K
   </k>[0m
-Original file line number
+Diff line change
@@ -1,5 +1,5 @@
     {
       V:K
     #Equals
-~> .
+~> .K
     }