From 931722246494bf390adc8d5f9d2f791c19959dc1 Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 9 Feb 2024 16:25:18 -0600 Subject: [PATCH] Remove latex attribute functionality (#3968) fixes: #3909 This removes functionality related to the `latex` attribute. It also adds a compiler warning for any usage of `latex` to give downstream semantics time to remove it. --- docs/user_manual.md | 1 - .../include/kframework/builtin/domains.md | 94 ++++++------- .../src/main/scripts/bin/kore-print | 5 +- k-distribution/src/main/scripts/bin/krun | 5 +- .../resources/compiler-tests/strategies_imp.k | 2 +- .../resources/convertor-tests/imp_lesson1.k | 2 +- .../resources/convertor-tests/imp_lesson2.k | 2 +- .../test/resources/convertor-tests/kore_imp.k | 2 +- .../tests/profiling/elrond-semantics/test.k | 16 +-- .../tests/profiling/pl-tutorial/imp/test.k | 2 +- .../tests/profiling/pl-tutorial/lambda/test.k | 4 +- .../tests/regression-new/imp++-llvm/imp.md | 2 +- .../tests/regression-new/imp-haskell/imp.k | 2 +- .../tests/regression-new/imp-json/imp.k | 2 +- .../tests/regression-new/imp-kore/imp.k | 2 +- .../tests/regression-new/imp-llvm/imp.k | 2 +- .../tests/regression-new/issue-1760/test.k | 18 +-- .../regression-new/issue-1760/test.k.out | 18 +-- .../tests/regression-new/issue-999/kat.k | 18 +-- .../tests/regression-new/issue-999/kat.k.out | 18 +-- .../regression-new/krun-deserialize/imp.k | 2 +- .../1_k/1_lambda/lesson_8/lambda.k | 4 +- .../pl-tutorial/1_k/2_imp/lesson_4/imp.k | 2 +- .../1_k/3_lambda++/lesson_5/lambda.k | 4 +- .../pl-tutorial/1_k/4_imp++/lesson_7/imp.k | 2 +- .../1_simple/1_untyped/simple-untyped.md | 5 +- .../2_typed/2_dynamic/simple-typed-dynamic.md | 5 +- .../2_kool/1_untyped/kool-untyped.md | 5 +- .../2_typed/1_dynamic/kool-typed-dynamic.md | 5 +- .../2_typed/2_static/kool-typed-static.md | 2 +- .../set-symbolic-tests/inset-11-spec.k.out | 13 -- k-distribution/tests/smoke/imp.k | 2 +- .../kframework/compile/checks/CheckAtt.java | 11 ++ .../java/org/kframework/unparser/KPrint.java | 2 - .../org/kframework/unparser/OutputModes.java | 1 - .../org/kframework/unparser/PrintOptions.java | 2 +- .../java/org/kframework/unparser/ToLatex.java | 131 ------------------ .../backend/html/Latex2HTMLone.properties | 34 ----- .../backend/html/Latex2HTMLzero.properties | 41 ------ 39 files changed, 136 insertions(+), 354 deletions(-) delete mode 100644 kernel/src/main/java/org/kframework/unparser/ToLatex.java delete mode 100755 kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLone.properties delete mode 100755 kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLzero.properties diff --git a/docs/user_manual.md b/docs/user_manual.md index 42e30816db1..cd938adc975 100644 --- a/docs/user_manual.md +++ b/docs/user_manual.md @@ -2961,7 +2961,6 @@ arguments. A legend describing how to interpret the index follows. | `hybrid(_)` | prod | all | [`hybrid` attribute](#hybrid-attribute) | | `hybrid` | prod | all | [`hybrid` attribute](#hybrid-attribute) | | `klabel(_)` | prod | all | [`klabel(_)` and `symbol` attributes](#klabel_-and-symbol-attributes) | -| `latex(_)` | prod | all | No reference yet | | `left` | prod | all | [Symbol priority and associativity](#symbol-priority-and-associativity) | | `locations` | sort | all | [Location Information](#location-information) | | `macro-rec` | prod | all | [Macros and Aliases](#macros-and-aliases) | diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 43e903bdaeb..f207a6f81e6 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -245,7 +245,7 @@ etc. The map with zero elements is represented by `.Map`. ```k - syntax Map ::= ".Map" [function, total, hook(MAP.unit), klabel(.Map), symbol, latex(\dotCt{Map})] + syntax Map ::= ".Map" [function, total, hook(MAP.unit), klabel(.Map), symbol] ``` ### Map elements @@ -254,7 +254,7 @@ An element of a `Map` is constructed via the `|->` operator. The key is on the left and the value is on the right. ```k - syntax Map ::= KItem "|->" KItem [function, total, hook(MAP.element), klabel(_|->_), symbol, latex({#1}\mapsto{#2}), injective] + syntax Map ::= KItem "|->" KItem [function, total, hook(MAP.element), klabel(_|->_), symbol, injective] syntax priorities _|->_ > _Map_ .Map syntax non-assoc _|->_ @@ -308,7 +308,7 @@ in both maps are removed. To remove all the keys in one map from another map, you can say `removeAll(M1, keys(M2))`. ```k - syntax Map ::= Map "-Map" Map [function, total, hook(MAP.difference), latex({#1}-_{\it Map}{#2})] + syntax Map ::= Map "-Map" Map [function, total, hook(MAP.difference)] ``` ### Multiple map update @@ -513,7 +513,7 @@ the size of the smaller map and M is the size of the larger map). The `RangeMap` with zero elements is represented by `.RangeMap`. ```k - syntax RangeMap ::= ".RangeMap" [function, total, hook(RANGEMAP.unit), klabel(.RangeMap), symbol, latex(\dotCt{RangeMap})] + syntax RangeMap ::= ".RangeMap" [function, total, hook(RANGEMAP.unit), klabel(.RangeMap), symbol] ``` ### Range map elements @@ -522,7 +522,7 @@ An element of a `RangeMap` is constructed via the `r|->` operator. The range of keys is on the left, and the value is on the right. ```k - syntax RangeMap ::= Range "r|->" KItem [function, hook(RANGEMAP.elementRng), klabel(_r|->_), symbol, latex({#1}\mapsto{#2}), injective] + syntax RangeMap ::= Range "r|->" KItem [function, hook(RANGEMAP.elementRng), klabel(_r|->_), symbol, injective] syntax priorities _r|->_ > _RangeMap_ .RangeMap syntax non-assoc _r|->_ @@ -588,7 +588,7 @@ the parts of overlapping ranges whose value is the same in both range maps will be removed. ```k - syntax RangeMap ::= RangeMap "-RangeMap" RangeMap [function, total, hook(RANGEMAP.difference), latex({#1}-_{\it RangeMap}{#2})] + syntax RangeMap ::= RangeMap "-RangeMap" RangeMap [function, total, hook(RANGEMAP.difference)] ``` ### Multiple range map update @@ -726,7 +726,7 @@ linear, two is quadratic, three is cubic, etc. The set with zero elements is represented by `.Set`. ```k - syntax Set ::= ".Set" [function, total, hook(SET.unit), klabel(.Set), symbol, latex(\dotCt{Set})] + syntax Set ::= ".Set" [function, total, hook(SET.unit), klabel(.Set), symbol] ``` ### Set elements @@ -766,7 +766,7 @@ N is the size of the second set), or effectively linear. This is the set of elements in the first set that are not present in the second set. ```k - syntax Set ::= Set "-Set" Set [function, total, hook(SET.difference), latex({#1}-_{\it Set}{#2}), klabel(Set:difference), symbol] + syntax Set ::= Set "-Set" Set [function, total, hook(SET.difference), klabel(Set:difference), symbol] ``` ### Set membership @@ -934,7 +934,7 @@ back of the list. The list with zero elements is represented by `.List`. ```k - syntax List ::= ".List" [function, total, hook(LIST.unit), klabel(.List), symbol, smtlib(smt_seq_nil), latex(\dotCt{List})] + syntax List ::= ".List" [function, total, hook(LIST.unit), klabel(.List), symbol, smtlib(smt_seq_nil)] ``` ### List elements @@ -1097,11 +1097,11 @@ and `orBool` may be short-circuited in concrete backends, but in symbolic backends, both arguments will be evaluated. ```k - syntax Bool ::= "notBool" Bool [function, total, klabel(notBool_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Bool}{#1}), hook(BOOL.not)] - > Bool "andBool" Bool [function, total, klabel(_andBool_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Bool}{#2}), hook(BOOL.and)] + syntax Bool ::= "notBool" Bool [function, total, klabel(notBool_), symbol, smt-hook(not), group(boolOperation), hook(BOOL.not)] + > Bool "andBool" Bool [function, total, klabel(_andBool_), symbol, left, smt-hook(and), group(boolOperation), hook(BOOL.and)] | Bool "andThenBool" Bool [function, total, klabel(_andThenBool_), symbol, left, smt-hook(and), group(boolOperation), hook(BOOL.andThen)] | Bool "xorBool" Bool [function, total, klabel(_xorBool_), symbol, left, smt-hook(xor), group(boolOperation), hook(BOOL.xor)] - | Bool "orBool" Bool [function, total, klabel(_orBool_), symbol, left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Bool}{#2}), hook(BOOL.or)] + | Bool "orBool" Bool [function, total, klabel(_orBool_), symbol, left, smt-hook(or), group(boolOperation), hook(BOOL.or)] | Bool "orElseBool" Bool [function, total, klabel(_orElseBool_), symbol, left, smt-hook(or), group(boolOperation), hook(BOOL.orElse)] | Bool "impliesBool" Bool [function, total, klabel(_impliesBool_), symbol, left, smt-hook(=>), group(boolOperation), hook(BOOL.implies)] > left: @@ -1225,31 +1225,31 @@ You can: * Compute the bitwise inclusive-or of two integers in twos-complement. ```k - syntax Int ::= "~Int" Int [function, klabel(~Int_), symbol, total, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not), smtlib(notInt)] + syntax Int ::= "~Int" Int [function, klabel(~Int_), symbol, total, hook(INT.not), smtlib(notInt)] > left: - Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook(^), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] + Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook(^), hook(INT.pow)] | Int "^%Int" Int Int [function, klabel(_^%Int__), symbol, left, smt-hook((mod (^ #1 #2) #3)), hook(INT.powmod)] > left: - Int "*Int" Int [function, total, klabel(_*Int_), symbol, left, comm, smt-hook(*), latex({#1}\mathrel{\ast_{\scriptstyle\it Int}}{#2}), hook(INT.mul)] + Int "*Int" Int [function, total, klabel(_*Int_), symbol, left, comm, smt-hook(*), hook(INT.mul)] /* FIXME: translate /Int and %Int into smtlib */ /* /Int and %Int implement t-division, which rounds towards 0 */ - | Int "/Int" Int [function, klabel(_/Int_), symbol, left, smt-hook(div), latex({#1}\mathrel{\div_{\scriptstyle\it Int}}{#2}), hook(INT.tdiv)] - | Int "%Int" Int [function, klabel(_%Int_), symbol, left, smt-hook(mod), latex({#1}\mathrel{\%_{\scriptstyle\it Int}}{#2}), hook(INT.tmod)] + | Int "/Int" Int [function, klabel(_/Int_), symbol, left, smt-hook(div), hook(INT.tdiv)] + | Int "%Int" Int [function, klabel(_%Int_), symbol, left, smt-hook(mod), hook(INT.tmod)] /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */ | Int "divInt" Int [function, klabel(_divInt_), symbol, left, smt-hook(div), hook(INT.ediv)] | Int "modInt" Int [function, klabel(_modInt_), symbol, left, smt-hook(mod), hook(INT.emod)] > left: - Int "+Int" Int [function, total, klabel(_+Int_), symbol, left, comm, smt-hook(+), latex({#1}\mathrel{+_{\scriptstyle\it Int}}{#2}), hook(INT.add)] - | Int "-Int" Int [function, total, klabel(_-Int_), symbol, left, smt-hook(-), latex({#1}\mathrel{-_{\scriptstyle\it Int}}{#2}), hook(INT.sub)] + Int "+Int" Int [function, total, klabel(_+Int_), symbol, left, comm, smt-hook(+), hook(INT.add)] + | Int "-Int" Int [function, total, klabel(_-Int_), symbol, left, smt-hook(-), hook(INT.sub)] > left: - Int ">>Int" Int [function, klabel(_>>Int_), symbol, left, latex({#1}\mathrel{\gg_{\scriptstyle\it Int}}{#2}), hook(INT.shr), smtlib(shrInt)] - | Int "<>Int" Int [function, klabel(_>>Int_), symbol, left, hook(INT.shr), smtlib(shrInt)] + | Int "< left: - Int "&Int" Int [function, total, klabel(_&Int_), symbol, left, comm, latex({#1}\mathrel{\&_{\scriptstyle\it Int}}{#2}), hook(INT.and), smtlib(andInt)] + Int "&Int" Int [function, total, klabel(_&Int_), symbol, left, comm, hook(INT.and), smtlib(andInt)] > left: - Int "xorInt" Int [function, total, klabel(_xorInt_), symbol, left, comm, latex({#1}\mathrel{\oplus_{\scriptstyle\it Int}}{#2}), hook(INT.xor), smtlib(xorInt)] + Int "xorInt" Int [function, total, klabel(_xorInt_), symbol, left, comm, hook(INT.xor), smtlib(xorInt)] > left: - Int "|Int" Int [function, total, klabel(_|Int_), symbol, left, comm, latex({#1}\mathrel{|_{\scriptstyle\it Int}}{#2}), hook(INT.or), smtlib(orInt)] + Int "|Int" Int [function, total, klabel(_|Int_), symbol, left, comm, hook(INT.or), smtlib(orInt)] ``` ### Integer minimum and maximum @@ -1301,12 +1301,12 @@ You can compute whether two integers are less than or equal to, less than, greater than or equal to, greater than, equal, or unequal to another integer. ```k - syntax Bool ::= Int "<=Int" Int [function, total, klabel(_<=Int_), symbol, smt-hook(<=), latex({#1}\mathrel{\leq_{\scriptstyle\it Int}}{#2}), hook(INT.le)] - | Int "=Int" Int [function, total, klabel(_>=Int_), symbol, smt-hook(>=), latex({#1}\mathrel{\geq_{\scriptstyle\it Int}}{#2}), hook(INT.ge)] - | Int ">Int" Int [function, total, klabel(_>Int_), symbol, smt-hook(>), latex({#1}\mathrel{>_{\scriptstyle\it Int}}{#2}), hook(INT.gt)] - | Int "==Int" Int [function, total, klabel(_==Int_), symbol, comm, smt-hook(=), latex({#1}\mathrel{{=}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.eq)] - | Int "=/=Int" Int [function, total, klabel(_=/=Int_), symbol, comm, smt-hook(distinct), latex({#1}\mathrel{{=}{/}{=}_{\scriptstyle\it Int}}{#2}), hook(INT.ne)] + syntax Bool ::= Int "<=Int" Int [function, total, klabel(_<=Int_), symbol, smt-hook(<=), hook(INT.le)] + | Int "=Int" Int [function, total, klabel(_>=Int_), symbol, smt-hook(>=), hook(INT.ge)] + | Int ">Int" Int [function, total, klabel(_>Int_), symbol, smt-hook(>), hook(INT.gt)] + | Int "==Int" Int [function, total, klabel(_==Int_), symbol, comm, smt-hook(=), hook(INT.eq)] + | Int "=/=Int" Int [function, total, klabel(_=/=Int_), symbol, comm, smt-hook(distinct), hook(INT.ne)] ``` ### Divides @@ -1536,14 +1536,14 @@ You can: ```k syntax Float ::= "--Float" Float [function, total, smt-hook(fp.neg), hook(FLOAT.neg)] - > Float "^Float" Float [function, left, latex({#1}^{#2}), hook(FLOAT.pow)] + > Float "^Float" Float [function, left, hook(FLOAT.pow)] > left: - Float "*Float" Float [function, left, smt-hook((fp.mul roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\ast_{\scriptstyle\it Float}}{#2}), hook(FLOAT.mul)] - | Float "/Float" Float [function, left, smt-hook((fp.div roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\div_{\scriptstyle\it Float}}{#2}), hook(FLOAT.div)] - | Float "%Float" Float [function, left, smt-hook((fp.rem roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{\%_{\scriptstyle\it Float}}{#2}), hook(FLOAT.rem)] + Float "*Float" Float [function, left, smt-hook((fp.mul roundNearestTiesToEven #1 #2)), hook(FLOAT.mul)] + | Float "/Float" Float [function, left, smt-hook((fp.div roundNearestTiesToEven #1 #2)), hook(FLOAT.div)] + | Float "%Float" Float [function, left, smt-hook((fp.rem roundNearestTiesToEven #1 #2)), hook(FLOAT.rem)] > left: - Float "+Float" Float [function, left, smt-hook((fp.add roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{+_{\scriptstyle\it Float}}{#2}), hook(FLOAT.add)] - | Float "-Float" Float [function, left, smt-hook((fp.sub roundNearestTiesToEven #1 #2)), latex({#1}\mathrel{-_{\scriptstyle\it Float}}{#2}), hook(FLOAT.sub)] + Float "+Float" Float [function, left, smt-hook((fp.add roundNearestTiesToEven #1 #2)), hook(FLOAT.add)] + | Float "-Float" Float [function, left, smt-hook((fp.sub roundNearestTiesToEven #1 #2)), hook(FLOAT.sub)] ``` ### Floating-point mathematics @@ -1614,12 +1614,12 @@ is true, because `NaN` compares unequal to all values, including itself, in IEEE 754 arithmetic. `0.0 ==Float -0.0` is also true. ```k - syntax Bool ::= Float "<=Float" Float [function, smt-hook(fp.leq), latex({#1}\mathrel{\leq_{\scriptstyle\it Float}}{#2}), hook(FLOAT.le)] - | Float "=Float" Float [function, smt-hook(fp.geq), latex({#1}\mathrel{\geq_{\scriptstyle\it Float}}{#2}), hook(FLOAT.ge)] - | Float ">Float" Float [function, smt-hook(fg.gt), latex({#1}\mathrel{>_{\scriptstyle\it Float}}{#2}), hook(FLOAT.gt)] - | Float "==Float" Float [function, comm, smt-hook(fp.eq), latex({#1}\mathrel{==_{\scriptstyle\it Float}}{#2}), hook(FLOAT.eq), klabel(_==Float_)] - | Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2))), latex({#1}\mathrel{\neq_{\scriptstyle\it Float}}{#2})] + syntax Bool ::= Float "<=Float" Float [function, smt-hook(fp.leq), hook(FLOAT.le)] + | Float "=Float" Float [function, smt-hook(fp.geq), hook(FLOAT.ge)] + | Float ">Float" Float [function, smt-hook(fg.gt), hook(FLOAT.gt)] + | Float "==Float" Float [function, comm, smt-hook(fp.eq), hook(FLOAT.eq), klabel(_==Float_)] + | Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2)))] rule F1:Float =/=Float F2:Float => notBool (F1 ==Float F2) ``` @@ -1634,8 +1634,8 @@ if the nearest integer is not representable in the specified floating-point type. ```k - syntax Float ::= Int2Float(Int, precision: Int, exponentBits: Int) [function, latex({\\it{}Int2Float}), hook(FLOAT.int2float)] - syntax Int ::= Float2Int(Float) [function, total, latex({\\it{}Float2Int}), hook(FLOAT.float2int)] + syntax Float ::= Int2Float(Int, precision: Int, exponentBits: Int) [function, hook(FLOAT.int2float)] + syntax Int ::= Float2Int(Float) [function, total, hook(FLOAT.float2int)] ``` ### Implementation of Floats @@ -1698,7 +1698,7 @@ You can concatenate two strings in O(N) time. For successive concatenation operations, it may be better to use the `STRING-BUFFER` module. ```k - syntax String ::= String "+String" String [function, total, left, latex({#1}+_{\scriptstyle\it String}{#2}), hook(STRING.concat)] + syntax String ::= String "+String" String [function, total, left, hook(STRING.concat)] ``` ### String length @@ -2274,8 +2274,8 @@ module K-EQUAL-SYNTAX imports private BASIC-K syntax Bool ::= left: - K "==K" K [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, latex({#1}\mathrel{=_K}{#2}), group(equalEqualK)] - | K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, latex({#1}\mathrel{\neq_K}{#2}), group(notEqualEqualK)] + K "==K" K [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, group(equalEqualK)] + | K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, group(notEqualEqualK)] syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp diff --git a/k-distribution/src/main/scripts/bin/kore-print b/k-distribution/src/main/scripts/bin/kore-print index d6b995a26e8..219ce01a1a4 100644 --- a/k-distribution/src/main/scripts/bin/kore-print +++ b/k-distribution/src/main/scripts/bin/kore-print @@ -50,7 +50,7 @@ $KORE_PRINT arguments: variables from substitution output -o, --output MODE Select output mode to use when unparsing. Valid values are pretty, program, kast, binary, json, - latex, kore, and none + kore, and none --output-file FILE Print converted term to FILE --save-temps Do not delete temporary files when $KORE_PRINT terminates @@ -114,12 +114,11 @@ do kast) ;; binary) ;; json) ;; - latex) ;; kore) ;; none) ;; *) - error 1 'Invalid value for --output. Should be one of "pretty", "program", "kast", "binary", "json", "latex", "kore", or "none".' + error 1 'Invalid value for --output. Should be one of "pretty", "program", "kast", "binary", "json", "kore", or "none".' ;; esac outputMode="$2" diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun index e5e88599fe4..93c2cf691e1 100755 --- a/k-distribution/src/main/scripts/bin/krun +++ b/k-distribution/src/main/scripts/bin/krun @@ -143,7 +143,7 @@ $KRUN options: variables from substitution output -o, --output MODE Select output mode to use when unparsing. Valid values are pretty, program, kast, binary, json, - latex, kore, and none. + kore, and none. --output-file FILE Print final configuration to FILE --parser VALUE Use VALUE as parser to parse \$PGM. For example, if the user says "$KRUN --parser cat foo.kore", then @@ -297,12 +297,11 @@ do kast) ;; binary) ;; json) ;; - latex) ;; kore) ;; none) ;; *) - error 1 'Invalid value for --output. Should be one of "pretty", "program", "kast", "binary", "json", "latex", "kore", or "none".' + error 1 'Invalid value for --output. Should be one of "pretty", "program", "kast", "binary", "json", "kore", or "none".' ;; esac outputMode="$2" diff --git a/k-distribution/src/test/resources/compiler-tests/strategies_imp.k b/k-distribution/src/test/resources/compiler-tests/strategies_imp.k index 715871d5b78..21ec271e850 100644 --- a/k-distribution/src/test/resources/compiler-tests/strategies_imp.k +++ b/k-distribution/src/test/resources/compiler-tests/strategies_imp.k @@ -13,7 +13,7 @@ module IMP-SYNTAX > AExp "+" AExp [left, strict] | "(" AExp ")" [bracket] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] > BExp "&&" BExp [left, strict(1)] | "(" BExp ")" [bracket] diff --git a/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k b/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k index a535783aedb..18d81483e79 100644 --- a/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k +++ b/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k @@ -11,7 +11,7 @@ module IMP-SYNTAX > AExp "+" AExp [left, strict] | "(" AExp ")" [bracket] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] > BExp "&&" BExp [left, strict(1)] | "(" BExp ")" [bracket] diff --git a/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k b/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k index 1f41f40e7cc..e1ca6e67358 100644 --- a/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k +++ b/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k @@ -11,7 +11,7 @@ module IMP-SYNTAX > AExp "+" AExp [left, strict] | "(" AExp ")" [bracket] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] > BExp "&&" BExp [left, strict(1)] | "(" BExp ")" [bracket] diff --git a/k-distribution/src/test/resources/convertor-tests/kore_imp.k b/k-distribution/src/test/resources/convertor-tests/kore_imp.k index e5a9982b8ef..bfb71bb1c42 100644 --- a/k-distribution/src/test/resources/convertor-tests/kore_imp.k +++ b/k-distribution/src/test/resources/convertor-tests/kore_imp.k @@ -11,7 +11,7 @@ module IMP-SYNTAX > AExp "+" AExp [left, strict] | "(" AExp ")" [bracket] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] > BExp "&&" BExp [left, strict(1)] | "(" BExp ")" [bracket] diff --git a/k-distribution/tests/profiling/elrond-semantics/test.k b/k-distribution/tests/profiling/elrond-semantics/test.k index 96afe61444c..5e72bdf7b4c 100644 --- a/k-distribution/tests/profiling/elrond-semantics/test.k +++ b/k-distribution/tests/profiling/elrond-semantics/test.k @@ -2118,7 +2118,7 @@ module LIST-BYTES syntax ListBytes ::= ListBytes ListBytes [assoc, element(ListBytesItem), format(%1%n%2), function, hook(LIST.concat), klabel(_ListBytes_), left, smtlib(smt_seq_concat), symbol, total, unit(.ListBytes)] syntax ListBytes ::= - ".ListBytes" [function, hook(LIST.unit), klabel(.ListBytes), latex(\dotCt{ListBytes}), smtlib(smt_seq_nil), symbol, total] + ".ListBytes" [function, hook(LIST.unit), klabel(.ListBytes), smtlib(smt_seq_nil), symbol, total] syntax ListBytes ::= "ListItem" "(" WrappedBytes ")" [function, hook(LIST.element), klabel(ListBytesItem), smtlib(smt_seq_elem), symbol, total] syntax WrappedBytes ::= @@ -2185,9 +2185,9 @@ module MAP-BYTES-TO-BYTES syntax MapBytesToBytes ::= MapBytesToBytes MapBytesToBytes [assoc, comm, element(_Bytes2Bytes|->_), format(%1%n%2), function, hook(MAP.concat), index(0), klabel(_MapBytesToBytes_), left, symbol, unit(.MapBytesToBytes)] syntax MapBytesToBytes ::= - ".MapBytesToBytes" [function, hook(MAP.unit), klabel(.MapBytesToBytes), latex(\dotCt{MapBytesToBytes}), symbol, total] + ".MapBytesToBytes" [function, hook(MAP.unit), klabel(.MapBytesToBytes), symbol, total] syntax MapBytesToBytes ::= - WrappedBytes "Bytes2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Bytes2Bytes|->_), latex({#1}\mapsto{#2}), symbol, total] + WrappedBytes "Bytes2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Bytes2Bytes|->_), symbol, total] syntax priorities _Bytes2Bytes|->_ > _MapBytesToBytes_ .MapBytesToBytes syntax non-assoc _Bytes2Bytes|->_ syntax WrappedBytes ::= @@ -2199,7 +2199,7 @@ module MAP-BYTES-TO-BYTES syntax MapBytesToBytes ::= MapBytesToBytes "[" WrappedBytes "<-" "undef" "]" [function, hook(MAP.remove), klabel(_MapBytesToBytes[_<-undef]), symbol, total] syntax MapBytesToBytes ::= - MapBytesToBytes "-Map" MapBytesToBytes [function, hook(MAP.difference), latex({#1}-_{\it MapBytesToBytesMap}{#2}), total] + MapBytesToBytes "-Map" MapBytesToBytes [function, hook(MAP.difference), total] syntax MapBytesToBytes ::= "updateMap" "(" MapBytesToBytes "," MapBytesToBytes ")" [function, hook(MAP.updateAll), klabel(updateMap), total] syntax MapBytesToBytes ::= @@ -2567,9 +2567,9 @@ module MAP-INT-TO-BYTES syntax MapIntToBytes ::= MapIntToBytes MapIntToBytes [assoc, comm, element(_Int2Bytes|->_), format(%1%n%2), function, hook(MAP.concat), index(0), klabel(_MapIntToBytes_), left, symbol, unit(.MapIntToBytes)] syntax MapIntToBytes ::= - ".MapIntToBytes" [function, hook(MAP.unit), klabel(.MapIntToBytes), latex(\dotCt{MapIntToBytes}), symbol, total] + ".MapIntToBytes" [function, hook(MAP.unit), klabel(.MapIntToBytes), symbol, total] syntax MapIntToBytes ::= - WrappedInt "Int2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Int2Bytes|->_), latex({#1}\mapsto{#2}), symbol, total] + WrappedInt "Int2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Int2Bytes|->_), symbol, total] syntax priorities _Int2Bytes|->_ > _MapIntToBytes_ .MapIntToBytes syntax non-assoc _Int2Bytes|->_ syntax WrappedBytes ::= @@ -2581,7 +2581,7 @@ module MAP-INT-TO-BYTES syntax MapIntToBytes ::= MapIntToBytes "[" WrappedInt "<-" "undef" "]" [function, hook(MAP.remove), klabel(_MapIntToBytes[_<-undef]), symbol, total] syntax MapIntToBytes ::= - MapIntToBytes "-Map" MapIntToBytes [function, hook(MAP.difference), latex({#1}-_{\it MapIntToBytesMap}{#2}), total] + MapIntToBytes "-Map" MapIntToBytes [function, hook(MAP.difference), total] syntax MapIntToBytes ::= "updateMap" "(" MapIntToBytes "," MapIntToBytes ")" [function, hook(MAP.updateAll), klabel(updateMap), total] syntax MapIntToBytes ::= @@ -5645,4 +5645,4 @@ module MANDOS syntax Bytes ::= "#incBytes" "(" val: Bytes "," inc: Int ")" [function, klabel(#incBytes)] rule #incBytes(VAL, INC) => Int2Bytes(Bytes2Int(VAL, BE, Signed) +Int INC, BE, Signed) -endmodule \ No newline at end of file +endmodule diff --git a/k-distribution/tests/profiling/pl-tutorial/imp/test.k b/k-distribution/tests/profiling/pl-tutorial/imp/test.k index 0ea81c6d477..404fbda6ad7 100644 --- a/k-distribution/tests/profiling/pl-tutorial/imp/test.k +++ b/k-distribution/tests/profiling/pl-tutorial/imp/test.k @@ -11,7 +11,7 @@ module IMP-SYNTAX > AExp "+" AExp [color(pink), left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [color(pink), latex({#1}\leq{#2}), seqstrict] + | AExp "<=" AExp [color(pink), seqstrict] | "!" BExp [color(pink), strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [color(pink), left, strict(1)] diff --git a/k-distribution/tests/profiling/pl-tutorial/lambda/test.k b/k-distribution/tests/profiling/pl-tutorial/lambda/test.k index 9b38dc8c2ef..417064f47da 100644 --- a/k-distribution/tests/profiling/pl-tutorial/lambda/test.k +++ b/k-distribution/tests/profiling/pl-tutorial/lambda/test.k @@ -32,7 +32,7 @@ module LAMBDA-SYNTAX imports public KVAR-SYNTAX syntax Val ::= KVar - | "lambda" KVar "." Exp [binder, latex(\lambda{#1}.{#2})] + | "lambda" KVar "." Exp [binder] syntax Exp ::= Val | Exp Exp [left, strict] @@ -53,7 +53,7 @@ module LAMBDA-SYNTAX rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro] - | "mu" KVar "." Exp [binder, latex(\mu{#1}.{#2})] + | "mu" KVar "." Exp [binder] rule letrec F:KVar X:KVar = E in E' => let F = mu F . lambda X . E in E' endmodule diff --git a/k-distribution/tests/regression-new/imp++-llvm/imp.md b/k-distribution/tests/regression-new/imp++-llvm/imp.md index 431fd9edf97..c6b54a3ca1c 100644 --- a/k-distribution/tests/regression-new/imp++-llvm/imp.md +++ b/k-distribution/tests/regression-new/imp++-llvm/imp.md @@ -131,7 +131,7 @@ of statements surrounded by curly brackets. > "spawn" Block > Id "=" AExp [strict(2)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/k-distribution/tests/regression-new/imp-haskell/imp.k b/k-distribution/tests/regression-new/imp-haskell/imp.k index 7bc04d1d0d4..defee40b702 100644 --- a/k-distribution/tests/regression-new/imp-haskell/imp.k +++ b/k-distribution/tests/regression-new/imp-haskell/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, seqstrict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/k-distribution/tests/regression-new/imp-json/imp.k b/k-distribution/tests/regression-new/imp-json/imp.k index 12be31219c2..40f29442395 100644 --- a/k-distribution/tests/regression-new/imp-json/imp.k +++ b/k-distribution/tests/regression-new/imp-json/imp.k @@ -9,7 +9,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict, color(pink)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | AExp "<=" AExp [seqstrict, color(pink)] | "!" BExp [strict, color(pink)] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1), color(pink)] diff --git a/k-distribution/tests/regression-new/imp-kore/imp.k b/k-distribution/tests/regression-new/imp-kore/imp.k index 69870bf8c8f..adf9f37e773 100644 --- a/k-distribution/tests/regression-new/imp-kore/imp.k +++ b/k-distribution/tests/regression-new/imp-kore/imp.k @@ -31,7 +31,7 @@ argument, because we want to give it a short-circuit semantics. */ | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict, color(pink)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | AExp "<=" AExp [seqstrict, color(pink)] | "!" BExp [strict, color(pink)] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1), color(pink)] diff --git a/k-distribution/tests/regression-new/imp-llvm/imp.k b/k-distribution/tests/regression-new/imp-llvm/imp.k index 56cd78b641c..ee2f8ce260b 100644 --- a/k-distribution/tests/regression-new/imp-llvm/imp.k +++ b/k-distribution/tests/regression-new/imp-llvm/imp.k @@ -11,7 +11,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict, color(pink)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | AExp "<=" AExp [seqstrict, color(pink)] | "!" BExp [strict, color(pink)] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1), color(pink)] diff --git a/k-distribution/tests/regression-new/issue-1760/test.k b/k-distribution/tests/regression-new/issue-1760/test.k index 01117e11792..7fc1b087108 100644 --- a/k-distribution/tests/regression-new/issue-1760/test.k +++ b/k-distribution/tests/regression-new/issue-1760/test.k @@ -18,9 +18,9 @@ module TEST // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + | "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)] @@ -66,19 +66,19 @@ module TEST /* syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), latex({#1}\mathrel{\ast_{\scriptstyle\it Kat}}{#2}), hook(KAT.mul)] + Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] > left: - Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), latex({#1}\mathrel{+_{\scriptstyle\it Kat}}{#2}), hook(KAT.seq)] + Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] > left: - Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), latex({#1}\mathrel{|_{\scriptstyle\it Kat}}{#2}), hook(KAT.pll)] + Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] */ syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), latex({#1}\mathrel{\ast_{\scriptstyle\it Kat}}{#2}), hook(KAT.mul)] - | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), latex({#1}\mathrel{+_{\scriptstyle\it Kat}}{#2}), hook(KAT.seq)] - | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), latex({#1}\mathrel{|_{\scriptstyle\it Kat}}{#2}), hook(KAT.pll)] + 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)] rule ONE Kat; B:Kat => B:Kat diff --git a/k-distribution/tests/regression-new/issue-1760/test.k.out b/k-distribution/tests/regression-new/issue-1760/test.k.out index a5da92020be..98dcbb73cf5 100644 --- a/k-distribution/tests/regression-new/issue-1760/test.k.out +++ b/k-distribution/tests/regression-new/issue-1760/test.k.out @@ -5,16 +5,16 @@ . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `notKat_`(_) Source(test.k) - Location(21,19,21,174) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,135) + 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(test.k) - Location(22,19,22,186) - 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(22,19,22,141) + 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_orKat__TEST_Kat_Kat_Kat`(_,_) Source(test.k) - Location(23,19,23,173) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(23,19,23,130) + 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/k-distribution/tests/regression-new/issue-999/kat.k b/k-distribution/tests/regression-new/issue-999/kat.k index cc4fcb9319a..ad420232c57 100644 --- a/k-distribution/tests/regression-new/issue-999/kat.k +++ b/k-distribution/tests/regression-new/issue-999/kat.k @@ -18,9 +18,9 @@ module KAT // Boolean Algebra Part of KAT syntax Kat ::= Bool - | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] + | "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)] @@ -66,19 +66,19 @@ module KAT /* syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), latex({#1}\mathrel{\ast_{\scriptstyle\it Kat}}{#2}), hook(KAT.mul)] + Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)] > left: - Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), latex({#1}\mathrel{+_{\scriptstyle\it Kat}}{#2}), hook(KAT.seq)] + Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)] > left: - Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), latex({#1}\mathrel{|_{\scriptstyle\it Kat}}{#2}), hook(KAT.pll)] + Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)] */ syntax Kat ::= "(" Kat ")" [bracket] > left: - Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), latex({#1}\mathrel{\ast_{\scriptstyle\it Kat}}{#2}), hook(KAT.mul)] - | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), latex({#1}\mathrel{+_{\scriptstyle\it Kat}}{#2}), hook(KAT.seq)] - | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), latex({#1}\mathrel{|_{\scriptstyle\it Kat}}{#2}), hook(KAT.pll)] + 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)] rule ONE Kat; B:Kat => B:Kat diff --git a/k-distribution/tests/regression-new/issue-999/kat.k.out b/k-distribution/tests/regression-new/issue-999/kat.k.out index 04d446fee84..d4a92c54985 100644 --- a/k-distribution/tests/regression-new/issue-999/kat.k.out +++ b/k-distribution/tests/regression-new/issue-999/kat.k.out @@ -5,16 +5,16 @@ . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `notKat_`(_) Source(kat.k) - Location(21,19,21,174) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), latex(\neg_{\scriptstyle\it Kat}{#1}), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,135) + 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(kat.k) - Location(22,19,22,186) - 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), latex({#1}\wedge_{\scriptstyle\it Kat}{#2}), hook(KAT.and)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(22,19,22,141) + 22 | > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_orKat__KAT_Kat_Kat_Kat`(_,_) Source(kat.k) - Location(23,19,23,173) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), latex({#1}\vee_{\scriptstyle\it Kat}{#2}), hook(KAT.or)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(23,19,23,130) + 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/k-distribution/tests/regression-new/krun-deserialize/imp.k b/k-distribution/tests/regression-new/krun-deserialize/imp.k index 9c29f705823..2373a7fe5e0 100644 --- a/k-distribution/tests/regression-new/krun-deserialize/imp.k +++ b/k-distribution/tests/regression-new/krun-deserialize/imp.k @@ -9,7 +9,7 @@ module IMP-SYNTAX > AExp "+" AExp [left, strict, color(pink)] | "(" AExp ")" [bracket] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | AExp "<=" AExp [seqstrict, color(pink)] | "!" BExp [strict, color(pink)] > BExp "&&" BExp [left, strict(1), color(pink)] | "(" BExp ")" [bracket] diff --git a/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k b/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k index 592fa48db29..15aa12449e0 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k +++ b/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k @@ -7,7 +7,7 @@ module LAMBDA-SYNTAX imports KVAR-SYNTAX syntax Val ::= KVar - | "lambda" KVar "." Exp [binder, latex(\lambda{#1}.{#2})] + | "lambda" KVar "." Exp [binder] syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] @@ -25,7 +25,7 @@ module LAMBDA-SYNTAX rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro] - | "mu" KVar "." Exp [binder, latex(\mu{#1}.{#2})] + | "mu" KVar "." Exp [binder] rule letrec F:KVar X = E in E' => let F = mu F . lambda X . E in E' endmodule diff --git a/k-distribution/tests/regression-new/pl-tutorial/1_k/2_imp/lesson_4/imp.k b/k-distribution/tests/regression-new/pl-tutorial/1_k/2_imp/lesson_4/imp.k index 35c69649bb1..59d6d507bb3 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/1_k/2_imp/lesson_4/imp.k +++ b/k-distribution/tests/regression-new/pl-tutorial/1_k/2_imp/lesson_4/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/k-distribution/tests/regression-new/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k b/k-distribution/tests/regression-new/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k index cd9e9213da9..b5ef701d2dc 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k +++ b/k-distribution/tests/regression-new/pl-tutorial/1_k/3_lambda++/lesson_5/lambda.k @@ -10,7 +10,7 @@ module LAMBDA syntax Exp ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] @@ -46,7 +46,7 @@ module LAMBDA rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro] - | "mu" Id "." Exp [latex(\mu{#1}.{#2})] + | "mu" Id "." Exp rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E' syntax Exp ::= muclosure(Map,Exp) diff --git a/k-distribution/tests/regression-new/pl-tutorial/1_k/4_imp++/lesson_7/imp.k b/k-distribution/tests/regression-new/pl-tutorial/1_k/4_imp++/lesson_7/imp.k index fef230a6925..d1e093058b8 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/1_k/4_imp++/lesson_7/imp.k +++ b/k-distribution/tests/regression-new/pl-tutorial/1_k/4_imp++/lesson_7/imp.k @@ -12,7 +12,7 @@ module IMP-SYNTAX > "spawn" Block > Id "=" AExp [strict(2)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md index d5cea45656e..e693e3b62e8 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/1_untyped/simple-untyped.md @@ -438,7 +438,7 @@ not mention these: the configuration context of the rule is automatically transformed to match the declared configuration structure. ```k - syntax KItem ::= "undefined" [latex(\bot)] + syntax KItem ::= "undefined" rule var X:Id; => . ... Env => Env[X <- L] @@ -1152,8 +1152,7 @@ corresponding store lookup operation. The following operation initializes a sequence of locations with the same value: ```k - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M ``` diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md index fbb607682e8..40792c86c35 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md @@ -222,7 +222,7 @@ location and then never allow that type to change. The typed undefined values effectively assign both a type and an undefined value to a location. ```k - syntax KItem ::= undefined(Type) [latex(\bot_{#1})] + syntax KItem ::= undefined(Type) rule T:Type X:Id; => . ... Env => Env[X <- L] @@ -578,8 +578,7 @@ Adds the corresponding depth to an array type ``` Sequences of locations. ```k - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map when N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md index 24d61397b4d..adfcd4fab41 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md @@ -381,7 +381,7 @@ object and method closures. The semantics below are taken verbatim from the untyped SIMPLE definition. ```k - syntax KItem ::= "undefined" [latex(\bot)] + syntax KItem ::= "undefined" rule var X:Id; => . ... Env => Env[X <- L] @@ -585,8 +585,7 @@ from SIMPLE unchanged. rule lvalue(lookup(L:Int) => loc(L)) - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map when N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K when N <=Int M ``` diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md index d716d40ad9b..24105e97e8a 100644 --- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md +++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md @@ -247,7 +247,7 @@ KOOL). syntax KResult ::= Vals - syntax KItem ::= undefined(Type) [latex(\bot_{#1})] + syntax KItem ::= undefined(Type) rule T:Type X:Id; => . ... Env => Env[X <- L] @@ -402,8 +402,7 @@ KOOL). rule T:Type<_,Vs:Vals> => T[] rule T:Type<.Vals> => T - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M 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 fe88145ec60..14de293b93a 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 @@ -891,7 +891,7 @@ is co-variant in the codomain and contra-variant in the domain). ## Generic operations which could be part of the **K** framework ```k - syntax KItem ::= stuck(K) [latex(\framebox{${#1}$})] + syntax KItem ::= stuck(K) syntax KItem ::= "discard" rule _:KResult ~> discard => . diff --git a/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out b/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out index 2d6852aa976..1d23c8966c1 100644 --- a/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out +++ b/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out @@ -3,13 +3,6 @@ SetItem ( X:MyId ) SetItem ( Z:MyId ) ) ~> . -#And - { - false - #Equals - X:MyId in SET - SetItem ( Z:MyId ) - } #And { false @@ -23,10 +16,4 @@ Z:MyId in SET SetItem ( X:MyId ) } -#And - { - false - #Equals - Z:MyId in SET - } [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details. diff --git a/k-distribution/tests/smoke/imp.k b/k-distribution/tests/smoke/imp.k index 35c69649bb1..59d6d507bb3 100644 --- a/k-distribution/tests/smoke/imp.k +++ b/k-distribution/tests/smoke/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index bc38572625e..e584bec01bf 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -69,6 +69,7 @@ private void checkProduction(Production prod) { checkFunctional(prod); checkTotal(prod); checkTerminatorKLabel(prod); + checkLatex(prod); } private void checkUnrecognizedAtts(T term) { @@ -327,4 +328,14 @@ private void checkTerminatorKLabel(Production prod) { prod)); } } + + private void checkLatex(Production prod) { + if (prod.att().contains(Att.LATEX())) { + kem.registerCompilerWarning( + ExceptionType.FUTURE_ERROR, + errors, + "The attribute 'latex' has been deprecated and all of its functionality has been removed. Using it will be an error in the future.", + prod); + } + } } diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/kernel/src/main/java/org/kframework/unparser/KPrint.java index 99633a6165b..7a9d3bd92be 100644 --- a/kernel/src/main/java/org/kframework/unparser/KPrint.java +++ b/kernel/src/main/java/org/kframework/unparser/KPrint.java @@ -144,7 +144,6 @@ public byte[] prettyPrint( case NONE: case BINARY: case JSON: - case LATEX: return serialize(result, outputMode); case PRETTY: Module prettyUnparsingModule = @@ -187,7 +186,6 @@ public static byte[] serialize(K term, OutputModes outputMode) { case NONE -> "".getBytes(); case BINARY -> ToBinary.apply(term); case JSON -> ToJson.apply(term); - case LATEX -> ToLatex.apply(term); default -> throw KEMException.criticalError("Unsupported serialization mode: " + outputMode); }; } diff --git a/kernel/src/main/java/org/kframework/unparser/OutputModes.java b/kernel/src/main/java/org/kframework/unparser/OutputModes.java index 5c402a25bbf..a9d270a2ecb 100644 --- a/kernel/src/main/java/org/kframework/unparser/OutputModes.java +++ b/kernel/src/main/java/org/kframework/unparser/OutputModes.java @@ -12,7 +12,6 @@ public enum OutputModes { KAST, BINARY, JSON, - LATEX, KORE, NONE; } diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java index 3e82b0ed4f3..415cd9e74bd 100644 --- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java +++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java @@ -66,7 +66,7 @@ public Class enumClass() { converter = OutputModeConverter.class, description = "How to display krun results. is either" - + " [pretty|program|kast|binary|json|latex|kore|none].") + + " [pretty|program|kast|binary|json|kore|none].") public OutputModes output = OutputModes.PRETTY; public static class OutputModeConverter extends BaseEnumConverter { diff --git a/kernel/src/main/java/org/kframework/unparser/ToLatex.java b/kernel/src/main/java/org/kframework/unparser/ToLatex.java deleted file mode 100644 index 85074d35a7b..00000000000 --- a/kernel/src/main/java/org/kframework/unparser/ToLatex.java +++ /dev/null @@ -1,131 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -package org.kframework.unparser; - -import java.io.ByteArrayOutputStream; -import java.io.DataOutputStream; -import java.io.IOException; -import java.nio.charset.StandardCharsets; -import java.util.Arrays; -import java.util.regex.Pattern; -import org.kframework.attributes.Att; -import org.kframework.kore.InjectedKLabel; -import org.kframework.kore.K; -import org.kframework.kore.KApply; -import org.kframework.kore.KAs; -import org.kframework.kore.KRewrite; -import org.kframework.kore.KSequence; -import org.kframework.kore.KToken; -import org.kframework.kore.KVariable; -import org.kframework.utils.StringUtil; -import org.kframework.utils.errorsystem.KEMException; - -/** Writes a KAST term to the LaTeX format. */ -public class ToLatex { - - public static byte[] apply(K k) { - try { - ByteArrayOutputStream out = new ByteArrayOutputStream(); - apply(new DataOutputStream(out), k); - return out.toByteArray(); - } catch (IOException e) { - throw KEMException.criticalError("Could not write K term to LaTeX", e, k); - } - } - - private static String[] asciiReadableEncodingLatexCalc() { - String[] latexEncoder = - Arrays.copyOf( - StringUtil.asciiReadableEncodingDefault, - StringUtil.asciiReadableEncodingDefault.length); - latexEncoder[0x30] = "Zero"; - latexEncoder[0x31] = "I"; - latexEncoder[0x32] = "II"; - latexEncoder[0x33] = "III"; - latexEncoder[0x34] = "IV"; - latexEncoder[0x35] = "V"; - latexEncoder[0x36] = "VI"; - latexEncoder[0x37] = "VII"; - latexEncoder[0x38] = "VIII"; - latexEncoder[0x39] = "IX"; - latexEncoder[0x7a] = "ActZ"; - return latexEncoder; - } - - public static final Pattern identChar = Pattern.compile("[A-Za-y]"); - public static String[] asciiReadableEncodingLatex = asciiReadableEncodingLatexCalc(); - - public static String latexedKLabel(String orig) { - StringBuilder buffer = new StringBuilder(); - StringUtil.encodeStringToAlphanumeric(buffer, orig, asciiReadableEncodingLatex, identChar, "z"); - return "klabel" + buffer; - } - - private static void writeString(DataOutputStream out, String str) throws IOException { - out.write(str.getBytes(StandardCharsets.UTF_8)); - } - - public static void apply(DataOutputStream out, Att att) throws IOException { - writeString(out, ("\\outerAtt{" + att.toString() + "}")); - } - - public static void apply(DataOutputStream out, K k) throws IOException { - if (k instanceof KToken tok) { - - writeString(out, ("\\texttt{ " + tok.s() + " }")); - - } else if (k instanceof KApply app) { - - writeString(out, ("\\" + latexedKLabel(app.klabel().name()))); - - for (K item : app.klist().asIterable()) { - writeString(out, "{"); - apply(out, item); - writeString(out, "}"); - } - - } else if (k instanceof KSequence kseq) { - - writeString(out, "\\kseq{"); - - for (K item : kseq.asIterable()) { - apply(out, item); - writeString(out, "}{\\kseq{"); - } - - writeString(out, "}{\\dotk{}}"); - - } else if (k instanceof KVariable var) { - - writeString(out, var.name()); - - } else if (k instanceof KRewrite rew) { - - writeString(out, "\\krewrites{"); - apply(out, rew.left()); - writeString(out, "}{"); - apply(out, rew.right()); - writeString(out, "}{"); - apply(out, rew.att()); - writeString(out, "}"); - - } else if (k instanceof KAs alias) { - - writeString(out, "\\kas{"); - apply(out, alias.pattern()); - writeString(out, "}{"); - apply(out, alias.alias()); - writeString(out, "}{"); - apply(out, alias.att()); - writeString(out, "}"); - - } else if (k instanceof InjectedKLabel inj) { - - writeString(out, "\\injectedklabel{"); - writeString(out, inj.klabel().name()); - writeString(out, "}"); - - } else { - throw KEMException.criticalError("Unimplemented for LaTeX serialization: ", k); - } - } -} diff --git a/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLone.properties b/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLone.properties deleted file mode 100755 index 5d29be77506..00000000000 --- a/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLone.properties +++ /dev/null @@ -1,34 +0,0 @@ -# This file supports replacements of type -# LATEX{#1} = HTML #1 HTML, LATEX{#1}{#2} = HTML #1 HTML #2 HTML, Latex{#1}{...}{#n} = HTML #1 ... #n HTML. - -# Use #1, #2, #3, ... to identify the group of characters in the command. -# Each #i is supposed to be between its own curly braces in the Latex commands. -# The n {#i} blocks are supposed to be on after each other in the Latex commands. - -# Do not put unescaped spaces in the keys. (Left side) - -# Some characters must be escaped with backslash. More info on : -# http://docs.oracle.com/javase/1.4.2/docs/api/java/util/Properties.html#load%28java.io.InputStream%29 - -# example : -# # a comment -# ! a comment - -# a = a string -# b = a string with escape sequences \t \n \r \\ \" \' \ (space) \u0123 -# c = a string with a continuation line \ -# continuation line -# d.e.f = another string - - -\\alert{#1} =
#1
-\\bluetext{#1} =
#1
-\\section{#1} =

#1


-\\subsection{#1} =

#1


-\\subsubsection{#1} =

#1


-\\texttt{#1} = #1 -\\textit{#1} = #1 -\\textsf{#1} = #1 -\\paragraph{#1}{#2} =

#1 #2

-{\\em#1} = #1 -\\href{#1}{#2} = #2 diff --git a/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLzero.properties b/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLzero.properties deleted file mode 100755 index 484ab06294e..00000000000 --- a/kernel/src/main/resources/org/kframework/backend/html/Latex2HTMLzero.properties +++ /dev/null @@ -1,41 +0,0 @@ -# This file supports simple replacements of type -# LATEX = HTML. - -# Some characters must be escaped with backslash. More info on : -# http://docs.oracle.com/javase/1.4.2/docs/api/java/util/Properties.html#load%28java.io.InputStream%29 - -# example : -# # a comment -# ! a comment - -# a = a string -# b = a string with escape sequences \t \n \r \\ \" \' \ (space) \u0123 -# c = a string with a continuation line \ -# continuation line -# d.e.f = another string - -\\@ = -\\, = -\\! = -{@} = @ -{\*} = * -\\K = K -\\textbackslash = \\ -{\\} = \\ -\\{ = { -\\} = } -\\texttildelow = ~ -\\begin{itemize} =
    -\\item =
  • -\\end{itemize} =
-\\begin{quote} =

-\\end{quote} =

-\\begin{verbatim} =

-\\end{verbatim} =

-\\c{s} = ş -\\c\ s = ş -\\c\ t = ț -\\c\ S = Ş -\\u\ a = ă -\\LaTeX\\ = LaTeX -\\kdot = •