Skip to content

Commit

Permalink
Remove latex attribute functionality (#3968)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@gtrepta
gtrepta authored Feb 9, 2024
1 parent 10e1a2b commit 9317222
Show file tree
Hide file tree
Showing 39 changed files with 136 additions and 354 deletions.
1 change: 0 additions & 1 deletion docs/user_manual.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
Expand Down
94 changes: 47 additions & 47 deletions k-distribution/include/kframework/builtin/domains.md
View file

Large diffs are not rendered by default.

5 changes: 2 additions & 3 deletions k-distribution/src/main/scripts/bin/kore-print
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down
5 changes: 2 additions & 3 deletions k-distribution/src/main/scripts/bin/krun
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/src/test/resources/compiler-tests/strategies_imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/src/test/resources/convertor-tests/imp_lesson1.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/src/test/resources/convertor-tests/imp_lesson2.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/src/test/resources/convertor-tests/kore_imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
16 changes: 8 additions & 8 deletions k-distribution/tests/profiling/elrond-semantics/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ::=
Expand Down Expand Up @@ -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 ::=
Expand All @@ -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 ::=
Expand Down Expand Up @@ -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 ::=
Expand All @@ -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 ::=
Expand Down Expand Up @@ -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
endmodule
2 changes: 1 addition & 1 deletion k-distribution/tests/profiling/pl-tutorial/imp/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/tests/profiling/pl-tutorial/lambda/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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

Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/imp++-llvm/imp.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/imp-haskell/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/imp-json/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/imp-kore/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/imp-llvm/imp.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
18 changes: 9 additions & 9 deletions k-distribution/tests/regression-new/issue-1760/test.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]

Expand Down Expand Up @@ -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
Expand Down
18 changes: 9 additions & 9 deletions k-distribution/tests/regression-new/issue-1760/test.k.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
. ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Loading

0 comments on commit 9317222

Please sign in to comment.