From 2495800f523c7bdc3c8607c04d217e68072924d6 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 26 Feb 2024 12:15:05 +0000 Subject: [PATCH] Fix regression tests --- .../tests/regression-new/bison-glr-bug/iele.k | 2 +- .../regression-new/checkWarns/missingKlabel.k | 4 ++-- .../regression-new/context-alias-2/test.k | 2 +- .../tests/regression-new/issue-1263/test.k | 2 +- .../tests/regression-new/issue-1273/test.k | 2 +- .../issue-1682-korePrettyPrint/test.k | 2 +- .../tests/regression-new/issue-1760/test.k | 24 +++++++++---------- .../issue-1879-kproveTrans/haskell/test.k | 2 +- .../issue-2321-kprovexCrash/test.k | 8 +++---- .../tests/regression-new/issue-999/kat.k | 24 +++++++++---------- .../2_typed/2_static/kool-typed-static.md | 2 +- .../1_untyped/1_environment/fun-untyped.md | 2 +- .../tests/regression-new/unparseKORE/test.k | 4 ++-- 13 files changed, 40 insertions(+), 40 deletions(-) diff --git a/k-distribution/tests/regression-new/bison-glr-bug/iele.k b/k-distribution/tests/regression-new/bison-glr-bug/iele.k index 042f2984a55..bddfc0530d4 100644 --- a/k-distribution/tests/regression-new/bison-glr-bug/iele.k +++ b/k-distribution/tests/regression-new/bison-glr-bug/iele.k @@ -76,7 +76,7 @@ module IELE-COMMON syntax IeleName ::= IeleNameToken syntax IeleName ::= - StringIeleName [avoid, function, klabel(StringIeleName), symbol] + StringIeleName [avoid, function, symbol(StringIeleName)] syntax GlobalName ::= "@" IeleName syntax LocalName ::= diff --git a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k index 4ce27642627..7ec6dbbb179 100644 --- a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k +++ b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k @@ -7,10 +7,10 @@ module MISSINGKLABEL imports BASIC-K syntax MyMap ::= KItem "M|->" KItem - [ function, total, hook(MAP.element), klabel(_M|->_), symbol, injective, unused] + [ function, total, hook(MAP.element), symbol(_M|->_), injective, unused] syntax MyMap ::= MyMap MyMap - [ left, function, hook(MAP.concat), klabel(_MyMap_), symbol, assoc, comm + [ left, function, hook(MAP.concat), symbol(_MyMap_), assoc, comm , unit(.MyMap), element(_M|->_), index(0), format(%1%n%2), unused ] diff --git a/k-distribution/tests/regression-new/context-alias-2/test.k b/k-distribution/tests/regression-new/context-alias-2/test.k index c7236c77caa..1ed5ccc42a6 100644 --- a/k-distribution/tests/regression-new/context-alias-2/test.k +++ b/k-distribution/tests/regression-new/context-alias-2/test.k @@ -8,7 +8,7 @@ module TEST | Id "=" Int | Id | Int - | l(Exp) [klabel(l), symbol] | m(Exp) [klabel(m), symbol] | r(Exp) [klabel(r), symbol] + | l(Exp) [symbol(l)] | m(Exp) [symbol(m)] | r(Exp) [symbol(r)] syntax KResult ::= Int context alias [left]: HERE [context(l)] diff --git a/k-distribution/tests/regression-new/issue-1263/test.k b/k-distribution/tests/regression-new/issue-1263/test.k index 11116707f64..cf4af38df5b 100644 --- a/k-distribution/tests/regression-new/issue-1263/test.k +++ b/k-distribution/tests/regression-new/issue-1263/test.k @@ -5,7 +5,7 @@ module TEST configuration $PGM:Pgm - syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol] + syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)] // --------------------------------------------------------------------- syntax Wad = FInt diff --git a/k-distribution/tests/regression-new/issue-1273/test.k b/k-distribution/tests/regression-new/issue-1273/test.k index 28d7244cd37..482aae99003 100644 --- a/k-distribution/tests/regression-new/issue-1273/test.k +++ b/k-distribution/tests/regression-new/issue-1273/test.k @@ -4,7 +4,7 @@ module TEST imports BOOL syntax FInt ::= "(" FInt ")" [bracket] - | FInt ( value: Int , one: Int ) [klabel(FInt), symbol] + | FInt ( value: Int , one: Int ) [symbol(FInt)] // --------------------------------------------------------------------- syntax FInt ::= "1FInt" "(" Int ")" [macro] diff --git a/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k b/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k index eed64262310..59eb3f06d57 100644 --- a/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k +++ b/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k @@ -4,5 +4,5 @@ module TEST syntax X ::= "a" configuration $PGM:X rule a => ?_:Int - syntax Bool ::= pred1 ( Int ) [function, total, klabel(pred1), symbol, no-evaluators] + syntax Bool ::= pred1 ( Int ) [function, total, symbol(pred1), no-evaluators] endmodule diff --git a/k-distribution/tests/regression-new/issue-1760/test.k b/k-distribution/tests/regression-new/issue-1760/test.k index 7fc1b087108..0be7ed1a953 100644 --- a/k-distribution/tests/regression-new/issue-1760/test.k +++ b/k-distribution/tests/regression-new/issue-1760/test.k @@ -18,13 +18,13 @@ module TEST // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] - | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)] - //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] + | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + | Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)] + //| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] - syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)] + syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)] syntax Kat ::= freshKat(Kat) [freshGenerator, function] @@ -66,19 +66,19 @@ module TEST /* syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] + Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)] > left: - Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] + Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)] > left: - Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] + Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)] */ syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] - | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] - | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] + Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)] + | Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)] + | Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)] rule ONE Kat; B:Kat => B:Kat diff --git a/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k b/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k index 12594e4fbcb..5dcbc869e0f 100644 --- a/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k +++ b/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k @@ -17,7 +17,7 @@ module TEST syntax Step ::= Int // ------------------- - syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol] + syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)] // --------------------------------------------------------------------- syntax FInt ::= "0FInt" "(" Int ")" [macro] diff --git a/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k b/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k index 4a1a3043d98..fa394701525 100644 --- a/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k +++ b/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k @@ -4,17 +4,17 @@ module TEST imports INT syntax Exp ::= Int | Bool - | pair(Int, Int) [klabel(pair), symbol] + | pair(Int, Int) [symbol(pair)] - syntax KItem ::= "#assume" Exp [klabel(assume), symbol] + syntax KItem ::= "#assume" Exp [symbol(assume)] rule #assume true => .K rule #assume false => #Bottom - syntax KItem ::= "#assert" Exp [klabel(assert), symbol] + syntax KItem ::= "#assert" Exp [symbol(assert)] | "#fail" rule #assert true => .K rule #assert false => #fail // Uninterpreted functions - syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), klabel(i)] + syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), symbol(i)] endmodule diff --git a/k-distribution/tests/regression-new/issue-999/kat.k b/k-distribution/tests/regression-new/issue-999/kat.k index ad420232c57..6ec30457d33 100644 --- a/k-distribution/tests/regression-new/issue-999/kat.k +++ b/k-distribution/tests/regression-new/issue-999/kat.k @@ -18,13 +18,13 @@ module KAT // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] - | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)] - //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] + | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + | Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)] + //| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)] - syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)] + syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)] syntax Kat ::= freshKat(Kat) [freshGenerator, function] @@ -66,19 +66,19 @@ module KAT /* syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] + Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)] > left: - Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] + Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)] > left: - Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] + Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)] */ syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] - | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] - | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] + Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)] + | Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)] + | Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)] rule ONE Kat; B:Kat => B:Kat diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md index 0669f2b0629..bba11c2331d 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md @@ -125,7 +125,7 @@ the wrapper in the generated documentation, we associate it an ```k syntax Type ::= "void" | "int" | "bool" | "string" - | Id [klabel("class"), symbol, avoid] // see next + | Id [symbol("class"), avoid] // see next | Type "[" "]" | "(" Type ")" [bracket] > Types "->" Type diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md index db442366b66..80e6182dafd 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md @@ -350,7 +350,7 @@ a constructor for function types: | "(" Type ")" [bracket] | TypeVar | TypeName [klabel(TypeName), avoid] - | Type TypeName [klabel(Type-TypeName), symbol, macro] + | Type TypeName [symbol(Type-TypeName), macro] | "(" Types ")" TypeName [prefer] syntax Types ::= List{Type,","} [klabel(types)] syntax Types ::= TypeVars diff --git a/k-distribution/tests/regression-new/unparseKORE/test.k b/k-distribution/tests/regression-new/unparseKORE/test.k index f57646f8187..51fed8939bf 100644 --- a/k-distribution/tests/regression-new/unparseKORE/test.k +++ b/k-distribution/tests/regression-new/unparseKORE/test.k @@ -5,8 +5,8 @@ module TEST syntax A ::= "a1" A | "a2" A - | "a1" [klabel(b1), symbol] - | "a2" [klabel(a2), symbol] + | "a1" [symbol(b1)] + | "a2" [symbol(a2)] rule a1 => #unparseKORE(a1) rule a2 => #unparseKORE(a2)